diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 1d3412c30..cfea8d0f1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1350,10 +1350,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')
@@ -1361,7 +1368,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')
@@ -2732,6 +2739,76 @@ def mk_z3consts_ml(api_files):
efile.write('end\n')
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