From 23febf13c40b56d7e7fe3fa4bd071c1b8c57c87d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 19 Feb 2013 19:49:27 +0000 Subject: [PATCH] ML API: basic structure and interface Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 81 +- scripts/update_api.py | 30 +- src/api/ml/Makefile | 2 +- src/api/ml/z3.ml | 2714 +++++++++++++++++++---------------------- 4 files changed, 1380 insertions(+), 1447 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index bea2939b6..a187bf9cb 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1340,10 +1340,17 @@ class MLComponent(Component): shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f)) for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)): shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f)) + cmis = '%s/z3enums.cmi %s/z3native.cmi %s/z3.cmi' % (src_dir,src_dir,src_dir) + out.write('%s/z3enums.cmi: %s/z3enums.mli\n' % (src_dir,src_dir)) + out.write('\t%s -I %s -c %s/z3enums.mli\n' % (OCAMLC,src_dir,src_dir)) + out.write('%s/z3native.cmi: %s/z3native.mli\n' % (src_dir,src_dir)) + out.write('\t%s -I %s -c %s/z3native.mli\n' % (OCAMLC,src_dir,src_dir)) + out.write('%s/z3.cmi: %s/z3.mli\n' % (src_dir,src_dir)) + out.write('\t%s -I %s -c %s/z3.mli\n' % (OCAMLC,src_dir,src_dir)) out.write('api/ml/libz3ml$(LIB_EXT): %s$(SO_EXT)\n' % get_component(Z3_DLL_COMPONENT).dll_name) out.write('\t$(CXX) $(CXXFLAGS) -I %s -I %s %s/z3native.c $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT)\n' % (OCAML_LIB, api_src, src_dir)) out.write('\t$(AR) $(AR_FLAGS) $(AR_OUTFLAG)api/ml/libz3ml$(LIB_EXT) api/ml/z3native$(OBJ_EXT)\n') - out.write('api/ml/z3.cmxa: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT)' % get_component(Z3_DLL_COMPONENT).dll_name) + out.write('api/ml/z3.cmxa: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (get_component(Z3_DLL_COMPONENT).dll_name, cmis)) for mlfile in get_ml_files(self.src_dir): out.write(' %s' % os.path.join(src_dir, mlfile)) out.write('\n') @@ -1351,7 +1358,7 @@ class MLComponent(Component): if DEBUG_MODE: out.write('-g ') out.write('-ccopt "-I../../%s" -cclib "-L../.. -lz3ml" -I %s %s/z3enums.ml %s/z3native.ml %s/z3.ml -a -o api/ml/z3.cmxa -linkall\n' % (api_src,src_dir,src_dir,src_dir,src_dir)) - out.write('api/ml/z3.cma: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT)' % get_component(Z3_DLL_COMPONENT).dll_name) + out.write('api/ml/z3.cma: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (get_component(Z3_DLL_COMPONENT).dll_name, cmis)) for mlfile in get_ml_files(self.src_dir): out.write(' %s' % os.path.join(self.to_src_dir, mlfile)) out.write('\n') @@ -2716,6 +2723,76 @@ def mk_z3consts_ml(api_files): linenum = linenum + 1 if VERBOSE: print "Generated '%s/z3enums.ml'" % ('%s' % gendir) + efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w') + efile.write('(* Automatically generated file *)\n\n') + efile.write('(** The enumeration types of Z3. *)\n\n') + for api_file in api_files: + api_file_c = ml.find_file(api_file, ml.name) + api_file = os.path.join(api_file_c.src_dir, api_file) + + api = open(api_file, 'r') + + SEARCHING = 0 + FOUND_ENUM = 1 + IN_ENUM = 2 + + mode = SEARCHING + decls = {} + idx = 0 + + linenum = 1 + for line in api: + m1 = blank_pat.match(line) + m2 = comment_pat.match(line) + if m1 or m2: + # skip blank lines and comments + linenum = linenum + 1 + elif mode == SEARCHING: + m = typedef_pat.match(line) + if m: + mode = FOUND_ENUM + m = typedef2_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + elif mode == FOUND_ENUM: + m = openbrace_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + else: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM + words = re.split('[^\-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] + if name not in DeprecatedEnums: + efile.write('(** %s *)\n' % name[3:]) + efile.write('type %s =\n' % name[3:]) # strip Z3_ + for k, i in decls.iteritems(): + efile.write(' | %s \n' % k[3:]) # strip Z3_ + efile.write('\n') + efile.write('(** Convert %s to int*)\n' % name[3:]) + efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_ + efile.write('(** Convert int to %s*)\n' % name[3:]) + efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_ + efile.write('\n') + mode = SEARCHING + else: + if words[2] != '': + if len(words[2]) > 1 and words[2][1] == 'x': + idx = int(words[2], 16) + else: + idx = int(words[2]) + decls[words[1]] = idx + idx = idx + 1 + linenum = linenum + 1 + if VERBOSE: + print "Generated '%s/z3enums.mli'" % ('%s' % gendir) def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id diff --git a/scripts/update_api.py b/scripts/update_api.py index c730a325e..6e9c14355 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1147,49 +1147,66 @@ def mk_ml(): return ml_dir = get_component('ml').src_dir ml_nativef = os.path.join(ml_dir, 'z3native.ml') + ml_nativefi = os.path.join(ml_dir, 'z3native.mli') ml_wrapperf = os.path.join(ml_dir, 'z3native.c') ml_native = open(ml_nativef, 'w') + ml_i = open(ml_nativefi, 'w') ml_native.write('(* Automatically generated file *)\n\n') ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n') + ml_i.write('(* Automatically generated file *)\n\n') + ml_i.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n') ml_native.write('open Z3enums\n\n') ml_native.write('(**/**)\n') ml_native.write('type ptr\n') + ml_i.write('type ptr\n') ml_native.write('and z3_symbol = ptr\n') + ml_i.write('and z3_symbol = ptr\n') for k, v in Type2Str.iteritems(): if is_obj(k): ml_native.write('and %s = ptr\n' % v.lower()) + ml_i.write('and %s = ptr\n' % v.lower()) ml_native.write('\n') - ml_native.write('external is_null : ptr -> bool\n') - ml_native.write(' = "n_is_null"\n\n') - ml_native.write('external mk_null : unit -> ptr\n') - ml_native.write(' = "n_mk_null"\n\n') + ml_i.write('\n') + ml_native.write('external is_null : ptr -> bool\n = "n_is_null"\n\n') + ml_native.write('external mk_null : unit -> ptr\n = "n_mk_null"\n\n') ml_native.write('exception Exception of string\n\n') + ml_i.write('val is_null : ptr -> bool\n') + ml_i.write('val mk_null : unit -> ptr\n') + ml_i.write('exception Exception of string\n\n') # ML declarations - ml_native.write(' module ML2C = struct\n\n') + ml_native.write('module ML2C = struct\n\n') for name, result, params in _dotnet_decls: ml_native.write(' external n_%s : ' % ml_method_name(name)) + ml_i.write('val %s : ' % ml_method_name(name)) ip = inparams(params) op = outparams(params) if len(ip) == 0: - ml_native.write(' unit -> ') + ml_native.write(' unit -> ') for p in ip: ml_native.write('%s -> ' % param2ml(p)) + ml_i.write('%s -> ' % param2ml(p)) if len(op) > 0: ml_native.write('(') + ml_i.write('(') first = True if result != VOID or len(op) == 0: ml_native.write('%s' % type2ml(result)) + ml_i.write('%s' % type2ml(result)) first = False for p in op: if first: first = False else: ml_native.write(' * ') + ml_i.write(' * ') ml_native.write('%s' % param2ml(p)) + ml_i.write('%s' % param2ml(p)) if len(op) > 0: ml_native.write(')') + ml_i.write(')') ml_native.write('\n') + ml_i.write('\n') ml_native.write(' = "n_%s"\n' % ml_method_name(name)) if len(ip) > 5: ml_native.write(' "n_%s_bytecode"\n' % ml_method_name(name)) @@ -1201,6 +1218,7 @@ def mk_ml(): ip = inparams(params) op = outparams(params) ml_native.write(' let %s ' % ml_method_name(name)) + first = True i = 0; for p in params: diff --git a/src/api/ml/Makefile b/src/api/ml/Makefile index ad5442327..abcefa4af 100644 --- a/src/api/ml/Makefile +++ b/src/api/ml/Makefile @@ -7,4 +7,4 @@ all: doc: *.ml mkdir -p doc - ocamldoc -html -d doc -I ../../../bld_dbg/api/ml -sort *.ml -hide Z3 + ocamldoc -html -d doc -I ../../../bld_dbg/api/ml -sort *.mli -hide Z3 diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index aeb9c0d03..ea8c9576e 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -7,8 +7,479 @@ open Z3enums -(** Interaction logging for Z3 +(* Some helpers. *) +let null = Z3native.mk_null() +let is_null o = (Z3native.is_null o) + +(* Internal types *) +type z3_native_context = { m_n_ctx : Z3native.z3_context; m_n_obj_cnt: int; } +type context = z3_native_context + + + +type z3_native_object = { + m_ctx : context ; + mutable m_n_obj : Z3native.ptr ; + inc_ref : Z3native.z3_context -> Z3native.ptr -> unit; + dec_ref : Z3native.z3_context -> Z3native.ptr -> unit } + + +(* Symbol types *) +type int_symbol = z3_native_object +type string_symbol = z3_native_object + +type symbol = + | S_Int of int_symbol + | S_Str of string_symbol + +(* AST types *) +type ast = z3_native_object +type ast_vector = z3_native_object +type ast_map = z3_native_object + +(* FuncDecl types *) +type func_decl = FuncDecl of ast + +(* Sort types *) +type sort = Sort of ast +type uninterpreted_sort = UninterpretedSort of sort +type bool_sort = BoolSort of sort +type array_sort = ArraySort of sort +type set_sort = SetSort of sort +type datatype_sort = DatatypeSort of sort +type relation_sort = RelationSort of sort +type finite_domain_sort = FiniteDomainSort of sort +type enum_sort = EnumSort of sort +type list_sort = ListSort of sort +type tuple_sort = TupleSort of sort +type arith_sort = ArithSort of sort +type bitvec_sort = BitVecSort of sort + +type int_sort = IntSort of arith_sort +type real_sort = RealSort of arith_sort + +(* FuncDecl parameters *) +type parameter = + | P_Int of int + | P_Dbl of float + | P_Sym of symbol + | P_Srt of sort + | P_Ast of ast + | P_Fdl of func_decl + | P_Rat of string +type params = z3_native_object +type param_descrs = z3_native_object + +(* Expr types *) +type expr = Expr of ast + +type bool_expr = BoolExpr of expr +type arith_expr = ArithExpr of expr +type int_expr = IntExpr of arith_expr +type real_expr = RealExpr of arith_expr +type bitvec_expr = BitVecExpr of expr +type array_expr = ArrayExpr of expr +type datatype_expr = DatatypeExpr of expr + +(* Numerals *) +type int_num = IntNum of int_expr +type rat_num = RatNum of real_expr +type algebraic_num = AlgebraicNum of arith_expr +type bitvec_num = BitVecNum of bitvec_expr + +(* Quantifier stuff *) +type quantifier = Quantifier of expr +type pattern = Pattern of ast + +(* Datatype stuff *) +type constructor_extra = { + m_n : int; + mutable m_tester_decl : func_decl option; + mutable m_constructor_decl : func_decl option ; + mutable m_accessor_decls : func_decl array option} + +type constructor = Constructor of (z3_native_object * constructor_extra) +type constructor_list = z3_native_object + +(* Tactical interface *) +type goal = z3_native_object +type model = z3_native_object +type func_interp = z3_native_object +type func_entry = z3_native_object +type probe = z3_native_object +type tactic = z3_native_object +type apply_result = z3_native_object +type solver = z3_native_object +type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE +type statistics = z3_native_object +type statistics_entry = { + mutable m_key : string; + mutable m_is_int : bool ; + mutable m_is_float : bool ; + mutable m_int : int ; + mutable m_float : float } +type fixedpoint = z3_native_object + + +(** Internal stuff *) +module Internal = +struct + let dispose_context ctx = + if ctx.m_n_obj_cnt == 0 then ( + (* Printf.printf "Disposing context \n" ; *) + (Z3native.del_context ctx.m_n_ctx) + ) else ( + Printf.printf "NOT DISPOSING context because it still has %d objects alive\n" ctx.m_n_obj_cnt; + (* re-queue for finalization? *) + ) + + let create_context settings = + let cfg = Z3native.mk_config in + let f e = (Z3native.set_param_value cfg (fst e) (snd e)) in + (List.iter f settings) ; + let v = Z3native.mk_context_rc cfg in + Z3native.del_config(cfg) ; + Z3native.set_ast_print_mode v (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ; + (* Printf.printf "Installing finalizer on context \n" ; *) + let res = { m_n_ctx = v; m_n_obj_cnt = 0 } in + let f = fun o -> dispose_context o in + Gc.finalise f res; + res + (* CMW: Install error handler here! + m_n_err_handler = new Z3native.error_handler(NativeErrorHandler); keep reference so it doesn't get collected. + Z3native.set_error_handler(m_ctx, m_n_err_handler); + GC.SuppressFinalize(this); + *) + + let context_add1 ctx = ignore (ctx.m_n_obj_cnt = ctx.m_n_obj_cnt + 1) + let context_sub1 ctx = ignore (ctx.m_n_obj_cnt = ctx.m_n_obj_cnt - 1) + let context_gno ctx = ctx.m_n_ctx + + + let z3obj_gc o = o.m_ctx + let z3obj_gnc o = (context_gno o.m_ctx) + + let z3obj_gno o = o.m_n_obj + let z3obj_sno o ctx no = + (context_add1 ctx) ; + o.inc_ref (context_gno ctx) no ; + ( + if not (is_null o.m_n_obj) then + o.dec_ref (context_gno ctx) o.m_n_obj ; + (context_sub1 ctx) + ) ; + o.m_n_obj <- no + + let z3obj_dispose o = + if not (is_null o.m_n_obj) then + ( + o.dec_ref (z3obj_gnc o) o.m_n_obj ; + (context_sub1 (z3obj_gc o)) + ) ; + o.m_n_obj <- null + + let z3obj_create o = + let f = fun o -> (z3obj_dispose o) in + Gc.finalise f o + + let z3obj_nil_ref x y = () + + let array_to_native a = + let f e = (z3obj_gno e) in + Array.map f a + + (* Internal coercions *) + let context_of_ast ( x : ast ) = (z3obj_gc x) + let nc_of_ast ( x : ast ) = (z3obj_gnc x) + let ptr_of_ast ( x : ast ) = (z3obj_gno x) + + let c_of_expr e = match e with Expr(a) -> (z3obj_gc a) + let nc_of_expr e = match e with Expr(a) -> (z3obj_gnc a) + let ptr_of_expr e = match e with Expr(a) -> (z3obj_gno a) + + + let z3_native_object_of_ast_ptr : context -> Z3native.ptr -> z3_native_object = fun ctx no -> + 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 sort_of_ptr : context -> Z3native.ptr -> sort = fun ctx no -> + let q = (z3_native_object_of_ast_ptr ctx no) in + if ((Z3enums.ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no)) != Z3enums.SORT_AST) then + raise (Z3native.Exception "Invalid coercion") + else + 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") + + let func_decl_of_ptr : context -> Z3native.ptr -> func_decl = fun ctx no -> + if ((Z3enums.ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no)) != Z3enums.FUNC_DECL_AST) then + raise (Z3native.Exception "Invalid coercion") + else + FuncDecl(z3_native_object_of_ast_ptr ctx no) + + let rec ast_of_ptr : context -> Z3native.ptr -> ast = fun ctx no -> + match (ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no)) with + | FUNC_DECL_AST + | SORT_AST + | QUANTIFIER_AST + | APP_AST + | NUMERAL_AST + | VAR_AST -> z3_native_object_of_ast_ptr ctx no + | UNKNOWN_AST -> raise (Z3native.Exception "Cannot create asts of type unknown") + + and expr_of_ptr : context -> Z3native.ptr -> expr = fun ctx no -> + if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no) == QUANTIFIER_AST then + Expr(z3_native_object_of_ast_ptr ctx no) + else + let s = Z3native.get_sort (context_gno ctx) no in + let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in + if (Z3native.is_algebraic_number (context_gno ctx) no) then + Expr(z3_native_object_of_ast_ptr ctx no) + else + if (Z3native.is_numeral_ast (context_gno ctx) no) then + if (sk == INT_SORT or sk == REAL_SORT or sk == BV_SORT) then + Expr(z3_native_object_of_ast_ptr ctx no) + else + raise (Z3native.Exception "Unsupported numeral object") + else + Expr(z3_native_object_of_ast_ptr ctx no) + + let expr_aton ( a : expr array ) = + let f ( e : expr ) = match e with Expr(a) -> (ptr_of_ast a) in + Array.map f a + + let expr_of_func_app : context -> func_decl -> expr array -> expr = fun ctx f args -> + match f with FuncDecl(fa) -> + let o = Z3native.mk_app (context_gno ctx) (ptr_of_ast fa) (Array.length args) (expr_aton args) in + expr_of_ptr ctx o +end + + +open Internal + + + +(* Sort coercions *) +let ast_of_sort s = match s with Sort(x) -> x +let sort_of_uninterpreted_sort s = match s with UninterpretedSort(x) -> x +let sort_of_bool_sort s = match s with BoolSort(x) -> x +let sort_of_array_sort s = match s with ArraySort(x) -> x +let sort_of_set_sort s = match s with SetSort(x) -> x +let sort_of_datatype_sort s = match s with DatatypeSort(x) -> x +let sort_of_relation_sort s = match s with RelationSort(x) -> x +let sort_of_finite_domain_sort s = match s with FiniteDomainSort(x) -> x +let sort_of_enum_sort s = match s with EnumSort(x) -> x +let sort_of_list_sort s = match s with ListSort(x) -> x +let sort_of_tuple_sort s = match s with TupleSort(x) -> x +let sort_of_arith_sort s = match s with ArithSort(x) -> x +let sort_of_bitvec_sort s = match s with BitVecSort(x) -> x +let arith_sort_of_int_sort s = match s with IntSort(x) -> x +let arith_sort_of_real_sort s = match s with RealSort(x) -> x + +let uninterpreted_sort_of_sort s = match s with Sort(a) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.UNINTERPRETED_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + UninterpretedSort(s) + +let bool_sort_of_sort s = match s with Sort(a) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.BOOL_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + BoolSort(s) + +let array_sort_of_sort s = match s with Sort(a) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.ARRAY_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + ArraySort(s) + +let datatype_sort_of_sort s = match s with Sort(a) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.DATATYPE_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + DatatypeSort(s) + +let relation_sort_of_sort s = match s with Sort(a) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.RELATION_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + RelationSort(s) + +let finite_domain_sort_of_sort s = match s with Sort(a) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.FINITE_DOMAIN_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + FiniteDomainSort(s) + +let arith_sort_of_sort s = match s with Sort(a) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) in + if (q != Z3enums.INT_SORT && q != Z3enums.REAL_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + ArithSort(s) + +let bitvec_sort_of_sort s = match s with Sort(a) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.BV_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + BitVecSort(s) + +let int_sort_of_arith_sort s = match s with ArithSort(Sort(a)) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.INT_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + IntSort(s) + +let real_sort_of_arith_sort s = match s with ArithSort(Sort(a)) -> + if ((Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) (z3obj_gno a))) != Z3enums.REAL_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + RealSort(s) + +(* FuncDecl coercions *) +let ast_of_func_decl f = match f with FuncDecl(x) -> x + +(* Expr coercions *) +let ast_of_expr e = match e with Expr(a) -> a +let expr_of_bool_expr e = match e with BoolExpr(x) -> x +let expr_of_arith_expr e = match e with ArithExpr(x) -> x +let expr_of_bitvec_expr e = match e with BitVecExpr(x) -> x +let expr_of_array_expr e = match e with ArrayExpr(x) -> x +let expr_of_datatype_expr e = match e with DatatypeExpr(x) -> x + +let arith_expr_of_int_expr e = match e with IntExpr(x) -> x +let arith_expr_of_real_expr e = match e with RealExpr(x) -> x + +let int_expr_of_int_num e = match e with IntNum(x) -> x +let real_expr_of_rat_num e = match e with RatNum(x) -> x +let arith_expr_of_algebraic_num e = match e with AlgebraicNum(x) -> x +let bitvec_expr_of_bitvec_num e = match e with BitVecNum(x) -> x + +let expr_of_quantifier e = match e with Quantifier(x) -> x +let ast_of_pattern e = match e with Pattern(x) -> x + + +let expr_of_ast a = + let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in + if (q != Z3enums.APP_AST && q != VAR_AST && q != QUANTIFIER_AST && q != NUMERAL_AST) then + raise (Z3native.Exception "Invalid coercion") + else + Expr(a) + +let bool_expr_of_expr e = + match e with Expr(no) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.BOOL_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + BoolExpr(e) + +let arith_expr_of_expr e = + match e with Expr(no) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.INT_SORT && q != Z3enums.REAL_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + ArithExpr(e) + +let bitvec_expr_of_expr e = + match e with Expr(no) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.BV_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + BitVecExpr(e) + +let array_expr_of_expr e = + match e with Expr(no) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.ARRAY_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + ArrayExpr(e) + +let datatype_expr_of_expr e = + match e with Expr(no) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.DATATYPE_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + DatatypeExpr(e) + +let int_expr_of_arith_expr e = + match e with ArithExpr(Expr(no)) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.INT_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + IntExpr(e) + +let real_expr_of_arith_expr e = + match e with ArithExpr(Expr(no)) -> + let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.REAL_SORT) then + raise (Z3native.Exception "Invalid coercion") + else + RealExpr(e) + +let int_num_of_int_expr e = + match e with IntExpr(ArithExpr(Expr(no))) -> + if (not (Z3native.is_numeral_ast (z3obj_gnc no) (z3obj_gno no))) then + raise (Z3native.Exception "Invalid coercion") + else + IntNum(e) + +let rat_num_of_real_expr e = + match e with RealExpr(ArithExpr(Expr(no))) -> + if (not (Z3native.is_numeral_ast (z3obj_gnc no) (z3obj_gno no))) then + raise (Z3native.Exception "Invalid coercion") + else + RatNum(e) + +let algebraic_num_of_arith_expr e = + match e with ArithExpr(Expr(no)) -> + if (not (Z3native.is_algebraic_number (z3obj_gnc no) (z3obj_gno no))) then + raise (Z3native.Exception "Invalid coercion") + else + AlgebraicNum(e) + +let bitvec_num_of_bitvec_expr e = + match e with BitVecExpr(Expr(no)) -> + if (not (Z3native.is_numeral_ast (z3obj_gnc no) (z3obj_gno no))) then + raise (Z3native.Exception "Invalid coercion") + else + BitVecNum(e) + +let quantifier_of_expr e = + match e with Expr(no) -> + let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc no) (z3obj_gno no))) in + if (q != Z3enums.QUANTIFIER_AST) then + raise (Z3native.Exception "Invalid coercion") + else + Quantifier(e) + +let pattern_of_ast a = + (* CMW: Unchecked ok? *) + Pattern(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 = @@ -28,6 +499,7 @@ struct let append s = Z3native.append_log s end + (** Version information *) module Version = struct @@ -52,11 +524,6 @@ struct string_of_int rev ^ "." end -(**/**) -(* Some helpers. *) - -let null = Z3native.mk_null() -let is_null o = (Z3native.is_null o) let mk_list ( f : int -> 'a ) ( n : int ) = let rec mk_list' ( f : int -> 'a ) ( i : int ) ( n : int ) ( tail : 'a list ) : 'a list = @@ -66,49 +533,8 @@ let mk_list ( f : int -> 'a ) ( n : int ) = (mk_list' f (i+1) n ((f i) :: tail)) in mk_list' f 0 n [] -(**/**) -(**/**) -type z3_native_context = { m_n_ctx : Z3native.z3_context; m_n_obj_cnt: int; } -(**/**) -type context = z3_native_context - -(**/**) - -let context_dispose ctx = - if ctx.m_n_obj_cnt == 0 then ( - (* Printf.printf "Disposing context \n" ; *) - (Z3native.del_context ctx.m_n_ctx) - ) else ( - Printf.printf "NOT DISPOSING context because it still has %d objects alive\n" ctx.m_n_obj_cnt; - (* re-queue for finalization? *) - ) - -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) ; - let v = Z3native.mk_context_rc cfg in - Z3native.del_config(cfg) ; - Z3native.set_ast_print_mode v (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ; - (* Printf.printf "Installing finalizer on context \n" ; *) - let res = { m_n_ctx = v; m_n_obj_cnt = 0 } in - let f = fun o -> context_dispose o in - Gc.finalise f res; - res -(* CMW: Install error handler here! - m_n_err_handler = new Z3native.error_handler(NativeErrorHandler); keep reference so it doesn't get collected. - Z3native.set_error_handler(m_ctx, m_n_err_handler); - GC.SuppressFinalize(this); -*) - -let context_add1 ctx = ignore (ctx.m_n_obj_cnt = ctx.m_n_obj_cnt + 1) -let context_sub1 ctx = ignore (ctx.m_n_obj_cnt = ctx.m_n_obj_cnt - 1) -let context_gno ctx = ctx.m_n_ctx - -(**/**) - (** Create a context object. Most interactions with Z3 are interpreted in some context; many users will only @@ -130,113 +556,14 @@ let context_gno ctx = ctx.m_n_ctx *) let mk_context ( cfg : ( string * string ) list ) = - context_create cfg + create_context cfg -(**/**) -class virtual z3object ctx_init obj_init = -object (self) - val mutable m_ctx : context = ctx_init - val mutable m_n_obj : Z3native.ptr option = obj_init - - initializer - (match m_n_obj with - | Some (x) -> self#incref (context_gno m_ctx) x; - (context_add1 m_ctx) - | None -> () - ); - (* Printf.printf "Installing finalizer on z3object %d \n" (Oo.id self) ; *) - let f = fun o -> o#dispose in - let v = self in - Gc.finalise f v - - method virtual incref : Z3native.ptr -> Z3native.ptr -> unit - method virtual decref : Z3native.ptr -> Z3native.ptr -> unit - - method dispose = - (* Printf.printf "Disposing z3object %d \n" (Oo.id self) ; *) - (match m_n_obj with - | Some (x) -> - self#decref (context_gno m_ctx) x; - (context_sub1 m_ctx) ; - m_n_obj <- None; - | None -> () - ); - - method gno = match m_n_obj with - | Some(x) -> x - | None -> raise (Z3native.Exception "Z3 object lost") - - method sno (ctx : context) o = - (context_add1 m_ctx) ; - self#incref (context_gno ctx) o ; - (match m_n_obj with - | Some(x) -> self#decref (context_gno ctx) x ; (context_sub1 m_ctx) - | None -> () - ); - m_n_obj <- Some o - - method gc = m_ctx - method gnc = (context_gno m_ctx) -end - - - -type z3_native_object = { - m_ctx : context ; - mutable m_n_obj : Z3native.ptr ; - inc_ref : Z3native.z3_context -> Z3native.ptr -> unit; - dec_ref : Z3native.z3_context -> Z3native.ptr -> unit } - -let z3obj_gc o = o.m_ctx -let z3obj_gnc o = (context_gno o.m_ctx) - -let z3obj_gno o = o.m_n_obj -let z3obj_sno o ctx no = - (context_add1 ctx) ; - o.inc_ref (context_gno ctx) no ; - ( - if not (is_null o.m_n_obj) then - o.dec_ref (context_gno ctx) o.m_n_obj ; - (context_sub1 ctx) - ) ; - o.m_n_obj <- no - -let z3obj_dispose o = - if not (is_null o.m_n_obj) then - ( - o.dec_ref (z3obj_gnc o) o.m_n_obj ; - (context_sub1 (z3obj_gc o)) - ) ; - o.m_n_obj <- null - -let z3obj_create o = - let f = fun o -> (z3obj_dispose o) in - Gc.finalise f o - -let z3obj_nil_ref x y = () - -let array_to_native a = - let f e = (z3obj_gno e) in - Array.map f a -(**/**) (** Symbols are used to name several term and type constructors *) module Symbol = -struct - (** Int symbol objects *) - type int_symbol = z3_native_object - - (** String symbol objects *) - type string_symbol = z3_native_object - - (** Symbol Objects *) - type symbol = - | S_Int of int_symbol - | S_Str of string_symbol - - (**/**) +struct let create_i ( ctx : context ) ( no : Z3native.ptr ) = let res : int_symbol = { m_ctx = ctx ; m_n_obj = null ; @@ -255,6 +582,11 @@ struct (z3obj_create res) ; res + let create ( ctx : context ) ( no : Z3native.ptr ) = + match (symbol_kind_of_int (Z3native.get_symbol_kind (context_gno ctx) no)) with + | INT_SYMBOL -> S_Int (create_i ctx no) + | STRING_SYMBOL -> S_Str (create_s ctx no) + let gc ( x : symbol ) = match x with | S_Int(n) -> (z3obj_gc n) @@ -269,17 +601,7 @@ struct match x with | 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 -> S_Int (create_i ctx no) - | STRING_SYMBOL -> S_Str (create_s ctx no) - - let aton a = - let f e = (gno e) in - Array.map f a - (**/**) - + (** The kind of the symbol (int or string) *) let kind ( o : symbol ) = (symbol_kind_of_int (Z3native.get_symbol_kind (gnc o) (gno o))) @@ -327,48 +649,11 @@ end (** The abstract syntax tree (AST) module *) -module rec AST : -sig - type ast = z3_native_object - -(**/**) - val create : context -> Z3native.ptr -> ast - val aton : ast array -> Z3native.ptr array -(**/**) - - module ASTVectors : sig - type ast_vector - val create : context -> Z3native.ptr -> ast_vector - val get_size : ast_vector -> int - val get : ast_vector -> int -> ast - end - - 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 - (**/**) - +module AST = +struct (** Vectors of ASTs *) - module ASTVectors = + module ASTVector = struct - type ast_vector = z3_native_object - - (**/**) let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_vector = { m_ctx = ctx ; m_n_obj = null ; @@ -377,7 +662,7 @@ end = struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** The size of the vector *) let get_size ( x : ast_vector ) = @@ -411,7 +696,7 @@ end = struct (** Translates all ASTs in the vector to . @param to_ctx A context - @return A new ASTVectors + @return A new ASTVector *) let translate ( x : ast_vector ) ( to_ctx : context ) = create to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) @@ -423,10 +708,8 @@ end = struct (** Map from AST to AST *) module ASTMap = - struct - type ast_map = z3_native_object - - (**/**) + struct + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : ast_map = { m_ctx = ctx ; m_n_obj = null ; @@ -435,7 +718,7 @@ end = struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Checks whether the map contains the key . @param k An AST @@ -476,7 +759,7 @@ end = struct (** The keys stored in the map. *) let get_keys ( x : ast_map ) = - ASTVectors.create (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 ) = @@ -576,7 +859,7 @@ end = struct if (z3obj_gnc x) == (context_gno to_ctx) then x else - create to_ctx (Z3native.translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) + ast_of_ptr to_ctx (Z3native.translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) (** Wraps an AST. @@ -590,7 +873,7 @@ end = struct @param nativeObject The native pointer to wrap. *) let wrap ( ctx : context ) ( ptr : Z3native.ptr ) = - create ctx ptr + ast_of_ptr ctx ptr (** Unwraps an AST. @@ -603,66 +886,17 @@ end = struct @param a The AST to unwrap. *) - 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") -(**/**) + let unwrap_ast ( x : ast ) = (z3obj_gno x) end (** The Sort module implements type information for ASTs *) -and Sort : -sig - type sort = Sort of AST.ast - type uninterpreted_sort = UninterpretedSort of sort - - val create : context -> Z3native.ptr -> sort - val gc : sort -> context - val gnc : sort -> Z3native.ptr - val gno : sort -> Z3native.ptr - val aton : sort array -> Z3native.ptr array -end = struct - type sort = Sort of AST.ast - type uninterpreted_sort = UninterpretedSort of sort - - (**/**) +module Sort = +struct + 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 @@ -700,7 +934,7 @@ end = struct (** Create a new uninterpreted sort. *) - let mk_uninterpreted ( ctx : context ) ( s : Symbol.symbol ) = + let mk_uninterpreted ( ctx : context ) ( s : symbol ) = let res = { m_ctx = ctx ; m_n_obj = null ; inc_ref = Z3native.inc_ref ; @@ -718,71 +952,37 @@ end (** Function declarations *) -and FuncDecl : -sig - type func_decl = FuncDecl of AST.ast - - val create : context -> Z3native.ptr -> func_decl - val gc : func_decl -> context - val gno : func_decl -> Z3native.ptr - val gnc : func_decl -> Z3native.ptr - val aton : func_decl array -> Z3native.ptr array - - val get_domain_size : func_decl -> int - val get_decl_kind : func_decl -> Z3enums.decl_kind - val get_arity : func_decl -> int -end = struct - 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.sort array ) ( range : Sort.sort ) = +module FuncDecl = +struct + (**/**) + let create_ndr ( ctx : context ) ( name : 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))) ; + let f x = (ptr_of_ast (ast_of_sort x)) in + (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (Array.length domain) (Array.map f domain) (Sort.gno range))) ; (z3obj_create res) ; FuncDecl(res) - let create_pdr ( ctx : context) ( prefix : string ) ( domain : Sort.sort array ) ( range : Sort.sort ) = + 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))) ; + let f x = (ptr_of_ast (ast_of_sort x)) in + (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (Array.length domain) (Array.map f 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 - + struct (** The kind of the parameter. *) let get_kind ( x : parameter ) = (match x with @@ -840,13 +1040,13 @@ end = struct (** Creates a new function declaration. *) - let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort array ) ( range : Sort.sort ) = + let mk_func_decl ( ctx : context ) ( name : 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.sort array ) ( range : Sort.sort ) = + 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 (** @@ -854,19 +1054,19 @@ end = struct *) - let mk_fresh_func_decl ( ctx : context ) ( prefix : string ) ( domain : Sort.sort array ) ( range : Sort.sort ) = + 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.sort ) = + let mk_const_decl ( ctx : context ) ( name : 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.sort ) = + let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : sort ) = create_ndr ctx (Symbol.mk_string ctx name) [||] range (** @@ -874,7 +1074,7 @@ end = struct *) - let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : Sort.sort ) = + let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : sort ) = create_pdr ctx prefix [||] range @@ -917,14 +1117,14 @@ end = struct *) 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 + let f i = sort_of_ptr (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)) + sort_of_ptr (gc x) (Z3native.get_range (gnc x) (gno x)) (** The kind of the function declaration. @@ -947,13 +1147,13 @@ end = struct 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 -> Parameter.P_Int (Z3native.get_decl_int_parameter (gnc x) (gno x) i) - | PARAMETER_DOUBLE -> Parameter.P_Dbl (Z3native.get_decl_double_parameter (gnc x) (gno x) i) - | PARAMETER_SYMBOL-> Parameter.P_Sym (Symbol.create (gc x) (Z3native.get_decl_symbol_parameter (gnc x) (gno x) i)) - | PARAMETER_SORT -> Parameter.P_Srt (Sort.create (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i)) - | PARAMETER_AST -> Parameter.P_Ast (AST.create (gc x) (Z3native.get_decl_ast_parameter (gnc x) (gno x) i)) - | PARAMETER_FUNC_DECL -> Parameter.P_Fdl (create (gc x) (Z3native.get_decl_func_decl_parameter (gnc x) (gno x) i)) - | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gnc x) (gno x) i) + | 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_of_ptr (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i)) + | PARAMETER_AST -> P_Ast (ast_of_ptr (gc x) (Z3native.get_decl_ast_parameter (gnc x) (gno x) i)) + | PARAMETER_FUNC_DECL -> P_Fdl (func_decl_of_ptr (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 @@ -961,7 +1161,7 @@ end = struct 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 + let apply ( x : func_decl ) ( args : expr array ) = expr_of_func_app (gc x) x args end (** @@ -969,43 +1169,12 @@ end A Params objects represents a configuration in the form of symbol/value pairs. *) -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 - val validate : param_descrs -> params -> unit - end -end = struct - type params = z3_native_object - - (**/**) - 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_create res) ; - res - (**/**) - +module Params = +struct (** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *) - module ParamDescrs : - sig - type param_descrs = z3_native_object - - val create : context -> Z3native.ptr -> param_descrs - val validate : param_descrs -> params -> unit - end = struct - type param_descrs = z3_native_object - - (**/**) + module ParamDescrs = + struct + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : param_descrs = { m_ctx = ctx ; m_n_obj = null ; @@ -1014,14 +1183,14 @@ end = struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Validate a set of parameters. *) let validate ( x : param_descrs ) ( p : params ) = Z3native.params_validate (z3obj_gnc x) (z3obj_gno p) (z3obj_gno x) (** Retrieve kind of parameter. *) - let get_kind ( x : param_descrs ) ( name : Symbol.symbol ) = + let get_kind ( x : param_descrs ) ( name : symbol ) = (param_kind_of_int (Z3native.param_descrs_get_kind (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name))) (** Retrieve all names of parameters. *) @@ -1040,25 +1209,25 @@ end = struct (** Adds a parameter setting. *) - let add_bool ( x : params ) ( name : Symbol.symbol ) ( value : bool ) = + let add_bool ( x : params ) ( name : symbol ) ( value : bool ) = Z3native.params_set_bool (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value (** Adds a parameter setting. *) - let add_int ( x : params ) (name : Symbol.symbol ) ( value : int ) = + let add_int ( x : params ) (name : symbol ) ( value : int ) = Z3native.params_set_uint (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value (** Adds a parameter setting. *) - let add_double ( x : params ) ( name : Symbol.symbol ) ( value : float ) = + let add_double ( x : params ) ( name : symbol ) ( value : float ) = Z3native.params_set_double (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value (** Adds a parameter setting. *) - let add_symbol ( x : params ) ( name : Symbol.symbol ) ( value : Symbol.symbol ) = + let add_symbol ( x : params ) ( name : symbol ) ( value : symbol ) = Z3native.params_set_symbol (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) (Symbol.gno value) (** @@ -1081,14 +1250,20 @@ end = struct (** Adds a parameter setting. *) - let add_s_symbol ( x : params ) ( name : string ) ( value : Symbol.symbol ) = + let add_s_symbol ( x : params ) ( name : string ) ( value : symbol ) = add_symbol x (Symbol.mk_string (z3obj_gc x) name) value (** Creates a new parameter set *) let mk_params ( ctx : context ) = - create ctx (Z3native.mk_params (context_gno ctx)) + 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 (Z3native.mk_params (context_gno ctx))) ; + (z3obj_create res) ; + res (** A string representation of the parameter set. @@ -1097,76 +1272,16 @@ end = struct end (** General expressions (terms) *) -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 - val is_numeral : expr -> bool - val to_string : expr -> string -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.AlgebraicNumbers.create_num ctx obj) with Arithmetic.AlgebraicNumbers.AlgebraicNum(Arithmetic.ArithExpr(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.Integers.create_num ctx obj) with Arithmetic.Integers.IntNum(Arithmetic.Integers.IntExpr(Arithmetic.ArithExpr(e))) -> e) - | REAL_SORT -> (match (Arithmetic.Reals.create_num ctx obj) with Arithmetic.Reals.RatNum(Arithmetic.Reals.RealExpr(Arithmetic.ArithExpr(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_expr ctx obj) with Booleans.BoolExpr(e) -> e) - | INT_SORT -> (match (Arithmetic.Integers.create_expr ctx obj) with Arithmetic.Integers.IntExpr(Arithmetic.ArithExpr(e)) -> e) - | REAL_SORT -> (match (Arithmetic.Reals.create_expr ctx obj) with Arithmetic.Reals.RealExpr(Arithmetic.ArithExpr(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) - - let aton (a : expr array) = - let f (e : expr) = (gno e) in - Array.map f a - (**/**) - +module Expr = +struct (** 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 -> 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)) + let simplify ( x : expr ) ( p : params option ) = match p with + | None -> expr_of_ptr (c_of_expr x) (Z3native.simplify (nc_of_expr x) (ptr_of_expr x)) + | Some pp -> expr_of_ptr (c_of_expr x) (Z3native.simplify_ex (nc_of_expr x) (ptr_of_expr x) (z3obj_gno pp)) (** a string describing all available parameters to Expr.Simplify. @@ -1183,24 +1298,24 @@ end = struct (** The function declaration of the function that is applied in this expression. *) - let get_func_decl ( x : expr ) = FuncDecl.create (gc x) (Z3native.get_app_decl (gnc x) (gno x)) + let get_func_decl ( x : expr ) = func_decl_of_ptr (c_of_expr x) (Z3native.get_app_decl (nc_of_expr x) (ptr_of_expr 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 (gnc x) (gno x)) + let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (nc_of_expr x) (ptr_of_expr x)) (** The number of arguments of the expression. *) - let get_num_args ( x : expr ) = Z3native.get_app_num_args (gnc x) (gno x) + let get_num_args ( x : expr ) = Z3native.get_app_num_args (nc_of_expr x) (ptr_of_expr x) (** The arguments of the expression. *) let get_args ( x : expr ) = let n = (get_num_args x) in - let f i = create (gc x) (Z3native.get_app_arg (gnc x) (gno x) i) in + let f i = expr_of_ptr (c_of_expr x) (Z3native.get_app_arg (nc_of_expr x) (ptr_of_expr x) i) in Array.init n f (** @@ -1211,7 +1326,7 @@ end = struct if (Array.length args <> (get_num_args x)) then raise (Z3native.Exception "Number of arguments does not match") else - create (gc x) (Z3native.update_term (gnc x) (gno x) (Array.length args) (aton args)) + expr_of_ptr (c_of_expr x) (Z3native.update_term (nc_of_expr x) (ptr_of_expr x) (Array.length args) (expr_aton args)) (** Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs. @@ -1224,7 +1339,7 @@ end = struct if (Array.length from) <> (Array.length to_) then raise (Z3native.Exception "Argument sizes do not match") else - create (gc x) (Z3native.substitute (gnc x) (gno x) (Array.length from) (aton from) (aton to_)) + expr_of_ptr (c_of_expr x) (Z3native.substitute (nc_of_expr x) (ptr_of_expr x) (Array.length from) (expr_aton from) (expr_aton to_)) (** Substitute every occurrence of from in the expression with to. @@ -1239,48 +1354,47 @@ end = 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 (gc x) (Z3native.substitute_vars (gnc x) (gno x) (Array.length to_) (aton to_)) + expr_of_ptr (c_of_expr x) (Z3native.substitute_vars (nc_of_expr x) (ptr_of_expr x) (Array.length to_) (expr_aton to_)) - (** Translates (copies) the term to the Context . @param ctx A context @return A copy of the term which is associated with *) let translate ( x : expr ) to_ctx = - if (gc x) == to_ctx then + if (c_of_expr x) == to_ctx then x else - create to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx)) + expr_of_ptr to_ctx (Z3native.translate (nc_of_expr x) (ptr_of_expr x) (context_gno to_ctx)) (** Returns a string representation of the expression. *) - let to_string ( x : expr ) = Z3native.ast_to_string (gnc x) (gno x) + let to_string ( x : expr ) = Z3native.ast_to_string (nc_of_expr x) (ptr_of_expr x) (** Indicates whether the term is a numeral *) - let is_numeral ( x : expr ) = (Z3native.is_numeral_ast (gnc x) (gno x)) + let is_numeral ( x : expr ) = (Z3native.is_numeral_ast (nc_of_expr x) (ptr_of_expr 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 (gnc x) (gno x) + let is_well_sorted ( x : expr ) = Z3native.is_well_sorted (nc_of_expr x) (ptr_of_expr x) (** The Sort of the term. *) - let get_sort ( x : expr ) = Sort.create (gc x) (Z3native.get_sort (gnc x) (gno x)) + let get_sort ( x : expr ) = sort_of_ptr (c_of_expr x) (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x)) (** Indicates whether the term has Boolean sort. *) 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))) + (Z3native.is_eq_sort (nc_of_expr x) + (Z3native.mk_bool_sort (nc_of_expr x)) + (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x))) (** Indicates whether the term represents a constant. @@ -1366,14 +1480,14 @@ end = struct (** Creates a new Constant of sort and named . *) - 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)) + let mk_const ( ctx : context ) ( name : symbol ) ( range : sort ) = + expr_of_ptr 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.sort ) = + let mk_const_s ( ctx : context ) ( name : string ) ( range : sort ) = mk_const ctx (Symbol.mk_string ctx name) range @@ -1381,21 +1495,21 @@ end = struct Creates a constant from the func_decl . @param f An expression of a 0-arity function *) - let mk_const_f ( ctx : context ) ( f : FuncDecl.func_decl ) = - create_fa ctx f [||] + let mk_const_f ( ctx : context ) ( f : func_decl ) = + expr_of_func_app ctx f [||] (** Creates a fresh constant of sort and a name prefixed with . *) - let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : Sort.sort ) = - create ctx (Z3native.mk_fresh_const (context_gno ctx) prefix (Sort.gno range)) + let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : sort ) = + expr_of_ptr ctx (Z3native.mk_fresh_const (context_gno ctx) prefix (Sort.gno range)) (** Create a new function application. *) - let mk_app ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : expr array ) = - create_fa ctx f args + let mk_app ( ctx : context ) ( f : func_decl ) ( args : expr array ) = + expr_of_func_app ctx f args (** Create a numeral of a given sort. @@ -1403,8 +1517,8 @@ end = 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.sort ) = - create ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno ty)) + let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : sort ) = + expr_of_ptr 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. @@ -1413,50 +1527,31 @@ end = struct @param ty Sort of the numeral @return A Term with value and type *) - let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : Sort.sort ) = - create ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty)) + let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : sort ) = + expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty)) end (** Boolean expressions *) -and Booleans : -sig - type bool_expr = BoolExpr of Expr.expr - type bool_sort = BoolSort of Sort.sort +module Boolean = +struct + let bool_expr_of_ptr ( ctx : context ) ( no : Z3native.ptr ) = + let a = (ast_of_ptr ctx no) in + BoolExpr(Expr(a)) - val create_expr : context -> Z3native.ptr -> bool_expr - val create_sort : context -> Z3native.ptr -> bool_sort - val gc : bool_expr -> context - val gnc : bool_expr -> Z3native.ptr - val gno : bool_expr -> Z3native.ptr - 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_expr ( ctx : context ) ( no : Z3native.ptr ) = - let a = (AST.create ctx no) in - BoolExpr(Expr.Expr(a)) + let bool_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) = + BoolSort(sort_of_ptr ctx no) - let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - BoolSort(Sort.create ctx no) - - 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 gc ( x : bool_expr ) = match x with BoolExpr(e) -> (c_of_expr e) + let gnc ( x : bool_expr ) = match x with BoolExpr(e) -> (nc_of_expr e) + let gno ( x : bool_expr ) = match x with BoolExpr(e) -> (ptr_of_expr e) let mk_sort ( ctx : context ) = - BoolSort(Sort.create ctx (Z3native.mk_bool_sort (context_gno ctx))) + BoolSort(sort_of_ptr ctx (Z3native.mk_bool_sort (context_gno ctx))) (** Create a Boolean constant. *) - let mk_const ( ctx : context ) ( name : Symbol.symbol ) = + let mk_const ( ctx : context ) ( name : symbol ) = let s = (match (mk_sort ctx) with BoolSort(q) -> q) in BoolExpr(Expr.mk_const ctx name s) @@ -1470,13 +1565,13 @@ end = struct The true Term. *) let mk_true ( ctx : context ) = - create_expr ctx (Z3native.mk_true (context_gno ctx)) + bool_expr_of_ptr ctx (Z3native.mk_true (context_gno ctx)) (** The false Term. *) let mk_false ( ctx : context ) = - create_expr ctx (Z3native.mk_false (context_gno ctx)) + bool_expr_of_ptr ctx (Z3native.mk_false (context_gno ctx)) (** Creates a Boolean value. @@ -1487,20 +1582,20 @@ end = struct (** Creates the equality = . *) - let mk_eq ( ctx : context ) ( x : Expr.expr ) ( y : Expr.expr ) = - create_expr ctx (Z3native.mk_eq (context_gno ctx) (Expr.gno x) (Expr.gno y)) + let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) = + bool_expr_of_ptr ctx (Z3native.mk_eq (context_gno ctx) (ptr_of_expr x) (ptr_of_expr y)) (** Creates a distinct term. *) - let mk_distinct ( ctx : context ) ( args : Expr.expr array ) = - create_expr ctx (Z3native.mk_distinct (context_gno ctx) (Array.length args) (Expr.aton args)) + let mk_distinct ( ctx : context ) ( args : expr array ) = + bool_expr_of_ptr 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_expr ctx (Z3native.mk_not (context_gno ctx) (gno a)) + bool_expr_of_ptr ctx (Z3native.mk_not (context_gno ctx) (gno a)) (** Create an expression representing an if-then-else: ite(t1, t2, t3). @@ -1509,103 +1604,70 @@ end = struct @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) (gno t1) (gno t2) (gno t3)) + bool_expr_of_ptr 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_expr ctx (Z3native.mk_iff (context_gno ctx) (gno t1) (gno t2)) + bool_expr_of_ptr 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_expr ctx (Z3native.mk_implies (context_gno ctx) (gno t1) (gno t2)) + bool_expr_of_ptr 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_expr ctx (Z3native.mk_xor (context_gno ctx) (gno t1) (gno t2)) + bool_expr_of_ptr 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_expr ctx (Z3native.mk_and (context_gno ctx) (Array.length args) (aton args)) + let f x = (ptr_of_expr (expr_of_bool_expr x)) in + bool_expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (Array.length args) (Array.map f args)) (** Create an expression representing the OR of args *) let mk_or ( ctx : context ) ( args : bool_expr array ) = - create_expr ctx (Z3native.mk_or (context_gno ctx) (Array.length args) (aton args)) + let f x = (ptr_of_expr (expr_of_bool_expr x)) in + bool_expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (Array.length args) (Array.map f args)) end (** Quantifier expressions *) -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) - (**/**) - +module Quantifier = +struct + let gc ( x : quantifier ) = match (x) with Quantifier(e) -> (c_of_expr e) + let gnc ( x : quantifier ) = match (x) with Quantifier(e) -> (nc_of_expr e) + let gno ( x : quantifier ) = match (x) with Quantifier(e) -> (ptr_of_expr e) + (** Quantifier patterns Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern. *) - module 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) - + module Pattern = struct 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) - let aton (a : pattern array) = - let f (e : pattern) = (gno e) in - Array.map f a - (**/**) - (** The number of terms in the pattern. *) let get_num_terms ( x : pattern ) = - Z3native.get_pattern_num_terms (gnc x) (gno x) - + 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 = (Expr.create (gc x) (Z3native.get_pattern (gnc x) (gno x) i)) in + let f i = (expr_of_ptr (gc x) (Z3native.get_pattern (gnc x) (gno x) i)) in Array.init n f (** @@ -1632,11 +1694,11 @@ end = struct on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its index. *) - let get_index ( x : Expr.expr ) = - if not (AST.is_var (match x with Expr.Expr(a) -> a)) then + let get_index ( x : expr ) = + if not (AST.is_var (match x with Expr(a) -> a)) then raise (Z3native.Exception "Term is not a bound variable.") else - Z3native.get_index_value (Expr.gnc x) (Expr.gno x) + Z3native.get_index_value (nc_of_expr x) (ptr_of_expr x) (** Indicates whether the quantifier is universal. @@ -1664,7 +1726,7 @@ end = struct *) let get_patterns ( x : quantifier ) = let n = (get_num_patterns x) in - let f i = (Patterns.create (gc x) (Z3native.get_quantifier_pattern_ast (gnc x) (gno x) i)) in + let f i = Pattern (z3_native_object_of_ast_ptr (gc x) (Z3native.get_quantifier_pattern_ast (gnc x) (gno x) i)) in Array.init n f (** @@ -1677,7 +1739,7 @@ end = struct *) let get_no_patterns ( x : quantifier ) = let n = (get_num_patterns x) in - let f i = (Patterns.create (gc x) (Z3native.get_quantifier_no_pattern_ast (gnc x) (gno x) i)) in + let f i = Pattern (z3_native_object_of_ast_ptr (gc x) (Z3native.get_quantifier_no_pattern_ast (gnc x) (gno x) i)) in Array.init n f (** @@ -1698,31 +1760,31 @@ end = struct *) let get_bound_variable_sorts ( x : quantifier ) = let n = (get_num_bound x) in - let f i = (Sort.create (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) i)) in + let f i = (sort_of_ptr (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 ) = - Booleans.create_expr (gc x) (Z3native.get_quantifier_body (gnc x) (gno x)) + Boolean.bool_expr_of_ptr (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.sort ) = - Expr.create ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) + let mk_bound ( ctx : context ) ( index : int ) ( ty : sort ) = + expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) (** Create a quantifier pattern. *) - let mk_pattern ( ctx : context ) ( terms : Expr.expr array ) = + let mk_pattern ( ctx : context ) ( terms : expr array ) = if (Array.length terms) == 0 then raise (Z3native.Exception "Cannot create a pattern from zero terms") else - Patterns.create ctx (Z3native.mk_pattern (context_gno ctx) (Array.length terms) (Expr.aton terms)) + Pattern(z3_native_object_of_ast_ptr ctx (Z3native.mk_pattern (context_gno ctx) (Array.length terms) (expr_aton terms))) (** Create a universal Quantifier. @@ -1743,96 +1805,96 @@ end = struct @param quantifierID optional symbol to track quantifier. @param skolemID optional symbol to track skolem constants. *) - 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 ) = + let mk_forall ( ctx : context ) ( sorts : sort array ) ( names : symbol array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : 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 - 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)) + Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) true + (match weight with | None -> 1 | Some(x) -> x) + (Array.length patterns) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (Array.length sorts) (let f x = (ptr_of_ast (ast_of_sort x)) in (Array.map f sorts)) + (let f x = (Symbol.gno x) in (Array.map f names)) + (ptr_of_expr body))) else - 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)) - + Quantifier(expr_of_ptr 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) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (Array.length nopatterns) (expr_aton nopatterns) + (Array.length sorts) (let f x = (ptr_of_ast (ast_of_sort x)) in (Array.map f sorts)) + (let f x = (Symbol.gno x) in (Array.map f names)) + (ptr_of_expr body))) + (** Create a universal Quantifier. *) - 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 ) = + let mk_forall_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) = if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then - 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)) + Quantifier(expr_of_ptr 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) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (ptr_of_expr body))) else - 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)) + Quantifier(expr_of_ptr 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) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (Array.length nopatterns) (expr_aton nopatterns) + (ptr_of_expr body))) (** Create an existential Quantifier. *) - 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 ) = + let mk_exists ( ctx : context ) ( sorts : sort array ) ( names : symbol array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : 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 - 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)) + Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) false + (match weight with | None -> 1 | Some(x) -> x) + (Array.length patterns) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (Array.length sorts) (let f x = (ptr_of_ast (ast_of_sort x)) in (Array.map f sorts)) + (let f x = (Symbol.gno x) in (Array.map f names)) + (ptr_of_expr body))) else - 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)) - + Quantifier(expr_of_ptr 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) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (Array.length nopatterns) (expr_aton nopatterns) + (Array.length sorts) (let f x = (ptr_of_ast (ast_of_sort x)) in (Array.map f sorts)) + (let f x = (Symbol.gno x) in (Array.map f names)) + (ptr_of_expr body))) + (** Create an existential Quantifier. *) - 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 ) = + let mk_exists_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) = if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then - 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)) + Quantifier(expr_of_ptr 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) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (ptr_of_expr body))) else - 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)) + Quantifier(expr_of_ptr 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) (let f x = (ptr_of_ast (ast_of_pattern x)) in (Array.map f patterns)) + (Array.length nopatterns) (expr_aton nopatterns) + (ptr_of_expr body))) (** Create a Quantifier. *) - 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 ) = + let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : sort array ) ( names : symbol array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) = if (universal) then (mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id) else @@ -1842,7 +1904,7 @@ end = struct (** Create a Quantifier. *) - 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 ) = + let mk_quantifier ( ctx : context ) ( universal : bool ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) = if (universal) then mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id else @@ -1850,42 +1912,29 @@ end = struct end (** Functions to manipulate Array expressions *) -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 - - (**/**) +module Array_ = +struct + let create_expr ( ctx : context ) ( no : Z3native.ptr ) = - let e = (Expr.create ctx no) in + let e = (expr_of_ptr ctx no) in ArrayExpr(e) let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - let s = (Sort.create ctx no) in + let s = (sort_of_ptr 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 sgc ( x : array_sort ) = match (x) with ArraySort(Sort(s)) -> (z3obj_gc s) + let sgnc ( x : array_sort ) = match (x) with ArraySort(Sort(s)) -> (z3obj_gnc s) + let sgno ( x : array_sort ) = match (x) with ArraySort(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 egc ( x : array_expr ) = match (x) with ArrayExpr(Expr(e)) -> (z3obj_gc e) + let egnc ( x : array_expr ) = match (x) with ArrayExpr(Expr(e)) -> (z3obj_gnc e) + let egno ( x : array_expr ) = match (x) with ArrayExpr(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 : Sort.sort ) ( range : Sort.sort ) = + let mk_sort ( ctx : context ) ( domain : sort ) ( range : sort ) = create_sort ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range)) (** @@ -1893,62 +1942,62 @@ end = struct 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.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) + let is_store ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) (** Indicates whether the term is an array select. *) - let is_select ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SELECT) + let is_select ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SELECT) (** Indicates whether the term is a constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary. *) - let is_constant_array ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONST_ARRAY) + let is_constant_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONST_ARRAY) (** Indicates whether the term is a default array. For example default(const(v)) = v. The function is unary. *) - let is_default_array ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_DEFAULT) + let is_default_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_DEFAULT) (** Indicates whether the term is an array map. It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. *) - let is_array_map ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_MAP) + let is_array_map ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_MAP) (** Indicates whether the term is an as-array term. An as-array term is n array value that behaves as the function graph of the function passed as parameter. *) - let is_as_array ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) + let is_as_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) (** Indicates whether the term is of an array sort. *) - let is_array ( x : Expr.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) + let is_array ( x : expr ) = + (Z3native.is_app (nc_of_expr x) (ptr_of_expr x)) && + ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x)))) == ARRAY_SORT) (** The domain of the array sort. *) - let get_domain ( x : array_sort ) = Sort.create (sgc x) (Z3native.get_array_sort_domain (sgnc x) (sgno x)) + let get_domain ( x : array_sort ) = sort_of_ptr (sgc x) (Z3native.get_array_sort_domain (sgnc x) (sgno x)) (** The range of the array sort. *) - let get_range ( x : array_sort ) = Sort.create (sgc x) (Z3native.get_array_sort_range (sgnc x) (sgno x)) + let get_range ( x : array_sort ) = sort_of_ptr (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.sort ) ( range : Sort.sort ) = + let mk_const ( ctx : context ) ( name : symbol ) ( domain : sort ) ( range : 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.sort ) ( range : Sort.sort ) = + let mk_const_s ( ctx : context ) ( name : string ) ( domain : sort ) ( range : sort ) = mk_const ctx (Symbol.mk_string ctx name) domain range (** @@ -1963,8 +2012,8 @@ end = struct *) - 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)) + let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) = + expr_of_ptr ctx (Z3native.mk_select (context_gno ctx) (egno a) (ptr_of_expr i)) (** Array update. @@ -1982,8 +2031,8 @@ end = struct *) - 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)) + let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) ( v : expr ) = + expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (egno a) (ptr_of_expr i) (ptr_of_expr v)) (** Create a constant array. @@ -1993,8 +2042,8 @@ end = struct *) - 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)) + let mk_const_array ( ctx : context ) ( domain : sort ) ( v : expr ) = + expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (ptr_of_expr v)) (** Maps f on the argument arrays. @@ -2006,8 +2055,9 @@ end = struct *) - 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)) + let mk_map ( ctx : context ) ( f : func_decl ) ( args : array_expr array ) = + let m x = (ptr_of_expr (expr_of_array_expr x)) in + expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (Array.length args) (Array.map m args)) (** Access the array default value. @@ -2016,137 +2066,122 @@ end = 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) (egno arg)) + expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (egno arg)) end (** Functions to manipulate Set expressions *) -and Sets : -sig - type set_sort = SetSort of Sort.sort - -end = struct - type set_sort = SetSort of Sort.sort - +module Set = +struct let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - let s = (Sort.create ctx no) in + let s = (sort_of_ptr ctx no) in SetSort(s) (** Indicates whether the term is set union *) - let is_union ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) + let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) (** Indicates whether the term is set intersection *) - let is_intersect ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) + let is_intersect ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) (** Indicates whether the term is set difference *) - let is_difference ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) + let is_difference ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) (** Indicates whether the term is set complement *) - let is_complement ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) + let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) (** Indicates whether the term is set subset *) - let is_subset ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) + let is_subset ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) (** Create a set type. *) - let mk_sort ( ctx : context ) ( ty : Sort.sort ) = + let mk_sort ( ctx : context ) ( ty : 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.sort ) = - (Expr.create ctx (Z3native.mk_empty_set (context_gno ctx) (Sort.gno domain))) + let mk_empty ( ctx : context ) ( domain : sort ) = + (expr_of_ptr ctx (Z3native.mk_empty_set (context_gno ctx) (Sort.gno domain))) (** Create the full set. *) - let mk_full ( ctx : context ) ( domain : Sort.sort ) = - Expr.create ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain)) + let mk_full ( ctx : context ) ( domain : sort ) = + expr_of_ptr 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.expr ) ( element : Expr.expr ) = - Expr.create ctx (Z3native.mk_set_add (context_gno ctx) (Expr.gno set) (Expr.gno element)) + let mk_set_add ( ctx : context ) ( set : expr ) ( element : expr ) = + expr_of_ptr ctx (Z3native.mk_set_add (context_gno ctx) (ptr_of_expr set) (ptr_of_expr element)) (** Remove an element from a set. *) - 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)) + let mk_del ( ctx : context ) ( set : expr ) ( element : expr ) = + expr_of_ptr ctx (Z3native.mk_set_del (context_gno ctx) (ptr_of_expr set) (ptr_of_expr element)) (** Take the union of a list of sets. *) - 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)) + let mk_union ( ctx : context ) ( args : expr array ) = + expr_of_ptr 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.expr array ) = - Expr.create ctx (Z3native.mk_set_intersect (context_gno ctx) (Array.length args) (Expr.aton args)) + let mk_intersection ( ctx : context ) ( args : expr array ) = + expr_of_ptr 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.expr ) ( arg2 : Expr.expr ) = - Expr.create ctx (Z3native.mk_set_difference (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) + let mk_difference ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = + expr_of_ptr ctx (Z3native.mk_set_difference (context_gno ctx) (ptr_of_expr arg1) (ptr_of_expr arg2)) (** Take the complement of a set. *) - let mk_complement ( ctx : context ) ( arg : Expr.expr ) = - Expr.create ctx (Z3native.mk_set_complement (context_gno ctx) (Expr.gno arg)) + let mk_complement ( ctx : context ) ( arg : expr ) = + expr_of_ptr ctx (Z3native.mk_set_complement (context_gno ctx) (ptr_of_expr arg)) (** Check for set membership. *) - 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)) + let mk_membership ( ctx : context ) ( elem : expr ) ( set : expr ) = + expr_of_ptr ctx (Z3native.mk_set_member (context_gno ctx) (ptr_of_expr elem) (ptr_of_expr set)) (** Check for subsetness of sets. *) - 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)) + let mk_subset ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = + expr_of_ptr ctx (Z3native.mk_set_subset (context_gno ctx) (ptr_of_expr arg1) (ptr_of_expr arg2)) end (** Functions to manipulate Finite Domain expressions *) -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) - (**/**) - +module FiniteDomain = +struct + let gc ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort(s)) -> (z3obj_gc s) + let gnc ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort(s)) -> (z3obj_gnc s) + let gno ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort(s))-> (z3obj_gno s) + (** Create a new finite domain sort. *) - 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) + let mk_sort ( ctx : context ) ( name : symbol ) ( size : int ) = + let s = (sort_of_ptr ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size)) in + FiniteDomainSort(s) (** Create a new finite domain sort. @@ -2158,14 +2193,15 @@ end = struct (** Indicates whether the term is of an array 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) + let is_finite_domain ( x : expr ) = + let nc = (nc_of_expr x) in + (Z3native.is_app (nc_of_expr x) (ptr_of_expr x)) && + (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc (ptr_of_expr x))) == FINITE_DOMAIN_SORT) (** Indicates whether the term is a less than predicate over a finite domain. *) - let is_lt ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT) + let is_lt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT) (** The size of the finite domain sort. *) let get_size ( x : finite_domain_sort ) = @@ -2175,29 +2211,25 @@ end = struct end (** Functions to manipulate Relation expressions *) -and Relations : -sig - type relation_sort = RelationSort of Sort.sort - -end = struct - type relation_sort = RelationSort of Sort.sort - - (**/**) +module Relation = +struct + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - let s = (Sort.create ctx no) in + let s = (sort_of_ptr 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) - (**/**) + let gc ( x : relation_sort ) = match (x) with RelationSort(Sort(s)) -> (z3obj_gc s) + let gnc ( x : relation_sort ) = match (x) with RelationSort(Sort(s)) -> (z3obj_gnc s) + let gno ( x : relation_sort ) = match (x) with RelationSort(Sort(s))-> (z3obj_gno s) + (** Indicates whether the term is of a 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)) + let is_relation ( x : expr ) = + let nc = (nc_of_expr x) in + ((Z3native.is_app (nc_of_expr x) (ptr_of_expr x)) && + (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc (ptr_of_expr x))) == RELATION_SORT)) (** Indicates whether the term is an relation store @@ -2206,40 +2238,40 @@ end = 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.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_STORE) + let is_store ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_STORE) (** Indicates whether the term is an empty relation *) - let is_empty ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_EMPTY) + let is_empty ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_EMPTY) (** Indicates whether the term is a test for the emptiness of a relation *) - let is_is_empty ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_IS_EMPTY) + let is_is_empty ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_IS_EMPTY) (** Indicates whether the term is a relational join *) - let is_join ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_JOIN) + let is_join ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_JOIN) (** Indicates whether the term is the union or convex hull of two relations. The function takes two arguments. *) - let is_union ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_UNION) + let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_UNION) (** Indicates whether the term is the widening of two relations The function takes two arguments. *) - let is_widen ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_WIDEN) + let is_widen ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_WIDEN) (** Indicates whether the term is a projection of columns (provided as numbers in the parameters). The function takes one argument. *) - let is_project ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_PROJECT) + let is_project ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_PROJECT) (** Indicates whether the term is a relation filter @@ -2250,7 +2282,7 @@ end = struct corresponding to the columns of the relation. So the first column in the relation has index 0. *) - let is_filter ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_FILTER) + let is_filter ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_FILTER) (** Indicates whether the term is an intersection of a relation with the negation of another. @@ -2265,7 +2297,7 @@ end = 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.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_NEGATION_FILTER) + let is_negation_filter ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_NEGATION_FILTER) (** Indicates whether the term is the renaming of a column in a relation @@ -2273,12 +2305,12 @@ end = struct The function takes one argument. The parameters contain the renaming as a cycle. *) - let is_rename ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_RENAME) + let is_rename ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_RENAME) (** Indicates whether the term is the complement of a relation *) - let is_complement ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_COMPLEMENT) + let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_COMPLEMENT) (** Indicates whether the term is a relational select @@ -2287,7 +2319,7 @@ end = 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.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT) + let is_select ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT) (** Indicates whether the term is a relational clone (copy) @@ -2298,7 +2330,7 @@ end = struct for terms of kind to perform destructive updates to the first argument. *) - let is_clone ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_CLONE) + let is_clone ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_CLONE) (** The arity of the relation sort. *) let get_arity ( x : relation_sort ) = Z3native.get_relation_arity (gnc x) (gno x) @@ -2312,46 +2344,22 @@ end = struct end (** Functions to manipulate Datatype expressions *) -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) - +module Datatype = +struct let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - let s = (Sort.create ctx no) in + let s = (sort_of_ptr 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) - (**/**) + let sgc ( x : datatype_sort ) = match (x) with DatatypeSort(Sort(s)) -> (z3obj_gc s) + let sgnc ( x : datatype_sort ) = match (x) with DatatypeSort(Sort(s)) -> (z3obj_gnc s) + let sgno ( x : datatype_sort ) = match (x) with DatatypeSort(Sort(s))-> (z3obj_gno s) + (** Constructors *) - module Constructor : sig - type constructor - val create : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol array -> Sort.sort array -> int array -> constructor - val aton : constructor array -> Z3native.ptr array - end = 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 ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( sort_refs : int array ) = + module Constructor = + struct + + let create ( ctx : context ) ( name : symbol ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : 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") @@ -2362,8 +2370,8 @@ end = struct let ptr = (Z3native.mk_constructor (context_gno ctx) (Symbol.gno name) (Symbol.gno recognizer) n - (Symbol.aton field_names) - (Sort.aton sorts) + (let f x = (Symbol.gno x) in (Array.map f field_names)) + (let f x = (ptr_of_ast (ast_of_sort x)) in (Array.map f sorts)) sort_refs) in let no : z3_native_object = { m_ctx = ctx ; m_n_obj = null ; @@ -2379,21 +2387,17 @@ end = struct Gc.finalise f no ; Constructor(no, ex) - let aton ( a : constructor array ) = - let f (e : constructor) = match e with Constructor(no, ex) -> (z3obj_gno no)in - Array.map f a - 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) ; + ex.m_constructor_decl <- Some (func_decl_of_ptr (z3obj_gc no) a) ; + ex.m_tester_decl <- Some (func_decl_of_ptr (z3obj_gc no) b) ; + ex.m_accessor_decls <- Some (let f e = (func_decl_of_ptr (z3obj_gc no) e) in Array.map f c) ; () | _ -> () - (**/**) + let get_n ( x : constructor ) = match x with Constructor(no, ex) -> @@ -2433,24 +2437,18 @@ end = struct (** Constructor list objects *) module ConstructorList = struct - type constructor_list = z3_native_object - - (**/**) - let create ( ctx : context )( c : Constructor.constructor array ) = + + let create ( ctx : context ) ( c : 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))) ; + let f x = match x with Constructor(no,_) -> (z3obj_gno no) in + (z3obj_sno res ctx (Z3native.mk_constructor_list (context_gno ctx) (Array.length c) (Array.map f 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 *) @@ -2464,7 +2462,7 @@ end = 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.sort array ) ( sort_refs : int array) = + let mk_constructor ( ctx : context ) ( name : symbol ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array) = Constructor.create ctx name recognizer field_names sorts sort_refs @@ -2478,21 +2476,22 @@ end = 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.sort array ) ( sort_refs : int array ) = + let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array ) = mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs (** Create a new datatype sort. *) - 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 + let mk_sort ( ctx : context ) ( name : symbol ) ( constructors : constructor array) = + let f x = match x with Constructor(no,_) -> (z3obj_gno no) in + let (x,_) = (Z3native.mk_datatype (context_gno ctx) (Symbol.gno name) (Array.length constructors) (Array.map f constructors)) in create_sort ctx x (** Create a new datatype sort. *) - let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : Constructor.constructor array ) = + let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : constructor array ) = mk_sort ctx (Symbol.mk_string ctx name) constructors (** @@ -2500,16 +2499,17 @@ end = 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.constructor array array ) = + let mk_sorts ( ctx : context ) ( names : symbol array ) ( c : constructor array array ) = let n = (Array.length names) in - let f e = (ConstructorList.create ctx e) in + let f e = (ptr_of_ast (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) (ConstructorList.aton cla)) in + let f2 x = (Symbol.gno x) in + let (r, a) = (Z3native.mk_datatypes (context_gno ctx) n (Array.map f2 names) 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.constructor array array ) = + let mk_sorts_s ( ctx : context ) ( names : string array ) ( c : constructor array array ) = mk_sorts ctx ( let f e = (Symbol.mk_string ctx e) in @@ -2523,54 +2523,50 @@ end = struct (** The range of the array sort. *) let get_constructors ( x : datatype_sort ) = let n = (get_num_constructors x) in - let f i = FuncDecl.create (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) i) in + let f i = func_decl_of_ptr (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 n = (get_num_constructors x) in - let f i = FuncDecl.create (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) i) in + let f i = func_decl_of_ptr (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 n = (get_num_constructors x) in let f i = ( - let fd = FuncDecl.create (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) i) in + let fd = func_decl_of_ptr (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 + let g j = func_decl_of_ptr (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 *) -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) - - (**/**) +module Enumeration = +struct + let _constdecls = Hashtbl.create 0 + let _testerdecls = Hashtbl.create 0 + 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 s = (sort_of_ptr ctx no) in + let res = EnumSort(s) in + Hashtbl.add _constdecls res (let f e = func_decl_of_ptr ctx e in (Array.map f cdecls)) ; + Hashtbl.add _testerdecls res (let f e = func_decl_of_ptr ctx e in (Array.map f tdecls)) ; + res - 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) - (**/**) + let sgc ( x : enum_sort ) = match (x) with EnumSort(Sort(s)) -> (z3obj_gc s) + let sgnc ( x : enum_sort ) = match (x) with EnumSort(Sort(s)) -> (z3obj_gnc s) + let sgno ( x : enum_sort ) = match (x) with EnumSort(Sort(s))-> (z3obj_gno s) (** Create a new enumeration sort. *) - 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 + let mk_sort ( ctx : context ) ( name : symbol ) ( enum_names : symbol array ) = + let f x = Symbol.gno x in + let (a, b, c) = (Z3native.mk_enumeration_sort (context_gno ctx) (Symbol.gno name) (Array.length enum_names) (Array.map f enum_names)) in create_sort ctx a b c (** @@ -2580,45 +2576,40 @@ end = struct 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 ) = match x with EnumSort(_,ex) -> ex._constdecls + let get_const_decls ( x : enum_sort ) = Hashtbl.find _constdecls x (** The test predicates for the constants in the enumeration. *) - let get_tester_decls ( x : enum_sort ) = match x with EnumSort(_,ex) -> ex._testerdecls + let get_tester_decls ( x : enum_sort ) = Hashtbl.find _testerdecls x end (** Functions to manipulate List expressions *) -and Lists : -sig - type list_sort_data - type list_sort = ListSort of (Sort.sort * list_sort_data) - -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) - - (**/**) +module List_ = +struct + let _nildecls = Hashtbl.create 0 + let _is_nildecls = Hashtbl.create 0 + let _consdecls = Hashtbl.create 0 + let _is_consdecls = Hashtbl.create 0 + let _headdecls = Hashtbl.create 0 + let _taildecls = Hashtbl.create 0 + 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 s = (sort_of_ptr ctx no) in + let res = ListSort(s) in + Hashtbl.add _nildecls res (func_decl_of_ptr ctx nildecl) ; + Hashtbl.add _is_nildecls res (func_decl_of_ptr ctx is_nildecl) ; + Hashtbl.add _consdecls res (func_decl_of_ptr ctx consdecl) ; + Hashtbl.add _is_consdecls res (func_decl_of_ptr ctx is_consdecl) ; + Hashtbl.add _headdecls res (func_decl_of_ptr ctx headdecl) ; + Hashtbl.add _taildecls res (func_decl_of_ptr ctx taildecl) ; + res - 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) - (**/**) + let sgc ( x : list_sort ) = match (x) with ListSort(Sort(s)) -> (z3obj_gc s) + let sgnc ( x : list_sort ) = match (x) with ListSort(Sort(s)) -> (z3obj_gnc s) + let sgno ( x : list_sort ) = match (x) with ListSort(Sort(s))-> (z3obj_gno s) + (** Create a new list sort. *) - let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : Sort.sort ) = + let mk_sort ( ctx : context ) ( name : symbol ) ( elem_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 @@ -2627,53 +2618,51 @@ end = struct 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 ) = match x with ListSort(no, ex) -> ex._nildecl + let get_nil_decl ( x : list_sort ) = (Hashtbl.find _nildecls x) (** The declaration of the isNil function of this list sort. *) - let get_is_nil_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._is_nildecl + let get_is_nil_decl ( x : list_sort ) = (Hashtbl.find _is_nildecls x) (** The declaration of the cons function of this list sort. *) - let get_cons_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._consdecl + let get_cons_decl ( x : list_sort ) = (Hashtbl.find _consdecls x) (** The declaration of the isCons function of this list sort. *) - let get_is_cons_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._is_consdecl + let get_is_cons_decl ( x : list_sort ) = (Hashtbl.find _is_consdecls x) (** The declaration of the head function of this list sort. *) - let get_head_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._headdecl + let get_head_decl ( x : list_sort ) = (Hashtbl.find _headdecls x) (** The declaration of the tail function of this list sort. *) - let get_tail_decl ( x : list_sort ) = match x with ListSort(no, ex) -> ex._taildecl + let get_tail_decl ( x : list_sort ) = (Hashtbl.find _taildecls x) (** The empty list. *) - let nil ( x : list_sort ) = Expr.create_fa (sgc x) (get_nil_decl x) [||] + let nil ( x : list_sort ) = expr_of_func_app (sgc x) (get_nil_decl x) [||] end (** Functions to manipulate Tuple expressions *) -and Tuples : -sig - type tuple_sort = TupleSort of Sort.sort -end = struct - type tuple_sort = TupleSort of Sort.sort - - (**/**) +module Tuple = +struct + let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - let s = (Sort.create ctx no) in + let s = (sort_of_ptr 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) - (**/**) + let sgc ( x : tuple_sort ) = match (x) with TupleSort(Sort(s)) -> (z3obj_gc s) + let sgnc ( x : tuple_sort ) = match (x) with TupleSort(Sort(s)) -> (z3obj_gnc s) + let sgno ( x : tuple_sort ) = match (x) with TupleSort(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 + let mk_sort ( ctx : context ) ( name : symbol ) ( field_names : symbol array ) ( field_sorts : sort array ) = + let f x = Symbol.gno x in + let f2 x = ptr_of_ast (ast_of_sort x) in + let (r, a, b) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (Array.length field_names) (Array.map f field_names) (Array.map f2 field_sorts)) in (* CMW: leaks a,b? *) create_sort ctx r (** The constructor function of the tuple. *) let get_mk_decl ( x : tuple_sort ) = - FuncDecl.create (sgc x) (Z3native.get_tuple_sort_mk_decl (sgnc x) (sgno x)) + func_decl_of_ptr (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 (sgnc x) (sgno x) @@ -2681,131 +2670,37 @@ end = struct (** The field declarations. *) let get_field_decls ( x : tuple_sort ) = let n = get_num_fields x in - let f i = FuncDecl.create (sgc x) (Z3native.get_tuple_sort_field_decl (sgnc x) (sgno x) i) in + let f i = func_decl_of_ptr (sgc x) (Z3native.get_tuple_sort_field_decl (sgnc x) (sgno x) i) in Array.init n f end (** Functions to manipulate arithmetic expressions *) -and Arithmetic : -sig - type arith_sort = ArithSort of Sort.sort - type arith_expr = ArithExpr of Expr.expr - - val create_expr : context -> Z3native.ptr -> arith_expr - val create_sort : context -> Z3native.ptr -> arith_sort - val aton : arith_expr array -> Z3native.ptr array - - module Integers : sig - type int_sort = IntSort of arith_sort - type int_expr = IntExpr of arith_expr - type int_num = IntNum of int_expr - - val create_sort : context -> Z3native.ptr -> int_sort - val create_expr : context -> Z3native.ptr -> int_expr - val create_num : context -> Z3native.ptr -> int_num - end - - module Reals : sig - type real_sort = RealSort of arith_sort - type real_expr = RealExpr of arith_expr - type rat_num = RatNum of real_expr - - val create_sort : context -> Z3native.ptr -> real_sort - val create_expr : context -> Z3native.ptr -> real_expr - val create_num : context -> Z3native.ptr -> rat_num - end - - module AlgebraicNumbers : sig - type algebraic_num = AlgebraicNum of arith_expr - - val create_num : context -> Z3native.ptr -> algebraic_num - end - - val is_int : Expr.expr -> bool - val is_arithmetic_numeral : Expr.expr -> bool - val is_le : Expr.expr -> bool - val is_ge : Expr.expr -> bool - val is_lt : Expr.expr -> bool - val is_gt : Expr.expr -> bool - val is_add : Expr.expr -> bool - val is_sub : Expr.expr -> bool - val is_uminus : Expr.expr -> bool - val is_mul : Expr.expr -> bool - val is_div : Expr.expr -> bool - val is_idiv : Expr.expr -> bool - val is_remainder : Expr.expr -> bool - val is_modulus : Expr.expr -> bool - val is_inttoreal : Expr.expr -> bool - val is_real_to_int : Expr.expr -> bool - val is_real_is_int : Expr.expr -> bool - val is_real : Expr.expr -> bool - val is_int_numeral : Expr.expr -> bool - val is_rat_num : Expr.expr -> bool - val is_algebraic_number : Expr.expr -> bool - val mk_add : context -> arith_expr array -> Arithmetic.arith_expr - val mk_mul : context -> arith_expr array -> Arithmetic.arith_expr - val mk_sub : context -> arith_expr array -> Arithmetic.arith_expr - val mk_unary_minus : - context -> arith_expr -> Arithmetic.arith_expr - val mk_div : - context -> arith_expr -> arith_expr -> Arithmetic.arith_expr - val mk_power : - context -> arith_expr -> arith_expr -> Arithmetic.arith_expr - val mk_lt : - context -> arith_expr -> arith_expr -> Booleans.bool_expr - val mk_le : - context -> arith_expr -> arith_expr -> Booleans.bool_expr - val mk_gt : - context -> arith_expr -> arith_expr -> Booleans.bool_expr - val mk_ge : - context -> arith_expr -> arith_expr -> Booleans.bool_expr - -end = struct - type arith_sort = ArithSort of Sort.sort - type arith_expr = ArithExpr of Expr.expr - - (**/**) +module Arithmetic = +struct + let create_expr ( ctx : context ) ( no : Z3native.ptr ) = - ArithExpr(Expr.create ctx no) + arith_expr_of_expr (expr_of_ptr ctx no) let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - ArithSort(Sort.create ctx no) + arith_sort_of_sort (sort_of_ptr ctx no) - let sgc ( x : arith_sort ) = match (x) with ArithSort(Sort.Sort(s)) -> (z3obj_gc s) - let sgnc ( x : arith_sort ) = match (x) with ArithSort(Sort.Sort(s)) -> (z3obj_gnc s) - let sgno ( x : arith_sort ) = match (x) with ArithSort(Sort.Sort(s)) -> (z3obj_gno s) - let egc ( x : arith_expr ) = match (x) with ArithExpr(e) -> (Expr.gc e) - let egnc ( x : arith_expr ) = match (x) with ArithExpr(e) -> (Expr.gnc e) - let egno ( x : arith_expr ) = match (x) with ArithExpr(e) -> (Expr.gno e) + let sgc ( x : arith_sort ) = match (x) with ArithSort(Sort(s)) -> (z3obj_gc s) + let sgnc ( x : arith_sort ) = match (x) with ArithSort(Sort(s)) -> (z3obj_gnc s) + let sgno ( x : arith_sort ) = match (x) with ArithSort(Sort(s)) -> (z3obj_gno s) + let egc ( x : arith_expr ) = match (x) with ArithExpr(e) -> (c_of_expr e) + let egnc ( x : arith_expr ) = match (x) with ArithExpr(e) -> (nc_of_expr e) + let egno ( x : arith_expr ) = match (x) with ArithExpr(e) -> (ptr_of_expr e) - let aton (a : arith_expr array) = - let f (e : arith_expr) = (egno e) in - Array.map f a - (**/**) - - module rec Integers : - sig - type int_sort = IntSort of arith_sort - type int_expr = IntExpr of arith_expr - type int_num = IntNum of int_expr - - val create_sort : context -> Z3native.ptr -> int_sort - val create_expr : context -> Z3native.ptr -> int_expr - val create_num : context -> Z3native.ptr -> int_num - end = struct - type int_sort = IntSort of arith_sort - type int_expr = IntExpr of arith_expr - type int_num = IntNum of int_expr - - (**/**) + module Integer = + struct let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - IntSort(Arithmetic.create_sort ctx no) + int_sort_of_arith_sort (arith_sort_of_sort (sort_of_ptr ctx no)) let create_expr ( ctx : context ) ( no : Z3native.ptr ) = - IntExpr(Arithmetic.create_expr ctx no) + int_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx no)) let create_num ( ctx : context ) ( no : Z3native.ptr ) = - IntNum(create_expr ctx no) + int_num_of_int_expr (create_expr ctx no) let sgc ( x : int_sort ) = match (x) with IntSort(s) -> (sgc s) let sgnc ( x : int_sort ) = match (x) with IntSort(s) -> (sgnc s) @@ -2816,7 +2711,7 @@ end = struct let ngc ( x : int_num ) = match (x) with IntNum(e) -> (egc e) let ngnc ( x : int_num ) = match (x) with IntNum(e) -> (egnc e) let ngno ( x : int_num ) = match (x) with IntNum(e) -> (egno e) - (**/**) + (** Create a new integer sort. *) let mk_sort ( ctx : context ) = @@ -2834,7 +2729,7 @@ end = struct (** Creates an integer constant. *) - let mk_int_const ( ctx : context ) ( name : Symbol.symbol ) = + let mk_int_const ( ctx : context ) ( name : symbol ) = IntExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with IntSort(ArithSort(s)) -> s))) (** @@ -2848,14 +2743,14 @@ end = struct The arguments must have int type. *) let mk_mod ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = - create_expr ctx (Z3native.mk_mod (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (egno t1) (egno t2)) (** Create an expression representing t1 rem t2. The arguments must have int type. *) let mk_rem ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = - create_expr ctx (Z3native.mk_rem (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (egno t1) (egno t2)) (** Create an integer numeral. @@ -2883,7 +2778,7 @@ end = struct The argument must be of integer sort. *) let mk_int2real ( ctx : context ) ( t : int_expr ) = - Reals.create_expr ctx (Z3native.mk_int2real (context_gno ctx) (egno t)) + real_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_int2real (context_gno ctx) (egno t)))) (** Create an bit bit-vector from the integer argument . @@ -2896,32 +2791,19 @@ end = struct The argument must be of integer sort. *) let mk_int2bv ( ctx : context ) ( n : int ) ( t : int_expr ) = - BitVectors.create_expr ctx (Z3native.mk_int2bv (context_gno ctx) n (egno t)) + bitvec_expr_of_expr (expr_of_ptr ctx (Z3native.mk_int2bv (context_gno ctx) n (egno t))) end - and Reals : - sig - type real_sort = RealSort of arith_sort - type real_expr = RealExpr of arith_expr - type rat_num = RatNum of real_expr - - val create_sort : context -> Z3native.ptr -> real_sort - val create_expr : context -> Z3native.ptr -> real_expr - val create_num : context -> Z3native.ptr -> rat_num - end = struct - type real_sort = RealSort of arith_sort - type real_expr = RealExpr of arith_expr - type rat_num = RatNum of real_expr - - (**/**) + module Real = + struct let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - RealSort(Arithmetic.create_sort ctx no) + real_sort_of_arith_sort (arith_sort_of_sort (sort_of_ptr ctx no)) let create_expr ( ctx : context ) ( no : Z3native.ptr ) = - RealExpr(Arithmetic.create_expr ctx no) - + real_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx no)) + let create_num ( ctx : context ) ( no : Z3native.ptr ) = - RatNum(create_expr ctx no) + rat_num_of_real_expr (create_expr ctx no) let sgc ( x : real_sort ) = match (x) with RealSort(s) -> (sgc s) let sgnc ( x : real_sort ) = match (x) with RealSort(s) -> (sgnc s) @@ -2932,7 +2814,7 @@ end = struct let ngc ( x : rat_num ) = match (x) with RatNum(e) -> (egc e) let ngnc ( x : rat_num ) = match (x) with RatNum(e) -> (egnc e) let ngno ( x : rat_num ) = match (x) with RatNum(e) -> (egno e) - (**/**) + (** Create a real sort. *) let mk_sort ( ctx : context ) = @@ -2940,11 +2822,11 @@ end = struct (** The numerator of a rational numeral. *) let get_numerator ( x : rat_num ) = - Integers.create_num (ngc x) (Z3native.get_numerator (ngnc x) (ngno x)) + Integer.create_num (ngc x) (Z3native.get_numerator (ngnc x) (ngno x)) (** The denominator of a rational numeral. *) let get_denominator ( x : rat_num ) = - Integers.create_num (ngc x) (Z3native.get_denominator (ngnc x) (ngno x)) + Integer.create_num (ngc x) (Z3native.get_denominator (ngnc x) (ngno x)) (** Returns a string representation in decimal notation. The result has at most decimal places.*) @@ -2955,7 +2837,7 @@ end = struct let to_string ( x : rat_num ) = Z3native.get_numeral_string (ngnc x) (ngno x) (** Creates a real constant. *) - let mk_real_const ( ctx : context ) ( name : Symbol.symbol ) = + let mk_real_const ( ctx : context ) ( name : symbol ) = RealExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with RealSort(ArithSort(s)) -> s))) (** Creates a real constant. *) @@ -2995,7 +2877,7 @@ end = struct (** Creates an expression that checks whether a real number is an integer. *) let mk_is_integer ( ctx : context ) ( t : real_expr ) = - Booleans.create_expr ctx (Z3native.mk_is_int (context_gno ctx) (egno t)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (egno t))) (** Coerce a real to an integer. @@ -3005,25 +2887,18 @@ end = struct The argument must be of real sort. *) let mk_real2int ( ctx : context ) ( t : real_expr ) = - Integers.create_expr ctx (Z3native.mk_real2int (context_gno ctx) (egno t)) + int_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (egno t)))) end - and AlgebraicNumbers : - sig - type algebraic_num = AlgebraicNum of arith_expr - - val create_num : context -> Z3native.ptr -> algebraic_num - end = struct - type algebraic_num = AlgebraicNum of arith_expr - - (**/**) + module AlgebraicNumber = + struct let create_num ( ctx : context ) ( no : Z3native.ptr ) = - AlgebraicNum(Arithmetic.create_expr ctx no) + algebraic_num_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx no)) let ngc ( x : algebraic_num ) = match (x) with AlgebraicNum(e) -> (egc e) let ngnc ( x : algebraic_num ) = match (x) with AlgebraicNum(e) -> (egnc e) let ngno ( x : algebraic_num ) = match (x) with AlgebraicNum(e) -> (egno e) - (**/**) + (** Return a upper bound for a given real algebraic number. @@ -3033,7 +2908,7 @@ end = struct @return A numeral Expr of sort Real *) let to_upper ( x : algebraic_num ) ( precision : int ) = - Reals.create_num (ngc x) (Z3native.get_algebraic_number_upper (ngnc x) (ngno x) precision) + Real.create_num (ngc x) (Z3native.get_algebraic_number_upper (ngnc x) (ngno x) precision) (** Return a lower bound for the given real algebraic number. @@ -3043,7 +2918,7 @@ end = struct @return A numeral Expr of sort Real *) let to_lower ( x : algebraic_num ) precision = - Reals.create_num (ngc x) (Z3native.get_algebraic_number_lower (ngnc x) (ngno x) precision) + Real.create_num (ngc x) (Z3native.get_algebraic_number_lower (ngnc x) (ngno x) precision) (** Returns a string representation in decimal notation. The result has at most decimal places.*) @@ -3057,207 +2932,197 @@ end = struct (** Indicates whether the term is of integer sort. *) - let is_int ( x : Expr.expr ) = - (Z3native.is_numeral_ast (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)))) == INT_SORT) + let is_int ( x : expr ) = + (Z3native.is_numeral_ast (nc_of_expr x) (nc_of_expr x)) && + ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (nc_of_expr x)))) == INT_SORT) (** Indicates whether the term is an arithmetic numeral. *) - let is_arithmetic_numeral ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM) + let is_arithmetic_numeral ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM) (** Indicates whether the term is a less-than-or-equal *) - let is_le ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE) + let is_le ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE) (** Indicates whether the term is a greater-than-or-equal *) - let is_ge ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE) + let is_ge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE) (** Indicates whether the term is a less-than *) - let is_lt ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LT) + let is_lt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LT) (** Indicates whether the term is a greater-than *) - let is_gt ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GT) + let is_gt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GT) (** Indicates whether the term is addition (binary) *) - let is_add ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ADD) + let is_add ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ADD) (** Indicates whether the term is subtraction (binary) *) - let is_sub ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SUB) + let is_sub ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SUB) (** Indicates whether the term is a unary minus *) - let is_uminus ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UMINUS) + let is_uminus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UMINUS) (** Indicates whether the term is multiplication (binary) *) - let is_mul ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MUL) + let is_mul ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MUL) (** Indicates whether the term is division (binary) *) - let is_div ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_DIV) + let is_div ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_DIV) (** Indicates whether the term is integer division (binary) *) - let is_idiv ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IDIV) + let is_idiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IDIV) (** Indicates whether the term is remainder (binary) *) - let is_remainder ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REM) + let is_remainder ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REM) (** Indicates whether the term is modulus (binary) *) - let is_modulus ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD) + let is_modulus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD) (** Indicates whether the term is a coercion of integer to real (unary) *) - let is_inttoreal ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL) + let is_inttoreal ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL) (** Indicates whether the term is a coercion of real to integer (unary) *) - let is_real_to_int ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT) + let is_real_to_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT) (** Indicates whether the term is a check that tests whether a real is integral (unary) *) - let is_real_is_int ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT) + let is_real_is_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT) (** Indicates whether the term is of sort real. *) - let is_real ( x : Expr.expr ) = - ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == REAL_SORT) + let is_real ( x : expr ) = + ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (nc_of_expr x)))) == REAL_SORT) (** Indicates whether the term is an integer numeral. *) - let is_int_numeral ( x : Expr.expr ) = (Expr.is_numeral x) && (is_int x) + let is_int_numeral ( x : expr ) = (Expr.is_numeral x) && (is_int x) (** Indicates whether the term is a real numeral. *) - let is_rat_num ( x : Expr.expr ) = (Expr.is_numeral x) && (is_real x) + let is_rat_num ( x : expr ) = (Expr.is_numeral x) && (is_real x) (** Indicates whether the term is an algebraic number *) - let is_algebraic_number ( x : Expr.expr ) = Z3native.is_algebraic_number (Expr.gnc x) (Expr.gno x) + let is_algebraic_number ( x : expr ) = Z3native.is_algebraic_number (nc_of_expr x) (nc_of_expr x) (** Create an expression representing t[0] + t[1] + .... *) let mk_add ( ctx : context ) ( t : arith_expr array ) = - Arithmetic.create_expr ctx (Z3native.mk_add (context_gno ctx) (Array.length t) (Arithmetic.aton t)) + let f x = (ptr_of_expr (expr_of_arith_expr x)) in + arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_add (context_gno ctx) (Array.length t) (Array.map f t))) (** Create an expression representing t[0] * t[1] * .... *) let mk_mul ( ctx : context ) ( t : arith_expr array ) = - Arithmetic.create_expr ctx (Z3native.mk_mul (context_gno ctx) (Array.length t) (Arithmetic.aton t)) + let f x = (ptr_of_expr (expr_of_arith_expr x)) in + arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_mul (context_gno ctx) (Array.length t) (Array.map f t))) (** Create an expression representing t[0] - t[1] - .... *) let mk_sub ( ctx : context ) ( t : arith_expr array ) = - Arithmetic.create_expr ctx (Z3native.mk_sub (context_gno ctx) (Array.length t) (Arithmetic.aton t)) + let f x = (ptr_of_expr (expr_of_arith_expr x)) in + arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_sub (context_gno ctx) (Array.length t) (Array.map f t))) (** Create an expression representing -t. *) let mk_unary_minus ( ctx : context ) ( t : arith_expr ) = - Arithmetic.create_expr ctx (Z3native.mk_unary_minus (context_gno ctx) (egno t)) + arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_unary_minus (context_gno ctx) (egno t))) (** Create an expression representing t1 / t2. *) let mk_div ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = - Arithmetic.create_expr ctx (Z3native.mk_div (context_gno ctx) (egno t1) (egno t2)) + arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_div (context_gno ctx) (egno t1) (egno t2))) (** Create an expression representing t1 ^ t2. *) let mk_power ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = - Arithmetic.create_expr ctx (Z3native.mk_power (context_gno ctx) (egno t1) (egno t2)) + arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_power (context_gno ctx) (egno t1) (egno t2))) (** Create an expression representing t1 < t2 *) let mk_lt ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = - Booleans.create_expr ctx (Z3native.mk_lt (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_lt (context_gno ctx) (egno t1) (egno t2))) (** Create an expression representing t1 <= t2 *) let mk_le ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = - Booleans.create_expr ctx (Z3native.mk_le (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_le (context_gno ctx) (egno t1) (egno t2))) (** Create an expression representing t1 > t2 *) let mk_gt ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = - Booleans.create_expr ctx (Z3native.mk_gt (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_gt (context_gno ctx) (egno t1) (egno t2))) (** Create an expression representing t1 >= t2 *) let mk_ge ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = - Booleans.create_expr ctx (Z3native.mk_ge (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_ge (context_gno ctx) (egno t1) (egno t2))) end (** Functions to manipulate bit-vector expressions *) -and BitVectors : -sig - type bitvec_sort = BitVecSort of Sort.sort - type bitvec_expr = BitVecExpr of Expr.expr - type bitvec_num = BitVecNum of bitvec_expr - - val create_sort : context -> Z3native.ptr -> bitvec_sort - val create_expr : context -> Z3native.ptr -> bitvec_expr - val create_num : context -> Z3native.ptr -> bitvec_num -end = struct - type bitvec_sort = BitVecSort of Sort.sort - type bitvec_expr = BitVecExpr of Expr.expr - type bitvec_num = BitVecNum of bitvec_expr - - (**/**) +module BitVector = +struct let create_sort ( ctx : context ) ( no : Z3native.ptr ) = - BitVecSort(Sort.create ctx no) + bitvec_sort_of_sort (sort_of_ptr ctx no) let create_expr ( ctx : context ) ( no : Z3native.ptr ) = - BitVecExpr(Expr.create ctx no) + bitvec_expr_of_expr (expr_of_ptr ctx no) let create_num ( ctx : context ) ( no : Z3native.ptr ) = - BitVecNum(create_expr ctx no) + bitvec_num_of_bitvec_expr (create_expr ctx no) let sgc ( x : bitvec_sort ) = match (x) with BitVecSort(s) -> (Sort.gc s) let sgnc ( x : bitvec_sort ) = match (x) with BitVecSort(s) -> (Sort.gnc s) let sgno ( x : bitvec_sort ) = match (x) with BitVecSort(s) -> (Sort.gno s) - let egc ( x : bitvec_expr ) = match (x) with BitVecExpr(e) -> (Expr.gc e) - let egnc ( x : bitvec_expr ) = match (x) with BitVecExpr(e) -> (Expr.gnc e) - let egno ( x : bitvec_expr ) = match (x) with BitVecExpr(e) -> (Expr.gno e) + let egc ( x : bitvec_expr ) = match (x) with BitVecExpr(e) -> (c_of_expr e) + let egnc ( x : bitvec_expr ) = match (x) with BitVecExpr(e) -> (nc_of_expr e) + let egno ( x : bitvec_expr ) = match (x) with BitVecExpr(e) -> (ptr_of_expr e) let ngc ( x : bitvec_num ) = match (x) with BitVecNum(e) -> (egc e) let ngnc ( x : bitvec_num ) = match (x) with BitVecNum(e) -> (egnc e) let ngno ( x : bitvec_num ) = match (x) with BitVecNum(e) -> (egno e) - (**/**) + (** Create a new bit-vector sort. @@ -3268,272 +3133,272 @@ end = struct (** Indicates whether the terms is of bit-vector sort. *) - let is_bv ( x : Expr.expr ) = - ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == BV_SORT) + let is_bv ( x : expr ) = + ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x)))) == BV_SORT) (** Indicates whether the term is a bit-vector numeral *) - let is_bv_numeral ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNUM) + let is_bv_numeral ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNUM) (** Indicates whether the term is a one-bit bit-vector with value one *) - let is_bv_bit1 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT1) + let is_bv_bit1 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT1) (** Indicates whether the term is a one-bit bit-vector with value zero *) - let is_bv_bit0 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT0) + let is_bv_bit0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT0) (** Indicates whether the term is a bit-vector unary minus *) - let is_bv_uminus ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNEG) + let is_bv_uminus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNEG) (** Indicates whether the term is a bit-vector addition (binary) *) - let is_bv_add ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BADD) + let is_bv_add ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BADD) (** Indicates whether the term is a bit-vector subtraction (binary) *) - let is_bv_sub ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSUB) + let is_bv_sub ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSUB) (** Indicates whether the term is a bit-vector multiplication (binary) *) - let is_bv_mul ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BMUL) + let is_bv_mul ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BMUL) (** Indicates whether the term is a bit-vector signed division (binary) *) - let is_bv_sdiv ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV) + let is_bv_sdiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV) (** Indicates whether the term is a bit-vector unsigned division (binary) *) - let is_bv_udiv ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV) + let is_bv_udiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV) (** Indicates whether the term is a bit-vector signed remainder (binary) *) - let is_bv_SRem ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM) + let is_bv_SRem ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM) (** Indicates whether the term is a bit-vector unsigned remainder (binary) *) - let is_bv_urem ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM) + let is_bv_urem ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM) (** Indicates whether the term is a bit-vector signed modulus *) - let is_bv_smod ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD) + let is_bv_smod ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD) (** Indicates whether the term is a bit-vector signed division by zero *) - let is_bv_sdiv0 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV0) + let is_bv_sdiv0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV0) (** Indicates whether the term is a bit-vector unsigned division by zero *) - let is_bv_udiv0 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV0) + let is_bv_udiv0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV0) (** Indicates whether the term is a bit-vector signed remainder by zero *) - let is_bv_srem0 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM0) + let is_bv_srem0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM0) (** Indicates whether the term is a bit-vector unsigned remainder by zero *) - let is_bv_urem0 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM0) + let is_bv_urem0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM0) (** Indicates whether the term is a bit-vector signed modulus by zero *) - let is_bv_smod0 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD0) + let is_bv_smod0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD0) (** Indicates whether the term is an unsigned bit-vector less-than-or-equal *) - let is_bv_ule ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULEQ) + let is_bv_ule ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULEQ) (** Indicates whether the term is a signed bit-vector less-than-or-equal *) - let is_bv_sle ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLEQ) + let is_bv_sle ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLEQ) (** Indicates whether the term is an unsigned bit-vector greater-than-or-equal *) - let is_bv_uge ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGEQ) + let is_bv_uge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGEQ) (** Indicates whether the term is a signed bit-vector greater-than-or-equal *) - let is_bv_sge ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGEQ) + let is_bv_sge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGEQ) (** Indicates whether the term is an unsigned bit-vector less-than *) - let is_bv_ult ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULT) + let is_bv_ult ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULT) (** Indicates whether the term is a signed bit-vector less-than *) - let is_bv_slt ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLT) + let is_bv_slt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLT) (** Indicates whether the term is an unsigned bit-vector greater-than *) - let is_bv_ugt ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGT) + let is_bv_ugt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGT) (** Indicates whether the term is a signed bit-vector greater-than *) - let is_bv_sgt ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGT) + let is_bv_sgt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGT) (** Indicates whether the term is a bit-wise AND *) - let is_bv_and ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BAND) + let is_bv_and ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BAND) (** Indicates whether the term is a bit-wise OR *) - let is_bv_or ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BOR) + let is_bv_or ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BOR) (** Indicates whether the term is a bit-wise NOT *) - let is_bv_not ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOT) + let is_bv_not ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOT) (** Indicates whether the term is a bit-wise XOR *) - let is_bv_xor ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXOR) + let is_bv_xor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXOR) (** Indicates whether the term is a bit-wise NAND *) - let is_bv_nand ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNAND) + let is_bv_nand ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNAND) (** Indicates whether the term is a bit-wise NOR *) - let is_bv_nor ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOR) + let is_bv_nor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOR) (** Indicates whether the term is a bit-wise XNOR *) - let is_bv_xnor ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXNOR) + let is_bv_xnor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXNOR) (** Indicates whether the term is a bit-vector concatenation (binary) *) - let is_bv_concat ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONCAT) + let is_bv_concat ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONCAT) (** Indicates whether the term is a bit-vector sign extension *) - let is_bv_signextension ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SIGN_EXT) + let is_bv_signextension ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SIGN_EXT) (** Indicates whether the term is a bit-vector zero extension *) - let is_bv_zeroextension ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ZERO_EXT) + let is_bv_zeroextension ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ZERO_EXT) (** Indicates whether the term is a bit-vector extraction *) - let is_bv_extract ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXTRACT) + let is_bv_extract ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXTRACT) (** Indicates whether the term is a bit-vector repetition *) - let is_bv_repeat ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REPEAT) + let is_bv_repeat ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REPEAT) (** Indicates whether the term is a bit-vector reduce OR *) - let is_bv_reduceor ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDOR) + let is_bv_reduceor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDOR) (** Indicates whether the term is a bit-vector reduce AND *) - let is_bv_reduceand ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDAND) + let is_bv_reduceand ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDAND) (** Indicates whether the term is a bit-vector comparison *) - let is_bv_comp ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BCOMP) + let is_bv_comp ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BCOMP) (** Indicates whether the term is a bit-vector shift left *) - let is_bv_shiftleft ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSHL) + let is_bv_shiftleft ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSHL) (** Indicates whether the term is a bit-vector logical shift right *) - let is_bv_shiftrightlogical ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BLSHR) + let is_bv_shiftrightlogical ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BLSHR) (** Indicates whether the term is a bit-vector arithmetic shift left *) - let is_bv_shiftrightarithmetic ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BASHR) + let is_bv_shiftrightarithmetic ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BASHR) (** Indicates whether the term is a bit-vector rotate left *) - let is_bv_rotateleft ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_LEFT) + let is_bv_rotateleft ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_LEFT) (** Indicates whether the term is a bit-vector rotate right *) - let is_bv_rotateright ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_RIGHT) + let is_bv_rotateright ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_RIGHT) (** Indicates whether the term is a bit-vector rotate left (extended) Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. *) - let is_bv_rotateleftextended ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_LEFT) + let is_bv_rotateleftextended ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_LEFT) (** Indicates whether the term is a bit-vector rotate right (extended) Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. *) - let is_bv_rotaterightextended ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) + let is_bv_rotaterightextended ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) (** Indicates whether the term is a coercion from integer to bit-vector This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function. *) - let is_int_to_bv ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV) + let is_int_to_bv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV) (** Indicates whether the term is a coercion from bit-vector to integer This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function. *) - let is_bv_to_int ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT) + let is_bv_to_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT) (** Indicates whether the term is a bit-vector carry Compute the carry bit in a full-adder. The meaning is given by the equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) *) - let is_bv_carry ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY) + let is_bv_carry ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY) (** Indicates whether the term is a bit-vector ternary XOR The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) *) - let is_bv_xor3 ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3) + let is_bv_xor3 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3) (** The size of a bit-vector sort. *) let get_size (x : bitvec_sort ) = Z3native.get_bv_sort_size (sgnc x) (sgno x) @@ -3550,7 +3415,7 @@ end = struct (** Creates a bit-vector constant. *) - let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) = + let mk_const ( ctx : context ) ( name : symbol ) ( size : int ) = BitVecExpr(Expr.mk_const ctx name (match (mk_sort ctx size) with BitVecSort(s) -> s)) (** @@ -3564,91 +3429,91 @@ end = struct The argument must have a bit-vector sort. *) let mk_not ( ctx : context ) ( t : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvnot (context_gno ctx) (egno t)) + expr_of_ptr ctx (Z3native.mk_bvnot (context_gno ctx) (egno t)) (** 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) = - create_expr ctx (Z3native.mk_bvredand (context_gno ctx) (egno t)) + expr_of_ptr ctx (Z3native.mk_bvredand (context_gno ctx) (egno t)) (** 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) = - create_expr ctx (Z3native.mk_bvredor (context_gno ctx) (egno t)) + expr_of_ptr ctx (Z3native.mk_bvredor (context_gno ctx) (egno t)) (** Bitwise conjunction. The arguments must have a bit-vector sort. *) let mk_and ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvand (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvand (context_gno ctx) (egno t1) (egno t2)) (** Bitwise disjunction. The arguments must have a bit-vector sort. *) let mk_or ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvor (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvor (context_gno ctx) (egno t1) (egno t2)) (** Bitwise XOR. The arguments must have a bit-vector sort. *) let mk_xor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvxor (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvxor (context_gno ctx) (egno t1) (egno t2)) (** Bitwise NAND. The arguments must have a bit-vector sort. *) let mk_nand ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvnand (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvnand (context_gno ctx) (egno t1) (egno t2)) (** Bitwise NOR. The arguments must have a bit-vector sort. *) let mk_nor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvnor (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvnor (context_gno ctx) (egno t1) (egno t2)) (** Bitwise XNOR. The arguments must have a bit-vector sort. *) let mk_xnor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvxnor (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvxnor (context_gno ctx) (egno t1) (egno t2)) (** Standard two's complement unary minus. The arguments must have a bit-vector sort. *) let mk_neg ( ctx : context ) ( t : bitvec_expr) = - create_expr ctx (Z3native.mk_bvneg (context_gno ctx) (egno t)) + expr_of_ptr ctx (Z3native.mk_bvneg (context_gno ctx) (egno t)) (** Two's complement addition. The arguments must have the same bit-vector sort. *) let mk_add ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvadd (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvadd (context_gno ctx) (egno t1) (egno t2)) (** Two's complement subtraction. The arguments must have the same bit-vector sort. *) let mk_sub ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvsub (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvsub (context_gno ctx) (egno t1) (egno t2)) (** Two's complement multiplication. The arguments must have the same bit-vector sort. *) let mk_mul ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvmul (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvmul (context_gno ctx) (egno t1) (egno t2)) (** Unsigned division. @@ -3660,7 +3525,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_udiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvudiv (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvudiv (context_gno ctx) (egno t1) (egno t2)) (** Signed division. @@ -3675,7 +3540,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_sdiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvsdiv (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvsdiv (context_gno ctx) (egno t1) (egno t2)) (** Unsigned remainder. @@ -3685,7 +3550,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_urem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvurem (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvurem (context_gno ctx) (egno t1) (egno t2)) (** Signed remainder. @@ -3697,7 +3562,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_srem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvsrem (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvsrem (context_gno ctx) (egno t1) (egno t2)) (** Two's complement signed remainder (sign follows divisor). @@ -3706,7 +3571,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_smod ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvsmod (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvsmod (context_gno ctx) (egno t1) (egno t2)) (** Unsigned less-than @@ -3714,7 +3579,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_ult ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvult (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvult (context_gno ctx) (egno t1) (egno t2))) (** Two's complement signed less-than @@ -3722,7 +3587,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_slt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvslt (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvslt (context_gno ctx) (egno t1) (egno t2))) (** Unsigned less-than or equal to. @@ -3730,7 +3595,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_ule ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvule (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvule (context_gno ctx) (egno t1) (egno t2))) (** Two's complement signed less-than or equal to. @@ -3738,7 +3603,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_sle ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvsle (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsle (context_gno ctx) (egno t1) (egno t2))) (** Unsigned greater than or equal to. @@ -3746,7 +3611,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_uge ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvuge (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvuge (context_gno ctx) (egno t1) (egno t2))) (** Two's complement signed greater than or equal to. @@ -3754,7 +3619,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_sge ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvsge (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (egno t1) (egno t2))) (** Unsigned greater-than. @@ -3762,7 +3627,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_ugt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvugt (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (egno t1) (egno t2))) (** Two's complement signed greater-than. @@ -3770,7 +3635,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_sgt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvsgt (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (egno t1) (egno t2))) (** Bit-vector concatenation. @@ -3781,7 +3646,7 @@ end = struct is the size of t1 (t2). *) let mk_concat ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_concat (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (egno t1) (egno t2)) (** Bit-vector extraction. @@ -3792,7 +3657,7 @@ end = struct The argument must have a bit-vector sort. *) let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : bitvec_expr ) = - create_expr ctx (Z3native.mk_extract (context_gno ctx) high low (egno t)) + expr_of_ptr ctx (Z3native.mk_extract (context_gno ctx) high low (egno t)) (** Bit-vector sign extension. @@ -3802,7 +3667,7 @@ end = struct The argument must have a bit-vector sort. *) let mk_sign_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = - create_expr ctx (Z3native.mk_sign_ext (context_gno ctx) i (egno t)) + expr_of_ptr ctx (Z3native.mk_sign_ext (context_gno ctx) i (egno t)) (** Bit-vector zero extension. @@ -3813,7 +3678,7 @@ end = struct The argument must have a bit-vector sort. *) let mk_zero_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = - create_expr ctx (Z3native.mk_zero_ext (context_gno ctx) i (egno t)) + expr_of_ptr ctx (Z3native.mk_zero_ext (context_gno ctx) i (egno t)) (** Bit-vector repetition. @@ -3821,7 +3686,7 @@ end = struct The argument must have a bit-vector sort. *) let mk_repeat ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = - create_expr ctx (Z3native.mk_repeat (context_gno ctx) i (egno t)) + expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (egno t)) (** Shift left. @@ -3836,7 +3701,7 @@ end = struct The arguments must have a bit-vector sort. *) let mk_shl ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvshl (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (egno t1) (egno t2)) (** @@ -3851,7 +3716,7 @@ end = struct The arguments must have a bit-vector sort. *) let mk_lshr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvlshr (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (egno t1) (egno t2)) (** Arithmetic shift right @@ -3867,7 +3732,7 @@ end = struct The arguments must have a bit-vector sort. *) let mk_ashr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_bvashr (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_bvashr (context_gno ctx) (egno t1) (egno t2)) (** Rotate Left. @@ -3876,7 +3741,7 @@ end = struct The argument must have a bit-vector sort. *) let mk_rotate_left ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = - create_expr ctx (Z3native.mk_rotate_left (context_gno ctx) i (egno t)) + expr_of_ptr ctx (Z3native.mk_rotate_left (context_gno ctx) i (egno t)) (** Rotate Right. @@ -3885,7 +3750,7 @@ end = struct The argument must have a bit-vector sort. *) let mk_rotate_right ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = - create_expr ctx (Z3native.mk_rotate_right (context_gno ctx) i (egno t)) + expr_of_ptr ctx (Z3native.mk_rotate_right (context_gno ctx) i (egno t)) (** Rotate Left. @@ -3894,7 +3759,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_rotate_left ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (egno t1) (egno t2)) (** Rotate Right. @@ -3904,7 +3769,7 @@ end = struct The arguments must have the same bit-vector sort. *) let mk_rotate_right ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - create_expr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (egno t1) (egno t2)) + expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (egno t1) (egno t2)) (** Create an integer from the bit-vector argument . @@ -3922,7 +3787,7 @@ end = struct The argument must be of bit-vector sort. *) let mk_bv2int ( ctx : context ) ( t : bitvec_expr ) ( signed : bool ) = - Arithmetic.Integers.create_expr ctx (Z3native.mk_bv2int (context_gno ctx) (egno t) signed) + Arithmetic.Integer.create_expr ctx (Z3native.mk_bv2int (context_gno ctx) (egno t) signed) (** Create a predicate that checks that the bit-wise addition does not overflow. @@ -3930,7 +3795,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_add_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = - Booleans.create_expr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (egno t1) (egno t2) signed) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (egno t1) (egno t2) signed)) (** Create a predicate that checks that the bit-wise addition does not underflow. @@ -3938,7 +3803,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_add_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (egno t1) (egno t2))) (** Create a predicate that checks that the bit-wise subtraction does not overflow. @@ -3946,7 +3811,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_sub_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (egno t1) (egno t2))) (** Create a predicate that checks that the bit-wise subtraction does not underflow. @@ -3954,7 +3819,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_sub_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = - Booleans.create_expr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (egno t1) (egno t2) signed) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (egno t1) (egno t2) signed)) (** Create a predicate that checks that the bit-wise signed division does not overflow. @@ -3962,7 +3827,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_sdiv_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) (egno t1) (egno t2))) (** Create a predicate that checks that the bit-wise negation does not overflow. @@ -3970,7 +3835,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_neg_no_overflow ( ctx : context ) ( t : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (egno t)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (egno t))) (** Create a predicate that checks that the bit-wise multiplication does not overflow. @@ -3978,7 +3843,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_mul_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = - Booleans.create_expr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (egno t1) (egno t2) signed) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (egno t1) (egno t2) signed)) (** Create a predicate that checks that the bit-wise multiplication does not underflow. @@ -3986,7 +3851,7 @@ end = struct The arguments must be of bit-vector sort. *) let mk_mul_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = - Booleans.create_expr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (egno t1) (egno t2)) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (egno t1) (egno t2))) (** Create a bit-vector numeral. @@ -3994,28 +3859,27 @@ end = struct @param v A string representing the value in decimal notation. @param size the size of the bit-vector *) - let mk_numeral ( ctx : context ) ( ctx : context ) ( v : string ) ( size : int) = + let mk_numeral ( ctx : context ) ( v : string ) ( size : int) = create_num ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx size))) end (** Functions to manipulate proof expressions *) -and Proofs : -sig -end = struct +module Proof = +struct (** Indicates whether the term is a Proof for the expression 'true'. *) - let is_true ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE) + let is_true ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE) (** Indicates whether the term is a proof for a fact asserted by the user. *) - let is_asserted ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ASSERTED) + let is_asserted ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ASSERTED) (** Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. *) - let is_goal ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_GOAL) + let is_goal ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_GOAL) (** Indicates whether the term is proof via modus ponens @@ -4026,7 +3890,7 @@ end = struct [mp T1 T2]: q The second antecedents may also be a proof for (iff p q). *) - let is_modus_ponens ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS) + let is_modus_ponens ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS) (** Indicates whether the term is a proof for (R t t), where R is a reflexive relation. @@ -4035,7 +3899,7 @@ end = struct equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'. *) - let is_reflexivity ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REFLEXIVITY) + let is_reflexivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REFLEXIVITY) (** Indicates whether the term is proof by symmetricity of a relation @@ -4045,7 +3909,7 @@ end = struct [symmetry T1]: (R s t) T1 is the antecedent of this proof object. *) - let is_symmetry ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SYMMETRY) + let is_symmetry ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SYMMETRY) (** Indicates whether the term is a proof by transitivity of a relation @@ -4056,7 +3920,7 @@ end = struct T2: (R s u) [trans T1 T2]: (R t u) *) - let is_transitivity ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY) + let is_transitivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY) (** Indicates whether the term is a proof by condensed transitivity of a relation @@ -4076,7 +3940,7 @@ end = struct if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b. *) - let is_Transitivity_star ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY_STAR) + let is_Transitivity_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY_STAR) (** @@ -4089,7 +3953,7 @@ end = struct Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are supressed to save space. *) - let is_monotonicity ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MONOTONICITY) + let is_monotonicity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MONOTONICITY) (** Indicates whether the term is a quant-intro proof @@ -4098,7 +3962,7 @@ end = struct T1: (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) *) - let is_quant_intro ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INTRO) + let is_quant_intro ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INTRO) (** Indicates whether the term is a distributivity proof object. @@ -4115,7 +3979,7 @@ end = struct Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and. *) - let is_distributivity ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DISTRIBUTIVITY) + let is_distributivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DISTRIBUTIVITY) (** Indicates whether the term is a proof by elimination of AND @@ -4124,7 +3988,7 @@ end = struct T1: (and l_1 ... l_n) [and-elim T1]: l_i *) - let is_and_elimination ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_AND_ELIM) + let is_and_elimination ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_AND_ELIM) (** Indicates whether the term is a proof by eliminiation of not-or @@ -4133,7 +3997,7 @@ end = struct T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) *) - let is_or_elimination ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NOT_OR_ELIM) + let is_or_elimination ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NOT_OR_ELIM) (** Indicates whether the term is a proof by rewriting @@ -4147,11 +4011,11 @@ end = struct Remark: if f is bool, then = is iff. Examples: - (= (+ ( x : Expr.expr ) 0) x) - (= (+ ( x : Expr.expr ) 1 2) (+ 3 x)) - (iff (or ( x : Expr.expr ) false) x) + (= (+ ( x : expr ) 0) x) + (= (+ ( x : expr ) 1 2) (+ 3 x)) + (iff (or ( x : expr ) false) x) *) - let is_rewrite ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE) + let is_rewrite ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE) (** Indicates whether the term is a proof by rewriting @@ -4166,14 +4030,14 @@ end = struct - When converting bit-vectors to Booleans (BIT2BOOL=true) - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) *) - let is_rewrite_star ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE_STAR) + let is_rewrite_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE_STAR) (** Indicates whether the term is a proof for pulling quantifiers out. A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *) - let is_pull_quant ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT) + let is_pull_quant ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT) (** Indicates whether the term is a proof for pulling quantifiers out. @@ -4182,7 +4046,7 @@ end = struct This proof object is only used if the parameter PROOF_MODE is 1. This proof object has no antecedents *) - let is_pull_quant_star ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT_STAR) + let is_pull_quant_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT_STAR) (** Indicates whether the term is a proof for pushing quantifiers in. @@ -4195,7 +4059,7 @@ end = struct This proof object has no antecedents *) - let is_push_quant ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PUSH_QUANT) + let is_push_quant ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PUSH_QUANT) (** Indicates whether the term is a proof for elimination of unused variables. @@ -4207,34 +4071,34 @@ end = struct This proof object has no antecedents. *) - let is_elim_unused_vars ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ELIM_UNUSED_VARS) + let is_elim_unused_vars ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ELIM_UNUSED_VARS) (** Indicates whether the term is a proof for destructive equality resolution A proof for destructive equality resolution: - (iff (forall (x) (or (not (= ( x : Expr.expr ) t)) P[x])) P[t]) - if ( x : Expr.expr ) does not occur in t. + (iff (forall (x) (or (not (= ( x : expr ) t)) P[x])) P[t]) + if ( x : expr ) does not occur in t. This proof object has no antecedents. Several variables can be eliminated simultaneously. *) - let is_der ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DER) + let is_der ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DER) (** Indicates whether the term is a proof for quantifier instantiation A proof of (or (not (forall (x) (P x))) (P a)) *) - let is_quant_inst ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INST) + let is_quant_inst ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INST) (** Indicates whether the term is a hypthesis marker. Mark a hypothesis in a natural deduction style proof. *) - let is_hypothesis ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_HYPOTHESIS) + let is_hypothesis ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_HYPOTHESIS) (** Indicates whether the term is a proof by lemma @@ -4246,7 +4110,7 @@ end = struct It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n. *) - let is_lemma ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_LEMMA) + let is_lemma ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_LEMMA) (** Indicates whether the term is a proof by unit resolution @@ -4257,7 +4121,7 @@ end = struct T(n+1): (not l_n) [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') *) - let is_unit_resolution ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_UNIT_RESOLUTION) + let is_unit_resolution ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_UNIT_RESOLUTION) (** Indicates whether the term is a proof by iff-true @@ -4265,7 +4129,7 @@ end = struct T1: p [iff-true T1]: (iff p true) *) - let is_iff_true ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_TRUE) + let is_iff_true ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_TRUE) (** Indicates whether the term is a proof by iff-false @@ -4273,7 +4137,7 @@ end = struct T1: (not p) [iff-false T1]: (iff p false) *) - let is_iff_false ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_FALSE) + let is_iff_false ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_FALSE) (** Indicates whether the term is a proof by commutativity @@ -4285,7 +4149,7 @@ end = struct This proof object has no antecedents. Remark: if f is bool, then = is iff. *) - let is_commutativity ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_COMMUTATIVITY) (* *) + let is_commutativity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_COMMUTATIVITY) (* *) (** Indicates whether the term is a proof for Tseitin-like axioms @@ -4320,7 +4184,7 @@ end = struct unfolding the Boolean connectives in the axioms a small bounded number of steps (=3). *) - let is_def_axiom ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_AXIOM) + let is_def_axiom ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_AXIOM) (** Indicates whether the term is a proof for introduction of a name @@ -4342,7 +4206,7 @@ end = struct Otherwise: [def-intro]: (= n e) *) - let is_def_intro ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_INTRO) + let is_def_intro ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_INTRO) (** Indicates whether the term is a proof for application of a definition @@ -4351,7 +4215,7 @@ end = struct F is 'equivalent' to n, given that T1 is a proof that n is a name for F. *) - let is_apply_def ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_APPLY_DEF) + let is_apply_def ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_APPLY_DEF) (** Indicates whether the term is a proof iff-oeq @@ -4359,7 +4223,7 @@ end = struct T1: (iff p q) [iff~ T1]: (~ p q) *) - let is_iff_oeq ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_OEQ) + let is_iff_oeq ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_OEQ) (** Indicates whether the term is a proof for a positive NNF step @@ -4386,7 +4250,7 @@ end = struct NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'. *) - let is_nnf_pos ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_POS) + let is_nnf_pos ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_POS) (** Indicates whether the term is a proof for a negative NNF step @@ -4410,7 +4274,7 @@ end = struct [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2'))) *) - let is_nnf_neg ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_NEG) + let is_nnf_neg ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_NEG) (** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. @@ -4421,7 +4285,7 @@ end = struct This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *) - let is_nnf_star ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_STAR) + let is_nnf_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_STAR) (** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. @@ -4430,19 +4294,19 @@ end = struct This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *) - let is_cnf_star ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_CNF_STAR) + let is_cnf_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_CNF_STAR) (** Indicates whether the term is a proof for a Skolemization step Proof for: - [sk]: (~ (not (forall ( x : Expr.expr ) (p ( x : Expr.expr ) y))) (not (p (sk y) y))) - [sk]: (~ (exists ( x : Expr.expr ) (p ( x : Expr.expr ) y)) (p (sk y) y)) + [sk]: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y))) + [sk]: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y)) This proof object has no antecedents. *) - let is_skolemize ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SKOLEMIZE) + let is_skolemize ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SKOLEMIZE) (** Indicates whether the term is a proof by modus ponens for equi-satisfiability. @@ -4452,7 +4316,7 @@ end = struct T2: (~ p q) [mp~ T1 T2]: q *) - let is_modus_ponens_oeq ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS_OEQ) + let is_modus_ponens_oeq ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS_OEQ) (** Indicates whether the term is a proof for theory lemma @@ -4470,7 +4334,7 @@ end = struct (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. *) - let is_theory_lemma ( x : Expr.expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TH_LEMMA) + let is_theory_lemma ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TH_LEMMA) end @@ -4480,10 +4344,8 @@ end of formulas, that can be solved and/or transformed using tactics and solvers. *) module Goal = -struct - type goal = z3_native_object - - (**/**) +struct + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : goal = { m_ctx = ctx ; m_n_obj = null ; @@ -4492,7 +4354,7 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** The precision of the goal. @@ -4521,8 +4383,8 @@ struct (** Adds the constraints to the given goal. *) (* CMW: assert seems to be a keyword. *) - let assert_ ( x : goal ) ( constraints : Booleans.bool_expr array ) = - let f e = Z3native.goal_assert (z3obj_gnc x) (z3obj_gno x) (Booleans.gno e) in + let assert_ ( x : goal ) ( constraints : bool_expr array ) = + let f e = Z3native.goal_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e) in ignore (Array.map f constraints) ; () @@ -4543,7 +4405,7 @@ struct (** The formulas in the goal. *) let get_formulas ( x : goal ) = let n = get_size x in - let f i = Booleans.create_expr (z3obj_gc x) (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i) in + let f i = bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (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. *) @@ -4562,7 +4424,7 @@ struct 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 ) = + let simplify ( x : goal ) ( p : params option ) = let tn = Z3native.mk_tactic (z3obj_gnc x) "simplify" in Z3native.tactic_inc_ref (z3obj_gnc x) tn ; let arn = match p with @@ -4602,9 +4464,7 @@ end A Model contains interpretations (assignments) of constants and functions. *) module Model = struct - type model = z3_native_object - - (**/**) + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : model = { m_ctx = ctx ; m_n_obj = null ; @@ -4613,7 +4473,7 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Function interpretations @@ -4622,9 +4482,7 @@ struct *) module FuncInterp = struct - type func_interp = z3_native_object - - (**/**) + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : func_interp = { m_ctx = ctx ; m_n_obj = null ; @@ -4633,17 +4491,15 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Function interpretations entries An Entry object represents an element in the finite map used to a function interpretation. *) module FuncEntry = - struct - type func_entry = z3_native_object - - (**/**) + struct + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : func_entry = { m_ctx = ctx ; m_n_obj = null ; @@ -4652,13 +4508,13 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Return the (symbolic) value of this entry. *) let get_value ( x : func_entry ) = - Expr.create (z3obj_gc x) (Z3native.func_entry_get_value (z3obj_gnc x) (z3obj_gno x)) + expr_of_ptr (z3obj_gc x) (Z3native.func_entry_get_value (z3obj_gnc x) (z3obj_gno x)) (** The number of arguments of the entry. @@ -4670,7 +4526,7 @@ struct *) let get_args ( x : func_entry ) = let n = (get_num_args x) in - let f i = (Expr.create (z3obj_gc x) (Z3native.func_entry_get_arg (z3obj_gnc x) (z3obj_gno x) i)) in + let f i = (expr_of_ptr (z3obj_gc x) (Z3native.func_entry_get_arg (z3obj_gnc x) (z3obj_gno x) i)) in Array.init n f (** @@ -4698,7 +4554,7 @@ struct (** The (symbolic) `else' value of the function interpretation. *) - let get_else ( x : func_interp ) = Expr.create (z3obj_gc x) (Z3native.func_interp_get_else (z3obj_gnc x) (z3obj_gno x)) + let get_else ( x : func_interp ) = expr_of_ptr (z3obj_gc x) (Z3native.func_interp_get_else (z3obj_gnc x) (z3obj_gno x)) (** The arity of the function interpretation @@ -4725,7 +4581,7 @@ struct (** Retrieves the interpretation (the assignment) of in the model. A function declaration of zero arity An expression if the function has an interpretation in the model, null otherwise. *) - let get_const_interp ( x : model ) ( f : FuncDecl.func_decl ) = + let get_const_interp ( x : model ) ( f : func_decl ) = if (FuncDecl.get_arity f) != 0 || (sort_kind_of_int (Z3native.get_sort_kind (FuncDecl.gnc f) (Z3native.get_range (FuncDecl.gnc f) (FuncDecl.gno f)))) == ARRAY_SORT then raise (Z3native.Exception "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.") @@ -4734,19 +4590,19 @@ struct if (Z3native.is_null np) then None else - Some (Expr.create (z3obj_gc x) np) + Some (expr_of_ptr (z3obj_gc x) np) (** Retrieves the interpretation (the assignment) of in the model. A Constant An expression if the constant has an interpretation in the model, null otherwise. *) - let get_const_interp_e ( x : model ) ( a : Expr.expr ) = get_const_interp x (Expr.get_func_decl a) + let get_const_interp_e ( x : model ) ( a : expr ) = get_const_interp x (Expr.get_func_decl a) (** Retrieves the interpretation (the assignment) of a non-constant in the model. A function declaration of non-zero arity A FunctionInterpretation if the function has an interpretation in the model, null otherwise. *) - let rec get_func_interp ( x : model ) ( f : FuncDecl.func_decl ) = + let rec get_func_interp ( x : model ) ( f : func_decl ) = let sk = (sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc x) (Z3native.get_range (FuncDecl.gnc f) (FuncDecl.gno f)))) in if (FuncDecl.get_arity f) == 0 then let n = Z3native.model_get_const_interp (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) in @@ -4759,7 +4615,7 @@ 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 (FuncDecl.create (z3obj_gc x) fd) + get_func_interp x (func_decl_of_ptr (z3obj_gc x) 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) (FuncDecl.gno f)) in @@ -4771,7 +4627,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 = FuncDecl.create (z3obj_gc x) (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in + let f i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f @@ -4781,15 +4637,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 = FuncDecl.create (z3obj_gc x) (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in + let f i = func_decl_of_ptr (z3obj_gc x) (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 = FuncDecl.create (z3obj_gc x) (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in - let g i = FuncDecl.create (z3obj_gc x) (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in + let f i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in + let g i = func_decl_of_ptr (z3obj_gc x) (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. *) @@ -4810,15 +4666,15 @@ struct The evaluation of in the model. *) - let eval ( x : model ) ( t : Expr.expr ) ( completion : bool ) = - let (r, v) = (Z3native.model_eval (z3obj_gnc x) (z3obj_gno x) (Expr.gno t) completion) in + let eval ( x : model ) ( t : expr ) ( completion : bool ) = + let (r, v) = (Z3native.model_eval (z3obj_gnc x) (z3obj_gno x) (ptr_of_expr t) completion) in if not r then raise (ModelEvaluationFailedException "evaluation failed") else - Expr.create (z3obj_gc x) v + expr_of_ptr (z3obj_gc x) v (** Alias for eval. *) - let evaluate ( x : model ) ( t : Expr.expr ) ( completion : bool ) = + let evaluate ( x : model ) ( t : expr ) ( completion : bool ) = eval x t completion (** The number of uninterpreted sorts that the model has an interpretation for. *) @@ -4834,7 +4690,7 @@ struct *) let get_sorts ( x : model ) = let n = (get_num_sorts x) in - let f i = (Sort.create (z3obj_gc x) (Z3native.model_get_sort (z3obj_gnc x) (z3obj_gno x) i)) in + let f i = (sort_of_ptr (z3obj_gc x) (Z3native.model_get_sort (z3obj_gnc x) (z3obj_gno x) i)) in Array.init n f @@ -4843,10 +4699,10 @@ struct An uninterpreted sort An array of expressions, where each is an element of the universe of *) - let sort_universe ( x : model ) ( s : Sort.sort ) = - let n_univ = AST.ASTVectors.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in - let n = (AST.ASTVectors.get_size n_univ) in - let f i = (AST.ASTVectors.get n_univ i) in + let sort_universe ( x : model ) ( s : sort ) = + let n_univ = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in + let n = (AST.ASTVector.get_size n_univ) in + let f i = (AST.ASTVector.get n_univ i) in Array.init n f (** Conversion of models to strings. @@ -4866,9 +4722,7 @@ end *) module Probe = struct - type probe = z3_native_object - - (**/**) + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : probe = { m_ctx = ctx ; m_n_obj = null ; @@ -4877,14 +4731,14 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Execute the probe over the goal. A probe always produce a double value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. *) - let apply ( x : probe ) (g : Goal.goal) = + let apply ( x : probe ) (g : goal) = Z3native.probe_apply (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g) (** @@ -4988,10 +4842,8 @@ end It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. *) module Tactic = -struct - type tactic = z3_native_object - - (**/**) +struct + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : tactic = { m_ctx = ctx ; m_n_obj = null ; @@ -5000,7 +4852,7 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Tactic application results @@ -5008,9 +4860,7 @@ struct tactic to a goal. It contains the subgoals that were produced. *) module ApplyResult = struct - type apply_result = z3_native_object - - (**/**) + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : apply_result = { m_ctx = ctx ; m_n_obj = null ; @@ -5019,7 +4869,7 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** The number of Subgoals. *) let get_num_subgoals ( x : apply_result ) = @@ -5039,7 +4889,7 @@ struct goal g, that the ApplyResult was obtained from. #return A model for g *) - let convert_model ( x : apply_result ) ( i : int ) ( m : Model.model ) = + let convert_model ( x : apply_result ) ( i : int ) ( m : model ) = 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. *) @@ -5054,7 +4904,7 @@ struct 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 ) = + let apply ( x : tactic ) ( g : goal ) ( p : params option ) = match p with | 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))) @@ -5122,14 +4972,14 @@ struct If evaluates to false, then the new tactic behaves like the skip tactic. *) (* CMW: when is a keyword *) - let when_ ( ctx : context ) ( p : Probe.probe ) ( t : tactic ) = + let when_ ( ctx : context ) ( p : probe ) ( t : tactic ) = 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 ) = + let cond ( ctx : context ) ( p : probe ) ( t1 : tactic ) ( t2 : tactic ) = create ctx (Z3native.tactic_cond (context_gno ctx) (z3obj_gno p) (z3obj_gno t1) (z3obj_gno t2)) (** @@ -5154,7 +5004,7 @@ struct (** Create a tactic that fails if the probe evaluates to false. *) - let fail_if ( ctx : context ) ( p : Probe.probe ) = + let fail_if ( ctx : context ) ( p : probe ) = create ctx (Z3native.tactic_fail_if (context_gno ctx) (z3obj_gno p)) (** @@ -5167,14 +5017,14 @@ struct (** Create a tactic that applies using the given set of parameters . *) - let using_params ( ctx : context ) ( t : tactic ) ( p : Params.params ) = + let using_params ( ctx : context ) ( t : tactic ) ( p : params ) = 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 . Alias for UsingParams*) (* CMW: with is a keyword *) - let with_ ( ctx : context ) ( t : tactic ) ( p : Params.params ) = + let with_ ( ctx : context ) ( t : tactic ) ( p : params ) = using_params ctx t p (** @@ -5201,10 +5051,8 @@ end (** Solvers *) module Solver = -struct - type solver = z3_native_object - - (**/**) +struct + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : solver = { m_ctx = ctx ; m_n_obj = null ; @@ -5213,9 +5061,7 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) - - type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE + let string_of_status ( s : status) = match s with | UNSATISFIABLE -> "unsatisfiable" @@ -5224,10 +5070,8 @@ struct (** Objects that track statistical information about solvers. *) module Statistics = - struct - type statistics = z3_native_object - - (**/**) + struct + let create ( ctx : context ) ( no : Z3native.ptr ) = let res : statistics = { m_ctx = ctx ; m_n_obj = null ; @@ -5236,7 +5080,7 @@ struct (z3obj_sno res ctx no) ; (z3obj_create res) ; res - (**/**) + (** Statistical data is organized into pairs of \[Key, Entry\], where every @@ -5245,14 +5089,7 @@ struct *) module Entry = struct - type statistics_entry = { - mutable m_key : string; - mutable m_is_int : bool ; - mutable m_is_float : bool ; - mutable m_int : int ; - mutable m_float : float } - - (**/**) + let create_si k v = let res : statistics_entry = { m_key = k ; @@ -5272,7 +5109,7 @@ struct m_float = v } in res - (**/**) + (** The key of the entry. *) let get_key (x : statistics_entry) = x.m_key @@ -5344,7 +5181,7 @@ struct (** Sets the solver parameters. *) - let set_parameters ( x : solver ) ( p : Params.params )= + let set_parameters ( x : solver ) ( p : params )= Z3native.solver_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) (** @@ -5382,8 +5219,8 @@ struct (** Assert a constraint (or multiple) into the solver. *) - let assert_ ( x : solver ) ( constraints : Booleans.bool_expr array ) = - let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) (Booleans.gno e)) in + let assert_ ( x : solver ) ( constraints : bool_expr array ) = + let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e)) in ignore (Array.map f constraints) (** @@ -5399,11 +5236,11 @@ struct * and the Boolean literals * provided using with assumptions. *) - let assert_and_track ( x : solver ) ( cs : Booleans.bool_expr array ) ( ps : Booleans.bool_expr array ) = + let assert_and_track ( x : solver ) ( cs : bool_expr array ) ( ps : bool_expr array ) = if ((Array.length cs) != (Array.length ps)) then raise (Z3native.Exception "Argument size mismatch") else - let f i e = (Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Booleans.gno e) (Booleans.gno (Array.get ps i))) in + let f i e = (Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e) (Boolean.gno (Array.get ps i))) in ignore (Array.iteri f cs) (** @@ -5418,24 +5255,24 @@ struct * and the Boolean literals * provided using with assumptions. *) - let assert_and_track ( x : solver ) ( c : Booleans.bool_expr ) ( p : Booleans.bool_expr ) = - Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Booleans.gno c) (Booleans.gno p) + let assert_and_track ( x : solver ) ( c : bool_expr ) ( p : bool_expr ) = + Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Boolean.gno c) (Boolean.gno p) (** The number of assertions in the solver. *) let get_num_assertions ( x : solver ) = - let a = AST.ASTVectors.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in - (AST.ASTVectors.get_size a) + let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in + (AST.ASTVector.get_size a) (** The set of asserted formulas. *) let get_assertions ( x : solver ) = - let a = AST.ASTVectors.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in - let n = (AST.ASTVectors.get_size a) in - let f i = Booleans.create_expr (z3obj_gc x) (z3obj_gno (AST.ASTVectors.get a i)) 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 = bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in Array.init n f (** @@ -5445,12 +5282,13 @@ struct *) - let check ( x : solver ) ( assumptions : Booleans.bool_expr array) = + let check ( x : solver ) ( assumptions : bool_expr array) = let r = 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) (Booleans.aton assumptions)) + let f x = (ptr_of_expr (expr_of_bool_expr x)) in + lbool_of_int (Z3native.solver_check_assumptions (z3obj_gnc x) (z3obj_gno x) (Array.length assumptions) (Array.map f assumptions)) in match r with | L_TRUE -> SATISFIABLE @@ -5481,7 +5319,7 @@ struct if (Z3native.is_null q) then None else - Some (Expr.create (z3obj_gc x) q) + Some (expr_of_ptr (z3obj_gc x) q) (** The unsat core of the last Check. @@ -5491,9 +5329,9 @@ struct if its results was not UNSATISFIABLE, or if core production is disabled. *) let get_unsat_core ( x : solver ) = - let cn = AST.ASTVectors.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in - let n = (AST.ASTVectors.get_size cn) in - let f i = (AST.ASTVectors.get cn i) 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 (** @@ -5515,7 +5353,7 @@ struct check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved. *) - let mk_solver ( ctx : context ) ( logic : Symbol.symbol option ) = + let mk_solver ( ctx : context ) ( logic : symbol option ) = match logic with | None -> (create ctx (Z3native.mk_solver (context_gno ctx))) | Some (x) -> (create ctx (Z3native.mk_solver_for_logic (context_gno ctx) (Symbol.gno x))) @@ -5539,7 +5377,7 @@ struct The solver supports the commands Push and Pop, but it will always solve each check from scratch. *) - let mk_solver_t ( ctx : context ) ( t : Tactic.tactic ) = + let mk_solver_t ( ctx : context ) ( t : tactic ) = (create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t))) (** @@ -5551,10 +5389,7 @@ end (** Fixedpoint solving *) module Fixedpoint = -struct - type fixedpoint = z3_native_object - - (**/**) +struct let create ( ctx : context ) = let res : fixedpoint = { m_ctx = ctx ; m_n_obj = null ; @@ -5563,7 +5398,7 @@ struct (z3obj_sno res ctx (Z3native.mk_fixedpoint (context_gno ctx))) ; (z3obj_create res) ; res - (**/**) + (** A string that describes all available fixedpoint solver parameters. @@ -5574,7 +5409,7 @@ struct (** Sets the fixedpoint solver parameters. *) - let set_params ( x : fixedpoint ) ( p : Params.params )= + let set_params ( x : fixedpoint ) ( p : params )= Z3native.fixedpoint_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) (** @@ -5586,29 +5421,29 @@ struct (** Assert a constraints into the fixedpoint solver. *) - let assert_ ( x : fixedpoint ) ( constraints : Booleans.bool_expr array ) = - let f e = (Z3native.fixedpoint_assert (z3obj_gnc x) (z3obj_gno x) (Booleans.gno e)) in + let assert_ ( x : fixedpoint ) ( constraints : bool_expr array ) = + let f e = (Z3native.fixedpoint_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e)) in ignore (Array.map f constraints) ; () (** Register predicate as recursive relation. *) - let register_relation ( x : fixedpoint ) ( f : FuncDecl.func_decl ) = + let register_relation ( x : fixedpoint ) ( f : func_decl ) = Z3native.fixedpoint_register_relation (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) (** Add rule into the fixedpoint solver. *) - let add_rule ( x : fixedpoint ) ( rule : Booleans.bool_expr ) ( name : Symbol.symbol option ) = + let add_rule ( x : fixedpoint ) ( rule : bool_expr ) ( name : symbol option ) = match name with - | None -> Z3native.fixedpoint_add_rule (z3obj_gnc x) (z3obj_gno x) (Booleans.gno rule) null - | Some(y) -> Z3native.fixedpoint_add_rule (z3obj_gnc x) (z3obj_gno x) (Booleans.gno rule) (Symbol.gno y) + | None -> Z3native.fixedpoint_add_rule (z3obj_gnc x) (z3obj_gno x) (Boolean.gno rule) null + | Some(y) -> Z3native.fixedpoint_add_rule (z3obj_gnc x) (z3obj_gno x) (Boolean.gno rule) (Symbol.gno y) (** Add table fact to the fixedpoint solver. *) - let add_fact ( x : fixedpoint ) ( pred : FuncDecl.func_decl ) ( args : int array ) = + let add_fact ( x : fixedpoint ) ( pred : func_decl ) ( args : int array ) = Z3native.fixedpoint_add_fact (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno pred) (Array.length args) args (** @@ -5617,11 +5452,11 @@ struct The query is satisfiable if there is an instance of the query variables and a derivation for it. The query is unsatisfiable if there are no derivations satisfying the query variables. *) - let query ( x : fixedpoint ) ( query : Booleans.bool_expr ) = - match (lbool_of_int (Z3native.fixedpoint_query (z3obj_gnc x) (z3obj_gno x) (Booleans.gno query))) with - | L_TRUE -> Solver.SATISFIABLE - | L_FALSE -> Solver.UNSATISFIABLE - | _ -> Solver.UNKNOWN + let query ( x : fixedpoint ) ( query : bool_expr ) = + match (lbool_of_int (Z3native.fixedpoint_query (z3obj_gnc x) (z3obj_gno x) (Boolean.gno query))) with + | L_TRUE -> SATISFIABLE + | L_FALSE -> UNSATISFIABLE + | _ -> UNKNOWN (** Query the fixedpoint solver. @@ -5629,11 +5464,12 @@ struct The query is satisfiable if there is an instance of some relation that is non-empty. The query is unsatisfiable if there are no derivations satisfying any of the relations. *) - let query_r ( x : fixedpoint ) ( relations : FuncDecl.func_decl array ) = - match (lbool_of_int (Z3native.fixedpoint_query_relations (z3obj_gnc x) (z3obj_gno x) (Array.length relations) (FuncDecl.aton relations))) with - | L_TRUE -> Solver.SATISFIABLE - | L_FALSE -> Solver.UNSATISFIABLE - | _ -> Solver.UNKNOWN + let query_r ( x : fixedpoint ) ( relations : func_decl array ) = + let f x = ptr_of_ast (ast_of_func_decl x) in + match (lbool_of_int (Z3native.fixedpoint_query_relations (z3obj_gnc x) (z3obj_gno x) (Array.length relations) (Array.map f relations))) with + | L_TRUE -> SATISFIABLE + | L_FALSE -> UNSATISFIABLE + | _ -> UNKNOWN (** Creates a backtracking point. @@ -5654,8 +5490,8 @@ struct (** Update named rule into in the fixedpoint solver. *) - let update_rule ( x : fixedpoint ) ( rule : Booleans.bool_expr ) ( name : Symbol.symbol ) = - Z3native.fixedpoint_update_rule (z3obj_gnc x) (z3obj_gno x) (Booleans.gno rule) (Symbol.gno name) + let update_rule ( x : fixedpoint ) ( rule : bool_expr ) ( name : symbol ) = + Z3native.fixedpoint_update_rule (z3obj_gnc x) (z3obj_gno x) (Boolean.gno rule) (Symbol.gno name) (** Retrieve satisfying instance or instances of solver, @@ -5666,7 +5502,7 @@ struct if (Z3native.is_null q) then None else - Some (Expr.create (z3obj_gc x) q) + Some (expr_of_ptr (z3obj_gc x) q) (** Retrieve explanation why fixedpoint engine returned status Unknown. @@ -5677,25 +5513,25 @@ struct (** Retrieve the number of levels explored for a given predicate. *) - let get_num_levels ( x : fixedpoint ) ( predicate : FuncDecl.func_decl ) = + let get_num_levels ( x : fixedpoint ) ( predicate : func_decl ) = Z3native.fixedpoint_get_num_levels (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno predicate) (** Retrieve the cover of a predicate. *) - let get_cover_delta ( x : fixedpoint ) ( level : int ) ( predicate : FuncDecl.func_decl ) = + let get_cover_delta ( x : fixedpoint ) ( level : int ) ( predicate : func_decl ) = let q = (Z3native.fixedpoint_get_cover_delta (z3obj_gnc x) (z3obj_gno x) level (FuncDecl.gno predicate)) in if (Z3native.is_null q) then None else - Some (Expr.create (z3obj_gc x) q) + Some (expr_of_ptr (z3obj_gc x) q) (** Add property about the predicate. The property is added at level. *) - let add_cover ( x : fixedpoint ) ( level : int ) ( predicate : FuncDecl.func_decl ) ( property : Expr.expr ) = - Z3native.fixedpoint_add_cover (z3obj_gnc x) (z3obj_gno x) level (FuncDecl.gno predicate) (Expr.gno property) + let add_cover ( x : fixedpoint ) ( level : int ) ( predicate : func_decl ) ( property : expr ) = + Z3native.fixedpoint_add_cover (z3obj_gnc x) (z3obj_gno x) level (FuncDecl.gno predicate) (ptr_of_expr property) (** Retrieve internal string representation of fixedpoint object. @@ -5705,31 +5541,33 @@ struct (** Instrument the Datalog engine on which table representation to use for recursive predicate. *) - let set_predicate_representation ( x : fixedpoint ) ( f : FuncDecl.func_decl ) ( kinds : Symbol.symbol array ) = - Z3native.fixedpoint_set_predicate_representation (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) (Array.length kinds) (Symbol.aton kinds) + let set_predicate_representation ( x : fixedpoint ) ( f : func_decl ) ( kinds : symbol array ) = + let f2 x = (Symbol.gno x) in + Z3native.fixedpoint_set_predicate_representation (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) (Array.length kinds) (Array.map f2 kinds) (** Convert benchmark given as set of axioms, rules and queries to a string. *) - let to_string_q ( x : fixedpoint ) ( queries : Booleans.bool_expr array ) = - Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (Array.length queries) (Booleans.aton queries) + let to_string_q ( x : fixedpoint ) ( queries : bool_expr array ) = + let f x = ptr_of_expr (expr_of_bool_expr x) in + Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (Array.length queries) (Array.map f queries) (** Retrieve set of rules added to fixedpoint context. *) let get_rules ( x : fixedpoint ) = - let v = (AST.ASTVectors.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in - let n = (AST.ASTVectors.get_size v) in - let f i = Booleans.create_expr (z3obj_gc x) (z3obj_gno (AST.ASTVectors.get v i)) 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 = bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in Array.init n f (** Retrieve set of assertions added to fixedpoint context. *) let get_assertions ( x : fixedpoint ) = - let v = (AST.ASTVectors.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in - let n = (AST.ASTVectors.get_size v) in - let f i = Booleans.create_expr (z3obj_gc x) (z3obj_gno (AST.ASTVectors.get v i)) 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 = bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in Array.init n f (** @@ -5813,10 +5651,10 @@ struct @param formula Formula to be checked for consistency in conjunction with assumptions. @return A string representation of the benchmark. *) - let benchmark_to_smtstring ( ctx : context ) ( name : string ) ( logic : string ) ( status : string ) ( attributes : string ) ( assumptions : Booleans.bool_expr array ) ( formula : Booleans.bool_expr ) = + 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) (Booleans.aton assumptions) - (Booleans.gno formula) + (Array.length assumptions) (let f x = ptr_of_expr (expr_of_bool_expr x) in (Array.map f assumptions)) + (Boolean.gno formula) (** Parse the given string using the SMT-LIB parser. @@ -5827,7 +5665,7 @@ struct and . This is a useful feature since we can use arbitrary names to reference sorts and declarations. *) - let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( decl_names : Symbol.symbol array ) ( decls : FuncDecl.func_decl array ) = + let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : symbol array ) ( sorts : sort array ) ( decl_names : symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in let cdn = (Array.length decl_names) in @@ -5837,17 +5675,17 @@ struct else Z3native.parse_smtlib_string (context_gno ctx) str cs - (Symbol.aton sort_names) - (Sort.aton sorts) + (let f x = Symbol.gno x in (Array.map f sort_names)) + (let f x = Sort.gno x in (Array.map f sorts)) cd - (Symbol.aton decl_names) - (FuncDecl.aton decls) + (let f x = Symbol.gno x in (Array.map f decl_names)) + (let f x = FuncDecl.gno x in (Array.map f decls)) (** Parse the given file using the SMT-LIB parser. *) - let parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( decl_names : Symbol.symbol array ) ( decls : FuncDecl.func_decl array ) = + let parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : symbol array ) ( sorts : sort array ) ( decl_names : symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in let cdn = (Array.length decl_names) in @@ -5857,11 +5695,11 @@ struct else Z3native.parse_smtlib_file (context_gno ctx) file_name cs - (Symbol.aton sort_names) - (Sort.aton sorts) + (let f x = Symbol.gno x in (Array.map f sort_names)) + (let f x = Sort.gno x in (Array.map f sorts)) cd - (Symbol.aton decl_names) - (FuncDecl.aton decls) + (let f x = Symbol.gno x in (Array.map f decl_names)) + (let f x = FuncDecl.gno x in (Array.map f decls)) (** The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. @@ -5873,7 +5711,7 @@ struct *) let get_smtlib_formulas ( ctx : context ) = let n = (get_num_smtlib_formulas ctx ) in - let f i = Booleans.create_expr ctx (Z3native.get_smtlib_formula (context_gno ctx) i) in + let f i = bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_formula (context_gno ctx) i)) in Array.init n f @@ -5887,7 +5725,7 @@ struct *) let get_smtlib_assumptions ( ctx : context ) = let n = (get_num_smtlib_assumptions ctx ) in - let f i = Booleans.create_expr ctx (Z3native.get_smtlib_assumption (context_gno ctx) i) in + let f i = bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_assumption (context_gno ctx) i)) in Array.init n f (** @@ -5900,7 +5738,7 @@ struct *) let get_smtlib_decls ( ctx : context ) = let n = (get_num_smtlib_decls ctx) in - let f i = FuncDecl.create ctx (Z3native.get_smtlib_decl (context_gno ctx) i) in + let f i = func_decl_of_ptr ctx (Z3native.get_smtlib_decl (context_gno ctx) i) in Array.init n f (** @@ -5913,7 +5751,7 @@ struct *) let get_smtlib_sorts ( ctx : context ) = let n = (get_num_smtlib_sorts ctx) in - let f i = (Sort.create ctx (Z3native.get_smtlib_sort (context_gno ctx) i)) in + let f i = (sort_of_ptr ctx (Z3native.get_smtlib_sort (context_gno ctx) i)) in Array.init n f (** @@ -5922,7 +5760,7 @@ struct @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *) - let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( decl_names : Symbol.symbol array ) ( decls : FuncDecl.func_decl array ) = + let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : symbol array ) ( sorts : sort array ) ( decl_names : symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in let cdn = (Array.length decl_names) in @@ -5930,19 +5768,19 @@ struct if (csn != cs || cdn != cd) then raise (Z3native.Exception "Argument size mismatch") else - Z3native.parse_smtlib2_string (context_gno ctx) str - cs - (Symbol.aton sort_names) - (Sort.aton sorts) - cd - (Symbol.aton decl_names) - (FuncDecl.aton decls) + bool_expr_of_expr (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) str + cs + (let f x = Symbol.gno x in (Array.map f sort_names)) + (let f x = Sort.gno x in (Array.map f sorts)) + cd + (let f x = Symbol.gno x in (Array.map f decl_names)) + (let f x = FuncDecl.gno x in (Array.map f decls)))) (** Parse the given file using the SMT-LIB2 parser. *) - let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol array ) ( sorts : Sort.sort array ) ( decl_names : Symbol.symbol array ) ( decls : FuncDecl.func_decl array ) = + let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : symbol array ) ( sorts : sort array ) ( decl_names : symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in let cdn = (Array.length decl_names) in @@ -5950,13 +5788,13 @@ struct if (csn != cs || cdn != cd) then raise (Z3native.Exception "Argument size mismatch") else - Z3native.parse_smtlib2_string (context_gno ctx) file_name + bool_expr_of_expr (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) file_name cs - (Symbol.aton sort_names) - (Sort.aton sorts) + (let f x = Symbol.gno x in (Array.map f sort_names)) + (let f x = Sort.gno x in (Array.map f sorts)) cd - (Symbol.aton decl_names) - (FuncDecl.aton decls) + (let f x = Symbol.gno x in (Array.map f decl_names)) + (let f x = FuncDecl.gno x in (Array.map f decls)))) end