From 7b51dc9bdd06e54b65229bdee9914367b665b23b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 4 Feb 2013 21:18:25 +0000 Subject: [PATCH] Checkpoint. Signed-off-by: Christoph M. Wintersteiger --- src/api/ml/z3.ml | 2989 ++++++++++++++++++++++++---------------------- 1 file changed, 1544 insertions(+), 1445 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index f5c3e3d82..0e47912ae 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -7,6 +7,51 @@ open Z3enums +(** Interaction logging for Z3 + + Note that this is a global, static log and if multiple Context + objects are created, it logs the interaction with all of them. *) +module Log = +struct + (** Open an interaction log file. + @param filename the name of the file to open. + @return True if opening the log file succeeds, false otherwise. + *) + (* CMW: "open" seems to be a reserved keyword? *) + let open_ filename = ((lbool_of_int (Z3native.open_log filename)) == L_TRUE) + + (** Closes the interaction log. *) + let close = Z3native.close_log + + (** Appends a user-provided string to the interaction log. + @param s the string to append*) + let append s = Z3native.append_log s +end + +(** Version information *) +module Version = +struct + (** The major version. *) + let major = let (x, _, _, _) = Z3native.get_version in x + + (** The minor version. *) + let minor = let (_, x, _, _) = Z3native.get_version in x + + (** The build version. *) + let build = let (_, _, x, _) = Z3native.get_version in x + + (** The revision. *) + let revision = let (_, _, _, x) = Z3native.get_version in x + + (** A string representation of the version information. *) + let to_string = + let (mj, mn, bld, rev) = Z3native.get_version in + string_of_int mj ^ "." ^ + string_of_int mn ^ "." ^ + string_of_int bld ^ "." ^ + string_of_int rev ^ "." +end + (**/**) (* Some helpers. *) @@ -40,7 +85,7 @@ let context_dispose ctx = (* re-queue for finalization? *) ) -let context_cnstr settings = +let context_create settings = let cfg = Z3native.mk_config in let f e = (Z3native.set_param_value cfg (fst e) (snd e)) in (List.iter f settings) ; @@ -85,7 +130,7 @@ let context_gno ctx = ctx.m_n_ctx *) let mk_context ( cfg : ( string * string ) list ) = - context_cnstr cfg + context_create cfg (**/**) @@ -165,7 +210,7 @@ let z3obj_dispose o = ) ; o.m_n_obj <- null -let z3obj_cnstr o = +let z3obj_create o = let f = fun o -> (z3obj_dispose o) in Gc.finalise f o @@ -184,44 +229,51 @@ struct type int_symbol = z3_native_object (** String symbol objects *) - and string_symbol = z3_native_object + type string_symbol = z3_native_object - and symbol = - | IntSymbol of int_symbol - | StringSymbol of string_symbol + (** Symbol Objects *) + type symbol = + | S_Int of int_symbol + | S_Str of string_symbol (**/**) - let cnstr_i ( ctx : context ) ( no : Z3native.ptr ) = + let create_i ( ctx : context ) ( no : Z3native.ptr ) = let res : int_symbol = { m_ctx = ctx ; m_n_obj = null ; inc_ref = z3obj_nil_ref ; dec_ref = z3obj_nil_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res - let cnstr_s ( ctx : context ) ( no : Z3native.ptr ) = + + let create_s ( ctx : context ) ( no : Z3native.ptr ) = let res : string_symbol = { m_ctx = ctx ; m_n_obj = null ; inc_ref = z3obj_nil_ref ; dec_ref = z3obj_nil_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res + + let gc ( x : symbol ) = + match x with + | S_Int(n) -> (z3obj_gc n) + | S_Str(n) -> (z3obj_gc n) let gnc ( x : symbol ) = match x with - | IntSymbol(n) -> (z3obj_gnc n) - | StringSymbol(n) -> (z3obj_gnc n) + | S_Int(n) -> (z3obj_gnc n) + | S_Str(n) -> (z3obj_gnc n) let gno ( x : symbol ) = match x with - | IntSymbol(n) -> (z3obj_gno n) - | StringSymbol(n) -> (z3obj_gno n) + | S_Int(n) -> (z3obj_gno n) + | S_Str(n) -> (z3obj_gno n) let create ( ctx : context ) ( no : Z3native.ptr ) = match (symbol_kind_of_int (Z3native.get_symbol_kind (context_gno ctx) no)) with - | INT_SYMBOL -> IntSymbol (cnstr_i ctx no) - | STRING_SYMBOL -> StringSymbol (cnstr_s ctx no) + | INT_SYMBOL -> S_Int (create_i ctx no) + | STRING_SYMBOL -> S_Str (create_s ctx no) let aton a = let f e = (gno e) in @@ -256,11 +308,11 @@ struct The legal range of unsigned integers is 0 to 2^30-1. *) let mk_int ( ctx : context ) ( i : int ) = - IntSymbol (cnstr_i ctx (Z3native.mk_int_symbol (context_gno ctx) i)) + S_Int (create_i ctx (Z3native.mk_int_symbol (context_gno ctx) i)) (** Creates a new symbol using a string. *) let mk_string ( ctx : context ) ( s : string ) = - StringSymbol (cnstr_s ctx (Z3native.mk_string_symbol (context_gno ctx) s)) + S_Str (create_s ctx (Z3native.mk_string_symbol (context_gno ctx) s)) (** Create an array of symbols. *) let mk_ints ( ctx : context ) ( names : int array ) = @@ -273,853 +325,47 @@ struct (Array.map f names) end -(**/**) - -(** AST objects *) -class ast ctx = -object (self) - inherit z3object ctx None as super (* CMW: derive from icomparable? *) - method cnstr_obj obj = (self#sno ctx obj) ; self - - method incref nc o = Z3native.inc_ref nc o - method decref nc o = Z3native.dec_ref nc o -end - -let astaton (a : ast array) = - let f (e : ast) = e#gno in - Array.map f a - -(** Sort objects *) -class sort ctx = -object (self) - inherit ast ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -let sortaton (a : sort array) = - let f (e : sort) = e#gno in - Array.map f a - -(** Arithmetic sort objects, i.e., Int or Real. *) -class arith_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Array sorts objects *) -class array_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_dr (domain : sort) (range : sort) = (self#sno ctx (Z3native.mk_array_sort (context_gno ctx) domain#gno range#gno)) ; self -end - -(** Bit-vector sort objects *) -class bitvec_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Boolean sort objects *) -class bool_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Int sort objects *) -class int_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Real sort objects *) -class real_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Uninterpreted sort objects *) -class uninterpreted_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_s (s : Symbol.symbol) = (self #sno ctx (Z3native.mk_uninterpreted_sort (context_gno ctx) (Symbol.gno s))) ; self -end - -(** Finite domain sort objects *) -class finite_domain_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_si (s : Symbol.symbol) ( sz : int )= (self #sno ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno s) sz)) ; self -end - -(** Relation sort objects *) -class relation_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Set sort objects *) -class set_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_s (s : sort) = (self#sno ctx s#gno) ; self -end - -(** Tuple sort objects *) -class tuple_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_siss (name : Symbol.symbol) (num_fields: int) (field_names : Symbol.symbol array) (field_sorts : sort array) = - let (x,_,_) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) num_fields (Symbol.aton field_names) (astaton field_sorts)) in - (self#sno ctx x) ; - self -end - - -(** Function declaration objects *) -class func_decl ctx = -object (self) - inherit ast ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_ndr (name : Symbol.symbol) (domain : sort array) (range : sort) = (self#sno ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (Array.length domain) (astaton domain) range#gno)) ; self - method cnstr_pdr (prefix : string) (domain : sort array) (range : sort) = (self#sno ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (Array.length domain) (astaton domain) range#gno)) ; self - - method incref nc o = super#incref nc o - method decref nc o = super#decref nc o -end - -let func_declaton (a : func_decl array) = - let f (e : func_decl) = e#gno in - Array.map f a - -(** Enum sort objects *) -class enum_sort ctx = -object (self) - inherit sort ctx as super - val mutable _constdecls : func_decl array option = None - val mutable _testerdecls : func_decl array option = None - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_ss (name : Symbol.symbol) (enum_names : Symbol.symbol array) = - let (r, a, b) = (Z3native.mk_enumeration_sort (context_gno ctx) (Symbol.gno name) (Array.length enum_names) (Symbol.aton enum_names)) in - _constdecls <- Some (let f e = (new func_decl ctx)#cnstr_obj e in (Array.map f a)) ; - _testerdecls <- Some (let f e = (new func_decl ctx)#cnstr_obj e in (Array.map f b)) ; - (self#sno ctx r) ; - self - - method const_decls = match _constdecls with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing const decls") - - method tester_decls = match _testerdecls with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing tester decls") -end - -(** List sort objects *) -class list_sort ctx = -object (self) - inherit sort ctx as super - val mutable _nildecl : func_decl option = None - val mutable _is_nildecl : func_decl option = None - val mutable _consdecl : func_decl option = None - val mutable _is_consdecl : func_decl option = None - val mutable _headdecl : func_decl option = None - val mutable _taildecl : func_decl option = None - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_ss (name : Symbol.symbol) (elem_sort : sort) = - let (r, a, b, c, d, e, f) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) elem_sort#gno) in - _nildecl <- Some ((new func_decl ctx)#cnstr_obj a) ; - _is_nildecl <- Some ((new func_decl ctx)#cnstr_obj b) ; - _consdecl <- Some ((new func_decl ctx)#cnstr_obj c) ; - _is_consdecl <- Some ((new func_decl ctx)#cnstr_obj d) ; - _headdecl <- Some ((new func_decl ctx)#cnstr_obj e) ; - _taildecl <- Some ((new func_decl ctx)#cnstr_obj f) ; - (self#sno ctx r) ; - self - - method nil_decl = match _nildecl with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing nil decl") - - method is_nil_decl = match _is_nildecl with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing is_nil decl") - - method cons_decl = match _consdecl with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing cons decl") - - method is_cons_decl = match _is_consdecl with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing is_cons decl") - - method head_decl = match _headdecl with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing head decl") - - method tail_decl = match _taildecl with - | Some(x) -> x - | None -> raise (Z3native.Exception "Missing tail decl") -end - -(** Constructor objects *) -class constructor ctx = -object (self) - inherit z3object ctx None as super - val mutable m_n : int = 0 - val mutable m_tester_decl : func_decl option = None - val mutable m_constructor_decl : func_decl option = None - val mutable m_accessor_decls : func_decl array option = None - method incref nc o = () - method decref nc o = () - initializer - let f = fun o -> Z3native.del_constructor o#gnc o#gno in - let v = self in - Gc.finalise f v - - method cnstr_ssssi (name : Symbol.symbol) (recognizer : Symbol.symbol) (field_names : Symbol.symbol array) (sorts : sort array) (sort_refs : int array) = - m_n <- (Array.length field_names) ; - if m_n != (Array.length sorts) then - raise (Z3native.Exception "Number of field names does not match number of sorts") - else - if m_n != (Array.length sort_refs) then - raise (Z3native.Exception "Number of field names does not match number of sort refs") - else - let o = (Z3native.mk_constructor (context_gno ctx) (Symbol.gno name) (Symbol.gno recognizer) m_n (Symbol.aton field_names) - (sortaton sorts) - sort_refs) in - self#sno ctx o ; - self - - method private init = - match m_tester_decl with - | None -> - let (a, b, c) = (Z3native.query_constructor self#gnc self#gno m_n) in - m_constructor_decl <- Some ((new func_decl ctx)#cnstr_obj a) ; - m_tester_decl <- Some ((new func_decl ctx)#cnstr_obj b) ; - m_accessor_decls <- Some (let f e = ((new func_decl ctx)#cnstr_obj e) in Array.map f c) ; - () - | _ -> () - - method get_n = m_n - - method tester_decl = match m_tester_decl with - | Some(x) -> x - | None -> self#init ; self#tester_decl - - method constructor_decl = match m_constructor_decl with - | Some(x) -> x - | None -> self#init ; self#constructor_decl - - method accessor_decls = match m_accessor_decls with - | Some(x) -> x - | None -> self#init ; self#accessor_decls -end - -let constructoraton (a : constructor array) = - let f (e : constructor) = e#gno in - Array.map f a - -(** Constructor list objects *) -class constructor_list ctx = -object (self) - inherit z3object ctx None - method incref nc o = () - method decref nc o = () - initializer - let f = fun o -> Z3native.del_constructor_list o#gnc o#gno in - let v = self in - Gc.finalise f v - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_ca ( c : constructor array ) = - self#sno ctx (Z3native.mk_constructor_list (context_gno ctx) (Array.length c) (constructoraton c)) ; - self -end - -let constructor_listaton (a : constructor_list array) = - let f (e : constructor_list) = e#gno in - Array.map f a - -(** Datatype sort objects *) -class datatype_sort ctx = -object (self) - inherit sort ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self - method cnstr_sc (name : Symbol.symbol) (constructors : constructor array) = (self#sno ctx (fst (Z3native.mk_datatype (context_gno ctx) (Symbol.gno name) (Array.length constructors) (constructoraton constructors)))) ; self -end - -let create_sort ctx obj = - match (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) obj)) with - | ARRAY_SORT -> (((new array_sort ctx)#cnstr_obj obj) :> sort) - | BOOL_SORT -> (((new bool_sort ctx)#cnstr_obj obj) :> sort) - | BV_SORT -> (((new bitvec_sort ctx)#cnstr_obj obj) :> sort) - | DATATYPE_SORT -> (((new datatype_sort ctx)#cnstr_obj obj) :> sort) - | INT_SORT -> (((new int_sort ctx)#cnstr_obj obj) :> sort) - | REAL_SORT -> (((new real_sort ctx)#cnstr_obj obj) :> sort) - | UNINTERPRETED_SORT -> (((new uninterpreted_sort ctx)#cnstr_obj obj) :> sort) - | FINITE_DOMAIN_SORT -> (((new finite_domain_sort ctx)#cnstr_obj obj) :> sort) - | RELATION_SORT -> (((new relation_sort ctx)#cnstr_obj obj) :> sort) - | UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered") - -(** Expression objects *) -class expr ctx = -object(self) - inherit ast ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -let expraton (a : expr array) = - let f (e : expr) = e#gno in - Array.map f a - -(** Boolean expression objects *) -class bool_expr ctx = -object (self) - inherit expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Arithmetic expression objects (int/real) *) -class arith_expr ctx = -object (self) - inherit expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Int expression objects *) -class int_expr ctx = -object (self) - inherit arith_expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Real expression objects *) -class real_expr ctx = -object (self) - inherit arith_expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Bit-vector expression objects *) -class bitvec_expr ctx = -object (self) - inherit expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Array expression objects *) -class array_expr ctx = -object (self) - inherit expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Datatype expression objects *) -class datatype_expr ctx = -object (self) - inherit expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Integer numeral expression objects *) -class int_num ctx = -object (self) - inherit int_expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Rational numeral expression objects *) -class rat_num ctx = -object (self) - inherit real_expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Bit-vector numeral expression objects *) -class bitvec_num ctx = -object (self) - inherit bitvec_expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Algebraic numeral expression objects *) -class algebraic_num ctx = -object (self) - inherit arith_expr ctx as super - method cnstr_obj obj = (self#sno ctx obj) ; self -end - -(** Quantifier objects *) -class quantifier ctx = -object (self) - inherit expr ctx as super - 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 - -let patternaton (a : pattern array) = - let f (e : pattern) = e#gno in - Array.map f a - -(**/**) - - -(** Interaction logging for Z3 - - Note that this is a global, static log and if multiple Context - objects are created, it logs the interaction with all of them. *) -module Log = -struct - (** Open an interaction log file. - @param filename the name of the file to open. - @return True if opening the log file succeeds, false otherwise. - *) - (* CMW: "open" seems to be a reserved keyword? *) - let open_ filename = ((lbool_of_int (Z3native.open_log filename)) == L_TRUE) - - (** Closes the interaction log. *) - let close = Z3native.close_log - - (** Appends a user-provided string to the interaction log. - @param s the string to append*) - let append s = Z3native.append_log s -end - -(** Version information *) -module Version = -struct - (** The major version. *) - let major = let (x, _, _, _) = Z3native.get_version in x - - (** The minor version. *) - let minor = let (_, x, _, _) = Z3native.get_version in x - - (** The build version. *) - let build = let (_, _, x, _) = Z3native.get_version in x - - (** The revision. *) - let revision = let (_, _, _, x) = Z3native.get_version in x - - (** A string representation of the version information. *) - let to_string = - let (mj, mn, bld, rev) = Z3native.get_version in - string_of_int mj ^ "." ^ - string_of_int mn ^ "." ^ - string_of_int bld ^ "." ^ - string_of_int rev ^ "." -end - - -(** The Sort module implements type information for ASTs *) -module Sort = -struct - (** - Comparison operator. - @param a A sort - @param b A sort - @return True if and are from the same context - and represent the same sort; false otherwise. - *) - let ( = ) (a : sort) (b : sort) = (a == b) || - if a#gnc != b#gnc then - false - else - (Z3native.is_eq_sort a#gnc a#gno b#gno) - - (** - Returns a unique identifier for the sort. - *) - let get_id (x : sort) = Z3native.get_sort_id x#gnc x#gno - - (** - The kind of the sort. - *) - let get_sort_kind (x : sort) = (sort_kind_of_int (Z3native.get_sort_kind x#gnc x#gno)) - - (** - The name of the sort - *) - let get_name (x : sort) = (Symbol.create x#gc (Z3native.get_sort_name x#gnc x#gno)) - - (** - 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 (context_gno ctx)) - - (** - Create a new uninterpreted sort. - *) - let mk_uninterpreted ( ctx : context ) ( s : Symbol.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) -end - -(**/**) -let create_expr ctx obj = - if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) obj) == QUANTIFIER_AST then - (((new quantifier ctx)#cnstr_obj obj) :> expr) - else - let s = Z3native.get_sort (context_gno ctx) obj in - let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in - if (Z3native.is_algebraic_number (context_gno ctx) obj) then - (((new algebraic_num ctx)#cnstr_obj obj) :> expr) - else - if (Z3native.is_numeral_ast (context_gno ctx) obj) && - (sk == INT_SORT or sk == REAL_SORT or sk == BV_SORT) then - match sk with - | INT_SORT -> (((new int_num ctx)#cnstr_obj obj) :> expr) - | REAL_SORT -> (((new rat_num ctx)#cnstr_obj obj) :> expr) - | BV_SORT -> (((new bitvec_num ctx)#cnstr_obj obj) :> expr) - | _ -> raise (Z3native.Exception "Unsupported numeral object") - else - match sk with - | BOOL_SORT -> (((new bool_expr ctx)#cnstr_obj obj) :> expr) - | INT_SORT -> (((new int_expr ctx)#cnstr_obj obj) :> expr) - | REAL_SORT -> (((new real_expr ctx)#cnstr_obj obj) :> expr) - | BV_SORT -> (((new bitvec_expr ctx)#cnstr_obj obj) :> expr) - | ARRAY_SORT -> (((new array_expr ctx)#cnstr_obj obj) :> expr) - | DATATYPE_SORT -> (((new datatype_expr ctx)#cnstr_obj obj) :> expr) - | _ -> (new expr ctx)#cnstr_obj obj - -let create_expr_fa (ctx : context) (f : func_decl) (args : expr array) = - let o = Z3native.mk_app (context_gno ctx) f#gno (Array.length args) (astaton args) in - create_expr ctx o - -let create_ast ctx no = - match (ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no)) with - | FUNC_DECL_AST -> (((new func_decl ctx)#cnstr_obj no) :> ast) - | QUANTIFIER_AST -> (((new quantifier ctx)#cnstr_obj no) :> ast) - | SORT_AST -> ((create_sort ctx no) :> ast) - | APP_AST - | NUMERAL_AST - | VAR_AST -> ((create_expr ctx no) :> ast) - | UNKNOWN_AST -> raise (Z3native.Exception "Cannot create asts of type unknown") -(**/**) - -(** Function declarations *) -module FuncDecl = -struct - - (** Parameters of Func_Decls *) - module Parameter = - struct - type parameter = { - m_kind : parameter_kind ; - m_i : int ; - m_d : float ; - m_sym : Symbol.symbol option ; - m_srt : sort option ; - m_ast : ast option ; - m_fd : func_decl option ; - m_r : string ; - } - - (**/**) - let cnstr_int i = { - m_kind = PARAMETER_INT ; - m_i = i ; - m_d = 0.0 ; - m_sym = None ; - m_srt = None ; - m_ast = None ; - m_fd = None ; - m_r = "" ; - } - - let cnstr_double d = { - m_kind = PARAMETER_DOUBLE ; - m_i = 0 ; - m_d = d ; - m_sym = None ; - m_srt = None ; - m_ast = None ; - m_fd = None ; - m_r = "" ; - } - - let cnstr_symbol sym = { - m_kind = PARAMETER_SYMBOL ; - m_i = 0 ; - m_d = 0.0 ; - m_sym = sym ; - m_srt = None ; - m_ast = None ; - m_fd = None ; - m_r = "" ; - } - - let cnstr_sort srt = { - m_kind = PARAMETER_SORT ; - m_i = 0 ; - m_d = 0.0 ; - m_sym = None ; - m_srt = srt ; - m_ast = None ; - m_fd = None ; - m_r = "" ; - } - - let cnstr_ast ast = { - m_kind = PARAMETER_AST ; - m_i = 0 ; - m_d = 0.0 ; - m_sym = None ; - m_srt = None ; - m_ast = ast ; - m_fd = None ; - m_r = "" ; - } - - let cnstr_func_decl fd ={ - m_kind = PARAMETER_FUNC_DECL ; - m_i = 0 ; - m_d = 0.0 ; - m_sym = None ; - m_srt = None ; - m_ast = None ; - m_fd = fd ; - m_r = "" ; - } - - let cnstr_rational r = { - m_kind = PARAMETER_RATIONAL ; - m_i = 0 ; - m_d = 0.0 ; - m_sym = None ; - m_srt = None ; - m_ast = None ; - m_fd = None ; - m_r = r ; - } - (**/**) - - (** - The kind of the parameter. - *) - let get_kind ( x : parameter ) = x.m_kind - - (**The int value of the parameter.*) - let get_int ( x : parameter ) = - if ((get_kind x) != PARAMETER_INT) then - raise (Z3native.Exception "parameter is not an int") - else - x.m_i - - (**The double value of the parameter.*) - let get_double ( x : parameter ) = - if ((get_kind x) != PARAMETER_DOUBLE) then - raise (Z3native.Exception "parameter is not a double") - else - x.m_d - - (**The Symbol value of the parameter.*) - let get_symbol ( x : parameter ) = - if ((get_kind x) != PARAMETER_SYMBOL) then - raise (Z3native.Exception "parameter is not a symbol") - else - x.m_sym - - (**The Sort value of the parameter.*) - let get_sort ( x : parameter ) = - if ((get_kind x) != PARAMETER_SORT) then - raise (Z3native.Exception "parameter is not a sort") - else - x.m_srt - - (**The AST value of the parameter.*) - let get_ast ( x : parameter ) = - if ((get_kind x) != PARAMETER_AST) then - raise (Z3native.Exception "parameter is not an ast") - else - x.m_ast - - (**The FunctionDeclaration value of the parameter.*) - let get_ast ( x : parameter ) = - if ((get_kind x) != PARAMETER_FUNC_DECL) then - raise (Z3native.Exception "parameter is not an function declaration") - else - x.m_fd - - (**The rational string value of the parameter.*) - let get_rational ( x : parameter ) = - if ((get_kind x) != PARAMETER_RATIONAL) then - raise (Z3native.Exception "parameter is not a ratinoal string") - else - x.m_r - end - - (** - Creates a new function declaration. - *) - let mk_func_decl ( ctx : context ) ( name : Symbol.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) 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.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) [||] 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 - - - (** - Comparison operator. - @param a A func_decl - @param b A func_decl - @return True if and are from the same context - and represent the same func_decl; false otherwise. - *) - let ( = ) (a : func_decl) (b : func_decl) = (a == b) || - if a#gnc == a#gnc then - false - else - (Z3native.is_eq_func_decl a#gnc a#gno b#gno) - (** - A string representations of the function declaration. - *) - let to_string (x : func_decl) = Z3native.func_decl_to_string x#gnc x#gno - - (** - Returns a unique identifier for the function declaration. - *) - let get_id (x : func_decl) = Z3native.get_func_decl_id x#gnc x#gno - - (** - The arity of the function declaration - *) - let get_arity (x : func_decl) = Z3native.get_arity x#gnc x#gno - - (** - The size of the domain of the function declaration - - *) - let get_domain_size (x : func_decl) = Z3native.get_domain_size x#gnc x#gno - - (** - The domain of the function declaration - *) - let get_domain (x : func_decl) = - let n = (get_domain_size x) in - let f i = create_sort x#gc (Z3native.get_domain x#gnc x#gno i) in - Array.init n f - - (** - The range of the function declaration - *) - let get_range (x : func_decl) = - create_sort x#gc (Z3native.get_range x#gnc x#gno) - - (** - The kind of the function declaration. - *) - let get_decl_kind (x : func_decl) = (decl_kind_of_int (Z3native.get_decl_kind x#gnc x#gno)) - - (** - The name of the function declaration - *) - let get_name (x : func_decl) = (Symbol.create x#gc (Z3native.get_decl_name x#gnc x#gno)) - - (** - The number of parameters of the function declaration - *) - let get_num_parameters (x : func_decl) = (Z3native.get_decl_num_parameters x#gnc x#gno) - - (** - The parameters of the function declaration - *) - let get_parameters (x : func_decl) = - let n = (get_num_parameters x) in - let f i = ( - match (parameter_kind_of_int (Z3native.get_decl_parameter_kind x#gnc x#gno i)) with - | PARAMETER_INT -> Parameter.cnstr_int (Z3native.get_decl_int_parameter x#gnc x#gno i) - | PARAMETER_DOUBLE -> Parameter.cnstr_double (Z3native.get_decl_double_parameter x#gnc x#gno i) - | PARAMETER_SYMBOL-> Parameter.cnstr_symbol (Some (Symbol.create x#gc (Z3native.get_decl_symbol_parameter x#gnc x#gno i))) - | PARAMETER_SORT -> Parameter.cnstr_sort (Some (create_sort x#gc (Z3native.get_decl_sort_parameter x#gnc x#gno i))) - | PARAMETER_AST -> Parameter.cnstr_ast (Some (create_ast x#gc (Z3native.get_decl_ast_parameter x#gnc x#gno i))) - | PARAMETER_FUNC_DECL -> Parameter.cnstr_func_decl (Some ((new func_decl x#gc)#cnstr_obj (Z3native.get_decl_func_decl_parameter x#gnc x#gno i))) - | PARAMETER_RATIONAL -> Parameter.cnstr_rational (Z3native.get_decl_rational_parameter x#gnc x#gno i) - ) in - mk_list f n - - (** - Create expression that applies function to arguments. - @param args The arguments - *) - let apply (x : func_decl) (args : expr array) = create_expr_fa x#gc x args - -end (** The abstract syntax tree (AST) module *) -module AST = -struct +module rec AST : +sig + type ast = z3_native_object + + val create : context -> Z3native.ptr -> ast + val aton : ast array -> Z3native.ptr array + + val is_expr : ast -> bool + val is_var : ast -> bool +end = struct + type ast = z3_native_object + + let create ( ctx : context ) ( no : Z3native.ptr ) = + let res : z3_native_object = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in + (z3obj_sno res ctx no) ; + (z3obj_create res) ; + res + + let aton (a : ast array) = + let f (e : ast) = (z3obj_gno e) in + Array.map f a + + (** Vectors of ASTs *) module ASTVector = struct type ast_vector = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_vector = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.ast_vector_inc_ref ; dec_ref = Z3native.ast_vector_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -1133,11 +379,11 @@ struct @return An AST *) let get ( x : ast_vector ) ( i : int ) = - create_ast (z3obj_gc x) (Z3native.ast_vector_get (z3obj_gnc x) (z3obj_gno x) i) + create (z3obj_gc x) (Z3native.ast_vector_get (z3obj_gnc x) (z3obj_gno x) i) (** Sets the i-th object in the vector. *) let set ( x : ast_vector ) ( i : int ) ( value : ast ) = - Z3native.ast_vector_set (z3obj_gnc x) (z3obj_gno x) i value#gno + Z3native.ast_vector_set (z3obj_gnc x) (z3obj_gno x) i (z3obj_gno value) (** Resize the vector to . @param newSize The new size of the vector. *) @@ -1150,7 +396,7 @@ struct @param a An AST *) let push ( x : ast_vector ) ( a : ast ) = - Z3native.ast_vector_push (z3obj_gnc x) (z3obj_gno x) a#gno + Z3native.ast_vector_push (z3obj_gnc x) (z3obj_gno x) (z3obj_gno a) (** Translates all ASTs in the vector to . @@ -1158,7 +404,7 @@ struct @return A new ASTVector *) let translate ( x : ast_vector ) ( to_ctx : context ) = - cnstr to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) + create to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) (** Retrieves a string representation of the vector. *) let to_string ( x : ast_vector ) = @@ -1171,13 +417,13 @@ struct type ast_map = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_map = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.ast_map_inc_ref ; dec_ref = Z3native.ast_map_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -1185,7 +431,7 @@ struct @param k An AST @return True if is a key in the map, false otherwise. *) let contains ( x : ast_map ) ( key : ast ) = - (Z3native.ast_map_contains (z3obj_gnc x) (z3obj_gno x) key#gno) + Z3native.ast_map_contains (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) (** Finds the value associated with the key . @@ -1193,7 +439,7 @@ struct @param k An AST *) let find ( x : ast_map ) ( key : ast ) = - create_ast (z3obj_gc x) (Z3native.ast_map_find (z3obj_gnc x) (z3obj_gno x) key#gno) + create (z3obj_gc x) (Z3native.ast_map_find (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key)) (** Stores or replaces a new key/value pair in the map. @@ -1201,14 +447,14 @@ struct @param v The value AST *) let insert ( x : ast_map ) ( key : ast ) ( value : ast) = - Z3native.ast_map_insert (z3obj_gnc x) (z3obj_gno x) key#gno value#gno + Z3native.ast_map_insert (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) (z3obj_gno value) (** Erases the key from the map. @param k An AST *) let erase ( x : ast_map ) ( key : ast ) = - Z3native.ast_map_erase (z3obj_gnc x) (z3obj_gno x) key#gno + Z3native.ast_map_erase (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) (** Removes all keys from the map. *) let reset ( x : ast_map ) = @@ -1220,7 +466,7 @@ struct (** The keys stored in the map. *) let get_keys ( x : ast_map ) = - ASTVector.cnstr (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x)) + ASTVector.create (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x)) (** Retrieves a string representation of the map.*) let to_string ( x : ast_map ) = @@ -1231,23 +477,23 @@ struct The AST's hash code. @return A hash code *) - let get_hash_code ( x : ast) = Z3native.get_ast_hash x#gnc x#gno + let get_hash_code ( x : ast ) = Z3native.get_ast_hash (z3obj_gnc x) (z3obj_gno x) (** A unique identifier for the AST (unique among all ASTs). *) - let get_id ( x : ast) = Z3native.get_ast_id x#gnc x#gno + let get_id ( x : ast ) = Z3native.get_ast_id (z3obj_gnc x) (z3obj_gno x) (** The kind of the AST. *) - let get_ast_kind ( x : ast) = (ast_kind_of_int (Z3native.get_ast_kind x#gnc x#gno)) + let get_ast_kind ( x : ast ) = (ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc x) (z3obj_gno x))) (** Indicates whether the AST is an Expr *) - let is_expr ( x : ast) = - match get_ast_kind ( x : ast) with + let is_expr ( x : ast ) = + match get_ast_kind ( x : ast ) with | APP_AST | NUMERAL_AST | QUANTIFIER_AST @@ -1257,33 +503,33 @@ struct (** Indicates whether the AST is a bound variable *) - let is_var ( x : ast) = (get_ast_kind x) == VAR_AST + let is_var ( x : ast ) = (get_ast_kind x) == VAR_AST (** Indicates whether the AST is a Quantifier *) - let is_quantifier ( x : ast) = (get_ast_kind x) == QUANTIFIER_AST + let is_quantifier ( x : ast ) = (get_ast_kind x) == QUANTIFIER_AST (** Indicates whether the AST is a Sort *) - let is_sort ( x : ast) = (get_ast_kind x) == SORT_AST + let is_sort ( x : ast ) = (get_ast_kind x) == SORT_AST (** Indicates whether the AST is a FunctionDeclaration *) - let is_func_decl ( x : ast) = (get_ast_kind x) == FUNC_DECL_AST + let is_func_decl ( x : ast ) = (get_ast_kind x) == FUNC_DECL_AST (** A string representation of the AST. *) - let to_string ( x : ast) = Z3native.ast_to_string x#gnc x#gno + let to_string ( x : ast ) = Z3native.ast_to_string (z3obj_gnc x) (z3obj_gno x) (** A string representation of the AST in s-expression notation. *) - let to_sexpr ( x : ast) = Z3native.ast_to_string x#gnc x#gno + let to_sexpr ( x : ast ) = Z3native.ast_to_string (z3obj_gnc x) (z3obj_gno x) (** Comparison operator. @@ -1292,11 +538,11 @@ struct @return True if and are from the same context and represent the same sort; false otherwise. *) - let ( = ) (a : expr) (b : expr) = (a == b) || - if a#gnc == b#gnc then + let ( = ) ( a : ast ) ( b : ast ) = (a == b) || + if (z3obj_gnc a) != (z3obj_gnc b) then false else - (Z3native.is_eq_ast a#gnc a#gno b#gno) + Z3native.is_eq_ast (z3obj_gnc a) (z3obj_gno a) (z3obj_gno b) (** Object Comparison. @@ -1316,11 +562,11 @@ struct @param ctx A context @return A copy of the AST which is associated with *) - let translate ( x : ast) to_ctx = - if x#gc == to_ctx then + let translate ( x : ast ) ( to_ctx : context ) = + if (z3obj_gnc x) == (context_gno to_ctx) then x else - (create_ast to_ctx (Z3native.translate x#gnc x#gno (context_gno to_ctx))) + create to_ctx (Z3native.translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) (** Wraps an AST. @@ -1334,7 +580,7 @@ struct @param nativeObject The native pointer to wrap. *) let wrap ( ctx : context ) ( ptr : Z3native.ptr ) = - create_ast ctx ptr + create ctx ptr (** Unwraps an AST. @@ -1347,43 +593,413 @@ struct @param a The AST to unwrap. *) - let unwrap_ast ( a : ast ) = a#gno + let unwrap_ast ( x : ast ) = (z3obj_gno x) + + (**/**) + let create ( ctx : context ) ( no : Z3native.ptr ) = + match (ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no)) with + | FUNC_DECL_AST -> (match (FuncDecl.create ctx no) with FuncDecl.FuncDecl(x) -> x) + | SORT_AST -> (match (Sort.create ctx no) with Sort.Sort(x) -> x) + | QUANTIFIER_AST -> (match (Quantifiers.create ctx no) with Quantifiers.Quantifier(Expr.Expr(x)) -> x) + | APP_AST + | NUMERAL_AST + | VAR_AST -> (match (Expr.create ctx no) with Expr.Expr(x) -> x) + | UNKNOWN_AST -> raise (Z3native.Exception "Cannot create asts of type unknown") +(**/**) end +(** The Sort module implements type information for ASTs *) +and Sort : +sig + type sort = Sort of AST.ast + type bitvec_sort = BitvecSort of sort + type uninterpreted_sort = UninterpretedSort of sort + + val create : context -> Z3native.ptr -> sort + val gno : sort -> Z3native.ptr + val gnc : sort -> Z3native.ptr + val aton : sort array -> Z3native.ptr array +end = struct + type sort = Sort of AST.ast + type bitvec_sort = BitvecSort of sort + type uninterpreted_sort = UninterpretedSort of sort + + let gc ( x : sort ) = (match x with Sort(a) -> (z3obj_gc a)) + let gnc ( x : sort ) = (match x with Sort(a) -> (z3obj_gnc a)) + let gno ( x : sort ) = (match x with Sort(a) -> (z3obj_gno a)) + + let aton : sort array -> Z3native.ptr array = fun a -> + let f e = (gno e) in + Array.map f a + + let create : context -> Z3native.ptr -> sort = fun ctx no -> + let q : z3_native_object = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in + (z3obj_sno q ctx no) ; + (z3obj_create q) ; + match (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) no)) with + | ARRAY_SORT + | BOOL_SORT + | BV_SORT + | DATATYPE_SORT + | INT_SORT + | REAL_SORT + | UNINTERPRETED_SORT + | FINITE_DOMAIN_SORT + | RELATION_SORT -> Sort(q) + | UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered") + + + (** + Comparison operator. + @param a A sort + @param b A sort + @return True if and are from the same context + and represent the same sort; false otherwise. + *) + let ( = ) : sort -> sort -> bool = fun a b -> + (a == b) || + if (gnc a) != (gnc b) then + false + else + (Z3native.is_eq_sort (gnc a) (gno a) (gno b)) + + (** + Returns a unique identifier for the sort. + *) + let get_id ( x : sort ) = Z3native.get_sort_id (gnc x) (gno x) + + (** + The kind of the sort. + *) + let get_sort_kind ( x : sort ) = (sort_kind_of_int (Z3native.get_sort_kind (gnc x) (gno x))) + + (** + The name of the sort + *) + let get_name ( x : sort ) = (Symbol.create (gc x) (Z3native.get_sort_name (gnc x) (gno x))) + + (** + A string representation of the sort. + *) + let to_string ( x : sort ) = Z3native.sort_to_string (gnc x) (gno x) + + (** + Create a new uninterpreted sort. + *) + let mk_uninterpreted ( ctx : context ) ( s : Symbol.symbol ) = + let res = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in + (z3obj_sno res ctx (Z3native.mk_uninterpreted_sort (context_gno ctx) (Symbol.gno s))) ; + (z3obj_create res) ; + UninterpretedSort(Sort(res)) + + (** + Create a new uninterpreted sort. + *) + let mk_uninterpreted_s ( ctx : context ) ( s : string ) = + mk_uninterpreted ctx (Symbol.mk_string ( ctx : context ) s) +end + + +(** Function declarations *) +and FuncDecl : +sig + type func_decl = FuncDecl of AST.ast + + val create : context -> Z3native.ptr -> func_decl + val gno : func_decl -> Z3native.ptr + val gnc : func_decl -> Z3native.ptr + + val get_domain_size : func_decl -> int + val get_decl_kind : func_decl -> Z3enums.decl_kind +end = struct + open Sort + + type func_decl = FuncDecl of AST.ast + + let create ( ctx : context ) ( no : Z3native.ptr ) = + let res = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in + (z3obj_sno res ctx no) ; + (z3obj_create res) ; + FuncDecl(res) + + let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort array ) ( range : sort ) = + let res = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in + (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (Array.length domain) (Sort.aton domain) (Sort.gno range))) ; + (z3obj_create res) ; + FuncDecl(res) + + let create_pdr ( ctx : context) ( prefix : string ) ( domain : sort array ) ( range : sort ) = + let res = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in + (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (Array.length domain) (Sort.aton domain) (Sort.gno range))) ; + (z3obj_create res) ; + FuncDecl(res) + + let gc ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gc a) + let gnc ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gnc a) + let gno ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gno a) + + let aton (a : func_decl array) = + let f (e : func_decl) = (gno e) in + Array.map f a + + (** Parameters of Func_Decls *) + module Parameter = + struct + type parameter = + | P_Int of int + | P_Dbl of float + | P_Sym of Symbol.symbol + | P_Srt of Sort.sort + | P_Ast of AST.ast + | P_Fdl of func_decl + | P_Rat of string + + (** The kind of the parameter. *) + let get_kind ( x : parameter ) = + (match x with + | P_Int(_) -> PARAMETER_INT + | P_Dbl(_) -> PARAMETER_DOUBLE + | P_Sym(_) -> PARAMETER_SYMBOL + | P_Srt(_) -> PARAMETER_SORT + | P_Ast(_) -> PARAMETER_AST + | P_Fdl(_) -> PARAMETER_FUNC_DECL + | P_Rat(_) -> PARAMETER_RATIONAL) + + (**The int value of the parameter.*) + let get_int ( x : parameter ) = + match x with + | P_Int(x) -> x + | _ -> raise (Z3native.Exception "parameter is not an int") + + (**The double value of the parameter.*) + let get_float ( x : parameter ) = + match x with + | P_Dbl(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a double") + + (**The Symbol value of the parameter.*) + let get_symbol ( x : parameter ) = + match x with + | P_Sym(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a symbol") + + (**The Sort value of the parameter.*) + let get_sort ( x : parameter ) = + match x with + | P_Srt(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a sort") + + (**The AST value of the parameter.*) + let get_ast ( x : parameter ) = + match x with + | P_Ast(x) -> x + | _ -> raise (Z3native.Exception "parameter is not an ast") + + (**The FunctionDeclaration value of the parameter.*) + let get_func_decl ( x : parameter ) = + match x with + | P_Fdl(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a func_decl") + + (**The rational string value of the parameter.*) + let get_func_decl ( x : parameter ) = + match x with + | P_Rat(x) -> x + | _ -> raise (Z3native.Exception "parameter is not a rational string") + end + + open Parameter + + (** + Creates a new function declaration. + *) + let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort array ) ( range : sort ) = + create_ndr ctx 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) 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 ) = + create_pdr ctx prefix domain range + + (** + Creates a new constant function declaration. + *) + let mk_const_decl ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) = + create_ndr ctx name [||] range + + (** + Creates a new constant function declaration. + *) + let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : sort ) = + create_ndr ctx (Symbol.mk_string ctx name) [||] range + + (** + Creates a fresh constant function declaration with a name prefixed with . + + + *) + let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : sort ) = + create_pdr ctx prefix [||] range + + + (** + Comparison operator. + @param a A func_decl + @param b A func_decl + @return True if and are from the same context + and represent the same func_decl; false otherwise. + *) + let ( = ) ( a : func_decl ) ( b : func_decl ) = (a == b) || + if (gnc a) != (gnc b) then + false + else + (Z3native.is_eq_func_decl (gnc a) (gno a) (gno b)) + + (** + A string representations of the function declaration. + *) + let to_string ( x : func_decl ) = Z3native.func_decl_to_string (gnc x) (gno x) + + (** + Returns a unique identifier for the function declaration. + *) + let get_id ( x : func_decl ) = Z3native.get_func_decl_id (gnc x) (gno x) + + (** + The arity of the function declaration + *) + let get_arity ( x : func_decl ) = Z3native.get_arity (gnc x) (gno x) + + (** + The size of the domain of the function declaration + + *) + let get_domain_size ( x : func_decl ) = Z3native.get_domain_size (gnc x) (gno x) + + (** + The domain of the function declaration + *) + let get_domain ( x : func_decl ) = + let n = (get_domain_size x) in + let f i = Sort.create (gc x) (Z3native.get_domain (gnc x) (gno x) i) in + Array.init n f + + (** + The range of the function declaration + *) + let get_range ( x : func_decl ) = + Sort.create (gc x) (Z3native.get_range (gnc x) (gno x)) + + (** + The kind of the function declaration. + *) + let get_decl_kind ( x : func_decl ) = (decl_kind_of_int (Z3native.get_decl_kind (gnc x) (gno x))) + + (** + The name of the function declaration + *) + let get_name ( x : func_decl ) = (Symbol.create (gc x) (Z3native.get_decl_name (gnc x) (gno x))) + + (** + The number of parameters of the function declaration + *) + let get_num_parameters ( x : func_decl ) = (Z3native.get_decl_num_parameters (gnc x) (gno x)) + + (** + The parameters of the function declaration + *) + let get_parameters ( x : func_decl ) = + let n = (get_num_parameters x) in + let f i = (match (parameter_kind_of_int (Z3native.get_decl_parameter_kind (gnc x) (gno x) i)) with + | PARAMETER_INT -> P_Int (Z3native.get_decl_int_parameter (gnc x) (gno x) i) + | PARAMETER_DOUBLE -> P_Dbl (Z3native.get_decl_double_parameter (gnc x) (gno x) i) + | PARAMETER_SYMBOL-> P_Sym (Symbol.create (gc x) (Z3native.get_decl_symbol_parameter (gnc x) (gno x) i)) + | PARAMETER_SORT -> P_Srt (Sort.create (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i)) + | PARAMETER_AST -> P_Ast (AST.create (gc x) (Z3native.get_decl_ast_parameter (gnc x) (gno x) i)) + | PARAMETER_FUNC_DECL -> P_Fdl (create (gc x) (Z3native.get_decl_func_decl_parameter (gnc x) (gno x) i)) + | PARAMETER_RATIONAL -> P_Rat (Z3native.get_decl_rational_parameter (gnc x) (gno x) i) + ) in + mk_list f n + + (** + Create expression that applies function to arguments. + @param args The arguments + *) + let apply ( x : func_decl ) ( args : Expr.expr array ) = Expr.create_fa (gc x) x args +end + (** Parameter sets (of Solvers, Tactics, ...) A Params objects represents a configuration in the form of symbol/value pairs. *) -module Params = -struct +and Params : +sig + type params = z3_native_object + + val create : context -> Z3native.ptr -> params + + module ParamDescrs : sig + type param_descrs = z3_native_object + + val create : context -> Z3native.ptr -> param_descrs + end +end = struct type params = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : params = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.params_inc_ref ; dec_ref = Z3native.params_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) (** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *) - module ParamDescrs = - struct + module ParamDescrs : + sig + type param_descrs = z3_native_object + + val create : context -> Z3native.ptr -> param_descrs + end = struct type param_descrs = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : param_descrs = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.param_descrs_inc_ref ; dec_ref = Z3native.param_descrs_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -1449,7 +1065,6 @@ struct *) let add_s_double ( x : params ) ( name : string ) ( value : float ) = add_double x (Symbol.mk_string (z3obj_gc x) name) value - (** Adds a parameter setting. *) @@ -1460,7 +1075,7 @@ struct Creates a new parameter set *) let mk_params ( ctx : context ) = - cnstr ctx (Z3native.mk_params (context_gno ctx)) + create ctx (Z3native.mk_params (context_gno ctx)) (** A string representation of the parameter set. @@ -1468,18 +1083,69 @@ struct let to_string ( x : params ) = Z3native.params_to_string (z3obj_gnc x) (z3obj_gno x) end - (** General expressions (terms), including Boolean logic *) -module Expr = -struct +and Expr : +sig + type expr = Expr of AST.ast + + val create : context -> Z3native.ptr -> expr + val create_fa : context -> FuncDecl.func_decl -> expr array -> expr + val gc : expr -> context + val gno : expr -> Z3native.ptr + val gnc : expr -> Z3native.ptr + val aton : expr array -> Z3native.ptr array + + val mk_const : context -> Symbol.symbol -> Sort.sort -> expr + val get_func_decl : expr -> FuncDecl.func_decl +end = struct + type expr = Expr of AST.ast + + let create ( ctx : context ) ( obj : Z3native.ptr ) = + if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) obj) == QUANTIFIER_AST then + (match (Quantifiers.create ctx obj) with Quantifiers.Quantifier(e) -> e) + else + let s = Z3native.get_sort (context_gno ctx) obj in + let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in + if (Z3native.is_algebraic_number (context_gno ctx) obj) then + (match (Arithmetic.create_algebraic_num ctx obj) with Arithmetic.AlgebraicNum(Arithmetic.Expr(e)) -> e) + else + if (Z3native.is_numeral_ast (context_gno ctx) obj) && + (sk == INT_SORT or sk == REAL_SORT or sk == BV_SORT) then + match sk with + | INT_SORT -> (match (Arithmetic.create_int_num ctx obj) with Arithmetic.IntNum(Arithmetic.IntExpr(Arithmetic.Expr(e))) -> e) + | REAL_SORT -> (match (Arithmetic.create_rat_num ctx obj) with Arithmetic.RatNum(Arithmetic.RealExpr(Arithmetic.Expr(e))) -> e) + | BV_SORT -> (match (BitVectors.create_num ctx obj) with BitVectors.BitVecNum(BitVectors.BitVecExpr(e)) -> e) + | _ -> raise (Z3native.Exception "Unsupported numeral object") + else + match sk with + | BOOL_SORT -> (match (Booleans.create ctx obj) with Booleans.BoolExpr(e) -> e) + | INT_SORT -> (match (Arithmetic.create_int_expr ctx obj) with Arithmetic.IntExpr(Arithmetic.Expr(e)) -> e) + | REAL_SORT -> (match (Arithmetic.create_real_expr ctx obj) with Arithmetic.RealExpr(Arithmetic.Expr(e)) -> e) + | BV_SORT -> (match (BitVectors.create_expr ctx obj) with BitVectors.BitVecExpr(e) -> e) + | ARRAY_SORT -> (match (Arrays.create_expr ctx obj) with Arrays.ArrayExpr(e) -> e) + | DATATYPE_SORT -> (match (Datatypes.create_expr ctx obj) with Datatypes.DatatypeExpr(e) -> e) + | _ -> Expr(AST.create ctx obj) + + let aton ( a : expr array ) = + let f ( e : expr ) = match e with Expr(a) -> (z3obj_gno a) in + Array.map f a + + let create_fa ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : expr array ) = + let o = Z3native.mk_app (context_gno ctx) (FuncDecl.gno f) (Array.length args) (aton args) in + Expr.create ctx o + + let gc ( x : expr ) = match x with Expr(a) -> (z3obj_gc a) + let gnc ( x : expr ) = match x with Expr(a) -> (z3obj_gnc a) + let gno ( x : expr ) = match x with Expr(a) -> (z3obj_gno a) + (** Returns a simplified version of the expression. @param p A set of parameters to configure the simplifier *) let simplify ( x : expr ) ( p : Params.params option ) = match p with - | None -> create_expr x#gc (Z3native.simplify x#gnc x#gno) - | Some pp -> create_expr x#gc (Z3native.simplify_ex x#gnc x#gno (z3obj_gno pp)) + | None -> Expr.create (gc x) (Z3native.simplify (gnc x) (gno x)) + | Some pp -> Expr.create (gc x) (Z3native.simplify_ex (gnc x) (gno x) (z3obj_gno pp)) (** a string describing all available parameters to Expr.Simplify. @@ -1491,29 +1157,29 @@ struct Retrieves parameter descriptions for simplifier. *) let get_simplify_parameter_descrs ( ctx : context ) = - Params.ParamDescrs.cnstr ctx (Z3native.simplify_get_param_descrs (context_gno ctx)) + Params.ParamDescrs.create ctx (Z3native.simplify_get_param_descrs (context_gno ctx)) (** The function declaration of the function that is applied in this expression. *) - let get_func_decl ( x : expr ) = (new func_decl x#gc)#cnstr_obj (Z3native.get_app_decl x#gnc x#gno) + let get_func_decl ( x : expr ) = FuncDecl.create (gc x) (Z3native.get_app_decl (gnc x) (gno x)) (** Indicates whether the expression is the true or false expression or something else (L_UNDEF). *) - let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value x#gnc x#gno) + let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (gnc x) (gno x)) (** The number of arguments of the expression. *) - let get_num_args ( x : expr ) = Z3native.get_app_num_args x#gnc x#gno + let get_num_args ( x : expr ) = Z3native.get_app_num_args (gnc x) (gno x) (** The arguments of the expression. *) let get_args ( x : expr ) = let n = (get_num_args x) in - let f i = create_expr x#gc (Z3native.get_app_arg x#gnc x#gno i) in + let f i = create (gc x) (Z3native.get_app_arg (gnc x) (gno x) i) in Array.init n f (** @@ -1524,7 +1190,7 @@ struct if (Array.length args <> (get_num_args x)) then raise (Z3native.Exception "Number of arguments does not match") else - x#sno x#gc (Z3native.update_term x#gnc x#gno (Array.length args) (expraton args)) + create (gc x) (Z3native.update_term (gnc x) (gno x) (Array.length args) (aton args)) (** Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs. @@ -1537,7 +1203,7 @@ struct if (Array.length from) <> (Array.length to_) then raise (Z3native.Exception "Argument sizes do not match") else - create_expr x#gc (Z3native.substitute x#gnc x#gno (Array.length from) (expraton from) (expraton to_)) + create (gc x) (Z3native.substitute (gnc x) (gno x) (Array.length from) (aton from) (aton to_)) (** Substitute every occurrence of from in the expression with to. @@ -1552,7 +1218,7 @@ struct 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_)) + create (gc x) (Z3native.substitute_vars (gnc x) (gno x) (Array.length to_) (aton to_)) (** @@ -1561,46 +1227,46 @@ struct @return A copy of the term which is associated with *) let translate ( x : expr ) to_ctx = - if x#gc == to_ctx then + if (gc x) == to_ctx then x else - create_expr to_ctx (Z3native.translate x#gnc x#gno (context_gno to_ctx)) + create to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx)) (** Returns a string representation of the expression. *) - let to_string ( x : expr ) = Z3native.ast_to_string x#gnc x#gno + let to_string ( x : expr ) = Z3native.ast_to_string (gnc x) (gno x) (** Indicates whether the term is a numeral *) - let is_numeral ( x : expr ) = (Z3native.is_numeral_ast x#gnc x#gno) + let is_numeral ( x : expr ) = (Z3native.is_numeral_ast (gnc x) (gno x)) (** Indicates whether the term is well-sorted. @return True if the term is well-sorted, false otherwise. *) - let is_well_sorted ( x : expr ) = Z3native.is_well_sorted x#gnc x#gno + let is_well_sorted ( x : expr ) = Z3native.is_well_sorted (gnc x) (gno x) (** The Sort of the term. *) - let get_sort ( x : expr ) = create_sort x#gc (Z3native.get_sort x#gnc x#gno) + let get_sort ( x : expr ) = Sort.create (gc x) (Z3native.get_sort (gnc x) (gno x)) (** Indicates whether the term has Boolean sort. *) - let is_bool ( x : expr ) = (AST.is_expr x) && - (Z3native.is_eq_sort x#gnc - (Z3native.mk_bool_sort x#gnc) - (Z3native.get_sort x#gnc x#gno)) - + let is_bool ( x : expr ) = (match x with Expr(a) -> (AST.is_expr a)) && + (Z3native.is_eq_sort (gnc x) + (Z3native.mk_bool_sort (gnc x)) + (Z3native.get_sort (gnc x) (gno x))) + (** Indicates whether the term represents a constant. *) - let is_const ( x : expr ) = (AST.is_expr x) && + let is_const ( x : expr ) = (match x with Expr(a) -> (AST.is_expr a)) && (get_num_args x) == 0 && - FuncDecl.get_domain_size(get_func_decl x) == 0 + (FuncDecl.get_domain_size (get_func_decl x)) == 0 (** Indicates whether the term is the constant true. @@ -1679,123 +1345,36 @@ struct (** Creates a new Constant of sort and named . *) - let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) = - create_expr ctx (Z3native.mk_const (context_gno ctx) (Symbol.gno name) range#gno) + let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : Sort.sort ) = + create ctx (Z3native.mk_const (context_gno ctx) (Symbol.gno name) (Sort.gno range)) (** Creates a new Constant of sort and named . *) - let mk_const_s ( ctx : context ) ( name : string ) ( range : sort ) = - mk_const ctx (Symbol.mk_string ctx name)range + let mk_const_s ( ctx : context ) ( name : string ) ( range : Sort.sort ) = + mk_const ctx (Symbol.mk_string ctx name) range (** Creates a constant from the func_decl . @param f An expression of a 0-arity function *) - let mk_const_f ( ctx : context ) ( f : func_decl ) = - create_expr_fa ctx f [||] + let mk_const_f ( ctx : context ) ( f : FuncDecl.func_decl ) = + create_fa ctx f [||] (** Creates a fresh constant of sort and a name prefixed with . *) - let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : sort) = - create_expr ctx (Z3native.mk_fresh_const (context_gno ctx) prefix range#gno) - - (** - Create a Boolean constant. - *) - let mk_bool_const ( ctx : context ) ( name : Symbol.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) + let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : Sort.sort ) = + create ctx (Z3native.mk_fresh_const (context_gno ctx) prefix (Sort.gno range)) (** Create a new function application. *) - let mk_app ( ctx : context ) ( f : func_decl ) ( args : expr array ) = - create_expr_fa ctx f args - - (** - The true Term. - *) - let mk_true ( ctx : context ) = - (new bool_expr ctx)#cnstr_obj (Z3native.mk_true (context_gno ctx)) - - (** - The false Term. - *) - let mk_false ( ctx : context ) = - (new bool_expr ctx)#cnstr_obj (Z3native.mk_false (context_gno ctx)) - - (** - Creates a Boolean value. - *) - let mk_bool ( ctx : context ) ( value : bool) = - if value then mk_true ctx else mk_false ctx - - (** - Creates the equality = . - *) - let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) = - (new bool_expr ctx)#cnstr_obj (Z3native.mk_eq (context_gno ctx) x#gno y#gno) - - (** - Creates a distinct term. - *) - let mk_distinct ( ctx : context ) ( args : expr array ) = - (new bool_expr ctx)#cnstr_obj (Z3native.mk_distinct (context_gno ctx) (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 (context_gno ctx) 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 (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) - - (** - Create an expression representing t1 -> t2. - *) - let mk_implies ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = - (new bool_expr ctx)#cnstr_obj (Z3native.mk_implies (context_gno ctx) t1#gno t2#gno) - - (** - Create an expression representing t1 xor t2. - *) - let mk_xor ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = - (new bool_expr ctx)#cnstr_obj (Z3native.mk_xor (context_gno ctx) 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 (context_gno ctx) (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 (context_gno ctx) (Array.length args) (astaton args)) + let mk_app ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : expr array ) = + create_fa ctx f args (** Create a numeral of a given sort. @@ -1803,8 +1382,8 @@ struct @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 *) - let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : sort ) = - create_expr ctx (Z3native.mk_numeral (context_gno ctx) v ty#gno) + let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : Sort.sort ) = + create ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno ty)) (** Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer. @@ -1813,13 +1392,147 @@ struct @param ty Sort of the numeral @return A Term with value and type *) - let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : sort ) = - create_expr ctx (Z3native.mk_int (context_gno ctx) v ty#gno) + let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : Sort.sort ) = + create ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty)) + + let aton (a : expr array) = + let f (e : expr) = (gno e) in + Array.map f a +end + +(** Boolean expressions *) +and Booleans : +sig + type bool_expr = BoolExpr of Expr.expr + type bool_sort = BoolSort of Sort.sort + + val create : context -> Z3native.ptr -> bool_expr + val aton : bool_expr array -> Z3native.ptr array +end = struct + type bool_expr = BoolExpr of Expr.expr + type bool_sort = BoolSort of Sort.sort + + let create ( ctx : context ) ( no : Z3native.ptr ) = + let a = (AST.create ctx no) in + BoolExpr(Expr.Expr(a)) + + let gc ( x : bool_expr ) = match x with BoolExpr(e) -> (Expr.gc e) + let gnc ( x : bool_expr ) = match x with BoolExpr(e) -> (Expr.gnc e) + let gno ( x : bool_expr ) = match x with BoolExpr(e) -> (Expr.gno e) + + let aton ( a : bool_expr array ) = + let f (e : bool_expr) = (gno e) in + Array.map f a + + let mk_sort ( ctx : context ) = + BoolSort(Sort.create ctx (Z3native.mk_bool_sort (context_gno ctx))) + + (** + Create a Boolean constant. + *) + let mk_const ( ctx : context ) ( name : Symbol.symbol ) = + let s = (match (mk_sort ctx) with BoolSort(q) -> q) in + BoolExpr(Expr.mk_const ctx name s) + + (** + Create a Boolean constant. + *) + let mk_const_s ( ctx : context ) ( name : string ) = + mk_const ctx (Symbol.mk_string ctx name) + + (** + The true Term. + *) + let mk_true ( ctx : context ) = + create ctx (Z3native.mk_true (context_gno ctx)) + + (** + The false Term. + *) + let mk_false ( ctx : context ) = + create ctx (Z3native.mk_false (context_gno ctx)) + + (** + Creates a Boolean value. + *) + let mk_val ( ctx : context ) ( value : bool ) = + if value then mk_true ctx else mk_false ctx + + (** + Creates the equality = . + *) + let mk_eq ( ctx : context ) ( x : Expr.expr ) ( y : Expr.expr ) = + create ctx (Z3native.mk_eq (context_gno ctx) (Expr.gno x) (Expr.gno y)) + + (** + Creates a distinct term. + *) + let mk_distinct ( ctx : context ) ( args : Expr.expr array ) = + create ctx (Z3native.mk_distinct (context_gno ctx) (Array.length args) (Expr.aton args)) + + (** + Mk an expression representing not(a). + *) + let mk_not ( ctx : context ) ( a : bool_expr ) = + create ctx (Z3native.mk_not (context_gno ctx) (gno a)) + + (** + 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 ctx (Z3native.mk_ite (context_gno ctx) (gno t1) (gno t2) (gno t3)) + + (** + Create an expression representing t1 iff t2. + *) + let mk_iff ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = + create ctx (Z3native.mk_iff (context_gno ctx) (gno t1) (gno t2)) + + (** + Create an expression representing t1 -> t2. + *) + let mk_implies ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = + create ctx (Z3native.mk_implies (context_gno ctx) (gno t1) (gno t2)) + (** + Create an expression representing t1 xor t2. + *) + let mk_xor ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = + create ctx (Z3native.mk_xor (context_gno ctx) (gno t1) (gno t2)) + + (** + Create an expression representing the AND of args + *) + let mk_and ( ctx : context ) ( args : bool_expr array ) = + create ctx (Z3native.mk_and (context_gno ctx) (Array.length args) (aton args)) + + (** + Create an expression representing the OR of args + *) + let mk_or ( ctx : context ) ( args : bool_expr array ) = + create ctx (Z3native.mk_or (context_gno ctx) (Array.length args) (aton args)) end (** Quantifier expressions *) -module Quantifiers = -struct +and Quantifiers : +sig + type quantifier = Quantifier of Expr.expr + + val create : context -> Z3native.ptr -> quantifier +end = struct + type quantifier = Quantifier of Expr.expr + + let create ( ctx : context ) ( no : Z3native.ptr ) = + let a = (AST.create ctx no) in + Quantifier(Expr.Expr(a)) + + let gc ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gc e) + let gnc ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gnc e) + let gno ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gno e) + + (** The de-Burijn index of a bound variable. @@ -1838,11 +1551,11 @@ struct 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 + let get_index ( x : Expr.expr ) = + if not (AST.is_var (match x with Expr.Expr(a) -> a)) then raise (Z3native.Exception "Term is not a bound variable.") else - Z3native.get_index_value x#gnc x#gno + Z3native.get_index_value (Expr.gnc x) (Expr.gno x) (** Quantifier patterns @@ -1850,33 +1563,57 @@ struct non-empty. If the list comprises of more than one term, it is also called a multi-pattern. *) - module Pattern = - struct + module Patterns : + sig + type pattern = Pattern of AST.ast + + val create : context -> Z3native.ptr -> pattern + val aton : pattern array -> Z3native.ptr array + end = struct + type pattern = Pattern of AST.ast + + let create ( ctx : context ) ( no : Z3native.ptr ) = + let res = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = Z3native.inc_ref ; + dec_ref = Z3native.dec_ref } in + (z3obj_sno res ctx no) ; + (z3obj_create res) ; + Pattern(res) + + let gc ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gc a) + let gnc ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gnc a) + let gno ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gno a) + (** The number of terms in the pattern. *) let get_num_terms ( x : pattern ) = - Z3native.get_pattern_num_terms x#gnc x#gno + Z3native.get_pattern_num_terms (gnc x) (gno x) (** 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 + let f i = (Expr.create (gc x) (Z3native.get_pattern (gnc x) (gno x) 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 + let to_string ( x : pattern ) = Z3native.pattern_to_string (gnc x) (gno x) + + let aton (a : pattern array) = + let f (e : pattern) = (gno e) in + Array.map f a end (** Indicates whether the quantifier is universal. *) let is_universal ( x : quantifier ) = - Z3native.is_quantifier_forall x#gnc x#gno + Z3native.is_quantifier_forall (gnc x) (gno x) (** Indicates whether the quantifier is existential. @@ -1886,45 +1623,45 @@ struct (** The weight of the quantifier. *) - let get_weight ( x : quantifier ) = Z3native.get_quantifier_weight x#gnc x#gno + let get_weight ( x : quantifier ) = Z3native.get_quantifier_weight (gnc x) (gno x) (** The number of patterns. *) - let get_num_patterns ( x : quantifier ) = Z3native.get_quantifier_num_patterns x#gnc x#gno + let get_num_patterns ( x : quantifier ) = Z3native.get_quantifier_num_patterns (gnc x) (gno x) (** 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 + let f i = (Patterns.create (gc x) (Z3native.get_quantifier_pattern_ast (gnc x) (gno x) 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 + let get_num_no_patterns ( x : quantifier ) = Z3native.get_quantifier_num_no_patterns (gnc x) (gno x) (** 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 + let f i = (Patterns.create (gc x) (Z3native.get_quantifier_no_pattern_ast (gnc x) (gno x) 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 + let get_num_bound ( x : quantifier ) = Z3native.get_quantifier_num_bound (gnc x) (gno x) (** The symbols for the bound variables. *) let get_bound_variable_names ( x : quantifier ) = let n = (get_num_bound x) in - let f i = (Symbol.create x#gc (Z3native.get_quantifier_bound_name x#gnc x#gno i)) in + let f i = (Symbol.create (gc x) (Z3native.get_quantifier_bound_name (gnc x) (gno x) i)) in Array.init n f (** @@ -1932,31 +1669,31 @@ struct *) 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 + let f i = (Sort.create (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) 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) + Booleans.create (gc x) (Z3native.get_quantifier_body (gnc x) (gno x)) (** 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 (context_gno ctx) index ty#gno) + let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) = + Expr.create ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) (** Create a quantifier pattern. *) - let mk_pattern ( ctx : context ) ( terms : expr array ) = + let mk_pattern ( ctx : context ) ( terms : Expr.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 (context_gno ctx) (Array.length terms) (astaton terms)) + Patterns.create ctx (Z3native.mk_pattern (context_gno ctx) (Array.length terms) (Expr.aton terms)) (** Create a universal Quantifier. @@ -1977,95 +1714,96 @@ struct @param quantifierID optional symbol to track quantifier. @param skolemID optional symbol to track skolem constants. *) - let mk_forall ( ctx : context ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : pattern array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_forall ( ctx : context ) ( sorts : Sort.sort array ) ( names : Symbol.symbol array ) ( body : Expr.expr ) ( weight : int option ) ( patterns : Patterns.pattern array ) ( nopatterns : Expr.expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (Array.length sorts) != (Array.length names) then raise (Z3native.Exception "Number of sorts does not match number of names") else if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (Array.length patterns) (patternaton patterns) - (Array.length sorts) (astaton sorts) - (Symbol.aton names) - body#gno) + create ctx (Z3native.mk_quantifier (context_gno ctx) true + (match weight with | None -> 1 | Some(x) -> x) + (Array.length patterns) (Patterns.aton patterns) + (Array.length sorts) (Sort.aton sorts) + (Symbol.aton names) + (Expr.gno body)) else - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_ex (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (Array.length patterns) (patternaton patterns) - (Array.length nopatterns) (patternaton nopatterns) - (Array.length sorts) (astaton sorts) - (Symbol.aton names) - body#gno) + create ctx (Z3native.mk_quantifier_ex (context_gno ctx) true + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (Array.length patterns) (Patterns.aton patterns) + (Array.length nopatterns) (Expr.aton nopatterns) + (Array.length sorts) (Sort.aton sorts) + (Symbol.aton names) + (Expr.gno body)) (** Create a universal Quantifier. *) - let mk_forall_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : pattern array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_forall_const ( ctx : context ) ( bound_constants : Expr.expr array ) ( body : Expr.expr ) ( weight : int option ) ( patterns : Patterns.pattern array ) ( nopatterns : Expr.expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (Array.length bound_constants) (expraton bound_constants) - (Array.length patterns) (patternaton patterns) - body#gno) + create ctx (Z3native.mk_quantifier_const (context_gno ctx) true + (match weight with | None -> 1 | Some(x) -> x) + (Array.length bound_constants) (Expr.aton bound_constants) + (Array.length patterns) (Patterns.aton patterns) + (Expr.gno body)) else - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const_ex (context_gno ctx) true - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (Array.length bound_constants) (expraton bound_constants) - (Array.length patterns) (patternaton patterns) - (Array.length nopatterns) (patternaton nopatterns) - body#gno) + create ctx (Z3native.mk_quantifier_const_ex (context_gno ctx) true + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (Array.length bound_constants) (Expr.aton bound_constants) + (Array.length patterns) (Patterns.aton patterns) + (Array.length nopatterns) (Expr.aton nopatterns) + (Expr.gno body)) + (** Create an existential Quantifier. *) - let mk_exists ( ctx : context ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : pattern array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_exists ( ctx : context ) ( sorts : Sort.sort array ) ( names : Symbol.symbol array ) ( body : Expr.expr ) ( weight : int option ) ( patterns : Patterns.pattern array ) ( nopatterns : Expr.expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (Array.length sorts) != (Array.length names) then raise (Z3native.Exception "Number of sorts does not match number of names") else if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (Array.length patterns) (patternaton patterns) - (Array.length sorts) (astaton sorts) - (Symbol.aton names) - body#gno) + create ctx (Z3native.mk_quantifier (context_gno ctx) false + (match weight with | None -> 1 | Some(x) -> x) + (Array.length patterns) (Patterns.aton patterns) + (Array.length sorts) (Sort.aton sorts) + (Symbol.aton names) + (Expr.gno body)) else - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_ex (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (Array.length patterns) (patternaton patterns) - (Array.length nopatterns) (patternaton nopatterns) - (Array.length sorts) (astaton sorts) - (Symbol.aton names) - body#gno) - + create ctx (Z3native.mk_quantifier_ex (context_gno ctx) false + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (Array.length patterns) (Patterns.aton patterns) + (Array.length nopatterns) (Expr.aton nopatterns) + (Array.length sorts) (Sort.aton sorts) + (Symbol.aton names) + (Expr.gno body)) + (** Create an existential Quantifier. *) - let mk_exists_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : pattern array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_exists_const ( ctx : context ) ( bound_constants : Expr.expr array ) ( body : Expr.expr ) ( weight : int option ) ( patterns : Patterns.pattern array ) ( nopatterns : Expr.expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (Array.length bound_constants) (expraton bound_constants) - (Array.length patterns) (patternaton patterns) - body#gno) + create ctx (Z3native.mk_quantifier_const (context_gno ctx) false + (match weight with | None -> 1 | Some(x) -> x) + (Array.length bound_constants) (Expr.aton bound_constants) + (Array.length patterns) (Patterns.aton patterns) + (Expr.gno body)) else - (new quantifier ctx)#cnstr_obj (Z3native.mk_quantifier_const_ex (context_gno ctx) false - (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) - (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) - (Array.length bound_constants) (expraton bound_constants) - (Array.length patterns) (patternaton patterns) - (Array.length nopatterns) (patternaton nopatterns) - body#gno) + create ctx (Z3native.mk_quantifier_const_ex (context_gno ctx) false + (match weight with | None -> 1 | Some(x) -> x) + (match quantifier_id with | None -> null | Some(x) -> (Symbol.gno x)) + (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x)) + (Array.length bound_constants) (Expr.aton bound_constants) + (Array.length patterns) (Patterns.aton patterns) + (Array.length nopatterns) (Expr.aton nopatterns) + (Expr.gno body)) (** Create a Quantifier. *) - let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : pattern array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : Sort.sort array ) ( names : Symbol.symbol array ) ( body : Expr.expr ) ( weight : int option ) ( patterns : Patterns.pattern array ) ( nopatterns : Expr.expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (universal) then (mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id) else @@ -2075,7 +1813,7 @@ struct (** Create a Quantifier. *) - let mk_quantifier ( ctx : context ) ( universal : bool ) ( bound_constants : expr array ) ( body : expr) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : pattern array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = + let mk_quantifier ( ctx : context ) ( universal : bool ) ( bound_constants : Expr.expr array ) ( body : Expr.expr ) ( weight : int option ) ( patterns : Patterns.pattern array ) ( nopatterns : Expr.expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (universal) then mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id else @@ -2083,75 +1821,104 @@ struct end (** Functions to manipulate Array expressions *) -module Arrays = -struct +and Arrays : +sig + type array_expr = ArrayExpr of Expr.expr + type array_sort = ArraySort of Sort.sort + + val create_expr : context -> Z3native.ptr -> array_expr +end = struct + type array_expr = ArrayExpr of Expr.expr + type array_sort = ArraySort of Sort.sort + + let create_expr ( ctx : context ) ( no : Z3native.ptr ) = + let e = (Expr.create ctx no) in + ArrayExpr(e) + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = + let s = (Sort.create ctx no) in + ArraySort(s) + + let sgc ( x : array_sort ) = match (x) with ArraySort(Sort.Sort(s)) -> (z3obj_gc s) + let sgnc ( x : array_sort ) = match (x) with ArraySort(Sort.Sort(s)) -> (z3obj_gnc s) + let sgno ( x : array_sort ) = match (x) with ArraySort(Sort.Sort(s)) -> (z3obj_gno s) + + let egc ( x : array_expr ) = match (x) with ArrayExpr(Expr.Expr(e)) -> (z3obj_gc e) + let egnc ( x : array_expr ) = match (x) with ArrayExpr(Expr.Expr(e)) -> (z3obj_gnc e) + let egno ( x : array_expr ) = match (x) with ArrayExpr(Expr.Expr(e)) -> (z3obj_gno e) + + let aton (a : array_expr array) = + let f (e : array_expr) = (egno e) in + Array.map f a + + (** Create a new array sort. *) - let mk_sort ( ctx : context ) domain range = - (new array_sort ctx)#cnstr_dr domain range + let mk_sort ( ctx : context ) ( domain : Sort.sort ) ( range : Sort.sort ) = + create_sort ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno 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. *) - let is_store ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) + let is_store ( x : Expr.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 (Expr.get_func_decl x) == OP_SELECT) + let is_select ( x : Expr.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. *) - let is_constant_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONST_ARRAY) + let is_constant_array ( x : Expr.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. *) - let is_default_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_DEFAULT) + let is_default_array ( x : Expr.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. *) - let is_array_map ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_MAP) + let is_array_map ( x : Expr.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. *) - let is_as_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) + let is_as_array ( x : Expr.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 ) = - (Z3native.is_app x#gnc x#gno) && - ((sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno))) == ARRAY_SORT) + let is_array ( x : Expr.expr ) = + (Z3native.is_app (Expr.gnc x) (Expr.gno x)) && + ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == 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) + let get_domain ( x : array_sort ) = Sort.create (sgc x) (Z3native.get_array_sort_domain (sgnc x) (sgno x)) (** 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) + let get_range ( x : array_sort ) = Sort.create (sgc x) (Z3native.get_array_sort_range (sgnc x) (sgno x)) (** Create an array constant. *) - let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort ) ( range : sort ) = - ((Expr.mk_const ctx name ((mk_sort ctx domain range) :> sort)) :> array_expr) + let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort ) ( range : Sort.sort ) = + ArrayExpr(Expr.mk_const ctx name (match (mk_sort ctx domain range) with ArraySort(s) -> s)) (** Create an array constant. *) - let mk_const_s ( ctx : context ) ( name : string ) ( domain : sort ) ( range : sort ) = + let mk_const_s ( ctx : context ) ( name : string ) ( domain : Sort.sort ) ( range : Sort.sort ) = mk_const ctx (Symbol.mk_string ctx name) domain range (** @@ -2166,8 +1933,8 @@ struct *) - let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) = - ((create_expr ctx (Z3native.mk_select (context_gno ctx) a#gno i#gno)) :> array_expr) + let mk_select ( ctx : context ) ( a : array_expr ) ( i : Expr.expr ) = + create_expr ctx (Z3native.mk_select (context_gno ctx) (egno a) (Expr.gno i)) (** Array update. @@ -2185,8 +1952,8 @@ struct *) - let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) ( v : expr) = - (new array_expr ctx)#cnstr_obj (Z3native.mk_store (context_gno ctx) a#gno i#gno v#gno) + let mk_select ( ctx : context ) ( a : array_expr ) ( i : Expr.expr ) ( v : Expr.expr ) = + create_expr ctx (Z3native.mk_store (context_gno ctx) (egno a) (Expr.gno i) (Expr.gno v)) (** Create a constant array. @@ -2196,8 +1963,8 @@ struct *) - let mk_const_array ( ctx : context ) ( domain : sort ) ( v : expr ) = - (new array_expr ctx)#cnstr_obj (Z3native.mk_const_array (context_gno ctx) domain#gno v#gno) + let mk_const_array ( ctx : context ) ( domain : Sort.sort ) ( v : Expr.expr ) = + create_expr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v)) (** Maps f on the argument arrays. @@ -2209,8 +1976,8 @@ struct *) - let mk_map ( ctx : context ) ( f : func_decl ) ( args : array_expr array ) = - ((create_expr ctx (Z3native.mk_map (context_gno ctx) f#gno (Array.length args) (astaton args))) :> array_expr) + let mk_map ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : array_expr array ) = + create_expr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (Array.length args) (aton args)) (** Access the array default value. @@ -2219,149 +1986,184 @@ struct finite maps with a default range value. *) let mk_term_array ( ctx : context ) ( arg : array_expr ) = - ((create_expr ctx (Z3native.mk_array_default (context_gno ctx) arg#gno)) :> array_expr) + create_expr ctx (Z3native.mk_array_default (context_gno ctx) (egno arg)) end (** Functions to manipulate Set expressions *) -module Sets = -struct +and Sets : +sig + type set_sort = SetSort of Sort.sort + +end = struct + type set_sort = SetSort of Sort.sort + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = + let s = (Sort.create ctx no) in + SetSort(s) + (** Indicates whether the term is set union *) - let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) + let is_union ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) (** Indicates whether the term is set intersection *) - let is_intersect ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) + let is_intersect ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) (** Indicates whether the term is set difference *) - let is_difference ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) + let is_difference ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) (** Indicates whether the term is set complement *) - let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) + let is_complement ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) (** Indicates whether the term is set subset *) - let is_subset ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) + let is_subset ( x : Expr.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 + let mk_sort ( ctx : context ) ( ty : Sort.sort ) = + create_sort ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty)) (** Create an empty set. *) - let mk_empty ( ctx : context ) ( domain : sort ) = - (create_expr ctx (Z3native.mk_empty_set (context_gno ctx) domain#gno)) + let mk_empty ( ctx : context ) ( domain : Sort.sort ) = + (Expr.create ctx (Z3native.mk_empty_set (context_gno ctx) (Sort.gno domain))) (** Create the full set. *) - let mk_full ( ctx : context ) ( domain : sort ) = - create_expr ctx (Z3native.mk_full_set (context_gno ctx) domain#gno) + let mk_full ( ctx : context ) ( domain : Sort.sort ) = + Expr.create ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain)) (** Add an element to the set. *) - let mk_set_add ( ctx : context ) ( set : expr ) ( element : expr ) = - create_expr ctx (Z3native.mk_set_add (context_gno ctx) set#gno element#gno) + let mk_set_add ( ctx : context ) ( set : Expr.expr ) ( element : Expr.expr ) = + Expr.create ctx (Z3native.mk_set_add (context_gno ctx) (Expr.gno set) (Expr.gno element)) (** Remove an element from a set. *) - let mk_del ( ctx : context ) ( set : expr ) ( element : expr ) = - create_expr ctx (Z3native.mk_set_del (context_gno ctx) set#gno element#gno) + let mk_del ( ctx : context ) ( set : Expr.expr ) ( element : Expr.expr ) = + Expr.create ctx (Z3native.mk_set_del (context_gno ctx) (Expr.gno set) (Expr.gno element)) (** Take the union of a list of sets. *) - let mk_union ( ctx : context ) ( args : expr array ) = - create_expr ctx (Z3native.mk_set_union (context_gno ctx) (Array.length args) (astaton args)) + let mk_union ( ctx : context ) ( args : Expr.expr array ) = + Expr.create ctx (Z3native.mk_set_union (context_gno ctx) (Array.length args) (Expr.aton args)) (** Take the intersection of a list of sets. *) - let mk_intersection ( ctx : context ) ( args : expr array ) = - create_expr ctx (Z3native.mk_set_intersect (context_gno ctx) (Array.length args) (astaton args)) + let mk_intersection ( ctx : context ) ( args : Expr.expr array ) = + Expr.create ctx (Z3native.mk_set_intersect (context_gno ctx) (Array.length args) (Expr.aton args)) (** Take the difference between two sets. *) - let mk_difference ( ctx : context ) ( arg1 : expr ) ( arg2 : expr) = - create_expr ctx (Z3native.mk_set_difference (context_gno ctx) arg1#gno arg2#gno) + let mk_difference ( ctx : context ) ( arg1 : Expr.expr ) ( arg2 : Expr.expr ) = + Expr.create ctx (Z3native.mk_set_difference (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) (** Take the complement of a set. *) - let mk_complement ( ctx : context ) ( arg : expr ) = - create_expr ctx (Z3native.mk_set_complement (context_gno ctx) arg#gno) + let mk_complement ( ctx : context ) ( arg : Expr.expr ) = + Expr.create ctx (Z3native.mk_set_complement (context_gno ctx) (Expr.gno arg)) (** Check for set membership. *) - let mk_membership ( ctx : context ) ( elem : expr ) ( set : expr ) = - create_expr ctx (Z3native.mk_set_member (context_gno ctx) elem#gno set#gno) + let mk_membership ( ctx : context ) ( elem : Expr.expr ) ( set : Expr.expr ) = + Expr.create ctx (Z3native.mk_set_member (context_gno ctx) (Expr.gno elem) (Expr.gno set)) (** Check for subsetness of sets. *) - let mk_subset ( ctx : context ) ( arg1 : expr ) ( arg2 : expr) = - create_expr ctx (Z3native.mk_set_subset (context_gno ctx) arg1#gno arg2#gno) + let mk_subset ( ctx : context ) ( arg1 : Expr.expr ) ( arg2 : Expr.expr ) = + Expr.create ctx (Z3native.mk_set_subset (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) end (** Functions to manipulate Finite Domain expressions *) -module FiniteDomains = -struct - (** - Create a new finite domain sort. - *) - let mk_sort ( ctx : context ) ( name : Symbol.symbol ) size = - (new finite_domain_sort ctx)#cnstr_si name size +and FiniteDomains : +sig + type finite_domain_sort = FiniteDomainSort of Sort.sort + +end = struct + type finite_domain_sort = FiniteDomainSort of Sort.sort + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = + let s = (Sort.create ctx no) in + FiniteDomainSort(s) + + let gc ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort.Sort(s)) -> (z3obj_gc s) + let gnc ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort.Sort(s)) -> (z3obj_gnc s) + let gno ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort.Sort(s))-> (z3obj_gno s) (** 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) size + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) = + create_sort ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size) + + (** + Create a new finite domain sort. + *) + let mk_sort_s ( ctx : context ) ( name : string ) ( size : int ) = + mk_sort ctx (Symbol.mk_string ctx name) size (** Indicates whether the term is of an array sort. *) - let is_finite_domain ( x : expr ) = - (Z3native.is_app x#gnc x#gno) && - (sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno)) == FINITE_DOMAIN_SORT) + let is_finite_domain ( x : Expr.expr ) = + (Z3native.is_app (Expr.gnc x) (Expr.gno x)) && + (sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x))) == 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) + let is_lt ( x : Expr.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 + let get_size ( x : finite_domain_sort ) = + let (r, v) = (Z3native.get_finite_domain_sort_size (gnc x) (gno x)) in if r then v else raise (Z3native.Exception "Conversion failed.") end (** Functions to manipulate Relation expressions *) -module Relations = -struct +and Relations : +sig + type relation_sort = RelationSort of Sort.sort + +end = struct + type relation_sort = RelationSort of Sort.sort + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = + let s = (Sort.create ctx no) in + RelationSort(s) + + let gc ( x : relation_sort ) = match (x) with RelationSort(Sort.Sort(s)) -> (z3obj_gc s) + let gnc ( x : relation_sort ) = match (x) with RelationSort(Sort.Sort(s)) -> (z3obj_gnc s) + let gno ( x : relation_sort ) = match (x) with RelationSort(Sort.Sort(s))-> (z3obj_gno s) + (** Indicates whether the term is of a relation sort. *) - let is_relation ( x : expr ) = - ((Z3native.is_app x#gnc x#gno) && - (sort_kind_of_int (Z3native.get_sort_kind x#gnc (Z3native.get_sort x#gnc x#gno)) == RELATION_SORT)) + let is_relation ( x : Expr.expr ) = + ((Z3native.is_app (Expr.gnc x) (Expr.gno x)) && + (sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x))) == RELATION_SORT)) (** Indicates whether the term is an relation store @@ -2370,40 +2172,40 @@ struct 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) + let is_store ( x : Expr.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) + let is_empty ( x : Expr.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) + let is_is_empty ( x : Expr.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) + let is_join ( x : Expr.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) + let is_union ( x : Expr.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) + let is_widen ( x : Expr.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) + let is_project ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_PROJECT) (** Indicates whether the term is a relation filter @@ -2414,7 +2216,7 @@ struct 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) + let is_filter ( x : Expr.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. @@ -2429,7 +2231,7 @@ struct 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) + let is_negation_filter ( x : Expr.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 @@ -2437,12 +2239,12 @@ struct 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) + let is_rename ( x : Expr.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) + let is_complement ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_COMPLEMENT) (** Indicates whether the term is a relational select @@ -2451,7 +2253,7 @@ struct 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) + let is_select ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT) (** Indicates whether the term is a relational clone (copy) @@ -2462,38 +2264,153 @@ struct 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) + let is_clone ( x : Expr.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 + let get_arity ( x : relation_sort ) = Z3native.get_relation_arity (gnc x) (gno x) (** The sorts of the columns of the relation sort. *) - let get_column_sorts (x : 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 + let f i = (create_sort (gc x) (Z3native.get_relation_column (gnc x) (gno x) i)) in Array.init n f end (** Functions to manipulate Datatype expressions *) -module Datatypes = -struct +and Datatypes : +sig + type datatype_expr = DatatypeExpr of Expr.expr + type datatype_sort = DatatypeSort of Sort.sort + + val create_expr : context -> Z3native.ptr -> datatype_expr +end = struct + type datatype_expr = DatatypeExpr of Expr.expr + type datatype_sort = DatatypeSort of Sort.sort + + let create_expr ( ctx : context ) ( no : Z3native.ptr ) = + let e = (Expr.create ctx no) in + DatatypeExpr(e) + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = + let s = (Sort.create ctx no) in + DatatypeSort(s) + + let sgc ( x : datatype_sort ) = match (x) with DatatypeSort(Sort.Sort(s)) -> (z3obj_gc s) + let sgnc ( x : datatype_sort ) = match (x) with DatatypeSort(Sort.Sort(s)) -> (z3obj_gnc s) + let sgno ( x : datatype_sort ) = match (x) with DatatypeSort(Sort.Sort(s))-> (z3obj_gno s) + + (** Constructors *) module Constructor = struct + type constructor_extra = { + m_n : int; + mutable m_tester_decl : FuncDecl.func_decl option; + mutable m_constructor_decl : FuncDecl.func_decl option ; + mutable m_accessor_decls : FuncDecl.func_decl array option} + type constructor = Constructor of (z3_native_object * constructor_extra) + + let create_ssssi ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( sort_refs : int array ) = + let n = (Array.length field_names) in + if n != (Array.length sorts) then + raise (Z3native.Exception "Number of field names does not match number of sorts") + else + if n != (Array.length sort_refs) then + raise (Z3native.Exception "Number of field names does not match number of sort refs") + else + let ptr = (Z3native.mk_constructor (context_gno ctx) (Symbol.gno name) + (Symbol.gno recognizer) + n + (Symbol.aton field_names) + (Sort.aton sorts) + sort_refs) in + let no : z3_native_object = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = z3obj_nil_ref ; + dec_ref = z3obj_nil_ref} in + let ex : constructor_extra = { m_n = n; + m_tester_decl = None; + m_constructor_decl = None; + m_accessor_decls = None} in + (z3obj_sno no ctx ptr) ; + (z3obj_create no) ; + let f = fun o -> Z3native.del_constructor (z3obj_gnc o) (z3obj_gno o) in + Gc.finalise f no ; + Constructor(no, ex) + + let init_extra ( x : constructor ) = + match x with Constructor(no, ex) -> + match ex.m_tester_decl with + | None -> + let (a, b, c) = (Z3native.query_constructor (z3obj_gnc no) (z3obj_gno no) ex.m_n) in + ex.m_constructor_decl <- Some (FuncDecl.create (z3obj_gc no) a) ; + ex.m_tester_decl <- Some (FuncDecl.create (z3obj_gc no) b) ; + ex.m_accessor_decls <- Some (let f e = (FuncDecl.create (z3obj_gc no) e) in Array.map f c) ; + () + | _ -> () + + let get_n ( x : constructor ) = + match x with Constructor(no, ex) -> + ex.m_n + + let rec tester_decl ( x : constructor ) = + match x with Constructor(no, ex) -> + match ex.m_tester_decl with + | Some(s) -> s + | None -> init_extra x ; tester_decl x + + let rec constructor_decl ( x : constructor ) = + match x with Constructor(no, ex) -> + match ex.m_constructor_decl with + | Some(s) -> s + | None -> init_extra x ; constructor_decl x + + let rec accessor_decls ( x : constructor ) = + match x with Constructor(no, ex) -> + match ex.m_accessor_decls with + | Some(s) -> s + | None -> init_extra x ; accessor_decls x + + let aton ( a : constructor array ) = + let f (e : constructor) = match e with Constructor(no, ex) -> (z3obj_gno no)in + Array.map f a + + (** The number of fields of the constructor. *) - let get_num_fields ( x : constructor ) = x#get_n + let get_num_fields ( x : constructor ) = get_n x (** The function declaration of the constructor. *) - let get_constructor_decl ( x : constructor ) = x#constructor_decl + let get_constructor_decl ( x : constructor ) = constructor_decl x (** The function declaration of the tester. *) - let get_tester_decl ( x : constructor ) = x#tester_decl + let get_tester_decl ( x : constructor ) = tester_decl x (** The function declarations of the accessors *) - let get_accessor_decls ( x : constructor ) = x#accessor_decls + let get_accessor_decls ( x : constructor ) = accessor_decls x end + (** Constructor list objects *) + module ConstructorList = + struct + type constructor_list = z3_native_object + + let create ( ctx : context )( c : Constructor.constructor array ) = + let res : constructor_list = { m_ctx = ctx ; + m_n_obj = null ; + inc_ref = z3obj_nil_ref ; + dec_ref = z3obj_nil_ref} in + (z3obj_sno res ctx (Z3native.mk_constructor_list (context_gno ctx) (Array.length c) (Constructor.aton c))) ; + (z3obj_create res) ; + let f = fun o -> Z3native.del_constructor_list (z3obj_gnc o) (z3obj_gno o) in + Gc.finalise f res; + res + + let aton (a : constructor_list array) = + let f (e : constructor_list) = (z3obj_gno e) in + Array.map f a + end + (* DATATYPES *) (** Create a datatype constructor. @@ -2505,8 +2422,8 @@ struct 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.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : sort array ) ( sort_refs : int array) = - (new constructor ctx)#cnstr_ssssi name recognizer field_names sorts sort_refs + let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( sort_refs : int array) = + Constructor.create_ssssi ctx name recognizer field_names sorts sort_refs (** @@ -2519,20 +2436,21 @@ struct 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.symbol ) ( field_names : Symbol.symbol array ) ( sorts : sort array ) ( sort_refs : int array ) = + let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( sort_refs : int array ) = mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs (** Create a new datatype sort. *) - let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : constructor array) = - (new datatype_sort ctx)#cnstr_sc name constructors + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : Constructor.constructor array) = + let (x,_) = (Z3native.mk_datatype (context_gno ctx) (Symbol.gno name) (Array.length constructors) (Constructor.aton constructors)) in + create_sort ctx x (** Create a new datatype sort. *) - let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : constructor array) = + let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : Constructor.constructor array ) = mk_sort ctx (Symbol.mk_string ctx name) constructors (** @@ -2540,16 +2458,16 @@ struct @param names names of datatype sorts @param c list of constructors, one list per sort. *) - let mk_sorts ( ctx : context ) ( names : Symbol.symbol array ) ( c : constructor array array ) = + let mk_sorts ( ctx : context ) ( names : Symbol.symbol array ) ( c : Constructor.constructor array array ) = let n = (Array.length names) in - let f e = ( (new constructor_list ctx)#cnstr_ca e ) in + let f e = (ConstructorList.create ctx e) in let cla = (Array.map f c) in - let (r, a) = (Z3native.mk_datatypes (context_gno ctx) n (Symbol.aton names) (constructor_listaton cla)) in - let g e = ( (new datatype_sort ctx)#cnstr_obj e) in + let (r, a) = (Z3native.mk_datatypes (context_gno ctx) n (Symbol.aton names) (ConstructorList.aton cla)) in + let g e = (create_sort ctx e) in (Array.map g r) (** Create mutually recursive data-types. *) - let mk_sorts_s ( ctx : context ) ( names : string array ) ( c : constructor array array ) = + let mk_sorts_s ( ctx : context ) ( names : string array ) ( c : Constructor.constructor array array ) = mk_sorts ctx ( let f e = (Symbol.mk_string ctx e) in @@ -2558,130 +2476,230 @@ struct 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 + let get_num_constructors ( x : datatype_sort ) = Z3native.get_datatype_sort_num_constructors (sgnc x) (sgno x) (** The range of the array sort. *) - let get_constructors (x : datatype_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 + let f i = FuncDecl.create (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) i) in Array.init n f (** The recognizers. *) - let get_recognizers (x : datatype_sort) = + 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 + let f i = FuncDecl.create (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) i) in Array.init n f (** The constructor accessors. *) - let get_accessors (x : datatype_sort) = + 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 + let fd = FuncDecl.create (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) i) in + let ds = Z3native.get_domain_size (FuncDecl.gnc fd) (FuncDecl.gno fd) in + let g j = FuncDecl.create (sgc x) (Z3native.get_datatype_sort_constructor_accessor (sgnc x) (sgno x) 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 +and Enumerations : +sig + type enum_sort_data + type enum_sort = EnumSort of (Sort.sort * enum_sort_data) +end = struct + type enum_sort_data = { mutable _constdecls : FuncDecl.func_decl array ; + mutable _testerdecls : FuncDecl.func_decl array } + type enum_sort = EnumSort of (Sort.sort * enum_sort_data) + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) ( cdecls : Z3native.z3_func_decl array ) ( tdecls : Z3native.z3_func_decl array ) = + let s = (Sort.create ctx no) in + let e = { _constdecls = (let f e = FuncDecl.create ctx e in (Array.map f cdecls)) ; + _testerdecls = (let f e = FuncDecl.create ctx e in (Array.map f tdecls)) } in + EnumSort(s, e) + + let sgc ( x : enum_sort ) = match (x) with EnumSort(Sort.Sort(s),_) -> (z3obj_gc s) + let sgnc ( x : enum_sort ) = match (x) with EnumSort(Sort.Sort(s),_) -> (z3obj_gnc s) + let sgno ( x : enum_sort ) = match (x) with EnumSort(Sort.Sort(s),_)-> (z3obj_gno s) + (** Create a new enumeration sort. *) - let mk_sort_s ( ctx : context ) name enum_names = - (new enum_sort ctx)#cnstr_ss - (Symbol.mk_string ctx name) - (Symbol.mk_strings ctx enum_names) + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( enum_names : Symbol.symbol array ) = + let (a, b, c) = (Z3native.mk_enumeration_sort (context_gno ctx) (Symbol.gno name) (Array.length enum_names) (Symbol.aton enum_names)) in + create_sort ctx a b c + + (** + Create a new enumeration sort. + *) + let mk_sort_s ( ctx : context ) ( name : string ) ( enum_names : string array ) = + mk_sort ctx (Symbol.mk_string ctx name) (Symbol.mk_strings ctx enum_names) (** The function declarations of the constants in the enumeration. *) - let get_const_decls (x : enum_sort) = x#const_decls + let get_const_decls ( x : enum_sort ) = match x with EnumSort(_,ex) -> ex._constdecls (** The test predicates for the constants in the enumeration. *) - let get_tester_decls (x : enum_sort) = x#tester_decls + let get_tester_decls ( x : enum_sort ) = match x with EnumSort(_,ex) -> ex._testerdecls end (** Functions to manipulate List expressions *) -module Lists = -struct - (** - Create a new list sort. - *) - let mk_sort ( ctx : context ) (name : Symbol.symbol) elem_sort = - (new list_sort ctx)#cnstr_ss name elem_sort +and Lists : +sig + type list_sort_data + type list_sort = ListSort of (Sort.sort * list_sort_data) - (** - Create a new list sort. - *) +end = struct + type list_sort_data = { _nildecl : FuncDecl.func_decl ; + _is_nildecl : FuncDecl.func_decl ; + _consdecl : FuncDecl.func_decl ; + _is_consdecl : FuncDecl.func_decl ; + _headdecl : FuncDecl.func_decl ; + _taildecl : FuncDecl.func_decl } + type list_sort = ListSort of (Sort.sort * list_sort_data) + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) ( nildecl : Z3native.ptr ) ( is_nildecl : Z3native.ptr ) ( consdecl : Z3native.ptr ) ( is_consdecl : Z3native.ptr ) ( headdecl : Z3native.ptr ) ( taildecl : Z3native.ptr ) = + let s = (Sort.create ctx no) in + let e = {_nildecl = FuncDecl.create ctx nildecl; + _is_nildecl = FuncDecl.create ctx is_nildecl; + _consdecl = FuncDecl.create ctx consdecl; + _is_consdecl = FuncDecl.create ctx is_consdecl; + _headdecl = FuncDecl.create ctx headdecl; + _taildecl = FuncDecl.create ctx taildecl} in + ListSort(s, e) + + let sgc ( x : list_sort ) = match (x) with ListSort(Sort.Sort(s),_) -> (z3obj_gc s) + let sgnc ( x : list_sort ) = match (x) with ListSort(Sort.Sort(s),_) -> (z3obj_gnc s) + let sgno ( x : list_sort ) = match (x) with ListSort(Sort.Sort(s),_)-> (z3obj_gno s) + + + (** Create a new list sort. *) + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : Sort.sort ) = + let (r, a, b, c, d, e, f) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) (Sort.gno elem_sort)) in + create_sort ctx r a b c d e f + + (** Create a new list sort. *) let mk_list_s ( ctx : context ) (name : string) elem_sort = mk_sort ctx (Symbol.mk_string ctx name) elem_sort (** The declaration of the nil function of this list sort. *) - let get_nil_decl (x : list_sort) = x#nil_decl + let get_nil_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._nildecl (** The declaration of the isNil function of this list sort. *) - let get_is_nil_decl (x : list_sort) = x#is_nil_decl + let get_is_nil_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._is_nildecl (** The declaration of the cons function of this list sort. *) - let get_cons_decl (x : list_sort) = x#cons_decl + let get_cons_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._consdecl (** The declaration of the isCons function of this list sort. *) - let get_is_cons_decl (x : list_sort) = x#is_cons_decl + let get_is_cons_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._is_consdecl (** The declaration of the head function of this list sort. *) - let get_head_decl (x : list_sort) = x#head_decl + let get_head_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._headdecl (** The declaration of the tail function of this list sort. *) - let get_tail_decl (x : list_sort) = x#tail_decl + let get_tail_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._taildecl (** The empty list. *) - let nil (x : list_sort) = create_expr_fa x#gc (get_nil_decl x) [||] + let nil ( x : list_sort ) = Expr.create_fa (sgc x) (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 +and Tuples : +sig + type tuple_sort = TupleSort of Sort.sort +end = struct + type tuple_sort = TupleSort of Sort.sort + + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = + let s = (Sort.create ctx no) in + TupleSort(s) + + let sgc ( x : tuple_sort ) = match (x) with TupleSort(Sort.Sort(s)) -> (z3obj_gc s) + let sgnc ( x : tuple_sort ) = match (x) with TupleSort(Sort.Sort(s)) -> (z3obj_gnc s) + let sgno ( x : tuple_sort ) = match (x) with TupleSort(Sort.Sort(s))-> (z3obj_gno s) + + (** Create a new tuple sort. *) + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( field_sorts : Sort.sort array ) = + let (r, a, b) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (Array.length field_names) (Symbol.aton field_names) (Sort.aton field_sorts)) in + (* CMW: leaks a,b? *) + create_sort ctx r (** 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) + let get_mk_decl ( x : tuple_sort ) = + FuncDecl.create (sgc x) (Z3native.get_tuple_sort_mk_decl (sgnc x) (sgno x)) (** The number of fields in the tuple. *) - let get_num_fields (x : tuple_sort) = Z3native.get_tuple_sort_num_fields x#gnc x#gno + let get_num_fields ( x : tuple_sort ) = Z3native.get_tuple_sort_num_fields (sgnc x) (sgno x) (** The field declarations. *) - let get_field_decls (x : tuple_sort) = + 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 + let f i = FuncDecl.create (sgc x) (Z3native.get_tuple_sort_field_decl (sgnc x) (sgno x) i) in Array.init n f end (** Functions to manipulate arithmetic expressions *) -module Arithmetic = -struct +and Arithmetic : +sig + type arith_sort = ArithSort of Sort.sort + type int_sort = IntSort of Sort.sort + type real_sort = RealSort of Sort.sort + + type arith_expr = Expr of Expr.expr + type int_expr = IntExpr of arith_expr + type real_expr = RealExpr of arith_expr + + type int_num = IntNum of int_expr + type rat_num = RatNum of real_expr + type algebraic_num = AlgebraicNum of arith_expr + + + val create_arith_expr : context -> Z3native.ptr -> arith_expr + val create_int_expr : context -> Z3native.ptr -> int_expr + val create_real_expr : context -> Z3native.ptr -> real_expr + val create_int_num : context -> Z3native.ptr -> int_num + val create_rat_num : context -> Z3native.ptr -> rat_num + val create_algebraic_num : context -> Z3native.ptr -> algebraic_num +end = struct + type arith_sort = ArithSort of Sort.sort + type int_sort = IntSort of Sort.sort + type real_sort = RealSort of Sort.sort + + type arith_expr = ArithExpr of Expr.expr + type int_expr = IntExpr of arith_expr + type real_expr = RealExpr of arith_expr + + type int_num = IntNum of int_expr + type rat_num = RatNum of real_expr + type algebraic_num = AlgebraicNum of arith_expr + + let create_arith_expr ( ctx : context ) ( no : Z3native.ptr ) = + ArithExpr(Expr.create ctx no) + + let create_int_expr ( ctx : context ) ( no : Z3native.ptr ) = + IntExpr(create_arith_expr ctx no) + + let create_real_expr ( ctx : context ) ( no : Z3native.ptr ) = + RealExpr(create_arith_expr ctx no) + + let create_int_num ( ctx : context ) ( no : Z3native.ptr ) = + IntNum(create_int_expr ctx no) + + let create_rat_num ( ctx : context ) ( no : Z3native.ptr ) = + RatNum(create_real_expr ctx no) + (** Create a new integer sort. *) let mk_int_sort ( ctx : context ) = - (new int_sort ctx)#cnstr_obj (Z3native.mk_int_sort (context_gno ctx)) + (new int_sort ctx)#create_obj (Z3native.mk_int_sort (context_gno ctx)) (** Create a real sort. *) let mk_real_sort ( ctx : context ) = - (new real_sort ctx)#cnstr_obj (Z3native.mk_real_sort (context_gno ctx)) + (new real_sort ctx)#create_obj (Z3native.mk_real_sort (context_gno ctx)) (** Indicates whether the term is of integer sort. @@ -2802,11 +2820,11 @@ 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) + (new int_num x#gc)#create_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) + (new int_num x#gc)#create_obj (Z3native.get_denominator x#gnc x#gno) (** Returns a string representation in decimal notation. The result has at most decimal places.*) @@ -2844,75 +2862,92 @@ struct Create an expression representing t[0] + t[1] + .... *) let mk_add ( ctx : context ) ( t : arith_expr array ) = - (create_expr ctx (Z3native.mk_add (context_gno ctx) (Array.length t) (astaton t)) :> arith_expr) + (create_expr ctx (Z3native.mk_add (context_gno ctx) (Array.length t) (AST.aton 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 (context_gno ctx) (Array.length t) (astaton t)) :> arith_expr) + (create_expr ctx (Z3native.mk_mul (context_gno ctx) (Array.length t) (AST.aton 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 (context_gno ctx) (Array.length t) (astaton t)) :> arith_expr) + (create_expr ctx (Z3native.mk_sub (context_gno ctx) (Array.length t) (AST.aton t)) :> arith_expr) (** Create an expression representing -t. *) let mk_unary_minus ( ctx : context ) ( t : arith_expr ) = - (create_expr ctx (Z3native.mk_unary_minus (context_gno ctx) t#gno) :> arith_expr) + ArithExpr(create ctx (Z3native.mk_unary_minus (context_gno ctx) + (gno (match t with ArithExpr(b) -> b)))) (** Create an expression representing t1 / t2. *) let mk_div ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = - (create_expr ctx (Z3native.mk_div (context_gno ctx) t1#gno t2#gno) :> arith_expr) + ArithExpr(create ctx (Z3native.mk_div (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** 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 (context_gno ctx) t1#gno t2#gno) + IntExpr(create ctx (Z3native.mk_mod (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** 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 (context_gno ctx) t1#gno t2#gno) + IntExpr(create ctx (Z3native.mk_rem (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Create an expression representing t1 ^ t2. *) - let mk_Power ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = - (create_expr ctx (Z3native.mk_power (context_gno ctx) t1#gno t2#gno) :> arith_expr) + let mk_power ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = + ArithExpr(create_expr ctx (Z3native.mk_power (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_lt (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_le (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_gt (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_ge (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Coerce an integer to a real. @@ -2925,7 +2960,8 @@ struct The argument must be of integer sort. *) let mk_int2real ( ctx : context ) ( t : int_expr ) = - (new real_expr ctx)#cnstr_obj (Z3native.mk_int2real (context_gno ctx) t#gno) + RealExpr(create (Z3native.mk_int2real (context_gno ctx) + (gno (match t with BoolExpr(b) -> b)))) (** Coerce a real to an integer. @@ -2935,14 +2971,14 @@ struct The argument must be of real sort. *) let mk_real2int ( ctx : context ) ( t : real_expr ) = - (new int_expr ctx)#cnstr_obj (Z3native.mk_real2int (context_gno ctx) t#gno) + (new int_expr ctx)#create_obj (Z3native.mk_real2int (context_gno ctx) 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 (context_gno ctx) t#gno) - + BoolExpr(create ctx (Z3native.mk_is_int (context_gno ctx) + (gno (match t with BoolExpr(b) -> b)))) (** Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^. @@ -2951,7 +2987,7 @@ struct @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) + (new rat_num x#gc)#create_obj (Z3native.get_algebraic_number_upper x#gnc x#gno precision) (** Return a lower bound for the given real algebraic number. @@ -2961,7 +2997,7 @@ struct @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) + (new rat_num x#gc)#create_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.*) @@ -2981,7 +3017,7 @@ struct raise (Z3native.Exception "Denominator is zero") else - (new rat_num ctx)#cnstr_obj (Z3native.mk_real (context_gno ctx) num den) + (new rat_num ctx)#create_obj (Z3native.mk_real (context_gno ctx) num den) (** Create a real numeral. @@ -2989,7 +3025,7 @@ struct @return A Term with value and sort Real *) let mk_real_numeral_s ( ctx : context ) ( v : string ) = - (new rat_num ctx)#cnstr_obj (Z3native.mk_numeral (context_gno ctx) v (mk_real_sort ctx)#gno) + (new rat_num ctx)#create_obj (Z3native.mk_numeral (context_gno ctx) v (mk_real_sort ctx)#gno) (** Create a real numeral. @@ -2998,14 +3034,14 @@ struct @return A Term with value and sort Real *) let mk_real_numeral_i ( ctx : context ) ( v : int ) = - (new rat_num ctx)#cnstr_obj (Z3native.mk_int (context_gno ctx) v (mk_real_sort ctx)#gno) + (new rat_num ctx)#create_obj (Z3native.mk_int (context_gno ctx) v (mk_real_sort ctx)#gno) (** Create an integer numeral. @param v A string representing the Term value in decimal notation. *) let mk_int_numeral_s ( ctx : context ) ( v : string ) = - (new int_num ctx)#cnstr_obj (Z3native.mk_numeral (context_gno ctx) v (mk_int_sort ctx)#gno) + (new int_num ctx)#create_obj (Z3native.mk_numeral (context_gno ctx) v (mk_int_sort ctx)#gno) (** Create an integer numeral. @@ -3013,7 +3049,7 @@ struct @return A Term with value and sort Integer *) let mk_int_numeral_i ( ctx : context ) ( v : int ) = - (new int_num ctx)#cnstr_obj (Z3native.mk_int (context_gno ctx) v (mk_int_sort ctx)#gno) + (new int_num ctx)#create_obj (Z3native.mk_int (context_gno ctx) v (mk_int_sort ctx)#gno) (** Returns a string representation of the numeral. *) let to_string ( x : algebraic_num ) = Z3native.get_numeral_string x#gnc x#gno @@ -3021,13 +3057,30 @@ end (** Functions to manipulate bit-vector expressions *) -module BitVectors = -struct +and BitVectors : +sig + type bitvec_expr = BitVecExpr of Expr.expr + type bitvec_num = BitVecNum of bitvec_expr + + val create_expr : context -> Z3native.ptr -> bitvec_expr + val create_num : context -> Z3native.ptr -> bitvec_num +end = struct + type bitvec_expr = Expr of Expr.expr + type bitvec_num = BitVecExpr of bitvec_expr + + let create_expr ( ctx : context ) ( no : Z3native.ptr ) = + let e = (Expr.create ctx no) in + BitVecExpr(e) + + let create_num ( ctx : context ) ( no : Z3native.ptr ) = + let e = (create_expr ctx no) in + BitVecNum(e) + (** Create a new bit-vector sort. *) let mk_sort ( ctx : context ) size = - (new bitvec_sort ctx)#cnstr_obj (Z3native.mk_bv_sort (context_gno ctx) size) + (new bitvec_sort ctx)#create_obj (Z3native.mk_bv_sort (context_gno ctx) size) (** Indicates whether the terms is of bit-vector sort. @@ -3328,91 +3381,91 @@ struct The argument must have a bit-vector sort. *) let mk_not ( ctx : context ) ( t : bitvec_expr ) = - (new bitvec_expr ctx)#cnstr_obj (Z3native.mk_bvnot (context_gno ctx) t#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvnot (context_gno ctx) 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 (context_gno ctx) t#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvredand (context_gno ctx) 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 (context_gno ctx) t#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvredor (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvand (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvor (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvxor (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvnand (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvnor (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvxnor (context_gno ctx) 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 (context_gno ctx) t#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvneg (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvadd (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvsub (context_gno ctx) 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvmul (context_gno ctx) t1#gno t2#gno) (** Unsigned division. @@ -3424,7 +3477,7 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvudiv (context_gno ctx) t1#gno t2#gno) (** Signed division. @@ -3439,7 +3492,7 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvsdiv (context_gno ctx) t1#gno t2#gno) (** Unsigned remainder. @@ -3449,7 +3502,7 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvurem (context_gno ctx) t1#gno t2#gno) (** Signed remainder. @@ -3461,7 +3514,7 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvsrem (context_gno ctx) t1#gno t2#gno) (** Two's complement signed remainder (sign follows divisor). @@ -3470,7 +3523,7 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_bvsmod (context_gno ctx) t1#gno t2#gno) (** Unsigned less-than @@ -3478,7 +3531,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvult (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Two's complement signed less-than @@ -3486,7 +3541,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvslt (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Unsigned less-than or equal to. @@ -3494,7 +3551,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvule (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Two's complement signed less-than or equal to. @@ -3502,7 +3561,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvsle (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Unsigned greater than or equal to. @@ -3510,7 +3571,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvuge (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Two's complement signed greater than or equal to. @@ -3518,7 +3581,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvsge (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Unsigned greater-than. @@ -3526,7 +3591,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvugt (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Two's complement signed greater-than. @@ -3534,7 +3601,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvsgt (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Bit-vector concatenation. @@ -3545,7 +3614,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BitVectors.BitVecExpr(create ctx (Z3native.mk_concat (context_gno ctx) + (gno (match t1 with BitVecExpr(b) -> b)) + (gno (match t2 with BitVecExpr(b) -> b)))) (** Bit-vector extraction. @@ -3556,7 +3627,7 @@ struct 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 (context_gno ctx) high low t#gno) + (new bitvec_expr ctx)#create_obj (Z3native.mk_extract (context_gno ctx) high low t#gno) (** Bit-vector sign extension. @@ -3566,7 +3637,7 @@ struct 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 (context_gno ctx) i t#gno) + BitVecExpr(create ctx (Z3native.mk_sign_ext (context_gno ctx) i (gno (match t with BitVecExpr(b) -> b)))) (** Bit-vector zero extension. @@ -3577,7 +3648,7 @@ struct 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 (context_gno ctx) i t#gno) + BitVecExpr(create ctx (Z3native.mk_zero_ext (context_gno ctx) i (gno (match t with BitVecExpr(b) -> b)))) (** Bit-vector repetition. @@ -3585,7 +3656,7 @@ struct 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 (context_gno ctx) i t#gno) + BitVecExpr(create ctx (Z3native.mk_repeat (context_gno ctx) i (gno (match t with BitVecExpr(b) -> b)))) (** Shift left. @@ -3600,7 +3671,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BitVecExpr(create ctx (Z3native.mk_bvshl (context_gno ctx) + (gno (match t1 with BitVecExpr(b) -> b)) + (gno (match t2 with BitVecExpr(b) -> b)))) (** Logical shift right @@ -3614,7 +3687,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BitVecExpr(create ctx (Z3native.mk_bvlshr (context_gno ctx) + (gno (match t1 with BitVecExpr(b) -> b)) + (gno (match t2 with BitVecExpr(b) -> b)))) (** Arithmetic shift right @@ -3630,7 +3705,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BitVecExpr(create ctx (Z3native.mk_bvashr (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Rotate Left. @@ -3639,7 +3716,7 @@ struct 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 (context_gno ctx) i t#gno) + BitVecExpr(create ctx (Z3native.mk_rotate_left (context_gno ctx) i (gno (match t with BoolExpr(b) -> b)))) (** Rotate Right. @@ -3648,7 +3725,7 @@ struct 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 (context_gno ctx) i t#gno) + BitVecExpr(create ctx (Z3native.mk_rotate_right (context_gno ctx) i (gno (match t with BoolExpr(b) -> b)))) (** Rotate Left. @@ -3657,7 +3734,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BitVecExpr(create ctx (Z3native.mk_ext_rotate_left (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Rotate Right. @@ -3667,7 +3746,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BitVecExpr(create ctx (Z3native.mk_ext_rotate_right (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Create an bit bit-vector from the integer argument . @@ -3680,7 +3761,7 @@ struct 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 (context_gno ctx) n t#gno) + BitVecExpr(create ctx (Z3native.mk_int2bv (context_gno ctx) n (gno (match t with IntExpr(b) -> b)))) (** Create an integer from the bit-vector argument . @@ -3698,7 +3779,7 @@ struct 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 (context_gno ctx) t#gno signed) + (new int_expr ctx)#create_obj (Z3native.mk_bv2int (context_gno ctx) t#gno signed) (** Create a predicate that checks that the bit-wise addition does not overflow. @@ -3706,7 +3787,10 @@ struct 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 (context_gno ctx) t1#gno t2#gno signed) + BoolExpr(create ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)) + signed)) (** Create a predicate that checks that the bit-wise addition does not underflow. @@ -3714,23 +3798,30 @@ struct 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 (context_gno ctx) t1#gno t2#gno) - + BoolExpr(create ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) + (** 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 (context_gno ctx) t1#gno t2#gno) - + BoolExpr(create ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) + (** 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 (context_gno ctx) t1#gno t2#gno signed) + BoolExpr(create ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)) + signed)) (** Create a predicate that checks that the bit-wise signed division does not overflow. @@ -3738,7 +3829,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Create a predicate that checks that the bit-wise negation does not overflow. @@ -3746,7 +3839,7 @@ struct 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 (context_gno ctx) t#gno) + BoolExpr(create ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (gno (match t with BitVecExpr(b) -> b)))) (** Create a predicate that checks that the bit-wise multiplication does not overflow. @@ -3754,7 +3847,10 @@ struct 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 (context_gno ctx) t1#gno t2#gno signed) + BoolExpr(create ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)) + signed)) (** Create a predicate that checks that the bit-wise multiplication does not underflow. @@ -3762,7 +3858,9 @@ struct 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 (context_gno ctx) t1#gno t2#gno) + BoolExpr(create ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) + (gno (match t1 with BoolExpr(b) -> b)) + (gno (match t2 with BoolExpr(b) -> b)))) (** Create a bit-vector numeral. @@ -3771,12 +3869,13 @@ struct @param size the size of the bit-vector *) let mk_numeral ( ctx : context ) ( ctx : context ) ( v : string ) ( size : int) = - (new bitvec_num ctx)#cnstr_obj (Z3native.mk_numeral (context_gno ctx) v (mk_sort ctx size)#gno) + (new bitvec_num ctx)#create_obj (Z3native.mk_numeral (context_gno ctx) v (mk_sort ctx size)#gno) end (** Functions to manipulate proof expressions *) -module Proofs = -struct +and Proofs : +sig +end = struct (** Indicates whether the term is a Proof for the expression 'true'. *) @@ -4259,13 +4358,13 @@ struct type goal = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : goal = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.goal_inc_ref ; dec_ref = Z3native.goal_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -4318,7 +4417,7 @@ struct (** The formulas in the goal. *) let get_formulas ( x : goal ) = let n = get_size x in - let f i = (new bool_expr (z3obj_gc x))#cnstr_obj (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i) in + let f i = (new bool_expr (z3obj_gc x))#create_obj (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f (** The number of formulas, subformulas and terms in the goal. *) @@ -4334,7 +4433,7 @@ struct (** Translates (copies) the Goal to the target Context . *) let translate ( x : goal ) ( to_ctx : context ) = - cnstr to_ctx (Z3native.goal_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) + create to_ctx (Z3native.goal_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) (** Simplifies the goal. Essentially invokes the `simplify' tactic on the goal. *) let simplify ( x : goal ) ( p : Params.params option ) = @@ -4352,7 +4451,7 @@ struct Z3native.apply_result_get_subgoal (z3obj_gnc x) arn 0 in Z3native.apply_result_dec_ref (z3obj_gnc x) arn ; Z3native.tactic_dec_ref (z3obj_gnc x) tn ; - cnstr (z3obj_gc x) res + create (z3obj_gc x) res (** @@ -4365,7 +4464,7 @@ struct @param proofs Indicates whether proof generation should be enabled. *) let mk_goal ( ctx : context ) ( models : bool ) ( unsat_cores : bool ) ( proofs : bool ) = - cnstr ctx (Z3native.mk_goal (context_gno ctx) models unsat_cores proofs) + create ctx (Z3native.mk_goal (context_gno ctx) models unsat_cores proofs) (** A string representation of the Goal. *) let to_string ( x : goal ) = Z3native.goal_to_string (z3obj_gnc x) (z3obj_gno x) @@ -4380,13 +4479,13 @@ struct type model = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : model = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.model_inc_ref ; dec_ref = Z3native.model_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -4400,13 +4499,13 @@ struct type func_interp = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : func_interp = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.func_interp_inc_ref ; dec_ref = Z3native.func_interp_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -4419,13 +4518,13 @@ struct type func_entry = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : func_entry = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.func_entry_inc_ref ; dec_ref = Z3native.func_entry_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -4467,7 +4566,7 @@ struct *) let get_entries ( x : func_interp ) = let n = (get_num_entries x) in - let f i = (FuncEntry.cnstr (z3obj_gc x) (Z3native.func_interp_get_entry (z3obj_gnc x) (z3obj_gno x) i)) in + let f i = (FuncEntry.create (z3obj_gc x) (Z3native.func_interp_get_entry (z3obj_gnc x) (z3obj_gno x) i)) in Array.init n f (** @@ -4534,11 +4633,11 @@ struct raise (Z3native.Exception "Argument was not an array constant") else let fd = Z3native.get_as_array_func_decl (z3obj_gnc x) n in - get_func_interp x ((new func_decl f#gc)#cnstr_obj fd) + get_func_interp x ((new func_decl f#gc)#create_obj fd) | _ -> raise (Z3native.Exception "Constant functions do not have a function interpretation; use ConstInterp"); else let n = (Z3native.model_get_func_interp (z3obj_gnc x) (z3obj_gno x) f#gno) in - if (Z3native.is_null n) then None else Some (FuncInterp.cnstr (z3obj_gc x) n) + if (Z3native.is_null n) then None else Some (FuncInterp.create (z3obj_gc x) n) (** The number of constants that have an interpretation in the model. *) let get_num_consts ( x : model ) = Z3native.model_get_num_consts (z3obj_gnc x) (z3obj_gno x) @@ -4546,7 +4645,7 @@ struct (** The function declarations of the constants in the model. *) let get_const_decls ( x : model ) = let n = (get_num_consts x) in - let f i = (new func_decl (z3obj_gc x))#cnstr_obj (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in + let f i = (new func_decl (z3obj_gc x))#create_obj (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f @@ -4556,15 +4655,15 @@ struct (** The function declarations of the function interpretations in the model. *) let get_func_decls ( x : model ) = let n = (get_num_consts x) in - let f i = (new func_decl (z3obj_gc x))#cnstr_obj (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in + let f i = (new func_decl (z3obj_gc x))#create_obj (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f (** All symbols that have an interpretation in the model. *) let get_decls ( x : model ) = let n_funcs = (get_num_funcs x) in let n_consts = (get_num_consts x ) in - let f i = (new func_decl (z3obj_gc x))#cnstr_obj (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in - let g i = (new func_decl (z3obj_gc x))#cnstr_obj (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in + let f i = (new func_decl (z3obj_gc x))#create_obj (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in + let g i = (new func_decl (z3obj_gc x))#create_obj (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in Array.append (Array.init n_funcs f) (Array.init n_consts g) (** A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. *) @@ -4619,7 +4718,7 @@ struct An array of expressions, where each is an element of the universe of *) let sort_universe ( x : model ) ( s : sort ) = - let n_univ = AST.ASTVector.cnstr (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) s#gno) in + let n_univ = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) s#gno) in let n = (AST.ASTVector.get_size n_univ) in let f i = (AST.ASTVector.get n_univ i) in Array.init n f @@ -4644,13 +4743,13 @@ struct type probe = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : probe = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.probe_inc_ref ; dec_ref = Z3native.probe_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -4686,48 +4785,48 @@ struct Creates a new Probe. *) let mk_probe ( ctx : context ) ( name : string ) = - (cnstr ctx (Z3native.mk_probe (context_gno ctx) name)) + (create ctx (Z3native.mk_probe (context_gno ctx) name)) (** Create a probe that always evaluates to . *) let const ( ctx : context ) ( v : float ) = - (cnstr ctx (Z3native.probe_const (context_gno ctx) v)) + (create ctx (Z3native.probe_const (context_gno ctx) v)) (** Create a probe that evaluates to "true" when the value returned by is less than the value returned by *) let lt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = - (cnstr ctx (Z3native.probe_lt (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) + (create ctx (Z3native.probe_lt (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) (** Create a probe that evaluates to "true" when the value returned by is greater than the value returned by *) let gt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = - (cnstr ctx (Z3native.probe_gt (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) + (create ctx (Z3native.probe_gt (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) (** Create a probe that evaluates to "true" when the value returned by is less than or equal the value returned by *) let le ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = - (cnstr ctx (Z3native.probe_le (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) + (create ctx (Z3native.probe_le (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) (** Create a probe that evaluates to "true" when the value returned by is greater than or equal the value returned by *) let ge ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = - (cnstr ctx (Z3native.probe_ge (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) + (create ctx (Z3native.probe_ge (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) (** Create a probe that evaluates to "true" when the value returned by is equal to the value returned by *) let eq ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = - (cnstr ctx (Z3native.probe_eq (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) + (create ctx (Z3native.probe_eq (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) (** Create a probe that evaluates to "true" when the value @@ -4735,7 +4834,7 @@ struct *) (* CMW: and is a keyword *) let and_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = - (cnstr ctx (Z3native.probe_and (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) + (create ctx (Z3native.probe_and (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) (** Create a probe that evaluates to "true" when the value @@ -4743,7 +4842,7 @@ struct *) (* CMW: or is a keyword *) let or_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = - (cnstr ctx (Z3native.probe_or (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) + (create ctx (Z3native.probe_or (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) (** Create a probe that evaluates to "true" when the value @@ -4751,7 +4850,7 @@ struct *) (* CMW: is not a keyword? *) let not_ ( ctx : context ) ( p : probe ) = - (cnstr ctx (Z3native.probe_not (context_gno ctx) (z3obj_gno p))) + (create ctx (Z3native.probe_not (context_gno ctx) (z3obj_gno p))) end @@ -4767,13 +4866,13 @@ struct type tactic = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : tactic = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.tactic_inc_ref ; dec_ref = Z3native.tactic_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -4786,13 +4885,13 @@ struct type apply_result = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : apply_result = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.apply_result_inc_ref ; dec_ref = Z3native.apply_result_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -4803,19 +4902,19 @@ struct (** Retrieves the subgoals from the apply_result. *) let get_subgoals ( x : apply_result ) = let n = (get_num_subgoals x) in - let f i = Goal.cnstr (z3obj_gc x) (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) in + let f i = Goal.create (z3obj_gc x) (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f (** Retrieves the subgoals from the apply_result. *) let get_subgoal ( x : apply_result ) ( i : int ) = - Goal.cnstr (z3obj_gc x) (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) + Goal.create (z3obj_gc x) (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) (** Convert a model for the subgoal into a model for the original goal g, that the ApplyResult was obtained from. #return A model for g *) let convert_model ( x : apply_result ) ( i : int ) ( m : Model.model ) = - Model.cnstr (z3obj_gc x) (Z3native.apply_result_convert_model (z3obj_gnc x) (z3obj_gno x) i (z3obj_gno m)) + Model.create (z3obj_gc x) (Z3native.apply_result_convert_model (z3obj_gnc x) (z3obj_gno x) i (z3obj_gno m)) (** A string representation of the ApplyResult. *) let to_string ( x : apply_result ) = Z3native.apply_result_to_string (z3obj_gnc x) (z3obj_gno x) @@ -4826,13 +4925,13 @@ struct (** Retrieves parameter descriptions for Tactics. *) let get_param_descrs ( x : tactic ) = - Params.ParamDescrs.cnstr (z3obj_gc x) (Z3native.tactic_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) + Params.ParamDescrs.create (z3obj_gc x) (Z3native.tactic_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) (** Apply the tactic to the goal. *) let apply ( x : tactic ) ( g : Goal.goal ) ( p : Params.params option ) = match p with - | None -> (ApplyResult.cnstr (z3obj_gc x) (Z3native.tactic_apply (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g))) - | Some (pn) -> (ApplyResult.cnstr (z3obj_gc x) (Z3native.tactic_apply_ex (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g) (z3obj_gno pn))) + | None -> (ApplyResult.create (z3obj_gc x) (Z3native.tactic_apply (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g))) + | Some (pn) -> (ApplyResult.create (z3obj_gc x) (Z3native.tactic_apply_ex (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g) (z3obj_gno pn))) (** The number of supported tactics. @@ -4858,7 +4957,7 @@ struct Creates a new Tactic. *) let mk_tactic ( ctx : context ) ( name : string ) = - cnstr ctx (Z3native.mk_tactic (context_gno ctx) name) + create ctx (Z3native.mk_tactic (context_gno ctx) name) (** Create a tactic that applies to a Goal and @@ -4870,17 +4969,17 @@ struct | Some(x) -> (Some (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno c) x))) in match (Array.fold_left f None ts) with | None -> - cnstr ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) + create ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) | Some(x) -> let o = (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t2) x) in - cnstr ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) o) + create ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) o) (** Create a tactic that first applies to a Goal and if it fails then returns the result of applied to the Goal. *) let or_else ( ctx : context ) ( t1 : tactic ) ( t2 : tactic ) = - cnstr ctx (Z3native.tactic_or_else (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) + create ctx (Z3native.tactic_or_else (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) (** Create a tactic that applies to a goal for milliseconds. @@ -4888,7 +4987,7 @@ struct If does not terminate within milliseconds, then it fails. *) let try_for ( ctx : context ) ( t : tactic ) ( ms : int ) = - cnstr ctx (Z3native.tactic_try_for (context_gno ctx) (z3obj_gno t) ms) + create ctx (Z3native.tactic_try_for (context_gno ctx) (z3obj_gno t) ms) (** Create a tactic that applies to a given goal if the probe @@ -4898,52 +4997,52 @@ struct *) (* CMW: when is a keyword *) let when_ ( ctx : context ) ( p : Probe.probe ) ( t : tactic ) = - cnstr ctx (Z3native.tactic_when (context_gno ctx) (z3obj_gno p) (z3obj_gno t)) + create ctx (Z3native.tactic_when (context_gno ctx) (z3obj_gno p) (z3obj_gno t)) (** Create a tactic that applies to a given goal if the probe evaluates to true and otherwise. *) let cond ( ctx : context ) ( p : Probe.probe ) ( t1 : tactic ) ( t2 : tactic ) = - cnstr ctx (Z3native.tactic_cond (context_gno ctx) (z3obj_gno p) (z3obj_gno t1) (z3obj_gno t2)) + create ctx (Z3native.tactic_cond (context_gno ctx) (z3obj_gno p) (z3obj_gno t1) (z3obj_gno t2)) (** Create a tactic that keeps applying until the goal is not modified anymore or the maximum number of iterations is reached. *) let repeat ( ctx : context ) ( t : tactic ) ( max : int ) = - cnstr ctx (Z3native.tactic_repeat (context_gno ctx) (z3obj_gno t) max) + create ctx (Z3native.tactic_repeat (context_gno ctx) (z3obj_gno t) max) (** Create a tactic that just returns the given goal. *) let skip ( ctx : context ) = - cnstr ctx (Z3native.tactic_skip (context_gno ctx)) + create ctx (Z3native.tactic_skip (context_gno ctx)) (** Create a tactic always fails. *) let fail ( ctx : context ) = - cnstr ctx (Z3native.tactic_fail (context_gno ctx)) + create ctx (Z3native.tactic_fail (context_gno ctx)) (** Create a tactic that fails if the probe evaluates to false. *) let fail_if ( ctx : context ) ( p : Probe.probe ) = - cnstr ctx (Z3native.tactic_fail_if (context_gno ctx) (z3obj_gno p)) + create ctx (Z3native.tactic_fail_if (context_gno ctx) (z3obj_gno p)) (** Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false'). *) let fail_if_not_decided ( ctx : context ) = - cnstr ctx (Z3native.tactic_fail_if_not_decided (context_gno ctx)) + create ctx (Z3native.tactic_fail_if_not_decided (context_gno ctx)) (** Create a tactic that applies using the given set of parameters . *) let using_params ( ctx : context ) ( t : tactic ) ( p : Params.params ) = - cnstr ctx (Z3native.tactic_using_params (context_gno ctx) (z3obj_gno t) (z3obj_gno p)) + create ctx (Z3native.tactic_using_params (context_gno ctx) (z3obj_gno t) (z3obj_gno p)) (** Create a tactic that applies using the given set of parameters . @@ -4956,14 +5055,14 @@ struct Create a tactic that applies the given tactics in parallel. *) let par_or ( ctx : context ) ( t : tactic array ) = - cnstr ctx (Z3native.tactic_par_or (context_gno ctx) (Array.length t) (array_to_native t)) + create ctx (Z3native.tactic_par_or (context_gno ctx) (Array.length t) (array_to_native t)) (** Create a tactic that applies to a given goal and then to every subgoal produced by . The subgoals are processed in parallel. *) let par_and_then ( ctx : context ) ( t1 : tactic ) ( t2 : tactic ) = - cnstr ctx (Z3native.tactic_par_and_then (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) + create ctx (Z3native.tactic_par_and_then (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) (** Interrupt the execution of a Z3 procedure. @@ -4980,13 +5079,13 @@ struct type solver = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : solver = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.solver_inc_ref ; dec_ref = Z3native.solver_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -5003,13 +5102,13 @@ struct type statistics = z3_native_object (**/**) - let cnstr ( ctx : context ) ( no : Z3native.ptr ) = + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : statistics = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.stats_inc_ref ; dec_ref = Z3native.stats_dec_ref } in (z3obj_sno res ctx no) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -5028,7 +5127,7 @@ struct mutable m_float : float } (**/**) - let cnstr_si k v = + let create_si k v = let res : statistics_entry = { m_key = k ; m_is_int = true ; @@ -5038,7 +5137,7 @@ struct } in res - let cnstr_sd k v = + let create_sd k v = let res : statistics_entry = { m_key = k ; m_is_int = false ; @@ -5089,9 +5188,9 @@ struct let f i = ( let k = Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i in if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then - (Entry.cnstr_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) + (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) else - (Entry.cnstr_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) + (Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) ) in Array.init n f @@ -5126,7 +5225,7 @@ struct Retrieves parameter descriptions for solver. *) let get_param_descrs ( x : solver ) = - Params.ParamDescrs.cnstr (z3obj_gc x) (Z3native.solver_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) + Params.ParamDescrs.create (z3obj_gc x) (Z3native.solver_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) (** The current number of backtracking points (scopes). @@ -5200,7 +5299,7 @@ struct The number of assertions in the solver. *) let get_num_assertions ( x : solver ) = - let a = AST.ASTVector.cnstr (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in + let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in (AST.ASTVector.get_size a) @@ -5208,9 +5307,9 @@ struct The set of asserted formulas. *) let get_assertions ( x : solver ) = - let a = AST.ASTVector.cnstr (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in + let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in let n = (AST.ASTVector.get_size a) in - let f i = ((new bool_expr (z3obj_gc x))#cnstr_obj (AST.ASTVector.get a i)#gno) in + let f i = ((new bool_expr (z3obj_gc x))#create_obj (AST.ASTVector.get a i)#gno) in Array.init n f (** @@ -5225,7 +5324,7 @@ struct if ((Array.length assumptions) == 0) then lbool_of_int (Z3native.solver_check (z3obj_gnc x) (z3obj_gno x)) else - lbool_of_int (Z3native.solver_check_assumptions (z3obj_gnc x) (z3obj_gno x) (Array.length assumptions) (astaton assumptions)) + lbool_of_int (Z3native.solver_check_assumptions (z3obj_gnc x) (z3obj_gno x) (Array.length assumptions) (AST.aton assumptions)) in match r with | L_TRUE -> SATISFIABLE @@ -5243,7 +5342,7 @@ struct if (Z3native.is_null q) then None else - Some (Model.cnstr (z3obj_gc x) q) + Some (Model.create (z3obj_gc x) q) (** The proof of the last Check. @@ -5266,7 +5365,7 @@ struct if its results was not UNSATISFIABLE, or if core production is disabled. *) let get_unsat_core ( x : solver ) = - let cn = AST.ASTVector.cnstr (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in + let cn = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in let n = (AST.ASTVector.get_size cn) in let f i = (AST.ASTVector.get cn i) in Array.init n f @@ -5281,7 +5380,7 @@ struct Solver statistics. *) let get_statistics ( x : solver ) = - (Statistics.cnstr (z3obj_gc x) (Z3native.solver_get_statistics (z3obj_gnc x) (z3obj_gno x))) + (Statistics.create (z3obj_gc x) (Z3native.solver_get_statistics (z3obj_gnc x) (z3obj_gno x))) (** Creates a new (incremental) solver. @@ -5292,8 +5391,8 @@ struct *) let mk_solver ( ctx : context ) ( logic : Symbol.symbol option ) = match logic with - | None -> (cnstr ctx (Z3native.mk_solver (context_gno ctx))) - | Some (x) -> (cnstr ctx (Z3native.mk_solver_for_logic (context_gno ctx) (Symbol.gno x))) + | None -> (create ctx (Z3native.mk_solver (context_gno ctx))) + | Some (x) -> (create ctx (Z3native.mk_solver_for_logic (context_gno ctx) (Symbol.gno x))) (** Creates a new (incremental) solver. @@ -5306,7 +5405,7 @@ struct Creates a new (incremental) solver. *) let mk_simple_solver ( ctx : context ) = - (cnstr ctx (Z3native.mk_simple_solver (context_gno ctx))) + (create ctx (Z3native.mk_simple_solver (context_gno ctx))) (** Creates a solver that is implemented using the given tactic. @@ -5315,7 +5414,7 @@ struct will always solve each check from scratch. *) let mk_solver_t ( ctx : context ) ( t : Tactic.tactic ) = - (cnstr ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t))) + (create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t))) (** A string representation of the solver. @@ -5330,13 +5429,13 @@ struct type fixedpoint = z3_native_object (**/**) - let cnstr ( ctx : context ) = + let create ( ctx : context ) = let res : fixedpoint = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.fixedpoint_inc_ref ; dec_ref = Z3native.fixedpoint_dec_ref } in (z3obj_sno res ctx (Z3native.mk_fixedpoint (context_gno ctx))) ; - (z3obj_cnstr res) ; + (z3obj_create res) ; res (**/**) @@ -5356,7 +5455,7 @@ struct Retrieves parameter descriptions for Fixedpoint solver. *) let get_param_descrs ( x : fixedpoint ) = - Params.ParamDescrs.cnstr (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) + Params.ParamDescrs.create (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) (** Assert a constraints into the fixedpoint solver. @@ -5487,30 +5586,30 @@ struct Convert benchmark given as set of axioms, rules and queries to a string. *) let to_string_q ( x : fixedpoint ) ( queries : bool_expr array ) = - Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (Array.length queries) (astaton queries) + Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (Array.length queries) (AST.aton queries) (** Retrieve set of rules added to fixedpoint context. *) let get_rules ( x : fixedpoint ) = - let v = (AST.ASTVector.cnstr (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in + let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in let n = (AST.ASTVector.get_size v) in - let f i = (new bool_expr (z3obj_gc x))#cnstr_obj (AST.ASTVector.get v i)#gno in + let f i = (new bool_expr (z3obj_gc x))#create_obj (AST.ASTVector.get v i)#gno in Array.init n f (** Retrieve set of assertions added to fixedpoint context. *) let get_assertions ( x : fixedpoint ) = - let v = (AST.ASTVector.cnstr (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in + let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in let n = (AST.ASTVector.get_size v) in - let f i = (new bool_expr (z3obj_gc x))#cnstr_obj (AST.ASTVector.get v i)#gno in + let f i = (new bool_expr (z3obj_gc x))#create_obj (AST.ASTVector.get v i)#gno in Array.init n f (** Create a Fixedpoint context. *) - let mk_fixedpoint ( ctx : context ) = cnstr ctx + let mk_fixedpoint ( ctx : context ) = create ctx end (** Global and context options @@ -5590,7 +5689,7 @@ struct *) let benchmark_to_smtstring ( ctx : context ) ( name : string ) ( logic : string ) ( status : string ) ( attributes : string ) ( assumptions : bool_expr array ) ( formula : bool_expr ) = Z3native.benchmark_to_smtlib_string (context_gno ctx) name logic status attributes - (Array.length assumptions) (astaton assumptions) + (Array.length assumptions) (AST.aton assumptions) formula#gno (** @@ -5613,7 +5712,7 @@ struct Z3native.parse_smtlib_string (context_gno ctx) str cs (Symbol.aton sort_names) - (astaton sorts) + (AST.aton sorts) cd (Symbol.aton decl_names) (func_declaton decls) @@ -5633,7 +5732,7 @@ struct Z3native.parse_smtlib_file (context_gno ctx) file_name cs (Symbol.aton sort_names) - (astaton sorts) + (AST.aton sorts) cd (Symbol.aton decl_names) (func_declaton decls) @@ -5675,7 +5774,7 @@ struct *) let get_smtlib_decls ( ctx : context ) = let n = (get_num_smtlib_decls ctx) in - let f i = (new func_decl ctx)#cnstr_obj (Z3native.get_smtlib_decl (context_gno ctx) i) in + let f i = (new func_decl ctx)#create_obj (Z3native.get_smtlib_decl (context_gno ctx) i) in Array.init n f (** @@ -5708,7 +5807,7 @@ struct Z3native.parse_smtlib2_string (context_gno ctx) str cs (Symbol.aton sort_names) - (astaton sorts) + (Sort.aton sorts) cd (Symbol.aton decl_names) (func_declaton decls) @@ -5728,7 +5827,7 @@ struct Z3native.parse_smtlib2_string (context_gno ctx) file_name cs (Symbol.aton sort_names) - (astaton sorts) + (Sort.aton sorts) cd (Symbol.aton decl_names) (func_declaton decls)