diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index c22ef869b..5f67e11e2 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -586,6 +586,13 @@ object (self) method cnstr_obj obj = (self#sno ctx obj) ; self end +(** Quantifier pattern objects *) +class pattern ctx = +object (self) + inherit ast ctx as super + method cnstr_obj obj = (self#sno ctx obj) ; self +end + (** Parameter description objects *) class param_descrs ctx = object (self) @@ -775,6 +782,33 @@ struct match (kind o) with | INT_SYMBOL -> (string_of_int (Z3native.get_symbol_int o#gnc o#gno)) | STRING_SYMBOL -> (Z3native.get_symbol_string o#gnc o#gno) + + (** + Creates a new symbol using an integer. + + Not all integers can be passed to this function. + The legal range of unsigned integers is 0 to 2^30-1. + *) + let mk_int ( ctx : context ) i = + (new int_symbol ctx)#cnstr_int i + + (** Creates a new symbol using a string. *) + let mk_string ( ctx : context ) s = + (new string_symbol ctx)#cnstr_string s + + (** + Create an array of symbols. + *) + let mk_ints ( ctx : context ) ( names : int array ) = + let f elem = mk_int ( ctx : context ) elem in + (Array.map f names) + + (** + Create an array of symbols. + *) + let mk_strings ( ctx : context ) ( names : string array ) = + let f elem = mk_string ( ctx : context ) elem in + (Array.map f names) end @@ -813,49 +847,26 @@ struct A string representation of the sort. *) let to_string (x : sort) = Z3native.sort_to_string x#gnc x#gno + + (** + Create a new Boolean sort. + *) + let mk_bool ( ctx : context ) = + (new bool_sort ctx)#cnstr_obj (Z3native.mk_bool_sort ctx#gno) + + (** + Create a new uninterpreted sort. + *) + let mk_uninterpreted ( ctx : context ) (s : symbol) = + (new uninterpreted_sort ctx)#cnstr_s s + + (** + Create a new uninterpreted sort. + *) + let mk_uninterpreted_s ( ctx : context ) (s : string) = + mk_uninterpreted ctx ((Symbol.mk_string ( ctx : context ) s) :> symbol) end -(** Array sorts *) -module ArraySort = -struct - (** The domain of the array sort. *) - let get_domain (x : array_sort) = create_sort x#gc (Z3native.get_array_sort_domain x#gnc x#gno) - - (** The range of the array sort. *) - let get_range (x : array_sort) = create_sort x#gc (Z3native.get_array_sort_range x#gnc x#gno) -end - -(** Bit-vector sorts *) -module BitVecSort = -struct - (** The size of the bit-vector sort. *) - let get_size (x : bitvec_sort) = Z3native.get_bv_sort_size x#gnc x#gno -end - -(** Finite domain sorts *) -module FiniteDomainSort = -struct - (** The size of the finite domain sort. *) - let get_size (x : finite_domain_sort) = - let (r, v) = Z3native.get_finite_domain_sort_size x#gnc x#gno in - if lbool_of_int(r) == L_TRUE then v - else raise (Z3native.Exception "Conversion failed.") -end - -(** Relation sorts *) -module RelationSort = -struct - (** The arity of the relation sort. *) - let get_arity (x : relation_sort) = Z3native.get_relation_arity x#gnc x#gno - - (** The sorts of the columns of the relation sort. *) - let get_column_sorts (x : relation_sort) = - let n = get_arity x in - let f i = create_sort x#gc (Z3native.get_relation_column x#gnc x#gno i) in - Array.init n f - -end - (**/**) let create_expr ctx obj = if ast_kind_of_int (Z3native.get_ast_kind ctx#gno obj) == QUANTIFIER_AST then @@ -957,6 +968,48 @@ struct raise (Z3native.Exception "parameter is not a ratinoal string") else x#rational + + (** + Creates a new function declaration. + *) + let mk_func_decl ( ctx : context ) ( name : symbol ) ( domain : sort array ) ( range : sort) = + (new func_decl ctx)#cnstr_ndr name domain range + + (** + Creates a new function declaration. + *) + let mk_func_decl_s ( ctx : context ) ( name : string ) ( domain : sort array ) ( range : sort) = + mk_func_decl ctx ((Symbol.mk_string ctx name) :> symbol) domain range + + (** + Creates a fresh function declaration with a name prefixed with . + + + *) + let mk_fresh_func_decl ( ctx : context ) ( prefix : string ) ( domain : sort array ) ( range : sort) = + (new func_decl ctx)#cnstr_pdr prefix domain range + + (** + Creates a new constant function declaration. + *) + let mk_const_decl ( ctx : context ) ( name : symbol ) ( range : sort) = + (new func_decl ctx)#cnstr_ndr name [||] range + + + (** + Creates a new constant function declaration. + *) + let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : sort) = + (new func_decl ctx)#cnstr_ndr ((Symbol.mk_string ctx name) :> symbol) [||] range + + (** + Creates a fresh constant function declaration with a name prefixed with . + + + *) + let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : sort) = + (new func_decl ctx)#cnstr_pdr prefix [||] range + end (** @@ -1046,91 +1099,103 @@ struct end -(** Datatype sorts *) -module DatatypeSort = -struct - (** The number of constructors of the datatype sort. *) - let get_num_constructors (x : datatype_sort) = Z3native.get_datatype_sort_num_constructors x#gnc x#gno - - (** The range of the array sort. *) - let get_constructors (x : datatype_sort) = - let n = (get_num_constructors x) in - let f i = (new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_constructor x#gnc x#gno i) in - Array.init n f - - (** The recognizers. *) - let get_recognizers (x : datatype_sort) = - let n = (get_num_constructors x) in - let f i = (new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_recognizer x#gnc x#gno i) in - Array.init n f - - (** The constructor accessors. *) - let get_accessors (x : datatype_sort) = - let n = (get_num_constructors x) in - let f i = ( - let fd = ((new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_constructor x#gnc x#gno i)) in - let ds = (Z3native.get_domain_size fd#gnc fd#gno) in - let g j = (new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_constructor_accessor x#gnc x#gno i j) in - Array.init ds g - ) in - Array.init n f -end - -(** Enumeration sorts *) -module EnumSort = -struct - (** The function declarations of the constants in the enumeration. *) - let get_const_decls (x : enum_sort) = x#const_decls - - (** The test predicates for the constants in the enumeration. *) - let get_tester_decls (x : enum_sort) = x#tester_decls -end - -(** List sorts *) -module ListSort = -struct - (** The declaration of the nil function of this list sort. *) - let get_nil_decl (x : list_sort) = x#nil_decl - - (** The declaration of the isNil function of this list sort. *) - let get_is_nil_decl (x : list_sort) = x#is_nil_decl - - (** The declaration of the cons function of this list sort. *) - let get_cons_decl (x : list_sort) = x#cons_decl - - (** The declaration of the isCons function of this list sort. *) - let get_is_cons_decl (x : list_sort) = x#is_cons_decl - - (** The declaration of the head function of this list sort.*) - let get_head_decl (x : list_sort) = x#head_decl - - (** The declaration of the tail function of this list sort. *) - let get_tail_decl (x : list_sort) = x#tail_decl - - (** The empty list. *) - let nil (x : list_sort) = create_expr_fa x#gc (get_nil_decl x) [||] -end - -(** Tuple sorts *) -module TupleSort = -struct - (** The constructor function of the tuple.*) - let get_mk_decl (x : tuple_sort) = - (new func_decl x#gc)#cnstr_obj (Z3native.get_tuple_sort_mk_decl x#gnc x#gno) - - (** The number of fields in the tuple. *) - let get_num_fields (x : tuple_sort) = Z3native.get_tuple_sort_num_fields x#gnc x#gno - - (** The field declarations. *) - let get_field_decls (x : tuple_sort) = - let n = get_num_fields x in - let f i = ((new func_decl x#gc)#cnstr_obj (Z3native.get_tuple_sort_field_decl x#gnc x#gno i)) in - Array.init n f -end - (** The abstract syntax tree (AST) module *) module AST = struct + (** Vectors of ASTs *) + module ASTVector = + struct + (** The size of the vector *) + let get_size ( x : ast_vector ) = + Z3native.ast_vector_size x#gnc x#gno + + (** + Retrieves the i-th object in the vector. + @param i Index + @return An AST + *) + let get ( x : ast_vector ) ( i : int ) = + create_ast x#gc (Z3native.ast_vector_get x#gnc x#gno i) + + (** Sets the i-th object in the vector. *) + let set ( x : ast_vector ) ( i : int ) ( value : ast ) = + Z3native.ast_vector_set x#gnc x#gno i value#gno + + (** Resize the vector to . + @param newSize The new size of the vector. *) + let resize ( x : ast_vector ) ( new_size : int ) = + Z3native.ast_vector_resize x#gnc x#gno new_size + + (** + Add the AST to the back of the vector. The size + is increased by 1. + @param a An AST + *) + let push ( x : ast_vector ) ( a : ast ) = + Z3native.ast_vector_push x#gnc x#gno a#gno + + (** + Translates all ASTs in the vector to . + @param to_ctx A context + @return A new ASTVector + *) + let translate ( x : ast_vector ) ( to_ctx : context ) = + (new ast_vector to_ctx)#cnstr_obj (Z3native.ast_vector_translate x#gnc x#gno to_ctx#gno) + + (** Retrieves a string representation of the vector. *) + let to_string ( x : ast_vector ) = + Z3native.ast_vector_to_string x#gnc x#gno + end + + (** Map from AST to AST *) + module ASTMap = + struct + (** Checks whether the map contains the key . + @param k An AST + @return True if is a key in the map, false otherwise. *) + let contains ( m : ast_map ) ( key : ast ) = + (lbool_of_int (Z3native.ast_map_contains m#gnc m#gno key#gno)) == L_TRUE + + (** Finds the value associated with the key . + + This function signs an error when is not a key in the map. + @param k An AST + *) + let find ( m : ast_map ) ( key : ast ) = + create_ast m#gc (Z3native.ast_map_find m#gnc m#gno key#gno) + + (** + Stores or replaces a new key/value pair in the map. + @param k The key AST + @param v The value AST + *) + let insert ( m : ast_map ) ( key : ast ) ( value : ast) = + Z3native.ast_map_insert m#gnc m#gno key#gno value#gno + + (** + Erases the key from the map. + @param k An AST + *) + let erase ( m : ast_map ) ( key : ast ) = + Z3native.ast_map_erase m#gnc m#gno key#gno + + (** Removes all keys from the map. *) + let reset ( m : ast_map ) = + Z3native.ast_map_reset m#gnc m#gno + + (** The size of the map *) + let get_size ( m : ast_map ) = + Z3native.ast_map_size m#gnc m#gno + + (** The keys stored in the map. *) + let get_keys ( m : ast_map ) = + (new ast_vector m#gc)#cnstr_obj (Z3native.ast_map_keys m#gnc m#gno) + + (** Retrieves a string representation of the map.*) + let to_strnig ( m : ast_map ) = + Z3native.ast_map_to_string m#gnc m#gno + end + (** The AST's hash code. @return A hash code @@ -1159,7 +1224,7 @@ struct | _ -> false (** - Indicates whether the AST is a BoundVariable + Indicates whether the AST is a bound variable *) let is_var ( x : ast) = (get_ast_kind x) == VAR_AST @@ -1227,163 +1292,7 @@ struct (create_ast to_ctx (Z3native.translate x#gnc x#gno to_ctx#gno)) end -(** - Parameter sets - - A Params objects represents a configuration in the form of Symbol/value pairs. -*) -module Params = -struct - (** - Adds a parameter setting. - *) - let add_bool (p : params) (name : symbol) (value : bool) = - Z3native.params_set_bool p#gnc p#gno name#gno (int_of_lbool (if value then L_TRUE else L_FALSE)) - - (** - Adds a parameter setting. - *) - let add_int (p : params) (name : symbol) (value : int) = - Z3native.params_set_uint p#gnc p#gno name#gno value - - (** - Adds a parameter setting. - *) - let add_double (p : params) (name : symbol) (value : float) = - Z3native.params_set_double p#gnc p#gno name#gno value - - (** - Adds a parameter setting. - *) - let add_symbol (p : params) (name : symbol) (value : symbol) = - Z3native.params_set_symbol p#gnc p#gno name#gno value#gno - - (** - Adds a parameter setting. - *) - let add_s_bool (p : params) (name : string) (value : bool) = - add_bool p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value - - (** - Adds a parameter setting. - *) - let add_s_int (p : params) (name : string) (value : int) = - add_int p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value - - (** - Adds a parameter setting. - *) - let add_s_double (p : params) (name : string) (value : float) = - add_double p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value - - (** - Adds a parameter setting. - *) - let add_s_symbol (p : params) (name : string) (value : symbol) = - add_symbol p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value - - (** - A string representation of the parameter set. - *) - let to_string (p : params) = Z3native.params_to_string p#gnc p#gno -end - -(** Vectors of ASTs *) -module ASTVector = -struct - (** The size of the vector *) - let get_size ( x : ast_vector ) = - Z3native.ast_vector_size x#gnc x#gno - - (** - Retrieves the i-th object in the vector. - @param i Index - @return An AST - *) - let get ( x : ast_vector ) ( i : int ) = - create_ast x#gc (Z3native.ast_vector_get x#gnc x#gno i) - - (** Sets the i-th object in the vector. *) - let set ( x : ast_vector ) ( i : int ) ( value : ast ) = - Z3native.ast_vector_set x#gnc x#gno i value#gno - - (** Resize the vector to . - @param newSize The new size of the vector. *) - let resize ( x : ast_vector ) ( new_size : int ) = - Z3native.ast_vector_resize x#gnc x#gno new_size - - (** - Add the AST to the back of the vector. The size - is increased by 1. - @param a An AST - *) - let push ( x : ast_vector ) ( a : ast ) = - Z3native.ast_vector_push x#gnc x#gno a#gno - - (** - Translates all ASTs in the vector to . - @param to_ctx A context - @return A new ASTVector - *) - let translate ( x : ast_vector ) ( to_ctx : context ) = - (new ast_vector to_ctx)#cnstr_obj (Z3native.ast_vector_translate x#gnc x#gno to_ctx#gno) - - (** Retrieves a string representation of the vector. *) - let to_string ( x : ast_vector ) = - Z3native.ast_vector_to_string x#gnc x#gno -end - -(** Map from AST to AST *) -module ASTMap = -struct - (** Checks whether the map contains the key . - @param k An AST - @return True if is a key in the map, false otherwise. *) - let contains ( m : ast_map ) ( key : ast ) = - (lbool_of_int (Z3native.ast_map_contains m#gnc m#gno key#gno)) == L_TRUE - - (** Finds the value associated with the key . - - This function signs an error when is not a key in the map. - - @param k An AST - *) - let find ( m : ast_map ) ( key : ast ) = - create_ast m#gc (Z3native.ast_map_find m#gnc m#gno key#gno) - - (** - Stores or replaces a new key/value pair in the map. - @param k The key AST - @param v The value AST - *) - let insert ( m : ast_map ) ( key : ast ) ( value : ast) = - Z3native.ast_map_insert m#gnc m#gno key#gno value#gno - - (** - Erases the key from the map. - @param k An AST - *) - let erase ( m : ast_map ) ( key : ast ) = - Z3native.ast_map_erase m#gnc m#gno key#gno - - (** Removes all keys from the map. *) - let reset ( m : ast_map ) = - Z3native.ast_map_reset m#gnc m#gno - - (** The size of the map *) - let get_size ( m : ast_map ) = - Z3native.ast_map_size m#gnc m#gno - - (** The keys stored in the map. *) - let get_keys ( m : ast_map ) = - (new ast_vector m#gc)#cnstr_obj (Z3native.ast_map_keys m#gnc m#gno) - - (** Retrieves a string representation of the map.*) - let to_strnig ( m : ast_map ) = - Z3native.ast_map_to_string m#gnc m#gno -end - -(** Expressions (terms) *) +(** General expressions (terms), including Boolean logic *) module Expr = struct (** @@ -1402,7 +1311,7 @@ struct (** Indicates whether the expression is the true or false expression - or something else (Z3_L_UNDEF). + or something else (L_UNDEF). *) let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value x#gnc x#gno) @@ -1434,7 +1343,6 @@ struct The result is the new expression. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i]. - *) let substitute ( x : expr ) from to_ = if (Array.length from) <> (Array.length to_) then @@ -1453,7 +1361,6 @@ struct Substitute the free variables in the expression with the expressions in For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term to[i]. - *) let substitute_vars ( x : expr ) to_ = create_expr x#gc (Z3native.substitute_vars x#gnc x#gno (Array.length to_) (expraton to_)) @@ -1496,28 +1403,8 @@ struct *) let is_bool ( x : expr ) = (AST.is_expr x) && (lbool_of_int (Z3native.is_eq_sort x#gnc - (Z3native.mk_bool_sort x#gnc) - (Z3native.get_sort x#gnc x#gno))) == L_TRUE - - (** - Indicates whether the term is of integer sort. - *) - let is_int ( x : expr ) = - ((lbool_of_int (Z3native.is_numeral_ast x#gnc x#gno)) == L_TRUE) && - ((sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno))) == INT_SORT) - - (** - Indicates whether the term is of sort real. - *) - let is_real ( x : expr ) = - ((sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno))) == REAL_SORT) - - (** - Indicates whether the term is of an array sort. - *) - let is_array ( x : expr ) = - ((lbool_of_int (Z3native.is_app x#gnc x#gno)) == L_TRUE) && - ((sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno))) == ARRAY_SORT) + (Z3native.mk_bool_sort x#gnc) + (Z3native.get_sort x#gnc x#gno))) == L_TRUE (** Indicates whether the term represents a constant. @@ -1526,21 +1413,6 @@ struct (get_num_args x) == 0 && FuncDecl.get_domain_size(get_func_decl x) == 0 - (** - Indicates whether the term is an integer numeral. - *) - let is_int_numeral ( x : expr ) = (is_numeral x) && (is_int x) - - (** - Indicates whether the term is a real numeral. - *) - let is_rat_num ( x : expr ) = (is_numeral x) && (is_real x) - - (** - Indicates whether the term is an algebraic number - *) - let is_algebraic_number ( x : expr ) = lbool_of_int(Z3native.is_algebraic_number x#gnc x#gno) == L_TRUE - (** Indicates whether the term is the constant true. *) @@ -1597,146 +1469,1189 @@ struct let is_implies ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES) (** - Indicates whether the term is an arithmetic numeral. + Indicates whether the term is a label (used by the Boogie Verification condition generator). + The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula. *) - let is_arithmetic_numeral ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ANUM) + let is_label ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL) (** - Indicates whether the term is a less-than-or-equal + Indicates whether the term is a label literal (used by the Boogie Verification condition generator). + A label literal has a set of string parameters. It takes no arguments. + let is_label_lit ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL_LIT) *) - let is_le ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LE) (** - Indicates whether the term is a greater-than-or-equal + Indicates whether the term is a binary equivalence modulo namings. + This binary predicate is used in proof terms. + It captures equisatisfiability and equivalence modulo renamings. *) - let is_ge ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_GE) + let is_oeq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_OEQ) (** - Indicates whether the term is a less-than + Creates a new Constant of sort and named . *) - let is_lt ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LT) + let mk_const ( ctx : context ) ( name : symbol ) ( range : sort ) = + create_expr ctx (Z3native.mk_const ctx#gno name#gno range#gno) + (** - Indicates whether the term is a greater-than + Creates a new Constant of sort and named . *) - let is_gt ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_GT) + let mk_const_s ( ctx : context ) ( name : string ) ( range : sort ) = + mk_const ctx ((Symbol.mk_string ctx name) :> symbol) range + (** - Indicates whether the term is addition (binary) + Creates a constant from the func_decl . + @param f An expression of a 0-arity function *) - let is_add ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ADD) + let mk_const_f ( ctx : context ) ( f : func_decl ) = + create_expr_fa ctx f [||] (** - Indicates whether the term is subtraction (binary) + Creates a fresh constant of sort and a + name prefixed with . *) - let is_sub ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SUB) + let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : sort) = + create_expr ctx (Z3native.mk_fresh_const ctx#gno prefix range#gno) (** - Indicates whether the term is a unary minus - *) - let is_uminus ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_UMINUS) + Create a Boolean constant. + *) + let mk_bool_const ( ctx : context ) ( name : symbol ) = + ((mk_const ctx name (Sort.mk_bool ctx)) :> bool_expr) + + (** + Create a Boolean constant. + *) + let mk_bool_const_s ( ctx : context ) ( name : string ) = + mk_bool_const ctx ((Symbol.mk_string ctx name) :> symbol) (** - Indicates whether the term is multiplication (binary) + Create a new function application. *) - let is_mul ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_MUL) + let mk_app ( ctx : context ) ( f : func_decl ) ( args : expr array ) = + create_expr_fa ctx f args (** - Indicates whether the term is division (binary) - *) - let is_div ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_DIV) + The true Term. + *) + let mk_true ( ctx : context ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_true ctx#gno) (** - Indicates whether the term is integer division (binary) - *) - let is_idiv ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IDIV) + The false Term. + *) + let mk_false ( ctx : context ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_false ctx#gno) (** - Indicates whether the term is remainder (binary) - *) - let is_remainder ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_REM) + Creates a Boolean value. + *) + let mk_bool ( ctx : context ) ( value : bool) = + if value then mk_true ctx else mk_false ctx (** - Indicates whether the term is modulus (binary) + Creates the equality = . *) - let is_modulus ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_MOD) + let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_eq ctx#gno x#gno y#gno) (** - Indicates whether the term is a coercion of integer to real (unary) + Creates a distinct term. *) - let is_inttoreal ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_TO_REAL) + let mk_distinct ( ctx : context ) ( args : expr array ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_distinct ctx#gno (Array.length args) (astaton args)) + + (** + Mk an expression representing not(a). + *) + let mk_not ( ctx : context ) ( a : bool_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_not ctx#gno a#gno) + + (** + Create an expression representing an if-then-else: ite(t1, t2, t3). + @param t1 An expression with Boolean sort + @param t2 An expression + @param t3 An expression with the same sort as + *) + let mk_ite ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) ( t3 : bool_expr ) = + create_expr ctx (Z3native.mk_ite ctx#gno t1#gno t2#gno t3#gno) + + (** + Create an expression representing t1 iff t2. + *) + let mk_iff ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_iff ctx#gno t1#gno t2#gno) (** - Indicates whether the term is a coercion of real to integer (unary) + Create an expression representing t1 -> t2. *) - let is_real_to_int ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_TO_INT) + let mk_implies ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_implies ctx#gno t1#gno t2#gno) (** - Indicates whether the term is a check that tests whether a real is integral (unary) + Create an expression representing t1 xor t2. *) - let is_real_is_int ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IS_INT) + let mk_xor ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_xor ctx#gno t1#gno t2#gno) + + (** + Create an expression representing the AND of args + *) + let mk_and ( ctx : context ) ( args : bool_expr array ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_and ctx#gno (Array.length args) (astaton args)) + + (** + Create an expression representing the OR of args + *) + let mk_or ( ctx : context ) ( args : bool_expr array ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_or ctx#gno (Array.length args) (astaton args)) +end + +(** Functions to manipulate Array expressions *) +module Arrays = +struct + (** + Create a new array sort. + *) + let mk_sort ( ctx : context ) domain range = + (new array_sort ctx)#cnstr_dr domain range (** Indicates whether the term is an array store. It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). - Array store takes at least 3 arguments. + Array store takes at least 3 arguments. *) - let is_store ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_STORE) + let is_store ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) (** Indicates whether the term is an array select. *) - let is_select ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SELECT) + let is_select ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SELECT) (** Indicates whether the term is a constant array. - For example, select(const(v),i) = v holds for every v and i. The function is unary. + For example, select(const(v),i) = v holds for every v and i. The function is unary. *) - let is_constant_array ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_CONST_ARRAY) + let is_constant_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONST_ARRAY) (** Indicates whether the term is a default array. - For example default(const(v)) = v. The function is unary. + For example default(const(v)) = v. The function is unary. *) - let is_default_array ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ARRAY_DEFAULT) + let is_default_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_DEFAULT) (** Indicates whether the term is an array map. - It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. + It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. *) - let is_array_map ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ARRAY_MAP) + let is_array_map ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_MAP) (** Indicates whether the term is an as-array term. An as-array term is n array value that behaves as the function graph of the - function passed as parameter. + function passed as parameter. *) - let is_as_array ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_AS_ARRAY) + let is_as_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) + (** + Indicates whether the term is of an array sort. + *) + let is_array ( x : expr ) = + ((lbool_of_int (Z3native.is_app x#gnc x#gno)) == L_TRUE) && + ((sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno))) == ARRAY_SORT) + + (** The domain of the array sort. *) + let get_domain (x : array_sort) = create_sort x#gc (Z3native.get_array_sort_domain x#gnc x#gno) + + (** The range of the array sort. *) + let get_range (x : array_sort) = create_sort x#gc (Z3native.get_array_sort_range x#gnc x#gno) + + + (** + Create an array constant. + *) + let mk_const ( ctx : context ) ( name : symbol ) ( domain : sort ) ( range : sort ) = + ((Expr.mk_const ctx name ((mk_sort ctx domain range) :> sort)) :> array_expr) + + (** + Create an array constant. + *) + let mk_const_s ( ctx : context ) ( name : string ) ( domain : sort ) ( range : sort ) = + mk_const ctx ((Symbol.mk_string ctx name) :> symbol) domain range + + (** + Array read. + + The argument a is the array and i is the index + of the array that gets read. + + The node a must have an array sort [domain -> range], + and i must have the sort domain. + The sort of the result is range. + + + *) + let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) = + ((create_expr ctx (Z3native.mk_select ctx#gno a#gno i#gno)) :> array_expr) + + (** + Array update. + + The node a must have an array sort [domain -> range], + i must have sort domain, + v must have sort range. The sort of the result is [domain -> range]. + The semantics of this function is given by the theory of arrays described in the SMT-LIB + standard. See http://smtlib.org for more details. + The result of this function is an array that is equal to a + (with respect to select) + on all indices except for i, where it maps to v + (and the select of a with + respect to i may be a different value). + + + *) + let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) ( v : expr) = + (new array_expr ctx)#cnstr_obj (Z3native.mk_store ctx#gno a#gno i#gno v#gno) + + (** + Create a constant array. + + The resulting term is an array, such that a selecton an arbitrary index + produces the value v. + + + *) + let mk_const_array ( ctx : context ) ( domain : sort ) ( v : expr ) = + (new array_expr ctx)#cnstr_obj (Z3native.mk_const_array ctx#gno domain#gno v#gno) + + (** + Maps f on the argument arrays. + + Eeach element of args must be of an array sort [domain_i -> range_i]. + The function declaration f must have type range_1 .. range_n -> range. + v must have sort range. The sort of the result is [domain_i -> range]. + + + + *) + let mk_map ( ctx : context ) ( f : func_decl ) ( args : array_expr array ) = + ((create_expr ctx (Z3native.mk_map ctx#gno f#gno (Array.length args) (astaton args))) :> array_expr) + + (** + Access the array default value. + + Produces the default range value, for arrays that can be represented as + finite maps with a default range value. + *) + let mk_term_array ( ctx : context ) ( arg : array_expr ) = + ((create_expr ctx (Z3native.mk_array_default ctx#gno arg#gno)) :> array_expr) +end + +(** Functions to manipulate Set expressions *) +module Sets = +struct (** Indicates whether the term is set union *) - let is_set_union ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SET_UNION) + let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) (** Indicates whether the term is set intersection *) - let is_set_intersect ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SET_INTERSECT) + let is_intersect ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) (** Indicates whether the term is set difference *) - let is_set_difference ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SET_DIFFERENCE) + let is_difference ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) (** Indicates whether the term is set complement *) - let is_set_complement ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SET_COMPLEMENT) + let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) (** Indicates whether the term is set subset *) - let is_set_subset ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SET_SUBSET) + let is_subset ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) + +(** + Create a set type. +*) +let mk_sort ( ctx : context ) ( ty : sort) = + (new set_sort ctx)#cnstr_s ty + +(** + Create an empty set. +*) +let mk_empty ( ctx : context ) ( domain : sort ) = + (create_expr ctx (Z3native.mk_empty_set ctx#gno domain#gno)) + + (** + Create the full set. + *) +let mk_full ( ctx : context ) ( domain : sort ) = + create_expr ctx (Z3native.mk_full_set ctx#gno domain#gno) + +(** + Add an element to the set. +*) +let mk_set_add ( ctx : context ) ( set : expr ) ( element : expr ) = + create_expr ctx (Z3native.mk_set_add ctx#gno set#gno element#gno) + + (** + Remove an element from a set. + *) +let mk_del ( ctx : context ) ( set : expr ) ( element : expr ) = + create_expr ctx (Z3native.mk_set_del ctx#gno set#gno element#gno) + + (** + Take the union of a list of sets. + *) +let mk_union ( ctx : context ) ( args : expr array ) = + create_expr ctx (Z3native.mk_set_union ctx#gno (Array.length args) (astaton args)) + +(** + Take the intersection of a list of sets. +*) +let mk_intersection ( ctx : context ) ( args : expr array ) = + create_expr ctx (Z3native.mk_set_intersect ctx#gno (Array.length args) (astaton args)) + +(** + Take the difference between two sets. +*) +let mk_difference ( ctx : context ) ( arg1 : expr ) ( arg2 : expr) = + create_expr ctx (Z3native.mk_set_difference ctx#gno arg1#gno arg2#gno) + +(** + Take the complement of a set. +*) +let mk_complement ( ctx : context ) ( arg : expr ) = + create_expr ctx (Z3native.mk_set_complement ctx#gno arg#gno) + +(** + Check for set membership. +*) +let mk_membership ( ctx : context ) ( elem : expr ) ( set : expr ) = + create_expr ctx (Z3native.mk_set_member ctx#gno elem#gno set#gno) + + (** + Check for subsetness of sets. + *) +let mk_subset ( ctx : context ) ( arg1 : expr ) ( arg2 : expr) = + create_expr ctx (Z3native.mk_set_subset ctx#gno arg1#gno arg2#gno) + +end + +(** Functions to manipulate Finite Domain expressions *) +module FiniteDomains = +struct + (** + Create a new finite domain sort. + *) + let mk_sort ( ctx : context ) ( name : symbol ) size = + (new finite_domain_sort ctx)#cnstr_si name size + + (** + Create a new finite domain sort. + *) + let mk_sort_s ( ctx : context ) ( name : string ) size = + (new finite_domain_sort ctx)#cnstr_si ((Symbol.mk_string ctx name) :> symbol) size + + + (** + Indicates whether the term is of an array sort. + *) + let is_finite_domain ( x : expr ) = + ((lbool_of_int (Z3native.is_app x#gnc x#gno)) == L_TRUE) && + (sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno)) == FINITE_DOMAIN_SORT) + + (** + Indicates whether the term is a less than predicate over a finite domain. + *) + let is_lt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT) + + (** The size of the finite domain sort. *) + let get_size (x : finite_domain_sort) = + let (r, v) = Z3native.get_finite_domain_sort_size x#gnc x#gno in + if lbool_of_int(r) == L_TRUE then v + else raise (Z3native.Exception "Conversion failed.") +end + +(** Functions to manipulate Relation expressions *) +module Relations = +struct + (** + Indicates whether the term is of a relation sort. + *) + let is_relation ( x : expr ) = + ((lbool_of_int (Z3native.is_app x#gnc x#gno)) == L_TRUE) && + (sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno)) == RELATION_SORT) + + (** + Indicates whether the term is an relation 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. + *) + let is_store ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_STORE) + + (** + Indicates whether the term is an empty relation + *) + let is_empty ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_EMPTY) + + (** + Indicates whether the term is a test for the emptiness of a relation + *) + let is_is_empty ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_IS_EMPTY) + + (** + Indicates whether the term is a relational join + *) + let is_join ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_JOIN) + + (** + Indicates whether the term is the union or convex hull of two relations. + The function takes two arguments. + *) + let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_UNION) + + (** + Indicates whether the term is the widening of two relations + The function takes two arguments. + *) + let is_widen ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_WIDEN) + + (** + Indicates whether the term is a projection of columns (provided as numbers in the parameters). + The function takes one argument. + *) + let is_project ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_PROJECT) + + (** + Indicates whether the term is a relation filter + + Filter (restrict) a relation with respect to a predicate. + The first argument is a relation. + The second argument is a predicate with free de-Brujin indices + corresponding to the columns of the relation. + So the first column in the relation has index 0. + *) + let is_filter ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_FILTER) + + (** + Indicates whether the term is an intersection of a relation with the negation of another. + + Intersect the first relation with respect to negation + of the second relation (the function takes two arguments). + Logically, the specification can be described by a function + + target = filter_by_negation(pos, neg, columns) + + where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that + target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with + ( x : expr ) on the columns c1, d1, .., cN, dN. + *) + let is_negation_filter ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_NEGATION_FILTER) + + (** + Indicates whether the term is the renaming of a column in a relation + + The function takes one argument. + The parameters contain the renaming as a cycle. + *) + let is_rename ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_RENAME) + + (** + Indicates whether the term is the complement of a relation + *) + let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_COMPLEMENT) + + (** + Indicates whether the term is a relational select + + Check if a record is an element of the relation. + The function takes n+1 arguments, where the first argument is a relation, + and the remaining n arguments correspond to a record. + *) + let is_select ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT) + + (** + Indicates whether the term is a relational clone (copy) + + Create a fresh copy (clone) of a relation. + The function is logically the identity, but + in the context of a register machine allows + for terms of kind + to perform destructive updates to the first argument. + *) + let is_clone ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_CLONE) + + (** The arity of the relation sort. *) + let get_arity (x : relation_sort) = Z3native.get_relation_arity x#gnc x#gno + + (** The sorts of the columns of the relation sort. *) + let get_column_sorts (x : relation_sort) = + let n = get_arity x in + let f i = create_sort x#gc (Z3native.get_relation_column x#gnc x#gno i) in + Array.init n f + +end + +(** Quantifier expressions *) +module Quantifiers = +struct + (** + The de-Burijn index of a bound variable. + + Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain + the meaning of de-Bruijn indices by indicating the compilation process from + non-de-Bruijn formulas to de-Bruijn format. + + abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) + abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) + abs1(x, x, n) = b_n + abs1(y, x, n) = y + abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) + abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) + + The last line is significant: the index of a bound variable is different depending + on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its + index. + *) + let get_index ( x : expr ) = + if not (AST.is_var x) then + raise (Z3native.Exception "Term is not a bound variable.") + else + Z3native.get_index_value x#gnc x#gno + + (** Quantifier patterns + + Patterns comprise a list of terms. The list should be + non-empty. If the list comprises of more than one term, it is + also called a multi-pattern. + *) + module Pattern = + struct + (** + The number of terms in the pattern. + *) + let get_num_terms ( x : pattern ) = + Z3native.get_pattern_num_terms x#gnc x#gno + + (** + The terms in the pattern. + *) + let get_terms ( x : pattern ) = + let n = (get_num_terms x) in + let f i = (create_expr x#gc (Z3native.get_pattern x#gnc x#gno i)) in + Array.init n f + + (** + A string representation of the pattern. + *) + let to_string ( x : pattern ) = Z3native.pattern_to_string x#gnc x#gno + end + + (** + Indicates whether the quantifier is universal. + *) + let is_universal ( x : quantifier ) = + lbool_of_int (Z3native.is_quantifier_forall x#gnc x#gno) == L_TRUE + + (** + Indicates whether the quantifier is existential. + *) + let is_existential ( x : quantifier ) = not (is_universal x) + + (** + The weight of the quantifier. + *) + let get_weight ( x : quantifier ) = Z3native.get_quantifier_weight x#gnc x#gno + + (** + The number of patterns. + *) + let get_num_patterns ( x : quantifier ) = Z3native.get_quantifier_num_patterns x#gnc x#gno + + (** + The patterns. + *) + let get_patterns ( x : quantifier ) = + let n = (get_num_patterns x) in + let f i = ((new pattern x#gc)#cnstr_obj (Z3native.get_quantifier_pattern_ast x#gnc x#gno i)) in + Array.init n f + + (** + The number of no-patterns. + *) + let get_num_no_patterns ( x : quantifier ) = Z3native.get_quantifier_num_no_patterns x#gnc x#gno + + (** + The no-patterns. + *) + let get_no_patterns ( x : quantifier ) = + let n = (get_num_patterns x) in + let f i = ((new pattern x#gc)#cnstr_obj (Z3native.get_quantifier_no_pattern_ast x#gnc x#gno i)) in + Array.init n f + + (** + The number of bound variables. + *) + let get_num_bound ( x : quantifier ) = Z3native.get_quantifier_num_bound x#gnc x#gno + + (** + The symbols for the bound variables. + *) + let get_bound_variable_names ( x : quantifier ) = + let n = (get_num_bound x) in + let f i = (create_symbol x#gc (Z3native.get_quantifier_bound_name x#gnc x#gno i)) in + Array.init n f + + (** + The sorts of the bound variables. + *) + let get_bound_variable_sorts ( x : quantifier ) = + let n = (get_num_bound x) in + let f i = (create_sort x#gc (Z3native.get_quantifier_bound_sort x#gnc x#gno i)) in + Array.init n f + + (** + The body of the quantifier. + *) + let get_body ( x : quantifier ) = + (new bool_expr x#gc)#cnstr_obj (Z3native.get_quantifier_body x#gnc x#gno) + + (** + Creates a new bound variable. + @param index The de-Bruijn index of the variable + @param ty The sort of the variable + *) + let mk_bound ( ctx : context ) ( index : int ) ( ty : sort ) = + create_expr ctx (Z3native.mk_bound ctx#gno index ty#gno) + + (** + Create a quantifier pattern. + *) + let mk_pattern ( ctx : context ) ( terms : expr array ) = + if (Array.length terms) == 0 then + raise (Z3native.Exception "Cannot create a pattern from zero terms") + else + (new pattern ctx)#cnstr_obj (Z3native.mk_pattern ctx#gno (Array.length terms) (astaton terms)) +end + +(** Functions to manipulate Datatype expressions *) +module Datatypes = +struct + (** Constructors *) + module Constructor = + struct + (** The number of fields of the constructor. *) + let get_num_fields ( x : constructor ) = x#get_n + + (** The function declaration of the constructor. *) + let get_constructor_decl ( x : constructor ) = x#constructor_decl + + (** The function declaration of the tester. *) + let get_tester_decl ( x : constructor ) = x#tester_decl + + (** The function declarations of the accessors *) + let get_accessor_decls ( x : constructor ) = x#accessor_decls + end + + (* DATATYPES *) + (** + Create a datatype constructor. + @param name constructor name + @param recognizer name of recognizer function. + @param fieldNames names of the constructor fields. + @param sorts field sorts, 0 if the field sort refers to a recursive sort. + @param sortRefs reference to datatype sort that is an argument to the constructor; + if the corresponding sort reference is 0, then the value in sort_refs should be an index + referring to one of the recursive datatypes that is declared. + *) + let mk_constructor ( ctx : context ) ( name : symbol ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array) = + (new constructor ctx)#cnstr_ssssi name recognizer field_names sorts sort_refs + + + (** + Create a datatype constructor. + @param name constructor name + @param recognizer name of recognizer function. + @param fieldNames names of the constructor fields. + @param sorts field sorts, 0 if the field sort refers to a recursive sort. + @param sortRefs reference to datatype sort that is an argument to the constructor; + if the corresponding sort reference is 0, then the value in sort_refs should be an index + referring to one of the recursive datatypes that is declared. + *) + let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array) = + mk_constructor ctx ((Symbol.mk_string ctx name) :> symbol) recognizer field_names sorts sort_refs + + + (** + Create a new datatype sort. + *) + let mk_sort ( ctx : context ) ( name : symbol ) ( constructors : constructor array) = + (new datatype_sort ctx)#cnstr_sc name constructors + + (** + Create a new datatype sort. + *) + let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : constructor array) = + mk_sort ctx ((Symbol.mk_string ctx name) :> symbol) constructors + + (** + Create mutually recursive datatypes. + @param names names of datatype sorts + @param c list of constructors, one list per sort. + *) + let mk_sorts ( ctx : context ) ( names : symbol array ) ( c : constructor array array ) = + let n = (Array.length names) in + let f e = ( (new constructor_list ctx)#cnstr_ca e ) in + let cla = (Array.map f c) in + let (r, a) = (Z3native.mk_datatypes ctx#gno n (symbolaton names) (constructor_listaton cla)) in + let g e = ( (new datatype_sort ctx)#cnstr_obj e) in + (Array.map g r) + + (** Create mutually recursive data-types. *) + let mk_sorts_s ( ctx : context ) ( names : string array ) ( c : constructor array array ) = + mk_sorts ctx + ( + let f e = ((Symbol.mk_string ctx e) :> symbol) in + Array.map f names + ) + c + + (** The number of constructors of the datatype sort. *) + let get_num_constructors (x : datatype_sort) = Z3native.get_datatype_sort_num_constructors x#gnc x#gno + + (** The range of the array sort. *) + let get_constructors (x : datatype_sort) = + let n = (get_num_constructors x) in + let f i = (new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_constructor x#gnc x#gno i) in + Array.init n f + + (** The recognizers. *) + let get_recognizers (x : datatype_sort) = + let n = (get_num_constructors x) in + let f i = (new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_recognizer x#gnc x#gno i) in + Array.init n f + + (** The constructor accessors. *) + let get_accessors (x : datatype_sort) = + let n = (get_num_constructors x) in + let f i = ( + let fd = ((new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_constructor x#gnc x#gno i)) in + let ds = (Z3native.get_domain_size fd#gnc fd#gno) in + let g j = (new func_decl x#gc)#cnstr_obj (Z3native.get_datatype_sort_constructor_accessor x#gnc x#gno i j) in + Array.init ds g + ) in + Array.init n f +end + +(** Functions to manipulate Enumeration expressions *) +module Enumerations = +struct + (** + Create a new enumeration sort. + *) + let mk_sort ( ctx : context ) name enum_names = + (new enum_sort ctx)#cnstr_ss name enum_names + + (** + Create a new enumeration sort. + *) + let mk_sort_s ( ctx : context ) name enum_names = + (new enum_sort ctx)#cnstr_ss + ((Symbol.mk_string ( ctx : context ) name) :> symbol) + (let f e = (e :> symbol) in + (Array.map f (Symbol.mk_strings ( ctx : context ) enum_names)) + ) + + (** The function declarations of the constants in the enumeration. *) + let get_const_decls (x : enum_sort) = x#const_decls + + (** The test predicates for the constants in the enumeration. *) + let get_tester_decls (x : enum_sort) = x#tester_decls +end + +(** Functions to manipulate List expressions *) +module Lists = +struct + (** + Create a new list sort. + *) + let mk_sort ( ctx : context ) (name : symbol) elem_sort = + (new list_sort ctx)#cnstr_ss name elem_sort + + (** + Create a new list sort. + *) + let mk_list_s ( ctx : context ) (name : string) elem_sort = + mk_sort ctx ((Symbol.mk_string ctx name) :> symbol) elem_sort + + + (** The declaration of the nil function of this list sort. *) + let get_nil_decl (x : list_sort) = x#nil_decl + + (** The declaration of the isNil function of this list sort. *) + let get_is_nil_decl (x : list_sort) = x#is_nil_decl + + (** The declaration of the cons function of this list sort. *) + let get_cons_decl (x : list_sort) = x#cons_decl + + (** The declaration of the isCons function of this list sort. *) + let get_is_cons_decl (x : list_sort) = x#is_cons_decl + + (** The declaration of the head function of this list sort. *) + let get_head_decl (x : list_sort) = x#head_decl + + (** The declaration of the tail function of this list sort. *) + let get_tail_decl (x : list_sort) = x#tail_decl + + (** The empty list. *) + let nil (x : list_sort) = create_expr_fa x#gc (get_nil_decl x) [||] +end + +(** Functions to manipulate Tuple expressions *) +module Tuples = +struct + (** + Create a new tuple sort. + *) + let mk_sort ( ctx : context ) name field_names field_sorts = + (new tuple_sort ctx)#cnstr_siss name (Array.length field_names) field_names field_sorts + + (** The constructor function of the tuple. *) + let get_mk_decl (x : tuple_sort) = + (new func_decl x#gc)#cnstr_obj (Z3native.get_tuple_sort_mk_decl x#gnc x#gno) + + (** The number of fields in the tuple. *) + let get_num_fields (x : tuple_sort) = Z3native.get_tuple_sort_num_fields x#gnc x#gno + + (** The field declarations. *) + let get_field_decls (x : tuple_sort) = + let n = get_num_fields x in + let f i = ((new func_decl x#gc)#cnstr_obj (Z3native.get_tuple_sort_field_decl x#gnc x#gno i)) in + Array.init n f +end + +(** Functions to manipulate arithmetic expressions *) +module Arithmetic = +struct + (** + Create a new integer sort. + *) + let mk_int_sort ( ctx : context ) = + (new int_sort ctx)#cnstr_obj (Z3native.mk_int_sort ctx#gno) + + (** + Create a real sort. + *) + let mk_real_sort ( ctx : context ) = + (new real_sort ctx)#cnstr_obj (Z3native.mk_real_sort ctx#gno) + + (** + Indicates whether the term is of integer sort. + *) + let is_int ( x : expr ) = + ((lbool_of_int (Z3native.is_numeral_ast x#gnc x#gno)) == L_TRUE) && + ((sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno))) == INT_SORT) + + (** + Indicates whether the term is an arithmetic numeral. + *) + let is_arithmetic_numeral ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM) + + (** + Indicates whether the term is a less-than-or-equal + *) + let is_le ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE) + + (** + Indicates whether the term is a greater-than-or-equal + *) + let is_ge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE) + + (** + Indicates whether the term is a less-than + *) + let is_lt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LT) + + (** + Indicates whether the term is a greater-than + *) + let is_gt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GT) + + (** + Indicates whether the term is addition (binary) + *) + let is_add ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ADD) + + (** + Indicates whether the term is subtraction (binary) + *) + let is_sub ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SUB) + + (** + Indicates whether the term is a unary minus + *) + let is_uminus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UMINUS) + + (** + Indicates whether the term is multiplication (binary) + *) + let is_mul ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MUL) + + (** + Indicates whether the term is division (binary) + *) + let is_div ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_DIV) + + (** + Indicates whether the term is integer division (binary) + *) + let is_idiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IDIV) + + (** + Indicates whether the term is remainder (binary) + *) + let is_remainder ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REM) + + (** + Indicates whether the term is modulus (binary) + *) + let is_modulus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD) + + (** + Indicates whether the term is a coercion of integer to real (unary) + *) + let is_inttoreal ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL) + + (** + Indicates whether the term is a coercion of real to integer (unary) + *) + let is_real_to_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT) + + (** + Indicates whether the term is a check that tests whether a real is integral (unary) + *) + let is_real_is_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT) + + (** + Indicates whether the term is of sort real. + *) + let is_real ( x : expr ) = + ((sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno))) == REAL_SORT) + + (** + Indicates whether the term is an integer numeral. + *) + let is_int_numeral ( x : expr ) = (Expr.is_numeral x) && (is_int x) + + (** + Indicates whether the term is a real numeral. + *) + let is_rat_num ( x : expr ) = (Expr.is_numeral x) && (is_real x) + + (** + Indicates whether the term is an algebraic number + *) + let is_algebraic_number ( x : expr ) = lbool_of_int(Z3native.is_algebraic_number x#gnc x#gno) == L_TRUE + + (** Retrieve the int value. *) + let get_int ( x : int_num ) = let (r, v) = Z3native.get_numeral_int x#gnc x#gno in + if lbool_of_int(r) == L_TRUE then v + else raise (Z3native.Exception "Conversion failed.") + + (** Returns a string representation of the numeral. *) + let to_string ( x : int_num ) = Z3native.get_numeral_string x#gnc x#gno + + (** The numerator of a rational numeral. *) + let get_numerator ( x : rat_num ) = + (new int_num x#gc)#cnstr_obj (Z3native.get_numerator x#gnc x#gno) + + (** The denominator of a rational numeral. *) + let get_denominator ( x : rat_num ) = + (new int_num x#gc)#cnstr_obj (Z3native.get_denominator x#gnc x#gno) + + (** Returns a string representation in decimal notation. + The result has at most decimal places.*) + let to_decimal_string ( x : rat_num ) (precision : int) = + Z3native.get_numeral_decimal_string x#gnc x#gno precision + + (** Returns a string representation of the numeral. *) + let to_string ( x : rat_num ) = Z3native.get_numeral_string x#gnc x#gno + + (** + Creates an integer constant. + *) + let mk_int_const ( ctx : context ) ( name : symbol ) = + ((Expr.mk_const ctx name (mk_int_sort ctx)) :> int_expr) + + (** + Creates an integer constant. + *) + let mk_int_const_s ( ctx : context ) ( name : string ) = + mk_int_const ctx ((Symbol.mk_string ctx name) :> symbol) + + (** + Creates a real constant. + *) + let mk_real_const ( ctx : context ) ( name : symbol ) = + ((Expr.mk_const ctx name (mk_real_sort ctx)) :> real_expr) + + (** + Creates a real constant. + *) + let mk_real_const_s ( ctx : context ) ( name : string ) = + mk_real_const ctx ((Symbol.mk_string ctx name) :> symbol) + + (** + Create an expression representing t[0] + t[1] + .... + *) + let mk_add ( ctx : context ) ( t : arith_expr array ) = + (create_expr ctx (Z3native.mk_add ctx#gno (Array.length t) (astaton t)) :> arith_expr) + + (** + Create an expression representing t[0] * t[1] * .... + *) + let mk_mul ( ctx : context ) ( t : arith_expr array ) = + (create_expr ctx (Z3native.mk_mul ctx#gno (Array.length t) (astaton t)) :> arith_expr) + + (** + Create an expression representing t[0] - t[1] - .... + *) + let mk_sub ( ctx : context ) ( t : arith_expr array ) = + (create_expr ctx (Z3native.mk_sub ctx#gno (Array.length t) (astaton t)) :> arith_expr) + + (** + Create an expression representing -t. + *) + let mk_unary_minus ( ctx : context ) ( t : arith_expr ) = + (create_expr ctx (Z3native.mk_unary_minus ctx#gno t#gno) :> arith_expr) + + (** + Create an expression representing t1 / t2. + *) + let mk_div ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = + (create_expr ctx (Z3native.mk_div ctx#gno t1#gno t2#gno) :> arith_expr) + + (** + Create an expression representing t1 mod t2. + The arguments must have int type. + *) + let mk_mod ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + (new int_expr ctx)#cnstr_obj (Z3native.mk_mod ctx#gno t1#gno t2#gno) + + (** + Create an expression representing t1 rem t2. + The arguments must have int type. + *) + let mk_rem ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + (new int_expr ctx)#cnstr_obj (Z3native.mk_rem ctx#gno t1#gno t2#gno) + + (** + Create an expression representing t1 ^ t2. + *) + let mk_Power ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + (create_expr ctx (Z3native.mk_power ctx#gno t1#gno t2#gno) :> arith_expr) + + (** + Create an expression representing t1 < t2 + *) + let mk_lt ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_lt ctx#gno t1#gno t2#gno) + + (** + Create an expression representing t1 <= t2 + *) + let mk_le ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_le ctx#gno t1#gno t2#gno) + + (** + Create an expression representing t1 > t2 + *) + let mk_gt ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_gt ctx#gno t1#gno t2#gno) + + (** + Create an expression representing t1 >= t2 + *) + let mk_ge ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_ge ctx#gno t1#gno t2#gno) + + (** + Coerce an integer to a real. + + + There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard. + + You can take the floor of a real by creating an auxiliary integer Term k and + and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. + The argument must be of integer sort. + *) + let mk_int2real ( ctx : context ) ( t : int_expr ) = + (new real_expr ctx)#cnstr_obj (Z3native.mk_int2real ctx#gno t#gno) + + (** + Coerce a real to an integer. + + + The semantics of this function follows the SMT-LIB standard for the function to_int. + The argument must be of real sort. + *) + let mk_real2int ( ctx : context ) ( t : real_expr ) = + (new int_expr ctx)#cnstr_obj (Z3native.mk_real2int ctx#gno t#gno) + + (** + Creates an expression that checks whether a real number is an integer. + *) + let mk_is_integer ( ctx : context ) ( t : real_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_is_int ctx#gno t#gno) + + (** + Return a upper bound for a given real algebraic number. + The interval isolating the number is smaller than 1/10^. + + @param precision the precision of the result + @return A numeral Expr of sort Real + *) + let to_upper ( x : algebraic_num ) ( precision : int ) = + (new rat_num x#gc)#cnstr_obj (Z3native.get_algebraic_number_upper x#gnc x#gno precision) + + (** + Return a lower bound for the given real algebraic number. + The interval isolating the number is smaller than 1/10^. + + @param precision the precision of the result + @return A numeral Expr of sort Real + *) + let to_lower ( x : algebraic_num ) precision = + (new rat_num x#gc)#cnstr_obj (Z3native.get_algebraic_number_lower x#gnc x#gno precision) + + (** Returns a string representation in decimal notation. + The result has at most decimal places.*) + let to_decimal_string ( x : algebraic_num ) ( precision : int ) = + Z3native.get_numeral_decimal_string x#gnc x#gno precision + + (** Returns a string representation of the numeral. *) + let to_string ( x : algebraic_num ) = Z3native.get_numeral_string x#gnc x#gno +end + + +(** Functions to manipulate bit-vector expressions *) +module BitVectors = +struct + (** + Create a new bit-vector sort. + *) + let mk_sort ( ctx : context ) size = + (new bitvec_sort ctx)#cnstr_obj (Z3native.mk_bv_sort ctx#gno size) (** Indicates whether the terms is of bit-vector sort. @@ -1747,300 +2662,750 @@ struct (** Indicates whether the term is a bit-vector numeral *) - let is_bv_numeral ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BNUM) + let is_bv_numeral ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNUM) (** Indicates whether the term is a one-bit bit-vector with value one *) - let is_bv_bit1 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BIT1) + let is_bv_bit1 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT1) (** Indicates whether the term is a one-bit bit-vector with value zero *) - let is_bv_bit0 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BIT0) + let is_bv_bit0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT0) (** Indicates whether the term is a bit-vector unary minus *) - let is_bv_uminus ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BNEG) + let is_bv_uminus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNEG) (** Indicates whether the term is a bit-vector addition (binary) *) - let is_bv_add ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BADD) + let is_bv_add ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BADD) (** Indicates whether the term is a bit-vector subtraction (binary) *) - let is_bv_sub ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSUB) + let is_bv_sub ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSUB) (** Indicates whether the term is a bit-vector multiplication (binary) *) - let is_bv_mul ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BMUL) + let is_bv_mul ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BMUL) (** Indicates whether the term is a bit-vector signed division (binary) *) - let is_bv_sdiv ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSDIV) + let is_bv_sdiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV) (** Indicates whether the term is a bit-vector unsigned division (binary) *) - let is_bv_udiv ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BUDIV) + let is_bv_udiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV) (** Indicates whether the term is a bit-vector signed remainder (binary) *) - let is_bv_SRem ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSREM) + let is_bv_SRem ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM) (** Indicates whether the term is a bit-vector unsigned remainder (binary) *) - let is_bv_urem ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BUREM) + let is_bv_urem ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM) (** Indicates whether the term is a bit-vector signed modulus *) - let is_bv_smod ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSMOD) + let is_bv_smod ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD) (** Indicates whether the term is a bit-vector signed division by zero *) - let is_bv_sdiv0 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSDIV0) + let is_bv_sdiv0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV0) (** Indicates whether the term is a bit-vector unsigned division by zero *) - let is_bv_udiv0 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BUDIV0) + let is_bv_udiv0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV0) (** Indicates whether the term is a bit-vector signed remainder by zero *) - let is_bv_srem0 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSREM0) + let is_bv_srem0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM0) (** Indicates whether the term is a bit-vector unsigned remainder by zero *) - let is_bv_urem0 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BUREM0) + let is_bv_urem0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM0) (** Indicates whether the term is a bit-vector signed modulus by zero *) - let is_bv_smod0 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSMOD0) + let is_bv_smod0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD0) (** Indicates whether the term is an unsigned bit-vector less-than-or-equal *) - let is_bv_ule ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ULEQ) + let is_bv_ule ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULEQ) (** Indicates whether the term is a signed bit-vector less-than-or-equal *) - let is_bv_sle ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SLEQ) + let is_bv_sle ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLEQ) (** Indicates whether the term is an unsigned bit-vector greater-than-or-equal *) - let is_bv_uge ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_UGEQ) + let is_bv_uge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGEQ) (** Indicates whether the term is a signed bit-vector greater-than-or-equal *) - let is_bv_sge ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SGEQ) + let is_bv_sge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGEQ) (** Indicates whether the term is an unsigned bit-vector less-than *) - let is_bv_ult ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ULT) + let is_bv_ult ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULT) (** Indicates whether the term is a signed bit-vector less-than *) - let is_bv_slt ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SLT) + let is_bv_slt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLT) (** Indicates whether the term is an unsigned bit-vector greater-than *) - let is_bv_ugt ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_UGT) + let is_bv_ugt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGT) (** Indicates whether the term is a signed bit-vector greater-than *) - let is_bv_sgt ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SGT) + let is_bv_sgt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGT) (** Indicates whether the term is a bit-wise AND *) - let is_bv_and ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BAND) + let is_bv_and ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BAND) (** Indicates whether the term is a bit-wise OR *) - let is_bv_or ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BOR) + let is_bv_or ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BOR) (** Indicates whether the term is a bit-wise NOT *) - let is_bv_not ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BNOT) + let is_bv_not ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOT) (** Indicates whether the term is a bit-wise XOR *) - let is_bv_xor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BXOR) + let is_bv_xor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXOR) (** Indicates whether the term is a bit-wise NAND *) - let is_bv_nand ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BNAND) + let is_bv_nand ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNAND) (** Indicates whether the term is a bit-wise NOR *) - let is_bv_nor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BNOR) + let is_bv_nor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOR) (** Indicates whether the term is a bit-wise XNOR *) - let is_bv_xnor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BXNOR) + let is_bv_xnor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXNOR) (** Indicates whether the term is a bit-vector concatenation (binary) *) - let is_bv_concat ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_CONCAT) + let is_bv_concat ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONCAT) (** Indicates whether the term is a bit-vector sign extension *) - let is_bv_signextension ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_SIGN_EXT) + let is_bv_signextension ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SIGN_EXT) (** Indicates whether the term is a bit-vector zero extension *) - let is_bv_zeroextension ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ZERO_EXT) + let is_bv_zeroextension ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ZERO_EXT) (** Indicates whether the term is a bit-vector extraction *) - let is_bv_extract ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_EXTRACT) + let is_bv_extract ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXTRACT) (** Indicates whether the term is a bit-vector repetition *) - let is_bv_repeat ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_REPEAT) + let is_bv_repeat ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REPEAT) (** Indicates whether the term is a bit-vector reduce OR *) - let is_bv_reduceor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BREDOR) + let is_bv_reduceor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDOR) (** Indicates whether the term is a bit-vector reduce AND *) - let is_bv_reduceand ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BREDAND) + let is_bv_reduceand ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDAND) (** Indicates whether the term is a bit-vector comparison *) - let is_bv_comp ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BCOMP) + let is_bv_comp ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BCOMP) (** Indicates whether the term is a bit-vector shift left *) - let is_bv_shiftleft ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BSHL) + let is_bv_shiftleft ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSHL) (** Indicates whether the term is a bit-vector logical shift right *) - let is_bv_shiftrightlogical ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BLSHR) + let is_bv_shiftrightlogical ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BLSHR) (** Indicates whether the term is a bit-vector arithmetic shift left *) - let is_bv_shiftrightarithmetic ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BASHR) + let is_bv_shiftrightarithmetic ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BASHR) (** Indicates whether the term is a bit-vector rotate left *) - let is_bv_rotateleft ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ROTATE_LEFT) + let is_bv_rotateleft ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_LEFT) (** Indicates whether the term is a bit-vector rotate right *) - let is_bv_rotateright ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ROTATE_RIGHT) + let is_bv_rotateright ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_RIGHT) (** Indicates whether the term is a bit-vector rotate left (extended) - Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. + Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. *) - let is_bv_rotateleftextended ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_EXT_ROTATE_LEFT) + let is_bv_rotateleftextended ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_LEFT) (** Indicates whether the term is a bit-vector rotate right (extended) - Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. + Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. *) - let is_bv_rotaterightextended ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_EXT_ROTATE_RIGHT) + let is_bv_rotaterightextended ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) (** Indicates whether the term is a coercion from integer to bit-vector This function is not supported by the decision procedures. Only the most - rudimentary simplification rules are applied to this function. + rudimentary simplification rules are applied to this function. *) - let is_int_to_bv ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_INT2BV) + let is_int_to_bv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV) (** Indicates whether the term is a coercion from bit-vector to integer This function is not supported by the decision procedures. Only the most - rudimentary simplification rules are applied to this function. + rudimentary simplification rules are applied to this function. *) - let is_bv_to_int ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_BV2INT) + let is_bv_to_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT) (** Indicates whether the term is a bit-vector carry Compute the carry bit in a full-adder. The meaning is given by the - equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) + equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) *) - let is_bv_carry ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_CARRY) + let is_bv_carry ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY) (** Indicates whether the term is a bit-vector ternary XOR - The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) + The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) *) - let is_bv_xor3 ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR3) + let is_bv_xor3 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3) + + (** The size of a bit-vector sort. *) + let get_size (x : bitvec_sort) = Z3native.get_bv_sort_size x#gnc x#gno + + (** Retrieve the int value. *) + let get_int ( x : bitvec_num ) = let (r, v) = Z3native.get_numeral_int x#gnc x#gno in + if lbool_of_int(r) == L_TRUE then v + else raise (Z3native.Exception "Conversion failed.") + + (** Returns a string representation of the numeral. *) + let to_string ( x : bitvec_num ) = Z3native.get_numeral_string x#gnc x#gno (** - Indicates whether the term is a label (used by the Boogie Verification condition generator). - The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula. + Creates a bit-vector constant. *) - let is_label ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL) + let mk_const ( ctx : context ) ( name : symbol ) ( size : int ) = + ((Expr.mk_const ctx name (mk_sort ctx size)) :> bitvec_expr) (** - Indicates whether the term is a label literal (used by the Boogie Verification condition generator). - A label literal has a set of string parameters. It takes no arguments. - let is_label_lit ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL_LIT) + Creates a bit-vector constant. *) + let mk_const_s ( ctx : context ) ( name : string ) ( size : int ) = + mk_const ctx ((Symbol.mk_string ctx name) :> symbol) size (** - Indicates whether the term is a binary equivalence modulo namings. - This binary predicate is used in proof terms. - It captures equisatisfiability and equivalence modulo renamings. + Bitwise negation. + The argument must have a bit-vector sort. *) - let is_oeq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_OEQ) + let mk_not ( ctx : context ) ( t : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvnot ctx#gno t#gno) + (** + Take conjunction of bits in a vector,vector of length 1. + The argument must have a bit-vector sort. + *) + let mk_redand ( ctx : context ) ( t : bitvec_expr) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvredand ctx#gno t#gno) + + (** + Take disjunction of bits in a vector,vector of length 1. + The argument must have a bit-vector sort. + *) + let mk_redor ( ctx : context ) ( t : bitvec_expr) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvredor ctx#gno t#gno) + + (** + Bitwise conjunction. + The arguments must have a bit-vector sort. + *) + let mk_and ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvand ctx#gno t1#gno t2#gno) + + (** + Bitwise disjunction. + The arguments must have a bit-vector sort. + *) + let mk_or ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvor ctx#gno t1#gno t2#gno) + + (** + Bitwise XOR. + The arguments must have a bit-vector sort. + *) + let mk_xor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvxor ctx#gno t1#gno t2#gno) + + (** + Bitwise NAND. + The arguments must have a bit-vector sort. + *) + let mk_nand ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvnand ctx#gno t1#gno t2#gno) + + (** + Bitwise NOR. + The arguments must have a bit-vector sort. + *) + let mk_nor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvnor ctx#gno t1#gno t2#gno) + + (** + Bitwise XNOR. + The arguments must have a bit-vector sort. + *) + let mk_xnor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvxnor ctx#gno t1#gno t2#gno) + + (** + Standard two's complement unary minus. + The arguments must have a bit-vector sort. + *) + let mk_neg ( ctx : context ) ( t : bitvec_expr) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvneg ctx#gno t#gno) + + (** + Two's complement addition. + The arguments must have the same bit-vector sort. + *) + let mk_add ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvadd ctx#gno t1#gno t2#gno) + + (** + Two's complement subtraction. + The arguments must have the same bit-vector sort. + *) + let mk_sub ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvsub ctx#gno t1#gno t2#gno) + + (** + Two's complement multiplication. + The arguments must have the same bit-vector sort. + *) + let mk_mul ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvmul ctx#gno t1#gno t2#gno) + + (** + Unsigned division. + + + It is defined as the floor of t1/t2 if \c t2 is + different from zero. If t2 is zero, then the result + is undefined. + The arguments must have the same bit-vector sort. + *) + let mk_udiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvudiv ctx#gno t1#gno t2#gno) + + (** + Signed division. + + It is defined in the following way: + + - The \c floor of t1/t2 if \c t2 is different from zero, and t1*t2 >= 0. + + - The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 < 0. + + If t2 is zero, then the result is undefined. + The arguments must have the same bit-vector sort. + *) + let mk_sdiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvsdiv ctx#gno t1#gno t2#gno) + + (** + Unsigned remainder. + + It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. + If t2 is zero, then the result is undefined. + The arguments must have the same bit-vector sort. + *) + let mk_urem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvurem ctx#gno t1#gno t2#gno) + + (** + Signed remainder. + + It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. + The most significant bit (sign) of the result is equal to the most significant bit of \c t1. + + If t2 is zero, then the result is undefined. + The arguments must have the same bit-vector sort. + *) + let mk_srem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvsrem ctx#gno t1#gno t2#gno) + + (** + Two's complement signed remainder (sign follows divisor). + + If t2 is zero, then the result is undefined. + The arguments must have the same bit-vector sort. + *) + let mk_smod ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvsmod ctx#gno t1#gno t2#gno) + + (** + Unsigned less-than + + The arguments must have the same bit-vector sort. + *) + let mk_ult ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvult ctx#gno t1#gno t2#gno) + + (** + Two's complement signed less-than + + The arguments must have the same bit-vector sort. + *) + let mk_slt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvslt ctx#gno t1#gno t2#gno) + + (** + Unsigned less-than or equal to. + + The arguments must have the same bit-vector sort. + *) + let mk_ule ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvule ctx#gno t1#gno t2#gno) + + (** + Two's complement signed less-than or equal to. + + The arguments must have the same bit-vector sort. + *) + let mk_sle ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvsle ctx#gno t1#gno t2#gno) + + (** + Unsigned greater than or equal to. + + The arguments must have the same bit-vector sort. + *) + let mk_uge ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvuge ctx#gno t1#gno t2#gno) + + (** + Two's complement signed greater than or equal to. + + The arguments must have the same bit-vector sort. + *) + let mk_SGE ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvsge ctx#gno t1#gno t2#gno) + + (** + Unsigned greater-than. + + The arguments must have the same bit-vector sort. + *) + let mk_ugt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvugt ctx#gno t1#gno t2#gno) + + (** + Two's complement signed greater-than. + + The arguments must have the same bit-vector sort. + *) + let mk_sgt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvsgt ctx#gno t1#gno t2#gno) + + (** + Bit-vector concatenation. + + The arguments must have a bit-vector sort. + @return + The result is a bit-vector of size n1+n2, where n1 (n2) + is the size of t1 (t2). + *) + let mk_concat ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_concat ctx#gno t1#gno t2#gno) + + (** + Bit-vector extraction. + + Extract the bits down to from a bitvector of + size m to yield a new bitvector of size n, where + n = high - low + 1. + The argument must have a bit-vector sort. + *) + let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_extract ctx#gno high low t#gno) + + (** + Bit-vector sign extension. + + Sign-extends the given bit-vector to the (signed) equivalent bitvector of + size m+i, where \c m is the size of the given bit-vector. + The argument must have a bit-vector sort. + *) + let mk_sign_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_sign_ext ctx#gno i t#gno) + + (** + Bit-vector zero extension. + + Extend the given bit-vector with zeros to the (unsigned) equivalent + bitvector of size m+i, where \c m is the size of the + given bit-vector. + The argument must have a bit-vector sort. + *) + let mk_zero_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_zero_ext ctx#gno i t#gno) + + (** + Bit-vector repetition. + + The argument must have a bit-vector sort. + *) + let mk_repeat ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_repeat ctx#gno i t#gno) + + (** + Shift left. + + + It is equivalent to multiplication by 2^x where \c x is the value of . + + NB. 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 arguments must have a bit-vector sort. + *) + let mk_shl ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvshl ctx#gno t1#gno t2#gno) + + (** + Logical shift right + + It is equivalent to unsigned division by 2^x where \c x is the value of . + + NB. 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 arguments must have a bit-vector sort. + *) + let mk_lshr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvlshr ctx#gno t1#gno t2#gno) + + (** + Arithmetic shift right + + It is like logical shift right except that the most significant + bits of the result always copy the most significant bit of the + second argument. + + NB. 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 arguments must have a bit-vector sort. + *) + let mk_ashr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvashr ctx#gno t1#gno t2#gno) + + (** + Rotate Left. + + Rotate bits of \c t to the left \c i times. + The argument must have a bit-vector sort. + *) + let mk_rotate_left ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_rotate_left ctx#gno i t#gno) + + (** + Rotate Right. + + Rotate bits of \c t to the right \c i times. + The argument must have a bit-vector sort. + *) + let mk_rotate_right ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_rotate_right ctx#gno i t#gno) + + (** + Rotate Left. + + Rotate bits of to the left times. + The arguments must have the same bit-vector sort. + *) + let mk_rotate_left ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_ext_rotate_left ctx#gno t1#gno t2#gno) + + (** + Rotate Right. + + + Rotate bits of to the right times. + The arguments must have the same bit-vector sort. + *) + let mk_rotate_right ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_ext_rotate_right ctx#gno t1#gno t2#gno) + + (** + Create an bit bit-vector from the integer argument . + + + NB. 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 argument must be of integer sort. + *) + let mk_int2bv ( ctx : context ) ( n : int ) ( t : int_expr ) = + (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_int2bv ctx#gno n t#gno) + + (** + Create an integer from the bit-vector argument . + + + If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. + So the result is non-negative and in the range [0..2^N-1], where + N are the number of bits in . + If \c is_signed is true, \c t1 is treated as a signed bit-vector. + + NB. 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 argument must be of bit-vector sort. + *) + let mk_bv2int ( ctx : context ) ( t : bitvec_expr ) ( signed : bool) = + (new int_expr ctx)#cnstr_obj (Z3native.mk_bv2int ctx#gno t#gno (int_of_lbool (if (signed) then L_TRUE else L_FALSE))) + + (** + Create a predicate that checks that the bit-wise addition does not overflow. + + The arguments must be of bit-vector sort. + *) + let mk_add_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvadd_no_overflow ctx#gno t1#gno t2#gno (int_of_lbool (if (signed) then L_TRUE else L_FALSE))) + + (** + Create a predicate that checks that the bit-wise addition does not underflow. + + The arguments must be of bit-vector sort. + *) + let mk_add_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvadd_no_underflow ctx#gno t1#gno t2#gno) + + (** + Create a predicate that checks that the bit-wise subtraction does not overflow. + + The arguments must be of bit-vector sort. + *) + let mk_sub_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvsub_no_overflow ctx#gno t1#gno t2#gno) + + (** + Create a predicate that checks that the bit-wise subtraction does not underflow. + + The arguments must be of bit-vector sort. + *) + let mk_sub_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvsub_no_underflow ctx#gno t1#gno t2#gno (int_of_lbool (if (signed) then L_TRUE else L_FALSE))) + + (** + Create a predicate that checks that the bit-wise signed division does not overflow. + + The arguments must be of bit-vector sort. + *) + let mk_sdiv_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvsdiv_no_overflow ctx#gno t1#gno t2#gno) + + (** + Create a predicate that checks that the bit-wise negation does not overflow. + + The arguments must be of bit-vector sort. + *) + let mk_neg_no_overflow ( ctx : context ) ( t : bitvec_expr) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvneg_no_overflow ctx#gno t#gno) + + (** + Create a predicate that checks that the bit-wise multiplication does not overflow. + + The arguments must be of bit-vector sort. + *) + let mk_mul_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvmul_no_overflow ctx#gno t1#gno t2#gno (int_of_lbool (if (signed) then L_TRUE else L_FALSE))) + + (** + Create a predicate that checks that the bit-wise multiplication does not underflow. + + The arguments must be of bit-vector sort. + *) + let mk_mul_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + (new bool_expr ctx)#cnstr_obj (Z3native.mk_bvmul_no_underflow ctx#gno t1#gno t2#gno) + +end + +(** Functions to manipulate Proof objects *) +module Proofs = +struct (** Indicates whether the term is a Proof for the expression 'true'. *) - let is_proof_true ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_TRUE) + let is_true ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE) (** Indicates whether the term is a proof for a fact asserted by the user. *) - let is_proof_asserted ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_ASSERTED) + let is_asserted ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ASSERTED) (** Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. *) - let is_proof_goal ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_GOAL) + let is_goal ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_GOAL) (** Indicates whether the term is proof via modus ponens @@ -2049,18 +3414,18 @@ struct T1: p T2: (implies p q) [mp T1 T2]: q - The second antecedents may also be a proof for (iff p q). + The second antecedents may also be a proof for (iff p q). *) - let is_proof_modus_ponens ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_MODUS_PONENS) + let is_modus_ponens ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS) (** Indicates whether the term is a proof for (R t t), where R is a reflexive relation. This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. - That is, R is either '~', '=' or 'iff'. + That is, R is either '~', '=' or 'iff'. *) - let is_proof_reflexivity ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_REFLEXIVITY) + let is_reflexivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REFLEXIVITY) (** Indicates whether the term is proof by symmetricity of a relation @@ -2069,9 +3434,8 @@ struct T1: (R t s) [symmetry T1]: (R s t) T1 is the antecedent of this proof object. - *) - let is_proof_symmetry ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_SYMMETRY) + let is_symmetry ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SYMMETRY) (** Indicates whether the term is a proof by transitivity of a relation @@ -2081,9 +3445,8 @@ struct T1: (R t s) T2: (R s u) [trans T1 T2]: (R t u) - *) - let is_proof_transitivity ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_TRANSITIVITY) + let is_transitivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY) (** Indicates whether the term is a proof by condensed transitivity of a relation @@ -2102,9 +3465,8 @@ struct using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b. - *) - let is_proof_Transitivity_star ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_TRANSITIVITY_STAR) + let is_Transitivity_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY_STAR) (** @@ -2116,9 +3478,8 @@ struct [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are supressed to save space. - *) - let is_proof_monotonicity ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_MONOTONICITY) + let is_monotonicity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MONOTONICITY) (** Indicates whether the term is a quant-intro proof @@ -2126,9 +3487,8 @@ struct Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) - *) - let is_proof_quant_intro ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_QUANT_INTRO) + let is_quant_intro ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INTRO) (** Indicates whether the term is a distributivity proof object. @@ -2144,9 +3504,8 @@ struct This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and. - *) - let is_proof_distributivity ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_DISTRIBUTIVITY) + let is_distributivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DISTRIBUTIVITY) (** Indicates whether the term is a proof by elimination of AND @@ -2154,9 +3513,8 @@ struct Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and l_1 ... l_n) [and-elim T1]: l_i - *) - let is_proof_and_elimination ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_AND_ELIM) + let is_and_elimination ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_AND_ELIM) (** Indicates whether the term is a proof by eliminiation of not-or @@ -2164,9 +3522,8 @@ struct Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) - *) - let is_proof_or_elimination ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_NOT_OR_ELIM) + let is_or_elimination ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NOT_OR_ELIM) (** Indicates whether the term is a proof by rewriting @@ -2183,9 +3540,8 @@ struct (= (+ ( x : expr ) 0) x) (= (+ ( x : expr ) 1 2) (+ 3 x)) (iff (or ( x : expr ) false) x) - *) - let is_proof_rewrite ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_REWRITE) + let is_rewrite ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE) (** Indicates whether the term is a proof by rewriting @@ -2199,17 +3555,15 @@ struct - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true) - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) - *) - let is_proof_rewrite_star ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_REWRITE_STAR) + let is_rewrite_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE_STAR) (** Indicates whether the term is a proof for pulling quantifiers out. A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. - *) - let is_proof_pull_quant ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_PULL_QUANT) + let is_pull_quant ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT) (** Indicates whether the term is a proof for pulling quantifiers out. @@ -2217,9 +3571,8 @@ struct A proof for (iff P Q) where Q is in prenex normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object has no antecedents - *) - let is_proof_pull_quant_star ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_PULL_QUANT_STAR) + let is_pull_quant_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT_STAR) (** Indicates whether the term is a proof for pushing quantifiers in. @@ -2230,9 +3583,9 @@ struct ... (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no antecedents - *) - let is_proof_push_quant ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_PUSH_QUANT) + + let is_push_quant ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PUSH_QUANT) (** Indicates whether the term is a proof for elimination of unused variables. @@ -2242,9 +3595,9 @@ struct It is used to justify the elimination of unused variables. This proof object has no antecedents. - *) - let is_proof_elim_unused_vars ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_ELIM_UNUSED_VARS) + + let is_elim_unused_vars ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ELIM_UNUSED_VARS) (** Indicates whether the term is a proof for destructive equality resolution @@ -2256,23 +3609,22 @@ struct This proof object has no antecedents. Several variables can be eliminated simultaneously. - *) - let is_proof_der ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_DER) + + let is_der ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DER) (** Indicates whether the term is a proof for quantifier instantiation A proof of (or (not (forall (x) (P x))) (P a)) - *) - let is_proof_quant_inst ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_QUANT_INST) + let is_quant_inst ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INST) (** Indicates whether the term is a hypthesis marker. - Mark a hypothesis in a natural deduction style proof. + Mark a hypothesis in a natural deduction style proof. *) - let is_proof_hypothesis ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_HYPOTHESIS) + let is_hypothesis ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_HYPOTHESIS) (** Indicates whether the term is a proof by lemma @@ -2283,9 +3635,8 @@ struct This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n. - *) - let is_proof_lemma ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_LEMMA) + let is_lemma ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_LEMMA) (** Indicates whether the term is a proof by unit resolution @@ -2295,27 +3646,24 @@ struct ... T(n+1): (not l_n) [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') - *) - let is_proof_unit_resolution ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_UNIT_RESOLUTION) + let is_unit_resolution ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_UNIT_RESOLUTION) (** Indicates whether the term is a proof by iff-true T1: p [iff-true T1]: (iff p true) - *) - let is_proof_iff_true ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_IFF_TRUE) + let is_iff_true ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_TRUE) (** Indicates whether the term is a proof by iff-false T1: (not p) [iff-false T1]: (iff p false) - *) - let is_proof_iff_false ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_IFF_FALSE) + let is_iff_false ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_FALSE) (** Indicates whether the term is a proof by commutativity @@ -2326,9 +3674,8 @@ struct This proof object has no antecedents. Remark: if f is bool, then = is iff. - *) - let is_proof_commutativity ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_COMMUTATIVITY) (* *) + let is_commutativity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_COMMUTATIVITY) (* *) (** Indicates whether the term is a proof for Tseitin-like axioms @@ -2362,9 +3709,8 @@ struct You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3). - *) - let is_proof_def_axiom ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_DEF_AXIOM) + let is_def_axiom ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_AXIOM) (** Indicates whether the term is a proof for introduction of a name @@ -2385,9 +3731,8 @@ struct Otherwise: [def-intro]: (= n e) - *) - let is_proof_def_intro ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_DEF_INTRO) + let is_def_intro ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_INTRO) (** Indicates whether the term is a proof for application of a definition @@ -2395,18 +3740,16 @@ struct [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F. - *) - let is_proof_apply_def ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_APPLY_DEF) + let is_apply_def ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_APPLY_DEF) (** Indicates whether the term is a proof iff-oeq T1: (iff p q) [iff~ T1]: (~ p q) - *) - let is_proof_iff_oeq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_IFF_OEQ) + let is_iff_oeq ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_OEQ) (** Indicates whether the term is a proof for a positive NNF step @@ -2432,9 +3775,8 @@ struct for NNF_POS are 'implies', 'iff', 'xor', 'ite'. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'. - *) - let is_proof_nnf_pos ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_NNF_POS) + let is_nnf_pos ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_POS) (** Indicates whether the term is a proof for a negative NNF step @@ -2457,9 +3799,8 @@ struct T4: s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2'))) - *) - let is_proof_nnf_neg ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_NNF_NEG) + let is_nnf_neg ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_NEG) (** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. @@ -2469,9 +3810,8 @@ struct This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. - *) - let is_proof_nnf_star ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_NNF_STAR) + let is_nnf_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_STAR) (** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. @@ -2479,9 +3819,8 @@ struct A proof for (~ P Q) where Q is in conjunctive normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. - *) - let is_proof_cnf_star ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_CNF_STAR) + let is_cnf_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_CNF_STAR) (** Indicates whether the term is a proof for a Skolemization step @@ -2492,9 +3831,8 @@ struct [sk]: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y)) This proof object has no antecedents. - *) - let is_proof_skolemize ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_SKOLEMIZE) + let is_skolemize ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SKOLEMIZE) (** Indicates whether the term is a proof by modus ponens for equi-satisfiability. @@ -2503,9 +3841,8 @@ struct T1: p T2: (~ p q) [mp~ T1 T2]: q - *) - let is_proof_modus_ponens_oeq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_MODUS_PONENS_OEQ) + let is_modus_ponens_oeq ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS_OEQ) (** Indicates whether the term is a proof for theory lemma @@ -2520,259 +3857,74 @@ struct - farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. - triangle-eq - Indicates a lemma related to the equivalence: - (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) + (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. - *) - let is_proof_theory_lemma ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_PR_TH_LEMMA) - - (** - Indicates whether the term is of a relation sort. - *) - let is_Relation ( x : expr ) = - ((lbool_of_int (Z3native.is_app x#gnc x#gno)) == L_TRUE) && - (sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno)) == RELATION_SORT) - - (** - Indicates whether the term is an relation 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. - - *) - let is_relation_store ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_STORE) - - (** - Indicates whether the term is an empty relation - *) - let is_empty_relation ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_EMPTY) - - (** - Indicates whether the term is a test for the emptiness of a relation - *) - let is_is_empty_relation ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_IS_EMPTY) - - (** - Indicates whether the term is a relational join - *) - let is_relational_join ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_JOIN) - - (** - Indicates whether the term is the union or convex hull of two relations. - The function takes two arguments. - *) - let is_relation_union ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_UNION) - - (** - Indicates whether the term is the widening of two relations - The function takes two arguments. - *) - let is_relation_widen ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_WIDEN) - - (** - Indicates whether the term is a projection of columns (provided as numbers in the parameters). - The function takes one argument. - *) - let is_relation_project ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_PROJECT) - - (** - Indicates whether the term is a relation filter - - Filter (restrict) a relation with respect to a predicate. - The first argument is a relation. - The second argument is a predicate with free de-Brujin indices - corresponding to the columns of the relation. - So the first column in the relation has index 0. - - *) - let is_relation_filter ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_FILTER) - - (** - Indicates whether the term is an intersection of a relation with the negation of another. - - Intersect the first relation with respect to negation - of the second relation (the function takes two arguments). - Logically, the specification can be described by a function - - target = filter_by_negation(pos, neg, columns) - - where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that - target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with - ( x : expr ) on the columns c1, d1, .., cN, dN. - - *) - let is_relation_negation_filter ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_NEGATION_FILTER) - - (** - Indicates whether the term is the renaming of a column in a relation - - The function takes one argument. - The parameters contain the renaming as a cycle. - - *) - let is_relation_rename ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_RENAME) - - (** - Indicates whether the term is the complement of a relation - *) - let is_relation_complement ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_COMPLEMENT) - - (** - Indicates whether the term is a relational select - - Check if a record is an element of the relation. - The function takes n+1 arguments, where the first argument is a relation, - and the remaining n arguments correspond to a record. - - *) - let is_relation_select ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_SELECT) - - (** - Indicates whether the term is a relational clone (copy) - - Create a fresh copy (clone) of a relation. - The function is logically the identity, but - in the context of a register machine allows - for terms of kind - to perform destructive updates to the first argument. - - *) - let is_relation_clone ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_RA_CLONE) - - (** - Indicates whether the term is of an array sort. - *) - let is_finite_domain ( x : expr ) = - ((lbool_of_int (Z3native.is_app x#gnc x#gno)) == L_TRUE) && - (sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno)) == FINITE_DOMAIN_SORT) - - (** - Indicates whether the term is a less than predicate over a finite domain. - *) - let is_finite_domain_lt ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_FD_LT) - - (** - The de-Burijn index of a bound variable. - - Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain - the meaning of de-Bruijn indices by indicating the compilation process from - non-de-Bruijn formulas to de-Bruijn format. - - abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) - abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) - abs1(x, x, n) = b_n - abs1(y, x, n) = y - abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) - abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) - - The last line is significant: the index of a bound variable is different depending - on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its - index. - - *) - let get_index ( x : expr ) = - if not (AST.is_var x) then - raise (Z3native.Exception "Term is not a bound variable.") - else - Z3native.get_index_value x#gnc x#gno + let is_theory_lemma ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TH_LEMMA) end -(** Integer Numerals *) -module IntNum = -struct - (** Retrieve the int value. *) - let get_int ( x : int_num ) = let (r, v) = Z3native.get_numeral_int x#gnc x#gno in - if lbool_of_int(r) == L_TRUE then v - else raise (Z3native.Exception "Conversion failed.") +(** + Parameter sets (of Solvers, Tactics, ...) - (** Returns a string representation of the numeral. *) - let to_string ( x : int_num ) = Z3native.get_numeral_string x#gnc x#gno -end - -(** Rational Numerals *) -module RatNum = -struct - - (** The numerator of a rational numeral. *) - let get_numerator ( x : rat_num ) = - (new int_num x#gc)#cnstr_obj (Z3native.get_numerator x#gnc x#gno) - - (** The denominator of a rational numeral. *) - let get_denominator ( x : rat_num ) = - (new int_num x#gc)#cnstr_obj (Z3native.get_denominator x#gnc x#gno) - - (** Returns a string representation in decimal notation. - The result has at most decimal places.*) - let to_decimal_string ( x : rat_num ) (precision : int) = - Z3native.get_numeral_decimal_string x#gnc x#gno precision - - (** Returns a string representation of the numeral. *) - let to_string ( x : rat_num ) = Z3native.get_numeral_string x#gnc x#gno -end - -(** Bit-vector numerals *) -module BitVecNum = -struct - (** Retrieve the int value. *) - let get_int ( x : bitvec_num ) = let (r, v) = Z3native.get_numeral_int x#gnc x#gno in - if lbool_of_int(r) == L_TRUE then v - else raise (Z3native.Exception "Conversion failed.") - - (** Returns a string representation of the numeral. *) - let to_string ( x : bitvec_num ) = Z3native.get_numeral_string x#gnc x#gno -end - -(** Algebraic numbers *) -module AlgebraicNum = + A Params objects represents a configuration in the form of symbol/value pairs. +*) +module Params = struct (** - Return a upper bound for a given real algebraic number. - The interval isolating the number is smaller than 1/10^. - - @param precision the precision of the result - @return A numeral Expr of sort Real + Adds a parameter setting. *) - let to_upper ( x : algebraic_num ) ( precision : int ) = - (new rat_num x#gc)#cnstr_obj (Z3native.get_algebraic_number_upper x#gnc x#gno precision) - - (** - Return a lower bound for the given real algebraic number. - The interval isolating the number is smaller than 1/10^. - - @param precision the precision of the result - @return A numeral Expr of sort Real - *) - let to_lower ( x : algebraic_num ) precision = - (new rat_num x#gc)#cnstr_obj (Z3native.get_algebraic_number_lower x#gnc x#gno precision) + let add_bool (p : params) (name : symbol) (value : bool) = + Z3native.params_set_bool p#gnc p#gno name#gno (int_of_lbool (if value then L_TRUE else L_FALSE)) - (** Returns a string representation in decimal notation. - The result has at most decimal places.*) - let to_decimal_string ( x : algebraic_num ) ( precision : int ) = - Z3native.get_numeral_decimal_string x#gnc x#gno precision + (** + Adds a parameter setting. + *) + let add_int (p : params) (name : symbol) (value : int) = + Z3native.params_set_uint p#gnc p#gno name#gno value - (** Returns a string representation of the numeral. *) - let to_string ( x : algebraic_num ) = Z3native.get_numeral_string x#gnc x#gno + (** + Adds a parameter setting. + *) + let add_double (p : params) (name : symbol) (value : float) = + Z3native.params_set_double p#gnc p#gno name#gno value + + (** + Adds a parameter setting. + *) + let add_symbol (p : params) (name : symbol) (value : symbol) = + Z3native.params_set_symbol p#gnc p#gno name#gno value#gno + + (** + Adds a parameter setting. + *) + let add_s_bool (p : params) (name : string) (value : bool) = + add_bool p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value + + (** + Adds a parameter setting. + *) + let add_s_int (p : params) (name : string) (value : int) = + add_int p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value + + (** + Adds a parameter setting. + *) + let add_s_double (p : params) (name : string) (value : float) = + add_double p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value + + (** + Adds a parameter setting. + *) + let add_s_symbol (p : params) (name : string) (value : symbol) = + add_symbol p ((new symbol p#gc)#cnstr_obj (Z3native.mk_string_symbol p#gnc name)) value + + (** + A string representation of the parameter set. + *) + let to_string (p : params) = Z3native.params_to_string p#gnc p#gno end -(** Constructors are used for datatype sorts *) -module Constructor = -struct - (** The number of fields of the constructor. *) - let get_num_fields ( x : constructor ) = x#get_n - - (** The function declaration of the constructor. *) - let get_constructor_decl ( x : constructor ) = x#constructor_decl - - (** The function declaration of the tester. *) - let get_tester_decl ( x : constructor ) = x#tester_decl - - (** The function declarations of the accessors *) - let get_accessor_decls ( x : constructor ) = x#accessor_decls -end - - -(** ParamDescrs describe sets of parameters.*) +(** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *) module ParamDescrs = struct @@ -2917,102 +4069,100 @@ struct | None -> (new apply_result x#gc)#cnstr_obj (Z3native.tactic_apply x#gnc x#gno g#gno) | Some (pn) -> (new apply_result x#gc)#cnstr_obj (Z3native.tactic_apply_ex x#gnc x#gno g#gno pn#gno) - (** Creates a solver that is implemented using the given tactic. + (** creates a solver that is implemented using the given tactic. *) let get_solver ( x : tactic ) = (new solver x#gc)#cnstr_obj (Z3native.mk_solver_from_tactic x#gnc x#gno) end - -(** Function interpretations - - A function interpretation is represented as a finite map and an 'else'. - Each entry in the finite map represents the value of a function given a set of arguments. -*) -module FuncInterp = -struct - - (** Function interpretations entries - - An Entry object represents an element in the finite map used to a function interpretation. - *) - module FuncEntry = - struct - (** - Return the (symbolic) value of this entry. - *) - let get_value ( x : func_entry ) = - create_expr x#gc (Z3native.func_entry_get_value x#gnc x#gno) - - (** - The number of arguments of the entry. - *) - let get_num_args ( x : func_entry ) = Z3native.func_entry_get_num_args x#gnc x#gno - - (** - The arguments of the function entry. - *) - let get_args ( x : func_entry ) = - let n = (get_num_args x) in - let f i = (create_expr x#gc (Z3native.func_entry_get_arg x#gnc x#gno i)) in - Array.init n f - - (** - A string representation of the function entry. - *) - let to_string ( x : func_entry ) = - let a = (get_args x) in - let f c p = (p ^ (Expr.to_string c) ^ ", ") in - "[" ^ Array.fold_right f a ((Expr.to_string (get_value x)) ^ "]]") - end - - (** - The number of entries in the function interpretation. - *) - let get_num_entries ( x: func_interp ) = Z3native.func_interp_get_num_entries x#gnc x#gno - - (** - The entries in the function interpretation - *) - let get_entries ( x : func_interp ) = - let n = (get_num_entries x) in - let f i = ((new func_entry x#gc)#cnstr_obj (Z3native.func_interp_get_entry x#gnc x#gno i)) in - Array.init n f - - (** - The (symbolic) `else' value of the function interpretation. - *) - let get_else ( x : func_interp ) = create_expr x#gc (Z3native.func_interp_get_else x#gnc x#gno) - - (** - The arity of the function interpretation - *) - let get_arity ( x : func_interp ) = Z3native.func_interp_get_arity x#gnc x#gno - - (** - A string representation of the function interpretation. - *) - let to_string ( x : func_interp ) = - let f c p = ( - let n = (FuncEntry.get_num_args c) in - p ^ - let g c p = (p ^ (Expr.to_string c) ^ ", ") in - (if n > 1 then "[" else "") ^ - (Array.fold_right - g - (FuncEntry.get_args c) - ((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", ")) - ) in - Array.fold_right f (get_entries x) ("else -> " ^ (Expr.to_string (get_else x)) ^ "]") -end - -(** Models. +(** Models A Model contains interpretations (assignments) of constants and functions. *) module Model = struct - + (** Function interpretations + + A function interpretation is represented as a finite map and an 'else'. + Each entry in the finite map represents the value of a function given a set of arguments. + *) + module FuncInterp = + struct + + (** Function interpretations entries + + An Entry object represents an element in the finite map used to a function interpretation. + *) + module FuncEntry = + struct + (** + Return the (symbolic) value of this entry. + *) + let get_value ( x : func_entry ) = + create_expr x#gc (Z3native.func_entry_get_value x#gnc x#gno) + + (** + The number of arguments of the entry. + *) + let get_num_args ( x : func_entry ) = Z3native.func_entry_get_num_args x#gnc x#gno + + (** + The arguments of the function entry. + *) + let get_args ( x : func_entry ) = + let n = (get_num_args x) in + let f i = (create_expr x#gc (Z3native.func_entry_get_arg x#gnc x#gno i)) in + Array.init n f + + (** + A string representation of the function entry. + *) + let to_string ( x : func_entry ) = + let a = (get_args x) in + let f c p = (p ^ (Expr.to_string c) ^ ", ") in + "[" ^ Array.fold_right f a ((Expr.to_string (get_value x)) ^ "]]") + end + + (** + The number of entries in the function interpretation. + *) + let get_num_entries ( x: func_interp ) = Z3native.func_interp_get_num_entries x#gnc x#gno + + (** + The entries in the function interpretation + *) + let get_entries ( x : func_interp ) = + let n = (get_num_entries x) in + let f i = ((new func_entry x#gc)#cnstr_obj (Z3native.func_interp_get_entry x#gnc x#gno i)) in + Array.init n f + + (** + The (symbolic) `else' value of the function interpretation. + *) + let get_else ( x : func_interp ) = create_expr x#gc (Z3native.func_interp_get_else x#gnc x#gno) + + (** + The arity of the function interpretation + *) + let get_arity ( x : func_interp ) = Z3native.func_interp_get_arity x#gnc x#gno + + (** + A string representation of the function interpretation. + *) + let to_string ( x : func_interp ) = + let f c p = ( + let n = (FuncEntry.get_num_args c) in + p ^ + let g c p = (p ^ (Expr.to_string c) ^ ", ") in + (if n > 1 then "[" else "") ^ + (Array.fold_right + g + (FuncEntry.get_args c) + ((if n > 1 then "]" else "") ^ " -> " ^ (Expr.to_string (FuncEntry.get_value c)) ^ ", ")) + ) in + Array.fold_right f (get_entries x) ("else -> " ^ (Expr.to_string (get_else x)) ^ "]") + end + (** Retrieves the interpretation (the assignment) of in the model. A function declaration of zero arity An expression if the function has an interpretation in the model, null otherwise. *) @@ -3093,7 +4243,7 @@ struct This function may fail if contains quantifiers, is partial (MODEL_PARTIAL enabled), or if is not well-sorted. In this case a ModelEvaluationFailedException is thrown. - + An expression When this flag is enabled, a model value will be assigned to any constant @@ -3120,7 +4270,6 @@ struct Z3 also provides an intepretation for uninterpreted sorts used in a formula. The interpretation for a sort is a finite set of distinct values. We say this finite set is the "universe" of the sort. - *) @@ -3137,8 +4286,8 @@ struct *) let sort_universe ( x : model ) ( s : sort ) = let n_univ = (new ast_vector x#gc)#cnstr_obj (Z3native.model_get_sort_universe x#gnc x#gno s#gno) in - let n = (ASTVector.get_size n_univ) in - let f i = (ASTVector.get n_univ i) in + let n = (AST.ASTVector.get_size n_univ) in + let f i = (AST.ASTVector.get n_univ i) in Array.init n f (** Conversion of models to strings. @@ -3174,84 +4323,85 @@ struct let to_string ( x : apply_result) = Z3native.apply_result_to_string x#gnc x#gno end -(** Objects that track statistical information about solvers. *) -module Statistics = -struct - - (** - Statistical data is organized into pairs of [Key, Entry], where every - Entry is either a DoubleEntry or a UIntEntry - *) - module Entry = - struct - (** The key of the entry. *) - let get_key (x : statistics_entry) = x#key - - (** The int-value of the entry. *) - let get_int (x : statistics_entry) = x#int - - (** The float-value of the entry. *) - let get_float (x : statistics_entry) = x#float - - (** True if the entry is uint-valued. *) - let is_int (x : statistics_entry) = x#is_int - - (** True if the entry is double-valued. *) - let is_float (x : statistics_entry) = x#is_float - - (** The string representation of the the entry's value. *) - let to_string_value (x : statistics_entry) = - if (is_int x) then - string_of_int (get_int x) - else if (is_float x) then - string_of_float (get_float x) - else - raise (Z3native.Exception "Unknown statistical entry type") - - (** The string representation of the entry (key and value) *) - let to_string ( x : statistics_entry ) = (get_key x) ^ ": " ^ (to_string_value x) - end - - (** A string representation of the statistical data. *) - let to_string ( x : statistics ) = Z3native.stats_to_string x#gnc x#gno - - (** The number of statistical data. *) - let get_size ( x : statistics ) = Z3native.stats_size x#gnc x#gno - - (** The data entries. *) - let get_entries ( x : statistics ) = - let n = (get_size x ) in - let f i = ( - let k = Z3native.stats_get_key x#gnc x#gno i in - if (lbool_of_int (Z3native.stats_is_uint x#gnc x#gno i)) == L_TRUE then - ((new statistics_entry)#cnstr_si k (Z3native.stats_get_uint_value x#gnc x#gno i)) - else - ((new statistics_entry)#cnstr_sd k (Z3native.stats_get_double_value x#gnc x#gno i)) - ) in - Array.init n f - - (** - The statistical counters. - *) - let get_keys ( x : statistics ) = - let n = (get_size x) in - let f i = (Z3native.stats_get_key x#gnc x#gno i) in - Array.init n f - - (** - The value of a particular statistical counter. - *) - let get ( x : statistics ) ( key : string ) = - let f p c = (if (Entry.get_key c) = key then (Some c) else p) in - Array.fold_left f None (get_entries x) - -end - (** Solvers *) module Solver = struct type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE + (** Objects that track statistical information about solvers. *) + module Statistics = + struct + + (** + Statistical data is organized into pairs of [Key, Entry], where every + Entry is either a DoubleEntry or a UIntEntry + *) + module Entry = + struct + (** The key of the entry. *) + let get_key (x : statistics_entry) = x#key + + (** The int-value of the entry. *) + let get_int (x : statistics_entry) = x#int + + (** The float-value of the entry. *) + let get_float (x : statistics_entry) = x#float + + (** True if the entry is uint-valued. *) + let is_int (x : statistics_entry) = x#is_int + + (** True if the entry is double-valued. *) + let is_float (x : statistics_entry) = x#is_float + + (** The string representation of the the entry's value. *) + let to_string_value (x : statistics_entry) = + if (is_int x) then + string_of_int (get_int x) + else if (is_float x) then + string_of_float (get_float x) + else + raise (Z3native.Exception "Unknown statistical entry type") + + (** The string representation of the entry (key and value) *) + let to_string ( x : statistics_entry ) = (get_key x) ^ ": " ^ (to_string_value x) + end + + (** A string representation of the statistical data. *) + let to_string ( x : statistics ) = Z3native.stats_to_string x#gnc x#gno + + (** The number of statistical data. *) + let get_size ( x : statistics ) = Z3native.stats_size x#gnc x#gno + + (** The data entries. *) + let get_entries ( x : statistics ) = + let n = (get_size x ) in + let f i = ( + let k = Z3native.stats_get_key x#gnc x#gno i in + if (lbool_of_int (Z3native.stats_is_uint x#gnc x#gno i)) == L_TRUE then + ((new statistics_entry)#cnstr_si k (Z3native.stats_get_uint_value x#gnc x#gno i)) + else + ((new statistics_entry)#cnstr_sd k (Z3native.stats_get_double_value x#gnc x#gno i)) + ) in + Array.init n f + + (** + The statistical counters. + *) + let get_keys ( x : statistics ) = + let n = (get_size x) in + let f i = (Z3native.stats_get_key x#gnc x#gno i) in + Array.init n f + + (** + The value of a particular statistical counter. + *) + let get ( x : statistics ) ( key : string ) = + let f p c = (if (Entry.get_key c) = key then (Some c) else p) in + Array.fold_left f None (get_entries x) + + end + + (** A string that describes all available solver parameters. *) @@ -3284,14 +4434,14 @@ struct (** Backtracks backtracking points. - Note that an exception is thrown if is not smaller than NumScopes + Note that an exception is thrown if is not smaller than NumScopes *) let pop ( x : solver ) ( n : int ) = Z3native.solver_pop x#gnc x#gno n (** Resets the Solver. - This removes all assertions from the solver. + This removes all assertions from the solver. *) let reset ( x : solver ) = Z3native.solver_reset x#gnc x#gno @@ -3307,7 +4457,7 @@ struct *) let get_num_assertions ( x : solver ) = let a = (new ast_vector x#gc)#cnstr_obj (Z3native.solver_get_assertions x#gnc x#gno) in - (ASTVector.get_size a) + (AST.ASTVector.get_size a) (** @@ -3315,8 +4465,8 @@ struct *) let get_assertions ( x : solver ) = let a = (new ast_vector x#gc)#cnstr_obj (Z3native.solver_get_assertions x#gnc x#gno) in - let n = (ASTVector.get_size a) in - let f i = ((new bool_expr x#gc)#cnstr_obj (ASTVector.get a i)#gno) in + let n = (AST.ASTVector.get_size a) in + let f i = ((new bool_expr x#gc)#cnstr_obj (AST.ASTVector.get a i)#gno) in Array.init n f (** @@ -3325,7 +4475,6 @@ struct - *) let check ( x : solver ) ( assumptions : bool_expr array option) = let r = @@ -3343,7 +4492,6 @@ struct The result is None if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled. - *) let get_model ( x : solver ) = let q = Z3native.solver_get_model x#gnc x#gno in @@ -3357,7 +4505,6 @@ struct The result is null if Check was not invoked before, if its results was not UNSATISFIABLE, or if proof production is disabled. - *) let get_proof ( x : solver ) = let q = Z3native.solver_get_proof x#gnc x#gno in @@ -3372,12 +4519,11 @@ struct The unsat core is a subset of Assertions The result is empty if Check was not invoked before, if its results was not UNSATISFIABLE, or if core production is disabled. - *) let get_unsat_core ( x : solver ) = let cn = (new ast_vector x#gc)#cnstr_obj (Z3native.solver_get_unsat_core x#gnc x#gno) in - let n = (ASTVector.get_size cn) in - let f i = (ASTVector.get cn i) in + let n = (AST.ASTVector.get_size cn) in + let f i = (AST.ASTVector.get cn i) in Array.init n f (** @@ -3418,3312 +4564,936 @@ struct end -(** The main interaction with Z3 happens via the Context module *) -module Context = -struct +(* STUFF FROM THE CONTEXT *) - (* SYMBOLS *) - - (** - Creates a new symbol using an integer. - - Not all integers can be passed to this function. - The legal range of unsigned integers is 0 to 2^30-1. - *) - let mk_symbol_int ( ctx : context ) i = - (new int_symbol ctx)#cnstr_int i - - (** Creates a new symbol using a string. *) - let mk_symbol_string ( ctx : context ) s = - (new string_symbol ctx)#cnstr_string s - - (** - Create an array of symbols. - *) - let mk_symbols_int ( ctx : context ) names = - let f elem = mk_symbol_int ( ctx : context ) elem in - (Array.map f names) - - (** - Create an array of symbols. - *) - let mk_symbols_string ( ctx : context ) names = - let f elem = mk_symbol_string ( ctx : context ) elem in - (Array.map f names) - - - (* SORTS *) - - (** - Create a new Boolean sort. - *) - let mk_bool_sort ( ctx : context ) = - (new bool_sort ctx)#cnstr_obj (Z3native.mk_bool_sort ctx#gno) - - (** - Create a new uninterpreted sort. - *) - let mk_uninterpreted_sort ( ctx : context ) (s : symbol) = - (new uninterpreted_sort ctx)#cnstr_s s - - (** - Create a new uninterpreted sort. - *) - let mk_uninterpreted_sort_s ( ctx : context ) (s : string) = - mk_uninterpreted_sort ctx ((mk_symbol_string ( ctx : context ) s) :> symbol) - - (** - Create a new integer sort. - *) - let mk_int_sort ( ctx : context ) = - (new int_sort ctx)#cnstr_obj (Z3native.mk_int_sort ctx#gno) - - (** - Create a real sort. - *) - let mk_real_sort ( ctx : context ) = - (new real_sort ctx)#cnstr_obj (Z3native.mk_real_sort ctx#gno) - - (** - Create a new bit-vector sort. - *) - let mk_bitvec_sort ( ctx : context ) size = - (new bitvec_sort ctx)#cnstr_obj (Z3native.mk_bv_sort ctx#gno size) - - (** - Create a new array sort. - *) - let mk_array_sort ( ctx : context ) domain range = - (new array_sort ctx)#cnstr_dr domain range - - (** - Create a new tuple sort. - *) - let mk_tuple_sort ( ctx : context ) name field_names field_sorts = - (new tuple_sort ctx)#cnstr_siss name (Array.length field_names) field_names field_sorts - - (** - Create a new enumeration sort. - *) - let mk_enum_sort ( ctx : context ) name enum_names = - (new enum_sort ctx)#cnstr_ss name enum_names - - (** - Create a new enumeration sort. - *) - let mk_enum_sort_s ( ctx : context ) name enum_names = - (new enum_sort ctx)#cnstr_ss - ((mk_symbol_string ( ctx : context ) name) :> symbol) - (let f e = (e :> symbol) in - (Array.map f (mk_symbols_string ( ctx : context ) enum_names)) - ) - - (** - Create a new list sort. - *) - let mk_list_sort ( ctx : context ) (name : symbol) elem_sort = - (new list_sort ctx)#cnstr_ss name elem_sort - - (** - Create a new list sort. - *) - let mk_list_sort_s ( ctx : context ) (name : string) elem_sort = - mk_list_sort ctx ((mk_symbol_string ctx name) :> symbol) elem_sort - - - (** - Create a new finite domain sort. - *) - let mk_finite_domain_sort ( ctx : context ) ( name : symbol ) size = - (new finite_domain_sort ctx)#cnstr_si name size - - (** - Create a new finite domain sort. - *) - let mk_finite_domain_sort_s ( ctx : context ) ( name : string ) size = - (new finite_domain_sort ctx)#cnstr_si ((mk_symbol_string ctx name) :> symbol) size - - (* DATATYPES *) - (** - Create a datatype constructor. - @param name constructor name - @param recognizer name of recognizer function. - @param fieldNames names of the constructor fields. - @param sorts field sorts, 0 if the field sort refers to a recursive sort. - @param sortRefs reference to datatype sort that is an argument to the constructor; - if the corresponding sort reference is 0, then the value in sort_refs should be an index - referring to one of the recursive datatypes that is declared. - *) - let mk_constructor ( ctx : context ) ( name : symbol ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array) = - (new constructor ctx)#cnstr_ssssi name recognizer field_names sorts sort_refs - - - (** - Create a datatype constructor. - @param name constructor name - @param recognizer name of recognizer function. - @param fieldNames names of the constructor fields. - @param sorts field sorts, 0 if the field sort refers to a recursive sort. - @param sortRefs reference to datatype sort that is an argument to the constructor; - if the corresponding sort reference is 0, then the value in sort_refs should be an index - referring to one of the recursive datatypes that is declared. - *) - let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array) = - mk_constructor ctx ((mk_symbol_string ctx name) :> symbol) recognizer field_names sorts sort_refs - - - (** - Create a new datatype sort. - *) - let mk_datatype_sort ( ctx : context ) ( name : symbol ) ( constructors : constructor array) = - (new datatype_sort ctx)#cnstr_sc name constructors - - (** - Create a new datatype sort. - *) - let mk_datatype_sort_s ( ctx : context ) ( name : string ) ( constructors : constructor array) = - mk_datatype_sort ctx ((mk_symbol_string ctx name) :> symbol) constructors - - (** - Create mutually recursive datatypes. - @param names names of datatype sorts - @param c list of constructors, one list per sort. - *) - let mk_datatype_sorts ( ctx : context ) ( names : symbol array ) ( c : constructor array array ) = - let n = (Array.length names) in - let f e = ( (new constructor_list ctx)#cnstr_ca e ) in - let cla = (Array.map f c) in - let (r, a) = (Z3native.mk_datatypes ctx#gno n (symbolaton names) (constructor_listaton cla)) in - let g e = ( (new datatype_sort ctx)#cnstr_obj e) in - (Array.map g r) - - (** Create mutually recursive data-types. *) - let mk_datatype_sorts_s ( ctx : context ) ( names : string array ) ( c : constructor array array ) = - mk_datatype_sorts ctx - ( - let f e = ((mk_symbol_string ctx e) :> symbol) in - Array.map f names - ) - c - -(** - - -(* FUNCTION DECLARATIONS *) -(** - Creates a new function declaration. -*) - public Func_Decl MkFunc_Decl(Symbol name, Sort[] domain, Sort range) - { - - - - - - CheckContextMatch(name); - CheckContextMatch(domain); - CheckContextMatch(range); - return new Func_Decl(this, name, domain, range); - } - -(** - Creates a new function declaration. -*) - public Func_Decl MkFunc_Decl(Symbol name, Sort domain, Sort range) - { - - - - - - CheckContextMatch(name); - CheckContextMatch(domain); - CheckContextMatch(range); - Sort[] q = new Sort[] { domain }; - return new Func_Decl(this, name, q, range); - } - -(** - Creates a new function declaration. -*) - public Func_Decl MkFunc_Decl(string name, Sort[] domain, Sort range) - { - - - - - CheckContextMatch(domain); - CheckContextMatch(range); - return new Func_Decl(this, MkSymbol(name), domain, range); - } - -(** - Creates a new function declaration. -*) - public Func_Decl MkFunc_Decl(string name, Sort domain, Sort range) - { - - - - - CheckContextMatch(domain); - CheckContextMatch(range); - Sort[] q = new Sort[] { domain }; - return new Func_Decl(this, MkSymbol(name), q, range); - } - -(** - Creates a fresh function declaration with a name prefixed with . -*) - - - let mk_Fresh_Func_Decl(string prefix, Sort[] domain, Sort range) - { - - - - - CheckContextMatch(domain); - CheckContextMatch(range); - return new Func_Decl(this, prefix, domain, range); - } - -(** - Creates a new constant function declaration. -*) - let mk_Const_Decl(Symbol name, Sort range) - { - - - - - CheckContextMatch(name); - CheckContextMatch(range); - return new Func_Decl(this, name, null, range); - } - -(** - Creates a new constant function declaration. -*) - let mk_Const_Decl(string name, Sort range) - { - - - - CheckContextMatch(range); - return new Func_Decl(this, MkSymbol(name), null, range); - } - -(** - Creates a fresh constant function declaration with a name prefixed with . -*) - - - let mk_Fresh_ConstDecl(string prefix, Sort range) - { - - - - CheckContextMatch(range); - return new Func_Decl(this, prefix, null, range); - } - - -(* BOUND VARIABLES *) -(** - Creates a new bound variable. -*) - @param index The de-Bruijn index of the variable - @param ty The sort of the variable - public Expr MkBound(uint index, Sort ty) - { - - - - return Expr.Create(this, Z3native.mk_bound(nCtx, index, ty.x#gno)); - } - - -(* QUANTIFIER PATTERNS *) -(** - Create a quantifier pattern. -*) - public Pattern MkPattern(params Expr[] terms) - { - - if (terms.Length == 0) - throw new Z3Exception("Cannot create a pattern from zero terms"); - - - - - - IntPtr[] termsNative = AST.ArrayToNative(terms); - return new Pattern(this, Z3native.mk_pattern(nCtx, (uint)terms.Length, termsNative)); - } - - -(* CONSTANTS *) -(** - Creates a new Constant of sort and named . -*) - public Expr MkConst(Symbol name, Sort range) - { - - - - - CheckContextMatch(name); - CheckContextMatch(range); - - return Expr.Create(this, Z3native.mk_const(nCtx, name.x#gno, range.x#gno)); - } - -(** - Creates a new Constant of sort and named . -*) - public Expr MkConst(string name, Sort range) - { - - - - return MkConst(MkSymbol(name), range); - } - -(** - Creates a fresh Constant of sort and a - name prefixed with . -*) - let mk_Fresh_Const(string prefix, Sort range) - { - - - - CheckContextMatch(range); - return Expr.Create(this, Z3native.mk_fresh_const(nCtx, prefix, range.x#gno)); - } - -(** - Creates a fresh constant from the Func_Decl . -*) - @param f A decl of a 0-arity function - public Expr MkConst(Func_Decl f) - { - - - - return MkApp(f); - } - -(** - Create a Boolean constant. -*) - let mk_Bool_Const(Symbol name) - { - - - - return (BoolExpr)MkConst(name, BoolSort); - } - -(** - Create a Boolean constant. -*) - let mk_Bool_Const(string name) - { - - - return (BoolExpr)MkConst(MkSymbol(name), BoolSort); - } - -(** - Creates an integer constant. -*) - let mk_Int_Const(Symbol name) - { - - - - return (IntExpr)MkConst(name, IntSort); - } - -(** - Creates an integer constant. -*) - let mk_Int_Const(string name) - { - - - - return (IntExpr)MkConst(name, IntSort); - } - -(** - Creates a real constant. -*) - let mk_Real_Const(Symbol name) - { - - - - return (RealExpr)MkConst(name, RealSort); - } - -(** - Creates a real constant. -*) - let mk_Real_Const(string name) - { - - - return (RealExpr)MkConst(name, RealSort); - } - -(** - Creates a bit-vector constant. -*) - let mk_B_VConst(Symbol name, uint size) - { - - - - return (BitVecExpr)MkConst(name, MkBitVecSort(size)); - } - -(** - Creates a bit-vector constant. -*) - let mk_B_VConst(string name, uint size) - { - - - return (BitVecExpr)MkConst(name, MkBitVecSort(size)); - } - - -(* TERMS *) -(** - Create a new function application. -*) - public Expr MkApp(Func_Decl f, params Expr[] args) - { - - - - - CheckContextMatch(f); - CheckContextMatch(args); - return Expr.Create(this, f, args); - } - -(* PROPOSITIONAL *) -(** - The true Term. -*) - public BoolExpr MkTrue ( ctx : context ) = - { - - - return new BoolExpr(this, Z3native.mk_true(nCtx)); - } - -(** - The false Term. -*) - public BoolExpr MkFalse ( ctx : context ) = - { - - - return new BoolExpr(this, Z3native.mk_false(nCtx)); - } - -(** - Creates a Boolean value. -*) - public BoolExpr MkBool(bool value) - { - - - return value ? MkTrue ( ctx : context ) = : MkFalse ( ctx : context ) =; - } - -(** - Creates the equality = . -*) - public BoolExpr MkEq(Expr x, Expr y) - { - - - - - CheckContextMatch(x); - CheckContextMatch(y); - return new BoolExpr(this, Z3native.mk_eq(nCtx, x.x#gno, y.x#gno)); - } - -(** - Creates a distinct term. -*) - public BoolExpr MkDistinct(params Expr[] args) - { - - - - - - CheckContextMatch(args); - return new BoolExpr(this, Z3native.mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); - } - -(** - Mk an expression representing not(a). -*) - public BoolExpr MkNot(BoolExpr a) - { - - - - CheckContextMatch(a); - return new BoolExpr(this, Z3native.mk_not(nCtx, a.x#gno)); - } - -(** - Create an expression representing an if-then-else: ite(t1, t2, t3). -*) - @param t1 An expression with Boolean sort - @param t2 An expression - @param t3 An expression with the same sort as - let mk_I_TE(BoolExpr t1, Expr t2, Expr t3) - { - - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - CheckContextMatch(t3); - return Expr.Create(this, Z3native.mk_ite(nCtx, t1.x#gno, t2.x#gno, t3.x#gno)); - } - -(** - Create an expression representing t1 iff t2. -*) - public BoolExpr MkIff(BoolExpr t1, BoolExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_iff(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 -> t2. -*) - public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_implies(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 xor t2. -*) - public BoolExpr MkXor(BoolExpr t1, BoolExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_xor(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t[0] and t[1] and .... -*) - public BoolExpr MkAnd(params BoolExpr[] t) - { - - - - - CheckContextMatch(t); - return new BoolExpr(this, Z3native.mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t))); - } - -(** - Create an expression representing t[0] or t[1] or .... -*) - public BoolExpr MkOr(params BoolExpr[] t) - { - - - - - CheckContextMatch(t); - return new BoolExpr(this, Z3native.mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t))); - } - - -(* ARITHMETIC *) -(** - Create an expression representing t[0] + t[1] + .... -*) - public ArithExpr MkAdd(params ArithExpr[] t) - { - - - - - CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Z3native.mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t))); - } - -(** - Create an expression representing t[0] * t[1] * .... -*) - public ArithExpr MkMul(params ArithExpr[] t) - { - - - - - CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Z3native.mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); - } - -(** - Create an expression representing t[0] - t[1] - .... -*) - public ArithExpr MkSub(params ArithExpr[] t) - { - - - - - CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Z3native.mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t))); - } - -(** - Create an expression representing -t. -*) - let mk_Unary_Minus(ArithExpr t) - { - - - - CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Z3native.mk_unary_minus(nCtx, t.x#gno)); - } - -(** - Create an expression representing t1 / t2. -*) - public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return (ArithExpr)Expr.Create(this, Z3native.mk_div(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 mod t2. -*) - The arguments must have int type. - public IntExpr MkMod(IntExpr t1, IntExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new IntExpr(this, Z3native.mk_mod(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 rem t2. -*) - The arguments must have int type. - public IntExpr MkRem(IntExpr t1, IntExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new IntExpr(this, Z3native.mk_rem(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 ^ t2. -*) - public ArithExpr MkPower(ArithExpr t1, ArithExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return (ArithExpr)Expr.Create(this, Z3native.mk_power(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 < t2 -*) - public BoolExpr MkLt(ArithExpr t1, ArithExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_lt(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 <= t2 -*) - public BoolExpr MkLe(ArithExpr t1, ArithExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_le(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 > t2 -*) - public BoolExpr MkGt(ArithExpr t1, ArithExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_gt(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an expression representing t1 >= t2 -*) - public BoolExpr MkGe(ArithExpr t1, ArithExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_ge(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Coerce an integer to a real. -*) - - There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard. - - You can take the floor of a real by creating an auxiliary integer Term k and - and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1. - The argument must be of integer sort. - - public RealExpr MkInt2Real(IntExpr t) - { - - - - CheckContextMatch(t); - return new RealExpr(this, Z3native.mk_int2real(nCtx, t.x#gno)); - } - -(** - Coerce a real to an integer. -*) - - The semantics of this function follows the SMT-LIB standard for the function to_int. - The argument must be of real sort. - - public IntExpr MkReal2Int(RealExpr t) - { - - - - CheckContextMatch(t); - return new IntExpr(this, Z3native.mk_real2int(nCtx, t.x#gno)); - } - -(** - Creates an expression that checks whether a real number is an integer. -*) - let mk_Is_Integer(RealExpr t) - { - - - - CheckContextMatch(t); - return new BoolExpr(this, Z3native.mk_is_int(nCtx, t.x#gno)); - } - - -(* BIT-VECTORS *) -(** - Bitwise negation. -*) - The argument must have a bit-vector sort. - let mk_B_VNot(BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_bvnot(nCtx, t.x#gno)); - } - -(** - Take conjunction of bits in a vector, return vector of length 1. -*) - The argument must have a bit-vector sort. - let mk_B_VRedAND(BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_bvredand(nCtx, t.x#gno)); - } - -(** - Take disjunction of bits in a vector, return vector of length 1. -*) - The argument must have a bit-vector sort. - let mk_B_VRedOR(BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_bvredor(nCtx, t.x#gno)); - } - -(** - Bitwise conjunction. -*) - The arguments must have a bit-vector sort. - let mk_B_VAND(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvand(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Bitwise disjunction. -*) - The arguments must have a bit-vector sort. - let mk_B_VOR(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvor(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Bitwise XOR. -*) - The arguments must have a bit-vector sort. - let mk_B_VXOR(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvxor(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Bitwise NAND. -*) - The arguments must have a bit-vector sort. - let mk_B_VNAND(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvnand(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Bitwise NOR. -*) - The arguments must have a bit-vector sort. - let mk_B_VNOR(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvnor(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Bitwise XNOR. -*) - The arguments must have a bit-vector sort. - let mk_B_VXNOR(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvxnor(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Standard two's complement unary minus. -*) - The arguments must have a bit-vector sort. - let mk_B_VNeg(BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_bvneg(nCtx, t.x#gno)); - } - -(** - Two's complement addition. -*) - The arguments must have the same bit-vector sort. - let mk_B_VAdd(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvadd(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Two's complement subtraction. -*) - The arguments must have the same bit-vector sort. - let mk_B_VSub(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvsub(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Two's complement multiplication. -*) - The arguments must have the same bit-vector sort. - let mk_B_VMul(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvmul(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Unsigned division. -*) - - It is defined as the floor of t1/t2 if \c t2 is - different from zero. If t2 is zero, then the result - is undefined. - The arguments must have the same bit-vector sort. - - let mk_B_VUDiv(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvudiv(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Signed division. -*) - - It is defined in the following way: - - - The \c floor of t1/t2 if \c t2 is different from zero, and t1*t2 >= 0. - - - The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 < 0. - - If t2 is zero, then the result is undefined. - The arguments must have the same bit-vector sort. - - let mk_B_VSDiv(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvsdiv(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Unsigned remainder. -*) - - It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. - If t2 is zero, then the result is undefined. - The arguments must have the same bit-vector sort. - - let mk_B_VURem(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvurem(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Signed remainder. -*) - - It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. - The most significant bit (sign) of the result is equal to the most significant bit of \c t1. - - If t2 is zero, then the result is undefined. - The arguments must have the same bit-vector sort. - - let mk_B_VSRem(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvsrem(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Two's complement signed remainder (sign follows divisor). -*) - - If t2 is zero, then the result is undefined. - The arguments must have the same bit-vector sort. - - let mk_B_VSMod(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvsmod(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Unsigned less-than -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VULT(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvult(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Two's complement signed less-than -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VSLT(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvslt(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Unsigned less-than or equal to. -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VULE(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvule(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Two's complement signed less-than or equal to. -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VSLE(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvsle(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Unsigned greater than or equal to. -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VUGE(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvuge(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Two's complement signed greater than or equal to. -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VSGE(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvsge(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Unsigned greater-than. -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VUGT(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvugt(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Two's complement signed greater-than. -*) - - The arguments must have the same bit-vector sort. - - let mk_B_VSGT(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvsgt(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Bit-vector concatenation. -*) - - The arguments must have a bit-vector sort. - - @return - The result is a bit-vector of size n1+n2, where n1 (n2) - is the size of t1 (t2). - - public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_concat(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Bit-vector extraction. -*) - - Extract the bits down to from a bitvector of - size m to yield a new bitvector of size n, where - n = high - low + 1. - The argument must have a bit-vector sort. - - public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_extract(nCtx, high, low, t.x#gno)); - } - -(** - Bit-vector sign extension. -*) - - Sign-extends the given bit-vector to the (signed) equivalent bitvector of - size m+i, where \c m is the size of the given bit-vector. - The argument must have a bit-vector sort. - - let mk_Sign_Ext(uint i, BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_sign_ext(nCtx, i, t.x#gno)); - } - -(** - Bit-vector zero extension. -*) - - Extend the given bit-vector with zeros to the (unsigned) equivalent - bitvector of size m+i, where \c m is the size of the - given bit-vector. - The argument must have a bit-vector sort. - - let mk_Zero_Ext(uint i, BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_zero_ext(nCtx, i, t.x#gno)); - } - -(** - Bit-vector repetition. -*) - - The argument must have a bit-vector sort. - - public BitVecExpr MkRepeat(uint i, BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_repeat(nCtx, i, t.x#gno)); - } - -(** - Shift left. -*) - - It is equivalent to multiplication by 2^x where \c x is the value of . - - NB. 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 arguments must have a bit-vector sort. - - let mk_B_VSHL(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvshl(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Logical shift right -*) - - It is equivalent to unsigned division by 2^x where \c x is the value of . - - NB. 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 arguments must have a bit-vector sort. - - let mk_B_VLSHR(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvlshr(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Arithmetic shift right -*) - - It is like logical shift right except that the most significant - bits of the result always copy the most significant bit of the - second argument. - - NB. 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 arguments must have a bit-vector sort. - - let mk_B_VASHR(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_bvashr(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Rotate Left. -*) - - Rotate bits of \c t to the left \c i times. - The argument must have a bit-vector sort. - - let mk_B_VRotateLeft(uint i, BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_rotate_left(nCtx, i, t.x#gno)); - } - -(** - Rotate Right. -*) - - Rotate bits of \c t to the right \c i times. - The argument must have a bit-vector sort. - - let mk_B_VRotateRight(uint i, BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_rotate_right(nCtx, i, t.x#gno)); - } - -(** - Rotate Left. -*) - - Rotate bits of to the left times. - The arguments must have the same bit-vector sort. - - let mk_B_VRotateLeft(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_ext_rotate_left(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Rotate Right. -*) - - Rotate bits of to the right times. - The arguments must have the same bit-vector sort. - - let mk_B_VRotateRight(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BitVecExpr(this, Z3native.mk_ext_rotate_right(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create an bit bit-vector from the integer argument . -*) - - NB. 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 argument must be of integer sort. - - public BitVecExpr MkInt2BV(uint n, IntExpr t) - { - - - - CheckContextMatch(t); - return new BitVecExpr(this, Z3native.mk_int2bv(nCtx, n, t.x#gno)); - } - -(** - Create an integer from the bit-vector argument . -*) - - If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. - So the result is non-negative and in the range [0..2^N-1], where - N are the number of bits in . - If \c is_signed is true, \c t1 is treated as a signed bit-vector. - - NB. 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 argument must be of bit-vector sort. - - let mk_B_V2Int(BitVecExpr t, bool signed) - { - - - - CheckContextMatch(t); - return new IntExpr(this, Z3native.mk_bv2int(nCtx, t.x#gno, (signed) ? 1 : 0)); - } - -(** - Create a predicate that checks that the bit-wise addition does not overflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvadd_no_overflow(nCtx, t1.x#gno, t2.x#gno, (isSigned) ? 1 : 0)); - } - -(** - Create a predicate that checks that the bit-wise addition does not underflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VAddNoUnderflow(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvadd_no_underflow(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create a predicate that checks that the bit-wise subtraction does not overflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VSubNoOverflow(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvsub_no_overflow(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create a predicate that checks that the bit-wise subtraction does not underflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvsub_no_underflow(nCtx, t1.x#gno, t2.x#gno, (isSigned) ? 1 : 0)); - } - -(** - Create a predicate that checks that the bit-wise signed division does not overflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VSDivNoOverflow(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvsdiv_no_overflow(nCtx, t1.x#gno, t2.x#gno)); - } - -(** - Create a predicate that checks that the bit-wise negation does not overflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VNegNoOverflow(BitVecExpr t) - { - - - - CheckContextMatch(t); - return new BoolExpr(this, Z3native.mk_bvneg_no_overflow(nCtx, t.x#gno)); - } - -(** - Create a predicate that checks that the bit-wise multiplication does not overflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvmul_no_overflow(nCtx, t1.x#gno, t2.x#gno, (isSigned) ? 1 : 0)); - } - -(** - Create a predicate that checks that the bit-wise multiplication does not underflow. -*) - - The arguments must be of bit-vector sort. - - let mk_B_VMulNoUnderflow(BitVecExpr t1, BitVecExpr t2) - { - - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new BoolExpr(this, Z3native.mk_bvmul_no_underflow(nCtx, t1.x#gno, t2.x#gno)); - } - - -(* ARRAYS *) -(** - Create an array constant. -*) - let mk_Array_Const(Symbol name, Sort domain, Sort range) - { - - - - - - return (ArrayExpr)MkConst(name, MkArraySort(domain, range)); - } - -(** - Create an array constant. -*) - let mk_Array_Const(string name, Sort domain, Sort range) - { - - - - - return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range)); - } - -(** - Array read. -*) - - The argument a is the array and i is the index - of the array that gets read. - - The node a must have an array sort [domain -> range], - and i must have the sort domain. - The sort of the result is range. - - - - public Expr MkSelect(ArrayExpr a, Expr i) - { - - - - - CheckContextMatch(a); - CheckContextMatch(i); - return Expr.Create(this, Z3native.mk_select(nCtx, a.x#gno, i.x#gno)); - } - -(** - Array update. -*) - - The node a must have an array sort [domain -> range], - i must have sort domain, - v must have sort range. The sort of the result is [domain -> range]. - The semantics of this function is given by the theory of arrays described in the SMT-LIB - standard. See http://smtlib.org for more details. - The result of this function is an array that is equal to a - (with respect to select) - on all indices except for i, where it maps to v - (and the select of a with - respect to i may be a different value). - - - - public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v) - { - - - - - - CheckContextMatch(a); - CheckContextMatch(i); - CheckContextMatch(v); - return new ArrayExpr(this, Z3native.mk_store(nCtx, a.x#gno, i.x#gno, v.x#gno)); - } - -(** - Create a constant array. -*) - - The resulting term is an array, such that a selecton an arbitrary index - produces the value v. - - - - let mk_Const_Array(Sort domain, Expr v) - { - - - - - CheckContextMatch(domain); - CheckContextMatch(v); - return new ArrayExpr(this, Z3native.mk_const_array(nCtx, domain.x#gno, v.x#gno)); - } - -(** - Maps f on the argument arrays. -*) - - Eeach element of args must be of an array sort [domain_i -> range_i]. - The function declaration f must have type range_1 .. range_n -> range. - v must have sort range. The sort of the result is [domain_i -> range]. - - - - - public ArrayExpr MkMap(Func_Decl f, params ArrayExpr[] args) - { - - - - - CheckContextMatch(f); - CheckContextMatch(args); - return (ArrayExpr)Expr.Create(this, Z3native.mk_map(nCtx, f.x#gno, AST.ArrayLength(args), AST.ArrayToNative(args))); - } - -(** - Access the array default value. -*) - - Produces the default range value, for arrays that can be represented as - finite maps with a default range value. - - let mk_Term_Array(ArrayExpr array) - { - - - - CheckContextMatch(array); - return Expr.Create(this, Z3native.mk_array_default(nCtx, array.x#gno)); - } - - -(* SETS *) -(** - Create a set type. -*) - let mk_Set_Sort(Sort ty) - { - - - - CheckContextMatch(ty); - return new SetSort(this, ty); - } - -(** - Create an empty set. -*) - let mk_Empty_Set(Sort domain) - { - - - - CheckContextMatch(domain); - return Expr.Create(this, Z3native.mk_empty_set(nCtx, domain.x#gno)); - } - -(** - Create the full set. -*) - let mk_Full_Set(Sort domain) - { - - - - CheckContextMatch(domain); - return Expr.Create(this, Z3native.mk_full_set(nCtx, domain.x#gno)); - } - -(** - Add an element to the set. -*) - let mk_Set_Add(Expr set, Expr element) - { - - - - - CheckContextMatch(set); - CheckContextMatch(element); - return Expr.Create(this, Z3native.mk_set_add(nCtx, set.x#gno, element.x#gno)); - } - - -(** - Remove an element from a set. -*) - let mk_Set_Del(Expr set, Expr element) - { - - - - - CheckContextMatch(set); - CheckContextMatch(element); - return Expr.Create(this, Z3native.mk_set_del(nCtx, set.x#gno, element.x#gno)); - } - -(** - Take the union of a list of sets. -*) - let mk_Set_Union(params Expr[] args) - { - - - - CheckContextMatch(args); - return Expr.Create(this, Z3native.mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); - } - -(** - Take the intersection of a list of sets. -*) - let mk_Set_Intersection(params Expr[] args) - { - - - - - CheckContextMatch(args); - return Expr.Create(this, Z3native.mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args))); - } - -(** - Take the difference between two sets. -*) - let mk_Set_Difference(Expr arg1, Expr arg2) - { - - - - - CheckContextMatch(arg1); - CheckContextMatch(arg2); - return Expr.Create(this, Z3native.mk_set_difference(nCtx, arg1.x#gno, arg2.x#gno)); - } - -(** - Take the complement of a set. -*) - let mk_Set_Complement(Expr arg) - { - - - - CheckContextMatch(arg); - return Expr.Create(this, Z3native.mk_set_complement(nCtx, arg.x#gno)); - } - -(** - Check for set membership. -*) - let mk_Set_Membership(Expr elem, Expr set) - { - - - - - CheckContextMatch(elem); - CheckContextMatch(set); - return Expr.Create(this, Z3native.mk_set_member(nCtx, elem.x#gno, set.x#gno)); - } - -(** - Check for subsetness of sets. -*) - let mk_Set_Subset(Expr arg1, Expr arg2) - { - - - - - CheckContextMatch(arg1); - CheckContextMatch(arg2); - return Expr.Create(this, Z3native.mk_set_subset(nCtx, arg1.x#gno, arg2.x#gno)); - } - +(** (* NUMERALS *) (* GENERAL NUMERALS *) (** - Create a Term of a given sort. + Create a Term of a given sort. *) - @param v A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*. - @param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. - @return A Term with value and sort - public Expr MkNumeral(string v, Sort ty) - { + @param v A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*. + @param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. + @return A Term with value and sort + public Expr MkNumeral(string v, Sort ty) - - - CheckContextMatch(ty); - return Expr.Create(this, Z3native.mk_numeral(nCtx, v, ty.x#gno)); - } + create_expr ctx (Z3native.mk_numeral ctx#gno v, ty#gno) (** - Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - It is slightly faster than MakeNumeral since it is not necessary to parse a string. + Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. + It is slightly faster than MakeNumeral since it is not necessary to parse a string. *) - @param v Value of the numeral - @param ty Sort of the numeral - @return A Term with value and type - public Expr MkNumeral(int v, Sort ty) - { + @param v Value of the numeral + @param ty Sort of the numeral + @return A Term with value and type + public Expr MkNumeral(int v, Sort ty) - - - CheckContextMatch(ty); - return Expr.Create(this, Z3native.mk_int(nCtx, v, ty.x#gno)); - } + create_expr ctx (Z3native.mk_int ctx#gno v, ty#gno) (** - Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - It is slightly faster than MakeNumeral since it is not necessary to parse a string. + Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. + It is slightly faster than MakeNumeral since it is not necessary to parse a string. *) - @param v Value of the numeral - @param ty Sort of the numeral - @return A Term with value and type - public Expr MkNumeral(uint v, Sort ty) - { + @param v Value of the numeral + @param ty Sort of the numeral + @return A Term with value and type + public Expr MkNumeral(uint v, Sort ty) - - - CheckContextMatch(ty); - return Expr.Create(this, Z3native.mk_unsigned_int(nCtx, v, ty.x#gno)); - } + create_expr ctx (Z3native.mk_unsigned_int ctx#gno v, ty#gno) (** - Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - It is slightly faster than MakeNumeral since it is not necessary to parse a string. + Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. + It is slightly faster than MakeNumeral since it is not necessary to parse a string. *) - @param v Value of the numeral - @param ty Sort of the numeral - @return A Term with value and type - public Expr MkNumeral(long v, Sort ty) - { + @param v Value of the numeral + @param ty Sort of the numeral + @return A Term with value and type + public Expr MkNumeral(long v, Sort ty) - - - CheckContextMatch(ty); - return Expr.Create(this, Z3native.mk_int64(nCtx, v, ty.x#gno)); - } + create_expr ctx (Z3native.mk_int64 ctx#gno v, ty#gno) (** - Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - It is slightly faster than MakeNumeral since it is not necessary to parse a string. + Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. + It is slightly faster than MakeNumeral since it is not necessary to parse a string. *) - @param v Value of the numeral - @param ty Sort of the numeral - @return A Term with value and type - public Expr MkNumeral(ulong v, Sort ty) - { + @param v Value of the numeral + @param ty Sort of the numeral + @return A Term with value and type + public Expr MkNumeral(ulong v, Sort ty) - - - CheckContextMatch(ty); - return Expr.Create(this, Z3native.mk_unsigned_int64(nCtx, v, ty.x#gno)); - } - + create_expr ctx (Z3native.mk_unsigned_int64 ctx#gno v, ty#gno) (* REALS *) (** - Create a real from a fraction. + Create a real from a fraction. *) - @param num numerator of rational. - @param den denominator of rational. - @return A Term with value / and sort Real - - public RatNum MkReal(int num, int den) - { - if (den == 0) - throw new Z3Exception("Denominator is zero"); + @param num numerator of rational. + @param den denominator of rational. + @return A Term with value / and sort Real + + public RatNum MkReal(int num, int den) + if (den == 0) + throw new Z3Exception("Denominator is zero"); - - - return new RatNum(this, Z3native.mk_real(nCtx, num, den)); - } + new RatNum(this, Z3native.mk_real ctx#gno num, den) (** - Create a real numeral. + Create a real numeral. *) - @param v A string representing the Term value in decimal notation. - @return A Term with value and sort Real - public RatNum MkReal(string v) - { + @param v A string representing the Term value in decimal notation. + @return A Term with value and sort Real + public RatNum MkReal(string v) - - return new RatNum(this, Z3native.mk_numeral(nCtx, v, RealSort.x#gno)); - } + new RatNum(this, Z3native.mk_numeral ctx#gno v, RealSort#gno) (** - Create a real numeral. + Create a real numeral. *) - @param v value of the numeral. - @return A Term with value and sort Real - public RatNum MkReal(int v) - { + @param v value of the numeral. + @return A Term with value and sort Real + public RatNum MkReal(int v) - - return new RatNum(this, Z3native.mk_int(nCtx, v, RealSort.x#gno)); - } + new RatNum(this, Z3native.mk_int ctx#gno v, RealSort#gno) (** - Create a real numeral. + Create a real numeral. *) - @param v value of the numeral. - @return A Term with value and sort Real - public RatNum MkReal(uint v) - { + @param v value of the numeral. + @return A Term with value and sort Real + public RatNum MkReal(uint v) - - return new RatNum(this, Z3native.mk_unsigned_int(nCtx, v, RealSort.x#gno)); - } + new RatNum(this, Z3native.mk_unsigned_int ctx#gno v, RealSort#gno) (** - Create a real numeral. + Create a real numeral. *) - @param v value of the numeral. - @return A Term with value and sort Real - public RatNum MkReal(long v) - { + @param v value of the numeral. + @return A Term with value and sort Real + public RatNum MkReal(long v) - - return new RatNum(this, Z3native.mk_int64(nCtx, v, RealSort.x#gno)); - } + new RatNum(this, Z3native.mk_int64 ctx#gno v, RealSort#gno) (** - Create a real numeral. + Create a real numeral. *) - @param v value of the numeral. - @return A Term with value and sort Real - public RatNum MkReal(ulong v) - { + @param v value of the numeral. + @return A Term with value and sort Real + public RatNum MkReal(ulong v) - - return new RatNum(this, Z3native.mk_unsigned_int64(nCtx, v, RealSort.x#gno)); - } - + new RatNum(this, Z3native.mk_unsigned_int64 ctx#gno v, RealSort#gno) (* INTEGERS *) (** - Create an integer numeral. + Create an integer numeral. *) - @param v A string representing the Term value in decimal notation. - public IntNum MkInt(string v) - { + @param v A string representing the Term value in decimal notation. + public IntNum MkInt(string v) - - return new IntNum(this, Z3native.mk_numeral(nCtx, v, IntSort.x#gno)); - } + new IntNum(this, Z3native.mk_numeral ctx#gno v, IntSort#gno) (** - Create an integer numeral. + Create an integer numeral. *) - @param v value of the numeral. - @return A Term with value and sort Integer - public IntNum MkInt(int v) - { + @param v value of the numeral. + @return A Term with value and sort Integer + public IntNum MkInt(int v) - - return new IntNum(this, Z3native.mk_int(nCtx, v, IntSort.x#gno)); - } + new IntNum(this, Z3native.mk_int ctx#gno v, IntSort#gno) (** - Create an integer numeral. + Create an integer numeral. *) - @param v value of the numeral. - @return A Term with value and sort Integer - public IntNum MkInt(uint v) - { + @param v value of the numeral. + @return A Term with value and sort Integer + public IntNum MkInt(uint v) - - return new IntNum(this, Z3native.mk_unsigned_int(nCtx, v, IntSort.x#gno)); - } + new IntNum(this, Z3native.mk_unsigned_int ctx#gno v, IntSort#gno) (** - Create an integer numeral. + Create an integer numeral. *) - @param v value of the numeral. - @return A Term with value and sort Integer - public IntNum MkInt(long v) - { + @param v value of the numeral. + @return A Term with value and sort Integer + public IntNum MkInt(long v) - - return new IntNum(this, Z3native.mk_int64(nCtx, v, IntSort.x#gno)); - } + new IntNum(this, Z3native.mk_int64 ctx#gno v, IntSort#gno) (** - Create an integer numeral. + Create an integer numeral. *) - @param v value of the numeral. - @return A Term with value and sort Integer - public IntNum MkInt(ulong v) - { + @param v value of the numeral. + @return A Term with value and sort Integer + public IntNum MkInt(ulong v) - - return new IntNum(this, Z3native.mk_unsigned_int64(nCtx, v, IntSort.x#gno)); - } - + new IntNum(this, Z3native.mk_unsigned_int64 ctx#gno v, IntSort#gno) (* BIT-VECTORS *) (** - Create a bit-vector numeral. + Create a bit-vector numeral. *) - @param v A string representing the value in decimal notation. - @param size the size of the bit-vector - let mk_B_V(string v, uint size) - { + @param v A string representing the value in decimal notation. + @param size the size of the bit-vector + let mk_bv_ ( ctx : context ) string v, uint size) - - return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); - } + (BitVecNum)MkNumeral(v, MkBitVecSort(size) (** - Create a bit-vector numeral. + Create a bit-vector numeral. *) - @param v value of the numeral. - @param size the size of the bit-vector - let mk_B_V(int v, uint size) - { + @param v value of the numeral. + @param size the size of the bit-vector + let mk_bv_ ( ctx : context ) int v, uint size) - - return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); - } + (BitVecNum)MkNumeral(v, MkBitVecSort(size) (** - Create a bit-vector numeral. + Create a bit-vector numeral. *) - @param v value of the numeral. - @param size the size of the bit-vector - let mk_B_V(uint v, uint size) - { + @param v value of the numeral. + @param size the size of the bit-vector + let mk_bv_ ( ctx : context ) uint v, uint size) - - return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); - } + (BitVecNum)MkNumeral(v, MkBitVecSort(size) (** - Create a bit-vector numeral. + Create a bit-vector numeral. *) - @param v value of the numeral. - @param size the size of the bit-vector - let mk_B_V(long v, uint size) - { + @param v value of the numeral. + @param size the size of the bit-vector + let mk_bv_ ( ctx : context ) long v, uint size) - - return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); - } + (BitVecNum)MkNumeral(v, MkBitVecSort(size) (** - Create a bit-vector numeral. + Create a bit-vector numeral. *) - @param v value of the numeral. - @param size the size of the bit-vector - let mk_B_V(ulong v, uint size) - { + @param v value of the numeral. + @param size the size of the bit-vector + let mk_bv_ ( ctx : context ) ulong v, uint size) + (BitVecNum)MkNumeral(v, MkBitVecSort(size) - return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); - } - - - // Numerals + // Numerals (* QUANTIFIERS *) (** - Create a universal Quantifier. + Create a universal Quantifier. + + Creates a forall formula, where is the weight, + is an array of patterns, is an array + with the sorts of the bound variables, is an array with the + 'names' of the bound variables, and is the body of the + quantifier. Quantifiers are associated with weights indicating + the importance of using the quantifier during instantiation. *) - - Creates a forall formula, where is the weight, - is an array of patterns, is an array - with the sorts of the bound variables, is an array with the - 'names' of the bound variables, and is the body of the - quantifier. Quantifiers are associated with weights indicating - the importance of using the quantifier during instantiation. - - @param sorts the sorts of the bound variables. - @param names names of the bound variables - @param body the body of the quantifier. - @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. - @param patterns array containing the patterns created using MkPattern. - @param noPatterns array containing the anti-patterns created using MkPattern. - @param quantifierID optional symbol to track quantifier. - @param skolemID optional symbol to track skolem constants. - public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - { - - - - - - - - - - - - return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); - } + @param sorts the sorts of the bound variables. + @param names names of the bound variables + @param body the body of the quantifier. + @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. + @param patterns array containing the patterns created using MkPattern. + @param noPatterns array containing the anti-patterns created using MkPattern. + @param quantifierID optional symbol to track quantifier. + @param skolemID optional symbol to track skolem constants. + public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) + new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); (** - Create a universal Quantifier. + Create a universal Quantifier. *) - public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - { + public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - - - - - - - return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); - } + new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); (** - Create an existential Quantifier. + Create an existential Quantifier. *) - - public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - { + + public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - - - - - - - - - - return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); - } + new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); (** - Create an existential Quantifier. + Create an existential Quantifier. *) - public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - { - - - - - - - return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); - } + public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) + new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); (** - Create a Quantifier. + Create a Quantifier. *) - public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - { - - - - - - - - - - - - if (universal) - return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); - else - return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); - } + public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) + if (universal) + MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); + else + MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); (** - Create a Quantifier. + Create a Quantifier. *) - public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) - { + public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) + if (universal) + MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); + else + MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); - - - - - - if (universal) - return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); - else - return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); - } - - - - // Expr + // Expr (* OPTIONS *) (** - Selects the format used for pretty-printing expressions. + Selects the format used for pretty-printing expressions. + + The default mode for pretty printing expressions is to produce + SMT-LIB style output where common subexpressions are printed + at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. + To print shared common subexpressions only once, + use the Z3_PRINT_LOW_LEVEL mode. + To print in way that conforms to SMT-LIB standards and uses let + expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. *) - - The default mode for pretty printing expressions is to produce - SMT-LIB style output where common subexpressions are printed - at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. - To print shared common subexpressions only once, - use the Z3_PRINT_LOW_LEVEL mode. - To print in way that conforms to SMT-LIB standards and uses let - expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. - - - - - - public Z3_ast_print_mode PrintMode - { - set { Z3native.set_ast_print_mode(nCtx, (uint)value); } - } - + + + + + public Z3_ast_print_mode PrintMode + + set { Z3native.set_ast_print_mode ctx#gno (uint)value); } (* SMT Files & Strings *) (** - Convert a benchmark into an SMT-LIB formatted string. + Convert a benchmark into an SMT-LIB formatted string. *) - @param name Name of the benchmark. The argument is optional. - @param logic The benchmark logic. - @param status The status string (sat, unsat, or unknown) - @param attributes Other attributes, such as source, difficulty or category. - @param assumptions Auxiliary assumptions. - @param formula Formula to be checked for consistency in conjunction with assumptions. - @return A string representation of the benchmark. - public string BenchmarkToSMTString(string name, string logic, string status, string attributes, - BoolExpr[] assumptions, BoolExpr formula) - { + @param name Name of the benchmark. The argument is optional. + @param logic The benchmark logic. + @param status The status string (sat, unsat, or unknown) + @param attributes Other attributes, such as source, difficulty or category. + @param assumptions Auxiliary assumptions. + @param formula Formula to be checked for consistency in conjunction with assumptions. + @return A string representation of the benchmark. + public string BenchmarkToSMTString(string name, string logic, string status, string attributes, + BoolExpr[] assumptions, BoolExpr formula) - - - - return Z3native.benchmark_to_smtlib_string(nCtx, name, logic, status, attributes, - (uint)assumptions.Length, AST.ArrayToNative(assumptions), - formula.x#gno); - } + Z3native.benchmark_to_smtlib_string ctx#gno name, logic, status, attributes, + (uint)assumptions.Length, AST.ArrayToNative(assumptions), + formula#gno); (** - Parse the given string using the SMT-LIB parser. + Parse the given string using the SMT-LIB parser. + + The symbol table of the parser can be initialized using the given sorts and declarations. + The symbols in the arrays and + don't need to match the names of the sorts and declarations in the arrays + and . This is a useful feature since we can use arbitrary names to + reference sorts and declarations. *) - - The symbol table of the parser can be initialized using the given sorts and declarations. - The symbols in the arrays and - don't need to match the names of the sorts and declarations in the arrays - and . This is a useful feature since we can use arbitrary names to - reference sorts and declarations. - - public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) - { - uint csn = Symbol.ArrayLength(sortNames); - uint cs = Sort.ArrayLength(sorts); - uint cdn = Symbol.ArrayLength(declNames); - uint cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Z3native.parse_smtlib_string(nCtx, str, - AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); - } + public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) + + uint csn = Symbol.ArrayLength(sortNames); + uint cs = Sort.ArrayLength(sorts); + uint cdn = Symbol.ArrayLength(declNames); + uint cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + Z3native.parse_smtlib_string ctx#gno str, + AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls) (** - Parse the given file using the SMT-LIB parser. + Parse the given file using the SMT-LIB parser. *) - - public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) - { - uint csn = Symbol.ArrayLength(sortNames); - uint cs = Sort.ArrayLength(sorts); - uint cdn = Symbol.ArrayLength(declNames); - uint cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Z3native.parse_smtlib_file(nCtx, fileName, - AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); - } + + public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) + + uint csn = Symbol.ArrayLength(sortNames); + uint cs = Sort.ArrayLength(sorts); + uint cdn = Symbol.ArrayLength(declNames); + uint cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + Z3native.parse_smtlib_file ctx#gno fileName, + AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls) (** - The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public uint NumSMTLIBFormulas { get { return Z3native.get_smtlib_num_formulas(nCtx)) + public uint NumSMTLIBFormulas { get {Z3native.get_smtlib_num_formulas ctx#gno)) (** - The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public BoolExpr[] SMTLIBFormulas - { - get - { + let[] SMTLIBFormulas + get + + uint n = NumSMTLIBFormulas; + BoolExpr[] res = new BoolExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (BoolExpr)create_expr ctx (Z3native.get_smtlib_formula ctx#gno i) + res; - uint n = NumSMTLIBFormulas; - BoolExpr[] res = new BoolExpr[n]; - for (uint i = 0; i < n; i++) - res[i] = (BoolExpr)Expr.Create(this, Z3native.get_smtlib_formula(nCtx, i)); - return res; - } - } (** - The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public uint NumSMTLIBAssumptions { get { return Z3native.get_smtlib_num_assumptions(nCtx)) + public uint NumSMTLIBAssumptions { get {Z3native.get_smtlib_num_assumptions ctx#gno)) (** - The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public BoolExpr[] SMTLIBAssumptions - { - get - { + let[] SMTLIBAssumptions + get + + uint n = NumSMTLIBAssumptions; + BoolExpr[] res = new BoolExpr[n]; + for (uint i = 0; i < n; i++) + res[i] = (BoolExpr)create_expr ctx (Z3native.get_smtlib_assumption ctx#gno i) + res; - uint n = NumSMTLIBAssumptions; - BoolExpr[] res = new BoolExpr[n]; - for (uint i = 0; i < n; i++) - res[i] = (BoolExpr)Expr.Create(this, Z3native.get_smtlib_assumption(nCtx, i)); - return res; - } - } (** - The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public uint NumSMTLIBDecls { get { return Z3native.get_smtlib_num_decls(nCtx)) + public uint NumSMTLIBDecls { get {Z3native.get_smtlib_num_decls ctx#gno)) (** - The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public Func_Decl[] SMTLIBDecls - { - get - { + public Func_Decl[] SMTLIBDecls + get + + uint n = NumSMTLIBDecls; + Func_Decl[] res = new Func_Decl[n]; + for (uint i = 0; i < n; i++) + res[i] = new Func_Decl(this, Z3native.get_smtlib_decl ctx#gno i) + res; - uint n = NumSMTLIBDecls; - Func_Decl[] res = new Func_Decl[n]; - for (uint i = 0; i < n; i++) - res[i] = new Func_Decl(this, Z3native.get_smtlib_decl(nCtx, i)); - return res; - } - } (** - The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public uint NumSMTLIBSorts { get { return Z3native.get_smtlib_num_sorts(nCtx)) + public uint NumSMTLIBSorts { get {Z3native.get_smtlib_num_sorts ctx#gno)) (** - The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. + The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) - public Sort[] SMTLIBSorts - { - get - { + public Sort[] SMTLIBSorts + get + + uint n = NumSMTLIBSorts; + Sort[] res = new Sort[n]; + for (uint i = 0; i < n; i++) + res[i] = Sort.Create(this, Z3native.get_smtlib_sort ctx#gno i) + res; - uint n = NumSMTLIBSorts; - Sort[] res = new Sort[n]; - for (uint i = 0; i < n; i++) - res[i] = Sort.Create(this, Z3native.get_smtlib_sort(nCtx, i)); - return res; - } - } (** - Parse the given string using the SMT-LIB2 parser. + Parse the given string using the SMT-LIB2 parser. *) - - @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. - public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) - { + + @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. + let ParseSMTLIB2String ( ctx : context ) string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) - - uint csn = Symbol.ArrayLength(sortNames); - uint cs = Sort.ArrayLength(sorts); - uint cdn = Symbol.ArrayLength(declNames); - uint cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - return (BoolExpr)Expr.Create(this, Z3native.parse_smtlib2_string(nCtx, str, - AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); - } + uint csn = Symbol.ArrayLength(sortNames); + uint cs = Sort.ArrayLength(sorts); + uint cdn = Symbol.ArrayLength(declNames); + uint cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + (BoolExpr)create_expr ctx (Z3native.parse_smtlib2_string ctx#gno str, + AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)) (** - Parse the given file using the SMT-LIB2 parser. + Parse the given file using the SMT-LIB2 parser. *) - - public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) - { + + let ParseSMTLIB2File ( ctx : context ) string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, Func_Decl[] decls = null) - - uint csn = Symbol.ArrayLength(sortNames); - uint cs = Sort.ArrayLength(sorts); - uint cdn = Symbol.ArrayLength(declNames); - uint cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - return (BoolExpr)Expr.Create(this, Z3native.parse_smtlib2_file(nCtx, fileName, - AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); - } - + uint csn = Symbol.ArrayLength(sortNames); + uint cs = Sort.ArrayLength(sorts); + uint cdn = Symbol.ArrayLength(declNames); + uint cd = AST.ArrayLength(decls); + if (csn != cs || cdn != cd) + throw new Z3Exception("Argument size mismatch"); + (BoolExpr)create_expr ctx (Z3native.parse_smtlib2_file ctx#gno fileName, + AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), + AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)) (* GOALS *) (** - Creates a new Goal. + Creates a new Goal. + + Note that the Context must have been created with proof generation support if + is set to true here. *) - - Note that the Context must have been created with proof generation support if - is set to true here. - - @param models Indicates whether model generation should be enabled. - @param unsatCores Indicates whether unsat core generation should be enabled. - @param proofs Indicates whether proof generation should be enabled. - public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false) - { + @param models Indicates whether model generation should be enabled. + @param unsatCores Indicates whether unsat core generation should be enabled. + @param proofs Indicates whether proof generation should be enabled. + public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false) - - return new Goal(this, models, unsatCores, proofs); - } - + new Goal(this, models, unsatCores, proofs); (* PARAMETERSETS *) (** - Creates a new ParameterSet. + Creates a new ParameterSet. *) - public Params MkParams ( ctx : context ) = - { + public Params MkParams ( ctx : context ) = - - return new Params(this); - } - + new Params(this); (* TACTICS *) (** - The number of supported tactics. + The number of supported tactics. *) - public uint NumTactics - { - get { return Z3native.get_num_tactics(nCtx); } - } + public uint NumTactics + + get {Z3native.get_num_tactics ctx#gno); } (** - The names of all supported tactics. + The names of all supported tactics. *) - public string[] TacticNames - { - get - { + public string[] TacticNames + get + + uint n = NumTactics; + string[] res = new string[n]; + for (uint i = 0; i < n; i++) + res[i] = Z3native.get_tactic_name ctx#gno i); + res; - uint n = NumTactics; - string[] res = new string[n]; - for (uint i = 0; i < n; i++) - res[i] = Z3native.get_tactic_name(nCtx, i); - return res; - } - } (** - Returns a string containing a description of the tactic with the given name. + Returns a string containing a description of the tactic with the given name. *) - public string TacticDescription(string name) - { + public string TacticDescription(string name) - - return Z3native.tactic_get_descr(nCtx, name); - } + Z3native.tactic_get_descr ctx#gno name); (** - Creates a new Tactic. + Creates a new Tactic. *) - public Tactic MkTactic(string name) - { + public Tactic MkTactic(string name) - - return new Tactic(this, name); - } + new Tactic(this, name); (** - Create a tactic that applies to a Goal and - then to every subgoal produced by . + Create a tactic that applies to a Goal and + then to every subgoal produced by . *) - public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts) - { + public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts) + IntPtr last = IntPtr.Zero; + if (ts != null && ts.Length > 0) + last = ts[ts.Length - 1]#gno; + for (int i = ts.Length - 2; i >= 0; i--) + last = Z3native.tactic_and_then ctx#gno ts[i]#gno last); + if (last != IntPtr.Zero) + last = Z3native.tactic_and_then ctx#gno t2#gno last); + new Tactic(this, Z3native.tactic_and_then ctx#gno t1#gno last) - - CheckContextMatch(t1); - CheckContextMatch(t2); - CheckContextMatch(ts); - - IntPtr last = IntPtr.Zero; - if (ts != null && ts.Length > 0) - { - last = ts[ts.Length - 1].x#gno; - for (int i = ts.Length - 2; i >= 0; i--) - last = Z3native.tactic_and_then(nCtx, ts[i].x#gno, last); - } - if (last != IntPtr.Zero) - { - last = Z3native.tactic_and_then(nCtx, t2.x#gno, last); - return new Tactic(this, Z3native.tactic_and_then(nCtx, t1.x#gno, last)); - } - else - return new Tactic(this, Z3native.tactic_and_then(nCtx, t1.x#gno, t2.x#gno)); - } + else + new Tactic(this, Z3native.tactic_and_then ctx#gno t1#gno t2#gno) (** - Create a tactic that applies to a Goal and - then to every subgoal produced by . + Create a tactic that applies to a Goal and + then to every subgoal produced by . + + Shorthand for AndThen. *) - - Shorthand for AndThen. - - public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts) - { + public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts) - - - - - return AndThen(t1, t2, ts); - } + AndThen(t1, t2, ts); (** - Create a tactic that first applies to a Goal and - if it fails then returns the result of applied to the Goal. + Create a tactic that first applies to a Goal and + if it fails then returns the result of applied to the Goal. *) - public Tactic OrElse(Tactic t1, Tactic t2) - { + public Tactic OrElse(Tactic t1, Tactic t2) - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new Tactic(this, Z3native.tactic_or_else(nCtx, t1.x#gno, t2.x#gno)); - } + new Tactic(this, Z3native.tactic_or_else ctx#gno t1#gno t2#gno) (** - Create a tactic that applies to a goal for milliseconds. + Create a tactic that applies to a goal for milliseconds. + + If does not terminate within milliseconds, then it fails. *) - - If does not terminate within milliseconds, then it fails. - - public Tactic TryFor(Tactic t, uint ms) - { + public Tactic TryFor(Tactic t, uint ms) - - - CheckContextMatch(t); - return new Tactic(this, Z3native.tactic_try_for(nCtx, t.x#gno, ms)); - } + new Tactic(this, Z3native.tactic_try_for ctx#gno t#gno ms) (** - Create a tactic that applies to a given goal if the probe - evaluates to true. + Create a tactic that applies to a given goal if the probe + evaluates to true. + + If evaluates to false, then the new tactic behaves like the skip tactic. *) - - If evaluates to false, then the new tactic behaves like the skip tactic. - - public Tactic When(Probe p, Tactic t) - { + public Tactic When(Probe p, Tactic t) - - - - CheckContextMatch(t); - CheckContextMatch(p); - return new Tactic(this, Z3native.tactic_when(nCtx, p.x#gno, t.x#gno)); - } + new Tactic(this, Z3native.tactic_when ctx#gno p#gno t#gno) (** - Create a tactic that applies to a given goal if the probe - evaluates to true and otherwise. + Create a tactic that applies to a given goal if the probe + evaluates to true and otherwise. *) - public Tactic Cond(Probe p, Tactic t1, Tactic t2) - { + public Tactic Cond(Probe p, Tactic t1, Tactic t2) - - - - - CheckContextMatch(p); - CheckContextMatch(t1); - CheckContextMatch(t2); - return new Tactic(this, Z3native.tactic_cond(nCtx, p.x#gno, t1.x#gno, t2.x#gno)); - } + new Tactic(this, Z3native.tactic_cond ctx#gno p#gno t1#gno t2#gno) (** - Create a tactic that keeps applying until the goal is not - modified anymore or the maximum number of iterations is reached. + Create a tactic that keeps applying until the goal is not + modified anymore or the maximum number of iterations is reached. *) - public Tactic Repeat(Tactic t, uint max = uint.MaxValue) - { + public Tactic Repeat(Tactic t, uint max = uint.MaxValue) - - - CheckContextMatch(t); - return new Tactic(this, Z3native.tactic_repeat(nCtx, t.x#gno, max)); - } + new Tactic(this, Z3native.tactic_repeat ctx#gno t#gno max) (** - Create a tactic that just returns the given goal. + Create a tactic that just returns the given goal. *) - public Tactic Skip ( ctx : context ) = - { + public Tactic Skip ( ctx : context ) = - - return new Tactic(this, Z3native.tactic_skip(nCtx)); - } + new Tactic(this, Z3native.tactic_skip ctx#gno) (** - Create a tactic always fails. + Create a tactic always fails. *) - public Tactic Fail ( ctx : context ) = - { + public Tactic Fail ( ctx : context ) = - - return new Tactic(this, Z3native.tactic_fail(nCtx)); - } + new Tactic(this, Z3native.tactic_fail ctx#gno) (** - Create a tactic that fails if the probe evaluates to false. + Create a tactic that fails if the probe evaluates to false. *) - public Tactic FailIf(Probe p) - { + public Tactic FailIf(Probe p) - - - CheckContextMatch(p); - return new Tactic(this, Z3native.tactic_fail_if(nCtx, p.x#gno)); - } + new Tactic(this, Z3native.tactic_fail_if ctx#gno p#gno) (** - Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) - or trivially unsatisfiable (i.e., contains `false'). + Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) + or trivially unsatisfiable (i.e., contains `false'). *) - public Tactic FailIfNotDecided ( ctx : context ) = - { + public Tactic FailIfNotDecided ( ctx : context ) = - - return new Tactic(this, Z3native.tactic_fail_if_not_decided(nCtx)); - } + new Tactic(this, Z3native.tactic_fail_if_not_decided ctx#gno) (** - Create a tactic that applies using the given set of parameters . + Create a tactic that applies using the given set of parameters . *) - public Tactic UsingParams(Tactic t, Params p) - { + public Tactic UsingParams(Tactic t, Params p) - - - - CheckContextMatch(t); - CheckContextMatch(p); - return new Tactic(this, Z3native.tactic_using_params(nCtx, t.x#gno, p.x#gno)); - } + new Tactic(this, Z3native.tactic_using_params ctx#gno t#gno p#gno) (** - Create a tactic that applies using the given set of parameters . -*) - Alias for UsingParams - public Tactic With(Tactic t, Params p) - { + Create a tactic that applies using the given set of parameters . + Alias for UsingParams*) + public Tactic With(Tactic t, Params p) - - - - return UsingParams(t, p); - } + UsingParams(t, p); (** - Create a tactic that applies the given tactics in parallel. + Create a tactic that applies the given tactics in parallel. *) - public Tactic ParOr(params Tactic[] t) - { + public Tactic ParOr(params Tactic[] t) - - - CheckContextMatch(t); - return new Tactic(this, Z3native.tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); - } + new Tactic(this, Z3native.tactic_par_or ctx#gno Tactic.ArrayLength(t), Tactic.ArrayToNative(t)) (** - Create a tactic that applies to a given goal and then - to every subgoal produced by . The subgoals are processed in parallel. + Create a tactic that applies to a given goal and then + to every subgoal produced by . The subgoals are processed in parallel. *) - public Tactic ParAndThen(Tactic t1, Tactic t2) - { + public Tactic ParAndThen(Tactic t1, Tactic t2) - - - - CheckContextMatch(t1); - CheckContextMatch(t2); - return new Tactic(this, Z3native.tactic_par_and_then(nCtx, t1.x#gno, t2.x#gno)); - } + new Tactic(this, Z3native.tactic_par_and_then ctx#gno t1#gno t2#gno) (** - Interrupt the execution of a Z3 procedure. + Interrupt the execution of a Z3 procedure. *) - This procedure can be used to interrupt: solvers, simplifiers and tactics. - public void Interrupt ( ctx : context ) = - { - Z3native.interrupt(nCtx); - } - + This procedure can be used to interrupt: solvers, simplifiers and tactics. + public void Interrupt ( ctx : context ) = + + Z3native.interrupt ctx#gno); (* PROBES *) (** - The number of supported Probes. + The number of supported Probes. *) - public uint NumProbes - { - get { return Z3native.get_num_probes(nCtx); } - } + public uint NumProbes + + get {Z3native.get_num_probes ctx#gno); } (** - The names of all supported Probes. + The names of all supported Probes. *) - public string[] ProbeNames - { - get - { + public string[] ProbeNames + get + + uint n = NumProbes; + string[] res = new string[n]; + for (uint i = 0; i < n; i++) + res[i] = Z3native.get_probe_name ctx#gno i); + res; - uint n = NumProbes; - string[] res = new string[n]; - for (uint i = 0; i < n; i++) - res[i] = Z3native.get_probe_name(nCtx, i); - return res; - } - } (** - Returns a string containing a description of the probe with the given name. + Returns a string containing a description of the probe with the given name. *) - public string ProbeDescription(string name) - { + public string ProbeDescription(string name) - - return Z3native.probe_get_descr(nCtx, name); - } + Z3native.probe_get_descr ctx#gno name); (** - Creates a new Probe. + Creates a new Probe. *) - public Probe MkProbe(string name) - { + public Probe MkProbe(string name) - - return new Probe(this, name); - } + new Probe(this, name); (** - Create a probe that always evaluates to . + Create a probe that always evaluates to . *) - public Probe Const(double val) - { + public Probe Const(double val) - - return new Probe(this, Z3native.probe_const(nCtx, val)); - } + new Probe(this, Z3native.probe_const ctx#gno val) (** - Create a probe that evaluates to "true" when the value returned by - is less than the value returned by + Create a probe that evaluates to "true" when the value returned by + is less than the value returned by *) - public Probe Lt(Probe p1, Probe p2) - { + public Probe Lt(Probe p1, Probe p2) - - - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Z3native.probe_lt(nCtx, p1.x#gno, p2.x#gno)); - } + new Probe(this, Z3native.probe_lt ctx#gno p1#gno p2#gno) (** - Create a probe that evaluates to "true" when the value returned by - is greater than the value returned by + Create a probe that evaluates to "true" when the value returned by + is greater than the value returned by *) - public Probe Gt(Probe p1, Probe p2) - { + public Probe Gt(Probe p1, Probe p2) - - - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Z3native.probe_gt(nCtx, p1.x#gno, p2.x#gno)); - } + new Probe(this, Z3native.probe_gt ctx#gno p1#gno p2#gno) (** - Create a probe that evaluates to "true" when the value returned by - is less than or equal the value returned by + Create a probe that evaluates to "true" when the value returned by + is less than or equal the value returned by *) - public Probe Le(Probe p1, Probe p2) - { + public Probe Le(Probe p1, Probe p2) - - - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Z3native.probe_le(nCtx, p1.x#gno, p2.x#gno)); - } + new Probe(this, Z3native.probe_le ctx#gno p1#gno p2#gno) (** - Create a probe that evaluates to "true" when the value returned by - is greater than or equal the value returned by + Create a probe that evaluates to "true" when the value returned by + is greater than or equal the value returned by *) - public Probe Ge(Probe p1, Probe p2) - { + public Probe Ge(Probe p1, Probe p2) - - - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Z3native.probe_ge(nCtx, p1.x#gno, p2.x#gno)); - } + new Probe(this, Z3native.probe_ge ctx#gno p1#gno p2#gno) (** - Create a probe that evaluates to "true" when the value returned by - is equal to the value returned by + Create a probe that evaluates to "true" when the value returned by + is equal to the value returned by *) - public Probe Eq(Probe p1, Probe p2) - { + public Probe Eq(Probe p1, Probe p2) - - - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Z3native.probe_eq(nCtx, p1.x#gno, p2.x#gno)); - } + new Probe(this, Z3native.probe_eq ctx#gno p1#gno p2#gno) (** - Create a probe that evaluates to "true" when the value - and evaluate to "true". + Create a probe that evaluates to "true" when the value + and evaluate to "true". *) - public Probe And(Probe p1, Probe p2) - { + public Probe And(Probe p1, Probe p2) - - - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Z3native.probe_and(nCtx, p1.x#gno, p2.x#gno)); - } + new Probe(this, Z3native.probe_and ctx#gno p1#gno p2#gno) (** - Create a probe that evaluates to "true" when the value - or evaluate to "true". + Create a probe that evaluates to "true" when the value + or evaluate to "true". *) - public Probe Or(Probe p1, Probe p2) - { + public Probe Or(Probe p1, Probe p2) - - - - CheckContextMatch(p1); - CheckContextMatch(p2); - return new Probe(this, Z3native.probe_or(nCtx, p1.x#gno, p2.x#gno)); - } + new Probe(this, Z3native.probe_or ctx#gno p1#gno p2#gno) (** - Create a probe that evaluates to "true" when the value - does not evaluate to "true". + Create a probe that evaluates to "true" when the value + does not evaluate to "true". *) - public Probe Not(Probe p) - { + public Probe Not(Probe p) - - - CheckContextMatch(p); - return new Probe(this, Z3native.probe_not(nCtx, p.x#gno)); - } - + new Probe(this, Z3native.probe_not ctx#gno p#gno) (* SOLVERS *) (** - Creates a new (incremental) solver. -*) - - This solver also uses a set of builtin tactics for handling the first - check-sat command, and check-sat commands that take more than a given - number of milliseconds to be solved. - - public Solver MkSolver(Symbol logic = null) - { + Creates a new (incremental) solver. + + This solver also uses a set of builtin tactics for handling the first + check-sat command, and check-sat commands that take more than a given + number of milliseconds to be solved. +*) + public Solver MkSolver(Symbol logic = null) - - if (logic == null) - return new Solver(this, Z3native.mk_solver(nCtx)); - else - return new Solver(this, Z3native.mk_solver_for_logic(nCtx, logic.x#gno)); - } + if (logic == null) + new Solver(this, Z3native.mk_solver ctx#gno) + else + new Solver(this, Z3native.mk_solver_for_logic ctx#gno logic#gno) (** - Creates a new (incremental) solver. + Creates a new (incremental) solver. *) - - public Solver MkSolver(string logic) - { + + public Solver MkSolver(string logic) - - return MkSolver(MkSymbol(logic)); - } + MkSolver(MkSymbol(logic) (** - Creates a new (incremental) solver. + Creates a new (incremental) solver. *) - let mk_Simple_Solver ( ctx : context ) = - { + let mk_Simple_Solver ( ctx : context ) ctx : context ) = - - return new Solver(this, Z3native.mk_simple_solver(nCtx)); - } + new Solver(this, Z3native.mk_simple_solver ctx#gno) (** - Creates a solver that is implemented using the given tactic. + Creates a solver that is implemented using the given tactic. + + The solver supports the commands Push and Pop, but it + will always solve each check from scratch. *) - - The solver supports the commands Push and Pop, but it - will always solve each check from scratch. - - public Solver MkSolver(Tactic t) - { + public Solver MkSolver(Tactic t) - - - return new Solver(this, Z3native.mk_solver_from_tactic(nCtx, t.x#gno)); - } - + new Solver(this, Z3native.mk_solver_from_tactic ctx#gno t#gno) (* FIXEDPOINTS *) (** - Create a Fixedpoint context. + Create a Fixedpoint context. *) - public Fixedpoint MkFixedpoint ( ctx : context ) = - { - - - return new Fixedpoint(this); - } - + public Fixedpoint MkFixedpoint ( ctx : context ) = + new Fixedpoint(this); (* MISCELLANEOUS *) (** - Wraps an AST. + Wraps an AST. *) - This function is used for transitions between native and - managed objects. Note that must be a - native object obtained from Z3 (e.g., through ) - and that it must have a correct reference count (see e.g., - . - - @param nativeObject The native pointer to wrap. - public AST WrapAST(IntPtr nativeObject) - { + This function is used for transitions between native and + managed objects. Note that must be a + native object obtained from Z3 (e.g., through ) + and that it must have a correct reference count (see e.g., + . + + @param nativeObject The native pointer to wrap. + public AST WrapAST(IntPtr nativeObject) - return AST.Create(this, nativeObject); - } + AST.Create(this, nativeObject); (** - Unwraps an AST. + Unwraps an AST. *) - This function is used for transitions between native and - managed objects. It returns the native pointer to the AST. Note that - AST objects are reference counted and unwrapping an AST disables automatic - reference counting, i.e., all references to the IntPtr that is returned - must be handled externally and through native calls (see e.g., - ). - - @param a The AST to unwrap. - public IntPtr UnwrapAST(AST a) - { - return a.x#gno; - } + This function is used for transitions between native and + managed objects. It returns the native pointer to the AST. Note that + AST objects are reference counted and unwrapping an AST disables automatic + reference counting, i.e., all references to the IntPtr that is returned + must be handled externally and through native calls (see e.g., + ). + + @param a The AST to unwrap. + public IntPtr UnwrapAST(AST a) + + a#gno; (** - Return a string describing all available parameters to Expr.Simplify. + a string describing all available parameters to Expr.Simplify. *) - public string SimplifyHelp ( ctx : context ) = - { + public string SimplifyHelp ( ctx : context ) = - - return Z3native.simplify_get_help(nCtx); - } + Z3native.simplify_get_help ctx#gno); (** - Retrieves parameter descriptions for simplifier. + Retrieves parameter descriptions for simplifier. *) - public ParamDescrs SimplifyParameterDescriptions - { - get { return new ParamDescrs(this, Z3native.simplify_get_param_descrs(nCtx)); } - } + public ParamDescrs SimplifyParameterDescriptions + + get {new ParamDescrs(this, Z3native.simplify_get_param_descrs ctx#gno)); } (** - Enable/disable printing of warning messages to the console. + Enable/disable printing of warning messages to the console. *) - Note that this function is static and effects the behaviour of - all contexts globally. - public static void ToggleWarningMessages(bool enabled) - { - Z3native.toggle_warning_messages((enabled) ? 1 : 0); - } - + Note that this function is static and effects the behaviour of + all contexts globally. + public static void ToggleWarningMessages(bool enabled) + + Z3native.toggle_warning_messages((enabled) ? 1 : 0); (* ERROR HANDLING *) - //(** - //A delegate which is executed when an error is raised. - //*) - // - //Note that it is possible for memory leaks to occur if error handlers - //throw exceptions. - // - //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString); +(** + A delegate which is executed when an error is raised. + + Note that it is possible for memory leaks to occur if error handlers + throw exceptions. +*) + public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString); - //(** - //The OnError event. - //*) - //public event ErrorHandler OnError = null; - +(** + The OnError event. +*) + public event ErrorHandler OnError = null; (* PARAMETERS *) (** - Update a mutable configuration parameter. + Update a mutable configuration parameter. + + The list of all configuration parameters can be obtained using the Z3 executable: + z3.exe -ini? + Only a few configuration parameters are mutable once the context is created. + An exception is thrown when trying to modify an immutable parameter. *) - - The list of all configuration parameters can be obtained using the Z3 executable: - z3.exe -ini? - Only a few configuration parameters are mutable once the context is created. - An exception is thrown when trying to modify an immutable parameter. - - - public void UpdateParamValue(string id, string value) - { - Z3native.update_param_value(nCtx, id, value); - } + + public void UpdateParamValue(string id, string value) + + Z3native.update_param_value ctx#gno id, value); (** - Get a configuration parameter. + Get a configuration parameter. + + Returns null if the parameter value does not exist. + *) - - Returns null if the parameter value does not exist. - - - public string GetParamValue(string id) - { - IntPtr res = IntPtr.Zero; - int r = Z3native.get_param_value(nCtx, id, out res); - if (r == (int)Z3_lbool.Z3_L_FALSE) - return null; - else - return Marshal.PtrToStringAnsi(res); - } + public string GetParamValue(string id) - + IntPtr res = IntPtr.Zero; + int r = Z3native.get_param_value ctx#gno id, out res); + if (r == (int)Z3_lbool.L_FALSE) + null; + else + Marshal.PtrToStringAnsi(res); (* INTERNAL *) - internal IntPtr m_ctx = IntPtr.Zero; - internal Z3native.error_handler m_n_err_handler = null; - internal IntPtr nCtx { get { return m_ctx) + internal IntPtr m_ctx = IntPtr.Zero; + internal Z3native.error_handler m_n_err_handler = null; + internal IntPtr nCtx { get {m_ctx) - internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode) - { - // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors. - } + internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode) + + Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors. + + internal void InitContext ( ctx : context ) = + + PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT; + m_n_err_handler = new Z3native.error_handler(NativeErrorHandler); keep reference so it doesn't get collected. + Z3native.set_error_handler(m_ctx, m_n_err_handler); + GC.SuppressFinalize(this); - internal void InitContext ( ctx : context ) = - { - PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT; - m_n_err_handler = new Z3native.error_handler(NativeErrorHandler); // keep reference so it doesn't get collected. - Z3native.set_error_handler(m_ctx, m_n_err_handler); - GC.SuppressFinalize(this); - } *) -end +