package smtlib-utils

  1. Overview
  2. Docs
package smtlib-utils
Legend:
Library
Module
Module type
Parameter
Class
Class type

Trivial AST for parsing

val pp_to_string : (Stdlib.Format.formatter -> 'a -> unit) -> 'b -> string
type var = string
type ty_var = string
type ty =
  1. | Ty_bool
  2. | Ty_real
  3. | Ty_app of ty_var * ty list
  4. | Ty_arrow of ty list * ty

Polymorphic types

type typed_var = var * ty
type arith_op =
  1. | Leq
  2. | Lt
  3. | Geq
  4. | Gt
  5. | Add
  6. | Minus
  7. | Mult
  8. | Div
type term =
  1. | True
  2. | False
  3. | Const of string
  4. | Arith of arith_op * term list
  5. | App of string * term list
  6. | HO_app of term * term
  7. | Match of term * match_branch list
  8. | If of term * term * term
  9. | Let of (var * term) list * term
  10. | Is_a of string * term
  11. | Fun of typed_var * term
  12. | Eq of term * term
  13. | Imply of term * term
  14. | And of term list
  15. | Or of term list
  16. | Not of term
  17. | Distinct of term list
  18. | Cast of term * ty
  19. | Forall of (var * ty) list * term
  20. | Exists of (var * ty) list * term
  21. | Attr of term * (string * string) list

AST: S-expressions with locations

and match_branch =
  1. | Match_default of term
  2. | Match_case of string * var list * term
type cstor = {
  1. cstor_ty_vars : ty_var list;
  2. cstor_name : string;
  3. cstor_args : (string * ty) list;
}
type 'arg fun_decl = {
  1. fun_ty_vars : ty_var list;
  2. fun_name : string;
  3. fun_args : 'arg list;
  4. fun_ret : ty;
}
type fun_def = {
  1. fr_decl : typed_var fun_decl;
  2. fr_body : term;
}
type funs_rec_def = {
  1. fsr_decls : typed_var fun_decl list;
  2. fsr_bodies : term list;
}
type prop_literal = string * bool
type statement = {
  1. stmt : stmt;
  2. loc : Smtlib_utils__.Loc.t option;
}
and stmt =
  1. | Stmt_set_logic of string
  2. | Stmt_set_info of string * string
  3. | Stmt_set_option of string list
  4. | Stmt_decl_sort of string * int
  5. | Stmt_decl of ty fun_decl
  6. | Stmt_fun_def of fun_def
  7. | Stmt_fun_rec of fun_def
  8. | Stmt_funs_rec of funs_rec_def
  9. | Stmt_data of ((string * int) * cstor list) list
  10. | Stmt_assert of term
  11. | Stmt_get_assertions
  12. | Stmt_get_assignment
  13. | Stmt_get_info of string
  14. | Stmt_get_model
  15. | Stmt_get_option of string
  16. | Stmt_get_proof
  17. | Stmt_get_unsat_assumptions
  18. | Stmt_get_unsat_core
  19. | Stmt_get_value of term list
  20. | Stmt_check_sat
  21. | Stmt_check_sat_assuming of prop_literal list
  22. | Stmt_pop of int
  23. | Stmt_push of int
  24. | Stmt_reset
  25. | Stmt_reset_assertions
  26. | Stmt_exit

Errors

exception Parse_error of Smtlib_utils__.Loc.t option * string
val parse_error : ?loc:Smtlib_utils__.Loc.t -> string -> 'a
val parse_errorf : ?loc:Smtlib_utils__.Loc.t -> ('a, unit, string, 'b) Stdlib.format4 -> 'c

Constructors

val ty_bool : ty
val ty_app : ty_var -> ty list -> ty
val ty_const : ty_var -> ty
val ty_real : ty
val ty_arrow_l : ty list -> ty -> ty
val ty_arrow : ty -> ty -> ty
val true_ : term
val false_ : term
val const : string -> term
val app : string -> term list -> term
val ho_app : term -> term -> term
val ho_app_l : term -> term list -> term
val match_ : term -> match_branch list -> term
val if_ : term -> term -> term -> term
val fun_ : typed_var -> term -> term
val fun_l : typed_var list -> term -> term
val let_ : (var * term) list -> term -> term
val eq : term -> term -> term
val imply : term -> term -> term
val is_a : string -> term -> term
val and_ : term list -> term
val or_ : term list -> term
val distinct : term list -> term
val cast : term -> ty:ty -> term
val forall : (var * ty) list -> term -> term
val exists : (var * ty) list -> term -> term
val attr : term -> (string * string) list -> term
val not_ : term -> term
val arith : arith_op -> term list -> term
val _mk : ?loc:Smtlib_utils__.Loc.t -> stmt -> statement
val mk_cstor : vars:ty_var list -> string -> (string * ty) list -> cstor
val mk_fun_decl : ty_vars:ty_var list -> string -> 'a list -> ty -> 'b fun_decl
val mk_fun_rec : ty_vars:ty_var list -> string -> typed_var list -> ty -> term -> fun_def
val decl_sort : ?loc:Smtlib_utils__.Loc.t -> string -> arity:int -> statement
val decl_fun : ?loc:Smtlib_utils__.Loc.t -> tyvars:ty_var list -> string -> ty list -> ty -> statement
val fun_def : ?loc:Smtlib_utils__.Loc.t -> fun_def -> statement
val fun_rec : ?loc:Smtlib_utils__.Loc.t -> fun_def -> statement
val funs_rec : ?loc:Smtlib_utils__.Loc.t -> typed_var fun_decl list -> term list -> statement
val data : ?loc:Smtlib_utils__.Loc.t -> ((string * int) * cstor list) list -> statement
val data_zip : ?loc:Smtlib_utils__.Loc.t -> (string * int) list -> cstor list list -> statement
val assert_ : ?loc:Smtlib_utils__.Loc.t -> term -> statement
val check_sat : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val check_sat_assuming : ?loc:Smtlib_utils__.Loc.t -> prop_literal list -> statement
val exit : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val set_logic : ?loc:Smtlib_utils__.Loc.t -> string -> statement
val set_info : ?loc:Smtlib_utils__.Loc.t -> string -> string -> statement
val get_info : ?loc:Smtlib_utils__.Loc.t -> string -> statement
val set_option : ?loc:Smtlib_utils__.Loc.t -> string list -> statement
val get_option : ?loc:Smtlib_utils__.Loc.t -> string -> statement
val push : ?loc:Smtlib_utils__.Loc.t -> int -> statement
val pop : ?loc:Smtlib_utils__.Loc.t -> int -> statement
val get_proof : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val get_model : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val get_assertions : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val get_assignment : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val get_value : ?loc:Smtlib_utils__.Loc.t -> term list -> statement
val get_unsat_core : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val get_unsat_assumptions : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val reset : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val reset_assertions : ?loc:Smtlib_utils__.Loc.t -> unit -> statement
val loc : statement -> Smtlib_utils__.Loc.t option
val view : statement -> stmt
val fpf : Stdlib.Format.formatter -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
val pp_list : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'b list -> unit
val pp_str : Stdlib.Format.formatter -> string -> unit
val pp_tyvar : Stdlib.Format.formatter -> string -> unit
val pp_ty : Stdlib.Format.formatter -> ty -> unit
val str_of_arith : arith_op -> string
val pp_arith : Stdlib.Format.formatter -> arith_op -> unit
val _lvl_top : int
val pp_typed_var : Stdlib.Format.formatter -> typed_var -> unit
val pp_term : Stdlib.Format.formatter -> term -> unit
val pp_par : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> (string list * 'b) -> unit
val pp_fun_decl : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'b fun_decl -> unit
val pp_fr : Stdlib.Format.formatter -> fun_def -> unit
val pp_prop_lit : Stdlib.Format.formatter -> (string * bool) -> unit
val pp_stmt : Stdlib.Format.formatter -> statement -> unit