Declaration of types *
val mk_abstract_type_decl : Loc.t -> string list -> string -> Parsed.declval mk_enum_type_decl :
Loc.t ->
string list ->
string ->
string list ->
Parsed.declval mk_algebraic_type_decl :
Loc.t ->
string list ->
string ->
(string * (string * Parsed.ppure_type) list) list ->
Parsed.declval mk_record_type_decl :
Loc.t ->
string list ->
string ->
?constr:string ->
(string * Parsed.ppure_type) list ->
Parsed.declval mk_rec_type_decl : Parsed.type_decl list -> Parsed.declDeclaration of symbols, functions, predicates, and goals
val mk_logic :
Loc.t ->
Symbols.name_kind ->
(string * string) list ->
Parsed.plogic_type ->
Parsed.declval mk_function_def :
Loc.t ->
(string * string) ->
(Loc.t * string * Parsed.ppure_type) list ->
Parsed.ppure_type ->
Parsed.lexpr ->
Parsed.declval mk_ground_predicate_def :
Loc.t ->
(string * string) ->
Parsed.lexpr ->
Parsed.declval mk_non_ground_predicate_def :
Loc.t ->
(string * string) ->
(Loc.t * string * Parsed.ppure_type) list ->
Parsed.lexpr ->
Parsed.declval mk_mut_rec_def :
(Loc.t
* (string * string)
* (Loc.t * string * Parsed.ppure_type) list
* Parsed.ppure_type option
* Parsed.lexpr)
list ->
Parsed.declval mk_goal : Loc.t -> string -> Parsed.lexpr -> Parsed.declval mk_check_sat : Loc.t -> string -> Parsed.lexpr -> Parsed.declDeclaration of theories, generic axioms and rewriting rules *
val mk_theory : Loc.t -> string -> string -> Parsed.decl list -> Parsed.declval mk_generic_axiom : Loc.t -> string -> Parsed.lexpr -> Parsed.declval mk_rewriting : Loc.t -> string -> Parsed.lexpr list -> Parsed.declDeclaration of theory axioms and case-splits *
val mk_theory_axiom : Loc.t -> string -> Parsed.lexpr -> Parsed.declval mk_theory_case_split : Loc.t -> string -> Parsed.lexpr -> Parsed.declDeclaration of stack assertions commands
val mk_push : Loc.t -> int -> Parsed.declval mk_pop : Loc.t -> int -> Parsed.declDeclaration of optimization of objective functions.
val mk_optimize : Loc.t -> Parsed.lexpr -> bool -> Parsed.declMaking pure and logic types
val int_type : Parsed.ppure_typeval bool_type : Parsed.ppure_typeval real_type : Parsed.ppure_typeval unit_type : Parsed.ppure_typeval mk_bitv_type : string -> Parsed.ppure_typeval mk_external_type :
Loc.t ->
Parsed.ppure_type list ->
string ->
Parsed.ppure_typeval mk_var_type : Loc.t -> string -> Parsed.ppure_typeval mk_logic_type :
Parsed.ppure_type list ->
Parsed.ppure_type option ->
Parsed.plogic_typeMaking arithmetic expressions and predicates *
val mk_int_const : Loc.t -> string -> Parsed.lexprval mk_real_const : Loc.t -> Numbers.Q.t -> Parsed.lexprval mk_add : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_sub : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_mul : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_div : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_mod : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_pow_int : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_pow_real : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_minus : Loc.t -> Parsed.lexpr -> Parsed.lexprval mk_pred_lt : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_pred_le : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_pred_gt : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_pred_ge : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprMaking Record expressions *
val mk_record : Loc.t -> (string * Parsed.lexpr) list -> Parsed.lexprval mk_with_record :
Loc.t ->
Parsed.lexpr ->
(string * Parsed.lexpr) list ->
Parsed.lexprval mk_dot_record : Loc.t -> Parsed.lexpr -> string -> Parsed.lexprMaking Array expressions *
val mk_array_get : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_array_set :
Loc.t ->
Parsed.lexpr ->
Parsed.lexpr ->
Parsed.lexpr ->
Parsed.lexprMaking Bit-vector expressions *
val mk_bitv_const : Loc.t -> string -> Parsed.lexprval mk_bitv_extract : Loc.t -> Parsed.lexpr -> string -> string -> Parsed.lexprval mk_bitv_concat : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprMaking Boolean / Propositional expressions *
val mk_true_const : Loc.t -> Parsed.lexprval mk_false_const : Loc.t -> Parsed.lexprval mk_and : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_or : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_xor : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_iff : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_implies : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_not : Loc.t -> Parsed.lexpr -> Parsed.lexprval mk_distinct : Loc.t -> Parsed.lexpr list -> Parsed.lexprval mk_pred_eq : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprval mk_pred_not_eq : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexprMaking quantified formulas *
val mk_forall :
Loc.t ->
(string * string * Parsed.ppure_type) list ->
(Parsed.lexpr list * bool) list ->
Parsed.lexpr list ->
Parsed.lexpr ->
Parsed.lexprval mk_exists :
Loc.t ->
(string * string * Parsed.ppure_type) list ->
(Parsed.lexpr list * bool) list ->
Parsed.lexpr list ->
Parsed.lexpr ->
Parsed.lexprNaming and casting types of expressions *
val mk_type_cast : Loc.t -> Parsed.lexpr -> Parsed.ppure_type -> Parsed.lexprval mk_named : Loc.t -> string -> Parsed.lexpr -> Parsed.lexprMaking vars, applications, if-then-else, and let expressions *
val mk_var : Loc.t -> string -> Parsed.lexprval mk_application : Loc.t -> string -> Parsed.lexpr list -> Parsed.lexprval mk_pattern : Loc.t -> string -> string list -> Parsed.patternval mk_ite :
Loc.t ->
Parsed.lexpr ->
Parsed.lexpr ->
Parsed.lexpr ->
Parsed.lexprval mk_let :
Loc.t ->
(string * Parsed.lexpr) list ->
Parsed.lexpr ->
Parsed.lexprval mk_void : Loc.t -> Parsed.lexprMaking particular expression used in semantic triggers *
val mk_in_interval :
Loc.t ->
Parsed.lexpr ->
bool ->
Parsed.lexpr ->
Parsed.lexpr ->
bool ->
Parsed.lexprval mk_maps_to : Loc.t -> string -> Parsed.lexpr -> Parsed.lexprMaking cuts and checks *
val mk_check : Loc.t -> Parsed.lexpr -> Parsed.lexprval mk_cut : Loc.t -> Parsed.lexpr -> Parsed.lexprval mk_match :
Loc.t ->
Parsed.lexpr ->
(Parsed.pattern * Parsed.lexpr) list ->
Parsed.lexprval mk_algebraic_test : Loc.t -> Parsed.lexpr -> string -> Parsed.lexprval mk_algebraic_project : Loc.t -> Parsed.lexpr -> string -> Parsed.lexpr