diff --git a/ml/z3.ml b/ml/z3.ml index a34c3eb57..76536ef43 100644 --- a/ml/z3.ml +++ b/ml/z3.ml @@ -198,6 +198,7 @@ and decl_kind = | OP_PR_SKOLEMIZE | OP_PR_MODUS_PONENS_OEQ | OP_PR_TH_LEMMA + | OP_PR_HYPER_RESOLVE | OP_RA_STORE | OP_RA_EMPTY | OP_RA_IS_EMPTY @@ -342,6 +343,9 @@ external param_descrs_size : context -> param_descrs -> int external param_descrs_get_name : context -> param_descrs -> int -> symbol = "camlidl_z3_Z3_param_descrs_get_name" +external param_descrs_to_string : context -> param_descrs -> string + = "camlidl_z3_Z3_param_descrs_to_string" + (** Refined view of a {!symbol}. @@ -2153,6 +2157,7 @@ and decl_kind = | OP_PR_SKOLEMIZE | OP_PR_MODUS_PONENS_OEQ | OP_PR_TH_LEMMA + | OP_PR_HYPER_RESOLVE | OP_RA_STORE | OP_RA_EMPTY | OP_RA_IS_EMPTY diff --git a/ml/z3.mli b/ml/z3.mli index c91729c3c..b0935f03c 100644 --- a/ml/z3.mli +++ b/ml/z3.mli @@ -198,6 +198,7 @@ and decl_kind = | OP_PR_SKOLEMIZE | OP_PR_MODUS_PONENS_OEQ | OP_PR_TH_LEMMA + | OP_PR_HYPER_RESOLVE | OP_RA_STORE | OP_RA_EMPTY | OP_RA_IS_EMPTY @@ -886,6 +887,47 @@ and goal_prec = - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. + - OP_PR_HYPER_RESOLVE: Hyper-resolution rule. + + The premises of the rules is a sequence of clauses. + The first clause argument is the main clause of the rule. + One literal from the second, third, .. clause is resolved + with a literal from the first (main) clause. + + Premises of the rules are of the form + {e + (or l0 l1 l2 .. ln) + } + or + {e + (=> (and ln+1 ln+2 .. ln+m) l0) + } + or in the most general (ground) form: + {e + (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)) + } + In other words we use the following (Prolog style) convention for Horn + implications: + The head of a Horn implication is position 0, + the first conjunct in the body of an implication is position 1 + the second conjunct in the body of an implication is position 2 + + For general implications where the head is a disjunction, the + first n positions correspond to the n disjuncts in the head. + The next m positions correspond to the m conjuncts in the body. + + The premises can be universally quantified so that the most + general non-ground form is: + + {e + (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))) + } + + The hyper-resolution rule takes a sequence of parameters. + The parameters are substitutions of bound variables separated by pairs + of literal positions from the main clause and side clause. + + - OP_RA_STORE: Insert a record into a relation. The function takes [n+1] arguments, where the first argument is the relation and the remaining [n] elements correspond to the [n] columns of the relation. @@ -1010,6 +1052,36 @@ and goal_prec = - DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized. - EXCEPTION: Internal Z3 exception. Additional details can be retrieved using {!get_error_msg}. *) +(** + Definitions for update_api.py + + def_Type('CONFIG', 'config', 'Config') + def_Type('CONTEXT', 'context', 'ContextObj') + def_Type('AST', 'ast', 'Ast') + def_Type('APP', 'app', 'Ast') + def_Type('SORT', 'sort', 'Sort') + def_Type('FUNC_DECL', 'func_decl', 'FuncDecl') + def_Type('PATTERN', 'pattern', 'Pattern') + def_Type('MODEL', 'model', 'Model') + def_Type('LITERALS', 'literals', 'Literals') + def_Type('CONSTRUCTOR', 'constructor', 'Constructor') + def_Type('CONSTRUCTOR_LIST', 'constructor_list', 'ConstructorList') + def_Type('THEORY', 'theory', 'ctypes.c_void_p') + def_Type('THEORY_DATA', 'theory_data', 'ctypes.c_void_p') + def_Type('SOLVER', 'solver', 'SolverObj') + def_Type('GOAL', 'goal', 'GoalObj') + def_Type('TACTIC', 'tactic', 'TacticObj') + def_Type('PARAMS', 'params', 'Params') + def_Type('PROBE', 'probe', 'ProbeObj') + def_Type('STATS', 'stats', 'StatsObj') + def_Type('AST_VECTOR', 'ast_vector', 'AstVectorObj') + def_Type('AST_MAP', 'ast_map', 'AstMapObj') + def_Type('APPLY_RESULT', 'apply_result', 'ApplyResultObj') + def_Type('FUNC_INTERP', 'func_interp', 'FuncInterpObj') + def_Type('FUNC_ENTRY', 'func_entry', 'FuncEntryObj') + def_Type('FIXEDPOINT', 'fixedpoint', 'FixedpointObj') + def_Type('PARAM_DESCRS', 'param_descrs', 'ParamDescrs') +*) (** Exceptions raised by Z3. It is safe to continue interacting with Z3 after catching [Error] exceptions. @@ -1040,6 +1112,8 @@ exception Error of context * error_code + + def_API('mk_context', CONTEXT, (_in(CONFIG),)) *) external mk_context: (string * string) list -> context = "caml_z3_mk_context" @@ -1057,6 +1131,8 @@ external mk_context: (string * string) list -> context = "caml_z3_mk_context" - {b See also}: {!mk_context } + + def_API('update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING))) *) external update_param_value : context -> string -> string -> unit = "camlidl_z3_Z3_update_param_value" @@ -1070,6 +1146,8 @@ external update_param_value : context -> string -> string -> unit - {b See also}: {!mk_context } + + def_API('get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING))) *) external get_param_value : context -> string -> string option = "camlidl_z3_Z3_get_param_value" @@ -1077,6 +1155,8 @@ external get_param_value : context -> string -> string option (** Summary: Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics. + + def_API('interrupt', VOID, (_in(CONTEXT),)) *) external interrupt : context -> unit = "camlidl_z3_Z3_interrupt" @@ -1091,30 +1171,40 @@ external interrupt : context -> unit + + def_API('mk_params', PARAMS, (_in(CONTEXT),)) *) external mk_params : context -> params = "camlidl_z3_Z3_mk_params" (** Summary: Add a Boolean parameter [k] with value [v] to the parameter set [p]. + + def_API('params_set_bool', VOID, (_in(CONTEXT), _in(PARAMS), _in(SYMBOL), _in(BOOL))) *) external params_set_bool : context -> params -> symbol -> bool -> unit = "camlidl_z3_Z3_params_set_bool" (** Summary: Add a unsigned int parameter [k] with value [v] to the parameter set [p]. + + def_API('params_set_uint', VOID, (_in(CONTEXT), _in(PARAMS), _in(SYMBOL), _in(UINT))) *) external params_set_uint : context -> params -> symbol -> int -> unit = "camlidl_z3_Z3_params_set_uint" (** Summary: Add a double parameter [k] with value [v] to the parameter set [p]. + + def_API('params_set_double', VOID, (_in(CONTEXT), _in(PARAMS), _in(SYMBOL), _in(DOUBLE))) *) external params_set_double : context -> params -> symbol -> float -> unit = "camlidl_z3_Z3_params_set_double" (** Summary: Add a symbol parameter [k] with value [v] to the parameter set [p]. + + def_API('params_set_symbol', VOID, (_in(CONTEXT), _in(PARAMS), _in(SYMBOL), _in(SYMBOL))) *) external params_set_symbol : context -> params -> symbol -> symbol -> unit = "camlidl_z3_Z3_params_set_symbol" @@ -1122,6 +1212,8 @@ external params_set_symbol : context -> params -> symbol -> symbol -> unit (** Summary: Convert a parameter set into a string. This function is mainly used for printing the contents of a parameter set. + + def_API('params_to_string', STRING, (_in(CONTEXT), _in(PARAMS))) *) external params_to_string : context -> params -> string = "camlidl_z3_Z3_params_to_string" @@ -1130,6 +1222,8 @@ external params_to_string : context -> params -> string Summary: Validate the parameter set [p] against the parameter description set [d]. The procedure invokes the error handler if [p] is invalid. + + def_API('params_validate', VOID, (_in(CONTEXT), _in(PARAMS), _in(PARAM_DESCRS))) *) external params_validate : context -> params -> param_descrs -> unit = "camlidl_z3_Z3_params_validate" @@ -1139,12 +1233,16 @@ external params_validate : context -> params -> param_descrs -> unit *) (** Summary: Return the kind associated with the given parameter name [n]. + + def_API('param_descrs_get_kind', UINT, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL))) *) external param_descrs_get_kind : context -> param_descrs -> symbol -> param_kind = "camlidl_z3_Z3_param_descrs_get_kind" (** Summary: Return the number of parameters in the given parameter description set. + + def_API('param_descrs_size', UINT, (_in(CONTEXT), _in(PARAM_DESCRS))) *) external param_descrs_size : context -> param_descrs -> int = "camlidl_z3_Z3_param_descrs_size" @@ -1153,10 +1251,21 @@ external param_descrs_size : context -> param_descrs -> int Summary: Return the number of parameters in the given parameter description set. - {b Precondition}: i < param_descrs_size c p + + def_API('param_descrs_get_name', SYMBOL, (_in(CONTEXT), _in(PARAM_DESCRS), _in(UINT))) *) external param_descrs_get_name : context -> param_descrs -> int -> symbol = "camlidl_z3_Z3_param_descrs_get_name" +(** + Summary: Convert a parameter description set into a string. This function is mainly used for printing the + contents of a parameter description set. + + def_API('param_descrs_to_string', STRING, (_in(CONTEXT), _in(PARAM_DESCRS))) +*) +external param_descrs_to_string : context -> param_descrs -> string + = "camlidl_z3_Z3_param_descrs_to_string" + (** {2 {L Symbols}} *) @@ -1191,6 +1300,8 @@ val mk_symbol: context -> symbol_refined -> symbol The legal range of unsigned int integers is 0 to 2^30-1. - {b See also}: {!mk_string_symbol} + + def_API('mk_int_symbol', SYMBOL, (_in(CONTEXT), _in(INT))) *) external mk_int_symbol : context -> int -> symbol = "camlidl_z3_Z3_mk_int_symbol" @@ -1201,6 +1312,8 @@ external mk_int_symbol : context -> int -> symbol Symbols are used to name several term and type constructors. - {b See also}: {!mk_int_symbol} + + def_API('mk_string_symbol', SYMBOL, (_in(CONTEXT), _in(STRING))) *) external mk_string_symbol : context -> string -> symbol = "camlidl_z3_Z3_mk_string_symbol" @@ -1281,6 +1394,8 @@ val mk_datatypes: context -> (sort array -> (datatype_desc array) option) -> dat Summary: Create a free (uninterpreted) type using the given name (symbol). Two free types are considered the same iff the have the same name. + + def_API('mk_uninterpreted_sort', SORT, (_in(CONTEXT), _in(SYMBOL))) *) external mk_uninterpreted_sort : context -> symbol -> sort = "camlidl_z3_Z3_mk_uninterpreted_sort" @@ -1289,6 +1404,8 @@ external mk_uninterpreted_sort : context -> symbol -> sort Summary: Create the Boolean type. This type is used to create propositional variables and predicates. + + def_API('mk_bool_sort', SORT, (_in(CONTEXT), )) *) external mk_bool_sort : context -> sort = "camlidl_z3_Z3_mk_bool_sort" @@ -1301,6 +1418,8 @@ external mk_bool_sort : context -> sort {!mk_bv_sort} creates a bit-vector type. - {b See also}: {!mk_bv_sort} + + def_API('mk_int_sort', SORT, (_in(CONTEXT), )) *) external mk_int_sort : context -> sort = "camlidl_z3_Z3_mk_int_sort" @@ -1310,6 +1429,8 @@ external mk_int_sort : context -> sort This type is not a floating point number. Z3 does not have support for floating point numbers yet. + + def_API('mk_real_sort', SORT, (_in(CONTEXT), )) *) external mk_real_sort : context -> sort = "camlidl_z3_Z3_mk_real_sort" @@ -1320,6 +1441,8 @@ external mk_real_sort : context -> sort This type can also be seen as a machine integer. - {b Remarks}: The size of the bitvector type must be greater than zero. + + def_API('mk_bv_sort', SORT, (_in(CONTEXT), _in(UINT))) *) external mk_bv_sort : context -> int -> sort = "camlidl_z3_Z3_mk_bv_sort" @@ -1332,6 +1455,8 @@ external mk_bv_sort : context -> int -> sort constant together with the sort returned by this call. - {b See also}: {!get_finite_domain_sort_size.} + + def_API('mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64))) *) external mk_finite_domain_sort : context -> symbol -> int64 -> sort = "camlidl_z3_Z3_mk_finite_domain_sort" @@ -1344,6 +1469,8 @@ external mk_finite_domain_sort : context -> symbol -> int64 -> sort - {b See also}: {!mk_select} - {b See also}: {!mk_store} + + def_API('mk_array_sort', SORT, (_in(CONTEXT), _in(SORT), _in(SORT))) *) external mk_array_sort : context -> sort -> sort -> sort = "camlidl_z3_Z3_mk_array_sort" @@ -1365,6 +1492,8 @@ external mk_array_sort : context -> sort -> sort -> sort @param field_sorts type of the tuple fields. @param mk_tuple_decl output parameter that will contain the constructor declaration. @param proj_decl output parameter that will contain the projection function declarations. This field must be a buffer of size [num_fields] allocated by the user. + + def_API('mk_tuple_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _out(FUNC_DECL), _out_array(2, FUNC_DECL))) *) external mk_tuple_sort : context -> symbol -> symbol array -> sort array -> sort * func_decl * func_decl array = "camlidl_z3_Z3_mk_tuple_sort" @@ -1392,6 +1521,8 @@ external mk_tuple_sort : context -> symbol -> symbol array -> sort array -> sort [enum_consts]. The array [enum_testers] has three predicates of type {e (s -> Bool) }. The first predicate (corresponding to A) is true when applied to A, and false otherwise. Similarly for the other predicates. + + def_API('mk_enumeration_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SYMBOL), _out_array(2, FUNC_DECL), _out_array(2, FUNC_DECL))) *) external mk_enumeration_sort : context -> symbol -> symbol array -> sort * func_decl array * func_decl array = "camlidl_z3_Z3_mk_enumeration_sort" @@ -1414,6 +1545,8 @@ external mk_enumeration_sort : context -> symbol -> symbol array -> sort * func_ @param is_cons_decl cons cell test. @param head_decl list head. @param tail_decl list tail. + + def_API('mk_list_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(SORT), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL))) *) external mk_list_sort : context -> symbol -> sort -> sort * func_decl * func_decl * func_decl * func_decl * func_decl * func_decl = "camlidl_z3_Z3_mk_list_sort" @@ -1433,6 +1566,8 @@ external mk_list_sort : context -> symbol -> sort -> sort * func_decl * func_dec sort reference is [None], then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. + + def_API('mk_constructor', CONSTRUCTOR, (_in(CONTEXT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(3, SYMBOL), _in_array(3, SORT), _in_array(3, UINT))) *) external mk_constructor : context -> symbol -> symbol -> symbol array -> sort option array -> int array -> constructor = "camlidl_z3_Z3_mk_constructor_bytecode" "camlidl_z3_Z3_mk_constructor" @@ -1442,6 +1577,8 @@ external mk_constructor : context -> symbol -> symbol -> symbol array -> sort op @param c logical context. @param constr constructor. + + def_API('del_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR))) *) external del_constructor : context -> constructor -> unit = "camlidl_z3_Z3_del_constructor" @@ -1454,6 +1591,8 @@ external del_constructor : context -> constructor -> unit @param name name of datatype. @param num_constructors number of constructors passed in. @param constructors array of constructor containers. + + def_API('mk_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _inout_array(2, CONSTRUCTOR))) *) external mk_datatype : context -> symbol -> constructor array -> sort * constructor array = "camlidl_z3_Z3_mk_datatype" @@ -1464,6 +1603,8 @@ external mk_datatype : context -> symbol -> constructor array -> sort * construc @param c logical context. @param num_constructors number of constructors in list. @param constructors list of constructors. + + def_API('mk_constructor_list', CONSTRUCTOR_LIST, (_in(CONTEXT), _in(UINT), _in_array(1, CONSTRUCTOR))) *) external mk_constructor_list : context -> constructor array -> constructor_list = "camlidl_z3_Z3_mk_constructor_list" @@ -1476,6 +1617,7 @@ external mk_constructor_list : context -> constructor array -> constructor_list @param c logical context. @param clist constructor list container. + def_API('del_constructor_list', VOID, (_in(CONTEXT), _in(CONSTRUCTOR_LIST))) *) external del_constructor_list : context -> constructor_list -> unit = "camlidl_z3_Z3_del_constructor_list" @@ -1488,6 +1630,8 @@ external del_constructor_list : context -> constructor_list -> unit @param sort_names names of datatype sorts. @param sorts array of datattype sorts. @param constructor_lists list of constructors, one list per sort. + + def_API('mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST))) *) external mk_datatypes : context -> symbol array -> constructor_list array -> sort array * constructor_list array = "camlidl_z3_Z3_mk_datatypes" @@ -1501,6 +1645,8 @@ external mk_datatypes : context -> symbol array -> constructor_list array -> sor @param constructor constructor function declaration. @param tester constructor test function declaration. @param accessors array of accessor function declarations. + + def_API('query_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR), _in(UINT), _out(FUNC_DECL), _out(FUNC_DECL), _out_array(2, FUNC_DECL))) *) external query_constructor : context -> constructor -> int -> func_decl * func_decl * func_decl array = "camlidl_z3_Z3_query_constructor" @@ -1526,6 +1672,8 @@ external query_constructor : context -> constructor -> int -> func_decl * func_d application. - {b See also}: {!mk_app} + + def_API('mk_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) *) external mk_func_decl : context -> symbol -> sort array -> sort -> func_decl = "camlidl_z3_Z3_mk_func_decl" @@ -1534,6 +1682,8 @@ external mk_func_decl : context -> symbol -> sort array -> sort -> func_decl Summary: Create a constant or function application. - {b See also}: {!mk_func_decl} + + def_API('mk_app', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST))) *) external mk_app : context -> func_decl -> ast array -> ast = "camlidl_z3_Z3_mk_app" @@ -1551,6 +1701,8 @@ external mk_app : context -> func_decl -> ast array -> ast - {b See also}: {!mk_func_decl} - {b See also}: {!mk_app} + + def_API('mk_const', AST, (_in(CONTEXT), _in(SYMBOL), _in(SORT))) *) external mk_const : context -> symbol -> sort -> ast = "camlidl_z3_Z3_mk_const" @@ -1564,6 +1716,8 @@ external mk_const : context -> symbol -> sort -> ast - {b See also}: {!mk_func_decl} + + def_API('mk_fresh_func_decl', FUNC_DECL, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SORT), _in(SORT))) *) external mk_fresh_func_decl : context -> string -> sort array -> sort -> func_decl = "camlidl_z3_Z3_mk_fresh_func_decl" @@ -1580,6 +1734,8 @@ external mk_fresh_func_decl : context -> string -> sort array -> sort -> func_de - {b See also}: {!mk_func_decl} - {b See also}: {!mk_app} + + def_API('mk_fresh_const', AST, (_in(CONTEXT), _in(STRING), _in(SORT))) *) external mk_fresh_const : context -> string -> sort -> ast = "camlidl_z3_Z3_mk_fresh_const" @@ -1589,12 +1745,16 @@ external mk_fresh_const : context -> string -> sort -> ast *) (** Summary: Create an AST node representing [true]. + + def_API('mk_true', AST, (_in(CONTEXT), )) *) external mk_true : context -> ast = "camlidl_z3_Z3_mk_true" (** Summary: Create an AST node representing [false]. + + def_API('mk_false', AST, (_in(CONTEXT), )) *) external mk_false : context -> ast = "camlidl_z3_Z3_mk_false" @@ -1604,6 +1764,8 @@ external mk_false : context -> ast Create an AST node representing {e l = r }. The nodes [l] and [r] must have the same type. + + def_API('mk_eq', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_eq : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_eq" @@ -1620,6 +1782,8 @@ external mk_eq : context -> ast -> ast -> ast All arguments must have the same sort. - {b Remarks}: The number of arguments of a distinct construct must be greater than one. + + def_API('mk_distinct', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_distinct : context -> ast array -> ast = "camlidl_z3_Z3_mk_distinct" @@ -1629,6 +1793,8 @@ external mk_distinct : context -> ast array -> ast Create an AST node representing {e not(a) }. The node [a] must have Boolean sort. + + def_API('mk_not', AST, (_in(CONTEXT), _in(AST))) *) external mk_not : context -> ast -> ast = "camlidl_z3_Z3_mk_not" @@ -1640,6 +1806,8 @@ external mk_not : context -> ast -> ast The node [t1] must have Boolean sort, [t2] and [t3] must have the same sort. The sort of the new node is equal to the sort of [t2] and [t3]. + + def_API('mk_ite', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) *) external mk_ite : context -> ast -> ast -> ast -> ast = "camlidl_z3_Z3_mk_ite" @@ -1649,6 +1817,8 @@ external mk_ite : context -> ast -> ast -> ast -> ast Create an AST node representing {e t1 iff t2 }. The nodes [t1] and [t2] must have Boolean sort. + + def_API('mk_iff', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_iff : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_iff" @@ -1658,6 +1828,8 @@ external mk_iff : context -> ast -> ast -> ast Create an AST node representing {e t1 implies t2 }. The nodes [t1] and [t2] must have Boolean sort. + + def_API('mk_implies', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_implies : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_implies" @@ -1667,6 +1839,8 @@ external mk_implies : context -> ast -> ast -> ast Create an AST node representing {e t1 xor t2 }. The nodes [t1] and [t2] must have Boolean sort. + + def_API('mk_xor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_xor : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_xor" @@ -1679,6 +1853,8 @@ external mk_xor : context -> ast -> ast -> ast All arguments must have Boolean sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_and', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_and : context -> ast array -> ast = "camlidl_z3_Z3_mk_and" @@ -1691,6 +1867,8 @@ external mk_and : context -> ast array -> ast All arguments must have Boolean sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_or', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_or : context -> ast array -> ast = "camlidl_z3_Z3_mk_or" @@ -1706,6 +1884,8 @@ external mk_or : context -> ast array -> ast All arguments must have int or real sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_add', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_add : context -> ast array -> ast = "camlidl_z3_Z3_mk_add" @@ -1719,6 +1899,8 @@ external mk_add : context -> ast array -> ast - {b Remarks}: Z3 has limited support for non-linear arithmetic. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_mul', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_mul : context -> ast array -> ast = "camlidl_z3_Z3_mk_mul" @@ -1731,6 +1913,8 @@ external mk_mul : context -> ast array -> ast All arguments must have int or real sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_sub', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_sub : context -> ast array -> ast = "camlidl_z3_Z3_mk_sub" @@ -1740,6 +1924,8 @@ external mk_sub : context -> ast array -> ast Summary: \[ [mk_unary_minus c arg] \] Create the term: {e - arg}. The arguments must have int or real type. + + def_API('mk_unary_minus', AST, (_in(CONTEXT), _in(AST))) *) external mk_unary_minus : context -> ast -> ast = "camlidl_z3_Z3_mk_unary_minus" @@ -1752,6 +1938,7 @@ external mk_unary_minus : context -> ast -> ast If the arguments have int type, then the result type is an int type, otherwise the the result type is real. + def_API('mk_div', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_div : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_div" @@ -1762,6 +1949,7 @@ external mk_div : context -> ast -> ast -> ast The arguments must have int type. + def_API('mk_mod', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_mod : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_mod" @@ -1772,6 +1960,7 @@ external mk_mod : context -> ast -> ast -> ast The arguments must have int type. + def_API('mk_rem', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_rem : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_rem" @@ -1780,6 +1969,8 @@ external mk_rem : context -> ast -> ast -> ast The arguments must have int or real type. + + def_API('mk_power', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_power : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_power" @@ -1789,6 +1980,8 @@ external mk_power : context -> ast -> ast -> ast Create less than. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_lt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_lt : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_lt" @@ -1798,6 +1991,8 @@ external mk_lt : context -> ast -> ast -> ast Create less than or equal to. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_le', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_le : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_le" @@ -1807,6 +2002,8 @@ external mk_le : context -> ast -> ast -> ast Create greater than. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_gt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_gt : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_gt" @@ -1816,6 +2013,8 @@ external mk_gt : context -> ast -> ast -> ast Create greater than or equal to. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_ge', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_ge : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_ge" @@ -1835,6 +2034,8 @@ external mk_ge : context -> ast -> ast -> ast - {b See also}: {!mk_real2int} - {b See also}: {!mk_is_int} + + def_API('mk_int2real', AST, (_in(CONTEXT), _in(AST))) *) external mk_int2real : context -> ast -> ast = "camlidl_z3_Z3_mk_int2real" @@ -1848,6 +2049,8 @@ external mk_int2real : context -> ast -> ast - {b See also}: {!mk_int2real} - {b See also}: {!mk_is_int} + + def_API('mk_real2int', AST, (_in(CONTEXT), _in(AST))) *) external mk_real2int : context -> ast -> ast = "camlidl_z3_Z3_mk_real2int" @@ -1858,6 +2061,8 @@ external mk_real2int : context -> ast -> ast - {b See also}: {!mk_int2real} - {b See also}: {!mk_real2int} + + def_API('mk_is_int', AST, (_in(CONTEXT), _in(AST))) *) external mk_is_int : context -> ast -> ast = "camlidl_z3_Z3_mk_is_int" @@ -1870,6 +2075,8 @@ external mk_is_int : context -> ast -> ast Bitwise negation. The node [t1] must have a bit-vector sort. + + def_API('mk_bvnot', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvnot : context -> ast -> ast = "camlidl_z3_Z3_mk_bvnot" @@ -1879,6 +2086,8 @@ external mk_bvnot : context -> ast -> ast Take conjunction of bits in vector, return vector of length 1. The node [t1] must have a bit-vector sort. + + def_API('mk_bvredand', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvredand : context -> ast -> ast = "camlidl_z3_Z3_mk_bvredand" @@ -1888,6 +2097,8 @@ external mk_bvredand : context -> ast -> ast Take disjunction of bits in vector, return vector of length 1. The node [t1] must have a bit-vector sort. + + def_API('mk_bvredor', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvredor : context -> ast -> ast = "camlidl_z3_Z3_mk_bvredor" @@ -1897,6 +2108,8 @@ external mk_bvredor : context -> ast -> ast Bitwise and. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvand', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvand : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvand" @@ -1906,6 +2119,8 @@ external mk_bvand : context -> ast -> ast -> ast Bitwise or. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvor : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvor" @@ -1915,6 +2130,8 @@ external mk_bvor : context -> ast -> ast -> ast Bitwise exclusive-or. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvxor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvxor : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvxor" @@ -1924,6 +2141,8 @@ external mk_bvxor : context -> ast -> ast -> ast Bitwise nand. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvnand', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvnand : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvnand" @@ -1933,6 +2152,8 @@ external mk_bvnand : context -> ast -> ast -> ast Bitwise nor. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvnor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvnor : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvnor" @@ -1942,6 +2163,8 @@ external mk_bvnor : context -> ast -> ast -> ast Bitwise xnor. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvxnor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvxnor : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvxnor" @@ -1951,6 +2174,8 @@ external mk_bvxnor : context -> ast -> ast -> ast Standard two's complement unary minus. The node [t1] must have bit-vector sort. + + def_API('mk_bvneg', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvneg : context -> ast -> ast = "camlidl_z3_Z3_mk_bvneg" @@ -1960,6 +2185,8 @@ external mk_bvneg : context -> ast -> ast Standard two's complement addition. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvadd', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvadd : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvadd" @@ -1969,6 +2196,8 @@ external mk_bvadd : context -> ast -> ast -> ast Standard two's complement subtraction. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsub', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsub : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsub" @@ -1978,6 +2207,8 @@ external mk_bvsub : context -> ast -> ast -> ast Standard two's complement multiplication. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvmul', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvmul : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvmul" @@ -1991,6 +2222,8 @@ external mk_bvmul : context -> ast -> ast -> ast is undefined. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvudiv', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvudiv : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvudiv" @@ -2008,6 +2241,8 @@ external mk_bvudiv : context -> ast -> ast -> ast If {e t2 } is zero, then the result is undefined. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsdiv', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsdiv : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsdiv" @@ -2021,6 +2256,8 @@ external mk_bvsdiv : context -> ast -> ast -> ast If {e t2 } is zero, then the result is undefined. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvurem', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvurem : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvurem" @@ -2037,6 +2274,8 @@ external mk_bvurem : context -> ast -> ast -> ast The nodes [t1] and [t2] must have the same bit-vector sort. - {b See also}: {!mk_bvsmod} + + def_API('mk_bvsrem', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsrem : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsrem" @@ -2050,6 +2289,8 @@ external mk_bvsrem : context -> ast -> ast -> ast The nodes [t1] and [t2] must have the same bit-vector sort. - {b See also}: {!mk_bvsrem} + + def_API('mk_bvsmod', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsmod : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsmod" @@ -2059,6 +2300,8 @@ external mk_bvsmod : context -> ast -> ast -> ast Unsigned less than. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvult', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvult : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvult" @@ -2076,6 +2319,8 @@ external mk_bvult : context -> ast -> ast -> ast v} The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvslt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvslt : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvslt" @@ -2085,6 +2330,8 @@ external mk_bvslt : context -> ast -> ast -> ast Unsigned less than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvule', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvule : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvule" @@ -2094,6 +2341,8 @@ external mk_bvule : context -> ast -> ast -> ast Two's complement signed less than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsle', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsle : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsle" @@ -2103,6 +2352,8 @@ external mk_bvsle : context -> ast -> ast -> ast Unsigned greater than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvuge', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvuge : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvuge" @@ -2112,6 +2363,8 @@ external mk_bvuge : context -> ast -> ast -> ast Two's complement signed greater than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsge', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsge : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsge" @@ -2121,6 +2374,8 @@ external mk_bvsge : context -> ast -> ast -> ast Unsigned greater than. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvugt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvugt : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvugt" @@ -2130,6 +2385,8 @@ external mk_bvugt : context -> ast -> ast -> ast Two's complement signed greater than. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsgt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsgt : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsgt" @@ -2142,6 +2399,8 @@ external mk_bvsgt : context -> ast -> ast -> ast The result is a bit-vector of size {e n1+n2 }, where [n1] ([n2)] is the size of [t1] ([t2)]. + + def_API('mk_concat', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_concat : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_concat" @@ -2153,6 +2412,8 @@ external mk_concat : context -> ast -> ast -> ast high - low + 1 }. The node [t1] must have a bit-vector sort. + + def_API('mk_extract', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in(AST))) *) external mk_extract : context -> int -> int -> ast -> ast = "camlidl_z3_Z3_mk_extract" @@ -2164,6 +2425,8 @@ external mk_extract : context -> int -> int -> ast -> ast bit-vector. The node [t1] must have a bit-vector sort. + + def_API('mk_sign_ext', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_sign_ext : context -> int -> ast -> ast = "camlidl_z3_Z3_mk_sign_ext" @@ -2175,6 +2438,8 @@ external mk_sign_ext : context -> int -> ast -> ast given bit-vector. The node [t1] must have a bit-vector sort. + + def_API('mk_zero_ext', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_zero_ext : context -> int -> ast -> ast = "camlidl_z3_Z3_mk_zero_ext" @@ -2184,6 +2449,8 @@ external mk_zero_ext : context -> int -> ast -> ast Repeat the given bit-vector up length {e i }. The node [t1] must have a bit-vector sort. + + def_API('mk_repeat', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_repeat : context -> int -> ast -> ast = "camlidl_z3_Z3_mk_repeat" @@ -2200,6 +2467,8 @@ external mk_repeat : context -> int -> ast -> ast programming language or assembly architecture you are modeling. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvshl', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvshl : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvshl" @@ -2216,6 +2485,8 @@ external mk_bvshl : context -> ast -> ast -> ast programming language or assembly architecture you are modeling. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvlshr', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvlshr : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvlshr" @@ -2228,11 +2499,13 @@ external mk_bvlshr : context -> ast -> ast -> ast bits of the result always copy the most significant bit of the second argument. - NB. The semantics of shift operations varies between environments. This + The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvashr', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvashr : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvashr" @@ -2242,6 +2515,8 @@ external mk_bvashr : context -> ast -> ast -> ast Rotate bits of [t1] to the left [i] times. The node [t1] must have a bit-vector sort. + + def_API('mk_rotate_left', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_rotate_left : context -> int -> ast -> ast = "camlidl_z3_Z3_mk_rotate_left" @@ -2251,6 +2526,8 @@ external mk_rotate_left : context -> int -> ast -> ast Rotate bits of [t1] to the right [i] times. The node [t1] must have a bit-vector sort. + + def_API('mk_rotate_right', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_rotate_right : context -> int -> ast -> ast = "camlidl_z3_Z3_mk_rotate_right" @@ -2260,6 +2537,8 @@ external mk_rotate_right : context -> int -> ast -> ast Rotate bits of [t1] to the left [t2] times. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_ext_rotate_left', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_ext_rotate_left : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_ext_rotate_left" @@ -2269,6 +2548,8 @@ external mk_ext_rotate_left : context -> ast -> ast -> ast Rotate bits of [t1] to the right [t2] times. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_ext_rotate_right', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_ext_rotate_right : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_ext_rotate_right" @@ -2282,6 +2563,8 @@ external mk_ext_rotate_right : context -> ast -> ast -> ast when solving constraints with this function. The node [t1] must have integer sort. + + def_API('mk_int2bv', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_int2bv : context -> int -> ast -> ast = "camlidl_z3_Z3_mk_int2bv" @@ -2294,11 +2577,13 @@ external mk_int2bv : context -> int -> ast -> ast and in the range {e [0..2^N-1] }, where N are the number of bits in [t1]. If [is_signed] is true, [t1] is treated as a signed bit-vector. - NB. This function is essentially treated as uninterpreted. + This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function. The node [t1] must have a bit-vector sort. + + def_API('mk_bv2int', AST, (_in(CONTEXT), _in(AST), _in(BOOL))) *) external mk_bv2int : context -> ast -> bool -> ast = "camlidl_z3_Z3_mk_bv2int" @@ -2309,6 +2594,8 @@ external mk_bv2int : context -> ast -> bool -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvadd_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL))) *) external mk_bvadd_no_overflow : context -> ast -> ast -> bool -> ast = "camlidl_z3_Z3_mk_bvadd_no_overflow" @@ -2319,6 +2606,8 @@ external mk_bvadd_no_overflow : context -> ast -> ast -> bool -> ast of [t1] and [t2] does not underflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvadd_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvadd_no_underflow : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvadd_no_underflow" @@ -2329,6 +2618,8 @@ external mk_bvadd_no_underflow : context -> ast -> ast -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsub_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsub_no_overflow : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsub_no_overflow" @@ -2339,6 +2630,8 @@ external mk_bvsub_no_overflow : context -> ast -> ast -> ast of [t1] and [t2] does not underflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsub_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL))) *) external mk_bvsub_no_underflow : context -> ast -> ast -> bool -> ast = "camlidl_z3_Z3_mk_bvsub_no_underflow" @@ -2349,6 +2642,8 @@ external mk_bvsub_no_underflow : context -> ast -> ast -> bool -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsdiv_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsdiv_no_overflow : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvsdiv_no_overflow" @@ -2359,6 +2654,8 @@ external mk_bvsdiv_no_overflow : context -> ast -> ast -> ast [t1] is interpreted as a signed bit-vector. The node [t1] must have bit-vector sort. + + def_API('mk_bvneg_no_overflow', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvneg_no_overflow : context -> ast -> ast = "camlidl_z3_Z3_mk_bvneg_no_overflow" @@ -2369,6 +2666,8 @@ external mk_bvneg_no_overflow : context -> ast -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvmul_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL))) *) external mk_bvmul_no_overflow : context -> ast -> ast -> bool -> ast = "camlidl_z3_Z3_mk_bvmul_no_overflow" @@ -2379,6 +2678,8 @@ external mk_bvmul_no_overflow : context -> ast -> ast -> bool -> ast of [t1] and [t2] does not underflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvmul_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvmul_no_underflow : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_bvmul_no_underflow" @@ -2397,6 +2698,8 @@ external mk_bvmul_no_underflow : context -> ast -> ast -> ast - {b See also}: {!mk_array_sort} - {b See also}: {!mk_store} + + def_API('mk_select', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_select : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_select" @@ -2415,6 +2718,8 @@ external mk_select : context -> ast -> ast -> ast - {b See also}: {!mk_array_sort} - {b See also}: {!mk_select} + + def_API('mk_store', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) *) external mk_store : context -> ast -> ast -> ast -> ast = "camlidl_z3_Z3_mk_store" @@ -2428,6 +2733,8 @@ external mk_store : context -> ast -> ast -> ast -> ast @param c logical context. @param domain domain sort for the array. @param v value that the array maps to. + + def_API('mk_const_array', AST, (_in(CONTEXT), _in(SORT), _in(AST))) *) external mk_const_array : context -> sort -> ast -> ast = "camlidl_z3_Z3_mk_const_array" @@ -2443,6 +2750,8 @@ external mk_const_array : context -> sort -> ast -> ast - {b See also}: {!mk_array_sort} - {b See also}: {!mk_store} - {b See also}: {!mk_select} + + def_API('mk_map', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST))) *) external mk_map : context -> func_decl -> int -> ast -> ast = "camlidl_z3_Z3_mk_map" @@ -2455,6 +2764,7 @@ external mk_map : context -> func_decl -> int -> ast -> ast @param c logical context. @param array array value whose default range value is accessed. + def_API('mk_array_default', AST, (_in(CONTEXT), _in(AST))) *) external mk_array_default : context -> ast -> ast = "camlidl_z3_Z3_mk_array_default" @@ -2464,18 +2774,24 @@ external mk_array_default : context -> ast -> ast *) (** Summary: Create Set type. + + def_API('mk_set_sort', SORT, (_in(CONTEXT), _in(SORT))) *) external mk_set_sort : context -> sort -> sort = "camlidl_z3_Z3_mk_set_sort" (** Summary: Create the empty set. + + def_API('mk_empty_set', AST, (_in(CONTEXT), _in(SORT))) *) external mk_empty_set : context -> sort -> ast = "camlidl_z3_Z3_mk_empty_set" (** Summary: Create the full set. + + def_API('mk_full_set', AST, (_in(CONTEXT), _in(SORT))) *) external mk_full_set : context -> sort -> ast = "camlidl_z3_Z3_mk_full_set" @@ -2484,6 +2800,8 @@ external mk_full_set : context -> sort -> ast Summary: Add an element to a set. The first argument must be a set, the second an element. + + def_API('mk_set_add', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_add : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_set_add" @@ -2492,30 +2810,40 @@ external mk_set_add : context -> ast -> ast -> ast Summary: Remove an element to a set. The first argument must be a set, the second an element. + + def_API('mk_set_del', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_del : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_set_del" (** Summary: Take the union of a list of sets. + + def_API('mk_set_union', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_set_union : context -> ast array -> ast = "camlidl_z3_Z3_mk_set_union" (** Summary: Take the intersection of a list of sets. + + def_API('mk_set_intersect', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_set_intersect : context -> ast array -> ast = "camlidl_z3_Z3_mk_set_intersect" (** Summary: Take the set difference between two sets. + + def_API('mk_set_difference', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_difference : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_set_difference" (** Summary: Take the complement of a set. + + def_API('mk_set_complement', AST, (_in(CONTEXT), _in(AST))) *) external mk_set_complement : context -> ast -> ast = "camlidl_z3_Z3_mk_set_complement" @@ -2524,12 +2852,16 @@ external mk_set_complement : context -> ast -> ast Summary: Check for set membership. The first argument should be an element type of the set. + + def_API('mk_set_member', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_member : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_set_member" (** Summary: Check for subsetness of sets. + + def_API('mk_set_subset', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_subset : context -> ast -> ast -> ast = "camlidl_z3_Z3_mk_set_subset" @@ -2567,6 +2899,8 @@ val embed_numeral: context -> numeral_refined -> ast - {b See also}: {!mk_int} + + def_API('mk_numeral', AST, (_in(CONTEXT), _in(STRING), _in(SORT))) *) external mk_numeral : context -> string -> sort -> ast = "camlidl_z3_Z3_mk_numeral" @@ -2583,6 +2917,8 @@ external mk_numeral : context -> string -> sort -> ast - {b See also}: {!mk_numeral} - {b See also}: {!mk_int} + + def_API('mk_real', AST, (_in(CONTEXT), _in(INT), _in(INT))) *) external mk_real : context -> int -> int -> ast = "camlidl_z3_Z3_mk_real" @@ -2594,6 +2930,8 @@ external mk_real : context -> int -> int -> ast It is slightly faster than {!mk_numeral} since it is not necessary to parse a string. - {b See also}: {!mk_numeral} + + def_API('mk_int', AST, (_in(CONTEXT), _in(INT), _in(SORT))) *) external mk_int : context -> int -> sort -> ast = "camlidl_z3_Z3_mk_int" @@ -2605,6 +2943,8 @@ external mk_int : context -> int -> sort -> ast It is slightly faster than {!mk_numeral} since it is not necessary to parse a string. - {b See also}: {!mk_numeral} + + def_API('mk_int64', AST, (_in(CONTEXT), _in(INT64), _in(SORT))) *) external mk_int64 : context -> int64 -> sort -> ast = "camlidl_z3_Z3_mk_int64" @@ -2627,9 +2967,10 @@ external mk_int64 : context -> int64 -> sort -> ast In general, one can pass in a list of (multi-)patterns in the quantifier constructor. - - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_pattern', PATTERN, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_pattern : context -> ast array -> pattern = "camlidl_z3_Z3_mk_pattern" @@ -2660,6 +3001,8 @@ external mk_pattern : context -> ast array -> pattern - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_bound', AST, (_in(CONTEXT), _in(UINT), _in(SORT))) *) external mk_bound : context -> int -> sort -> ast = "camlidl_z3_Z3_mk_bound" @@ -2694,6 +3037,8 @@ external mk_bound : context -> int -> sort -> ast - {b See also}: {!mk_pattern} - {b See also}: {!mk_bound} - {b See also}: {!mk_exists} + + def_API('mk_forall', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, PATTERN), _in(UINT), _in_array(4, SORT), _in_array(4, SYMBOL), _in(AST))) *) external mk_forall : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_forall_bytecode" "camlidl_z3_Z3_mk_forall" @@ -2705,6 +3050,8 @@ external mk_forall : context -> int -> pattern array -> sort array -> symbol arr - {b See also}: {!mk_bound} - {b See also}: {!mk_forall} - {b See also}: {!mk_quantifier} + + def_API('mk_exists', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, PATTERN), _in(UINT), _in_array(4, SORT), _in_array(4, SYMBOL), _in(AST))) *) external mk_exists : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_exists_bytecode" "camlidl_z3_Z3_mk_exists" @@ -2727,6 +3074,8 @@ external mk_exists : context -> int -> pattern array -> sort array -> symbol arr - {b See also}: {!mk_bound} - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_quantifier', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(UINT), _in_array(3, PATTERN), _in(UINT), _in_array(5, SORT), _in_array(5, SYMBOL), _in(AST))) *) external mk_quantifier : context -> bool -> int -> pattern array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_bytecode" "camlidl_z3_Z3_mk_quantifier" @@ -2752,6 +3101,8 @@ external mk_quantifier : context -> bool -> int -> pattern array -> sort array - - {b See also}: {!mk_bound} - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_quantifier_ex', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(5, PATTERN), _in(UINT), _in_array(7, AST), _in(UINT), _in_array(9, SORT), _in_array(9, SYMBOL), _in(AST))) *) external mk_quantifier_ex : context -> bool -> int -> symbol -> symbol -> pattern array -> ast array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_ex_bytecode" "camlidl_z3_Z3_mk_quantifier_ex" @@ -2772,6 +3123,7 @@ external mk_quantifier_ex : context -> bool -> int -> symbol -> symbol -> patter - {b See also}: {!mk_pattern} - {b See also}: {!mk_exists_const} + def_API('mk_forall_const', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, APP), _in(UINT), _in_array(4, PATTERN), _in(AST))) *) external mk_forall_const : context -> int -> app array -> pattern array -> ast -> ast = "camlidl_z3_Z3_mk_forall_const" @@ -2793,6 +3145,8 @@ external mk_forall_const : context -> int -> app array -> pattern array -> ast - - {b See also}: {!mk_pattern} - {b See also}: {!mk_forall_const} + + def_API('mk_exists_const', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, APP), _in(UINT), _in_array(4, PATTERN), _in(AST))) *) external mk_exists_const : context -> int -> app array -> pattern array -> ast -> ast = "camlidl_z3_Z3_mk_exists_const" @@ -2801,6 +3155,8 @@ external mk_exists_const : context -> int -> app array -> pattern array -> ast - Summary: Create a universal or existential quantifier using a list of constants that will form the set of bound variables. + + def_API('mk_quantifier_const', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(UINT), _in_array(3, APP), _in(UINT), _in_array(5, PATTERN), _in(AST))) *) external mk_quantifier_const : context -> bool -> int -> app array -> pattern array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_const_bytecode" "camlidl_z3_Z3_mk_quantifier_const" @@ -2809,6 +3165,8 @@ external mk_quantifier_const : context -> bool -> int -> app array -> pattern ar Summary: Create a universal or existential quantifier using a list of constants that will form the set of bound variables. + + def_API('mk_quantifier_const_ex', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(5, APP), _in(UINT), _in_array(7, PATTERN), _in(UINT), _in_array(9, AST), _in(AST))) *) external mk_quantifier_const_ex : context -> bool -> int -> symbol -> symbol -> app array -> pattern array -> ast array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_const_ex_bytecode" "camlidl_z3_Z3_mk_quantifier_const_ex" @@ -2832,6 +3190,8 @@ val symbol_refine: context -> symbol -> symbol_refined Summary: Return [INT_SYMBOL] if the symbol was constructed using {!mk_int_symbol}, and [STRING_SYMBOL] if the symbol was constructed using {!mk_string_symbol}. + + def_API('get_symbol_kind', UINT, (_in(CONTEXT), _in(SYMBOL))) *) external get_symbol_kind : context -> symbol -> symbol_kind = "camlidl_z3_Z3_get_symbol_kind" @@ -2843,6 +3203,8 @@ external get_symbol_kind : context -> symbol -> symbol_kind - {b Precondition}: get_symbol_kind s == INT_SYMBOL - {b See also}: {!mk_int_symbol} + + def_API('get_symbol_int', INT, (_in(CONTEXT), _in(SYMBOL))) *) external get_symbol_int : context -> symbol -> int = "camlidl_z3_Z3_get_symbol_int" @@ -2858,6 +3220,8 @@ external get_symbol_int : context -> symbol -> int - {b See also}: {!mk_string_symbol} + + def_API('get_symbol_string', STRING, (_in(CONTEXT), _in(SYMBOL))) *) external get_symbol_string : context -> symbol -> string = "camlidl_z3_Z3_get_symbol_string" @@ -2873,6 +3237,8 @@ val sort_refine: context -> sort -> sort_refined (** Summary: Return the sort name as a symbol. + + def_API('get_sort_name', SYMBOL, (_in(CONTEXT), _in(SORT))) *) external get_sort_name : context -> sort -> symbol = "camlidl_z3_Z3_get_sort_name" @@ -2880,6 +3246,8 @@ external get_sort_name : context -> sort -> symbol (** Summary: Return a unique identifier for [s]. - {b Remarks}: Implicitly used by [Pervasives.( = )] and [Pervasives.compare]. + + def_API('get_sort_id', UINT, (_in(CONTEXT), _in(SORT))) *) external get_sort_id : context -> sort -> int = "camlidl_z3_Z3_get_sort_id" @@ -2890,6 +3258,8 @@ external get_sort_id : context -> sort -> int (** Summary: Convert a [sort] into [ast]. - {b Remarks}: [sort_to_ast c s] can be replaced by [(s :> ast)]. + + def_API('sort_to_ast', AST, (_in(CONTEXT), _in(SORT))) *) external sort_to_ast : context -> sort -> ast = "camlidl_z3_Z3_sort_to_ast" @@ -2897,6 +3267,8 @@ external sort_to_ast : context -> sort -> ast (** Summary: compare sorts. - {b Remarks}: [Pervasives.( = )] or [Pervasives.compare] can also be used. + + def_API('is_eq_sort', BOOL, (_in(CONTEXT), _in(SORT), _in(SORT))) *) external is_eq_sort : context -> sort -> sort -> bool = "camlidl_z3_Z3_is_eq_sort" @@ -2905,6 +3277,8 @@ external is_eq_sort : context -> sort -> sort -> bool Summary: Return the sort kind (e.g., array, tuple, int, bool, etc). - {b See also}: {!sort_kind} + + def_API('get_sort_kind', UINT, (_in(CONTEXT), _in(SORT))) *) external get_sort_kind : context -> sort -> sort_kind = "camlidl_z3_Z3_get_sort_kind" @@ -2917,6 +3291,8 @@ external get_sort_kind : context -> sort -> sort_kind - {b See also}: {!mk_bv_sort} - {b See also}: {!get_sort_kind} + + def_API('get_bv_sort_size', UINT, (_in(CONTEXT), _in(SORT))) *) external get_bv_sort_size : context -> sort -> int = "camlidl_z3_Z3_get_bv_sort_size" @@ -2925,6 +3301,8 @@ external get_bv_sort_size : context -> sort -> int Summary: Return the size of the sort in [r]. Return [None] if the call failed. That is, get_sort_kind(s) == FINITE_DOMAIN_SORT + + def_API('get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64))) *) external get_finite_domain_sort_size : context -> sort -> int64 option = "camlidl_z3_Z3_get_finite_domain_sort_size" @@ -2937,6 +3315,8 @@ external get_finite_domain_sort_size : context -> sort -> int64 option - {b See also}: {!mk_array_sort} - {b See also}: {!get_sort_kind} + + def_API('get_array_sort_domain', SORT, (_in(CONTEXT), _in(SORT))) *) external get_array_sort_domain : context -> sort -> sort = "camlidl_z3_Z3_get_array_sort_domain" @@ -2949,6 +3329,8 @@ external get_array_sort_domain : context -> sort -> sort - {b See also}: {!mk_array_sort} - {b See also}: {!get_sort_kind} + + def_API('get_array_sort_range', SORT, (_in(CONTEXT), _in(SORT))) *) external get_array_sort_range : context -> sort -> sort = "camlidl_z3_Z3_get_array_sort_range" @@ -2962,6 +3344,8 @@ external get_array_sort_range : context -> sort -> sort - {b See also}: {!mk_tuple_sort} - {b See also}: {!get_sort_kind} + + def_API('get_tuple_sort_mk_decl', FUNC_DECL, (_in(CONTEXT), _in(SORT))) *) external get_tuple_sort_mk_decl : context -> sort -> func_decl = "camlidl_z3_Z3_get_tuple_sort_mk_decl" @@ -2974,6 +3358,8 @@ external get_tuple_sort_mk_decl : context -> sort -> func_decl - {b See also}: {!mk_tuple_sort} - {b See also}: {!get_sort_kind} + + def_API('get_tuple_sort_num_fields', UINT, (_in(CONTEXT), _in(SORT))) *) external get_tuple_sort_num_fields : context -> sort -> int = "camlidl_z3_Z3_get_tuple_sort_num_fields" @@ -2988,6 +3374,8 @@ external get_tuple_sort_num_fields : context -> sort -> int - {b See also}: {!mk_tuple_sort} - {b See also}: {!get_sort_kind} + + def_API('get_tuple_sort_field_decl', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_tuple_sort_field_decl : context -> sort -> int -> func_decl = "camlidl_z3_Z3_get_tuple_sort_field_decl" @@ -3001,6 +3389,7 @@ external get_tuple_sort_field_decl : context -> sort -> int -> func_decl - {b See also}: {!get_datatype_sort_recognizer} - {b See also}: {!get_datatype_sort_constructor_accessor} + def_API('get_datatype_sort_num_constructors', UINT, (_in(CONTEXT), _in(SORT))) *) external get_datatype_sort_num_constructors : context -> sort -> int = "camlidl_z3_Z3_get_datatype_sort_num_constructors" @@ -3015,6 +3404,7 @@ external get_datatype_sort_num_constructors : context -> sort -> int - {b See also}: {!get_datatype_sort_recognizer} - {b See also}: {!get_datatype_sort_constructor_accessor} + def_API('get_datatype_sort_constructor', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_datatype_sort_constructor : context -> sort -> int -> func_decl = "camlidl_z3_Z3_get_datatype_sort_constructor" @@ -3029,6 +3419,7 @@ external get_datatype_sort_constructor : context -> sort -> int -> func_decl - {b See also}: {!get_datatype_sort_constructor} - {b See also}: {!get_datatype_sort_constructor_accessor} + def_API('get_datatype_sort_recognizer', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_datatype_sort_recognizer : context -> sort -> int -> func_decl = "camlidl_z3_Z3_get_datatype_sort_recognizer" @@ -3043,6 +3434,8 @@ external get_datatype_sort_recognizer : context -> sort -> int -> func_decl - {b See also}: {!get_datatype_sort_num_constructors} - {b See also}: {!get_datatype_sort_constructor} - {b See also}: {!get_datatype_sort_recognizer} + + def_API('get_datatype_sort_constructor_accessor', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT), _in(UINT))) *) external get_datatype_sort_constructor_accessor : context -> sort -> int -> int -> func_decl = "camlidl_z3_Z3_get_datatype_sort_constructor_accessor" @@ -3053,6 +3446,8 @@ external get_datatype_sort_constructor_accessor : context -> sort -> int -> int - {b Precondition}: get_sort_kind s == RELATION_SORT - {b See also}: {!get_relation_column} + + def_API('get_relation_arity', UINT, (_in(CONTEXT), _in(SORT))) *) external get_relation_arity : context -> sort -> int = "camlidl_z3_Z3_get_relation_arity" @@ -3064,6 +3459,8 @@ external get_relation_arity : context -> sort -> int - {b Precondition}: col < get_relation_arity c s - {b See also}: {!get_relation_arity} + + def_API('get_relation_column', SORT, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_relation_column : context -> sort -> int -> sort = "camlidl_z3_Z3_get_relation_column" @@ -3074,6 +3471,8 @@ external get_relation_column : context -> sort -> int -> sort (** Summary: Convert a [func_decl] into [ast]. - {b Remarks}: [func_decl_to_ast c f] can be replaced by [(f :> ast)]. + + def_API('func_decl_to_ast', AST, (_in(CONTEXT), _in(FUNC_DECL))) *) external func_decl_to_ast : context -> func_decl -> ast = "camlidl_z3_Z3_func_decl_to_ast" @@ -3081,6 +3480,8 @@ external func_decl_to_ast : context -> func_decl -> ast (** Summary: compare terms. - {b Remarks}: [Pervasives.( = )] or [Pervasives.compare] can also be used. + + def_API('is_eq_func_decl', BOOL, (_in(CONTEXT), _in(FUNC_DECL), _in(FUNC_DECL))) *) external is_eq_func_decl : context -> func_decl -> func_decl -> bool = "camlidl_z3_Z3_is_eq_func_decl" @@ -3088,18 +3489,24 @@ external is_eq_func_decl : context -> func_decl -> func_decl -> bool (** Summary: Return a unique identifier for [f]. - {b Remarks}: Implicitly used by [Pervasives.( = )] and [Pervasives.compare]. + + def_API('get_func_decl_id', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_func_decl_id : context -> func_decl -> int = "camlidl_z3_Z3_get_func_decl_id" (** Summary: Return the constant declaration name as a symbol. + + def_API('get_decl_name', SYMBOL, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_decl_name : context -> func_decl -> symbol = "camlidl_z3_Z3_get_decl_name" (** Summary: Return declaration kind corresponding to declaration. + + def_API('get_decl_kind', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_decl_kind : context -> func_decl -> decl_kind = "camlidl_z3_Z3_get_decl_kind" @@ -3108,6 +3515,8 @@ external get_decl_kind : context -> func_decl -> decl_kind Summary: Return the number of parameters of the given declaration. - {b See also}: {!get_arity} + + def_API('get_domain_size', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_domain_size : context -> func_decl -> int = "camlidl_z3_Z3_get_domain_size" @@ -3116,6 +3525,8 @@ external get_domain_size : context -> func_decl -> int Summary: Alias for [get_domain_size]. - {b See also}: {!get_domain_size} + + def_API('get_arity', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_arity : context -> func_decl -> int = "camlidl_z3_Z3_get_arity" @@ -3127,6 +3538,8 @@ external get_arity : context -> func_decl -> int - {b Precondition}: i < get_domain_size d - {b See also}: {!get_domain_size} + + def_API('get_domain', SORT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_domain : context -> func_decl -> int -> sort = "camlidl_z3_Z3_get_domain" @@ -3146,12 +3559,16 @@ val get_domains: context -> func_decl -> sort array If [d] is a constant (i.e., has zero arguments), then this function returns the sort of the constant. + + def_API('get_range', SORT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_range : context -> func_decl -> sort = "camlidl_z3_Z3_get_range" (** Summary: Return the number of parameters associated with a declaration. + + def_API('get_decl_num_parameters', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_decl_num_parameters : context -> func_decl -> int = "camlidl_z3_Z3_get_decl_num_parameters" @@ -3162,6 +3579,8 @@ external get_decl_num_parameters : context -> func_decl -> int @param c the context @param d the function declaration @param idx is the index of the named parameter it should be between 0 and the number of parameters. + + def_API('get_decl_parameter_kind', UINT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_parameter_kind : context -> func_decl -> int -> parameter_kind = "camlidl_z3_Z3_get_decl_parameter_kind" @@ -3170,6 +3589,8 @@ external get_decl_parameter_kind : context -> func_decl -> int -> parameter_kind Summary: Return the integer value associated with an integer parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_INT + + def_API('get_decl_int_parameter', INT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_int_parameter : context -> func_decl -> int -> int = "camlidl_z3_Z3_get_decl_int_parameter" @@ -3178,6 +3599,8 @@ external get_decl_int_parameter : context -> func_decl -> int -> int Summary: Return the double value associated with an double parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_DOUBLE + + def_API('get_decl_double_parameter', DOUBLE, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_double_parameter : context -> func_decl -> int -> float = "camlidl_z3_Z3_get_decl_double_parameter" @@ -3186,6 +3609,8 @@ external get_decl_double_parameter : context -> func_decl -> int -> float Summary: Return the double value associated with an double parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_SYMBOL + + def_API('get_decl_symbol_parameter', SYMBOL, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_symbol_parameter : context -> func_decl -> int -> symbol = "camlidl_z3_Z3_get_decl_symbol_parameter" @@ -3194,6 +3619,8 @@ external get_decl_symbol_parameter : context -> func_decl -> int -> symbol Summary: Return the sort value associated with a sort parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_SORT + + def_API('get_decl_sort_parameter', SORT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_sort_parameter : context -> func_decl -> int -> sort = "camlidl_z3_Z3_get_decl_sort_parameter" @@ -3202,6 +3629,8 @@ external get_decl_sort_parameter : context -> func_decl -> int -> sort Summary: Return the expresson value associated with an expression parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_AST + + def_API('get_decl_ast_parameter', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_ast_parameter : context -> func_decl -> int -> ast = "camlidl_z3_Z3_get_decl_ast_parameter" @@ -3210,6 +3639,8 @@ external get_decl_ast_parameter : context -> func_decl -> int -> ast Summary: Return the expresson value associated with an expression parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_FUNC_DECL + + def_API('get_decl_func_decl_parameter', FUNC_DECL, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_func_decl_parameter : context -> func_decl -> int -> func_decl = "camlidl_z3_Z3_get_decl_func_decl_parameter" @@ -3218,6 +3649,8 @@ external get_decl_func_decl_parameter : context -> func_decl -> int -> func_decl Summary: Return the rational value, as a string, associated with a rational parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_RATIONAL + + def_API('get_decl_rational_parameter', STRING, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_rational_parameter : context -> func_decl -> int -> string = "camlidl_z3_Z3_get_decl_rational_parameter" @@ -3228,12 +3661,16 @@ external get_decl_rational_parameter : context -> func_decl -> int -> string (** Summary: Convert a [app] into [ast]. - {b Remarks}: [app_to_ast c a] can be replaced by [(a :> ast)]. + + def_API('app_to_ast', AST, (_in(CONTEXT), _in(APP))) *) external app_to_ast : context -> app -> ast = "camlidl_z3_Z3_app_to_ast" (** Summary: Return the declaration of a constant or function application. + + def_API('get_app_decl', FUNC_DECL, (_in(CONTEXT), _in(APP))) *) external get_app_decl : context -> app -> func_decl = "camlidl_z3_Z3_get_app_decl" @@ -3242,6 +3679,8 @@ external get_app_decl : context -> app -> func_decl Summary: \[ [ get_app_num_args c a ] \] Return the number of argument of an application. If [t] is an constant, then the number of arguments is 0. + + def_API('get_app_num_args', UINT, (_in(CONTEXT), _in(APP))) *) external get_app_num_args : context -> app -> int = "camlidl_z3_Z3_get_app_num_args" @@ -3251,6 +3690,8 @@ external get_app_num_args : context -> app -> int Return the i-th argument of the given application. - {b Precondition}: i < get_num_args c a + + def_API('get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT))) *) external get_app_arg : context -> app -> int -> ast = "camlidl_z3_Z3_get_app_arg" @@ -3304,6 +3745,8 @@ val term_refine : context -> ast -> term_refined (** Summary: compare terms. - {b Remarks}: [Pervasives.( = )] or [Pervasives.compare] can also be used. + + def_API('is_eq_ast', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) *) external is_eq_ast : context -> ast -> ast -> bool = "camlidl_z3_Z3_is_eq_ast" @@ -3311,6 +3754,8 @@ external is_eq_ast : context -> ast -> ast -> bool (** Summary: Return a unique identifier for [t]. - {b Remarks}: Implicitly used by [Pervasives.compare] for values of type [ast], [app], [sort], [func_decl], and [pattern]. + + def_API('get_ast_id', UINT, (_in(CONTEXT), _in(AST))) *) external get_ast_id : context -> ast -> int = "camlidl_z3_Z3_get_ast_id" @@ -3318,6 +3763,8 @@ external get_ast_id : context -> ast -> int (** Summary: Return a hash code for the given AST. - {b Remarks}: Implicitly used by [Hashtbl.hash] for values of type [ast], [app], [sort], [func_decl], and [pattern]. + + def_API('get_ast_hash', UINT, (_in(CONTEXT), _in(AST))) *) external get_ast_hash : context -> ast -> int = "camlidl_z3_Z3_get_ast_hash" @@ -3326,37 +3773,52 @@ external get_ast_hash : context -> ast -> int Summary: Return the sort of an AST node. The AST node must be a constant, application, numeral, bound variable, or quantifier. - + + def_API('get_sort', SORT, (_in(CONTEXT), _in(AST))) *) external get_sort : context -> ast -> sort = "camlidl_z3_Z3_get_sort" (** Summary: Return true if the given expression [t] is well sorted. + + def_API('is_well_sorted', BOOL, (_in(CONTEXT), _in(AST))) *) external is_well_sorted : context -> ast -> bool = "camlidl_z3_Z3_is_well_sorted" (** Summary: Return L_TRUE if [a] is true, L_FALSE if it is false, and L_UNDEF otherwise. + + def_API('get_bool_value', UINT, (_in(CONTEXT), _in(AST))) *) external get_bool_value : context -> ast -> lbool = "camlidl_z3_Z3_get_bool_value" (** Summary: Return the kind of the given AST. + + def_API('get_ast_kind', UINT, (_in(CONTEXT), _in(AST))) *) external get_ast_kind : context -> ast -> ast_kind = "camlidl_z3_Z3_get_ast_kind" +(** + def_API('is_app', BOOL, (_in(CONTEXT), _in(AST))) +*) external is_app : context -> ast -> bool = "camlidl_z3_Z3_is_app" +(** + def_API('is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST))) +*) external is_numeral_ast : context -> ast -> bool = "camlidl_z3_Z3_is_numeral_ast" (** Summary: Return true if the give AST is a real algebraic number. + + def_API('is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST))) *) external is_algebraic_number : context -> ast -> bool = "camlidl_z3_Z3_is_algebraic_number" @@ -3365,6 +3827,8 @@ external is_algebraic_number : context -> ast -> bool Summary: Convert an [ast] into an [APP_AST]. - {b Precondition}: {v get_ast_kind c a == [APP_AST] v} + + def_API('to_app', APP, (_in(CONTEXT), _in(AST))) *) external to_app : context -> ast -> app = "camlidl_z3_Z3_to_app" @@ -3373,6 +3837,8 @@ external to_app : context -> ast -> app Summary: Convert an AST into a FUNC_DECL_AST. This is just type casting. - {b Precondition}: {v get_ast_kind c a == FUNC_DECL_AST v} + + def_API('to_func_decl', FUNC_DECL, (_in(CONTEXT), _in(AST))) *) external to_func_decl : context -> ast -> func_decl = "camlidl_z3_Z3_to_func_decl" @@ -3395,6 +3861,8 @@ val numeral_refine : context -> ast -> numeral_refined Summary: Return numeral value, as a string of a numeric constant term - {b Precondition}: get_ast_kind c a == NUMERAL_AST + + def_API('get_numeral_string', STRING, (_in(CONTEXT), _in(AST))) *) external get_numeral_string : context -> ast -> string = "camlidl_z3_Z3_get_numeral_string" @@ -3404,6 +3872,8 @@ external get_numeral_string : context -> ast -> string The result has at most [precision] decimal places. - {b Precondition}: get_ast_kind c a == NUMERAL_AST || is_algebraic_number c a + + def_API('get_numeral_decimal_string', STRING, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_numeral_decimal_string : context -> ast -> int -> string = "camlidl_z3_Z3_get_numeral_decimal_string" @@ -3412,6 +3882,8 @@ external get_numeral_decimal_string : context -> ast -> int -> string Summary: Return the numerator (as a numeral AST) of a numeral AST of sort Real. - {b Precondition}: get_ast_kind c a == NUMERAL_AST + + def_API('get_numerator', AST, (_in(CONTEXT), _in(AST))) *) external get_numerator : context -> ast -> ast = "camlidl_z3_Z3_get_numerator" @@ -3420,6 +3892,8 @@ external get_numerator : context -> ast -> ast Summary: Return the denominator (as a numeral AST) of a numeral AST of sort Real. - {b Precondition}: get_ast_kind c a == NUMERAL_AST + + def_API('get_denominator', AST, (_in(CONTEXT), _in(AST))) *) external get_denominator : context -> ast -> ast = "camlidl_z3_Z3_get_denominator" @@ -3435,6 +3909,8 @@ external get_denominator : context -> ast -> ast Return [TRUE] if the numeral value fits in 64 bit numerals, [FALSE] otherwise. - {b Precondition}: get_ast_kind a == NUMERAL_AST + + def_API('get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64))) *) external get_numeral_small : context -> ast -> bool * int64 * int64 = "camlidl_z3_Z3_get_numeral_small" @@ -3447,6 +3923,8 @@ external get_numeral_small : context -> ast -> bool * int64 * int64 - {b Precondition}: get_ast_kind c v == NUMERAL_AST - {b See also}: {!get_numeral_string} + + def_API('get_numeral_int', BOOL, (_in(CONTEXT), _in(AST), _out(INT))) *) external get_numeral_int : context -> ast -> bool * int = "camlidl_z3_Z3_get_numeral_int" @@ -3459,6 +3937,8 @@ external get_numeral_int : context -> ast -> bool * int - {b Precondition}: get_ast_kind c v == NUMERAL_AST - {b See also}: {!get_numeral_string} + + def_API('get_numeral_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) *) external get_numeral_int64 : context -> ast -> bool * int64 = "camlidl_z3_Z3_get_numeral_int64" @@ -3471,6 +3951,8 @@ external get_numeral_int64 : context -> ast -> bool * int64 - {b Precondition}: get_ast_kind c v == NUMERAL_AST - {b See also}: {!get_numeral_string} + + def_API('get_numeral_rational_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64))) *) external get_numeral_rational_int64 : context -> ast -> bool * int64 * int64 = "camlidl_z3_Z3_get_numeral_rational_int64" @@ -3481,6 +3963,8 @@ external get_numeral_rational_int64 : context -> ast -> bool * int64 * int64 The result is a numeral AST of sort Real. - {b Precondition}: is_algebraic_number c a + + def_API('get_algebraic_number_lower', AST, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_algebraic_number_lower : context -> ast -> int -> ast = "camlidl_z3_Z3_get_algebraic_number_lower" @@ -3491,6 +3975,8 @@ external get_algebraic_number_lower : context -> ast -> int -> ast The result is a numeral AST of sort Real. - {b Precondition}: is_algebraic_number c a + + def_API('get_algebraic_number_upper', AST, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_algebraic_number_upper : context -> ast -> int -> ast = "camlidl_z3_Z3_get_algebraic_number_upper" @@ -3501,6 +3987,8 @@ external get_algebraic_number_upper : context -> ast -> int -> ast (** Summary: Convert a pattern into ast. - {b Remarks}: [pattern_to_ast c p] can be replaced by [(p :> ast)]. + + def_API('pattern_to_ast', AST, (_in(CONTEXT), _in(PATTERN))) *) external pattern_to_ast : context -> pattern -> ast = "camlidl_z3_Z3_pattern_to_ast" @@ -3516,12 +4004,16 @@ val get_pattern_terms: context -> pattern -> ast array;; (** Summary: Return number of terms in pattern. + + def_API('get_pattern_num_terms', UINT, (_in(CONTEXT), _in(PATTERN))) *) external get_pattern_num_terms : context -> pattern -> int = "camlidl_z3_Z3_get_pattern_num_terms" (** Summary: Return i'th ast in pattern. + + def_API('get_pattern', AST, (_in(CONTEXT), _in(PATTERN), _in(UINT))) *) external get_pattern : context -> pattern -> int -> ast = "camlidl_z3_Z3_get_pattern" @@ -3533,6 +4025,8 @@ external get_pattern : context -> pattern -> int -> ast Summary: Return index of de-Brujin bound variable. - {b Precondition}: get_ast_kind a == VAR_AST + + def_API('get_index_value', UINT, (_in(CONTEXT), _in(AST))) *) external get_index_value : context -> ast -> int = "camlidl_z3_Z3_get_index_value" @@ -3541,6 +4035,8 @@ external get_index_value : context -> ast -> int Summary: Determine if quantifier is universal. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('is_quantifier_forall', BOOL, (_in(CONTEXT), _in(AST))) *) external is_quantifier_forall : context -> ast -> bool = "camlidl_z3_Z3_is_quantifier_forall" @@ -3549,6 +4045,8 @@ external is_quantifier_forall : context -> ast -> bool Summary: Obtain weight of quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_weight', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_weight : context -> ast -> int = "camlidl_z3_Z3_get_quantifier_weight" @@ -3557,6 +4055,8 @@ external get_quantifier_weight : context -> ast -> int Summary: Return number of patterns used in quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_num_patterns', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_num_patterns : context -> ast -> int = "camlidl_z3_Z3_get_quantifier_num_patterns" @@ -3565,6 +4065,8 @@ external get_quantifier_num_patterns : context -> ast -> int Summary: Return i'th pattern. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_pattern_ast', PATTERN, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_pattern_ast : context -> ast -> int -> pattern = "camlidl_z3_Z3_get_quantifier_pattern_ast" @@ -3573,6 +4075,8 @@ external get_quantifier_pattern_ast : context -> ast -> int -> pattern Summary: Return number of no_patterns used in quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_num_no_patterns', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_num_no_patterns : context -> ast -> int = "camlidl_z3_Z3_get_quantifier_num_no_patterns" @@ -3581,6 +4085,8 @@ external get_quantifier_num_no_patterns : context -> ast -> int Summary: Return i'th no_pattern. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_no_pattern_ast', AST, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_no_pattern_ast : context -> ast -> int -> ast = "camlidl_z3_Z3_get_quantifier_no_pattern_ast" @@ -3589,6 +4095,8 @@ external get_quantifier_no_pattern_ast : context -> ast -> int -> ast Summary: Return number of bound variables of quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_num_bound', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_num_bound : context -> ast -> int = "camlidl_z3_Z3_get_quantifier_num_bound" @@ -3597,6 +4105,8 @@ external get_quantifier_num_bound : context -> ast -> int Summary: Return symbol of the i'th bound variable. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_bound_name', SYMBOL, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_bound_name : context -> ast -> int -> symbol = "camlidl_z3_Z3_get_quantifier_bound_name" @@ -3605,6 +4115,8 @@ external get_quantifier_bound_name : context -> ast -> int -> symbol Summary: Return sort of the i'th bound variable. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_bound_sort', SORT, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_bound_sort : context -> ast -> int -> sort = "camlidl_z3_Z3_get_quantifier_bound_sort" @@ -3613,6 +4125,8 @@ external get_quantifier_bound_sort : context -> ast -> int -> sort Summary: Return body of quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_body', AST, (_in(CONTEXT), _in(AST))) *) external get_quantifier_body : context -> ast -> ast = "camlidl_z3_Z3_get_quantifier_body" @@ -3624,6 +4138,8 @@ external get_quantifier_body : context -> ast -> ast Summary: Interface to simplifier. Provides an interface to the AST simplifier used by Z3. + + def_API('simplify', AST, (_in(CONTEXT), _in(AST))) *) external simplify : context -> ast -> ast = "camlidl_z3_Z3_simplify" @@ -3634,18 +4150,24 @@ external simplify : context -> ast -> ast Provides an interface to the AST simplifier used by Z3. This procedure is similar to {!simplify}, but the behavior of the simplifier can be configured using the given parameter set. + + def_API('simplify_ex', AST, (_in(CONTEXT), _in(AST), _in(PARAMS))) *) external simplify_ex : context -> ast -> params -> ast = "camlidl_z3_Z3_simplify_ex" (** Summary: Return a string describing all available parameters. + + def_API('simplify_get_help', STRING, (_in(CONTEXT),)) *) external simplify_get_help : context -> string = "camlidl_z3_Z3_simplify_get_help" (** Summary: Return the parameter description set for the simplify procedure. + + def_API('simplify_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT),)) *) external simplify_get_param_descrs : context -> param_descrs = "camlidl_z3_Z3_simplify_get_param_descrs" @@ -3658,6 +4180,8 @@ external simplify_get_param_descrs : context -> param_descrs The number of arguments [num_args] should coincide with the number of arguments to [a]. If [a] is a quantifier, then num_args has to be 1. + + def_API('update_term', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST))) *) external update_term : context -> ast -> ast array -> ast = "camlidl_z3_Z3_update_term" @@ -3666,6 +4190,8 @@ external update_term : context -> ast -> ast array -> ast Summary: Substitute every occurrence of {e from[i] } in [a] with {e to[i] }, for [i] smaller than [num_exprs]. The result is the new AST. The arrays [from] and [to] must have size [num_exprs]. For every [i] smaller than [num_exprs], we must have that sort of {e from[i] } must be equal to sort of {e to[i] }. + + def_API('substitute', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST), _in_array(2, AST))) *) external substitute : context -> ast -> ast array -> ast array -> ast = "camlidl_z3_Z3_substitute" @@ -3673,6 +4199,8 @@ external substitute : context -> ast -> ast array -> ast array -> ast (** Summary: Substitute the free variables in [a] with the expressions in [to]. For every [i] smaller than [num_exprs], the variable with de-Bruijn index [i] is replaced with term {e to[i] }. + + def_API('substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST))) *) external substitute_vars : context -> ast -> ast array -> ast = "camlidl_z3_Z3_substitute_vars" @@ -3681,6 +4209,8 @@ external substitute_vars : context -> ast -> ast array -> ast Summary: Translate/Copy the AST [a] from context [source] to context [target]. AST [a] must have been created using context [source]. - {b Precondition}: source != target + + def_API('translate', AST, (_in(CONTEXT), _in(AST), _in(CONTEXT))) *) external translate : context -> ast -> context -> ast = "camlidl_z3_Z3_translate" @@ -3724,6 +4254,8 @@ val model_refine : context -> model -> model_refined That is, the option {e MODEL_PARTIAL=true } was used. - [t] is type incorrect. + + def_API('model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST))) *) external model_eval : context -> model -> ast -> bool -> ast option = "camlidl_z3_Z3_model_eval" @@ -3738,6 +4270,8 @@ external model_eval : context -> model -> ast -> bool -> ast option That should be interpreted as: the value of [a] does not matter. - {b Precondition}: get_arity c a == 0 + + def_API('model_get_const_interp', AST, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL))) *) external model_get_const_interp : context -> model -> func_decl -> ast option = "camlidl_z3_Z3_model_get_const_interp" @@ -3752,6 +4286,8 @@ external model_get_const_interp : context -> model -> func_decl -> ast option + + def_API('model_get_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL))) *) external model_get_func_interp : context -> model -> func_decl -> func_interp option = "camlidl_z3_Z3_model_get_func_interp" @@ -3760,6 +4296,8 @@ external model_get_func_interp : context -> model -> func_decl -> func_interp op Summary: Return the number of constants assigned by the given model. - {b See also}: {!model_get_const_decl} + + def_API('model_get_num_consts', UINT, (_in(CONTEXT), _in(MODEL))) *) external model_get_num_consts : context -> model -> int = "camlidl_z3_Z3_model_get_num_consts" @@ -3771,6 +4309,8 @@ external model_get_num_consts : context -> model -> int - {b Precondition}: i < model_get_num_consts c m - {b See also}: {!model_eval} + + def_API('model_get_const_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT))) *) external model_get_const_decl : context -> model -> int -> func_decl = "camlidl_z3_Z3_model_get_const_decl" @@ -3780,6 +4320,8 @@ external model_get_const_decl : context -> model -> int -> func_decl A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. + + def_API('model_get_num_funcs', UINT, (_in(CONTEXT), _in(MODEL))) *) external model_get_num_funcs : context -> model -> int = "camlidl_z3_Z3_model_get_num_funcs" @@ -3791,6 +4333,8 @@ external model_get_num_funcs : context -> model -> int - {b Precondition}: i < model_get_num_funcs c m - {b See also}: {!model_get_num_funcs} + + def_API('model_get_func_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT))) *) external model_get_func_decl : context -> model -> int -> func_decl = "camlidl_z3_Z3_model_get_func_decl" @@ -3804,6 +4348,8 @@ external model_get_func_decl : context -> model -> int -> func_decl - {b See also}: {!model_get_sort} - {b See also}: {!model_get_sort_universe} + + def_API('model_get_num_sorts', UINT, (_in(CONTEXT), _in(MODEL))) *) external model_get_num_sorts : context -> model -> int = "camlidl_z3_Z3_model_get_num_sorts" @@ -3815,6 +4361,8 @@ external model_get_num_sorts : context -> model -> int - {b See also}: {!model_get_num_sorts} - {b See also}: {!model_get_sort_universe} + + def_API('model_get_sort', SORT, (_in(CONTEXT), _in(MODEL), _in(UINT))) *) external model_get_sort : context -> model -> int -> sort = "camlidl_z3_Z3_model_get_sort" @@ -3824,6 +4372,8 @@ external model_get_sort : context -> model -> int -> sort - {b See also}: {!model_get_num_sorts} - {b See also}: {!model_get_sort} + + def_API('model_get_sort_universe', AST_VECTOR, (_in(CONTEXT), _in(MODEL), _in(SORT))) *) external model_get_sort_universe : context -> model -> sort -> ast_vector = "camlidl_z3_Z3_model_get_sort_universe" @@ -3836,6 +4386,8 @@ external model_get_sort_universe : context -> model -> sort -> ast_vector Z3 current solvers have minimal support for [as_array] nodes. - {b See also}: {!get_as_array_func_decl} + + def_API('is_as_array', BOOL, (_in(CONTEXT), _in(AST))) *) external is_as_array : context -> ast -> bool = "camlidl_z3_Z3_is_as_array" @@ -3844,6 +4396,8 @@ external is_as_array : context -> ast -> bool Summary: Return the function declaration [f] associated with a {e (_ as_array f) } node. - {b See also}: {!is_as_array} + + def_API('get_as_array_func_decl', FUNC_DECL, (_in(CONTEXT), _in(AST))) *) external get_as_array_func_decl : context -> ast -> func_decl = "camlidl_z3_Z3_get_as_array_func_decl" @@ -3854,6 +4408,8 @@ external get_as_array_func_decl : context -> ast -> func_decl A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. This procedure return the number of element in the finite map of [f]. + + def_API('func_interp_get_num_entries', UINT, (_in(CONTEXT), _in(FUNC_INTERP))) *) external func_interp_get_num_entries : context -> func_interp -> int = "camlidl_z3_Z3_func_interp_get_num_entries" @@ -3865,6 +4421,8 @@ external func_interp_get_num_entries : context -> func_interp -> int - {b Precondition}: i < func_interp_get_num_entries c f - {b See also}: {!func_interp_get_num_entries} + + def_API('func_interp_get_entry', FUNC_ENTRY, (_in(CONTEXT), _in(FUNC_INTERP), _in(UINT))) *) external func_interp_get_entry : context -> func_interp -> int -> func_entry = "camlidl_z3_Z3_func_interp_get_entry" @@ -3874,12 +4432,16 @@ external func_interp_get_entry : context -> func_interp -> int -> func_entry A function interpretation is represented as a finite map and an 'else' value. This procedure returns the 'else' value. + + def_API('func_interp_get_else', AST, (_in(CONTEXT), _in(FUNC_INTERP))) *) external func_interp_get_else : context -> func_interp -> ast = "camlidl_z3_Z3_func_interp_get_else" (** Summary: Return the arity (number of arguments) of the given function interpretation. + + def_API('func_interp_get_arity', UINT, (_in(CONTEXT), _in(FUNC_INTERP))) *) external func_interp_get_arity : context -> func_interp -> int = "camlidl_z3_Z3_func_interp_get_arity" @@ -3891,6 +4453,8 @@ external func_interp_get_arity : context -> func_interp -> int a function interpretation. - {b See also}: {!func_interp_get_entry} + + def_API('func_entry_get_value', AST, (_in(CONTEXT), _in(FUNC_ENTRY))) *) external func_entry_get_value : context -> func_entry -> ast = "camlidl_z3_Z3_func_entry_get_value" @@ -3899,6 +4463,8 @@ external func_entry_get_value : context -> func_entry -> ast Summary: Return the number of arguments in a func_entry object. - {b See also}: {!func_interp_get_entry} + + def_API('func_entry_get_num_args', UINT, (_in(CONTEXT), _in(FUNC_ENTRY))) *) external func_entry_get_num_args : context -> func_entry -> int = "camlidl_z3_Z3_func_entry_get_num_args" @@ -3909,6 +4475,8 @@ external func_entry_get_num_args : context -> func_entry -> int - {b Precondition}: i < func_entry_get_num_args c e - {b See also}: {!func_interp_get_entry} + + def_API('func_entry_get_arg', AST, (_in(CONTEXT), _in(FUNC_ENTRY), _in(UINT))) *) external func_entry_get_arg : context -> func_entry -> int -> ast = "camlidl_z3_Z3_func_entry_get_arg" @@ -3918,6 +4486,8 @@ external func_entry_get_arg : context -> func_entry -> int -> ast *) (** Summary: Log interaction to a file. + + extra_API('open_log', INT, (_in(STRING),)) *) external open_log : string -> bool = "camlidl_z3_Z3_open_log" @@ -3928,12 +4498,16 @@ external open_log : string -> bool The interaction log is opened using open_log. It contains the formulas that are checked using Z3. You can use this command to append comments, for instance. + + extra_API('append_log', VOID, (_in(STRING),)) *) external append_log : string -> unit = "camlidl_z3_Z3_append_log" (** Summary: Close interaction log. + + extra_API('close_log', VOID, ()) *) external close_log : unit -> unit = "camlidl_z3_Z3_close_log" @@ -3943,6 +4517,8 @@ external close_log : unit -> unit Warnings are printed after passing [true], warning messages are suppressed after calling this method with [false]. + + def_API('toggle_warning_messages', VOID, (_in(BOOL),)) *) external toggle_warning_messages : bool -> unit = "camlidl_z3_Z3_toggle_warning_messages" @@ -3965,6 +4541,7 @@ external toggle_warning_messages : bool -> unit - {b See also}: {!pattern_to_string} - {b See also}: {!func_decl_to_string} + def_API('set_ast_print_mode', VOID, (_in(CONTEXT), _in(PRINT_MODE))) *) external set_ast_print_mode : context -> ast_print_mode -> unit = "camlidl_z3_Z3_set_ast_print_mode" @@ -3977,16 +4554,27 @@ external set_ast_print_mode : context -> ast_print_mode -> unit - {b See also}: {!pattern_to_string} - {b See also}: {!sort_to_string} + + def_API('ast_to_string', STRING, (_in(CONTEXT), _in(AST))) *) external ast_to_string : context -> ast -> string = "camlidl_z3_Z3_ast_to_string" +(** + def_API('pattern_to_string', STRING, (_in(CONTEXT), _in(PATTERN))) +*) external pattern_to_string : context -> pattern -> string = "camlidl_z3_Z3_pattern_to_string" +(** + def_API('sort_to_string', STRING, (_in(CONTEXT), _in(SORT))) +*) external sort_to_string : context -> sort -> string = "camlidl_z3_Z3_sort_to_string" +(** + def_API('func_decl_to_string', STRING, (_in(CONTEXT), _in(FUNC_DECL))) +*) external func_decl_to_string : context -> func_decl -> string = "camlidl_z3_Z3_func_decl_to_string" @@ -3996,6 +4584,8 @@ external func_decl_to_string : context -> func_decl -> string + + def_API('model_to_string', STRING, (_in(CONTEXT), _in(MODEL))) *) external model_to_string : context -> model -> string = "camlidl_z3_Z3_model_to_string" @@ -4015,6 +4605,8 @@ external model_to_string : context -> model -> string @param num_assumptions - number of assumptions. @param assumptions - auxiliary assumptions. @param formula - formula to be checked for consistency in conjunction with assumptions. + + def_API('benchmark_to_smtlib_string', STRING, (_in(CONTEXT), _in(STRING), _in(STRING), _in(STRING), _in(STRING), _in(UINT), _in_array(5, AST), _in(AST))) *) external benchmark_to_smtlib_string : context -> string -> string -> string -> string -> ast array -> ast -> string = "camlidl_z3_Z3_benchmark_to_smtlib_string_bytecode" "camlidl_z3_Z3_benchmark_to_smtlib_string" @@ -4028,12 +4620,16 @@ external benchmark_to_smtlib_string : context -> string -> string -> string -> s It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string. + + def_API('parse_smtlib2_string', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib2_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast = "camlidl_z3_Z3_parse_smtlib2_string_bytecode" "camlidl_z3_Z3_parse_smtlib2_string" (** Summary: Similar to {!parse_smtlib2_string}, but reads the benchmark from a file. + + def_API('parse_smtlib2_file', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib2_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast = "camlidl_z3_Z3_parse_smtlib2_file_bytecode" "camlidl_z3_Z3_parse_smtlib2_file" @@ -4091,18 +4687,24 @@ val parse_smtlib_file_formula: context -> string -> symbol array -> sort array - The formulas, assumptions and declarations defined in [str] can be extracted using the functions: {!get_smtlib_num_formulas}, {!get_smtlib_formula}, {!get_smtlib_num_assumptions}, {!get_smtlib_assumption}, {!get_smtlib_num_decls}, and {!get_smtlib_decl}. + + def_API('parse_smtlib_string', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit = "camlidl_z3_Z3_parse_smtlib_string_bytecode" "camlidl_z3_Z3_parse_smtlib_string" (** Summary: Similar to {!parse_smtlib_string}, but reads the benchmark from a file. + + def_API('parse_smtlib_file', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit = "camlidl_z3_Z3_parse_smtlib_file_bytecode" "camlidl_z3_Z3_parse_smtlib_file" (** Summary: Return the number of SMTLIB formulas parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_formulas', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_formulas : context -> int = "camlidl_z3_Z3_get_smtlib_num_formulas" @@ -4112,12 +4714,16 @@ external get_smtlib_num_formulas : context -> int Return the i-th formula parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_formulas c + + def_API('get_smtlib_formula', AST, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_formula : context -> int -> ast = "camlidl_z3_Z3_get_smtlib_formula" (** Summary: Return the number of SMTLIB assumptions parsed by {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_assumptions', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_assumptions : context -> int = "camlidl_z3_Z3_get_smtlib_num_assumptions" @@ -4127,12 +4733,16 @@ external get_smtlib_num_assumptions : context -> int Return the i-th assumption parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_assumptions c + + def_API('get_smtlib_assumption', AST, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_assumption : context -> int -> ast = "camlidl_z3_Z3_get_smtlib_assumption" (** Summary: Return the number of declarations parsed by {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_decls', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_decls : context -> int = "camlidl_z3_Z3_get_smtlib_num_decls" @@ -4142,12 +4752,16 @@ external get_smtlib_num_decls : context -> int Return the i-th declaration parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_decls c + + def_API('get_smtlib_decl', FUNC_DECL, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_decl : context -> int -> func_decl = "camlidl_z3_Z3_get_smtlib_decl" (** Summary: Return the number of sorts parsed by {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_sorts', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_sorts : context -> int = "camlidl_z3_Z3_get_smtlib_num_sorts" @@ -4157,6 +4771,8 @@ external get_smtlib_num_sorts : context -> int Return the i-th sort parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_sorts c + + def_API('get_smtlib_sort', SORT, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_sort : context -> int -> sort = "camlidl_z3_Z3_get_smtlib_sort" @@ -4165,6 +4781,8 @@ external get_smtlib_sort : context -> int -> sort (** Summary: \[ [ get_smtlib_error c ] \] Retrieve that last error message information generated from parsing. + + def_API('get_smtlib_error', STRING, (_in(CONTEXT), )) *) external get_smtlib_error : context -> string = "camlidl_z3_Z3_get_smtlib_error" @@ -4175,12 +4793,16 @@ external get_smtlib_error : context -> string Parse the given string using the Z3 native parser. Return the conjunction of asserts made in the input. + + def_API('parse_z3_string', AST, (_in(CONTEXT), _in(STRING))) *) external parse_z3_string : context -> string -> ast = "camlidl_z3_Z3_parse_z3_string" (** Summary: Similar to {!parse_z3_string}, but reads the benchmark from a file. + + def_API('parse_z3_file', AST, (_in(CONTEXT), _in(STRING))) *) external parse_z3_file : context -> string -> ast = "camlidl_z3_Z3_parse_z3_file" @@ -4190,6 +4812,8 @@ external parse_z3_file : context -> string -> ast *) (** Summary: Set an error. + + def_API('set_error', VOID, (_in(CONTEXT), _in(ERROR_CODE))) *) external set_error : context -> error_code -> unit = "camlidl_z3_Z3_set_error" @@ -4197,6 +4821,8 @@ external set_error : context -> error_code -> unit (* (** Summary: Return a string describing the given error code. + + def_API('get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE))) *) external get_error_msg_ex : context -> error_code -> string = "camlidl_z3_Z3_get_error_msg_ex" @@ -4213,6 +4839,8 @@ val get_error_msg: context -> error_code -> string *) (** Summary: Return Z3 version number information. + + def_API('get_version', VOID, (_out(UINT), _out(UINT), _out(UINT), _out(UINT))) *) external get_version : unit -> int * int * int * int = "camlidl_z3_Z3_get_version" @@ -4225,6 +4853,8 @@ external get_version : unit -> int * int * int * int + + def_API('mk_fixedpoint', FIXEDPOINT, (_in(CONTEXT), )) *) external mk_fixedpoint : context -> fixedpoint = "camlidl_z3_Z3_mk_fixedpoint" @@ -4238,6 +4868,8 @@ external mk_fixedpoint : context -> fixedpoint | (=> atoms horn_rule) | atom v} + + def_API('fixedpoint_add_rule', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(SYMBOL))) *) external fixedpoint_add_rule : context -> fixedpoint -> ast -> symbol -> unit = "camlidl_z3_Z3_fixedpoint_add_rule" @@ -4256,7 +4888,8 @@ external fixedpoint_add_rule : context -> fixedpoint -> ast -> symbol -> unit (bit-vector, Boolean or or finite domain sort). The call has the same effect as adding a rule where is applied to the arguments. - + + def_API('fixedpoint_add_fact', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(UINT), _in_array(3, UINT))) *) external fixedpoint_add_fact : context -> fixedpoint -> func_decl -> int array -> unit = "camlidl_z3_Z3_fixedpoint_add_fact" @@ -4266,6 +4899,8 @@ external fixedpoint_add_fact : context -> fixedpoint -> func_decl -> int array - The constraints are used as background axioms when the fixedpoint engine uses the PDR mode. They are ignored for standard Datalog mode. + + def_API('fixedpoint_assert', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST))) *) external fixedpoint_assert : context -> fixedpoint -> ast -> unit = "camlidl_z3_Z3_fixedpoint_assert" @@ -4283,6 +4918,7 @@ external fixedpoint_assert : context -> fixedpoint -> ast -> unit - L_TRUE if the query is satisfiable. Obtain the answer by calling {!fixedpoint_get_answer}. - L_UNDEF if the query was interrupted, timed out or otherwise failed. + def_API('fixedpoint_query', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST))) *) external fixedpoint_query : context -> fixedpoint -> ast -> lbool = "camlidl_z3_Z3_fixedpoint_query" @@ -4297,6 +4933,7 @@ external fixedpoint_query : context -> fixedpoint -> ast -> lbool - L_TRUE if the query is satisfiable. Obtain the answer by calling {!fixedpoint_get_answer}. - L_UNDEF if the query was interrupted, timed out or otherwise failed. + def_API('fixedpoint_query_relations', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, FUNC_DECL))) *) external fixedpoint_query_relations : context -> fixedpoint -> func_decl array -> lbool = "camlidl_z3_Z3_fixedpoint_query_relations" @@ -4310,6 +4947,8 @@ external fixedpoint_query_relations : context -> fixedpoint -> func_decl array - In PDR mode, the returned answer is a single conjunction. The previous call to fixedpoint_query must have returned L_TRUE. + + def_API('fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT))) *) external fixedpoint_get_answer : context -> fixedpoint -> ast = "camlidl_z3_Z3_fixedpoint_get_answer" @@ -4318,6 +4957,8 @@ external fixedpoint_get_answer : context -> fixedpoint -> ast Summary: Retrieve a string that describes the last status returned by {!fixedpoint_query}. Use this method when {!fixedpoint_query} returns L_UNDEF. + + def_API('fixedpoint_get_reason_unknown', STRING, (_in(CONTEXT), _in(FIXEDPOINT) )) *) external fixedpoint_get_reason_unknown : context -> fixedpoint -> string = "camlidl_z3_Z3_fixedpoint_get_reason_unknown" @@ -4325,6 +4966,8 @@ external fixedpoint_get_reason_unknown : context -> fixedpoint -> string (** Summary: Update a named rule. A rule with the same name must have been previously created. + + def_API('fixedpoint_update_rule', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(SYMBOL))) *) external fixedpoint_update_rule : context -> fixedpoint -> ast -> symbol -> unit = "camlidl_z3_Z3_fixedpoint_update_rule" @@ -4335,6 +4978,8 @@ external fixedpoint_update_rule : context -> fixedpoint -> ast -> symbol -> unit This call retrieves the maximal number of relevant unfoldings of [pred] with respect to the current exploration state. Note: this functionality is PDR specific. + + def_API('fixedpoint_get_num_levels', UINT, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL))) *) external fixedpoint_get_num_levels : context -> fixedpoint -> func_decl -> int = "camlidl_z3_Z3_fixedpoint_get_num_levels" @@ -4346,6 +4991,8 @@ external fixedpoint_get_num_levels : context -> fixedpoint -> func_decl -> int at [level+1] , [level+2] etc, and include [level=-1]. Note: this functionality is PDR specific. + + def_API('fixedpoint_get_cover_delta', AST, (_in(CONTEXT), _in(FIXEDPOINT), _in(INT), _in(FUNC_DECL))) *) external fixedpoint_get_cover_delta : context -> fixedpoint -> int -> func_decl -> ast = "camlidl_z3_Z3_fixedpoint_get_cover_delta" @@ -4359,12 +5006,16 @@ external fixedpoint_get_cover_delta : context -> fixedpoint -> int -> func_decl means that the property is true of the fixed-point unfolding with respect to [pred]. Note: this functionality is PDR specific. + + def_API('fixedpoint_add_cover', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(INT), _in(FUNC_DECL), _in(AST))) *) external fixedpoint_add_cover : context -> fixedpoint -> int -> func_decl -> ast -> unit = "camlidl_z3_Z3_fixedpoint_add_cover" (** Summary: Retrieve statistics information from the last call to {!fixedpoint_query}. + + def_API('fixedpoint_get_statistics', STATS, (_in(CONTEXT), _in(FIXEDPOINT))) *) external fixedpoint_get_statistics : context -> fixedpoint -> stats = "camlidl_z3_Z3_fixedpoint_get_statistics" @@ -4374,6 +5025,8 @@ external fixedpoint_get_statistics : context -> fixedpoint -> stats Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact. + + def_API('fixedpoint_register_relation', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL))) *) external fixedpoint_register_relation : context -> fixedpoint -> func_decl -> unit = "camlidl_z3_Z3_fixedpoint_register_relation" @@ -4384,6 +5037,8 @@ external fixedpoint_register_relation : context -> fixedpoint -> func_decl -> un It sets the predicate to use a set of domains given by the list of symbols. The domains given by the list of symbols must belong to a set of built-in domains. + + def_API('fixedpoint_set_predicate_representation', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(UINT), _in_array(3, SYMBOL))) *) external fixedpoint_set_predicate_representation : context -> fixedpoint -> func_decl -> symbol array -> unit = "camlidl_z3_Z3_fixedpoint_set_predicate_representation" @@ -4392,24 +5047,32 @@ external fixedpoint_set_predicate_representation : context -> fixedpoint -> func Summary: Simplify rules into a set of new rules that are returned. The simplification routines apply inlining, quantifier elimination, and other algebraic simplifications. + + def_API('fixedpoint_simplify_rules', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2,AST), _in(UINT), _in_array(4,FUNC_DECL))) *) external fixedpoint_simplify_rules : context -> fixedpoint -> ast array -> func_decl array -> ast_vector = "camlidl_z3_Z3_fixedpoint_simplify_rules" (** Summary: Set parameters on fixedpoint context. + + def_API('fixedpoint_set_params', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(PARAMS))) *) external fixedpoint_set_params : context -> fixedpoint -> params -> unit = "camlidl_z3_Z3_fixedpoint_set_params" (** Summary: Return a string describing all fixedpoint available parameters. + + def_API('fixedpoint_get_help', STRING, (_in(CONTEXT), _in(FIXEDPOINT))) *) external fixedpoint_get_help : context -> fixedpoint -> string = "camlidl_z3_Z3_fixedpoint_get_help" (** Summary: Return the parameter description set for the given fixedpoint object. + + def_API('fixedpoint_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(FIXEDPOINT))) *) external fixedpoint_get_param_descrs : context -> fixedpoint -> param_descrs = "camlidl_z3_Z3_fixedpoint_get_param_descrs" @@ -4420,6 +5083,8 @@ external fixedpoint_get_param_descrs : context -> fixedpoint -> param_descrs @param f - fixedpoint context. @param num_queries - number of additional queries to print. @param queries - additional queries. + + def_API('fixedpoint_to_string', STRING, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, AST))) *) external fixedpoint_to_string : context -> fixedpoint -> ast array -> string = "camlidl_z3_Z3_fixedpoint_to_string" @@ -4431,6 +5096,8 @@ external fixedpoint_to_string : context -> fixedpoint -> ast array -> string The set of rules, facts and assertions are restored upon calling {!fixedpoint_pop}. - {b See also}: {!fixedpoint_pop} + + def_API('fixedpoint_push', VOID, (_in(CONTEXT), _in(FIXEDPOINT))) *) external fixedpoint_push : context -> fixedpoint -> unit = "camlidl_z3_Z3_fixedpoint_push" @@ -4438,9 +5105,11 @@ external fixedpoint_push : context -> fixedpoint -> unit (** Summary: Backtrack one backtracking point. - - {b See also}: {!fixedpoing_push} + - {b See also}: {!fixedpoint_push} - {b Precondition}: The number of calls to pop cannot exceed calls to push. + + def_API('fixedpoint_pop', VOID, (_in(CONTEXT), _in(FIXEDPOINT))) *) external fixedpoint_pop : context -> fixedpoint -> unit = "camlidl_z3_Z3_fixedpoint_pop" @@ -4453,12 +5122,16 @@ external fixedpoint_pop : context -> fixedpoint -> unit + + def_API('mk_ast_vector', AST_VECTOR, (_in(CONTEXT),)) *) external mk_ast_vector : context -> ast_vector = "camlidl_z3_Z3_mk_ast_vector" (** Summary: Return the size of the given AST vector. + + def_API('ast_vector_size', UINT, (_in(CONTEXT), _in(AST_VECTOR))) *) external ast_vector_size : context -> ast_vector -> int = "camlidl_z3_Z3_ast_vector_size" @@ -4467,6 +5140,8 @@ external ast_vector_size : context -> ast_vector -> int Summary: Return the AST at position [i] in the AST vector [v]. - {b Precondition}: i < ast_vector_size c v + + def_API('ast_vector_get', AST, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT))) *) external ast_vector_get : context -> ast_vector -> int -> ast = "camlidl_z3_Z3_ast_vector_get" @@ -4475,30 +5150,40 @@ external ast_vector_get : context -> ast_vector -> int -> ast Summary: Update position [i] of the AST vector [v] with the AST [a]. - {b Precondition}: i < ast_vector_size c v + + def_API('ast_vector_set', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT), _in(AST))) *) external ast_vector_set : context -> ast_vector -> int -> ast -> unit = "camlidl_z3_Z3_ast_vector_set" (** Summary: Resize the AST vector [v]. + + def_API('ast_vector_resize', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(UINT))) *) external ast_vector_resize : context -> ast_vector -> int -> unit = "camlidl_z3_Z3_ast_vector_resize" (** Summary: Add the AST [a] in the end of the AST vector [v]. The size of [v] is increased by one. + + def_API('ast_vector_push', VOID, (_in(CONTEXT), _in(AST_VECTOR), _in(AST))) *) external ast_vector_push : context -> ast_vector -> ast -> unit = "camlidl_z3_Z3_ast_vector_push" (** Summary: Translate the AST vector [v] from context [s] into an AST vector in context [t]. + + def_API('ast_vector_translate', AST_VECTOR, (_in(CONTEXT), _in(AST_VECTOR), _in(CONTEXT))) *) external ast_vector_translate : context -> ast_vector -> context -> ast_vector = "camlidl_z3_Z3_ast_vector_translate" (** Summary: Convert AST vector into a string. + + def_API('ast_vector_to_string', STRING, (_in(CONTEXT), _in(AST_VECTOR))) *) external ast_vector_to_string : context -> ast_vector -> string = "camlidl_z3_Z3_ast_vector_to_string" @@ -4511,12 +5196,16 @@ external ast_vector_to_string : context -> ast_vector -> string + + def_API('mk_ast_map', AST_MAP, (_in(CONTEXT),) ) *) external mk_ast_map : context -> ast_map = "camlidl_z3_Z3_mk_ast_map" (** Summary: Return true if the map [m] contains the AST key [k]. + + def_API('ast_map_contains', BOOL, (_in(CONTEXT), _in(AST_MAP), _in(AST))) *) external ast_map_contains : context -> ast_map -> ast -> bool = "camlidl_z3_Z3_ast_map_contains" @@ -4525,42 +5214,56 @@ external ast_map_contains : context -> ast_map -> ast -> bool Summary: Return the value associated with the key [k]. The procedure invokes the error handler if [k] is not in the map. + + def_API('ast_map_find', AST, (_in(CONTEXT), _in(AST_MAP), _in(AST))) *) external ast_map_find : context -> ast_map -> ast -> ast = "camlidl_z3_Z3_ast_map_find" (** Summary: Store/Replace a new key, value pair in the given map. + + def_API('ast_map_insert', VOID, (_in(CONTEXT), _in(AST_MAP), _in(AST), _in(AST))) *) external ast_map_insert : context -> ast_map -> ast -> ast -> unit = "camlidl_z3_Z3_ast_map_insert" (** Summary: Erase a key from the map. + + def_API('ast_map_erase', VOID, (_in(CONTEXT), _in(AST_MAP), _in(AST))) *) external ast_map_erase : context -> ast_map -> ast -> unit = "camlidl_z3_Z3_ast_map_erase" (** Summary: Remove all keys from the given map. + + def_API('ast_map_reset', VOID, (_in(CONTEXT), _in(AST_MAP))) *) external ast_map_reset : context -> ast_map -> unit = "camlidl_z3_Z3_ast_map_reset" (** Summary: Return the size of the given map. + + def_API('ast_map_size', UINT, (_in(CONTEXT), _in(AST_MAP))) *) external ast_map_size : context -> ast_map -> int = "camlidl_z3_Z3_ast_map_size" (** Summary: Return the keys stored in the given map. + + def_API('ast_map_keys', AST_VECTOR, (_in(CONTEXT), _in(AST_MAP))) *) external ast_map_keys : context -> ast_map -> ast_vector = "camlidl_z3_Z3_ast_map_keys" (** Summary: Convert the given map into a string. + + def_API('ast_map_to_string', STRING, (_in(CONTEXT), _in(AST_MAP))) *) external ast_map_to_string : context -> ast_map -> string = "camlidl_z3_Z3_ast_map_to_string" @@ -4582,6 +5285,8 @@ external ast_map_to_string : context -> ast_map -> string + + def_API('mk_goal', GOAL, (_in(CONTEXT), _in(BOOL), _in(BOOL), _in(BOOL))) *) external mk_goal : context -> bool -> bool -> bool -> goal = "camlidl_z3_Z3_mk_goal" @@ -4590,36 +5295,48 @@ external mk_goal : context -> bool -> bool -> bool -> goal Summary: Return the "precision" of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal. + + def_API('goal_precision', UINT, (_in(CONTEXT), _in(GOAL))) *) external goal_precision : context -> goal -> goal_prec = "camlidl_z3_Z3_goal_precision" (** Summary: Add a new formula [a] to the given goal. + + def_API('goal_assert', VOID, (_in(CONTEXT), _in(GOAL), _in(AST))) *) external goal_assert : context -> goal -> ast -> unit = "camlidl_z3_Z3_goal_assert" (** Summary: Return true if the given goal contains the formula [false]. + + def_API('goal_inconsistent', BOOL, (_in(CONTEXT), _in(GOAL))) *) external goal_inconsistent : context -> goal -> bool = "camlidl_z3_Z3_goal_inconsistent" (** Summary: Return the depth of the given goal. It tracks how many transformations were applied to it. + + def_API('goal_depth', UINT, (_in(CONTEXT), _in(GOAL))) *) external goal_depth : context -> goal -> int = "camlidl_z3_Z3_goal_depth" (** Summary: Erase all formulas from the given goal. + + def_API('goal_reset', VOID, (_in(CONTEXT), _in(GOAL))) *) external goal_reset : context -> goal -> unit = "camlidl_z3_Z3_goal_reset" (** Summary: Return the number of formulas in the given goal. + + def_API('goal_size', UINT, (_in(CONTEXT), _in(GOAL))) *) external goal_size : context -> goal -> int = "camlidl_z3_Z3_goal_size" @@ -4628,36 +5345,48 @@ external goal_size : context -> goal -> int Summary: Return a formula from the given goal. - {b Precondition}: idx < goal_size c g + + def_API('goal_formula', AST, (_in(CONTEXT), _in(GOAL), _in(UINT))) *) external goal_formula : context -> goal -> int -> ast = "camlidl_z3_Z3_goal_formula" (** Summary: Return the number of formulas, subformulas and terms in the given goal. + + def_API('goal_num_exprs', UINT, (_in(CONTEXT), _in(GOAL))) *) external goal_num_exprs : context -> goal -> int = "camlidl_z3_Z3_goal_num_exprs" (** Summary: Return true if the goal is empty, and it is precise or the product of a under approximation. + + def_API('goal_is_decided_sat', BOOL, (_in(CONTEXT), _in(GOAL))) *) external goal_is_decided_sat : context -> goal -> bool = "camlidl_z3_Z3_goal_is_decided_sat" (** Summary: Return true if the goal contains false, and it is precise or the product of an over approximation. + + def_API('goal_is_decided_unsat', BOOL, (_in(CONTEXT), _in(GOAL))) *) external goal_is_decided_unsat : context -> goal -> bool = "camlidl_z3_Z3_goal_is_decided_unsat" (** Summary: Copy a goal [g] from the context [source] to a the context [target]. + + def_API('goal_translate', GOAL, (_in(CONTEXT), _in(GOAL), _in(CONTEXT))) *) external goal_translate : context -> goal -> context -> goal = "camlidl_z3_Z3_goal_translate" (** Summary: Convert a goal into a string. + + def_API('goal_to_string', STRING, (_in(CONTEXT), _in(GOAL))) *) external goal_to_string : context -> goal -> string = "camlidl_z3_Z3_goal_to_string" @@ -4671,6 +5400,8 @@ external goal_to_string : context -> goal -> string It may also be obtained using the command {e (help-tactics) } in the SMT 2.0 front-end. Tactics are the basic building block for creating custom solvers for specific problem domains. + + def_API('mk_tactic', TACTIC, (_in(CONTEXT), _in(STRING))) *) external mk_tactic : context -> string -> tactic = "camlidl_z3_Z3_mk_tactic" @@ -4682,6 +5413,8 @@ external mk_tactic : context -> string -> tactic Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. + + def_API('mk_probe', PROBE, (_in(CONTEXT), _in(STRING))) *) external mk_probe : context -> string -> probe = "camlidl_z3_Z3_mk_probe" @@ -4689,6 +5422,8 @@ external mk_probe : context -> string -> probe (** Summary: Return a tactic that applies [t1] to a given goal and [t2] to every subgoal produced by t1. + + def_API('tactic_and_then', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(TACTIC))) *) external tactic_and_then : context -> tactic -> tactic -> tactic = "camlidl_z3_Z3_tactic_and_then" @@ -4696,12 +5431,16 @@ external tactic_and_then : context -> tactic -> tactic -> tactic (** Summary: Return a tactic that first applies [t1] to a given goal, if it fails then returns the result of [t2] applied to the given goal. + + def_API('tactic_or_else', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(TACTIC))) *) external tactic_or_else : context -> tactic -> tactic -> tactic = "camlidl_z3_Z3_tactic_or_else" (** Summary: Return a tactic that applies the given tactics in parallel. + + def_API('tactic_par_or', TACTIC, (_in(CONTEXT), _in(UINT), _in_array(1, TACTIC))) *) external tactic_par_or : context -> tactic array -> tactic = "camlidl_z3_Z3_tactic_par_or" @@ -4709,6 +5448,8 @@ external tactic_par_or : context -> tactic array -> tactic (** Summary: Return a tactic that applies [t1] to a given goal and then [t2] to every subgoal produced by t1. The subgoals are processed in parallel. + + def_API('tactic_par_and_then', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(TACTIC))) *) external tactic_par_and_then : context -> tactic -> tactic -> tactic = "camlidl_z3_Z3_tactic_par_and_then" @@ -4716,6 +5457,8 @@ external tactic_par_and_then : context -> tactic -> tactic -> tactic (** Summary: Return a tactic that applies [t] to a given goal for [ms] milliseconds. If [t] does not terminate in [ms] milliseconds, then it fails. + + def_API('tactic_try_for', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(UINT))) *) external tactic_try_for : context -> tactic -> int -> tactic = "camlidl_z3_Z3_tactic_try_for" @@ -4723,6 +5466,8 @@ external tactic_try_for : context -> tactic -> int -> tactic (** Summary: Return a tactic that applies [t] to a given goal is the probe [p] evaluates to true. If [p] evaluates to false, then the new tactic behaves like the skip tactic. + + def_API('tactic_when', TACTIC, (_in(CONTEXT), _in(PROBE), _in(TACTIC))) *) external tactic_when : context -> probe -> tactic -> tactic = "camlidl_z3_Z3_tactic_when" @@ -4730,6 +5475,8 @@ external tactic_when : context -> probe -> tactic -> tactic (** Summary: Return a tactic that applies [t1] to a given goal if the probe [p] evaluates to true, and [t2] if [p] evaluates to false. + + def_API('tactic_cond', TACTIC, (_in(CONTEXT), _in(PROBE), _in(TACTIC), _in(TACTIC))) *) external tactic_cond : context -> probe -> tactic -> tactic -> tactic = "camlidl_z3_Z3_tactic_cond" @@ -4737,24 +5484,32 @@ external tactic_cond : context -> probe -> tactic -> tactic -> tactic (** Summary: Return a tactic that keeps applying [t] until the goal is not modified anymore or the maximum number of iterations [max] is reached. + + def_API('tactic_repeat', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(UINT))) *) external tactic_repeat : context -> tactic -> int -> tactic = "camlidl_z3_Z3_tactic_repeat" (** Summary: Return a tactic that just return the given goal. + + def_API('tactic_skip', TACTIC, (_in(CONTEXT),)) *) external tactic_skip : context -> tactic = "camlidl_z3_Z3_tactic_skip" (** Summary: Return a tactic that always fails. + + def_API('tactic_fail', TACTIC, (_in(CONTEXT),)) *) external tactic_fail : context -> tactic = "camlidl_z3_Z3_tactic_fail" (** Summary: Return a tactic that fails if the probe [p] evaluates to false. + + def_API('tactic_fail_if', TACTIC, (_in(CONTEXT), _in(PROBE))) *) external tactic_fail_if : context -> probe -> tactic = "camlidl_z3_Z3_tactic_fail_if" @@ -4762,18 +5517,24 @@ external tactic_fail_if : context -> probe -> tactic (** Summary: Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false). + + def_API('tactic_fail_if_not_decided', TACTIC, (_in(CONTEXT),)) *) external tactic_fail_if_not_decided : context -> tactic = "camlidl_z3_Z3_tactic_fail_if_not_decided" (** Summary: Return a tactic that applies [t] using the given set of parameters. + + def_API('tactic_using_params', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(PARAMS))) *) external tactic_using_params : context -> tactic -> params -> tactic = "camlidl_z3_Z3_tactic_using_params" (** Summary: Return a probe that always evaluates to val. + + def_API('probe_const', PROBE, (_in(CONTEXT), _in(DOUBLE))) *) external probe_const : context -> float -> probe = "camlidl_z3_Z3_probe_const" @@ -4782,6 +5543,8 @@ external probe_const : context -> float -> probe Summary: Return a probe that evaluates to "true" when the value returned by [p1] is less than the value returned by [p2]. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_lt', PROBE, (_in(CONTEXT), _in(PROBE), _in(PROBE))) *) external probe_lt : context -> probe -> probe -> probe = "camlidl_z3_Z3_probe_lt" @@ -4790,6 +5553,8 @@ external probe_lt : context -> probe -> probe -> probe Summary: Return a probe that evaluates to "true" when the value returned by [p1] is greater than the value returned by [p2]. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_gt', PROBE, (_in(CONTEXT), _in(PROBE), _in(PROBE))) *) external probe_gt : context -> probe -> probe -> probe = "camlidl_z3_Z3_probe_gt" @@ -4798,6 +5563,8 @@ external probe_gt : context -> probe -> probe -> probe Summary: Return a probe that evaluates to "true" when the value returned by [p1] is less than or equal to the value returned by [p2]. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_le', PROBE, (_in(CONTEXT), _in(PROBE), _in(PROBE))) *) external probe_le : context -> probe -> probe -> probe = "camlidl_z3_Z3_probe_le" @@ -4806,6 +5573,8 @@ external probe_le : context -> probe -> probe -> probe Summary: Return a probe that evaluates to "true" when the value returned by [p1] is greater than or equal to the value returned by [p2]. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_ge', PROBE, (_in(CONTEXT), _in(PROBE), _in(PROBE))) *) external probe_ge : context -> probe -> probe -> probe = "camlidl_z3_Z3_probe_ge" @@ -4814,6 +5583,8 @@ external probe_ge : context -> probe -> probe -> probe Summary: Return a probe that evaluates to "true" when the value returned by [p1] is equal to the value returned by [p2]. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_eq', PROBE, (_in(CONTEXT), _in(PROBE), _in(PROBE))) *) external probe_eq : context -> probe -> probe -> probe = "camlidl_z3_Z3_probe_eq" @@ -4822,6 +5593,8 @@ external probe_eq : context -> probe -> probe -> probe Summary: Return a probe that evaluates to "true" when [p1] and [p2] evaluates to true. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_and', PROBE, (_in(CONTEXT), _in(PROBE), _in(PROBE))) *) external probe_and : context -> probe -> probe -> probe = "camlidl_z3_Z3_probe_and" @@ -4830,6 +5603,8 @@ external probe_and : context -> probe -> probe -> probe Summary: Return a probe that evaluates to "true" when [p1] or [p2] evaluates to true. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_or', PROBE, (_in(CONTEXT), _in(PROBE), _in(PROBE))) *) external probe_or : context -> probe -> probe -> probe = "camlidl_z3_Z3_probe_or" @@ -4838,12 +5613,16 @@ external probe_or : context -> probe -> probe -> probe Summary: Return a probe that evaluates to "true" when [p] does not evaluate to true. - {b Remarks}: For probes, "true" is any value different from 0.0. + + def_API('probe_not', PROBE, (_in(CONTEXT), _in(PROBE))) *) external probe_not : context -> probe -> probe = "camlidl_z3_Z3_probe_not" (** Summary: Return the number of builtin tactics available in Z3. + + def_API('get_num_tactics', UINT, (_in(CONTEXT),)) *) external get_num_tactics : context -> int = "camlidl_z3_Z3_get_num_tactics" @@ -4852,12 +5631,16 @@ external get_num_tactics : context -> int Summary: Return the name of the idx tactic. - {b Precondition}: i < get_num_tactics c + + def_API('get_tactic_name', STRING, (_in(CONTEXT), _in(UINT))) *) external get_tactic_name : context -> int -> string = "camlidl_z3_Z3_get_tactic_name" (** Summary: Return the number of builtin probes available in Z3. + + def_API('get_num_probes', UINT, (_in(CONTEXT),)) *) external get_num_probes : context -> int = "camlidl_z3_Z3_get_num_probes" @@ -4866,30 +5649,40 @@ external get_num_probes : context -> int Summary: Return the name of the i probe. - {b Precondition}: i < get_num_probes c + + def_API('get_probe_name', STRING, (_in(CONTEXT), _in(UINT))) *) external get_probe_name : context -> int -> string = "camlidl_z3_Z3_get_probe_name" (** Summary: Return a string containing a description of parameters accepted by the given tactic. + + def_API('tactic_get_help', STRING, (_in(CONTEXT), _in(TACTIC))) *) external tactic_get_help : context -> tactic -> string = "camlidl_z3_Z3_tactic_get_help" (** Summary: Return the parameter description set for the given tactic object. + + def_API('tactic_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(TACTIC))) *) external tactic_get_param_descrs : context -> tactic -> param_descrs = "camlidl_z3_Z3_tactic_get_param_descrs" (** Summary: Return a string containing a description of the tactic with the given name. + + def_API('tactic_get_descr', STRING, (_in(CONTEXT), _in(STRING))) *) external tactic_get_descr : context -> string -> string = "camlidl_z3_Z3_tactic_get_descr" (** Summary: Return a string containing a description of the probe with the given name. + + def_API('probe_get_descr', STRING, (_in(CONTEXT), _in(STRING))) *) external probe_get_descr : context -> string -> string = "camlidl_z3_Z3_probe_get_descr" @@ -4897,30 +5690,40 @@ external probe_get_descr : context -> string -> string (** Summary: Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. + + def_API('probe_apply', DOUBLE, (_in(CONTEXT), _in(PROBE), _in(GOAL))) *) external probe_apply : context -> probe -> goal -> float = "camlidl_z3_Z3_probe_apply" (** Summary: Apply tactic [t] to the goal [g]. + + def_API('tactic_apply', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL))) *) external tactic_apply : context -> tactic -> goal -> apply_result = "camlidl_z3_Z3_tactic_apply" (** Summary: Apply tactic [t] to the goal [g] using the parameter set [p]. + + def_API('tactic_apply_ex', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL), _in(PARAMS))) *) external tactic_apply_ex : context -> tactic -> goal -> params -> apply_result = "camlidl_z3_Z3_tactic_apply_ex" (** Summary: Convert the [apply_result] object returned by {!tactic_apply} into a string. + + def_API('apply_result_to_string', STRING, (_in(CONTEXT), _in(APPLY_RESULT))) *) external apply_result_to_string : context -> apply_result -> string = "camlidl_z3_Z3_apply_result_to_string" (** Summary: Return the number of subgoals in the [apply_result] object returned by {!tactic_apply}. + + def_API('apply_result_get_num_subgoals', UINT, (_in(CONTEXT), _in(APPLY_RESULT))) *) external apply_result_get_num_subgoals : context -> apply_result -> int = "camlidl_z3_Z3_apply_result_get_num_subgoals" @@ -4929,6 +5732,8 @@ external apply_result_get_num_subgoals : context -> apply_result -> int Summary: Return one of the subgoals in the [apply_result] object returned by {!tactic_apply}. - {b Precondition}: i < apply_result_get_num_subgoals c r + + def_API('apply_result_get_subgoal', GOAL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT))) *) external apply_result_get_subgoal : context -> apply_result -> int -> goal = "camlidl_z3_Z3_apply_result_get_subgoal" @@ -4936,6 +5741,8 @@ external apply_result_get_subgoal : context -> apply_result -> int -> goal (** Summary: Convert a model for the subgoal [apply_result_get_subgoal(c], r, i) into a model for the original goal [g]. Where [g] is the goal used to create [r] using [tactic_apply(c], t, g). + + def_API('apply_result_convert_model', MODEL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT), _in(MODEL))) *) external apply_result_convert_model : context -> apply_result -> int -> model -> model = "camlidl_z3_Z3_apply_result_convert_model" @@ -4950,12 +5757,16 @@ external apply_result_convert_model : context -> apply_result -> int -> model -> + + def_API('mk_solver', SOLVER, (_in(CONTEXT),)) *) external mk_solver : context -> solver = "camlidl_z3_Z3_mk_solver" (** Summary: Create a new (incremental) solver. + + def_API('mk_simple_solver', SOLVER, (_in(CONTEXT),)) *) external mk_simple_solver : context -> solver = "camlidl_z3_Z3_mk_simple_solver" @@ -4966,6 +5777,8 @@ external mk_simple_solver : context -> solver + + def_API('mk_solver_for_logic', SOLVER, (_in(CONTEXT), _in(SYMBOL))) *) external mk_solver_for_logic : context -> symbol -> solver = "camlidl_z3_Z3_mk_solver_for_logic" @@ -4974,24 +5787,32 @@ external mk_solver_for_logic : context -> symbol -> solver Summary: Create a new solver that is implemented using the given tactic. The solver supports the commands {!solver_push} and {!solver_pop}, but it will always solve each {!solver_check} from scratch. + + def_API('mk_solver_from_tactic', SOLVER, (_in(CONTEXT), _in(TACTIC))) *) external mk_solver_from_tactic : context -> tactic -> solver = "camlidl_z3_Z3_mk_solver_from_tactic" (** Summary: Return a string describing all solver available parameters. + + def_API('solver_get_help', STRING, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_help : context -> solver -> string = "camlidl_z3_Z3_solver_get_help" (** Summary: Return the parameter description set for the given solver object. + + def_API('solver_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_param_descrs : context -> solver -> param_descrs = "camlidl_z3_Z3_solver_get_param_descrs" (** Summary: Set the given solver using the given parameters. + + def_API('solver_set_params', VOID, (_in(CONTEXT), _in(SOLVER), _in(PARAMS))) *) external solver_set_params : context -> solver -> params -> unit = "camlidl_z3_Z3_solver_set_params" @@ -5002,6 +5823,8 @@ external solver_set_params : context -> solver -> params -> unit The solver contains a stack of assertions. - {b See also}: {!solver_pop} + + def_API('solver_push', VOID, (_in(CONTEXT), _in(SOLVER))) *) external solver_push : context -> solver -> unit = "camlidl_z3_Z3_solver_push" @@ -5012,12 +5835,16 @@ external solver_push : context -> solver -> unit - {b See also}: {!solver_push} - {b Precondition}: n <= solver_get_num_scopes c s + + def_API('solver_pop', VOID, (_in(CONTEXT), _in(SOLVER), _in(UINT))) *) external solver_pop : context -> solver -> int -> unit = "camlidl_z3_Z3_solver_pop" (** Summary: Remove all assertions from the solver. + + def_API('solver_reset', VOID, (_in(CONTEXT), _in(SOLVER))) *) external solver_reset : context -> solver -> unit = "camlidl_z3_Z3_solver_reset" @@ -5027,6 +5854,8 @@ external solver_reset : context -> solver -> unit - {b See also}: {!solver_push} - {b See also}: {!solver_pop} + + def_API('solver_get_num_scopes', UINT, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_num_scopes : context -> solver -> int = "camlidl_z3_Z3_solver_get_num_scopes" @@ -5036,12 +5865,16 @@ external solver_get_num_scopes : context -> solver -> int The functions {!solver_check} and {!solver_check_assumptions} should be used to check whether the logical context is consistent or not. + + def_API('solver_assert', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST))) *) external solver_assert : context -> solver -> ast -> unit = "camlidl_z3_Z3_solver_assert" (** Summary: Return the set of asserted formulas as a goal object. + + def_API('solver_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_assertions : context -> solver -> ast_vector = "camlidl_z3_Z3_solver_get_assertions" @@ -5056,6 +5889,8 @@ external solver_get_assertions : context -> solver -> ast_vector The function {!solver_get_proof} retrieves a proof if proof generation was enabled when the context was created, and the assertions are unsatisfiable (i.e., the result is [L_FALSE)]. + + def_API('solver_check', INT, (_in(CONTEXT), _in(SOLVER))) *) external solver_check : context -> solver -> lbool = "camlidl_z3_Z3_solver_check" @@ -5068,6 +5903,8 @@ external solver_check : context -> solver -> lbool assumptions used in the unsatisfiability proof produced by Z3. - {b See also}: {!solver_check} + + def_API('solver_check_assumptions', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST))) *) external solver_check_assumptions : context -> solver -> ast array -> lbool = "camlidl_z3_Z3_solver_check_assumptions" @@ -5077,6 +5914,8 @@ external solver_check_assumptions : context -> solver -> ast array -> lbool The error handler is invoked if a model is not available because the commands above were not invoked for the given solver, or if the result was [L_FALSE]. + + def_API('solver_get_model', MODEL, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_model : context -> solver -> model = "camlidl_z3_Z3_solver_get_model" @@ -5087,6 +5926,8 @@ external solver_get_model : context -> solver -> model The error handler is invoked if proof generation is not enabled, or if the commands above were not invoked for the given solver, or if the result was different from [L_FALSE]. + + def_API('solver_get_proof', AST, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_proof : context -> solver -> ast = "camlidl_z3_Z3_solver_get_proof" @@ -5094,6 +5935,8 @@ external solver_get_proof : context -> solver -> ast (** Summary: Retrieve the unsat core for the last {!solver_check_assumptions} The unsat core is a subset of the assumptions [a]. + + def_API('solver_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_unsat_core : context -> solver -> ast_vector = "camlidl_z3_Z3_solver_get_unsat_core" @@ -5101,6 +5944,8 @@ external solver_get_unsat_core : context -> solver -> ast_vector (** Summary: Return a brief justification for an "unknown" result (i.e., L_UNDEF) for the commands {!solver_check} and {!solver_check_assumptions} + + def_API('solver_get_reason_unknown', STRING, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_reason_unknown : context -> solver -> string = "camlidl_z3_Z3_solver_get_reason_unknown" @@ -5109,12 +5954,16 @@ external solver_get_reason_unknown : context -> solver -> string Summary: Return statistics for the given solver. + + def_API('solver_get_statistics', STATS, (_in(CONTEXT), _in(SOLVER))) *) external solver_get_statistics : context -> solver -> stats = "camlidl_z3_Z3_solver_get_statistics" (** Summary: Convert a solver into a string. + + def_API('solver_to_string', STRING, (_in(CONTEXT), _in(SOLVER))) *) external solver_to_string : context -> solver -> string = "camlidl_z3_Z3_solver_to_string" @@ -5134,6 +5983,8 @@ val stats_refine : context -> stats -> stats_refined (** Summary: Convert a statistics into a string. + + def_API('stats_to_string', STRING, (_in(CONTEXT), _in(STATS))) *) external stats_to_string : context -> stats -> string = "camlidl_z3_Z3_stats_to_string" @@ -5143,6 +5994,8 @@ external stats_to_string : context -> stats -> string *) (** Summary: Return the number of statistical data in [s]. + + def_API('stats_size', UINT, (_in(CONTEXT), _in(STATS))) *) external stats_size : context -> stats -> int = "camlidl_z3_Z3_stats_size" @@ -5151,6 +6004,8 @@ external stats_size : context -> stats -> int Summary: Return the key (a string) for a particular statistical data. - {b Precondition}: idx < stats_size c s + + def_API('stats_get_key', STRING, (_in(CONTEXT), _in(STATS), _in(UINT))) *) external stats_get_key : context -> stats -> int -> string = "camlidl_z3_Z3_stats_get_key" @@ -5159,6 +6014,8 @@ external stats_get_key : context -> stats -> int -> string Summary: Return TRUE if the given statistical data is a unsigned int integer. - {b Precondition}: idx < stats_size c s + + def_API('stats_is_uint', BOOL, (_in(CONTEXT), _in(STATS), _in(UINT))) *) external stats_is_uint : context -> stats -> int -> bool = "camlidl_z3_Z3_stats_is_uint" @@ -5167,6 +6024,8 @@ external stats_is_uint : context -> stats -> int -> bool Summary: Return TRUE if the given statistical data is a double. - {b Precondition}: idx < stats_size c s + + def_API('stats_is_double', BOOL, (_in(CONTEXT), _in(STATS), _in(UINT))) *) external stats_is_double : context -> stats -> int -> bool = "camlidl_z3_Z3_stats_is_double" @@ -5175,6 +6034,8 @@ external stats_is_double : context -> stats -> int -> bool Summary: Return the unsigned int value of the given statistical data. - {b Precondition}: idx < stats_size c s && stats_is_uint c s + + def_API('stats_get_uint_value', UINT, (_in(CONTEXT), _in(STATS), _in(UINT))) *) external stats_get_uint_value : context -> stats -> int -> int = "camlidl_z3_Z3_stats_get_uint_value" @@ -5183,6 +6044,8 @@ external stats_get_uint_value : context -> stats -> int -> int Summary: Return the double value of the given statistical data. - {b Precondition}: idx < stats_size c s && stats_is_double c s + + def_API('stats_get_double_value', DOUBLE, (_in(CONTEXT), _in(STATS), _in(UINT))) *) external stats_get_double_value : context -> stats -> int -> float = "camlidl_z3_Z3_stats_get_double_value" @@ -5384,6 +6247,7 @@ and decl_kind = | OP_PR_SKOLEMIZE | OP_PR_MODUS_PONENS_OEQ | OP_PR_TH_LEMMA + | OP_PR_HYPER_RESOLVE | OP_RA_STORE | OP_RA_EMPTY | OP_RA_IS_EMPTY @@ -6051,6 +6915,47 @@ and ast_print_mode = - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. + - OP_PR_HYPER_RESOLVE: Hyper-resolution rule. + + The premises of the rules is a sequence of clauses. + The first clause argument is the main clause of the rule. + One literal from the second, third, .. clause is resolved + with a literal from the first (main) clause. + + Premises of the rules are of the form + {e + (or l0 l1 l2 .. ln) + } + or + {e + (=> (and ln+1 ln+2 .. ln+m) l0) + } + or in the most general (ground) form: + {e + (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)) + } + In other words we use the following (Prolog style) convention for Horn + implications: + The head of a Horn implication is position 0, + the first conjunct in the body of an implication is position 1 + the second conjunct in the body of an implication is position 2 + + For general implications where the head is a disjunction, the + first n positions correspond to the n disjuncts in the head. + The next m positions correspond to the m conjuncts in the body. + + The premises can be universally quantified so that the most + general non-ground form is: + + {e + (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))) + } + + The hyper-resolution rule takes a sequence of parameters. + The parameters are substitutions of bound variables separated by pairs + of literal positions from the main clause and side clause. + + - OP_RA_STORE: Insert a record into a relation. The function takes [n+1] arguments, where the first argument is the relation and the remaining [n] elements correspond to the [n] columns of the relation. @@ -6157,6 +7062,36 @@ and ast_print_mode = - PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format. - PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format. *) +(** + Definitions for update_api.py + + def_Type('CONFIG', 'config', 'Config') + def_Type('CONTEXT', 'context', 'ContextObj') + def_Type('AST', 'ast', 'Ast') + def_Type('APP', 'app', 'Ast') + def_Type('SORT', 'sort', 'Sort') + def_Type('FUNC_DECL', 'func_decl', 'FuncDecl') + def_Type('PATTERN', 'pattern', 'Pattern') + def_Type('MODEL', 'model', 'Model') + def_Type('LITERALS', 'literals', 'Literals') + def_Type('CONSTRUCTOR', 'constructor', 'Constructor') + def_Type('CONSTRUCTOR_LIST', 'constructor_list', 'ConstructorList') + def_Type('THEORY', 'theory', 'ctypes.c_void_p') + def_Type('THEORY_DATA', 'theory_data', 'ctypes.c_void_p') + def_Type('SOLVER', 'solver', 'SolverObj') + def_Type('GOAL', 'goal', 'GoalObj') + def_Type('TACTIC', 'tactic', 'TacticObj') + def_Type('PARAMS', 'params', 'Params') + def_Type('PROBE', 'probe', 'ProbeObj') + def_Type('STATS', 'stats', 'StatsObj') + def_Type('AST_VECTOR', 'ast_vector', 'AstVectorObj') + def_Type('AST_MAP', 'ast_map', 'AstMapObj') + def_Type('APPLY_RESULT', 'apply_result', 'ApplyResultObj') + def_Type('FUNC_INTERP', 'func_interp', 'FuncInterpObj') + def_Type('FUNC_ENTRY', 'func_entry', 'FuncEntryObj') + def_Type('FIXEDPOINT', 'fixedpoint', 'FixedpointObj') + def_Type('PARAM_DESCRS', 'param_descrs', 'ParamDescrs') +*) (** {2 {L Create configuration}} *) @@ -6176,6 +7111,8 @@ and ast_print_mode = - {b See also}: {!set_param_value} - {b See also}: {!del_config} + + def_API('mk_config', CONFIG, ()) *) external mk_config : unit -> config = "camlidl_z3V3_Z3_mk_config" @@ -6184,6 +7121,8 @@ external mk_config : unit -> config Summary: Delete the given configuration object. - {b See also}: {!mk_config} + + def_API('del_config', VOID, (_in(CONFIG),)) *) external del_config : config -> unit = "camlidl_z3V3_Z3_del_config" @@ -6198,6 +7137,8 @@ external del_config : config -> unit v} - {b See also}: {!mk_config} + + def_API('set_param_value', VOID, (_in(CONFIG), _in(STRING), _in(STRING))) *) external set_param_value : config -> string -> string -> unit = "camlidl_z3V3_Z3_set_param_value" @@ -6215,6 +7156,8 @@ external set_param_value : config -> string -> string -> unit + + def_API('mk_context', CONTEXT, (_in(CONFIG),)) *) external mk_context : config -> context = "camlidl_z3V3_Z3_mk_context" @@ -6223,6 +7166,8 @@ external mk_context : config -> context Summary: Delete the given logical context. - {b See also}: {!mk_context} + + def_API('del_context', VOID, (_in(CONTEXT),)) *) external del_context : context -> unit = "camlidl_z3V3_Z3_del_context" @@ -6241,6 +7186,8 @@ external del_context : context -> unit - {b See also}: {!mk_context } + + def_API('update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING))) *) external update_param_value : context -> string -> string -> unit = "camlidl_z3V3_Z3_update_param_value" @@ -6254,6 +7201,8 @@ external update_param_value : context -> string -> string -> unit - {b See also}: {!mk_context } + + def_API('get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING))) *) external get_param_value : context -> string -> string option = "camlidl_z3V3_Z3_get_param_value" @@ -6273,6 +7222,8 @@ external get_param_value : context -> string -> string option The legal range of unsigned int integers is 0 to 2^30-1. - {b See also}: {!mk_string_symbol} + + def_API('mk_int_symbol', SYMBOL, (_in(CONTEXT), _in(INT))) *) external mk_int_symbol : context -> int -> symbol = "camlidl_z3V3_Z3_mk_int_symbol" @@ -6283,6 +7234,8 @@ external mk_int_symbol : context -> int -> symbol Symbols are used to name several term and type constructors. - {b See also}: {!mk_int_symbol} + + def_API('mk_string_symbol', SYMBOL, (_in(CONTEXT), _in(STRING))) *) external mk_string_symbol : context -> string -> symbol = "camlidl_z3V3_Z3_mk_string_symbol" @@ -6297,6 +7250,8 @@ external mk_string_symbol : context -> string -> symbol Summary: Create a free (uninterpreted) type using the given name (symbol). Two free types are considered the same iff the have the same name. + + def_API('mk_uninterpreted_sort', SORT, (_in(CONTEXT), _in(SYMBOL))) *) external mk_uninterpreted_sort : context -> symbol -> sort = "camlidl_z3V3_Z3_mk_uninterpreted_sort" @@ -6305,6 +7260,8 @@ external mk_uninterpreted_sort : context -> symbol -> sort Summary: Create the Boolean type. This type is used to create propositional variables and predicates. + + def_API('mk_bool_sort', SORT, (_in(CONTEXT), )) *) external mk_bool_sort : context -> sort = "camlidl_z3V3_Z3_mk_bool_sort" @@ -6317,6 +7274,8 @@ external mk_bool_sort : context -> sort {!mk_bv_sort} creates a bit-vector type. - {b See also}: {!mk_bv_sort} + + def_API('mk_int_sort', SORT, (_in(CONTEXT), )) *) external mk_int_sort : context -> sort = "camlidl_z3V3_Z3_mk_int_sort" @@ -6326,6 +7285,8 @@ external mk_int_sort : context -> sort This type is not a floating point number. Z3 does not have support for floating point numbers yet. + + def_API('mk_real_sort', SORT, (_in(CONTEXT), )) *) external mk_real_sort : context -> sort = "camlidl_z3V3_Z3_mk_real_sort" @@ -6336,6 +7297,8 @@ external mk_real_sort : context -> sort This type can also be seen as a machine integer. - {b Remarks}: The size of the bitvector type must be greater than zero. + + def_API('mk_bv_sort', SORT, (_in(CONTEXT), _in(UINT))) *) external mk_bv_sort : context -> int -> sort = "camlidl_z3V3_Z3_mk_bv_sort" @@ -6348,6 +7311,8 @@ external mk_bv_sort : context -> int -> sort constant together with the sort returned by this call. - {b See also}: {!get_finite_domain_sort_size.} + + def_API('mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64))) *) external mk_finite_domain_sort : context -> symbol -> int64 -> sort = "camlidl_z3V3_Z3_mk_finite_domain_sort" @@ -6360,6 +7325,8 @@ external mk_finite_domain_sort : context -> symbol -> int64 -> sort - {b See also}: {!mk_select} - {b See also}: {!mk_store} + + def_API('mk_array_sort', SORT, (_in(CONTEXT), _in(SORT), _in(SORT))) *) external mk_array_sort : context -> sort -> sort -> sort = "camlidl_z3V3_Z3_mk_array_sort" @@ -6381,6 +7348,8 @@ external mk_array_sort : context -> sort -> sort -> sort @param field_sorts type of the tuple fields. @param mk_tuple_decl output parameter that will contain the constructor declaration. @param proj_decl output parameter that will contain the projection function declarations. This field must be a buffer of size [num_fields] allocated by the user. + + def_API('mk_tuple_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _out(FUNC_DECL), _out_array(2, FUNC_DECL))) *) external mk_tuple_sort : context -> symbol -> symbol array -> sort array -> sort * func_decl * func_decl array = "camlidl_z3V3_Z3_mk_tuple_sort" @@ -6408,6 +7377,8 @@ external mk_tuple_sort : context -> symbol -> symbol array -> sort array -> sort [enum_consts]. The array [enum_testers] has three predicates of type {e (s -> Bool) }. The first predicate (corresponding to A) is true when applied to A, and false otherwise. Similarly for the other predicates. + + def_API('mk_enumeration_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SYMBOL), _out_array(2, FUNC_DECL), _out_array(2, FUNC_DECL))) *) external mk_enumeration_sort : context -> symbol -> symbol array -> sort * func_decl array * func_decl array = "camlidl_z3V3_Z3_mk_enumeration_sort" @@ -6430,6 +7401,8 @@ external mk_enumeration_sort : context -> symbol -> symbol array -> sort * func_ @param is_cons_decl cons cell test. @param head_decl list head. @param tail_decl list tail. + + def_API('mk_list_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(SORT), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL))) *) external mk_list_sort : context -> symbol -> sort -> sort * func_decl * func_decl * func_decl * func_decl * func_decl * func_decl = "camlidl_z3V3_Z3_mk_list_sort" @@ -6448,6 +7421,8 @@ external mk_list_sort : context -> symbol -> sort -> sort * func_decl * func_dec sort reference is [None], then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. + + def_API('mk_constructor', CONSTRUCTOR, (_in(CONTEXT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(3, SYMBOL), _in_array(3, SORT), _in_array(3, UINT))) *) external mk_constructor : context -> symbol -> symbol -> symbol array -> sort array -> int array -> constructor = "camlidl_z3_Z3_mk_constructor_bytecode" "camlidl_z3V3_Z3_mk_constructor" @@ -6457,6 +7432,8 @@ external mk_constructor : context -> symbol -> symbol -> symbol array -> sort ar @param c logical context. @param constr constructor. + + def_API('del_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR))) *) external del_constructor : context -> constructor -> unit = "camlidl_z3V3_Z3_del_constructor" @@ -6469,6 +7446,8 @@ external del_constructor : context -> constructor -> unit @param name name of datatype. @param num_constructors number of constructors passed in. @param constructors array of constructor containers. + + def_API('mk_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _inout_array(2, CONSTRUCTOR))) *) external mk_datatype : context -> symbol -> constructor array -> sort * constructor array = "camlidl_z3V3_Z3_mk_datatype" @@ -6479,6 +7458,8 @@ external mk_datatype : context -> symbol -> constructor array -> sort * construc @param c logical context. @param num_constructors number of constructors in list. @param constructors list of constructors. + + def_API('mk_constructor_list', CONSTRUCTOR_LIST, (_in(CONTEXT), _in(UINT), _in_array(1, CONSTRUCTOR))) *) external mk_constructor_list : context -> constructor array -> constructor_list = "camlidl_z3V3_Z3_mk_constructor_list" @@ -6491,6 +7472,7 @@ external mk_constructor_list : context -> constructor array -> constructor_list @param c logical context. @param clist constructor list container. + def_API('del_constructor_list', VOID, (_in(CONTEXT), _in(CONSTRUCTOR_LIST))) *) external del_constructor_list : context -> constructor_list -> unit = "camlidl_z3V3_Z3_del_constructor_list" @@ -6503,6 +7485,8 @@ external del_constructor_list : context -> constructor_list -> unit @param sort_names names of datatype sorts. @param sorts array of datattype sorts. @param constructor_lists list of constructors, one list per sort. + + def_API('mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST))) *) external mk_datatypes : context -> symbol array -> constructor_list array -> sort array * constructor_list array = "camlidl_z3V3_Z3_mk_datatypes" @@ -6516,6 +7500,8 @@ external mk_datatypes : context -> symbol array -> constructor_list array -> sor @param constructor constructor function declaration. @param tester constructor test function declaration. @param accessors array of accessor function declarations. + + def_API('query_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR), _in(UINT), _out(FUNC_DECL), _out(FUNC_DECL), _out_array(2, FUNC_DECL))) *) external query_constructor : context -> constructor -> int -> func_decl * func_decl * func_decl array = "camlidl_z3V3_Z3_query_constructor" @@ -6540,6 +7526,8 @@ external query_constructor : context -> constructor -> int -> func_decl * func_d application. - {b See also}: {!mk_app} + + def_API('mk_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) *) external mk_func_decl : context -> symbol -> sort array -> sort -> func_decl = "camlidl_z3V3_Z3_mk_func_decl" @@ -6548,6 +7536,8 @@ external mk_func_decl : context -> symbol -> sort array -> sort -> func_decl Summary: Create a constant or function application. - {b See also}: {!mk_func_decl} + + def_API('mk_app', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST))) *) external mk_app : context -> func_decl -> ast array -> ast = "camlidl_z3V3_Z3_mk_app" @@ -6565,6 +7555,8 @@ external mk_app : context -> func_decl -> ast array -> ast - {b See also}: {!mk_func_decl} - {b See also}: {!mk_app} + + def_API('mk_const', AST, (_in(CONTEXT), _in(SYMBOL), _in(SORT))) *) external mk_const : context -> symbol -> sort -> ast = "camlidl_z3V3_Z3_mk_const" @@ -6578,6 +7570,8 @@ external mk_const : context -> symbol -> sort -> ast - {b See also}: {!mk_func_decl} + + def_API('mk_fresh_func_decl', FUNC_DECL, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SORT), _in(SORT))) *) external mk_fresh_func_decl : context -> string -> sort array -> sort -> func_decl = "camlidl_z3V3_Z3_mk_fresh_func_decl" @@ -6594,6 +7588,8 @@ external mk_fresh_func_decl : context -> string -> sort array -> sort -> func_de - {b See also}: {!mk_func_decl} - {b See also}: {!mk_app} + + def_API('mk_fresh_const', AST, (_in(CONTEXT), _in(STRING), _in(SORT))) *) external mk_fresh_const : context -> string -> sort -> ast = "camlidl_z3V3_Z3_mk_fresh_const" @@ -6603,12 +7599,16 @@ external mk_fresh_const : context -> string -> sort -> ast *) (** Summary: Create an AST node representing [true]. + + def_API('mk_true', AST, (_in(CONTEXT), )) *) external mk_true : context -> ast = "camlidl_z3V3_Z3_mk_true" (** Summary: Create an AST node representing [false]. + + def_API('mk_false', AST, (_in(CONTEXT), )) *) external mk_false : context -> ast = "camlidl_z3V3_Z3_mk_false" @@ -6618,6 +7618,8 @@ external mk_false : context -> ast Create an AST node representing {e l = r }. The nodes [l] and [r] must have the same type. + + def_API('mk_eq', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_eq : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_eq" @@ -6634,6 +7636,8 @@ external mk_eq : context -> ast -> ast -> ast All arguments must have the same sort. - {b Remarks}: The number of arguments of a distinct construct must be greater than one. + + def_API('mk_distinct', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_distinct : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_distinct" @@ -6643,6 +7647,8 @@ external mk_distinct : context -> ast array -> ast Create an AST node representing {e not(a) }. The node [a] must have Boolean sort. + + def_API('mk_not', AST, (_in(CONTEXT), _in(AST))) *) external mk_not : context -> ast -> ast = "camlidl_z3V3_Z3_mk_not" @@ -6654,6 +7660,8 @@ external mk_not : context -> ast -> ast The node [t1] must have Boolean sort, [t2] and [t3] must have the same sort. The sort of the new node is equal to the sort of [t2] and [t3]. + + def_API('mk_ite', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) *) external mk_ite : context -> ast -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_ite" @@ -6663,6 +7671,8 @@ external mk_ite : context -> ast -> ast -> ast -> ast Create an AST node representing {e t1 iff t2 }. The nodes [t1] and [t2] must have Boolean sort. + + def_API('mk_iff', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_iff : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_iff" @@ -6672,6 +7682,8 @@ external mk_iff : context -> ast -> ast -> ast Create an AST node representing {e t1 implies t2 }. The nodes [t1] and [t2] must have Boolean sort. + + def_API('mk_implies', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_implies : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_implies" @@ -6681,6 +7693,8 @@ external mk_implies : context -> ast -> ast -> ast Create an AST node representing {e t1 xor t2 }. The nodes [t1] and [t2] must have Boolean sort. + + def_API('mk_xor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_xor : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_xor" @@ -6693,6 +7707,8 @@ external mk_xor : context -> ast -> ast -> ast All arguments must have Boolean sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_and', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_and : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_and" @@ -6705,6 +7721,8 @@ external mk_and : context -> ast array -> ast All arguments must have Boolean sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_or', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_or : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_or" @@ -6720,6 +7738,8 @@ external mk_or : context -> ast array -> ast All arguments must have int or real sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_add', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_add : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_add" @@ -6733,6 +7753,8 @@ external mk_add : context -> ast array -> ast - {b Remarks}: Z3 has limited support for non-linear arithmetic. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_mul', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_mul : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_mul" @@ -6745,6 +7767,8 @@ external mk_mul : context -> ast array -> ast All arguments must have int or real sort. - {b Remarks}: The number of arguments must be greater than zero. + + def_API('mk_sub', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_sub : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_sub" @@ -6754,6 +7778,8 @@ external mk_sub : context -> ast array -> ast Summary: \[ [mk_unary_minus c arg] \] Create the term: {e - arg}. The arguments must have int or real type. + + def_API('mk_unary_minus', AST, (_in(CONTEXT), _in(AST))) *) external mk_unary_minus : context -> ast -> ast = "camlidl_z3V3_Z3_mk_unary_minus" @@ -6766,6 +7792,7 @@ external mk_unary_minus : context -> ast -> ast If the arguments have int type, then the result type is an int type, otherwise the the result type is real. + def_API('mk_div', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_div : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_div" @@ -6776,6 +7803,7 @@ external mk_div : context -> ast -> ast -> ast The arguments must have int type. + def_API('mk_mod', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_mod : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_mod" @@ -6786,6 +7814,7 @@ external mk_mod : context -> ast -> ast -> ast The arguments must have int type. + def_API('mk_rem', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_rem : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_rem" @@ -6794,6 +7823,8 @@ external mk_rem : context -> ast -> ast -> ast The arguments must have int or real type. + + def_API('mk_power', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_power : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_power" @@ -6803,6 +7834,8 @@ external mk_power : context -> ast -> ast -> ast Create less than. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_lt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_lt : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_lt" @@ -6812,6 +7845,8 @@ external mk_lt : context -> ast -> ast -> ast Create less than or equal to. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_le', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_le : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_le" @@ -6821,6 +7856,8 @@ external mk_le : context -> ast -> ast -> ast Create greater than. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_gt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_gt : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_gt" @@ -6830,6 +7867,8 @@ external mk_gt : context -> ast -> ast -> ast Create greater than or equal to. The nodes [t1] and [t2] must have the same sort, and must be int or real. + + def_API('mk_ge', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_ge : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_ge" @@ -6849,6 +7888,8 @@ external mk_ge : context -> ast -> ast -> ast - {b See also}: {!mk_real2int} - {b See also}: {!mk_is_int} + + def_API('mk_int2real', AST, (_in(CONTEXT), _in(AST))) *) external mk_int2real : context -> ast -> ast = "camlidl_z3V3_Z3_mk_int2real" @@ -6862,6 +7903,8 @@ external mk_int2real : context -> ast -> ast - {b See also}: {!mk_int2real} - {b See also}: {!mk_is_int} + + def_API('mk_real2int', AST, (_in(CONTEXT), _in(AST))) *) external mk_real2int : context -> ast -> ast = "camlidl_z3V3_Z3_mk_real2int" @@ -6872,6 +7915,8 @@ external mk_real2int : context -> ast -> ast - {b See also}: {!mk_int2real} - {b See also}: {!mk_real2int} + + def_API('mk_is_int', AST, (_in(CONTEXT), _in(AST))) *) external mk_is_int : context -> ast -> ast = "camlidl_z3V3_Z3_mk_is_int" @@ -6884,6 +7929,8 @@ external mk_is_int : context -> ast -> ast Bitwise negation. The node [t1] must have a bit-vector sort. + + def_API('mk_bvnot', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvnot : context -> ast -> ast = "camlidl_z3V3_Z3_mk_bvnot" @@ -6893,6 +7940,8 @@ external mk_bvnot : context -> ast -> ast Take conjunction of bits in vector, return vector of length 1. The node [t1] must have a bit-vector sort. + + def_API('mk_bvredand', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvredand : context -> ast -> ast = "camlidl_z3V3_Z3_mk_bvredand" @@ -6902,6 +7951,8 @@ external mk_bvredand : context -> ast -> ast Take disjunction of bits in vector, return vector of length 1. The node [t1] must have a bit-vector sort. + + def_API('mk_bvredor', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvredor : context -> ast -> ast = "camlidl_z3V3_Z3_mk_bvredor" @@ -6911,6 +7962,8 @@ external mk_bvredor : context -> ast -> ast Bitwise and. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvand', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvand : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvand" @@ -6920,6 +7973,8 @@ external mk_bvand : context -> ast -> ast -> ast Bitwise or. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvor : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvor" @@ -6929,6 +7984,8 @@ external mk_bvor : context -> ast -> ast -> ast Bitwise exclusive-or. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvxor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvxor : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvxor" @@ -6938,6 +7995,8 @@ external mk_bvxor : context -> ast -> ast -> ast Bitwise nand. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvnand', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvnand : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvnand" @@ -6947,6 +8006,8 @@ external mk_bvnand : context -> ast -> ast -> ast Bitwise nor. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvnor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvnor : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvnor" @@ -6956,6 +8017,8 @@ external mk_bvnor : context -> ast -> ast -> ast Bitwise xnor. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvxnor', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvxnor : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvxnor" @@ -6965,6 +8028,8 @@ external mk_bvxnor : context -> ast -> ast -> ast Standard two's complement unary minus. The node [t1] must have bit-vector sort. + + def_API('mk_bvneg', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvneg : context -> ast -> ast = "camlidl_z3V3_Z3_mk_bvneg" @@ -6974,6 +8039,8 @@ external mk_bvneg : context -> ast -> ast Standard two's complement addition. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvadd', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvadd : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvadd" @@ -6983,6 +8050,8 @@ external mk_bvadd : context -> ast -> ast -> ast Standard two's complement subtraction. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsub', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsub : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsub" @@ -6992,6 +8061,8 @@ external mk_bvsub : context -> ast -> ast -> ast Standard two's complement multiplication. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvmul', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvmul : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvmul" @@ -7005,6 +8076,8 @@ external mk_bvmul : context -> ast -> ast -> ast is undefined. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvudiv', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvudiv : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvudiv" @@ -7022,6 +8095,8 @@ external mk_bvudiv : context -> ast -> ast -> ast If {e t2 } is zero, then the result is undefined. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsdiv', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsdiv : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsdiv" @@ -7035,6 +8110,8 @@ external mk_bvsdiv : context -> ast -> ast -> ast If {e t2 } is zero, then the result is undefined. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvurem', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvurem : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvurem" @@ -7051,6 +8128,8 @@ external mk_bvurem : context -> ast -> ast -> ast The nodes [t1] and [t2] must have the same bit-vector sort. - {b See also}: {!mk_bvsmod} + + def_API('mk_bvsrem', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsrem : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsrem" @@ -7064,6 +8143,8 @@ external mk_bvsrem : context -> ast -> ast -> ast The nodes [t1] and [t2] must have the same bit-vector sort. - {b See also}: {!mk_bvsrem} + + def_API('mk_bvsmod', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsmod : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsmod" @@ -7073,6 +8154,8 @@ external mk_bvsmod : context -> ast -> ast -> ast Unsigned less than. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvult', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvult : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvult" @@ -7090,6 +8173,8 @@ external mk_bvult : context -> ast -> ast -> ast v} The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvslt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvslt : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvslt" @@ -7099,6 +8184,8 @@ external mk_bvslt : context -> ast -> ast -> ast Unsigned less than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvule', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvule : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvule" @@ -7108,6 +8195,8 @@ external mk_bvule : context -> ast -> ast -> ast Two's complement signed less than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsle', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsle : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsle" @@ -7117,6 +8206,8 @@ external mk_bvsle : context -> ast -> ast -> ast Unsigned greater than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvuge', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvuge : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvuge" @@ -7126,6 +8217,8 @@ external mk_bvuge : context -> ast -> ast -> ast Two's complement signed greater than or equal to. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsge', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsge : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsge" @@ -7135,6 +8228,8 @@ external mk_bvsge : context -> ast -> ast -> ast Unsigned greater than. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvugt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvugt : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvugt" @@ -7144,6 +8239,8 @@ external mk_bvugt : context -> ast -> ast -> ast Two's complement signed greater than. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsgt', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsgt : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsgt" @@ -7156,6 +8253,8 @@ external mk_bvsgt : context -> ast -> ast -> ast The result is a bit-vector of size {e n1+n2 }, where [n1] ([n2)] is the size of [t1] ([t2)]. + + def_API('mk_concat', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_concat : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_concat" @@ -7167,6 +8266,8 @@ external mk_concat : context -> ast -> ast -> ast high - low + 1 }. The node [t1] must have a bit-vector sort. + + def_API('mk_extract', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in(AST))) *) external mk_extract : context -> int -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_extract" @@ -7178,6 +8279,8 @@ external mk_extract : context -> int -> int -> ast -> ast bit-vector. The node [t1] must have a bit-vector sort. + + def_API('mk_sign_ext', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_sign_ext : context -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_sign_ext" @@ -7189,6 +8292,8 @@ external mk_sign_ext : context -> int -> ast -> ast given bit-vector. The node [t1] must have a bit-vector sort. + + def_API('mk_zero_ext', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_zero_ext : context -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_zero_ext" @@ -7198,6 +8303,8 @@ external mk_zero_ext : context -> int -> ast -> ast Repeat the given bit-vector up length {e i }. The node [t1] must have a bit-vector sort. + + def_API('mk_repeat', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_repeat : context -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_repeat" @@ -7214,6 +8321,8 @@ external mk_repeat : context -> int -> ast -> ast programming language or assembly architecture you are modeling. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvshl', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvshl : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvshl" @@ -7230,6 +8339,8 @@ external mk_bvshl : context -> ast -> ast -> ast programming language or assembly architecture you are modeling. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvlshr', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvlshr : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvlshr" @@ -7242,11 +8353,13 @@ external mk_bvlshr : context -> ast -> ast -> ast bits of the result always copy the most significant bit of the second argument. - NB. The semantics of shift operations varies between environments. This + The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvashr', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvashr : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvashr" @@ -7256,6 +8369,8 @@ external mk_bvashr : context -> ast -> ast -> ast Rotate bits of [t1] to the left [i] times. The node [t1] must have a bit-vector sort. + + def_API('mk_rotate_left', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_rotate_left : context -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_rotate_left" @@ -7265,6 +8380,8 @@ external mk_rotate_left : context -> int -> ast -> ast Rotate bits of [t1] to the right [i] times. The node [t1] must have a bit-vector sort. + + def_API('mk_rotate_right', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_rotate_right : context -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_rotate_right" @@ -7274,6 +8391,8 @@ external mk_rotate_right : context -> int -> ast -> ast Rotate bits of [t1] to the left [t2] times. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_ext_rotate_left', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_ext_rotate_left : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_ext_rotate_left" @@ -7283,6 +8402,8 @@ external mk_ext_rotate_left : context -> ast -> ast -> ast Rotate bits of [t1] to the right [t2] times. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_ext_rotate_right', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_ext_rotate_right : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_ext_rotate_right" @@ -7296,6 +8417,8 @@ external mk_ext_rotate_right : context -> ast -> ast -> ast when solving constraints with this function. The node [t1] must have integer sort. + + def_API('mk_int2bv', AST, (_in(CONTEXT), _in(UINT), _in(AST))) *) external mk_int2bv : context -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_int2bv" @@ -7308,11 +8431,13 @@ external mk_int2bv : context -> int -> ast -> ast and in the range {e [0..2^N-1] }, where N are the number of bits in [t1]. If [is_signed] is true, [t1] is treated as a signed bit-vector. - NB. This function is essentially treated as uninterpreted. + This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function. The node [t1] must have a bit-vector sort. + + def_API('mk_bv2int', AST, (_in(CONTEXT), _in(AST), _in(BOOL))) *) external mk_bv2int : context -> ast -> bool -> ast = "camlidl_z3V3_Z3_mk_bv2int" @@ -7323,6 +8448,8 @@ external mk_bv2int : context -> ast -> bool -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvadd_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL))) *) external mk_bvadd_no_overflow : context -> ast -> ast -> bool -> ast = "camlidl_z3V3_Z3_mk_bvadd_no_overflow" @@ -7333,6 +8460,8 @@ external mk_bvadd_no_overflow : context -> ast -> ast -> bool -> ast of [t1] and [t2] does not underflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvadd_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvadd_no_underflow : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvadd_no_underflow" @@ -7343,6 +8472,8 @@ external mk_bvadd_no_underflow : context -> ast -> ast -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsub_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsub_no_overflow : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsub_no_overflow" @@ -7353,6 +8484,8 @@ external mk_bvsub_no_overflow : context -> ast -> ast -> ast of [t1] and [t2] does not underflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsub_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL))) *) external mk_bvsub_no_underflow : context -> ast -> ast -> bool -> ast = "camlidl_z3V3_Z3_mk_bvsub_no_underflow" @@ -7363,6 +8496,8 @@ external mk_bvsub_no_underflow : context -> ast -> ast -> bool -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvsdiv_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvsdiv_no_overflow : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvsdiv_no_overflow" @@ -7373,6 +8508,8 @@ external mk_bvsdiv_no_overflow : context -> ast -> ast -> ast [t1] is interpreted as a signed bit-vector. The node [t1] must have bit-vector sort. + + def_API('mk_bvneg_no_overflow', AST, (_in(CONTEXT), _in(AST))) *) external mk_bvneg_no_overflow : context -> ast -> ast = "camlidl_z3V3_Z3_mk_bvneg_no_overflow" @@ -7383,6 +8520,8 @@ external mk_bvneg_no_overflow : context -> ast -> ast of [t1] and [t2] does not overflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvmul_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL))) *) external mk_bvmul_no_overflow : context -> ast -> ast -> bool -> ast = "camlidl_z3V3_Z3_mk_bvmul_no_overflow" @@ -7393,6 +8532,8 @@ external mk_bvmul_no_overflow : context -> ast -> ast -> bool -> ast of [t1] and [t2] does not underflow. The nodes [t1] and [t2] must have the same bit-vector sort. + + def_API('mk_bvmul_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_bvmul_no_underflow : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_bvmul_no_underflow" @@ -7411,6 +8552,8 @@ external mk_bvmul_no_underflow : context -> ast -> ast -> ast - {b See also}: {!mk_array_sort} - {b See also}: {!mk_store} + + def_API('mk_select', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_select : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_select" @@ -7429,6 +8572,8 @@ external mk_select : context -> ast -> ast -> ast - {b See also}: {!mk_array_sort} - {b See also}: {!mk_select} + + def_API('mk_store', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) *) external mk_store : context -> ast -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_store" @@ -7442,6 +8587,8 @@ external mk_store : context -> ast -> ast -> ast -> ast @param c logical context. @param domain domain sort for the array. @param v value that the array maps to. + + def_API('mk_const_array', AST, (_in(CONTEXT), _in(SORT), _in(AST))) *) external mk_const_array : context -> sort -> ast -> ast = "camlidl_z3V3_Z3_mk_const_array" @@ -7457,6 +8604,8 @@ external mk_const_array : context -> sort -> ast -> ast - {b See also}: {!mk_array_sort} - {b See also}: {!mk_store} - {b See also}: {!mk_select} + + def_API('mk_map', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST))) *) external mk_map : context -> func_decl -> int -> ast -> ast = "camlidl_z3V3_Z3_mk_map" @@ -7469,6 +8618,7 @@ external mk_map : context -> func_decl -> int -> ast -> ast @param c logical context. @param array array value whose default range value is accessed. + def_API('mk_array_default', AST, (_in(CONTEXT), _in(AST))) *) external mk_array_default : context -> ast -> ast = "camlidl_z3V3_Z3_mk_array_default" @@ -7478,18 +8628,24 @@ external mk_array_default : context -> ast -> ast *) (** Summary: Create Set type. + + def_API('mk_set_sort', SORT, (_in(CONTEXT), _in(SORT))) *) external mk_set_sort : context -> sort -> sort = "camlidl_z3V3_Z3_mk_set_sort" (** Summary: Create the empty set. + + def_API('mk_empty_set', AST, (_in(CONTEXT), _in(SORT))) *) external mk_empty_set : context -> sort -> ast = "camlidl_z3V3_Z3_mk_empty_set" (** Summary: Create the full set. + + def_API('mk_full_set', AST, (_in(CONTEXT), _in(SORT))) *) external mk_full_set : context -> sort -> ast = "camlidl_z3V3_Z3_mk_full_set" @@ -7498,6 +8654,8 @@ external mk_full_set : context -> sort -> ast Summary: Add an element to a set. The first argument must be a set, the second an element. + + def_API('mk_set_add', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_add : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_set_add" @@ -7506,30 +8664,40 @@ external mk_set_add : context -> ast -> ast -> ast Summary: Remove an element to a set. The first argument must be a set, the second an element. + + def_API('mk_set_del', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_del : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_set_del" (** Summary: Take the union of a list of sets. + + def_API('mk_set_union', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_set_union : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_set_union" (** Summary: Take the intersection of a list of sets. + + def_API('mk_set_intersect', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_set_intersect : context -> ast array -> ast = "camlidl_z3V3_Z3_mk_set_intersect" (** Summary: Take the set difference between two sets. + + def_API('mk_set_difference', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_difference : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_set_difference" (** Summary: Take the complement of a set. + + def_API('mk_set_complement', AST, (_in(CONTEXT), _in(AST))) *) external mk_set_complement : context -> ast -> ast = "camlidl_z3V3_Z3_mk_set_complement" @@ -7538,12 +8706,16 @@ external mk_set_complement : context -> ast -> ast Summary: Check for set membership. The first argument should be an element type of the set. + + def_API('mk_set_member', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_member : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_set_member" (** Summary: Check for subsetness of sets. + + def_API('mk_set_subset', AST, (_in(CONTEXT), _in(AST), _in(AST))) *) external mk_set_subset : context -> ast -> ast -> ast = "camlidl_z3V3_Z3_mk_set_subset" @@ -7563,6 +8735,8 @@ external mk_set_subset : context -> ast -> ast -> ast - {b See also}: {!mk_int} + + def_API('mk_numeral', AST, (_in(CONTEXT), _in(STRING), _in(SORT))) *) external mk_numeral : context -> string -> sort -> ast = "camlidl_z3V3_Z3_mk_numeral" @@ -7579,6 +8753,8 @@ external mk_numeral : context -> string -> sort -> ast - {b See also}: {!mk_numeral} - {b See also}: {!mk_int} + + def_API('mk_real', AST, (_in(CONTEXT), _in(INT), _in(INT))) *) external mk_real : context -> int -> int -> ast = "camlidl_z3V3_Z3_mk_real" @@ -7590,6 +8766,8 @@ external mk_real : context -> int -> int -> ast It is slightly faster than {!mk_numeral} since it is not necessary to parse a string. - {b See also}: {!mk_numeral} + + def_API('mk_int', AST, (_in(CONTEXT), _in(INT), _in(SORT))) *) external mk_int : context -> int -> sort -> ast = "camlidl_z3V3_Z3_mk_int" @@ -7601,6 +8779,8 @@ external mk_int : context -> int -> sort -> ast It is slightly faster than {!mk_numeral} since it is not necessary to parse a string. - {b See also}: {!mk_numeral} + + def_API('mk_int64', AST, (_in(CONTEXT), _in(INT64), _in(SORT))) *) external mk_int64 : context -> int64 -> sort -> ast = "camlidl_z3V3_Z3_mk_int64" @@ -7623,9 +8803,10 @@ external mk_int64 : context -> int64 -> sort -> ast In general, one can pass in a list of (multi-)patterns in the quantifier constructor. - - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_pattern', PATTERN, (_in(CONTEXT), _in(UINT), _in_array(1, AST))) *) external mk_pattern : context -> ast array -> pattern = "camlidl_z3V3_Z3_mk_pattern" @@ -7656,6 +8837,8 @@ external mk_pattern : context -> ast array -> pattern - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_bound', AST, (_in(CONTEXT), _in(UINT), _in(SORT))) *) external mk_bound : context -> int -> sort -> ast = "camlidl_z3V3_Z3_mk_bound" @@ -7690,6 +8873,8 @@ external mk_bound : context -> int -> sort -> ast - {b See also}: {!mk_pattern} - {b See also}: {!mk_bound} - {b See also}: {!mk_exists} + + def_API('mk_forall', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, PATTERN), _in(UINT), _in_array(4, SORT), _in_array(4, SYMBOL), _in(AST))) *) external mk_forall : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_forall_bytecode" "camlidl_z3V3_Z3_mk_forall" @@ -7701,6 +8886,8 @@ external mk_forall : context -> int -> pattern array -> sort array -> symbol arr - {b See also}: {!mk_bound} - {b See also}: {!mk_forall} - {b See also}: {!mk_quantifier} + + def_API('mk_exists', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, PATTERN), _in(UINT), _in_array(4, SORT), _in_array(4, SYMBOL), _in(AST))) *) external mk_exists : context -> int -> pattern array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_exists_bytecode" "camlidl_z3V3_Z3_mk_exists" @@ -7723,6 +8910,8 @@ external mk_exists : context -> int -> pattern array -> sort array -> symbol arr - {b See also}: {!mk_bound} - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_quantifier', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(UINT), _in_array(3, PATTERN), _in(UINT), _in_array(5, SORT), _in_array(5, SYMBOL), _in(AST))) *) external mk_quantifier : context -> bool -> int -> pattern array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_bytecode" "camlidl_z3V3_Z3_mk_quantifier" @@ -7748,6 +8937,8 @@ external mk_quantifier : context -> bool -> int -> pattern array -> sort array - - {b See also}: {!mk_bound} - {b See also}: {!mk_forall} - {b See also}: {!mk_exists} + + def_API('mk_quantifier_ex', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(5, PATTERN), _in(UINT), _in_array(7, AST), _in(UINT), _in_array(9, SORT), _in_array(9, SYMBOL), _in(AST))) *) external mk_quantifier_ex : context -> bool -> int -> symbol -> symbol -> pattern array -> ast array -> sort array -> symbol array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_ex_bytecode" "camlidl_z3V3_Z3_mk_quantifier_ex" @@ -7768,6 +8959,7 @@ external mk_quantifier_ex : context -> bool -> int -> symbol -> symbol -> patter - {b See also}: {!mk_pattern} - {b See also}: {!mk_exists_const} + def_API('mk_forall_const', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, APP), _in(UINT), _in_array(4, PATTERN), _in(AST))) *) external mk_forall_const : context -> int -> app array -> pattern array -> ast -> ast = "camlidl_z3V3_Z3_mk_forall_const" @@ -7789,6 +8981,8 @@ external mk_forall_const : context -> int -> app array -> pattern array -> ast - - {b See also}: {!mk_pattern} - {b See also}: {!mk_forall_const} + + def_API('mk_exists_const', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, APP), _in(UINT), _in_array(4, PATTERN), _in(AST))) *) external mk_exists_const : context -> int -> app array -> pattern array -> ast -> ast = "camlidl_z3V3_Z3_mk_exists_const" @@ -7797,6 +8991,8 @@ external mk_exists_const : context -> int -> app array -> pattern array -> ast - Summary: Create a universal or existential quantifier using a list of constants that will form the set of bound variables. + + def_API('mk_quantifier_const', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(UINT), _in_array(3, APP), _in(UINT), _in_array(5, PATTERN), _in(AST))) *) external mk_quantifier_const : context -> bool -> int -> app array -> pattern array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_const_bytecode" "camlidl_z3V3_Z3_mk_quantifier_const" @@ -7805,6 +9001,8 @@ external mk_quantifier_const : context -> bool -> int -> app array -> pattern ar Summary: Create a universal or existential quantifier using a list of constants that will form the set of bound variables. + + def_API('mk_quantifier_const_ex', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(5, APP), _in(UINT), _in_array(7, PATTERN), _in(UINT), _in_array(9, AST), _in(AST))) *) external mk_quantifier_const_ex : context -> bool -> int -> symbol -> symbol -> app array -> pattern array -> ast array -> ast -> ast = "camlidl_z3_Z3_mk_quantifier_const_ex_bytecode" "camlidl_z3V3_Z3_mk_quantifier_const_ex" @@ -7822,6 +9020,8 @@ external mk_quantifier_const_ex : context -> bool -> int -> symbol -> symbol -> Summary: Return [INT_SYMBOL] if the symbol was constructed using {!mk_int_symbol}, and [STRING_SYMBOL] if the symbol was constructed using {!mk_string_symbol}. + + def_API('get_symbol_kind', UINT, (_in(CONTEXT), _in(SYMBOL))) *) external get_symbol_kind : context -> symbol -> symbol_kind = "camlidl_z3V3_Z3_get_symbol_kind" @@ -7833,6 +9033,8 @@ external get_symbol_kind : context -> symbol -> symbol_kind - {b Precondition}: get_symbol_kind s == INT_SYMBOL - {b See also}: {!mk_int_symbol} + + def_API('get_symbol_int', INT, (_in(CONTEXT), _in(SYMBOL))) *) external get_symbol_int : context -> symbol -> int = "camlidl_z3V3_Z3_get_symbol_int" @@ -7848,6 +9050,8 @@ external get_symbol_int : context -> symbol -> int - {b See also}: {!mk_string_symbol} + + def_API('get_symbol_string', STRING, (_in(CONTEXT), _in(SYMBOL))) *) external get_symbol_string : context -> symbol -> string = "camlidl_z3V3_Z3_get_symbol_string" @@ -7857,6 +9061,8 @@ external get_symbol_string : context -> symbol -> string *) (** Summary: Return the sort name as a symbol. + + def_API('get_sort_name', SYMBOL, (_in(CONTEXT), _in(SORT))) *) external get_sort_name : context -> sort -> symbol = "camlidl_z3V3_Z3_get_sort_name" @@ -7864,6 +9070,8 @@ external get_sort_name : context -> sort -> symbol (** Summary: Return a unique identifier for [s]. - {b Remarks}: Implicitly used by [Pervasives.( = )] and [Pervasives.compare]. + + def_API('get_sort_id', UINT, (_in(CONTEXT), _in(SORT))) *) external get_sort_id : context -> sort -> int = "camlidl_z3V3_Z3_get_sort_id" @@ -7874,6 +9082,8 @@ external get_sort_id : context -> sort -> int (** Summary: Convert a [sort] into [ast]. - {b Remarks}: [sort_to_ast c s] can be replaced by [(s :> ast)]. + + def_API('sort_to_ast', AST, (_in(CONTEXT), _in(SORT))) *) external sort_to_ast : context -> sort -> ast = "camlidl_z3V3_Z3_sort_to_ast" @@ -7881,6 +9091,8 @@ external sort_to_ast : context -> sort -> ast (** Summary: compare sorts. - {b Remarks}: [Pervasives.( = )] or [Pervasives.compare] can also be used. + + def_API('is_eq_sort', BOOL, (_in(CONTEXT), _in(SORT), _in(SORT))) *) external is_eq_sort : context -> sort -> sort -> bool = "camlidl_z3V3_Z3_is_eq_sort" @@ -7889,6 +9101,8 @@ external is_eq_sort : context -> sort -> sort -> bool Summary: Return the sort kind (e.g., array, tuple, int, bool, etc). - {b See also}: {!sort_kind} + + def_API('get_sort_kind', UINT, (_in(CONTEXT), _in(SORT))) *) external get_sort_kind : context -> sort -> sort_kind = "camlidl_z3V3_Z3_get_sort_kind" @@ -7901,6 +9115,8 @@ external get_sort_kind : context -> sort -> sort_kind - {b See also}: {!mk_bv_sort} - {b See also}: {!get_sort_kind} + + def_API('get_bv_sort_size', UINT, (_in(CONTEXT), _in(SORT))) *) external get_bv_sort_size : context -> sort -> int = "camlidl_z3V3_Z3_get_bv_sort_size" @@ -7909,6 +9125,8 @@ external get_bv_sort_size : context -> sort -> int Summary: Return the size of the sort in [r]. Return [None] if the call failed. That is, get_sort_kind(s) == FINITE_DOMAIN_SORT + + def_API('get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64))) *) external get_finite_domain_sort_size : context -> sort -> int64 option = "camlidl_z3V3_Z3_get_finite_domain_sort_size" @@ -7921,6 +9139,8 @@ external get_finite_domain_sort_size : context -> sort -> int64 option - {b See also}: {!mk_array_sort} - {b See also}: {!get_sort_kind} + + def_API('get_array_sort_domain', SORT, (_in(CONTEXT), _in(SORT))) *) external get_array_sort_domain : context -> sort -> sort = "camlidl_z3V3_Z3_get_array_sort_domain" @@ -7933,6 +9153,8 @@ external get_array_sort_domain : context -> sort -> sort - {b See also}: {!mk_array_sort} - {b See also}: {!get_sort_kind} + + def_API('get_array_sort_range', SORT, (_in(CONTEXT), _in(SORT))) *) external get_array_sort_range : context -> sort -> sort = "camlidl_z3V3_Z3_get_array_sort_range" @@ -7946,6 +9168,8 @@ external get_array_sort_range : context -> sort -> sort - {b See also}: {!mk_tuple_sort} - {b See also}: {!get_sort_kind} + + def_API('get_tuple_sort_mk_decl', FUNC_DECL, (_in(CONTEXT), _in(SORT))) *) external get_tuple_sort_mk_decl : context -> sort -> func_decl = "camlidl_z3V3_Z3_get_tuple_sort_mk_decl" @@ -7958,6 +9182,8 @@ external get_tuple_sort_mk_decl : context -> sort -> func_decl - {b See also}: {!mk_tuple_sort} - {b See also}: {!get_sort_kind} + + def_API('get_tuple_sort_num_fields', UINT, (_in(CONTEXT), _in(SORT))) *) external get_tuple_sort_num_fields : context -> sort -> int = "camlidl_z3V3_Z3_get_tuple_sort_num_fields" @@ -7972,6 +9198,8 @@ external get_tuple_sort_num_fields : context -> sort -> int - {b See also}: {!mk_tuple_sort} - {b See also}: {!get_sort_kind} + + def_API('get_tuple_sort_field_decl', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_tuple_sort_field_decl : context -> sort -> int -> func_decl = "camlidl_z3V3_Z3_get_tuple_sort_field_decl" @@ -7985,6 +9213,7 @@ external get_tuple_sort_field_decl : context -> sort -> int -> func_decl - {b See also}: {!get_datatype_sort_recognizer} - {b See also}: {!get_datatype_sort_constructor_accessor} + def_API('get_datatype_sort_num_constructors', UINT, (_in(CONTEXT), _in(SORT))) *) external get_datatype_sort_num_constructors : context -> sort -> int = "camlidl_z3V3_Z3_get_datatype_sort_num_constructors" @@ -7999,6 +9228,7 @@ external get_datatype_sort_num_constructors : context -> sort -> int - {b See also}: {!get_datatype_sort_recognizer} - {b See also}: {!get_datatype_sort_constructor_accessor} + def_API('get_datatype_sort_constructor', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_datatype_sort_constructor : context -> sort -> int -> func_decl = "camlidl_z3V3_Z3_get_datatype_sort_constructor" @@ -8013,6 +9243,7 @@ external get_datatype_sort_constructor : context -> sort -> int -> func_decl - {b See also}: {!get_datatype_sort_constructor} - {b See also}: {!get_datatype_sort_constructor_accessor} + def_API('get_datatype_sort_recognizer', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_datatype_sort_recognizer : context -> sort -> int -> func_decl = "camlidl_z3V3_Z3_get_datatype_sort_recognizer" @@ -8027,6 +9258,8 @@ external get_datatype_sort_recognizer : context -> sort -> int -> func_decl - {b See also}: {!get_datatype_sort_num_constructors} - {b See also}: {!get_datatype_sort_constructor} - {b See also}: {!get_datatype_sort_recognizer} + + def_API('get_datatype_sort_constructor_accessor', FUNC_DECL, (_in(CONTEXT), _in(SORT), _in(UINT), _in(UINT))) *) external get_datatype_sort_constructor_accessor : context -> sort -> int -> int -> func_decl = "camlidl_z3V3_Z3_get_datatype_sort_constructor_accessor" @@ -8037,6 +9270,8 @@ external get_datatype_sort_constructor_accessor : context -> sort -> int -> int - {b Precondition}: get_sort_kind s == RELATION_SORT - {b See also}: {!get_relation_column} + + def_API('get_relation_arity', UINT, (_in(CONTEXT), _in(SORT))) *) external get_relation_arity : context -> sort -> int = "camlidl_z3V3_Z3_get_relation_arity" @@ -8048,6 +9283,8 @@ external get_relation_arity : context -> sort -> int - {b Precondition}: col < get_relation_arity c s - {b See also}: {!get_relation_arity} + + def_API('get_relation_column', SORT, (_in(CONTEXT), _in(SORT), _in(UINT))) *) external get_relation_column : context -> sort -> int -> sort = "camlidl_z3V3_Z3_get_relation_column" @@ -8058,6 +9295,8 @@ external get_relation_column : context -> sort -> int -> sort (** Summary: Convert a [func_decl] into [ast]. - {b Remarks}: [func_decl_to_ast c f] can be replaced by [(f :> ast)]. + + def_API('func_decl_to_ast', AST, (_in(CONTEXT), _in(FUNC_DECL))) *) external func_decl_to_ast : context -> func_decl -> ast = "camlidl_z3V3_Z3_func_decl_to_ast" @@ -8065,6 +9304,8 @@ external func_decl_to_ast : context -> func_decl -> ast (** Summary: compare terms. - {b Remarks}: [Pervasives.( = )] or [Pervasives.compare] can also be used. + + def_API('is_eq_func_decl', BOOL, (_in(CONTEXT), _in(FUNC_DECL), _in(FUNC_DECL))) *) external is_eq_func_decl : context -> func_decl -> func_decl -> bool = "camlidl_z3V3_Z3_is_eq_func_decl" @@ -8072,18 +9313,24 @@ external is_eq_func_decl : context -> func_decl -> func_decl -> bool (** Summary: Return a unique identifier for [f]. - {b Remarks}: Implicitly used by [Pervasives.( = )] and [Pervasives.compare]. + + def_API('get_func_decl_id', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_func_decl_id : context -> func_decl -> int = "camlidl_z3V3_Z3_get_func_decl_id" (** Summary: Return the constant declaration name as a symbol. + + def_API('get_decl_name', SYMBOL, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_decl_name : context -> func_decl -> symbol = "camlidl_z3V3_Z3_get_decl_name" (** Summary: Return declaration kind corresponding to declaration. + + def_API('get_decl_kind', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_decl_kind : context -> func_decl -> decl_kind = "camlidl_z3V3_Z3_get_decl_kind" @@ -8092,6 +9339,8 @@ external get_decl_kind : context -> func_decl -> decl_kind Summary: Return the number of parameters of the given declaration. - {b See also}: {!get_arity} + + def_API('get_domain_size', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_domain_size : context -> func_decl -> int = "camlidl_z3V3_Z3_get_domain_size" @@ -8100,6 +9349,8 @@ external get_domain_size : context -> func_decl -> int Summary: Alias for [get_domain_size]. - {b See also}: {!get_domain_size} + + def_API('get_arity', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_arity : context -> func_decl -> int = "camlidl_z3V3_Z3_get_arity" @@ -8111,6 +9362,8 @@ external get_arity : context -> func_decl -> int - {b Precondition}: i < get_domain_size d - {b See also}: {!get_domain_size} + + def_API('get_domain', SORT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_domain : context -> func_decl -> int -> sort = "camlidl_z3V3_Z3_get_domain" @@ -8121,12 +9374,16 @@ external get_domain : context -> func_decl -> int -> sort If [d] is a constant (i.e., has zero arguments), then this function returns the sort of the constant. + + def_API('get_range', SORT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_range : context -> func_decl -> sort = "camlidl_z3V3_Z3_get_range" (** Summary: Return the number of parameters associated with a declaration. + + def_API('get_decl_num_parameters', UINT, (_in(CONTEXT), _in(FUNC_DECL))) *) external get_decl_num_parameters : context -> func_decl -> int = "camlidl_z3V3_Z3_get_decl_num_parameters" @@ -8137,6 +9394,8 @@ external get_decl_num_parameters : context -> func_decl -> int @param c the context @param d the function declaration @param idx is the index of the named parameter it should be between 0 and the number of parameters. + + def_API('get_decl_parameter_kind', UINT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_parameter_kind : context -> func_decl -> int -> parameter_kind = "camlidl_z3V3_Z3_get_decl_parameter_kind" @@ -8145,6 +9404,8 @@ external get_decl_parameter_kind : context -> func_decl -> int -> parameter_kind Summary: Return the integer value associated with an integer parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_INT + + def_API('get_decl_int_parameter', INT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_int_parameter : context -> func_decl -> int -> int = "camlidl_z3V3_Z3_get_decl_int_parameter" @@ -8153,6 +9414,8 @@ external get_decl_int_parameter : context -> func_decl -> int -> int Summary: Return the double value associated with an double parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_DOUBLE + + def_API('get_decl_double_parameter', DOUBLE, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_double_parameter : context -> func_decl -> int -> float = "camlidl_z3V3_Z3_get_decl_double_parameter" @@ -8161,6 +9424,8 @@ external get_decl_double_parameter : context -> func_decl -> int -> float Summary: Return the double value associated with an double parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_SYMBOL + + def_API('get_decl_symbol_parameter', SYMBOL, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_symbol_parameter : context -> func_decl -> int -> symbol = "camlidl_z3V3_Z3_get_decl_symbol_parameter" @@ -8169,6 +9434,8 @@ external get_decl_symbol_parameter : context -> func_decl -> int -> symbol Summary: Return the sort value associated with a sort parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_SORT + + def_API('get_decl_sort_parameter', SORT, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_sort_parameter : context -> func_decl -> int -> sort = "camlidl_z3V3_Z3_get_decl_sort_parameter" @@ -8177,6 +9444,8 @@ external get_decl_sort_parameter : context -> func_decl -> int -> sort Summary: Return the expresson value associated with an expression parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_AST + + def_API('get_decl_ast_parameter', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_ast_parameter : context -> func_decl -> int -> ast = "camlidl_z3V3_Z3_get_decl_ast_parameter" @@ -8185,6 +9454,8 @@ external get_decl_ast_parameter : context -> func_decl -> int -> ast Summary: Return the expresson value associated with an expression parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_FUNC_DECL + + def_API('get_decl_func_decl_parameter', FUNC_DECL, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_func_decl_parameter : context -> func_decl -> int -> func_decl = "camlidl_z3V3_Z3_get_decl_func_decl_parameter" @@ -8193,6 +9464,8 @@ external get_decl_func_decl_parameter : context -> func_decl -> int -> func_decl Summary: Return the rational value, as a string, associated with a rational parameter. - {b Precondition}: get_decl_parameter_kind c d idx == PARAMETER_RATIONAL + + def_API('get_decl_rational_parameter', STRING, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT))) *) external get_decl_rational_parameter : context -> func_decl -> int -> string = "camlidl_z3V3_Z3_get_decl_rational_parameter" @@ -8203,12 +9476,16 @@ external get_decl_rational_parameter : context -> func_decl -> int -> string (** Summary: Convert a [app] into [ast]. - {b Remarks}: [app_to_ast c a] can be replaced by [(a :> ast)]. + + def_API('app_to_ast', AST, (_in(CONTEXT), _in(APP))) *) external app_to_ast : context -> app -> ast = "camlidl_z3V3_Z3_app_to_ast" (** Summary: Return the declaration of a constant or function application. + + def_API('get_app_decl', FUNC_DECL, (_in(CONTEXT), _in(APP))) *) external get_app_decl : context -> app -> func_decl = "camlidl_z3V3_Z3_get_app_decl" @@ -8217,6 +9494,8 @@ external get_app_decl : context -> app -> func_decl Summary: \[ [ get_app_num_args c a ] \] Return the number of argument of an application. If [t] is an constant, then the number of arguments is 0. + + def_API('get_app_num_args', UINT, (_in(CONTEXT), _in(APP))) *) external get_app_num_args : context -> app -> int = "camlidl_z3V3_Z3_get_app_num_args" @@ -8226,6 +9505,8 @@ external get_app_num_args : context -> app -> int Return the i-th argument of the given application. - {b Precondition}: i < get_num_args c a + + def_API('get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT))) *) external get_app_arg : context -> app -> int -> ast = "camlidl_z3V3_Z3_get_app_arg" @@ -8236,6 +9517,8 @@ external get_app_arg : context -> app -> int -> ast (** Summary: compare terms. - {b Remarks}: [Pervasives.( = )] or [Pervasives.compare] can also be used. + + def_API('is_eq_ast', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) *) external is_eq_ast : context -> ast -> ast -> bool = "camlidl_z3V3_Z3_is_eq_ast" @@ -8243,6 +9526,8 @@ external is_eq_ast : context -> ast -> ast -> bool (** Summary: Return a unique identifier for [t]. - {b Remarks}: Implicitly used by [Pervasives.compare] for values of type [ast], [app], [sort], [func_decl], and [pattern]. + + def_API('get_ast_id', UINT, (_in(CONTEXT), _in(AST))) *) external get_ast_id : context -> ast -> int = "camlidl_z3V3_Z3_get_ast_id" @@ -8250,6 +9535,8 @@ external get_ast_id : context -> ast -> int (** Summary: Return a hash code for the given AST. - {b Remarks}: Implicitly used by [Hashtbl.hash] for values of type [ast], [app], [sort], [func_decl], and [pattern]. + + def_API('get_ast_hash', UINT, (_in(CONTEXT), _in(AST))) *) external get_ast_hash : context -> ast -> int = "camlidl_z3V3_Z3_get_ast_hash" @@ -8258,37 +9545,52 @@ external get_ast_hash : context -> ast -> int Summary: Return the sort of an AST node. The AST node must be a constant, application, numeral, bound variable, or quantifier. - + + def_API('get_sort', SORT, (_in(CONTEXT), _in(AST))) *) external get_sort : context -> ast -> sort = "camlidl_z3V3_Z3_get_sort" (** Summary: Return true if the given expression [t] is well sorted. + + def_API('is_well_sorted', BOOL, (_in(CONTEXT), _in(AST))) *) external is_well_sorted : context -> ast -> bool = "camlidl_z3V3_Z3_is_well_sorted" (** Summary: Return L_TRUE if [a] is true, L_FALSE if it is false, and L_UNDEF otherwise. + + def_API('get_bool_value', UINT, (_in(CONTEXT), _in(AST))) *) external get_bool_value : context -> ast -> lbool = "camlidl_z3V3_Z3_get_bool_value" (** Summary: Return the kind of the given AST. + + def_API('get_ast_kind', UINT, (_in(CONTEXT), _in(AST))) *) external get_ast_kind : context -> ast -> ast_kind = "camlidl_z3V3_Z3_get_ast_kind" +(** + def_API('is_app', BOOL, (_in(CONTEXT), _in(AST))) +*) external is_app : context -> ast -> bool = "camlidl_z3V3_Z3_is_app" +(** + def_API('is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST))) +*) external is_numeral_ast : context -> ast -> bool = "camlidl_z3V3_Z3_is_numeral_ast" (** Summary: Return true if the give AST is a real algebraic number. + + def_API('is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST))) *) external is_algebraic_number : context -> ast -> bool = "camlidl_z3V3_Z3_is_algebraic_number" @@ -8297,6 +9599,8 @@ external is_algebraic_number : context -> ast -> bool Summary: Convert an [ast] into an [APP_AST]. - {b Precondition}: {v get_ast_kind c a == [APP_AST] v} + + def_API('to_app', APP, (_in(CONTEXT), _in(AST))) *) external to_app : context -> ast -> app = "camlidl_z3V3_Z3_to_app" @@ -8305,6 +9609,8 @@ external to_app : context -> ast -> app Summary: Convert an AST into a FUNC_DECL_AST. This is just type casting. - {b Precondition}: {v get_ast_kind c a == FUNC_DECL_AST v} + + def_API('to_func_decl', FUNC_DECL, (_in(CONTEXT), _in(AST))) *) external to_func_decl : context -> ast -> func_decl = "camlidl_z3V3_Z3_to_func_decl" @@ -8319,6 +9625,8 @@ external to_func_decl : context -> ast -> func_decl Summary: Return numeral value, as a string of a numeric constant term - {b Precondition}: get_ast_kind c a == NUMERAL_AST + + def_API('get_numeral_string', STRING, (_in(CONTEXT), _in(AST))) *) external get_numeral_string : context -> ast -> string = "camlidl_z3V3_Z3_get_numeral_string" @@ -8328,6 +9636,8 @@ external get_numeral_string : context -> ast -> string The result has at most [precision] decimal places. - {b Precondition}: get_ast_kind c a == NUMERAL_AST || is_algebraic_number c a + + def_API('get_numeral_decimal_string', STRING, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_numeral_decimal_string : context -> ast -> int -> string = "camlidl_z3V3_Z3_get_numeral_decimal_string" @@ -8336,6 +9646,8 @@ external get_numeral_decimal_string : context -> ast -> int -> string Summary: Return the numerator (as a numeral AST) of a numeral AST of sort Real. - {b Precondition}: get_ast_kind c a == NUMERAL_AST + + def_API('get_numerator', AST, (_in(CONTEXT), _in(AST))) *) external get_numerator : context -> ast -> ast = "camlidl_z3V3_Z3_get_numerator" @@ -8344,6 +9656,8 @@ external get_numerator : context -> ast -> ast Summary: Return the denominator (as a numeral AST) of a numeral AST of sort Real. - {b Precondition}: get_ast_kind c a == NUMERAL_AST + + def_API('get_denominator', AST, (_in(CONTEXT), _in(AST))) *) external get_denominator : context -> ast -> ast = "camlidl_z3V3_Z3_get_denominator" @@ -8359,6 +9673,8 @@ external get_denominator : context -> ast -> ast Return [TRUE] if the numeral value fits in 64 bit numerals, [FALSE] otherwise. - {b Precondition}: get_ast_kind a == NUMERAL_AST + + def_API('get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64))) *) external get_numeral_small : context -> ast -> bool * int64 * int64 = "camlidl_z3V3_Z3_get_numeral_small" @@ -8371,6 +9687,8 @@ external get_numeral_small : context -> ast -> bool * int64 * int64 - {b Precondition}: get_ast_kind c v == NUMERAL_AST - {b See also}: {!get_numeral_string} + + def_API('get_numeral_int', BOOL, (_in(CONTEXT), _in(AST), _out(INT))) *) external get_numeral_int : context -> ast -> bool * int = "camlidl_z3V3_Z3_get_numeral_int" @@ -8383,6 +9701,8 @@ external get_numeral_int : context -> ast -> bool * int - {b Precondition}: get_ast_kind c v == NUMERAL_AST - {b See also}: {!get_numeral_string} + + def_API('get_numeral_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) *) external get_numeral_int64 : context -> ast -> bool * int64 = "camlidl_z3V3_Z3_get_numeral_int64" @@ -8395,6 +9715,8 @@ external get_numeral_int64 : context -> ast -> bool * int64 - {b Precondition}: get_ast_kind c v == NUMERAL_AST - {b See also}: {!get_numeral_string} + + def_API('get_numeral_rational_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64))) *) external get_numeral_rational_int64 : context -> ast -> bool * int64 * int64 = "camlidl_z3V3_Z3_get_numeral_rational_int64" @@ -8405,6 +9727,8 @@ external get_numeral_rational_int64 : context -> ast -> bool * int64 * int64 The result is a numeral AST of sort Real. - {b Precondition}: is_algebraic_number c a + + def_API('get_algebraic_number_lower', AST, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_algebraic_number_lower : context -> ast -> int -> ast = "camlidl_z3V3_Z3_get_algebraic_number_lower" @@ -8415,6 +9739,8 @@ external get_algebraic_number_lower : context -> ast -> int -> ast The result is a numeral AST of sort Real. - {b Precondition}: is_algebraic_number c a + + def_API('get_algebraic_number_upper', AST, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_algebraic_number_upper : context -> ast -> int -> ast = "camlidl_z3V3_Z3_get_algebraic_number_upper" @@ -8425,18 +9751,24 @@ external get_algebraic_number_upper : context -> ast -> int -> ast (** Summary: Convert a pattern into ast. - {b Remarks}: [pattern_to_ast c p] can be replaced by [(p :> ast)]. + + def_API('pattern_to_ast', AST, (_in(CONTEXT), _in(PATTERN))) *) external pattern_to_ast : context -> pattern -> ast = "camlidl_z3V3_Z3_pattern_to_ast" (** Summary: Return number of terms in pattern. + + def_API('get_pattern_num_terms', UINT, (_in(CONTEXT), _in(PATTERN))) *) external get_pattern_num_terms : context -> pattern -> int = "camlidl_z3V3_Z3_get_pattern_num_terms" (** Summary: Return i'th ast in pattern. + + def_API('get_pattern', AST, (_in(CONTEXT), _in(PATTERN), _in(UINT))) *) external get_pattern : context -> pattern -> int -> ast = "camlidl_z3V3_Z3_get_pattern" @@ -8448,6 +9780,8 @@ external get_pattern : context -> pattern -> int -> ast Summary: Return index of de-Brujin bound variable. - {b Precondition}: get_ast_kind a == VAR_AST + + def_API('get_index_value', UINT, (_in(CONTEXT), _in(AST))) *) external get_index_value : context -> ast -> int = "camlidl_z3V3_Z3_get_index_value" @@ -8456,6 +9790,8 @@ external get_index_value : context -> ast -> int Summary: Determine if quantifier is universal. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('is_quantifier_forall', BOOL, (_in(CONTEXT), _in(AST))) *) external is_quantifier_forall : context -> ast -> bool = "camlidl_z3V3_Z3_is_quantifier_forall" @@ -8464,6 +9800,8 @@ external is_quantifier_forall : context -> ast -> bool Summary: Obtain weight of quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_weight', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_weight : context -> ast -> int = "camlidl_z3V3_Z3_get_quantifier_weight" @@ -8472,6 +9810,8 @@ external get_quantifier_weight : context -> ast -> int Summary: Return number of patterns used in quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_num_patterns', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_num_patterns : context -> ast -> int = "camlidl_z3V3_Z3_get_quantifier_num_patterns" @@ -8480,6 +9820,8 @@ external get_quantifier_num_patterns : context -> ast -> int Summary: Return i'th pattern. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_pattern_ast', PATTERN, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_pattern_ast : context -> ast -> int -> pattern = "camlidl_z3V3_Z3_get_quantifier_pattern_ast" @@ -8488,6 +9830,8 @@ external get_quantifier_pattern_ast : context -> ast -> int -> pattern Summary: Return number of no_patterns used in quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_num_no_patterns', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_num_no_patterns : context -> ast -> int = "camlidl_z3V3_Z3_get_quantifier_num_no_patterns" @@ -8496,6 +9840,8 @@ external get_quantifier_num_no_patterns : context -> ast -> int Summary: Return i'th no_pattern. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_no_pattern_ast', AST, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_no_pattern_ast : context -> ast -> int -> ast = "camlidl_z3V3_Z3_get_quantifier_no_pattern_ast" @@ -8504,6 +9850,8 @@ external get_quantifier_no_pattern_ast : context -> ast -> int -> ast Summary: Return number of bound variables of quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_num_bound', UINT, (_in(CONTEXT), _in(AST))) *) external get_quantifier_num_bound : context -> ast -> int = "camlidl_z3V3_Z3_get_quantifier_num_bound" @@ -8512,6 +9860,8 @@ external get_quantifier_num_bound : context -> ast -> int Summary: Return symbol of the i'th bound variable. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_bound_name', SYMBOL, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_bound_name : context -> ast -> int -> symbol = "camlidl_z3V3_Z3_get_quantifier_bound_name" @@ -8520,6 +9870,8 @@ external get_quantifier_bound_name : context -> ast -> int -> symbol Summary: Return sort of the i'th bound variable. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_bound_sort', SORT, (_in(CONTEXT), _in(AST), _in(UINT))) *) external get_quantifier_bound_sort : context -> ast -> int -> sort = "camlidl_z3V3_Z3_get_quantifier_bound_sort" @@ -8528,6 +9880,8 @@ external get_quantifier_bound_sort : context -> ast -> int -> sort Summary: Return body of quantifier. - {b Precondition}: get_ast_kind a == QUANTIFIER_AST + + def_API('get_quantifier_body', AST, (_in(CONTEXT), _in(AST))) *) external get_quantifier_body : context -> ast -> ast = "camlidl_z3V3_Z3_get_quantifier_body" @@ -8539,6 +9893,8 @@ external get_quantifier_body : context -> ast -> ast Summary: Interface to simplifier. Provides an interface to the AST simplifier used by Z3. + + def_API('simplify', AST, (_in(CONTEXT), _in(AST))) *) external simplify : context -> ast -> ast = "camlidl_z3V3_Z3_simplify" @@ -8551,6 +9907,8 @@ external simplify : context -> ast -> ast The number of arguments [num_args] should coincide with the number of arguments to [a]. If [a] is a quantifier, then num_args has to be 1. + + def_API('update_term', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST))) *) external update_term : context -> ast -> ast array -> ast = "camlidl_z3V3_Z3_update_term" @@ -8559,6 +9917,8 @@ external update_term : context -> ast -> ast array -> ast Summary: Substitute every occurrence of {e from[i] } in [a] with {e to[i] }, for [i] smaller than [num_exprs]. The result is the new AST. The arrays [from] and [to] must have size [num_exprs]. For every [i] smaller than [num_exprs], we must have that sort of {e from[i] } must be equal to sort of {e to[i] }. + + def_API('substitute', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST), _in_array(2, AST))) *) external substitute : context -> ast -> ast array -> ast array -> ast = "camlidl_z3V3_Z3_substitute" @@ -8566,6 +9926,8 @@ external substitute : context -> ast -> ast array -> ast array -> ast (** Summary: Substitute the free variables in [a] with the expressions in [to]. For every [i] smaller than [num_exprs], the variable with de-Bruijn index [i] is replaced with term {e to[i] }. + + def_API('substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST))) *) external substitute_vars : context -> ast -> ast array -> ast = "camlidl_z3V3_Z3_substitute_vars" @@ -8575,6 +9937,8 @@ external substitute_vars : context -> ast -> ast array -> ast *) (** Summary: Log interaction to a file. + + extra_API('open_log', INT, (_in(STRING),)) *) external open_log : string -> bool = "camlidl_z3V3_Z3_open_log" @@ -8585,12 +9949,16 @@ external open_log : string -> bool The interaction log is opened using open_log. It contains the formulas that are checked using Z3. You can use this command to append comments, for instance. + + extra_API('append_log', VOID, (_in(STRING),)) *) external append_log : string -> unit = "camlidl_z3V3_Z3_append_log" (** Summary: Close interaction log. + + extra_API('close_log', VOID, ()) *) external close_log : unit -> unit = "camlidl_z3V3_Z3_close_log" @@ -8600,6 +9968,8 @@ external close_log : unit -> unit Warnings are printed after passing [true], warning messages are suppressed after calling this method with [false]. + + def_API('toggle_warning_messages', VOID, (_in(BOOL),)) *) external toggle_warning_messages : bool -> unit = "camlidl_z3V3_Z3_toggle_warning_messages" @@ -8622,6 +9992,7 @@ external toggle_warning_messages : bool -> unit - {b See also}: {!pattern_to_string} - {b See also}: {!func_decl_to_string} + def_API('set_ast_print_mode', VOID, (_in(CONTEXT), _in(PRINT_MODE))) *) external set_ast_print_mode : context -> ast_print_mode -> unit = "camlidl_z3V3_Z3_set_ast_print_mode" @@ -8634,16 +10005,27 @@ external set_ast_print_mode : context -> ast_print_mode -> unit - {b See also}: {!pattern_to_string} - {b See also}: {!sort_to_string} + + def_API('ast_to_string', STRING, (_in(CONTEXT), _in(AST))) *) external ast_to_string : context -> ast -> string = "camlidl_z3V3_Z3_ast_to_string" +(** + def_API('pattern_to_string', STRING, (_in(CONTEXT), _in(PATTERN))) +*) external pattern_to_string : context -> pattern -> string = "camlidl_z3V3_Z3_pattern_to_string" +(** + def_API('sort_to_string', STRING, (_in(CONTEXT), _in(SORT))) +*) external sort_to_string : context -> sort -> string = "camlidl_z3V3_Z3_sort_to_string" +(** + def_API('func_decl_to_string', STRING, (_in(CONTEXT), _in(FUNC_DECL))) +*) external func_decl_to_string : context -> func_decl -> string = "camlidl_z3V3_Z3_func_decl_to_string" @@ -8653,6 +10035,8 @@ external func_decl_to_string : context -> func_decl -> string + + def_API('model_to_string', STRING, (_in(CONTEXT), _in(MODEL))) *) external model_to_string : context -> model -> string = "camlidl_z3V3_Z3_model_to_string" @@ -8672,6 +10056,8 @@ external model_to_string : context -> model -> string @param num_assumptions - number of assumptions. @param assumptions - auxiliary assumptions. @param formula - formula to be checked for consistency in conjunction with assumptions. + + def_API('benchmark_to_smtlib_string', STRING, (_in(CONTEXT), _in(STRING), _in(STRING), _in(STRING), _in(STRING), _in(UINT), _in_array(5, AST), _in(AST))) *) external benchmark_to_smtlib_string : context -> string -> string -> string -> string -> ast array -> ast -> string = "camlidl_z3_Z3_benchmark_to_smtlib_string_bytecode" "camlidl_z3V3_Z3_benchmark_to_smtlib_string" @@ -8685,12 +10071,16 @@ external benchmark_to_smtlib_string : context -> string -> string -> string -> s It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string. + + def_API('parse_smtlib2_string', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib2_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast = "camlidl_z3_Z3_parse_smtlib2_string_bytecode" "camlidl_z3V3_Z3_parse_smtlib2_string" (** Summary: Similar to {!parse_smtlib2_string}, but reads the benchmark from a file. + + def_API('parse_smtlib2_file', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib2_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast = "camlidl_z3_Z3_parse_smtlib2_file_bytecode" "camlidl_z3V3_Z3_parse_smtlib2_file" @@ -8710,18 +10100,24 @@ external parse_smtlib2_file : context -> string -> symbol array -> sort array -> The formulas, assumptions and declarations defined in [str] can be extracted using the functions: {!get_smtlib_num_formulas}, {!get_smtlib_formula}, {!get_smtlib_num_assumptions}, {!get_smtlib_assumption}, {!get_smtlib_num_decls}, and {!get_smtlib_decl}. + + def_API('parse_smtlib_string', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit = "camlidl_z3_Z3_parse_smtlib_string_bytecode" "camlidl_z3V3_Z3_parse_smtlib_string" (** Summary: Similar to {!parse_smtlib_string}, but reads the benchmark from a file. + + def_API('parse_smtlib_file', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) *) external parse_smtlib_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit = "camlidl_z3_Z3_parse_smtlib_file_bytecode" "camlidl_z3V3_Z3_parse_smtlib_file" (** Summary: Return the number of SMTLIB formulas parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_formulas', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_formulas : context -> int = "camlidl_z3V3_Z3_get_smtlib_num_formulas" @@ -8731,12 +10127,16 @@ external get_smtlib_num_formulas : context -> int Return the i-th formula parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_formulas c + + def_API('get_smtlib_formula', AST, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_formula : context -> int -> ast = "camlidl_z3V3_Z3_get_smtlib_formula" (** Summary: Return the number of SMTLIB assumptions parsed by {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_assumptions', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_assumptions : context -> int = "camlidl_z3V3_Z3_get_smtlib_num_assumptions" @@ -8746,12 +10146,16 @@ external get_smtlib_num_assumptions : context -> int Return the i-th assumption parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_assumptions c + + def_API('get_smtlib_assumption', AST, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_assumption : context -> int -> ast = "camlidl_z3V3_Z3_get_smtlib_assumption" (** Summary: Return the number of declarations parsed by {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_decls', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_decls : context -> int = "camlidl_z3V3_Z3_get_smtlib_num_decls" @@ -8761,12 +10165,16 @@ external get_smtlib_num_decls : context -> int Return the i-th declaration parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_decls c + + def_API('get_smtlib_decl', FUNC_DECL, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_decl : context -> int -> func_decl = "camlidl_z3V3_Z3_get_smtlib_decl" (** Summary: Return the number of sorts parsed by {!parse_smtlib_string} or {!parse_smtlib_file}. + + def_API('get_smtlib_num_sorts', UINT, (_in(CONTEXT), )) *) external get_smtlib_num_sorts : context -> int = "camlidl_z3V3_Z3_get_smtlib_num_sorts" @@ -8776,6 +10184,8 @@ external get_smtlib_num_sorts : context -> int Return the i-th sort parsed by the last call to {!parse_smtlib_string} or {!parse_smtlib_file}. - {b Precondition}: i < get_smtlib_num_sorts c + + def_API('get_smtlib_sort', SORT, (_in(CONTEXT), _in(UINT))) *) external get_smtlib_sort : context -> int -> sort = "camlidl_z3V3_Z3_get_smtlib_sort" @@ -8783,6 +10193,8 @@ external get_smtlib_sort : context -> int -> sort (** Summary: \[ [ get_smtlib_error c ] \] Retrieve that last error message information generated from parsing. + + def_API('get_smtlib_error', STRING, (_in(CONTEXT), )) *) external get_smtlib_error : context -> string = "camlidl_z3V3_Z3_get_smtlib_error" @@ -8792,12 +10204,16 @@ external get_smtlib_error : context -> string Parse the given string using the Z3 native parser. Return the conjunction of asserts made in the input. + + def_API('parse_z3_string', AST, (_in(CONTEXT), _in(STRING))) *) external parse_z3_string : context -> string -> ast = "camlidl_z3_Z3_parse_z3V3_string" (** Summary: Similar to {!parse_z3_string}, but reads the benchmark from a file. + + def_API('parse_z3_file', AST, (_in(CONTEXT), _in(STRING))) *) external parse_z3_file : context -> string -> ast = "camlidl_z3_Z3_parse_z3V3_file" @@ -8807,6 +10223,8 @@ external parse_z3_file : context -> string -> ast *) (** Summary: Return Z3 version number information. + + def_API('get_version', VOID, (_out(UINT), _out(UINT), _out(UINT), _out(UINT))) *) external get_version : unit -> int * int * int * int = "camlidl_z3V3_Z3_get_version" @@ -8818,6 +10236,8 @@ external get_version : unit -> int * int * int * int It allows discharging the previous state and resuming afresh. Any pointers previously returned by the API become invalid. + + def_API('reset_memory', VOID, ()) *) external reset_memory : unit -> unit = "camlidl_z3V3_Z3_reset_memory" @@ -8980,6 +10400,8 @@ external theory_get_app : theory -> int -> ast @deprecated This method just asserts a (universally quantified) formula that asserts that the new function is injective. It is compatible with the old interface for solving: {!assert_cnstr}, {!check_assumptions}, etc. + + def_API('mk_injective_function', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) *) external mk_injective_function : context -> symbol -> sort array -> sort -> func_decl = "camlidl_z3V3_Z3_mk_injective_function" @@ -8994,6 +10416,8 @@ external mk_injective_function : context -> symbol -> sort array -> sort -> func Return [TRUE] if the logic was changed successfully, and [FALSE] otherwise. @deprecated Subsumed by {!mk_solver_for_logic} + + def_API('set_logic', VOID, (_in(CONTEXT), _in(STRING))) *) external set_logic : context -> string -> bool = "camlidl_z3V3_Z3_set_logic" @@ -9008,6 +10432,8 @@ external set_logic : context -> string -> bool - {b See also}: {!pop} @deprecated Subsumed by {!solver_push} + + def_API('push', VOID, (_in(CONTEXT),)) *) external push : context -> unit = "camlidl_z3V3_Z3_push" @@ -9024,6 +10450,8 @@ external push : context -> unit - {b See also}: {!push} @deprecated Subsumed by {!solver_pop} + + def_API('pop', VOID, (_in(CONTEXT), _in(UINT))) *) external pop : context -> int -> unit = "camlidl_z3V3_Z3_pop" @@ -9037,6 +10465,8 @@ external pop : context -> int -> unit - {b See also}: {!pop} @deprecated Subsumed by {!solver_get_num_scopes}. + + def_API('get_num_scopes', UINT, (_in(CONTEXT),)) *) external get_num_scopes : context -> int = "camlidl_z3V3_Z3_get_num_scopes" @@ -9059,6 +10489,8 @@ external get_num_scopes : context -> int @deprecated This function has no effect. + + def_API('persist_ast', VOID, (_in(CONTEXT), _in(AST), _in(UINT))) *) external persist_ast : context -> ast -> int -> unit = "camlidl_z3V3_Z3_persist_ast" @@ -9076,6 +10508,8 @@ external persist_ast : context -> ast -> int -> unit - {b See also}: {!check_and_get_model} @deprecated Subsumed by {!solver_assert} + + def_API('assert_cnstr', VOID, (_in(CONTEXT), _in(AST))) *) external assert_cnstr : context -> ast -> unit = "camlidl_z3V3_Z3_assert_cnstr" @@ -9100,6 +10534,8 @@ external assert_cnstr : context -> ast -> unit @deprecated Subsumed by {!solver_check} + + def_API('check_and_get_model', INT, (_in(CONTEXT), _out(MODEL))) *) external check_and_get_model : context -> lbool * model = "camlidl_z3V3_Z3_check_and_get_model" @@ -9112,6 +10548,8 @@ external check_and_get_model : context -> lbool * model - {b See also}: {!check_and_get_model} @deprecated Subsumed by {!solver_check} + + def_API('check', INT, (_in(CONTEXT),)) *) external check : context -> lbool = "camlidl_z3V3_Z3_check" @@ -9151,6 +10589,8 @@ external check : context -> lbool @deprecated Subsumed by {!solver_check_assumptions} + + def_API('check_assumptions', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out(MODEL), _out(AST), _out(UINT), _out_array2(1, 5, AST))) *) external check_assumptions : context -> ast array -> int -> ast array -> lbool * model * ast * int * ast array = "camlidl_z3V3_Z3_check_assumptions" @@ -9175,6 +10615,8 @@ external check_assumptions : context -> ast array -> int -> ast array -> lbool * - {b See also}: {!check} @deprecated Subsumed by solver API + + def_API('get_implied_equalities', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out_array(1, UINT))) *) external get_implied_equalities : context -> ast array -> lbool * int array = "camlidl_z3V3_Z3_get_implied_equalities" @@ -9185,6 +10627,8 @@ external get_implied_equalities : context -> ast array -> lbool * int array - {b See also}: {!check_and_get_model} @deprecated Subsumed by solver API + + def_API('del_model', VOID, (_in(CONTEXT), _in(MODEL))) *) external del_model : context -> model -> unit = "camlidl_z3V3_Z3_del_model" @@ -9200,6 +10644,8 @@ external del_model : context -> model -> unit than the one performing the check. @deprecated Use {!interrupt} instead. + + def_API('soft_check_cancel', VOID, (_in(CONTEXT), )) *) external soft_check_cancel : context -> unit = "camlidl_z3V3_Z3_soft_check_cancel" @@ -9211,6 +10657,8 @@ external soft_check_cancel : context -> unit use this facility to determine the more detailed cause of search failure. @deprecated Subsumed by {!solver_get_reason_unknown} + + def_API('get_search_failure', UINT, (_in(CONTEXT), )) *) external get_search_failure : context -> search_failure = "camlidl_z3V3_Z3_get_search_failure" @@ -9233,6 +10681,8 @@ external get_search_failure : context -> search_failure @deprecated Labels are only supported by the old Solver API. This feature is not essential (it can be simulated using auxiliary Boolean variables). It is only available for backward compatibility. + + def_API('mk_label', AST, (_in(CONTEXT), _in(SYMBOL), _in(BOOL), _in(AST))) *) external mk_label : context -> symbol -> bool -> ast -> ast = "camlidl_z3V3_Z3_mk_label" @@ -9247,6 +10697,8 @@ external mk_label : context -> symbol -> bool -> ast -> ast - {b See also}: {!get_literal} @deprecated This procedure is based on the old Solver API. + + def_API('get_relevant_labels', LITERALS, (_in(CONTEXT), )) *) external get_relevant_labels : context -> literals = "camlidl_z3V3_Z3_get_relevant_labels" @@ -9260,6 +10712,8 @@ external get_relevant_labels : context -> literals - {b See also}: {!get_literal} @deprecated This procedure is based on the old Solver API. + + def_API('get_relevant_literals', LITERALS, (_in(CONTEXT), )) *) external get_relevant_literals : context -> literals = "camlidl_z3V3_Z3_get_relevant_literals" @@ -9274,6 +10728,8 @@ external get_relevant_literals : context -> literals - {b See also}: {!get_literal} @deprecated This procedure is based on the old Solver API. + + def_API('get_guessed_literals', LITERALS, (_in(CONTEXT), )) *) external get_guessed_literals : context -> literals = "camlidl_z3V3_Z3_get_guessed_literals" @@ -9284,6 +10740,8 @@ external get_guessed_literals : context -> literals - {b See also}: {!get_relevant_labels} @deprecated This procedure is based on the old Solver API. + + def_API('del_literals', VOID, (_in(CONTEXT), _in(LITERALS))) *) external del_literals : context -> literals -> unit = "camlidl_z3V3_Z3_del_literals" @@ -9294,6 +10752,8 @@ external del_literals : context -> literals -> unit - {b See also}: {!get_relevant_labels} @deprecated This procedure is based on the old Solver API. + + def_API('get_num_literals', UINT, (_in(CONTEXT), _in(LITERALS))) *) external get_num_literals : context -> literals -> int = "camlidl_z3V3_Z3_get_num_literals" @@ -9302,6 +10762,8 @@ external get_num_literals : context -> literals -> int Summary: Retrieve label symbol at idx. @deprecated This procedure is based on the old Solver API. + + def_API('get_label_symbol', SYMBOL, (_in(CONTEXT), _in(LITERALS), _in(UINT))) *) external get_label_symbol : context -> literals -> int -> symbol = "camlidl_z3V3_Z3_get_label_symbol" @@ -9310,6 +10772,8 @@ external get_label_symbol : context -> literals -> int -> symbol Summary: Retrieve literal expression at idx. @deprecated This procedure is based on the old Solver API. + + def_API('get_literal', AST, (_in(CONTEXT), _in(LITERALS), _in(UINT))) *) external get_literal : context -> literals -> int -> ast = "camlidl_z3V3_Z3_get_literal" @@ -9322,6 +10786,8 @@ external get_literal : context -> literals -> int -> ast - {b See also}: {!block_literals} @deprecated This procedure is based on the old Solver API. + + def_API('disable_literal', VOID, (_in(CONTEXT), _in(LITERALS), _in(UINT))) *) external disable_literal : context -> literals -> int -> unit = "camlidl_z3V3_Z3_disable_literal" @@ -9330,6 +10796,8 @@ external disable_literal : context -> literals -> int -> unit Summary: Block subsequent checks using the remaining enabled labels. @deprecated This procedure is based on the old Solver API. + + def_API('block_literals', VOID, (_in(CONTEXT), _in(LITERALS))) *) external block_literals : context -> literals -> unit = "camlidl_z3V3_Z3_block_literals" @@ -9345,6 +10813,8 @@ external block_literals : context -> literals -> unit - {b See also}: {!get_model_constant} @deprecated use {!model_get_num_consts} + + def_API('get_model_num_constants', UINT, (_in(CONTEXT), _in(MODEL))) *) external get_model_num_constants : context -> model -> int = "camlidl_z3V3_Z3_get_model_num_constants" @@ -9358,6 +10828,8 @@ external get_model_num_constants : context -> model -> int - {b Precondition}: i < get_model_num_constants c m @deprecated use {!model_get_const_decl} + + def_API('get_model_constant', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT))) *) external get_model_constant : context -> model -> int -> func_decl = "camlidl_z3V3_Z3_get_model_constant" @@ -9369,6 +10841,8 @@ external get_model_constant : context -> model -> int -> func_decl Each entry in the finite map represents the value of a function given a set of arguments. @deprecated use {!model_get_num_funcs} + + def_API('get_model_num_funcs', UINT, (_in(CONTEXT), _in(MODEL))) *) external get_model_num_funcs : context -> model -> int = "camlidl_z3V3_Z3_get_model_num_funcs" @@ -9382,6 +10856,8 @@ external get_model_num_funcs : context -> model -> int - {b See also}: {!get_model_num_funcs} @deprecated use {!model_get_func_decl} + + def_API('get_model_func_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT))) *) external get_model_func_decl : context -> model -> int -> func_decl = "camlidl_z3V3_Z3_get_model_func_decl" @@ -9391,6 +10867,8 @@ external get_model_func_decl : context -> model -> int -> func_decl in the given model. @deprecated Consider using {!model_eval} or {!model_get_func_interp} + + def_API('eval_func_decl', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _out(AST))) *) external eval_func_decl : context -> model -> func_decl -> bool * ast = "camlidl_z3V3_Z3_eval_func_decl" @@ -9407,6 +10885,8 @@ external eval_func_decl : context -> model -> func_decl -> bool * ast Return the number of entries mapping to non-default values of the array. @deprecated Use {!is_as_array} + + def_API('is_array_value', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _out(UINT))) *) external is_array_value : context -> model -> ast -> bool * int = "camlidl_z3V3_Z3_is_array_value" @@ -9419,6 +10899,8 @@ external is_array_value : context -> model -> ast -> bool * int - {b Precondition}: TRUE == is_array_value c v &num_entries @deprecated Use func_interp objects and {!get_as_array_func_decl} + + def_API('get_array_value', VOID, (_in(CONTEXT), _in(MODEL), _in(AST), _in(UINT), _out_array(3, AST), _out_array(3, AST), _out (AST))) *) external get_array_value : context -> model -> ast -> ast array -> ast array -> ast array * ast array * ast = "camlidl_z3V3_Z3_get_array_value" @@ -9439,6 +10921,8 @@ external get_array_value : context -> model -> ast -> ast array -> ast array -> - {b See also}: {!get_model_func_entry_arg} @deprecated Use func_interp objects + + def_API('get_model_func_else', AST, (_in(CONTEXT), _in(MODEL), _in(UINT))) *) external get_model_func_else : context -> model -> int -> ast = "camlidl_z3V3_Z3_get_model_func_else" @@ -9459,6 +10943,8 @@ external get_model_func_else : context -> model -> int -> ast - {b See also}: {!get_model_func_entry_arg} @deprecated Use func_interp objects + + def_API('get_model_func_num_entries', UINT, (_in(CONTEXT), _in(MODEL), _in(UINT))) *) external get_model_func_num_entries : context -> model -> int -> int = "camlidl_z3V3_Z3_get_model_func_num_entries" @@ -9484,6 +10970,8 @@ external get_model_func_num_entries : context -> model -> int -> int - {b See also}: {!get_model_func_entry_arg} @deprecated Use func_interp objects + + def_API('get_model_func_entry_num_args', UINT, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT))) *) external get_model_func_entry_num_args : context -> model -> int -> int -> int = "camlidl_z3V3_Z3_get_model_func_entry_num_args" @@ -9510,6 +10998,8 @@ external get_model_func_entry_num_args : context -> model -> int -> int -> int - {b See also}: {!get_model_func_entry_num_args} @deprecated Use func_interp objects + + def_API('get_model_func_entry_arg', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT), _in(UINT))) *) external get_model_func_entry_arg : context -> model -> int -> int -> int -> ast = "camlidl_z3V3_Z3_get_model_func_entry_arg" @@ -9534,6 +11024,8 @@ external get_model_func_entry_arg : context -> model -> int -> int -> int -> ast - {b See also}: {!get_model_func_num_entries } @deprecated Use func_interp objects + + def_API('get_model_func_entry_value', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT))) *) external get_model_func_entry_value : context -> model -> int -> int -> ast = "camlidl_z3V3_Z3_get_model_func_entry_value" @@ -9554,6 +11046,8 @@ external get_model_func_entry_value : context -> model -> int -> int -> ast - [t] is type incorrect. @deprecated Use {!model_eval} + + def_API('eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _out(AST))) *) external eval : context -> model -> ast -> bool * ast = "camlidl_z3V3_Z3_eval" @@ -9565,6 +11059,8 @@ external eval : context -> model -> ast -> bool * ast without going over terms. @deprecated Consider using {!model_eval} and {!substitute_vars} + + def_API('eval_decl', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(UINT), _in_array(3, AST), _out(AST))) *) external eval_decl : context -> model -> func_decl -> ast array -> bool * ast = "camlidl_z3V3_Z3_eval_decl" @@ -9584,6 +11080,8 @@ external eval_decl : context -> model -> func_decl -> ast array -> bool * ast @deprecated This method is obsolete. It just displays the internal representation of the global solver available for backward compatibility reasons. + + def_API('context_to_string', STRING, (_in(CONTEXT),)) *) external context_to_string : context -> string = "camlidl_z3V3_Z3_context_to_string" @@ -9600,6 +11098,8 @@ external context_to_string : context -> string @deprecated This method is based on the old solver API. Use {!stats_to_string} when using the new solver API. + + def_API('statistics_to_string', STRING, (_in(CONTEXT),)) *) external statistics_to_string : context -> string = "camlidl_z3V3_Z3_statistics_to_string" @@ -9614,6 +11114,8 @@ external statistics_to_string : context -> string if there has been a call to {!check} or {!check_and_get_model}. @deprecated This method is based on the old solver API. + + def_API('get_context_assignment', AST, (_in(CONTEXT),)) *) external get_context_assignment : context -> ast = "camlidl_z3V3_Z3_get_context_assignment" diff --git a/ml/z3_stubs.c b/ml/z3_stubs.c index dd21f7e79..0f32cb20e 100644 --- a/ml/z3_stubs.c +++ b/ml/z3_stubs.c @@ -416,7 +416,7 @@ value _v1; return _v1; } -int camlidl_transl_table_z3_enum_6[151] = { +int camlidl_transl_table_z3_enum_6[152] = { Z3_OP_TRUE, Z3_OP_FALSE, Z3_OP_EQ, @@ -548,6 +548,7 @@ int camlidl_transl_table_z3_enum_6[151] = { Z3_OP_PR_SKOLEMIZE, Z3_OP_PR_MODUS_PONENS_OEQ, Z3_OP_PR_TH_LEMMA, + Z3_OP_PR_HYPER_RESOLVE, Z3_OP_RA_STORE, Z3_OP_RA_EMPTY, Z3_OP_RA_IS_EMPTY, @@ -578,7 +579,7 @@ void camlidl_ml2c_z3_Z3_decl_kind(value _v1, Z3_decl_kind * _c2, camlidl_ctx _ct value camlidl_c2ml_z3_Z3_decl_kind(Z3_decl_kind * _c2, camlidl_ctx _ctx) { value _v1; - _v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_6, 151, "typedef Z3_decl_kind: bad enum value"); + _v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_6, 152, "typedef Z3_decl_kind: bad enum value"); return _v1; } @@ -1063,6 +1064,28 @@ check_error_code(c); return _vres; } +value camlidl_z3_Z3_param_descrs_to_string( + value _v_c, + value _v_p) +{ + Z3_context c; /*in*/ + Z3_param_descrs p; /*in*/ + Z3_string _res; + value _vres; + + struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL }; + camlidl_ctx _ctx = &_ctxs; + camlidl_ml2c_z3_Z3_context(_v_c, &c, _ctx); + camlidl_ml2c_z3_Z3_param_descrs(_v_p, &p, _ctx); + _res = Z3_param_descrs_to_string(c, p); + _vres = camlidl_c2ml_z3_Z3_string(&_res, _ctx); + camlidl_free(_ctx); + /* begin user-supplied deallocation sequence */ +check_error_code(c); + /* end user-supplied deallocation sequence */ + return _vres; +} + value camlidl_z3_Z3_mk_int_symbol( value _v_c, value _v_i) @@ -11344,7 +11367,7 @@ value _v1; return _v1; } -int camlidl_transl_table_z3V3_enum_6[151] = { +int camlidl_transl_table_z3V3_enum_6[152] = { Z3_OP_TRUE, Z3_OP_FALSE, Z3_OP_EQ, @@ -11476,6 +11499,7 @@ int camlidl_transl_table_z3V3_enum_6[151] = { Z3_OP_PR_SKOLEMIZE, Z3_OP_PR_MODUS_PONENS_OEQ, Z3_OP_PR_TH_LEMMA, + Z3_OP_PR_HYPER_RESOLVE, Z3_OP_RA_STORE, Z3_OP_RA_EMPTY, Z3_OP_RA_IS_EMPTY, @@ -11506,7 +11530,7 @@ void camlidl_ml2c_z3V3_Z3_decl_kind(value _v1, Z3_decl_kind * _c2, camlidl_ctx _ value camlidl_c2ml_z3V3_Z3_decl_kind(Z3_decl_kind * _c2, camlidl_ctx _ctx) { value _v1; - _v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3V3_enum_6, 151, "typedef Z3_decl_kind: bad enum value"); + _v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3V3_enum_6, 152, "typedef Z3_decl_kind: bad enum value"); return _v1; }