diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml
index 49db6fb50..6dfe11623 100644
--- a/examples/ml/ml_example.ml
+++ b/examples/ml/ml_example.ml
@@ -15,6 +15,9 @@ open Z3.Tactic.ApplyResult
open Z3.Probe
open Z3.Solver
open Z3.Arithmetic
+open Z3.Arithmetic.Integer
+open Z3.Arithmetic.Real
+open Z3.BitVector
exception TestFailedException of string
@@ -35,7 +38,7 @@ let model_converter_test ( ctx : context ) =
(Real.mk_numeral_nd ctx 10 1)))) |]) ;
(Goal.assert_ g4 [| (mk_eq ctx
(expr_of_arith_expr yr)
- (expr_of_arith_expr (mk_add ctx [| xr; (arith_expr_of_real_expr (real_expr_of_rat_num (Real.mk_numeral_nd ctx 1 1))) |] ))) |] ) ;
+ (expr_of_arith_expr (Arithmetic.mk_add ctx [| xr; (arith_expr_of_real_expr (real_expr_of_rat_num (Real.mk_numeral_nd ctx 1 1))) |]) ) ) |] ) ;
(Goal.assert_ g4 [| (mk_gt ctx yr (arith_expr_of_real_expr (real_expr_of_rat_num (Real.mk_numeral_nd ctx 1 1)))) |]) ;
(
let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
diff --git a/scripts/update_api.py b/scripts/update_api.py
index e5c66dd39..a0b7e6250 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1155,6 +1155,7 @@ def mk_ml():
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_i.write('(**/**)\n\n');
ml_native.write('open Z3enums\n\n')
ml_native.write('(**/**)\n')
ml_native.write('type ptr\n')
@@ -1214,6 +1215,7 @@ def mk_ml():
ml_native.write(' "n_%s_bytecode"\n' % ml_method_name(name))
ml_native.write('\n')
ml_native.write(' end\n\n')
+ ml_i.write('\n(**/**)\n');
# Exception wrappers
for name, result, params in _dotnet_decls:
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 45faae468..c261fce05 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -16,104 +16,11 @@ let is_null o = (Z3native.is_null o)
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 = z3_native_object
-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 *)
@@ -121,11 +28,9 @@ 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? *)
+ Printf.printf "ERROR: NOT DISPOSING CONTEXT (because it still has %d objects alive)\n" ctx.m_n_obj_cnt;
)
let create_context settings =
@@ -136,7 +41,6 @@ struct
Z3native.del_config(cfg) ;
Z3native.set_ast_print_mode v (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ;
Z3native.set_internal_error_handler v ;
- (* 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;
@@ -178,16 +82,6 @@ struct
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 ;
@@ -196,323 +90,25 @@ struct
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
+ res
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(a) ->
- let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
- let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) 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(a) ->
- let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
- let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) 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(a) ->
- let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
- let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) 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(a) ->
- let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
- let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) 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(a) ->
- let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
- let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) 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(a)) ->
- let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
- let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) 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(a)) ->
- let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
- let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) 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(a))) ->
- if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
- raise (Z3native.Exception "Invalid coercion")
- else
- IntNum(e)
-
-let rat_num_of_real_expr e =
- match e with RealExpr(ArithExpr(Expr(a))) ->
- if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
- raise (Z3native.Exception "Invalid coercion")
- else
- RatNum(e)
-
-let algebraic_num_of_arith_expr e =
- match e with ArithExpr(Expr(a)) ->
- if (not (Z3native.is_algebraic_number (z3obj_gnc a) (z3obj_gno a))) then
- raise (Z3native.Exception "Invalid coercion")
- else
- AlgebraicNum(e)
-
-let bitvec_num_of_bitvec_expr e =
- match e with BitVecExpr(Expr(a)) ->
- if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
- raise (Z3native.Exception "Invalid coercion")
- else
- BitVecNum(e)
-
-let quantifier_of_expr e =
- match e with Expr(a) ->
- let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) 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 =
struct
- (** Open an interaction log file.
- @param filename the name of the file to open.
- @return True if opening the log file succeeds, false otherwise.
- *)
- (* CMW: "open" seems to be a reserved keyword? *)
let open_ filename = ((lbool_of_int (Z3native.open_log filename)) == L_TRUE)
-
- (** Closes the interaction log. *)
let close = Z3native.close_log
-
- (** Appends a user-provided string to the interaction log.
- @param s the string to append*)
let append s = Z3native.append_log s
end
-(** Version information *)
module Version =
struct
- (** The major version. *)
let major = let (x, _, _, _) = Z3native.get_version in x
-
- (** The minor version. *)
let minor = let (_, x, _, _) = Z3native.get_version in x
-
- (** The build version. *)
let build = let (_, _, x, _) = Z3native.get_version in x
-
- (** The revision. *)
let revision = let (_, _, _, x) = Z3native.get_version in x
-
- (** A string representation of the version information. *)
let to_string =
let (mj, mn, bld, rev) = Z3native.get_version in
string_of_int mj ^ "." ^
@@ -532,35 +128,21 @@ let mk_list ( f : int -> 'a ) ( n : int ) =
mk_list' f 0 n []
-(** Create a context object.
-
- Most interactions with Z3 are interpreted in some context; many users will only
- require one such object, but power users may require more than one. To start using
- Z3, do
-
-
- let ctx = (mk_context []) in
- (...)
-
-
- where a list of pairs of strings may be passed to set options on
- the context, e.g., like so:
-
-
- let cfg = [("model", "true"); ("...", "...")] in
- let ctx = (mk_context cfg) in
- (...)
-
-*)
let mk_context ( cfg : ( string * string ) list ) =
create_context cfg
-
-
-(** Symbols are used to name several term and type constructors *)
module Symbol =
-struct
+struct
+ (* 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
+
+
let create_i ( ctx : context ) ( no : Z3native.ptr ) =
let res : int_symbol = { m_ctx = ctx ;
m_n_obj = null ;
@@ -588,7 +170,7 @@ struct
match x with
| S_Int(n) -> (z3obj_gc n)
| S_Str(n) -> (z3obj_gc n)
-
+
let gnc ( x : symbol ) =
match x with
| S_Int(n) -> (z3obj_gnc n)
@@ -599,59 +181,55 @@ struct
| S_Int(n) -> (z3obj_gno n)
| S_Str(n) -> (z3obj_gno n)
- (** The kind of the symbol (int or string) *)
- let kind ( o : symbol ) = (symbol_kind_of_int (Z3native.get_symbol_kind (gnc o) (gno o)))
-
- (** Indicates whether the symbol is of Int kind *)
+ let kind ( o : symbol ) = (symbol_kind_of_int (Z3native.get_symbol_kind (gnc o) (gno o)))
let is_int_symbol ( o : symbol ) = (kind o) == INT_SYMBOL
-
- (** Indicates whether the symbol is of string kind. *)
let is_string_symbol ( o : symbol ) = (kind o) == STRING_SYMBOL
-
- (** The int value of the symbol. *)
let get_int (o : int_symbol) = Z3native.get_symbol_int (z3obj_gnc o) (z3obj_gno o)
-
- (** The string value of the symbol. *)
let get_string (o : string_symbol) = Z3native.get_symbol_string (z3obj_gnc o) (z3obj_gno o)
-
- (** A string representation of the symbol. *)
let to_string ( o : symbol ) =
match (kind o) with
| INT_SYMBOL -> (string_of_int (Z3native.get_symbol_int (gnc o) (gno o)))
| STRING_SYMBOL -> (Z3native.get_symbol_string (gnc o) (gno o))
- (**
- Creates a new symbol using an integer.
-
- Not all integers can be passed to this function.
- The legal range of unsigned integers is 0 to 2^30-1.
- *)
let mk_int ( ctx : context ) ( i : int ) =
S_Int (create_i ctx (Z3native.mk_int_symbol (context_gno ctx) i))
- (** Creates a new symbol using a string. *)
let mk_string ( ctx : context ) ( s : string ) =
S_Str (create_s ctx (Z3native.mk_string_symbol (context_gno ctx) s))
- (** Create an array of symbols. *)
let mk_ints ( ctx : context ) ( names : int array ) =
let f elem = mk_int ( ctx : context ) elem in
(Array.map f names)
- (** Create an array of symbols. *)
let mk_strings ( ctx : context ) ( names : string array ) =
let f elem = mk_string ( ctx : context ) elem in
(Array.map f names)
end
-(** The abstract syntax tree (AST) module *)
module AST =
-struct
- (** Vectors of ASTs *)
+struct
+ type ast = z3_native_object
+
+ 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 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")
+
module ASTVector =
struct
- let create ( ctx : context ) ( no : Z3native.ptr ) =
+ type ast_vector = z3_native_object
+
+ let ast_vector_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let res : ast_vector = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = Z3native.ast_vector_inc_ref ;
@@ -659,55 +237,34 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
-
- (** The size of the vector *)
+
let get_size ( x : ast_vector ) =
Z3native.ast_vector_size (z3obj_gnc x) (z3obj_gno x)
- (**
- Retrieves the i-th object in the vector.
- @param i Index
- @return An AST
- *)
let get ( x : ast_vector ) ( i : int ) =
- create (z3obj_gc x) (Z3native.ast_vector_get (z3obj_gnc x) (z3obj_gno x) i)
+ ast_of_ptr (z3obj_gc x) (Z3native.ast_vector_get (z3obj_gnc x) (z3obj_gno x) i)
- (** Sets the i-th object in the vector. *)
let set ( x : ast_vector ) ( i : int ) ( value : ast ) =
Z3native.ast_vector_set (z3obj_gnc x) (z3obj_gno x) i (z3obj_gno value)
- (** Resize the vector to .
- @param newSize The new size of the vector. *)
let resize ( x : ast_vector ) ( new_size : int ) =
Z3native.ast_vector_resize (z3obj_gnc x) (z3obj_gno x) new_size
- (**
- Add the AST to the back of the vector. The size
- is increased by 1.
- @param a An AST
- *)
let push ( x : ast_vector ) ( a : ast ) =
Z3native.ast_vector_push (z3obj_gnc x) (z3obj_gno x) (z3obj_gno a)
- (**
- Translates all ASTs in the vector to .
- @param to_ctx A context
- @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))
+ ast_vector_of_ptr to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx))
- (** Retrieves a string representation of the vector. *)
let to_string ( x : ast_vector ) =
Z3native.ast_vector_to_string (z3obj_gnc x) (z3obj_gno x)
end
- (** Map from AST to AST *)
module ASTMap =
struct
+ type ast_map = z3_native_object
- let create ( ctx : context ) ( no : Z3native.ptr ) =
+ let astmap_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let res : ast_map = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = Z3native.ast_map_inc_ref ;
@@ -715,73 +272,36 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
-
- (** Checks whether the map contains the key .
- @param k An AST
- @return True if is a key in the map, false otherwise. *)
+
let contains ( x : ast_map ) ( key : ast ) =
Z3native.ast_map_contains (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key)
- (** Finds the value associated with the key .
-
- This function signs an error when is not a key in the map.
- @param k An AST
- *)
let find ( x : ast_map ) ( key : ast ) =
- create (z3obj_gc x) (Z3native.ast_map_find (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key))
+ ast_of_ptr (z3obj_gc x) (Z3native.ast_map_find (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key))
- (**
- Stores or replaces a new key/value pair in the map.
- @param k The key AST
- @param v The value AST
- *)
let insert ( x : ast_map ) ( key : ast ) ( value : ast) =
Z3native.ast_map_insert (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key) (z3obj_gno value)
- (**
- Erases the key from the map.
- @param k An AST
- *)
let erase ( x : ast_map ) ( key : ast ) =
Z3native.ast_map_erase (z3obj_gnc x) (z3obj_gno x) (z3obj_gno key)
- (** Removes all keys from the map. *)
let reset ( x : ast_map ) =
Z3native.ast_map_reset (z3obj_gnc x) (z3obj_gno x)
- (** The size of the map *)
let get_size ( x : ast_map ) =
Z3native.ast_map_size (z3obj_gnc x) (z3obj_gno x)
- (** The keys stored in the map. *)
let get_keys ( x : ast_map ) =
- ASTVector.create (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x))
+ ASTVector.ast_vector_of_ptr (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 ) =
Z3native.ast_map_to_string (z3obj_gnc x) (z3obj_gno x)
end
- (**
- The AST's hash code.
- @return A hash code
- *)
let get_hash_code ( x : ast ) = Z3native.get_ast_hash (z3obj_gnc x) (z3obj_gno x)
-
- (**
- A unique identifier for the AST (unique among all ASTs).
- *)
let get_id ( x : ast ) = Z3native.get_ast_id (z3obj_gnc x) (z3obj_gno x)
-
- (**
- The kind of the AST.
- *)
let get_ast_kind ( x : ast ) = (ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc x) (z3obj_gno x)))
- (**
- Indicates whether the AST is an Expr
- *)
let is_expr ( x : ast ) =
match get_ast_kind ( x : ast ) with
| APP_AST
@@ -790,117 +310,77 @@ struct
| VAR_AST -> true
| _ -> false
- (**
- Indicates whether the AST is a bound variable
- *)
let is_var ( x : ast ) = (get_ast_kind x) == VAR_AST
-
- (**
- Indicates whether the AST is a Quantifier
- *)
let is_quantifier ( x : ast ) = (get_ast_kind x) == QUANTIFIER_AST
-
-
- (**
- Indicates whether the AST is a Sort
- *)
let is_sort ( x : ast ) = (get_ast_kind x) == SORT_AST
-
- (**
- Indicates whether the AST is a FunctionDeclaration
- *)
let is_func_decl ( x : ast ) = (get_ast_kind x) == FUNC_DECL_AST
- (**
- A string representation of the AST.
- *)
let to_string ( x : ast ) = Z3native.ast_to_string (z3obj_gnc x) (z3obj_gno x)
-
- (**
- A string representation of the AST in s-expression notation.
- *)
let to_sexpr ( x : ast ) = Z3native.ast_to_string (z3obj_gnc x) (z3obj_gno x)
- (**
- Comparison operator.
- @param a An AST
- @param b An AST
- @return True if and are from the same context
- and represent the same sort; false otherwise.
- *)
+
let ( = ) ( a : ast ) ( b : ast ) = (a == b) ||
if (z3obj_gnc a) != (z3obj_gnc b) then
false
else
Z3native.is_eq_ast (z3obj_gnc a) (z3obj_gno a) (z3obj_gno b)
- (**
- Object Comparison.
- @param other Another ast
- @return Negative if the object should be sorted before , positive if after else zero.
- *)
let compare a b =
if (get_id a) < (get_id b) then -1 else
if (get_id a) > (get_id b) then 1 else
0
- (** Operator < *)
let ( < ) (a : ast) (b : ast) = (compare a b)
- (**
- Translates (copies) the AST to the Context .
- @param ctx A context
- @return A copy of the AST which is associated with
- *)
let translate ( x : ast ) ( to_ctx : context ) =
if (z3obj_gnc x) == (context_gno to_ctx) then
x
else
ast_of_ptr to_ctx (Z3native.translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx))
- (**
- Wraps an AST.
-
- This function is used for transitions between native and
- managed objects. Note that must be a
- native object obtained from Z3 (e.g., through )
- and that it must have a correct reference count (see e.g.,
- .
-
- @param nativeObject The native pointer to wrap.
- *)
- let wrap ( ctx : context ) ( ptr : Z3native.ptr ) =
- ast_of_ptr ctx ptr
-
- (**
- Unwraps an AST.
- This function is used for transitions between native and
- managed objects. It returns the native pointer to the AST. Note that
- AST objects are reference counted and unwrapping an AST disables automatic
- reference counting, i.e., all references to the IntPtr that is returned
- must be handled externally and through native calls (see e.g.,
- ).
-
- @param a The AST to unwrap.
- *)
+ let wrap ( ctx : context ) ( ptr : Z3native.ptr ) = ast_of_ptr ctx ptr
let unwrap_ast ( x : ast ) = (z3obj_gno x)
end
-(** The Sort module implements type information for ASTs *)
+open AST
+
+
module Sort =
struct
-
+ type sort = Sort of AST.ast
+ type uninterpreted_sort = UninterpretedSort of sort
+
+ 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 ast_of_sort s = match s with Sort(x) -> x
+ let sort_of_uninterpreted_sort s = match s with UninterpretedSort(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 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))
-
- (**
- Comparison operator.
- @param a A sort
- @param b A sort
- @return True if and are from the same context
- and represent the same sort; false otherwise.
- *)
+
let ( = ) : sort -> sort -> bool = fun a b ->
(a == b) ||
if (gnc a) != (gnc b) then
@@ -908,30 +388,13 @@ struct
else
(Z3native.is_eq_sort (gnc a) (gno a) (gno b))
- (**
- Returns a unique identifier for the sort.
- *)
+
let get_id ( x : sort ) = Z3native.get_sort_id (gnc x) (gno x)
-
- (**
- The kind of the sort.
- *)
let get_sort_kind ( x : sort ) = (sort_kind_of_int (Z3native.get_sort_kind (gnc x) (gno x)))
-
- (**
- The name of the sort
- *)
let get_name ( x : sort ) = (Symbol.create (gc x) (Z3native.get_sort_name (gnc x) (gno x)))
-
- (**
- A string representation of the sort.
- *)
let to_string ( x : sort ) = Z3native.sort_to_string (gnc x) (gno x)
-
- (**
- Create a new uninterpreted sort.
- *)
- let mk_uninterpreted ( ctx : context ) ( s : symbol ) =
+
+ let mk_uninterpreted ( ctx : context ) ( s : Symbol.symbol ) =
let res = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = Z3native.inc_ref ;
@@ -940,24 +403,76 @@ struct
(z3obj_create res) ;
UninterpretedSort(Sort(res))
- (**
- Create a new uninterpreted sort.
- *)
let mk_uninterpreted_s ( ctx : context ) ( s : string ) =
mk_uninterpreted ctx (Symbol.mk_string ( ctx : context ) s)
end
+open Sort
-(** Function declarations *)
-module FuncDecl =
-struct
- (**/**)
- let create_ndr ( ctx : context ) ( name : symbol ) ( domain : sort array ) ( range : sort ) =
+
+module rec FuncDecl :
+sig
+ type func_decl = FuncDecl of AST.ast
+ val ast_of_func_decl : FuncDecl.func_decl -> AST.ast
+ val func_decl_of_ptr : context -> Z3native.ptr -> func_decl
+ val gc : func_decl -> context
+ val gnc : func_decl -> Z3native.ptr
+ val gno : func_decl -> Z3native.ptr
+ module Parameter :
+ sig
+ 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
+
+ val get_kind : parameter -> Z3enums.parameter_kind
+ val get_int : parameter -> int
+ val get_float : parameter -> float
+ val get_symbol : parameter -> Symbol.symbol
+ val get_sort : parameter -> Sort.sort
+ val get_ast : parameter -> AST.ast
+ val get_func_decl : parameter -> func_decl
+ val get_rational : parameter -> string
+ end
+ val mk_func_decl : context -> Symbol.symbol -> Sort.sort array -> Sort.sort -> func_decl
+ val mk_func_decl_s : context -> string -> Sort.sort array -> Sort.sort -> func_decl
+ val mk_fresh_func_decl : context -> string -> Sort.sort array -> Sort.sort -> func_decl
+ val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl
+ val mk_const_decl_s : context -> string -> Sort.sort -> func_decl
+ val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl
+ val ( = ) : func_decl -> func_decl -> bool
+ val to_string : func_decl -> string
+ val get_id : func_decl -> int
+ val get_arity : func_decl -> int
+ val get_domain_size : func_decl -> int
+ val get_domain : func_decl -> Sort.sort array
+ val get_range : func_decl -> Sort.sort
+ val get_decl_kind : func_decl -> Z3enums.decl_kind
+ val get_name : func_decl -> Symbol.symbol
+ val get_num_parameters : func_decl -> int
+ val get_parameters : func_decl -> Parameter.parameter list
+ val apply : func_decl -> Expr.expr array -> Expr.expr
+end = struct
+ type func_decl = FuncDecl of AST.ast
+
+ 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 ast_of_func_decl f = match f with FuncDecl(x) -> x
+
+ let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort array ) ( range : sort ) =
let res = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = Z3native.inc_ref ;
dec_ref = Z3native.dec_ref } in
- let f x = (ptr_of_ast (ast_of_sort x)) in
+ let f x = (AST.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)
@@ -967,20 +482,26 @@ struct
m_n_obj = null ;
inc_ref = Z3native.inc_ref ;
dec_ref = Z3native.dec_ref } in
- let f x = (ptr_of_ast (ast_of_sort x)) in
+ let f x = (AST.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 gno ( x : func_decl ) = match x with FuncDecl(a) -> (z3obj_gno a)
- (** Parameters of Func_Decls *)
module Parameter =
- struct
- (** The kind of the 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
+
let get_kind ( x : parameter ) =
(match x with
| P_Int(_) -> PARAMETER_INT
@@ -991,188 +512,137 @@ struct
| P_Fdl(_) -> PARAMETER_FUNC_DECL
| P_Rat(_) -> PARAMETER_RATIONAL)
- (**The int value of the parameter.*)
let get_int ( x : parameter ) =
match x with
| P_Int(x) -> x
| _ -> raise (Z3native.Exception "parameter is not an int")
-
- (**The double value of the parameter.*)
+
let get_float ( x : parameter ) =
match x with
| P_Dbl(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a double")
-
- (**The Symbol value of the parameter.*)
+
let get_symbol ( x : parameter ) =
match x with
| P_Sym(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a symbol")
- (**The Sort value of the parameter.*)
let get_sort ( x : parameter ) =
match x with
| P_Srt(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a sort")
- (**The AST value of the parameter.*)
let get_ast ( x : parameter ) =
match x with
| P_Ast(x) -> x
| _ -> raise (Z3native.Exception "parameter is not an ast")
- (**The FunctionDeclaration value of the parameter.*)
let get_func_decl ( x : parameter ) =
match x with
| P_Fdl(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a func_decl")
- (**The rational string value of the parameter.*)
- let get_func_decl ( x : parameter ) =
+ let get_rational ( x : parameter ) =
match x with
| P_Rat(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a rational string")
end
- (**
- Creates a new function declaration.
- *)
- let mk_func_decl ( ctx : context ) ( name : symbol ) ( domain : sort array ) ( range : sort ) =
+ let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort array ) ( range : sort ) =
create_ndr ctx name domain range
- (**
- Creates a new function declaration.
- *)
let mk_func_decl_s ( ctx : context ) ( name : string ) ( domain : sort array ) ( range : sort ) =
mk_func_decl ctx (Symbol.mk_string ctx name) domain range
- (**
- Creates a fresh function declaration with a name prefixed with .
-
-
- *)
let mk_fresh_func_decl ( ctx : context ) ( prefix : string ) ( domain : sort array ) ( range : sort ) =
create_pdr ctx prefix domain range
- (**
- Creates a new constant function declaration.
- *)
- let mk_const_decl ( ctx : context ) ( name : symbol ) ( range : sort ) =
+ let mk_const_decl ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) =
create_ndr ctx name [||] range
- (**
- Creates a new constant function declaration.
- *)
let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : sort ) =
create_ndr ctx (Symbol.mk_string ctx name) [||] range
- (**
- Creates a fresh constant function declaration with a name prefixed with .
-
-
- *)
let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : sort ) =
create_pdr ctx prefix [||] range
- (**
- Comparison operator.
- @param a A func_decl
- @param b A func_decl
- @return True if and are from the same context
- and represent the same func_decl; false otherwise.
- *)
let ( = ) ( a : func_decl ) ( b : func_decl ) = (a == b) ||
if (gnc a) != (gnc b) then
false
else
(Z3native.is_eq_func_decl (gnc a) (gno a) (gno b))
- (**
- A string representations of the function declaration.
- *)
let to_string ( x : func_decl ) = Z3native.func_decl_to_string (gnc x) (gno x)
- (**
- Returns a unique identifier for the function declaration.
- *)
let get_id ( x : func_decl ) = Z3native.get_func_decl_id (gnc x) (gno x)
- (**
- The arity of the function declaration
- *)
let get_arity ( x : func_decl ) = Z3native.get_arity (gnc x) (gno x)
- (**
- The size of the domain of the function declaration
-
- *)
let get_domain_size ( x : func_decl ) = Z3native.get_domain_size (gnc x) (gno x)
- (**
- The domain of the function declaration
- *)
let get_domain ( x : func_decl ) =
let n = (get_domain_size x) in
let f i = sort_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_of_ptr (gc x) (Z3native.get_range (gnc x) (gno x))
- (**
- The kind of the function declaration.
- *)
let get_decl_kind ( x : func_decl ) = (decl_kind_of_int (Z3native.get_decl_kind (gnc x) (gno x)))
- (**
- The name of the function declaration
- *)
let get_name ( x : func_decl ) = (Symbol.create (gc x) (Z3native.get_decl_name (gnc x) (gno x)))
- (**
- The number of parameters of the function declaration
- *)
let get_num_parameters ( x : func_decl ) = (Z3native.get_decl_num_parameters (gnc x) (gno x))
- (**
- The parameters of the function declaration
- *)
let get_parameters ( x : func_decl ) =
let n = (get_num_parameters x) in
let f i = (match (parameter_kind_of_int (Z3native.get_decl_parameter_kind (gnc x) (gno x) i)) with
- | PARAMETER_INT -> P_Int (Z3native.get_decl_int_parameter (gnc x) (gno x) i)
- | PARAMETER_DOUBLE -> P_Dbl (Z3native.get_decl_double_parameter (gnc x) (gno x) i)
- | PARAMETER_SYMBOL-> P_Sym (Symbol.create (gc x) (Z3native.get_decl_symbol_parameter (gnc x) (gno x) i))
- | PARAMETER_SORT -> P_Srt (sort_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)
+ | 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_of_ptr (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i))
+ | PARAMETER_AST -> Parameter.P_Ast (AST.ast_of_ptr (gc x) (Z3native.get_decl_ast_parameter (gnc x) (gno x) i))
+ | PARAMETER_FUNC_DECL -> Parameter.P_Fdl (func_decl_of_ptr (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)
) in
mk_list f n
- (**
- Create expression that applies function to arguments.
- @param args The arguments
- *)
- let apply ( x : func_decl ) ( args : expr array ) = expr_of_func_app (gc x) x args
+ let apply ( x : func_decl ) ( args : Expr.expr array ) = Expr.expr_of_func_app (gc x) x args
end
-(**
- Parameter sets (of Solvers, Tactics, ...)
- A Params objects represents a configuration in the form of symbol/value pairs.
-*)
-module Params =
-struct
- (** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *)
+and Params :
+sig
+ type params = z3_native_object
+ module ParamDescrs :
+ sig
+ type param_descrs
+ val param_descrs_of_ptr : context -> Z3native.ptr -> param_descrs
+ val validate : param_descrs -> params -> unit
+ val get_kind : param_descrs -> Symbol.symbol -> Z3enums.param_kind
+ val get_names : param_descrs -> Symbol.symbol array
+ val get_size : param_descrs -> int
+ val to_string : param_descrs -> string
+ end
+ val add_bool : params -> Symbol.symbol -> bool -> unit
+ val add_int : params -> Symbol.symbol -> int -> unit
+ val add_double : params -> Symbol.symbol -> float -> unit
+ val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
+ val add_s_bool : params -> string -> bool -> unit
+ val add_s_int : params -> string -> int -> unit
+ val add_s_double : params -> string -> float -> unit
+ val add_s_symbol : params -> string -> Symbol.symbol -> unit
+ val mk_params : context -> params
+ val to_string : params -> string
+end = struct
+ type params = z3_native_object
+
module ParamDescrs =
- struct
-
- let create ( ctx : context ) ( no : Z3native.ptr ) =
+ struct
+ type param_descrs = z3_native_object
+
+ let param_descrs_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let res : param_descrs = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = Z3native.param_descrs_inc_ref ;
@@ -1180,79 +650,46 @@ 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 ) =
+ let get_kind ( x : param_descrs ) ( name : Symbol.symbol ) =
(param_kind_of_int (Z3native.param_descrs_get_kind (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name)))
- (** Retrieve all names of parameters. *)
let get_names ( x : param_descrs ) =
let n = Z3native.param_descrs_size (z3obj_gnc x) (z3obj_gno x) in
let f i = Symbol.create (z3obj_gc x) (Z3native.param_descrs_get_name (z3obj_gnc x) (z3obj_gno x) i) in
Array.init n f
- (** The size of the ParamDescrs. *)
- let get_size ( x : param_descrs ) = Z3native.param_descrs_size (z3obj_gnc x) (z3obj_gno x)
-
- (** Retrieves a string representation of the ParamDescrs. *)
+ let get_size ( x : param_descrs ) = Z3native.param_descrs_size (z3obj_gnc x) (z3obj_gno x)
let to_string ( x : param_descrs ) = Z3native.param_descrs_to_string (z3obj_gnc x) (z3obj_gno x)
end
- (**
- Adds a parameter setting.
- *)
- let add_bool ( x : params ) ( name : symbol ) ( value : bool ) =
+ let add_bool ( x : params ) ( name : Symbol.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 ) ( value : int ) =
+ let add_int ( x : params ) (name : Symbol.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 ) ( value : float ) =
+ let add_double ( x : params ) ( name : Symbol.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 ) ( value : symbol ) =
+ let add_symbol ( x : params ) ( name : Symbol.symbol ) ( value : Symbol.symbol ) =
Z3native.params_set_symbol (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) (Symbol.gno value)
- (**
- Adds a parameter setting.
- *)
let add_s_bool ( x : params ) ( name : string ) ( value : bool ) =
add_bool x (Symbol.mk_string (z3obj_gc x) name) value
- (**
- Adds a parameter setting.
- *)
let add_s_int ( x : params) ( name : string ) ( value : int ) =
add_int x (Symbol.mk_string (z3obj_gc x) name) value
- (**
- Adds a parameter setting.
- *)
let add_s_double ( x : params ) ( name : string ) ( value : float ) =
add_double x (Symbol.mk_string (z3obj_gc x) name) value
- (**
- Adds a parameter setting.
- *)
- let add_s_symbol ( x : params ) ( name : string ) ( value : symbol ) =
+
+ let add_s_symbol ( x : params ) ( name : string ) ( value : Symbol.symbol ) =
add_symbol x (Symbol.mk_string (z3obj_gc x) name) value
- (**
- Creates a new parameter set
- *)
let mk_params ( ctx : context ) =
let res : params = { m_ctx = ctx ;
m_n_obj = null ;
@@ -1262,21 +699,107 @@ struct
(z3obj_create res) ;
res
- (**
- A string representation of the parameter set.
- *)
let to_string ( x : params ) = Z3native.params_to_string (z3obj_gnc x) (z3obj_gno x)
end
(** General expressions (terms) *)
-module Expr =
-struct
+and Expr :
+sig
+ type expr = Expr of AST.ast
+ val expr_of_ptr : context -> Z3native.ptr -> expr
+ val c_of_expr : expr -> context
+ val nc_of_expr : expr -> Z3native.ptr
+ val ptr_of_expr : expr -> Z3native.ptr
+ val expr_aton : expr array -> Z3native.ptr array
+ val ast_of_expr : expr -> AST.ast
+ val expr_of_ast : AST.ast -> expr
+ val expr_of_func_app : context -> FuncDecl.func_decl -> expr array -> expr
+ val simplify : expr -> Params.params option -> expr
+ val get_simplify_help : context -> string
+ val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs
+ val get_func_decl : expr -> FuncDecl.func_decl
+ val get_bool_value : expr -> Z3enums.lbool
+ val get_num_args : expr -> int
+ val get_args : expr -> expr array
+ val update : expr -> expr array -> expr
+ val substitute : expr -> expr array -> expr array -> expr
+ val substitute_one : expr -> expr -> expr -> expr
+ val substitute_vars : expr -> expr array -> expr
+ val translate : expr -> context -> expr
+ val to_string : expr -> string
+ val is_numeral : expr -> bool
+ val is_well_sorted : expr -> bool
+ val get_sort : expr -> Sort.sort
+ val is_bool : expr -> bool
+ val is_const : expr -> bool
+ val is_true : expr -> bool
+ val is_false : expr -> bool
+ val is_eq : expr -> bool
+ val is_distinct : expr -> bool
+ val is_ite : expr -> bool
+ val is_and : expr -> bool
+ val is_or : expr -> bool
+ val is_iff : expr -> bool
+ val is_xor : expr -> bool
+ val is_not : expr -> bool
+ val is_implies : expr -> bool
+ val is_label : expr -> bool
+ val is_oeq : expr -> bool
+ val mk_const : context -> Symbol.symbol -> Sort.sort -> expr
+ val mk_const_s : context -> string -> Sort.sort -> expr
+ val mk_const_f : context -> FuncDecl.func_decl -> expr
+ val mk_fresh_const : context -> string -> Sort.sort -> expr
+ val mk_app : context -> FuncDecl.func_decl -> expr array -> expr
+ val mk_numeral_string : context -> string -> Sort.sort -> expr
+ val mk_numeral_int : context -> int -> Sort.sort -> expr
+end = struct
+ type expr = Expr of AST.ast
+
+ 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 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_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 ast_of_expr e = match e with Expr(a) -> a
+
+ let expr_aton ( a : expr array ) =
+ let f ( e : expr ) = match e with Expr(a) -> (AST.ptr_of_ast a) in
+ Array.map f a
+
+ let expr_of_func_app : context -> FuncDecl.func_decl -> expr array -> expr = fun ctx f args ->
+ match f with FuncDecl.FuncDecl(fa) ->
+ let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (Array.length args) (expr_aton args) in
+ expr_of_ptr ctx o
+
(**
Returns a simplified version of the expression.
@param p A set of parameters to configure the simplifier
*)
- let simplify ( x : expr ) ( p : params option ) = match p with
+ let simplify ( x : expr ) ( p : Params.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))
@@ -1290,12 +813,12 @@ struct
Retrieves parameter descriptions for simplifier.
*)
let get_simplify_parameter_descrs ( ctx : context ) =
- Params.ParamDescrs.create ctx (Z3native.simplify_get_param_descrs (context_gno ctx))
+ Params.ParamDescrs.param_descrs_of_ptr ctx (Z3native.simplify_get_param_descrs (context_gno ctx))
(**
The function declaration of the function that is applied in this expression.
*)
- let get_func_decl ( x : expr ) = func_decl_of_ptr (c_of_expr x) (Z3native.get_app_decl (nc_of_expr x) (ptr_of_expr x))
+ let get_func_decl ( x : expr ) = FuncDecl.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
@@ -1477,7 +1000,7 @@ struct
(**
Creates a new Constant of sort and named .
*)
- let mk_const ( ctx : context ) ( name : symbol ) ( range : sort ) =
+ let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) =
expr_of_ptr ctx (Z3native.mk_const (context_gno ctx) (Symbol.gno name) (Sort.gno range))
@@ -1492,8 +1015,7 @@ struct
Creates a constant from the func_decl .
@param f An expression of a 0-arity function
*)
- let mk_const_f ( ctx : context ) ( f : func_decl ) =
- expr_of_func_app ctx f [||]
+ let mk_const_f ( ctx : context ) ( f : FuncDecl.func_decl ) = Expr.expr_of_func_app ctx f [||]
(**
Creates a fresh constant of sort and a
@@ -1505,8 +1027,7 @@ struct
(**
Create a new function application.
*)
- let mk_app ( ctx : context ) ( f : func_decl ) ( args : expr array ) =
- expr_of_func_app ctx f args
+ let mk_app ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : expr array ) = expr_of_func_app ctx f args
(**
Create a numeral of a given sort.
@@ -1528,19 +1049,44 @@ struct
expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty))
end
+open FuncDecl
+open Expr
+
(** Boolean expressions *)
module Boolean =
-struct
+struct
+ type bool_sort = BoolSort of Sort.sort
+ type bool_expr = BoolExpr of Expr.expr
+
let bool_expr_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
- let a = (ast_of_ptr ctx no) in
- BoolExpr(Expr(a))
+ let a = (AST.ast_of_ptr ctx no) in
+ BoolExpr(Expr.Expr(a))
+
+ let bool_expr_of_expr e =
+ match e with Expr.Expr(a) ->
+ let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
+ let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
+ if (q != Z3enums.BOOL_SORT) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ BoolExpr(e)
let bool_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
BoolSort(sort_of_ptr ctx no)
- 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 sort_of_bool_sort s = match s with BoolSort(x) -> x
+
+ 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 expr_of_bool_expr e = match e with BoolExpr(x) -> x
+
+ let gc ( x : bool_expr ) = match x with BoolExpr(e) -> (Expr.c_of_expr e)
+ let gnc ( x : bool_expr ) = match x with BoolExpr(e) -> (Expr.nc_of_expr e)
+ let gno ( x : bool_expr ) = match x with BoolExpr(e) -> (Expr.ptr_of_expr e)
let mk_sort ( ctx : context ) =
BoolSort(sort_of_ptr ctx (Z3native.mk_bool_sort (context_gno ctx)))
@@ -1548,7 +1094,7 @@ struct
(**
Create a Boolean constant.
*)
- let mk_const ( ctx : context ) ( name : symbol ) =
+ let mk_const ( ctx : context ) ( name : Symbol.symbol ) =
let s = (match (mk_sort ctx) with BoolSort(q) -> q) in
BoolExpr(Expr.mk_const ctx name s)
@@ -1638,17 +1184,38 @@ end
(** Quantifier expressions *)
module Quantifier =
struct
+ type quantifier = Quantifier of expr
+
+ let expr_of_quantifier e = match e with Quantifier(x) -> x
+
+ let quantifier_of_expr e =
+ match e with Expr.Expr(a) ->
+ let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in
+ if (q != Z3enums.QUANTIFIER_AST) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ Quantifier(e)
+
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 Pattern = struct
+ module Pattern =
+ struct
+ type pattern = Pattern of ast
+
+ let ast_of_pattern e = match e with Pattern(x) -> x
+
+ let pattern_of_ast a =
+ (* CMW: Unchecked ok? *)
+ Pattern(a)
+
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)
@@ -1692,7 +1259,7 @@ struct
index.
*)
let get_index ( x : expr ) =
- if not (AST.is_var (match x with Expr(a) -> a)) then
+ if not (AST.is_var (match x with Expr.Expr(a) -> a)) then
raise (Z3native.Exception "Term is not a bound variable.")
else
Z3native.get_index_value (nc_of_expr x) (ptr_of_expr x)
@@ -1723,7 +1290,7 @@ struct
*)
let get_patterns ( x : quantifier ) =
let n = (get_num_patterns x) in
- let f i = Pattern (z3_native_object_of_ast_ptr (gc x) (Z3native.get_quantifier_pattern_ast (gnc x) (gno x) i)) in
+ let f i = Pattern.Pattern (z3_native_object_of_ast_ptr (gc x) (Z3native.get_quantifier_pattern_ast (gnc x) (gno x) i)) in
Array.init n f
(**
@@ -1736,7 +1303,7 @@ struct
*)
let get_no_patterns ( x : quantifier ) =
let n = (get_num_patterns x) 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
+ let f i = Pattern.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
(**
@@ -1781,7 +1348,7 @@ struct
if (Array.length terms) == 0 then
raise (Z3native.Exception "Cannot create a pattern from zero terms")
else
- Pattern(z3_native_object_of_ast_ptr ctx (Z3native.mk_pattern (context_gno ctx) (Array.length terms) (expr_aton terms)))
+ Pattern.Pattern(z3_native_object_of_ast_ptr ctx (Z3native.mk_pattern (context_gno ctx) (Array.length terms) (expr_aton terms)))
(**
Create a universal Quantifier.
@@ -1802,14 +1369,14 @@ struct
@param quantifierID optional symbol to track quantifier.
@param skolemID optional symbol to track skolem constants.
*)
- let mk_forall ( ctx : context ) ( sorts : sort array ) ( names : symbol array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
+ let mk_forall ( ctx : context ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
if (Array.length sorts) != (Array.length names) then
raise (Z3native.Exception "Number of sorts does not match number of names")
else if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
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))
+ (Array.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.map f patterns))
+ (Array.length sorts) (let f x = (AST.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
@@ -1817,21 +1384,21 @@ struct
(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 patterns) (let f x = (AST.ptr_of_ast (Pattern.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))
+ (Array.length sorts) (let f x = (AST.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 array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
+ let mk_forall_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
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))
+ (Array.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.map f patterns))
(ptr_of_expr body)))
else
Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const_ex (context_gno ctx) true
@@ -1839,7 +1406,7 @@ struct
(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 patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.map f patterns))
(Array.length nopatterns) (expr_aton nopatterns)
(ptr_of_expr body)))
@@ -1847,14 +1414,14 @@ struct
Create an existential Quantifier.
*)
- 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 ) =
+ let mk_exists ( ctx : context ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
if (Array.length sorts) != (Array.length names) then
raise (Z3native.Exception "Number of sorts does not match number of names")
else if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
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))
+ (Array.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.map f patterns))
+ (Array.length sorts) (let f x = (AST.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
@@ -1862,21 +1429,21 @@ struct
(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 patterns) (let f x = (AST.ptr_of_ast (Pattern.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))
+ (Array.length sorts) (let f x = (AST.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 array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
+ let mk_exists_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
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))
+ (Array.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.map f patterns))
(ptr_of_expr body)))
else
Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const_ex (context_gno ctx) false
@@ -1884,14 +1451,14 @@ struct
(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 patterns) (let f x = (AST.ptr_of_ast (Pattern.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 array ) ( names : symbol array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
+ let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
if (universal) then
(mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id)
else
@@ -1901,7 +1468,7 @@ struct
(**
Create a Quantifier.
*)
- let mk_quantifier ( ctx : context ) ( universal : bool ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : pattern array ) ( nopatterns : expr array ) ( quantifier_id : symbol option ) ( skolem_id : symbol option ) =
+ let mk_quantifier ( ctx : context ) ( universal : bool ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
if (universal) then
mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id
else
@@ -1911,14 +1478,35 @@ end
(** Functions to manipulate Array expressions *)
module Array_ =
struct
+ type array_sort = ArraySort of sort
+ type array_expr = ArrayExpr of expr
- let create_expr ( ctx : context ) ( no : Z3native.ptr ) =
+ let array_expr_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let e = (expr_of_ptr ctx no) in
ArrayExpr(e)
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
+ let array_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let s = (sort_of_ptr ctx no) in
- ArraySort(s)
+ ArraySort(s)
+
+ let sort_of_array_sort s = match s with ArraySort(x) -> x
+
+ 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 array_expr_of_expr e =
+ match e with Expr(a) ->
+ let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
+ let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
+ if (q != Z3enums.ARRAY_SORT) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ ArrayExpr(e)
+
+ let expr_of_array_expr e = match e with ArrayExpr(x) -> x
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)
@@ -1932,7 +1520,7 @@ struct
Create a new array 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))
+ array_sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range))
(**
Indicates whether the term is an array store.
@@ -1979,16 +1567,15 @@ struct
((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_of_ptr (sgc x) (Z3native.get_array_sort_domain (sgnc x) (sgno x))
+ let get_domain ( x : array_sort ) = 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_of_ptr (sgc x) (Z3native.get_array_sort_range (sgnc x) (sgno x))
-
+ let get_range ( x : array_sort ) = 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 ) ( domain : sort ) ( range : sort ) =
+ let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort ) ( range : sort ) =
ArrayExpr(Expr.mk_const ctx name (match (mk_sort ctx domain range) with ArraySort(s) -> s))
(**
@@ -2010,7 +1597,7 @@ struct
*)
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_expr_of_ptr ctx (Z3native.mk_select (context_gno ctx) (egno a) (ptr_of_expr i))
(**
Array update.
@@ -2029,7 +1616,7 @@ struct
*)
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))
+ array_expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (egno a) (ptr_of_expr i) (ptr_of_expr v))
(**
Create a constant array.
@@ -2040,7 +1627,7 @@ struct
*)
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))
+ array_expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (ptr_of_expr v))
(**
Maps f on the argument arrays.
@@ -2054,7 +1641,7 @@ struct
*)
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))
+ array_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.
@@ -2063,16 +1650,20 @@ struct
finite maps with a default range value.
*)
let mk_term_array ( ctx : context ) ( arg : array_expr ) =
- expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (egno arg))
+ array_expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (egno arg))
end
(** Functions to manipulate Set expressions *)
module Set =
struct
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
+ type set_sort = SetSort of sort
+
+ let set_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let s = (sort_of_ptr ctx no) in
SetSort(s)
+ let sort_of_set_sort s = match s with SetSort(x) -> x
+
(**
Indicates whether the term is set union
*)
@@ -2102,7 +1693,7 @@ struct
Create a set type.
*)
let mk_sort ( ctx : context ) ( ty : sort ) =
- create_sort ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty))
+ set_sort_of_ptr ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty))
(**
Create an empty set.
@@ -2169,14 +1760,24 @@ end
(** Functions to manipulate Finite Domain expressions *)
module FiniteDomain =
struct
+ type finite_domain_sort = FiniteDomainSort of sort
+
+ let sort_of_finite_domain_sort s = match s with FiniteDomainSort(x) -> x
+
+ 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 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 ) ( size : int ) =
+ let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) =
let s = (sort_of_ptr ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size)) in
FiniteDomainSort(s)
@@ -2210,15 +1811,24 @@ end
(** Functions to manipulate Relation expressions *)
module Relation =
struct
-
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
+ type relation_sort = RelationSort of sort
+
+ let sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let s = (sort_of_ptr ctx no) in
RelationSort(s)
+ let sort_of_relation_sort s = match s with RelationSort(x) -> x
+
+ 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 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.
@@ -2335,29 +1945,53 @@ struct
(** The sorts of the columns of the relation sort. *)
let get_column_sorts ( x : relation_sort ) =
let n = get_arity x in
- let f i = (create_sort (gc x) (Z3native.get_relation_column (gnc x) (gno x) i)) in
+ let f i = (sort_of_ptr (gc x) (Z3native.get_relation_column (gnc x) (gno x) i)) in
Array.init n f
end
(** Functions to manipulate Datatype expressions *)
module Datatype =
-struct
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
+struct
+ type datatype_sort = DatatypeSort of sort
+ type datatype_expr = DatatypeExpr of expr
+
+ let sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let s = (sort_of_ptr ctx no) in
DatatypeSort(s)
+ let sort_of_datatype_sort s = match s with DatatypeSort(x) -> x
+
+ 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 datatype_expr_of_expr e =
+ match e with Expr(a) ->
+ let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
+ let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
+ if (q != Z3enums.DATATYPE_SORT) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ DatatypeExpr(e)
+
+ let expr_of_datatype_expr e = match e with DatatypeExpr(x) -> x
+
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 =
struct
+ type constructor = z3_native_object
+
let _counts = Hashtbl.create 0
- let create ( ctx : context ) ( name : symbol ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array ) =
+ let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.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")
@@ -2366,11 +2000,11 @@ struct
raise (Z3native.Exception "Number of field names does not match number of sort refs")
else
let ptr = (Z3native.mk_constructor (context_gno ctx) (Symbol.gno name)
- (Symbol.gno recognizer)
- n
- (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
+ (Symbol.gno recognizer)
+ n
+ (let f x = (Symbol.gno x) in (Array.map f field_names))
+ (let f x = (AST.ptr_of_ast (ast_of_sort x)) in (Array.map f sorts))
+ sort_refs) in
let no : constructor = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = z3obj_nil_ref ;
@@ -2383,7 +2017,7 @@ struct
no
let get_n ( x : constructor ) = (Hashtbl.find _counts x)
-
+
let rec constructor_decl ( x : constructor ) =
let (a, _, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (Hashtbl.find _counts x)) in
func_decl_of_ptr (z3obj_gc x) a
@@ -2391,12 +2025,12 @@ struct
let rec tester_decl ( x : constructor ) =
let (_, b, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (Hashtbl.find _counts x)) in
func_decl_of_ptr (z3obj_gc x) b
-
+
let rec accessor_decls ( x : constructor ) =
let (_, _, c) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (Hashtbl.find _counts x)) in
let f y = func_decl_of_ptr (z3obj_gc x) y in
Array.map f c
-
+
(** The number of fields of the constructor. *)
let get_num_fields ( x : constructor ) = get_n x
@@ -2413,8 +2047,9 @@ struct
(** Constructor list objects *)
module ConstructorList =
struct
-
- let create ( ctx : context ) ( c : constructor array ) =
+ type constructor_list = z3_native_object
+
+ let create ( ctx : context ) ( c : Constructor.constructor array ) =
let res : constructor_list = { m_ctx = ctx ;
m_n_obj = null ;
inc_ref = z3obj_nil_ref ;
@@ -2438,7 +2073,7 @@ 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 ) ( recognizer : symbol ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array ) =
+ let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : sort array ) ( sort_refs : int array ) =
Constructor.create ctx name recognizer field_names sorts sort_refs
@@ -2452,22 +2087,22 @@ 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 ) ( field_names : symbol array ) ( sorts : sort array ) ( sort_refs : int array ) =
+ let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : sort 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 ) ( constructors : constructor array ) =
+ let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : Constructor.constructor array ) =
let f x = (z3obj_gno x) in
let (x,_) = (Z3native.mk_datatype (context_gno ctx) (Symbol.gno name) (Array.length constructors) (Array.map f constructors)) in
- create_sort ctx x
+ sort_of_ptr ctx x
(**
Create a new datatype sort.
*)
- let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : constructor array ) =
+ let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : Constructor.constructor array ) =
mk_sort ctx (Symbol.mk_string ctx name) constructors
(**
@@ -2475,17 +2110,17 @@ struct
@param names names of datatype sorts
@param c list of constructors, one list per sort.
*)
- let mk_sorts ( ctx : context ) ( names : symbol array ) ( c : constructor array array ) =
+ let mk_sorts ( ctx : context ) ( names : Symbol.symbol array ) ( c : Constructor.constructor array array ) =
let n = (Array.length names) in
- let f e = (ptr_of_ast (ConstructorList.create ctx e)) in
+ let f e = (AST.ptr_of_ast (ConstructorList.create ctx e)) in
let cla = (Array.map f c) 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
+ let g e = (sort_of_ptr ctx e) in
(Array.map g r)
(** Create mutually recursive data-types. *)
- let mk_sorts_s ( ctx : context ) ( names : string array ) ( c : constructor array array ) =
+ let mk_sorts_s ( ctx : context ) ( names : string array ) ( c : Constructor.constructor array array ) =
mk_sorts ctx
(
let f e = (Symbol.mk_string ctx e) in
@@ -2522,17 +2157,21 @@ end
(** Functions to manipulate Enumeration expressions *)
module Enumeration =
-struct
+struct
+ type enum_sort = EnumSort of sort
+
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 sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) ( cdecls : Z3native.z3_func_decl array ) ( tdecls : Z3native.z3_func_decl array ) =
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 sort_of_enum_sort s = match s with EnumSort(x) -> x
+
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)
@@ -2540,10 +2179,10 @@ struct
(**
Create a new enumeration sort.
*)
- let mk_sort ( ctx : context ) ( name : symbol ) ( enum_names : symbol array ) =
+ let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( enum_names : Symbol.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
+ sort_of_ptr ctx a b c
(**
Create a new enumeration sort.
@@ -2561,14 +2200,16 @@ end
(** Functions to manipulate List expressions *)
module List_ =
struct
+ type list_sort = ListSort of sort
+
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 sort_of_ptr ( 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_of_ptr ctx no) in
let res = ListSort(s) in
Hashtbl.add _nildecls res (func_decl_of_ptr ctx nildecl) ;
@@ -2578,16 +2219,18 @@ struct
Hashtbl.add _headdecls res (func_decl_of_ptr ctx headdecl) ;
Hashtbl.add _taildecls res (func_decl_of_ptr ctx taildecl) ;
res
+
+ let sort_of_list_sort s = match s with ListSort(x) -> x
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 ) ( elem_sort : sort ) =
+ let mk_sort ( ctx : context ) ( name : Symbol.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
+ sort_of_ptr ctx r a b c d e f
(** Create a new list sort. *)
let mk_list_s ( ctx : context ) (name : string) elem_sort =
@@ -2618,23 +2261,26 @@ end
(** Functions to manipulate Tuple expressions *)
module Tuple =
struct
-
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
+ type tuple_sort = TupleSort of sort
+
+ let sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
let s = (sort_of_ptr ctx no) in
TupleSort(s)
+ let sort_of_tuple_sort s = match s with TupleSort(x) -> x
+
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 ) ( field_names : symbol array ) ( field_sorts : sort array ) =
+ let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( field_names : Symbol.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
+ sort_of_ptr ctx r
(** The constructor function of the tuple. *)
let get_mk_decl ( x : tuple_sort ) =
@@ -2651,13 +2297,144 @@ struct
end
(** Functions to manipulate arithmetic expressions *)
-module Arithmetic =
-struct
-
- let create_expr ( ctx : context ) ( no : Z3native.ptr ) =
- arith_expr_of_expr (expr_of_ptr ctx no)
+module rec Arithmetic :
+sig
+ type arith_sort = ArithSort of Sort.sort
+ type arith_expr = ArithExpr of Expr.expr
+
+ val sort_of_arith_sort : arith_sort -> Sort.sort
+ val arith_sort_of_sort : Sort.sort -> arith_sort
+ val expr_of_arith_expr : arith_expr -> Expr.expr
+ val arith_expr_of_expr : Expr.expr -> arith_expr
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
+ module rec Integer :
+ sig
+ type int_sort = IntSort of arith_sort
+ type int_expr = IntExpr of arith_expr
+ type int_num = IntNum of int_expr
+
+ val int_expr_of_ptr : context -> Z3native.ptr -> int_expr
+ val int_num_of_ptr : context -> Z3native.ptr -> int_num
+
+ val arith_sort_of_int_sort : Integer.int_sort -> arith_sort
+ val int_sort_of_arith_sort : arith_sort -> int_sort
+ val arith_expr_of_int_expr : int_expr -> arith_expr
+ val int_expr_of_int_num : int_num -> int_expr
+ val int_expr_of_arith_expr : arith_expr -> int_expr
+ val int_num_of_int_expr : int_expr -> int_num
+
+ val mk_sort : context -> int_sort
+ val get_int : int_num -> int
+ val to_string : int_num -> string
+ val mk_int_const : context -> Symbol.symbol -> int_expr
+ val mk_int_const_s : context -> string -> int_expr
+ val mk_mod : context -> int_expr -> int_expr -> int_expr
+ val mk_rem : context -> int_expr -> int_expr -> int_expr
+ val mk_int_numeral_s : context -> string -> int_num
+ val mk_int_numeral_i : context -> int -> int_num
+ val mk_int2real : context -> int_expr -> Real.real_expr
+ val mk_int2bv : context -> int -> int_expr -> BitVector.bitvec_expr
+ end
+ and Real :
+ sig
+ type real_sort = RealSort of arith_sort
+ type real_expr = RealExpr of arith_expr
+ type rat_num = RatNum of real_expr
+
+ val real_expr_of_ptr : context -> Z3native.ptr -> real_expr
+ val rat_num_of_ptr : context -> Z3native.ptr -> rat_num
+
+ val arith_sort_of_real_sort : Arithmetic.Real.real_sort -> Arithmetic.arith_sort
+ val real_sort_of_arith_sort : Arithmetic.arith_sort -> Arithmetic.Real.real_sort
+ val arith_expr_of_real_expr : Arithmetic.Real.real_expr -> Arithmetic.arith_expr
+ val real_expr_of_rat_num : Arithmetic.Real.rat_num -> Arithmetic.Real.real_expr
+ val real_expr_of_arith_expr : Arithmetic.arith_expr -> Arithmetic.Real.real_expr
+ val rat_num_of_real_expr : Arithmetic.Real.real_expr -> Arithmetic.Real.rat_num
+
+ val mk_sort : context -> real_sort
+ val get_numerator : rat_num -> Integer.int_num
+ val get_denominator : rat_num -> Integer.int_num
+ val to_decimal_string : rat_num -> int -> string
+ val to_string : rat_num -> string
+ val mk_real_const : context -> Symbol.symbol -> real_expr
+ val mk_real_const_s : context -> string -> real_expr
+ val mk_numeral_nd : context -> int -> int -> rat_num
+ val mk_numeral_s : context -> string -> rat_num
+ val mk_numeral_i : context -> int -> rat_num
+ val mk_is_integer : context -> real_expr -> Boolean.bool_expr
+ val mk_real2int : context -> real_expr -> Integer.int_expr
+ end
+ and AlgebraicNumber :
+ sig
+ type algebraic_num = AlgebraicNum of arith_expr
+
+ val arith_expr_of_algebraic_num : algebraic_num -> arith_expr
+ val algebraic_num_of_arith_expr : arith_expr -> algebraic_num
+
+ val to_upper : algebraic_num -> int -> Real.rat_num
+ val to_lower : algebraic_num -> int -> Real.rat_num
+ val to_decimal_string : algebraic_num -> int -> string
+ val to_string : algebraic_num -> string
+ 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 -> arith_expr
+ val mk_mul : context -> arith_expr array -> arith_expr
+ val mk_sub : context -> arith_expr array -> arith_expr
+ val mk_unary_minus : context -> arith_expr -> arith_expr
+ val mk_div : context -> arith_expr -> arith_expr -> arith_expr
+ val mk_power : context -> arith_expr -> arith_expr -> arith_expr
+ val mk_lt : context -> arith_expr -> arith_expr -> Boolean.bool_expr
+ val mk_le : context -> arith_expr -> arith_expr -> Boolean.bool_expr
+ val mk_gt : context -> arith_expr -> arith_expr -> Boolean.bool_expr
+ val mk_ge : context -> arith_expr -> arith_expr -> Boolean.bool_expr
+end = struct
+ type arith_sort = ArithSort of sort
+ type arith_expr = ArithExpr of expr
+
+ let arith_expr_of_expr e =
+ match e with Expr(a) ->
+ let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
+ let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
+ if (q != Z3enums.INT_SORT && q != Z3enums.REAL_SORT) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ ArithExpr(e)
+
+ let arith_expr_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ arith_expr_of_expr (expr_of_ptr ctx no)
+
+ let sort_of_arith_sort s = match s with ArithSort(x) -> x
+ let expr_of_arith_expr e = match e with ArithExpr(x) -> x
+
+ 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 arith_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
arith_sort_of_sort (sort_of_ptr ctx no)
let sgc ( x : arith_sort ) = match (x) with ArithSort(Sort(s)) -> (z3obj_gc s)
@@ -2667,16 +2444,72 @@ struct
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)
- module Integer =
- struct
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
- int_sort_of_arith_sort (arith_sort_of_sort (sort_of_ptr ctx no))
-
- let create_expr ( ctx : context ) ( no : Z3native.ptr ) =
- int_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx no))
+ module rec Integer :
+ sig
+ type int_sort = IntSort of arith_sort
+ type int_expr = IntExpr of arith_expr
+ type int_num = IntNum of int_expr
- let create_num ( ctx : context ) ( no : Z3native.ptr ) =
- int_num_of_int_expr (create_expr ctx no)
+ val int_expr_of_ptr : context -> Z3native.ptr -> int_expr
+ val int_num_of_ptr : context -> Z3native.ptr -> int_num
+
+ val arith_sort_of_int_sort : Integer.int_sort -> arith_sort
+ val int_sort_of_arith_sort : arith_sort -> int_sort
+ val arith_expr_of_int_expr : int_expr -> arith_expr
+ val int_expr_of_int_num : int_num -> int_expr
+ val int_expr_of_arith_expr : arith_expr -> int_expr
+ val int_num_of_int_expr : int_expr -> int_num
+
+ val mk_sort : context -> int_sort
+ val get_int : int_num -> int
+ val to_string : int_num -> string
+ val mk_int_const : context -> Symbol.symbol -> int_expr
+ val mk_int_const_s : context -> string -> int_expr
+ val mk_mod : context -> int_expr -> int_expr -> int_expr
+ val mk_rem : context -> int_expr -> int_expr -> int_expr
+ val mk_int_numeral_s : context -> string -> int_num
+ val mk_int_numeral_i : context -> int -> int_num
+ val mk_int2real : context -> int_expr -> Real.real_expr
+ val mk_int2bv : context -> int -> int_expr -> BitVector.bitvec_expr
+ end = struct
+ type int_sort = IntSort of arith_sort
+ type int_expr = IntExpr of arith_expr
+ type int_num = IntNum of int_expr
+
+ let int_expr_of_arith_expr e =
+ match e with ArithExpr(Expr(a)) ->
+ let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
+ let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
+ if (q != Z3enums.INT_SORT) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ IntExpr(e)
+
+ let int_expr_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ int_expr_of_arith_expr (arith_expr_of_expr (Expr.expr_of_ptr ctx no))
+
+ let int_num_of_int_expr e =
+ match e with IntExpr(ArithExpr(Expr(a))) ->
+ if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ IntNum(e)
+
+ let int_num_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ int_num_of_int_expr (int_expr_of_ptr ctx no)
+
+ let arith_sort_of_int_sort s = match s with IntSort(x) -> x
+ let arith_expr_of_int_expr e = match e with IntExpr(x) -> x
+ let int_expr_of_int_num e = match e with IntNum(x) -> x
+
+ 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 int_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ int_sort_of_arith_sort (arith_sort_of_sort (Sort.sort_of_ptr 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)
@@ -2687,11 +2520,11 @@ 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 ) =
- create_sort ctx (Z3native.mk_int_sort (context_gno ctx))
+ int_sort_of_ptr ctx (Z3native.mk_int_sort (context_gno ctx))
(** Retrieve the int value. *)
let get_int ( x : int_num ) =
@@ -2705,7 +2538,7 @@ struct
(**
Creates an integer constant.
*)
- let mk_int_const ( ctx : context ) ( name : symbol ) =
+ let mk_int_const ( ctx : context ) ( name : Symbol.symbol ) =
IntExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with IntSort(ArithSort(s)) -> s)))
(**
@@ -2719,21 +2552,21 @@ struct
The arguments must have int type.
*)
let mk_mod ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) =
- expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (egno t1) (egno t2))
+ int_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 ) =
- expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (egno t1) (egno t2))
+ int_expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (egno t1) (egno t2))
(**
Create an integer numeral.
@param v A string representing the Term value in decimal notation.
*)
let mk_int_numeral_s ( ctx : context ) ( v : string ) =
- create_num ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx)))
+ int_num_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx)))
(**
Create an integer numeral.
@@ -2741,7 +2574,7 @@ struct
@return A Term with value and sort Integer
*)
let mk_int_numeral_i ( ctx : context ) ( v : int ) =
- create_num ctx (Z3native.mk_int (context_gno ctx) v (sgno (mk_sort ctx)))
+ int_num_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (sgno (mk_sort ctx)))
(**
Coerce an integer to a real.
@@ -2754,7 +2587,7 @@ struct
The argument must be of integer sort.
*)
let mk_int2real ( ctx : context ) ( t : int_expr ) =
- real_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_int2real (context_gno ctx) (egno t))))
+ Real.real_expr_of_arith_expr (arith_expr_of_expr (Expr.expr_of_ptr ctx (Z3native.mk_int2real (context_gno ctx) (egno t))))
(**
Create an bit bit-vector from the integer argument .
@@ -2767,19 +2600,76 @@ struct
The argument must be of integer sort.
*)
let mk_int2bv ( ctx : context ) ( n : int ) ( t : int_expr ) =
- bitvec_expr_of_expr (expr_of_ptr ctx (Z3native.mk_int2bv (context_gno ctx) n (egno t)))
+ BitVector.bitvec_expr_of_expr (Expr.expr_of_ptr ctx (Z3native.mk_int2bv (context_gno ctx) n (egno t)))
end
- module Real =
- struct
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
- real_sort_of_arith_sort (arith_sort_of_sort (sort_of_ptr ctx no))
-
- let create_expr ( ctx : context ) ( no : Z3native.ptr ) =
- real_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx no))
+ and Real :
+ sig
+ type real_sort = RealSort of arith_sort
+ type real_expr = RealExpr of arith_expr
+ type rat_num = RatNum of real_expr
- let create_num ( ctx : context ) ( no : Z3native.ptr ) =
- rat_num_of_real_expr (create_expr ctx no)
+ val real_expr_of_ptr : context -> Z3native.ptr -> real_expr
+ val rat_num_of_ptr : context -> Z3native.ptr -> rat_num
+
+ val arith_sort_of_real_sort : real_sort -> arith_sort
+ val real_sort_of_arith_sort : arith_sort -> real_sort
+ val arith_expr_of_real_expr : real_expr -> arith_expr
+ val real_expr_of_rat_num : rat_num -> real_expr
+ val real_expr_of_arith_expr : arith_expr -> real_expr
+ val rat_num_of_real_expr : real_expr -> rat_num
+
+ val mk_sort : context -> real_sort
+ val get_numerator : rat_num -> Integer.int_num
+ val get_denominator : rat_num -> Integer.int_num
+ val to_decimal_string : rat_num -> int -> string
+ val to_string : rat_num -> string
+ val mk_real_const : context -> Symbol.symbol -> real_expr
+ val mk_real_const_s : context -> string -> real_expr
+ val mk_numeral_nd : context -> int -> int -> rat_num
+ val mk_numeral_s : context -> string -> rat_num
+ val mk_numeral_i : context -> int -> rat_num
+ val mk_is_integer : context -> real_expr -> Boolean.bool_expr
+ val mk_real2int : context -> real_expr -> Integer.int_expr
+ end = struct
+ type real_sort = RealSort of arith_sort
+ type real_expr = RealExpr of arith_expr
+ type rat_num = RatNum of real_expr
+
+ let arith_sort_of_real_sort s = match s with RealSort(x) -> x
+ let arith_expr_of_real_expr e = match e with RealExpr(x) -> x
+ let real_expr_of_rat_num e = match e with RatNum(x) -> x
+
+ let real_expr_of_arith_expr e =
+ match e with ArithExpr(Expr(a)) ->
+ let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
+ let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
+ if (q != Z3enums.REAL_SORT) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ RealExpr(e)
+
+ let real_expr_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ real_expr_of_arith_expr (arith_expr_of_expr (Expr.expr_of_ptr ctx no))
+
+ let rat_num_of_real_expr e =
+ match e with RealExpr(ArithExpr(Expr(a))) ->
+ if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ RatNum(e)
+
+ let rat_num_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ rat_num_of_real_expr (real_expr_of_ptr ctx no)
+
+ 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)
+
+ let real_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ real_sort_of_arith_sort (arith_sort_of_sort (sort_of_ptr 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)
@@ -2790,19 +2680,19 @@ 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 ) =
- create_sort ctx (Z3native.mk_real_sort (context_gno ctx))
+ real_sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx))
(** The numerator of a rational numeral. *)
let get_numerator ( x : rat_num ) =
- Integer.create_num (ngc x) (Z3native.get_numerator (ngnc x) (ngno x))
+ Integer.int_num_of_ptr (ngc x) (Z3native.get_numerator (ngnc x) (ngno x))
(** The denominator of a rational numeral. *)
let get_denominator ( x : rat_num ) =
- Integer.create_num (ngc x) (Z3native.get_denominator (ngnc x) (ngno x))
+ Integer.int_num_of_ptr (ngc x) (Z3native.get_denominator (ngnc x) (ngno x))
(** Returns a string representation in decimal notation.
The result has at most decimal places.*)
@@ -2813,7 +2703,7 @@ 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 ) =
+ let mk_real_const ( ctx : context ) ( name : Symbol.symbol ) =
RealExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with RealSort(ArithSort(s)) -> s)))
(** Creates a real constant. *)
@@ -2832,7 +2722,7 @@ struct
if (den == 0) then
raise (Z3native.Exception "Denominator is zero")
else
- create_num ctx (Z3native.mk_real (context_gno ctx) num den)
+ rat_num_of_ptr ctx (Z3native.mk_real (context_gno ctx) num den)
(**
Create a real numeral.
@@ -2840,7 +2730,7 @@ struct
@return A Term with value and sort Real
*)
let mk_numeral_s ( ctx : context ) ( v : string ) =
- create_num ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx)))
+ rat_num_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx)))
(**
Create a real numeral.
@@ -2849,11 +2739,11 @@ struct
@return A Term with value and sort Real
*)
let mk_numeral_i ( ctx : context ) ( v : int ) =
- create_num ctx (Z3native.mk_int (context_gno ctx) v (sgno (mk_sort ctx)))
+ rat_num_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (sgno (mk_sort ctx)))
(** Creates an expression that checks whether a real number is an integer. *)
let mk_is_integer ( ctx : context ) ( t : real_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (egno t)))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (egno t)))
(**
Coerce a real to an integer.
@@ -2863,18 +2753,39 @@ struct
The argument must be of real sort.
*)
let mk_real2int ( ctx : context ) ( t : real_expr ) =
- int_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (egno t))))
+ Integer.int_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (egno t))))
end
- module AlgebraicNumber =
- struct
- let create_num ( ctx : context ) ( no : Z3native.ptr ) =
- algebraic_num_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx no))
+ and AlgebraicNumber :
+ sig
+ type algebraic_num = AlgebraicNum of arith_expr
+ val arith_expr_of_algebraic_num : algebraic_num -> arith_expr
+ val algebraic_num_of_arith_expr : arith_expr -> algebraic_num
+
+ val to_upper : algebraic_num -> int -> Real.rat_num
+ val to_lower : algebraic_num -> int -> Real.rat_num
+ val to_decimal_string : algebraic_num -> int -> string
+ val to_string : algebraic_num -> string
+ end = struct
+ type algebraic_num = AlgebraicNum of arith_expr
+
+ let arith_expr_of_algebraic_num e = match e with AlgebraicNum(x) -> x
+
+ let algebraic_num_of_arith_expr e =
+ match e with ArithExpr(Expr(a)) ->
+ if (not (Z3native.is_algebraic_number (z3obj_gnc a) (z3obj_gno a))) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ AlgebraicNum(e)
+
+ let algebraic_num_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ 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.
@@ -2884,7 +2795,7 @@ struct
@return A numeral Expr of sort Real
*)
let to_upper ( x : algebraic_num ) ( precision : int ) =
- Real.create_num (ngc x) (Z3native.get_algebraic_number_upper (ngnc x) (ngno x) precision)
+ Real.rat_num_of_ptr (ngc x) (Z3native.get_algebraic_number_upper (ngnc x) (ngno x) precision)
(**
Return a lower bound for the given real algebraic number.
@@ -2894,7 +2805,7 @@ struct
@return A numeral Expr of sort Real
*)
let to_lower ( x : algebraic_num ) precision =
- Real.create_num (ngc x) (Z3native.get_algebraic_number_lower (ngnc x) (ngno x) precision)
+ Real.rat_num_of_ptr (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.*)
@@ -3056,38 +2967,186 @@ struct
Create an expression representing t1 < t2
*)
let mk_lt ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_lt (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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 ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_le (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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 ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_gt (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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 ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_ge (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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 *)
-module BitVector =
-struct
- let create_sort ( ctx : context ) ( no : Z3native.ptr ) =
+and BitVector :
+sig
+ type bitvec_sort = BitVecSort of Sort.sort
+ type bitvec_expr = BitVecExpr of Expr.expr
+ type bitvec_num = BitVecNum of bitvec_expr
+
+ val sort_of_bitvec_sort : BitVector.bitvec_sort -> Sort.sort
+ val bitvec_sort_of_sort : Sort.sort -> BitVector.bitvec_sort
+ val expr_of_bitvec_expr : BitVector.bitvec_expr -> Expr.expr
+ val bitvec_expr_of_bitvec_num : BitVector.bitvec_num -> BitVector.bitvec_expr
+ val bitvec_expr_of_expr : Expr.expr -> BitVector.bitvec_expr
+ val bitvec_num_of_bitvec_expr : BitVector.bitvec_expr -> BitVector.bitvec_num
+
+ val mk_sort : context -> int -> bitvec_sort
+ val is_bv : Expr.expr -> bool
+ val is_bv_numeral : Expr.expr -> bool
+ val is_bv_bit1 : Expr.expr -> bool
+ val is_bv_bit0 : Expr.expr -> bool
+ val is_bv_uminus : Expr.expr -> bool
+ val is_bv_add : Expr.expr -> bool
+ val is_bv_sub : Expr.expr -> bool
+ val is_bv_mul : Expr.expr -> bool
+ val is_bv_sdiv : Expr.expr -> bool
+ val is_bv_udiv : Expr.expr -> bool
+ val is_bv_SRem : Expr.expr -> bool
+ val is_bv_urem : Expr.expr -> bool
+ val is_bv_smod : Expr.expr -> bool
+ val is_bv_sdiv0 : Expr.expr -> bool
+ val is_bv_udiv0 : Expr.expr -> bool
+ val is_bv_srem0 : Expr.expr -> bool
+ val is_bv_urem0 : Expr.expr -> bool
+ val is_bv_smod0 : Expr.expr -> bool
+ val is_bv_ule : Expr.expr -> bool
+ val is_bv_sle : Expr.expr -> bool
+ val is_bv_uge : Expr.expr -> bool
+ val is_bv_sge : Expr.expr -> bool
+ val is_bv_ult : Expr.expr -> bool
+ val is_bv_slt : Expr.expr -> bool
+ val is_bv_ugt : Expr.expr -> bool
+ val is_bv_sgt : Expr.expr -> bool
+ val is_bv_and : Expr.expr -> bool
+ val is_bv_or : Expr.expr -> bool
+ val is_bv_not : Expr.expr -> bool
+ val is_bv_xor : Expr.expr -> bool
+ val is_bv_nand : Expr.expr -> bool
+ val is_bv_nor : Expr.expr -> bool
+ val is_bv_xnor : Expr.expr -> bool
+ val is_bv_concat : Expr.expr -> bool
+ val is_bv_signextension : Expr.expr -> bool
+ val is_bv_zeroextension : Expr.expr -> bool
+ val is_bv_extract : Expr.expr -> bool
+ val is_bv_repeat : Expr.expr -> bool
+ val is_bv_reduceor : Expr.expr -> bool
+ val is_bv_reduceand : Expr.expr -> bool
+ val is_bv_comp : Expr.expr -> bool
+ val is_bv_shiftleft : Expr.expr -> bool
+ val is_bv_shiftrightlogical : Expr.expr -> bool
+ val is_bv_shiftrightarithmetic : Expr.expr -> bool
+ val is_bv_rotateleft : Expr.expr -> bool
+ val is_bv_rotateright : Expr.expr -> bool
+ val is_bv_rotateleftextended : Expr.expr -> bool
+ val is_bv_rotaterightextended : Expr.expr -> bool
+ val is_int_to_bv : Expr.expr -> bool
+ val is_bv_to_int : Expr.expr -> bool
+ val is_bv_carry : Expr.expr -> bool
+ val is_bv_xor3 : Expr.expr -> bool
+ val get_size : bitvec_sort -> int
+ val get_int : bitvec_num -> int
+ val to_string : bitvec_num -> string
+ val mk_const : context -> Symbol.symbol -> int -> bitvec_expr
+ val mk_const_s : context -> string -> int -> bitvec_expr
+ val mk_not : context -> bitvec_expr -> Expr.expr
+ val mk_redand : context -> bitvec_expr -> Expr.expr
+ val mk_redor : context -> bitvec_expr -> Expr.expr
+ val mk_and : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_or : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_xor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_nand : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_nor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_xnor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_neg : context -> bitvec_expr -> bitvec_expr
+ val mk_add : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_sub : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_mul : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_udiv : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_sdiv : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_urem : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_srem : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_smod : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_ult : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_slt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_ule : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sle : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_uge : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sge : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_ugt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sgt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_concat : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_extract : context -> int -> int -> bitvec_expr -> bitvec_expr
+ val mk_sign_ext : context -> int -> bitvec_expr -> bitvec_expr
+ val mk_zero_ext : context -> int -> bitvec_expr -> bitvec_expr
+ val mk_repeat : context -> int -> bitvec_expr -> bitvec_expr
+ val mk_shl : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_lshr : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_ashr : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_rotate_left : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_rotate_right : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_bv2int : context -> bitvec_expr -> bool -> Arithmetic.Integer.int_expr
+ val mk_add_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr
+ val mk_add_no_underflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sub_no_overflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sub_no_underflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr
+ val mk_sdiv_no_overflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_neg_no_overflow : context -> bitvec_expr -> Boolean.bool_expr
+ val mk_mul_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr
+ val mk_mul_no_underflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_numeral : context -> string -> int -> bitvec_num
+end = struct
+ type bitvec_sort = BitVecSort of sort
+ type bitvec_expr = BitVecExpr of expr
+ type bitvec_num = BitVecNum of bitvec_expr
+
+ let sort_of_bitvec_sort s = match s with BitVecSort(x) -> x
+
+ 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 bitvec_sort_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
bitvec_sort_of_sort (sort_of_ptr ctx no)
- let create_expr ( ctx : context ) ( no : Z3native.ptr ) =
+ let bitvec_expr_of_expr e =
+ match e with Expr(a) ->
+ let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
+ let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
+ if (q != Z3enums.BV_SORT) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ BitVecExpr(e)
+
+ let bitvec_expr_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
bitvec_expr_of_expr (expr_of_ptr ctx no)
- let create_num ( ctx : context ) ( no : Z3native.ptr ) =
- bitvec_num_of_bitvec_expr (create_expr ctx no)
+ let bitvec_num_of_bitvec_expr e =
+ match e with BitVecExpr(Expr(a)) ->
+ if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
+ raise (Z3native.Exception "Invalid coercion")
+ else
+ BitVecNum(e)
+
+ let bitvec_num_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
+ bitvec_num_of_bitvec_expr (bitvec_expr_of_expr (expr_of_ptr ctx no))
+
+ let expr_of_bitvec_expr e = match e with BitVecExpr(x) -> x
+ let bitvec_expr_of_bitvec_num e = match e with BitVecNum(x) -> x
+
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)
@@ -3098,13 +3157,13 @@ struct
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.
*)
let mk_sort ( ctx : context ) size =
- create_sort ctx (Z3native.mk_bv_sort (context_gno ctx) size)
+ bitvec_sort_of_ptr ctx (Z3native.mk_bv_sort (context_gno ctx) size)
(**
Indicates whether the terms is of bit-vector sort.
@@ -3391,8 +3450,8 @@ struct
(**
Creates a bit-vector constant.
*)
- let mk_const ( ctx : context ) ( name : symbol ) ( size : int ) =
- BitVecExpr(Expr.mk_const ctx name (match (mk_sort ctx size) with BitVecSort(s) -> s))
+ let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) =
+ BitVecExpr(Expr.mk_const ctx name (match (BitVector.mk_sort ctx size) with BitVecSort(s) -> s))
(**
Creates a bit-vector constant.
@@ -3426,70 +3485,70 @@ struct
The arguments must have a bit-vector sort.
*)
let mk_and ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvand (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvor (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvxor (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvnand (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvnor (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvxnor (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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) =
- expr_of_ptr ctx (Z3native.mk_bvneg (context_gno ctx) (egno t))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvadd (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvsub (context_gno ctx) (egno t1) (egno t2))
+ bitvec_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 ) =
- expr_of_ptr ctx (Z3native.mk_bvmul (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvmul (context_gno ctx) (egno t1) (egno t2))
(**
Unsigned division.
@@ -3501,7 +3560,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_udiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvudiv (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvudiv (context_gno ctx) (egno t1) (egno t2))
(**
Signed division.
@@ -3516,7 +3575,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_sdiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvsdiv (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvsdiv (context_gno ctx) (egno t1) (egno t2))
(**
Unsigned remainder.
@@ -3526,7 +3585,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_urem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvurem (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvurem (context_gno ctx) (egno t1) (egno t2))
(**
Signed remainder.
@@ -3538,7 +3597,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_srem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvsrem (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvsrem (context_gno ctx) (egno t1) (egno t2))
(**
Two's complement signed remainder (sign follows divisor).
@@ -3547,7 +3606,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_smod ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvsmod (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvsmod (context_gno ctx) (egno t1) (egno t2))
(**
Unsigned less-than
@@ -3555,7 +3614,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_ult ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvult (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvult (context_gno ctx) (egno t1) (egno t2)))
(**
Two's complement signed less-than
@@ -3563,7 +3622,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_slt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvslt (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvslt (context_gno ctx) (egno t1) (egno t2)))
(**
Unsigned less-than or equal to.
@@ -3571,7 +3630,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_ule ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvule (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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.
@@ -3579,7 +3638,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_sle ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsle (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsle (context_gno ctx) (egno t1) (egno t2)))
(**
Unsigned greater than or equal to.
@@ -3587,7 +3646,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_uge ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvuge (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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.
@@ -3595,7 +3654,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_sge ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (egno t1) (egno t2)))
(**
Unsigned greater-than.
@@ -3603,7 +3662,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_ugt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (egno t1) (egno t2)))
(**
Two's complement signed greater-than.
@@ -3611,7 +3670,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_sgt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (egno t1) (egno t2)))
(**
Bit-vector concatenation.
@@ -3622,7 +3681,7 @@ struct
is the size of t1 (t2).
*)
let mk_concat ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (egno t1) (egno t2))
(**
Bit-vector extraction.
@@ -3633,7 +3692,7 @@ struct
The argument must have a bit-vector sort.
*)
let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_extract (context_gno ctx) high low (egno t))
+ bitvec_expr_of_ptr ctx (Z3native.mk_extract (context_gno ctx) high low (egno t))
(**
Bit-vector sign extension.
@@ -3643,7 +3702,7 @@ struct
The argument must have a bit-vector sort.
*)
let mk_sign_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_sign_ext (context_gno ctx) i (egno t))
+ bitvec_expr_of_ptr ctx (Z3native.mk_sign_ext (context_gno ctx) i (egno t))
(**
Bit-vector zero extension.
@@ -3654,7 +3713,7 @@ struct
The argument must have a bit-vector sort.
*)
let mk_zero_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_zero_ext (context_gno ctx) i (egno t))
+ bitvec_expr_of_ptr ctx (Z3native.mk_zero_ext (context_gno ctx) i (egno t))
(**
Bit-vector repetition.
@@ -3662,7 +3721,7 @@ struct
The argument must have a bit-vector sort.
*)
let mk_repeat ( ctx : context ) ( i : int ) ( t : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (egno t))
+ bitvec_expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (egno t))
(**
Shift left.
@@ -3677,8 +3736,8 @@ struct
The arguments must have a bit-vector sort.
*)
let mk_shl ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (egno t1) (egno t2))
-
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (egno t1) (egno t2))
+
(**
Logical shift right
@@ -3692,7 +3751,7 @@ struct
The arguments must have a bit-vector sort.
*)
let mk_lshr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (egno t1) (egno t2))
(**
Arithmetic shift right
@@ -3708,7 +3767,7 @@ struct
The arguments must have a bit-vector sort.
*)
let mk_ashr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_bvashr (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_bvashr (context_gno ctx) (egno t1) (egno t2))
(**
Rotate Left.
@@ -3717,7 +3776,7 @@ struct
The argument must have a bit-vector sort.
*)
let mk_rotate_left ( ctx : context ) ( i : int ) ( t : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_rotate_left (context_gno ctx) i (egno t))
+ bitvec_expr_of_ptr ctx (Z3native.mk_rotate_left (context_gno ctx) i (egno t))
(**
Rotate Right.
@@ -3726,7 +3785,7 @@ struct
The argument must have a bit-vector sort.
*)
let mk_rotate_right ( ctx : context ) ( i : int ) ( t : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_rotate_right (context_gno ctx) i (egno t))
+ bitvec_expr_of_ptr ctx (Z3native.mk_rotate_right (context_gno ctx) i (egno t))
(**
Rotate Left.
@@ -3735,7 +3794,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_rotate_left ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (egno t1) (egno t2))
(**
Rotate Right.
@@ -3745,7 +3804,7 @@ struct
The arguments must have the same bit-vector sort.
*)
let mk_rotate_right ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (egno t1) (egno t2))
+ bitvec_expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (egno t1) (egno t2))
(**
Create an integer from the bit-vector argument .
@@ -3763,7 +3822,7 @@ struct
The argument must be of bit-vector sort.
*)
let mk_bv2int ( ctx : context ) ( t : bitvec_expr ) ( signed : bool ) =
- Arithmetic.Integer.create_expr ctx (Z3native.mk_bv2int (context_gno ctx) (egno t) signed)
+ Arithmetic.Integer.int_expr_of_ptr ctx (Z3native.mk_bv2int (context_gno ctx) (egno t) signed)
(**
Create a predicate that checks that the bit-wise addition does not overflow.
@@ -3771,7 +3830,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_add_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (egno t1) (egno t2) signed))
+ Boolean.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.
@@ -3779,7 +3838,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_add_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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.
@@ -3787,7 +3846,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_sub_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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.
@@ -3795,7 +3854,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_sub_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (egno t1) (egno t2) signed))
+ Boolean.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.
@@ -3803,7 +3862,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_sdiv_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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.
@@ -3811,7 +3870,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_neg_no_overflow ( ctx : context ) ( t : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (egno t)))
+ Boolean.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.
@@ -3819,7 +3878,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_mul_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (egno t1) (egno t2) signed))
+ Boolean.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.
@@ -3827,7 +3886,7 @@ struct
The arguments must be of bit-vector sort.
*)
let mk_mul_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) =
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (egno t1) (egno t2)))
+ Boolean.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.
@@ -3836,7 +3895,7 @@ struct
@param size the size of the bit-vector
*)
let mk_numeral ( ctx : context ) ( v : string ) ( size : int) =
- create_num ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx size)))
+ bitvec_num_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (BitVector.mk_sort ctx size)))
end
(** Functions to manipulate proof expressions *)
@@ -4321,7 +4380,8 @@ end
tactics and solvers. *)
module Goal =
struct
-
+ type goal = z3_native_object
+
let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : goal = { m_ctx = ctx ;
m_n_obj = null ;
@@ -4330,7 +4390,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
(** The precision of the goal.
@@ -4359,7 +4419,7 @@ struct
(** Adds the constraints to the given goal. *)
(* CMW: assert seems to be a keyword. *)
- let assert_ ( x : goal ) ( constraints : bool_expr array ) =
+ let assert_ ( x : goal ) ( constraints : Boolean.bool_expr array ) =
let f e = Z3native.goal_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e) in
ignore (Array.map f constraints) ;
()
@@ -4381,7 +4441,7 @@ struct
(** The formulas in the goal. *)
let get_formulas ( x : goal ) =
let n = get_size x in
- let f i = (bool_expr_of_expr (expr_of_ptr (z3obj_gc x)
+ let f i = (Boolean.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
@@ -4401,7 +4461,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 option ) =
+ let simplify ( x : goal ) ( p : Params.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
@@ -4441,7 +4501,8 @@ 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 ;
@@ -4450,7 +4511,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
(** Function interpretations
@@ -4459,7 +4520,8 @@ 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 ;
@@ -4468,7 +4530,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
(** Function interpretations entries
@@ -4476,7 +4538,8 @@ struct
*)
module FuncEntry =
struct
-
+ type func_entry = z3_native_object
+
let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : func_entry = { m_ctx = ctx ;
m_n_obj = null ;
@@ -4485,7 +4548,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
(**
Return the (symbolic) value of this entry.
@@ -4677,7 +4740,7 @@ struct
An array of expressions, where each is an element of the universe of
*)
let sort_universe ( x : model ) ( s : sort ) =
- let n_univ = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in
+ let n_univ = AST.ASTVector.ast_vector_of_ptr (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
@@ -4699,7 +4762,8 @@ 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 ;
@@ -4708,14 +4772,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) =
+ let apply ( x : probe ) ( g : Goal.goal ) =
Z3native.probe_apply (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g)
(**
@@ -4820,7 +4884,8 @@ end
*)
module Tactic =
struct
-
+ type tactic = z3_native_object
+
let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : tactic = { m_ctx = ctx ;
m_n_obj = null ;
@@ -4829,7 +4894,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
(** Tactic application results
@@ -4837,7 +4902,8 @@ 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 ;
@@ -4846,7 +4912,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
(** The number of Subgoals. *)
let get_num_subgoals ( x : apply_result ) =
@@ -4866,7 +4932,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 ) =
+ let convert_model ( x : apply_result ) ( i : int ) ( m : Model.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. *)
@@ -4878,10 +4944,10 @@ struct
(** Retrieves parameter descriptions for Tactics. *)
let get_param_descrs ( x : tactic ) =
- Params.ParamDescrs.create (z3obj_gc x) (Z3native.tactic_get_param_descrs (z3obj_gnc x) (z3obj_gno x))
+ Params.ParamDescrs.param_descrs_of_ptr (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 ) ( p : params option ) =
+ let apply ( x : tactic ) ( g : Goal.goal ) ( p : Params.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)))
@@ -4949,14 +5015,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 ) ( t : tactic ) =
+ let when_ ( ctx : context ) ( p : Probe.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 ) ( t1 : tactic ) ( t2 : tactic ) =
+ let cond ( ctx : context ) ( p : Probe.probe ) ( t1 : tactic ) ( t2 : tactic ) =
create ctx (Z3native.tactic_cond (context_gno ctx) (z3obj_gno p) (z3obj_gno t1) (z3obj_gno t2))
(**
@@ -4981,7 +5047,7 @@ struct
(**
Create a tactic that fails if the probe evaluates to false.
*)
- let fail_if ( ctx : context ) ( p : probe ) =
+ let fail_if ( ctx : context ) ( p : Probe.probe ) =
create ctx (Z3native.tactic_fail_if (context_gno ctx) (z3obj_gno p))
(**
@@ -4994,14 +5060,14 @@ struct
(**
Create a tactic that applies using the given set of parameters .
*)
- let using_params ( ctx : context ) ( t : tactic ) ( p : params ) =
+ let using_params ( ctx : context ) ( t : tactic ) ( p : Params.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 ) =
+ let with_ ( ctx : context ) ( t : tactic ) ( p : Params.params ) =
using_params ctx t p
(**
@@ -5029,7 +5095,9 @@ end
(** Solvers *)
module Solver =
struct
-
+ type solver = z3_native_object
+ type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
+
let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : solver = { m_ctx = ctx ;
m_n_obj = null ;
@@ -5038,7 +5106,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
let string_of_status ( s : status) = match s with
| UNSATISFIABLE -> "unsatisfiable"
@@ -5048,7 +5116,8 @@ struct
(** Objects that track statistical information about solvers. *)
module Statistics =
struct
-
+ type statistics = z3_native_object
+
let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : statistics = { m_ctx = ctx ;
m_n_obj = null ;
@@ -5066,7 +5135,13 @@ 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 ;
@@ -5086,7 +5161,7 @@ struct
m_float = v
} in
res
-
+
(** The key of the entry. *)
let get_key (x : statistics_entry) = x.m_key
@@ -5142,11 +5217,9 @@ struct
let f i = (Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i) in
Array.init n f
- (**
- The value of a particular statistical counter.
- *)
+ (** The value of a particular statistical counter. *)
let get ( x : statistics ) ( key : string ) =
- let f p c = (if (Entry.get_key c) = key then (Some c) else p) in
+ let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in
Array.fold_left f None (get_entries x)
end
@@ -5158,14 +5231,14 @@ struct
(**
Sets the solver parameters.
*)
- let set_parameters ( x : solver ) ( p : params )=
+ let set_parameters ( x : solver ) ( p : Params.params )=
Z3native.solver_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p)
(**
Retrieves parameter descriptions for solver.
*)
let get_param_descrs ( x : solver ) =
- Params.ParamDescrs.create (z3obj_gc x) (Z3native.solver_get_param_descrs (z3obj_gnc x) (z3obj_gno x))
+ Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.solver_get_param_descrs (z3obj_gnc x) (z3obj_gno x))
(**
The current number of backtracking points (scopes).
@@ -5196,7 +5269,7 @@ struct
(**
Assert a constraint (or multiple) into the solver.
*)
- let assert_ ( x : solver ) ( constraints : bool_expr array ) =
+ let assert_ ( x : solver ) ( constraints : Boolean.bool_expr array ) =
let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e)) in
ignore (Array.map f constraints)
@@ -5213,7 +5286,7 @@ struct
* and the Boolean literals
* provided using with assumptions.
*)
- let assert_and_track ( x : solver ) ( cs : bool_expr array ) ( ps : bool_expr array ) =
+ let assert_and_track ( x : solver ) ( cs : Boolean.bool_expr array ) ( ps : Boolean.bool_expr array ) =
if ((Array.length cs) != (Array.length ps)) then
raise (Z3native.Exception "Argument size mismatch")
else
@@ -5232,14 +5305,14 @@ struct
* and the Boolean literals
* provided using with assumptions.
*)
- let assert_and_track ( x : solver ) ( c : bool_expr ) ( p : bool_expr ) =
+ let assert_and_track ( x : solver ) ( c : Boolean.bool_expr ) ( p : Boolean.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.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in
+ let a = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in
(AST.ASTVector.get_size a)
@@ -5247,9 +5320,9 @@ struct
The set of asserted formulas.
*)
let get_assertions ( x : solver ) =
- let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in
+ let a = AST.ASTVector.ast_vector_of_ptr (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
+ let f i = Boolean.bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in
Array.init n f
(**
@@ -5259,12 +5332,12 @@ struct
*)
- let check ( x : solver ) ( assumptions : bool_expr array) =
+ let check ( x : solver ) ( assumptions : Boolean.bool_expr array) =
let r =
if ((Array.length assumptions) == 0) then
lbool_of_int (Z3native.solver_check (z3obj_gnc x) (z3obj_gno x))
else
- let f x = (ptr_of_expr (expr_of_bool_expr x)) in
+ let f x = (ptr_of_expr (Boolean.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
@@ -5306,7 +5379,7 @@ struct
if its results was not UNSATISFIABLE, or if core production is disabled.
*)
let get_unsat_core ( x : solver ) =
- let cn = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in
+ let cn = AST.ASTVector.ast_vector_of_ptr (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
@@ -5330,7 +5403,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 option ) =
+ let mk_solver ( ctx : context ) ( logic : Symbol.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)))
@@ -5354,7 +5427,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 ) =
+ let mk_solver_t ( ctx : context ) ( t : Tactic.tactic ) =
(create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t)))
(**
@@ -5366,7 +5439,9 @@ end
(** Fixedpoint solving *)
module Fixedpoint =
-struct
+struct
+ type fixedpoint = z3_native_object
+
let create ( ctx : context ) =
let res : fixedpoint = { m_ctx = ctx ;
m_n_obj = null ;
@@ -5375,7 +5450,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.
@@ -5386,19 +5461,19 @@ struct
(**
Sets the fixedpoint solver parameters.
*)
- let set_params ( x : fixedpoint ) ( p : params )=
+ let set_params ( x : fixedpoint ) ( p : Params.params )=
Z3native.fixedpoint_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p)
(**
Retrieves parameter descriptions for Fixedpoint solver.
*)
let get_param_descrs ( x : fixedpoint ) =
- Params.ParamDescrs.create (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x))
+ Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x))
(**
Assert a constraints into the fixedpoint solver.
*)
- let assert_ ( x : fixedpoint ) ( constraints : bool_expr array ) =
+ let assert_ ( x : fixedpoint ) ( constraints : Boolean.bool_expr array ) =
let f e = (Z3native.fixedpoint_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e)) in
ignore (Array.map f constraints) ;
()
@@ -5412,7 +5487,7 @@ struct
(**
Add rule into the fixedpoint solver.
*)
- let add_rule ( x : fixedpoint ) ( rule : bool_expr ) ( name : symbol option ) =
+ let add_rule ( x : fixedpoint ) ( rule : Boolean.bool_expr ) ( name : Symbol.symbol option ) =
match name with
| 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)
@@ -5429,11 +5504,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 : bool_expr ) =
+ let query ( x : fixedpoint ) ( query : Boolean.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
+ | L_TRUE -> Solver.SATISFIABLE
+ | L_FALSE -> Solver.UNSATISFIABLE
+ | _ -> Solver.UNKNOWN
(**
Query the fixedpoint solver.
@@ -5444,9 +5519,9 @@ struct
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
+ | L_TRUE -> Solver.SATISFIABLE
+ | L_FALSE -> Solver.UNSATISFIABLE
+ | _ -> Solver.UNKNOWN
(**
Creates a backtracking point.
@@ -5467,7 +5542,7 @@ struct
(**
Update named rule into in the fixedpoint solver.
*)
- let update_rule ( x : fixedpoint ) ( rule : bool_expr ) ( name : symbol ) =
+ let update_rule ( x : fixedpoint ) ( rule : Boolean.bool_expr ) ( name : Symbol.symbol ) =
Z3native.fixedpoint_update_rule (z3obj_gnc x) (z3obj_gno x) (Boolean.gno rule) (Symbol.gno name)
(**
@@ -5518,33 +5593,33 @@ struct
(**
Instrument the Datalog engine on which table representation to use for recursive predicate.
*)
- let set_predicate_representation ( x : fixedpoint ) ( f : func_decl ) ( kinds : symbol array ) =
+ let set_predicate_representation ( x : fixedpoint ) ( f : func_decl ) ( kinds : Symbol.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 : bool_expr array ) =
- let f x = ptr_of_expr (expr_of_bool_expr x) in
+ let to_string_q ( x : fixedpoint ) ( queries : Boolean.bool_expr array ) =
+ let f x = ptr_of_expr (Boolean.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.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in
+ let v = (AST.ASTVector.ast_vector_of_ptr (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
+ let f i = Boolean.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.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in
+ let v = (AST.ASTVector.ast_vector_of_ptr (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
+ let f i = Boolean.bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in
Array.init n f
(**
@@ -5628,9 +5703,9 @@ 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 : bool_expr array ) ( formula : bool_expr ) =
+ let benchmark_to_smtstring ( ctx : context ) ( name : string ) ( logic : string ) ( status : string ) ( attributes : string ) ( assumptions : Boolean.bool_expr array ) ( formula : Boolean.bool_expr ) =
Z3native.benchmark_to_smtlib_string (context_gno ctx) name logic status attributes
- (Array.length assumptions) (let f x = ptr_of_expr (expr_of_bool_expr x) in (Array.map f assumptions))
+ (Array.length assumptions) (let f x = ptr_of_expr (Boolean.expr_of_bool_expr x) in (Array.map f assumptions))
(Boolean.gno formula)
(**
@@ -5642,7 +5717,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 array ) ( sorts : sort array ) ( decl_names : symbol array ) ( decls : func_decl array ) =
+ let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.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
@@ -5662,7 +5737,7 @@ struct
Parse the given file using the SMT-LIB parser.
*)
- 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 parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.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
@@ -5688,7 +5763,7 @@ struct
*)
let get_smtlib_formulas ( ctx : context ) =
let n = (get_num_smtlib_formulas ctx ) in
- let f i = bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_formula (context_gno ctx) i)) in
+ let f i = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_formula (context_gno ctx) i)) in
Array.init n f
@@ -5702,7 +5777,7 @@ struct
*)
let get_smtlib_assumptions ( ctx : context ) =
let n = (get_num_smtlib_assumptions ctx ) in
- let f i = bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_assumption (context_gno ctx) i)) in
+ let f i = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_assumption (context_gno ctx) i)) in
Array.init n f
(**
@@ -5737,7 +5812,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 array ) ( sorts : sort array ) ( decl_names : symbol array ) ( decls : func_decl array ) =
+ let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.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
@@ -5745,19 +5820,19 @@ struct
if (csn != cs || cdn != cd) then
raise (Z3native.Exception "Argument size mismatch")
else
- 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))))
+ Boolean.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 array ) ( sorts : sort array ) ( decl_names : symbol array ) ( decls : func_decl array ) =
+ let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.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
@@ -5765,13 +5840,13 @@ struct
if (csn != cs || cdn != cd) then
raise (Z3native.Exception "Argument size mismatch")
else
- bool_expr_of_expr (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) file_name
- 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))))
+ Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) file_name
+ 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))))
end
@@ -5818,23 +5893,3 @@ let get_global_param ( id : string ) =
*)
let global_param_reset_all =
Z3native.global_param_reset_all
-
-
-
-(*
-
-(**
- A delegate which is executed when an error is raised.
-
- Note that it is possible for memory leaks to occur if error handlers
- throw exceptions.
-*)
- public delegate void ErrorHandler(Context ctx, error_code errorCode, string errorString);
-
- internal Z3native.error_handler m_n_err_handler = null;
-
- internal void NativeErrorHandler(IntPtr ctx, error_code errorCode)
-
- Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
-
-*)
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 5d5d7adf0..5b1b2073a 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -7,333 +7,566 @@
type context
-type int_symbol
-type string_symbol
-type symbol = S_Int of int_symbol | S_Str of string_symbol
+(** Create a context object.
-type ast
-type ast_vector
-type ast_map
+ Most interactions with Z3 are interpreted in some context; many users will only
+ require one such object, but power users may require more than one. To start using
+ Z3, do
-type sort = Sort of ast
+
+ let ctx = (mk_context []) in
+ (...)
+
-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
+ where a list of pairs of strings may be passed to set options on
+ the context, e.g., like so:
-type func_decl = FuncDecl of ast
+
+ let cfg = [("model", "true"); ("...", "...")] in
+ let ctx = (mk_context cfg) in
+ (...)
+
+*)
+val mk_context : (string * string) list -> context
-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
-type param_descrs
-
-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
-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
-type quantifier = Quantifier of expr
-type pattern = Pattern of ast
-
-type constructor
-
-type goal
-
-type model
-type func_interp
-type func_entry
-
-type probe
-
-type tactic
-type apply_result
-
-type solver
-type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
-
-type statistics
-type statistics_entry
-
-type fixedpoint
-
-val ast_of_sort : sort -> ast
-val sort_of_uninterpreted_sort : uninterpreted_sort -> sort
-val sort_of_bool_sort : bool_sort -> sort
-val sort_of_array_sort : array_sort -> sort
-val sort_of_set_sort : set_sort -> sort
-val sort_of_datatype_sort : datatype_sort -> sort
-val sort_of_relation_sort : relation_sort -> sort
-val sort_of_finite_domain_sort : finite_domain_sort -> sort
-val sort_of_enum_sort : enum_sort -> sort
-val sort_of_list_sort : list_sort -> sort
-val sort_of_tuple_sort : tuple_sort -> sort
-val sort_of_arith_sort : arith_sort -> sort
-val sort_of_bitvec_sort : bitvec_sort -> sort
-val arith_sort_of_int_sort : int_sort -> arith_sort
-val arith_sort_of_real_sort : real_sort -> arith_sort
-val uninterpreted_sort_of_sort : sort -> uninterpreted_sort
-val bool_sort_of_sort : sort -> bool_sort
-val array_sort_of_sort : sort -> array_sort
-val datatype_sort_of_sort : sort -> datatype_sort
-val relation_sort_of_sort : sort -> relation_sort
-val finite_domain_sort_of_sort : sort -> finite_domain_sort
-val arith_sort_of_sort : sort -> arith_sort
-val bitvec_sort_of_sort : sort -> bitvec_sort
-val int_sort_of_arith_sort : arith_sort -> int_sort
-val real_sort_of_arith_sort : arith_sort -> real_sort
-val ast_of_func_decl : func_decl -> ast
-val ast_of_expr : expr -> ast
-val expr_of_bool_expr : bool_expr -> expr
-val expr_of_arith_expr : arith_expr -> expr
-val expr_of_bitvec_expr : bitvec_expr -> expr
-val expr_of_array_expr : array_expr -> expr
-val expr_of_datatype_expr : datatype_expr -> expr
-val arith_expr_of_int_expr : int_expr -> arith_expr
-val arith_expr_of_real_expr : real_expr -> arith_expr
-val int_expr_of_int_num : int_num -> int_expr
-val real_expr_of_rat_num : rat_num -> real_expr
-val arith_expr_of_algebraic_num : algebraic_num -> arith_expr
-val bitvec_expr_of_bitvec_num : bitvec_num -> bitvec_expr
-val expr_of_quantifier : quantifier -> expr
-val ast_of_pattern : pattern -> ast
-val expr_of_ast : ast -> expr
-val bool_expr_of_expr : expr -> bool_expr
-val arith_expr_of_expr : expr -> arith_expr
-val bitvec_expr_of_expr : expr -> bitvec_expr
-val array_expr_of_expr : expr -> array_expr
-val datatype_expr_of_expr : expr -> datatype_expr
-val int_expr_of_arith_expr : arith_expr -> int_expr
-val real_expr_of_arith_expr : arith_expr -> real_expr
-val int_num_of_int_expr : int_expr -> int_num
-val rat_num_of_real_expr : real_expr -> rat_num
-val algebraic_num_of_arith_expr : arith_expr -> algebraic_num
-val bitvec_num_of_bitvec_expr : bitvec_expr -> bitvec_num
-val quantifier_of_expr : expr -> quantifier
-val pattern_of_ast : ast -> pattern
+(** 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 :
sig
+ (** Open an interaction log file.
+ @param filename the name of the file to open.
+ @return True if opening the log file succeeds, false otherwise.
+ *)
+ (* CMW: "open" seems to be a reserved keyword? *)
val open_ : string -> bool
+
+ (** Closes the interaction log. *)
val close : unit
+
+ (** Appends a user-provided string to the interaction log.
+ @param s the string to append*)
val append : string -> unit
end
+(** Version information *)
module Version :
sig
+ (** The major version. *)
val major : int
+
+ (** The minor version. *)
val minor : int
+
+ (** The build version. *)
val build : int
+
+ (** The revision. *)
val revision : int
+
+ (** A string representation of the version information. *)
val to_string : string
end
-val mk_context : (string * string) list -> context
-
+(** Symbols are used to name several term and type constructors *)
module Symbol :
sig
+ (** Numbered Symbols *)
+ type int_symbol
+
+ (** Named Symbols *)
+ type string_symbol
+
+ (** Symbols *)
+ type symbol = S_Int of int_symbol | S_Str of string_symbol
+
+ (** The kind of the symbol (int or string) *)
val kind : symbol -> Z3enums.symbol_kind
+
+ (** Indicates whether the symbol is of Int kind *)
val is_int_symbol : symbol -> bool
+
+ (** Indicates whether the symbol is of string kind. *)
val is_string_symbol : symbol -> bool
+
+ (** The int value of the symbol. *)
val get_int : int_symbol -> int
+
+ (** The string value of the symbol. *)
val get_string : string_symbol -> string
+
+ (** A string representation of the symbol. *)
val to_string : symbol -> string
+
+ (**
+ Creates a new symbol using an integer.
+
+ Not all integers can be passed to this function.
+ The legal range of unsigned integers is 0 to 2^30-1.
+ *)
val mk_int : context -> int -> symbol
+
+ (** Creates a new symbol using a string. *)
val mk_string : context -> string -> symbol
+
+ (** Create an array of symbols. *)
val mk_ints : context -> int array -> symbol array
+
+ (** Create an array of symbols. *)
val mk_strings : context -> string array -> symbol array
end
+(** The abstract syntax tree (AST) module *)
module AST :
sig
+ type ast
+ (** Vectors of ASTs *)
module ASTVector :
sig
+ type ast_vector
+
+ (** The size of the vector *)
val get_size : ast_vector -> int
- val get : ast_vector -> int -> ast_vector
+
+ (**
+ Retrieves the i-th object in the vector.
+ @param i Index
+ @return An AST
+ *)
+ val get : ast_vector -> int -> ast
+
+ (** Sets the i-th object in the vector. *)
val set : ast_vector -> int -> ast -> unit
+
+ (** Resize the vector to .
+ @param newSize The new size of the vector. *)
val resize : ast_vector -> int -> unit
+
+ (**
+ Add the AST to the back of the vector. The size
+ is increased by 1.
+ @param a An AST
+ *)
val push : ast_vector -> ast -> unit
+
+ (**
+ Translates all ASTs in the vector to .
+ @param to_ctx A context
+ @return A new ASTVector
+ *)
val translate : ast_vector -> context -> ast_vector
+
+ (** Retrieves a string representation of the vector. *)
val to_string : ast_vector -> string
end
+ (** Map from AST to AST *)
module ASTMap :
sig
+ type ast_map
+
+ (** Checks whether the map contains the key .
+ @param k An AST
+ @return True if is a key in the map, false otherwise. *)
val contains : ast_map -> ast -> bool
- val find : ast_map -> ast -> ast_map
+
+ (** Finds the value associated with the key .
+
+ This function signs an error when is not a key in the map.
+ @param k An AST
+ *)
+ val find : ast_map -> ast -> ast
+
+ (**
+ Stores or replaces a new key/value pair in the map.
+ @param k The key AST
+ @param v The value AST
+ *)
val insert : ast_map -> ast -> ast -> unit
+
+ (**
+ Erases the key from the map.
+ @param k An AST
+ *)
val erase : ast_map -> ast -> unit
+
+ (** Removes all keys from the map. *)
val reset : ast_map -> unit
+
+ (** The size of the map *)
val get_size : ast_map -> int
- val get_keys : ast_map -> ast_vector
+
+ (** The keys stored in the map. *)
+ val get_keys : ast_map -> ASTVector.ast_vector
+
+ (** Retrieves a string representation of the map.*)
val to_string : ast_map -> string
end
+ (**
+ The AST's hash code.
+ @return A hash code
+ *)
val get_hash_code : ast -> int
+
+ (** A unique identifier for the AST (unique among all ASTs). *)
val get_id : ast -> int
+
+ (** The kind of the AST. *)
val get_ast_kind : ast -> Z3enums.ast_kind
+
+ (** Indicates whether the AST is an Expr *)
val is_expr : ast -> bool
+
+ (** Indicates whether the AST is a bound variable*)
val is_var : ast -> bool
+
+ (** Indicates whether the AST is a Quantifier *)
val is_quantifier : ast -> bool
+
+ (** Indicates whether the AST is a Sort *)
val is_sort : ast -> bool
+
+ (** Indicates whether the AST is a func_decl *)
val is_func_decl : ast -> bool
+
+ (** A string representation of the AST. *)
val to_string : ast -> string
+
+ (** A string representation of the AST in s-expression notation. *)
val to_sexpr : ast -> string
+
+ (**
+ Comparison operator.
+ @param a An AST
+ @param b An AST
+ @return True if and are from the same context
+ and represent the same sort; false otherwise.
+ *)
val ( = ) : ast -> ast -> bool
+
+ (**
+ Object Comparison.
+ @param other Another ast
+ @return Negative if the object should be sorted before , positive if after else zero.
+ *)
val compare : ast -> ast -> int
+
+ (** Operator < *)
val ( < ) : ast -> ast -> int
+
+ (**
+ Translates (copies) the AST to the Context .
+ @param ctx A context
+ @return A copy of the AST which is associated with
+ *)
val translate : ast -> context -> ast
+
+ (**
+ Wraps an AST.
+
+ This function is used for transitions between native and
+ managed objects. Note that must be a
+ native object obtained from Z3 (e.g., through )
+ and that it must have a correct reference count (see e.g.,
+ .
+
+ @param nativeObject The native pointer to wrap.
+ *)
val wrap : context -> Z3native.z3_ast -> ast
+
+ (**
+ Unwraps an AST.
+ This function is used for transitions between native and
+ managed objects. It returns the native pointer to the AST. Note that
+ AST objects are reference counted and unwrapping an AST disables automatic
+ reference counting, i.e., all references to the IntPtr that is returned
+ must be handled externally and through native calls (see e.g.,
+ ).
+
+ @param a The AST to unwrap.
+ *)
val unwrap_ast : ast -> Z3native.ptr
end
+(** The Sort module implements type information for ASTs *)
module Sort :
sig
+ (** Sorts *)
+ type sort = Sort of AST.ast
+
+ (** Uninterpreted Sorts *)
+ type uninterpreted_sort = UninterpretedSort of sort
+
+ val ast_of_sort : sort -> AST.ast
+ val sort_of_uninterpreted_sort : uninterpreted_sort -> sort
+ val uninterpreted_sort_of_sort : sort -> uninterpreted_sort
+
+ (**
+ Comparison operator.
+ @param a A sort
+ @param b A sort
+ @return True if and are from the same context
+ and represent the same sort; false otherwise.
+ *)
val ( = ) : sort -> sort -> bool
+
+ (** Returns a unique identifier for the sort. *)
val get_id : sort -> int
+
+ (** The kind of the sort. *)
val get_sort_kind : sort -> Z3enums.sort_kind
- val get_name : sort -> symbol
+
+ (** The name of the sort *)
+ val get_name : sort -> Symbol.symbol
+
+ (** A string representation of the sort. *)
val to_string : sort -> string
- val mk_uninterpreted : context -> symbol -> uninterpreted_sort
+
+ (** Create a new uninterpreted sort. *)
+ val mk_uninterpreted : context -> Symbol.symbol -> uninterpreted_sort
+
+ (** Create a new uninterpreted sort. *)
val mk_uninterpreted_s : context -> string -> uninterpreted_sort
end
-module FuncDecl :
+(** Function declarations *)
+module rec FuncDecl :
sig
+ type func_decl = FuncDecl of AST.ast
+ val ast_of_func_decl : FuncDecl.func_decl -> AST.ast
+
+ (** Parameters of Func_Decls *)
module Parameter :
sig
+ (** Parameters of func_decls *)
+ type parameter =
+ P_Int of int
+ | P_Dbl of float
+ | P_Sym of Symbol.symbol
+ | P_Srt of Sort.sort
+ | P_Ast of AST.ast
+ | P_Fdl of func_decl
+ | P_Rat of string
+
+ (** The kind of the parameter. *)
val get_kind : parameter -> Z3enums.parameter_kind
+
+ (** The int value of the parameter.*)
val get_int : parameter -> int
+
+ (** The double value of the parameter.*)
val get_float : parameter -> float
- val get_symbol : parameter -> symbol
- val get_sort : parameter -> sort
- val get_ast : parameter -> ast
- val get_func_decl : parameter -> string
+
+ (** The Symbol.Symbol value of the parameter.*)
+ val get_symbol : parameter -> Symbol.symbol
+
+ (** The Sort value of the parameter.*)
+ val get_sort : parameter -> Sort.sort
+
+ (** The AST value of the parameter.*)
+ val get_ast : parameter -> AST.ast
+
+ (** The FunctionDeclaration value of the parameter.*)
+ val get_func_decl : parameter -> func_decl
+
+ (** The rational string value of the parameter.*)
+ val get_rational : parameter -> string
end
- val mk_func_decl : context -> symbol -> sort array -> sort -> func_decl
- val mk_func_decl_s : context -> string -> sort array -> sort -> func_decl
- val mk_fresh_func_decl : context -> string -> sort array -> sort -> func_decl
- val mk_const_decl : context -> symbol -> sort -> func_decl
- val mk_const_decl_s : context -> string -> sort -> func_decl
- val mk_fresh_const_decl : context -> string -> sort -> func_decl
+ (** Creates a new function declaration. *)
+ val mk_func_decl : context -> Symbol.symbol -> Sort.sort array -> Sort.sort -> func_decl
+
+ (** Creates a new function declaration. *)
+ val mk_func_decl_s : context -> string -> Sort.sort array -> Sort.sort -> func_decl
+ (** Creates a fresh function declaration with a name prefixed with .
+
+ *)
+
+ val mk_fresh_func_decl : context -> string -> Sort.sort array -> Sort.sort -> func_decl
+
+ (** Creates a new constant function declaration. *)
+ val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl
+
+ (** Creates a new constant function declaration. *)
+ val mk_const_decl_s : context -> string -> Sort.sort -> func_decl
+
+ (** Creates a fresh constant function declaration with a name prefixed with .
+
+ *)
+ val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl
+
+ (** Comparison operator.
+ @param a A func_decl
+ @param b A func_decl
+ @return True if and are from the same context
+ and represent the same func_decl; false otherwise. *)
val ( = ) : func_decl -> func_decl -> bool
+
+ (** A string representations of the function declaration. *)
val to_string : func_decl -> string
+
+ (** Returns a unique identifier for the function declaration. *)
val get_id : func_decl -> int
+
+ (** The arity of the function declaration *)
val get_arity : func_decl -> int
+
+ (** The size of the domain of the function declaration
+ *)
val get_domain_size : func_decl -> int
- val get_domain : func_decl -> sort array
- val get_range : func_decl -> sort
+
+ (** The domain of the function declaration *)
+ val get_domain : func_decl -> Sort.sort array
+
+ (** The range of the function declaration *)
+ val get_range : func_decl -> Sort.sort
+
+ (** The kind of the function declaration. *)
val get_decl_kind : func_decl -> Z3enums.decl_kind
- val get_name : func_decl -> symbol
+
+ (** The name of the function declaration*)
+ val get_name : func_decl -> Symbol.symbol
+
+ (** The number of parameters of the function declaration *)
val get_num_parameters : func_decl -> int
- val get_parameters : func_decl -> parameter list
- val apply : func_decl -> expr array -> expr
+
+ (** The parameters of the function declaration *)
+ val get_parameters : func_decl -> Parameter.parameter list
+
+ (** Create expression that applies function to arguments.
+ @param args The arguments *)
+ val apply : func_decl -> Expr.expr array -> Expr.expr
end
-module Params :
-sig
+(** Parameter sets (of Solvers, Tactics, ...)
+ A Params objects represents a configuration in the form of Symbol.symbol/value pairs. *)
+and Params :
+sig
+ type params
+
+ (** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *)
module ParamDescrs :
sig
+ type param_descrs
+
+ (** Validate a set of parameters. *)
val validate : param_descrs -> params -> unit
- val get_kind : param_descrs -> symbol -> Z3enums.param_kind
- val get_names : param_descrs -> symbol array
+
+ (** Retrieve kind of parameter. *)
+ val get_kind : param_descrs -> Symbol.symbol -> Z3enums.param_kind
+
+ (** Retrieve all names of parameters. *)
+ val get_names : param_descrs -> Symbol.symbol array
+
+ (** The size of the ParamDescrs. *)
val get_size : param_descrs -> int
+
+ (** Retrieves a string representation of the ParamDescrs. *)
val to_string : param_descrs -> string
end
- val add_bool : params -> symbol -> bool -> unit
- val add_int : params -> symbol -> int -> unit
- val add_double : params -> symbol -> float -> unit
- val add_symbol : params -> symbol -> symbol -> unit
+ (** Adds a parameter setting. *)
+ val add_bool : params -> Symbol.symbol -> bool -> unit
+
+ (** Adds a parameter setting. *)
+ val add_int : params -> Symbol.symbol -> int -> unit
+
+ (** Adds a parameter setting. *)
+ val add_double : params -> Symbol.symbol -> float -> unit
+
+ (** Adds a parameter setting. *)
+ val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
+
+ (** Adds a parameter setting. *)
val add_s_bool : params -> string -> bool -> unit
+
+ (** Adds a parameter setting. *)
val add_s_int : params -> string -> int -> unit
+
+ (** Adds a parameter setting. *)
val add_s_double : params -> string -> float -> unit
- val add_s_symbol : params -> string -> symbol -> unit
+
+ (** Adds a parameter setting. *)
+ val add_s_symbol : params -> string -> Symbol.symbol -> unit
+
+ (** Creates a new parameter set *)
val mk_params : context -> params
+
+ (** A string representation of the parameter set. *)
val to_string : params -> string
end
-module Expr :
+and Expr :
sig
- val simplify : expr -> params option -> expr
+ (** General Expressions (Terms) *)
+ type expr = Expr of AST.ast
+
+ val ast_of_expr : Expr.expr -> AST.ast
+ val expr_of_ast : AST.ast -> Expr.expr
+
+ val simplify : Expr.expr -> Params.params option -> expr
val get_simplify_help : context -> string
- val get_simplify_parameter_descrs : context -> param_descrs
- val get_func_decl : expr -> func_decl
- val get_bool_value : expr -> Z3enums.lbool
- val get_num_args : expr -> int
- val get_args : expr -> expr array
- val update : expr -> expr array -> expr
- val substitute : expr -> expr array -> expr array -> expr
- val substitute_one : expr -> expr -> expr -> expr
- val substitute_vars : expr -> expr array -> expr
- val translate : expr -> context -> expr
- val to_string : expr -> string
- val is_numeral : expr -> bool
- val is_well_sorted : expr -> bool
- val get_sort : expr -> sort
- val is_bool : expr -> bool
- val is_const : expr -> bool
- val is_true : expr -> bool
- val is_false : expr -> bool
- val is_eq : expr -> bool
- val is_distinct : expr -> bool
- val is_ite : expr -> bool
- val is_and : expr -> bool
- val is_or : expr -> bool
- val is_iff : expr -> bool
- val is_xor : expr -> bool
- val is_not : expr -> bool
- val is_implies : expr -> bool
- val is_label : expr -> bool
- val is_oeq : expr -> bool
- val mk_const : context -> symbol -> sort -> expr
- val mk_const_s : context -> string -> sort -> expr
- val mk_const_f : context -> func_decl -> expr
- val mk_fresh_const : context -> string -> sort -> expr
- val mk_app : context -> func_decl -> expr array -> expr
- val mk_numeral_string : context -> string -> sort -> expr
- val mk_numeral_int : context -> int -> sort -> expr
+ val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs
+ val get_func_decl : Expr.expr -> FuncDecl.func_decl
+ val get_bool_value : Expr.expr -> Z3enums.lbool
+ val get_num_args : Expr.expr -> int
+ val get_args : Expr.expr -> Expr.expr array
+ val update : Expr.expr -> Expr.expr array -> expr
+ val substitute : Expr.expr -> Expr.expr array -> Expr.expr array -> expr
+ val substitute_one : Expr.expr -> Expr.expr -> Expr.expr -> expr
+ val substitute_vars : Expr.expr -> Expr.expr array -> expr
+ val translate : Expr.expr -> context -> expr
+ val to_string : Expr.expr -> string
+ val is_numeral : Expr.expr -> bool
+ val is_well_sorted : Expr.expr -> bool
+ val get_sort : Expr.expr -> Sort.sort
+ val is_bool : Expr.expr -> bool
+ val is_const : Expr.expr -> bool
+ val is_true : Expr.expr -> bool
+ val is_false : Expr.expr -> bool
+ val is_eq : Expr.expr -> bool
+ val is_distinct : Expr.expr -> bool
+ val is_ite : Expr.expr -> bool
+ val is_and : Expr.expr -> bool
+ val is_or : Expr.expr -> bool
+ val is_iff : Expr.expr -> bool
+ val is_xor : Expr.expr -> bool
+ val is_not : Expr.expr -> bool
+ val is_implies : Expr.expr -> bool
+ val is_label : Expr.expr -> bool
+ val is_oeq : Expr.expr -> bool
+ val mk_const : context -> Symbol.symbol -> Sort.sort -> expr
+ val mk_const_s : context -> string -> Sort.sort -> expr
+ val mk_const_f : context -> FuncDecl.func_decl -> expr
+ val mk_fresh_const : context -> string -> Sort.sort -> expr
+ val mk_app : context -> FuncDecl.func_decl -> Expr.expr array -> expr
+ val mk_numeral_string : context -> string -> Sort.sort -> expr
+ val mk_numeral_int : context -> int -> Sort.sort -> expr
end
module Boolean :
sig
+ type bool_sort = BoolSort of Sort.sort
+ type bool_expr = BoolExpr of Expr.expr
+
+ val expr_of_bool_expr : bool_expr -> Expr.expr
+ val sort_of_bool_sort : bool_sort -> Sort.sort
+ val bool_sort_of_sort : Sort.sort -> bool_sort
+ val bool_expr_of_expr : Expr.expr -> bool_expr
+
val mk_sort : context -> bool_sort
- val mk_const : context -> symbol -> bool_expr
+ val mk_const : context -> Symbol.symbol -> bool_expr
val mk_const_s : context -> string -> bool_expr
val mk_true : context -> bool_expr
val mk_false : context -> bool_expr
val mk_val : context -> bool -> bool_expr
- val mk_eq : context -> expr -> expr -> bool_expr
- val mk_distinct : context -> expr array -> bool_expr
+ val mk_eq : context -> Expr.expr -> Expr.expr -> bool_expr
+ val mk_distinct : context -> Expr.expr array -> bool_expr
val mk_not : context -> bool_expr -> bool_expr
val mk_ite : context -> bool_expr -> bool_expr -> bool_expr -> bool_expr
val mk_iff : context -> bool_expr -> bool_expr -> bool_expr
@@ -345,482 +578,590 @@ end
module Quantifier :
sig
+ type quantifier = Quantifier of Expr.expr
+
+ val expr_of_quantifier : quantifier -> Expr.expr
+ val quantifier_of_expr : Expr.expr -> quantifier
+
module Pattern :
sig
+ type pattern = Pattern of AST.ast
+
+ val ast_of_pattern : pattern -> AST.ast
+ val pattern_of_ast : AST.ast -> pattern
+
val get_num_terms : pattern -> int
- val get_terms : pattern -> expr array
+ val get_terms : pattern -> Expr.expr array
val to_string : pattern -> string
end
- val get_index : expr -> int
+ val get_index : Expr.expr -> int
val is_universal : quantifier -> bool
val is_existential : quantifier -> bool
val get_weight : quantifier -> int
val get_num_patterns : quantifier -> int
- val get_patterns : quantifier -> pattern array
+ val get_patterns : quantifier -> Pattern.pattern array
val get_num_no_patterns : quantifier -> int
- val get_no_patterns : quantifier -> pattern array
+ val get_no_patterns : quantifier -> Pattern.pattern array
val get_num_bound : quantifier -> int
- val get_bound_variable_names : quantifier -> symbol array
- val get_bound_variable_sorts : quantifier -> sort array
- val get_body : quantifier -> bool_expr
- val mk_bound : context -> int -> sort -> expr
- val mk_pattern : context -> expr array -> pattern
+ val get_bound_variable_names : quantifier -> Symbol.symbol array
+ val get_bound_variable_sorts : quantifier -> Sort.sort array
+ val get_body : quantifier -> Boolean.bool_expr
+ val mk_bound : context -> int -> Sort.sort -> Expr.expr
+ val mk_pattern : context -> Expr.expr array -> Pattern.pattern
val mk_forall :
context ->
- sort array ->
- symbol array ->
- expr ->
+ Sort.sort array ->
+ Symbol.symbol array ->
+ Expr.expr ->
int option ->
- pattern array ->
- expr array -> symbol option -> symbol option -> quantifier
+ Pattern.pattern array ->
+ Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier
val mk_forall_const :
context ->
- expr array ->
- expr ->
+ Expr.expr array ->
+ Expr.expr ->
int option ->
- pattern array ->
- expr array -> symbol option -> symbol option -> quantifier
+ Pattern.pattern array ->
+ Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier
val mk_exists :
context ->
- sort array ->
- symbol array ->
- expr ->
+ Sort.sort array ->
+ Symbol.symbol array ->
+ Expr.expr ->
int option ->
- pattern array ->
- expr array -> symbol option -> symbol option -> quantifier
+ Pattern.pattern array ->
+ Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier
val mk_exists_const :
context ->
- expr array ->
- expr ->
+ Expr.expr array ->
+ Expr.expr ->
int option ->
- pattern array ->
- expr array -> symbol option -> symbol option -> quantifier
+ Pattern.pattern array ->
+ Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier
val mk_quantifier :
context ->
bool ->
- expr array ->
- expr ->
+ Expr.expr array ->
+ Expr.expr ->
int option ->
- pattern array ->
- expr array -> symbol option -> symbol option -> quantifier
+ Pattern.pattern array ->
+ Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier
end
module Array_ :
sig
- val mk_sort : context -> sort -> sort -> array_sort
- val is_store : expr -> bool
- val is_select : expr -> bool
- val is_constant_array : expr -> bool
- val is_default_array : expr -> bool
- val is_array_map : expr -> bool
- val is_as_array : expr -> bool
- val is_array : expr -> bool
- val get_domain : array_sort -> sort
- val get_range : array_sort -> sort
- val mk_const : context -> symbol -> sort -> sort -> array_expr
- val mk_const_s : context -> string -> sort -> sort -> array_expr
- val mk_select : context -> array_expr -> expr -> expr -> expr
- val mk_const_array : context -> sort -> expr -> expr
- val mk_map : context -> func_decl -> array_expr array -> expr
- val mk_term_array : context -> array_expr -> expr
+ type array_sort = ArraySort of Sort.sort
+ type array_expr = ArrayExpr of Expr.expr
+
+ val sort_of_array_sort : array_sort -> Sort.sort
+ val array_sort_of_sort : Sort.sort -> array_sort
+ val expr_of_array_expr : array_expr -> Expr.expr
+
+ val array_expr_of_expr : Expr.expr -> array_expr
+
+ val mk_sort : context -> Sort.sort -> Sort.sort -> array_sort
+ val is_store : Expr.expr -> bool
+ val is_select : Expr.expr -> bool
+ val is_constant_array : Expr.expr -> bool
+ val is_default_array : Expr.expr -> bool
+ val is_array_map : Expr.expr -> bool
+ val is_as_array : Expr.expr -> bool
+ val is_array : Expr.expr -> bool
+ val get_domain : array_sort -> Sort.sort
+ val get_range : array_sort -> Sort.sort
+ val mk_const : context -> Symbol.symbol -> Sort.sort -> Sort.sort -> array_expr
+ val mk_const_s : context -> string -> Sort.sort -> Sort.sort -> array_expr
+ val mk_select : context -> array_expr -> Expr.expr -> Expr.expr -> array_expr
+ val mk_const_array : context -> Sort.sort -> Expr.expr -> array_expr
+ val mk_map : context -> FuncDecl.func_decl -> array_expr array -> array_expr
+ val mk_term_array : context -> array_expr -> array_expr
end
module Set :
sig
- val is_union : expr -> bool
- val is_intersect : expr -> bool
- val is_difference : expr -> bool
- val is_complement : expr -> bool
- val is_subset : expr -> bool
- val mk_sort : context -> sort -> set_sort
- val mk_empty : context -> sort -> expr
- val mk_full : context -> sort -> expr
- val mk_set_add : context -> expr -> expr -> expr
- val mk_del : context -> expr -> expr -> expr
- val mk_union : context -> expr array -> expr
- val mk_intersection : context -> expr array -> expr
- val mk_difference : context -> expr -> expr -> expr
- val mk_complement : context -> expr -> expr
- val mk_membership : context -> expr -> expr -> expr
- val mk_subset : context -> expr -> expr -> expr
+ type set_sort = SetSort of Sort.sort
+
+ val sort_of_set_sort : set_sort -> Sort.sort
+
+ val is_union : Expr.expr -> bool
+ val is_intersect : Expr.expr -> bool
+ val is_difference : Expr.expr -> bool
+ val is_complement : Expr.expr -> bool
+ val is_subset : Expr.expr -> bool
+ val mk_sort : context -> Sort.sort -> set_sort
+ val mk_empty : context -> Sort.sort -> Expr.expr
+ val mk_full : context -> Sort.sort -> Expr.expr
+ val mk_set_add : context -> Expr.expr -> Expr.expr -> Expr.expr
+ val mk_del : context -> Expr.expr -> Expr.expr -> Expr.expr
+ val mk_union : context -> Expr.expr array -> Expr.expr
+ val mk_intersection : context -> Expr.expr array -> Expr.expr
+ val mk_difference : context -> Expr.expr -> Expr.expr -> Expr.expr
+ val mk_complement : context -> Expr.expr -> Expr.expr
+ val mk_membership : context -> Expr.expr -> Expr.expr -> Expr.expr
+ val mk_subset : context -> Expr.expr -> Expr.expr -> Expr.expr
end
module FiniteDomain :
sig
- val mk_sort : context -> symbol -> int -> finite_domain_sort
+ type finite_domain_sort = FiniteDomainSort of Sort.sort
+
+ val sort_of_finite_domain_sort : finite_domain_sort -> Sort.sort
+ val finite_domain_sort_of_sort : Sort.sort -> finite_domain_sort
+
+ val mk_sort : context -> Symbol.symbol -> int -> finite_domain_sort
val mk_sort_s : context -> string -> int -> finite_domain_sort
- val is_finite_domain : expr -> bool
- val is_lt : expr -> bool
+ val is_finite_domain : Expr.expr -> bool
+ val is_lt : Expr.expr -> bool
val get_size : finite_domain_sort -> int
end
module Relation :
sig
- val is_relation : expr -> bool
- val is_store : expr -> bool
- val is_empty : expr -> bool
- val is_is_empty : expr -> bool
- val is_join : expr -> bool
- val is_union : expr -> bool
- val is_widen : expr -> bool
- val is_project : expr -> bool
- val is_filter : expr -> bool
- val is_negation_filter : expr -> bool
- val is_rename : expr -> bool
- val is_complement : expr -> bool
- val is_select : expr -> bool
- val is_clone : expr -> bool
+ type relation_sort = RelationSort of Sort.sort
+
+ val sort_of_relation_sort : relation_sort -> Sort.sort
+ val relation_sort_of_sort : Sort.sort -> relation_sort
+
+ val is_relation : Expr.expr -> bool
+ val is_store : Expr.expr -> bool
+ val is_empty : Expr.expr -> bool
+ val is_is_empty : Expr.expr -> bool
+ val is_join : Expr.expr -> bool
+ val is_union : Expr.expr -> bool
+ val is_widen : Expr.expr -> bool
+ val is_project : Expr.expr -> bool
+ val is_filter : Expr.expr -> bool
+ val is_negation_filter : Expr.expr -> bool
+ val is_rename : Expr.expr -> bool
+ val is_complement : Expr.expr -> bool
+ val is_select : Expr.expr -> bool
+ val is_clone : Expr.expr -> bool
val get_arity : relation_sort -> int
val get_column_sorts : relation_sort -> relation_sort array
end
module Datatype :
sig
+ type datatype_sort = DatatypeSort of Sort.sort
+ type datatype_expr = DatatypeExpr of Expr.expr
+
+ val sort_of_datatype_sort : datatype_sort -> Sort.sort
+ val datatype_sort_of_sort : Sort.sort -> datatype_sort
+ val expr_of_datatype_expr : datatype_expr -> Expr.expr
+ val datatype_expr_of_expr : Expr.expr -> datatype_expr
module Constructor :
sig
+ (** Constructors *)
+ type constructor
+
val get_n : constructor -> int
- val constructor_decl : constructor -> func_decl
- val tester_decl : constructor -> func_decl
- val accessor_decls : constructor -> func_decl array
+ val constructor_decl : constructor -> FuncDecl.func_decl
+ val tester_decl : constructor -> FuncDecl.func_decl
+ val accessor_decls : constructor -> FuncDecl.func_decl array
val get_num_fields : constructor -> int
- val get_constructor_decl : constructor -> func_decl
- val get_tester_decl : constructor -> func_decl
- val get_accessor_decls : constructor -> func_decl array
+ val get_constructor_decl : constructor -> FuncDecl.func_decl
+ val get_tester_decl : constructor -> FuncDecl.func_decl
+ val get_accessor_decls : constructor -> FuncDecl.func_decl array
end
- val mk_constructor : context -> symbol -> symbol -> symbol array -> sort array -> int array -> constructor
- val mk_constructor_s : context -> string -> symbol -> symbol array -> sort array -> int array -> constructor
- val mk_sort : context -> symbol -> constructor array -> datatype_sort
- val mk_sort_s : context -> string -> constructor array -> datatype_sort
- val mk_sorts : context -> symbol array -> constructor array array -> datatype_sort array
- val mk_sorts_s : context -> string array -> constructor array array -> datatype_sort array
+ val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol array -> Sort.sort array -> int array -> Constructor.constructor
+ val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol array -> Sort.sort array -> int array -> Constructor.constructor
+ val mk_sort : context -> Symbol.symbol -> Constructor.constructor array -> datatype_sort
+ val mk_sort_s : context -> string -> Constructor.constructor array -> datatype_sort
+ val mk_sorts : context -> Symbol.symbol array -> Constructor.constructor array array -> datatype_sort array
+ val mk_sorts_s : context -> string array -> Constructor.constructor array array -> datatype_sort array
val get_num_constructors : datatype_sort -> int
- val get_constructors : datatype_sort -> func_decl array
- val get_recognizers : datatype_sort -> func_decl array
- val get_accessors : datatype_sort -> func_decl array array
+ val get_constructors : datatype_sort -> FuncDecl.func_decl array
+ val get_recognizers : datatype_sort -> FuncDecl.func_decl array
+ val get_accessors : datatype_sort -> FuncDecl.func_decl array array
end
module Enumeration :
sig
- val mk_sort : context -> symbol -> symbol array -> enum_sort
+ type enum_sort = EnumSort of Sort.sort
+
+ val sort_of_enum_sort : enum_sort -> Sort.sort
+
+ val mk_sort : context -> Symbol.symbol -> Symbol.symbol array -> enum_sort
val mk_sort_s : context -> string -> string array -> enum_sort
- val get_const_decls : enum_sort -> func_decl array
- val get_tester_decls : enum_sort -> func_decl array
+ val get_const_decls : enum_sort -> FuncDecl.func_decl array
+ val get_tester_decls : enum_sort -> FuncDecl.func_decl array
end
module List_ :
sig
- val mk_sort : context -> symbol -> sort -> list_sort
- val mk_list_s : context -> string -> sort -> list_sort
- val get_nil_decl : list_sort -> func_decl
- val get_is_nil_decl : list_sort -> func_decl
- val get_cons_decl : list_sort -> func_decl
- val get_is_cons_decl : list_sort -> func_decl
- val get_head_decl : list_sort -> func_decl
- val get_tail_decl : list_sort -> func_decl
- val nil : list_sort -> expr
+ type list_sort = ListSort of Sort.sort
+
+ val sort_of_list_sort : list_sort -> Sort.sort
+
+ val mk_sort : context -> Symbol.symbol -> Sort.sort -> list_sort
+ val mk_list_s : context -> string -> Sort.sort -> list_sort
+ val get_nil_decl : list_sort -> FuncDecl.func_decl
+ val get_is_nil_decl : list_sort -> FuncDecl.func_decl
+ val get_cons_decl : list_sort -> FuncDecl.func_decl
+ val get_is_cons_decl : list_sort -> FuncDecl.func_decl
+ val get_head_decl : list_sort -> FuncDecl.func_decl
+ val get_tail_decl : list_sort -> FuncDecl.func_decl
+ val nil : list_sort -> Expr.expr
end
module Tuple :
sig
- val mk_sort :
- context -> symbol -> symbol array -> sort array -> tuple_sort
- val get_mk_decl : tuple_sort -> func_decl
+ type tuple_sort = TupleSort of Sort.sort
+
+ val sort_of_tuple_sort : tuple_sort -> Sort.sort
+
+ val mk_sort : context -> Symbol.symbol -> Symbol.symbol array -> Sort.sort array -> tuple_sort
+ val get_mk_decl : tuple_sort -> FuncDecl.func_decl
val get_num_fields : tuple_sort -> int
- val get_field_decls : tuple_sort -> func_decl array
+ val get_field_decls : tuple_sort -> FuncDecl.func_decl array
end
-module Arithmetic :
+module rec Arithmetic :
sig
+ type arith_sort = ArithSort of Sort.sort
+ type arith_expr = ArithExpr of Expr.expr
- module Integer :
+ val sort_of_arith_sort : Arithmetic.arith_sort -> Sort.sort
+ val arith_sort_of_sort : Sort.sort -> Arithmetic.arith_sort
+ val expr_of_arith_expr : Arithmetic.arith_expr -> Expr.expr
+ val arith_expr_of_expr : Expr.expr -> Arithmetic.arith_expr
+
+ module rec Integer :
sig
+ type int_sort = IntSort of arith_sort
+ type int_expr = IntExpr of arith_expr
+ type int_num = IntNum of int_expr
+
+ val arith_sort_of_int_sort : Arithmetic.Integer.int_sort -> Arithmetic.arith_sort
+ val int_sort_of_arith_sort : Arithmetic.arith_sort -> Arithmetic.Integer.int_sort
+ val arith_expr_of_int_expr : Arithmetic.Integer.int_expr -> Arithmetic.arith_expr
+ val int_expr_of_int_num : Arithmetic.Integer.int_num -> Arithmetic.Integer.int_expr
+ val int_expr_of_arith_expr : Arithmetic.arith_expr -> Arithmetic.Integer.int_expr
+ val int_num_of_int_expr : Arithmetic.Integer.int_expr -> Arithmetic.Integer.int_num
+
val mk_sort : context -> int_sort
val get_int : int_num -> int
val to_string : int_num -> string
- val mk_int_const : context -> symbol -> int_expr
+ val mk_int_const : context -> Symbol.symbol -> int_expr
val mk_int_const_s : context -> string -> int_expr
- val mk_mod : context -> int_expr -> int_expr -> expr
- val mk_rem : context -> int_expr -> int_expr -> expr
+ val mk_mod : context -> int_expr -> int_expr -> int_expr
+ val mk_rem : context -> int_expr -> int_expr -> int_expr
val mk_int_numeral_s : context -> string -> int_num
val mk_int_numeral_i : context -> int -> int_num
- val mk_int2real : context -> int_expr -> real_expr
- val mk_int2bv : context -> int -> int_expr -> bitvec_expr
+ val mk_int2real : context -> int_expr -> Real.real_expr
+ val mk_int2bv : context -> int -> int_expr -> BitVector.bitvec_expr
end
- module Real :
+ and Real :
sig
+ type real_sort = RealSort of arith_sort
+ type real_expr = RealExpr of arith_expr
+ type rat_num = RatNum of real_expr
+
+ val arith_sort_of_real_sort : Arithmetic.Real.real_sort -> Arithmetic.arith_sort
+ val real_sort_of_arith_sort : Arithmetic.arith_sort -> Arithmetic.Real.real_sort
+ val arith_expr_of_real_expr : Arithmetic.Real.real_expr -> Arithmetic.arith_expr
+ val real_expr_of_rat_num : Arithmetic.Real.rat_num -> Arithmetic.Real.real_expr
+ val real_expr_of_arith_expr : Arithmetic.arith_expr -> Arithmetic.Real.real_expr
+ val rat_num_of_real_expr : Arithmetic.Real.real_expr -> Arithmetic.Real.rat_num
+
val mk_sort : context -> real_sort
- val get_numerator : rat_num -> int_num
- val get_denominator : rat_num -> int_num
+ val get_numerator : rat_num -> Integer.int_num
+ val get_denominator : rat_num -> Integer.int_num
val to_decimal_string : rat_num -> int -> string
val to_string : rat_num -> string
- val mk_real_const : context -> symbol -> real_expr
+ val mk_real_const : context -> Symbol.symbol -> real_expr
val mk_real_const_s : context -> string -> real_expr
val mk_numeral_nd : context -> int -> int -> rat_num
val mk_numeral_s : context -> string -> rat_num
val mk_numeral_i : context -> int -> rat_num
- val mk_is_integer : context -> real_expr -> bool_expr
- val mk_real2int : context -> real_expr -> int_expr
+ val mk_is_integer : context -> real_expr -> Boolean.bool_expr
+ val mk_real2int : context -> real_expr -> Integer.int_expr
end
- module AlgebraicNumber :
+ and AlgebraicNumber :
sig
- val to_upper : algebraic_num -> int -> rat_num
- val to_lower : algebraic_num -> int -> rat_num
+ type algebraic_num = AlgebraicNum of arith_expr
+
+ val arith_expr_of_algebraic_num : Arithmetic.AlgebraicNumber.algebraic_num -> Arithmetic.arith_expr
+ val algebraic_num_of_arith_expr : Arithmetic.arith_expr -> Arithmetic.AlgebraicNumber.algebraic_num
+
+ val to_upper : algebraic_num -> int -> Real.rat_num
+ val to_lower : algebraic_num -> int -> Real.rat_num
val to_decimal_string : algebraic_num -> int -> string
val to_string : algebraic_num -> string
end
- val is_int : expr -> bool
- val is_arithmetic_numeral : expr -> bool
- val is_le : expr -> bool
- val is_ge : expr -> bool
- val is_lt : expr -> bool
- val is_gt : expr -> bool
- val is_add : expr -> bool
- val is_sub : expr -> bool
- val is_uminus : expr -> bool
- val is_mul : expr -> bool
- val is_div : expr -> bool
- val is_idiv : expr -> bool
- val is_remainder : expr -> bool
- val is_modulus : expr -> bool
- val is_inttoreal : expr -> bool
- val is_real_to_int : expr -> bool
- val is_real_is_int : expr -> bool
- val is_real : expr -> bool
- val is_int_numeral : expr -> bool
- val is_rat_num : expr -> bool
- val is_algebraic_number : expr -> bool
+ 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 -> arith_expr
val mk_mul : context -> arith_expr array -> arith_expr
val mk_sub : context -> arith_expr array -> arith_expr
val mk_unary_minus : context -> arith_expr -> arith_expr
val mk_div : context -> arith_expr -> arith_expr -> arith_expr
val mk_power : context -> arith_expr -> arith_expr -> arith_expr
- val mk_lt : context -> arith_expr -> arith_expr -> bool_expr
- val mk_le : context -> arith_expr -> arith_expr -> bool_expr
- val mk_gt : context -> arith_expr -> arith_expr -> bool_expr
- val mk_ge : context -> arith_expr -> arith_expr -> bool_expr
+ val mk_lt : context -> arith_expr -> arith_expr -> Boolean.bool_expr
+ val mk_le : context -> arith_expr -> arith_expr -> Boolean.bool_expr
+ val mk_gt : context -> arith_expr -> arith_expr -> Boolean.bool_expr
+ val mk_ge : context -> arith_expr -> arith_expr -> Boolean.bool_expr
end
-module BitVector :
+and BitVector :
sig
+ type bitvec_sort = BitVecSort of Sort.sort
+ type bitvec_expr = BitVecExpr of Expr.expr
+ type bitvec_num = BitVecNum of bitvec_expr
+
+ val sort_of_bitvec_sort : BitVector.bitvec_sort -> Sort.sort
+ val bitvec_sort_of_sort : Sort.sort -> BitVector.bitvec_sort
+ val expr_of_bitvec_expr : BitVector.bitvec_expr -> Expr.expr
+ val bitvec_expr_of_bitvec_num : BitVector.bitvec_num -> BitVector.bitvec_expr
+ val bitvec_expr_of_expr : Expr.expr -> BitVector.bitvec_expr
+ val bitvec_num_of_bitvec_expr : BitVector.bitvec_expr -> BitVector.bitvec_num
+
val mk_sort : context -> int -> bitvec_sort
- val is_bv : expr -> bool
- val is_bv_numeral : expr -> bool
- val is_bv_bit1 : expr -> bool
- val is_bv_bit0 : expr -> bool
- val is_bv_uminus : expr -> bool
- val is_bv_add : expr -> bool
- val is_bv_sub : expr -> bool
- val is_bv_mul : expr -> bool
- val is_bv_sdiv : expr -> bool
- val is_bv_udiv : expr -> bool
- val is_bv_SRem : expr -> bool
- val is_bv_urem : expr -> bool
- val is_bv_smod : expr -> bool
- val is_bv_sdiv0 : expr -> bool
- val is_bv_udiv0 : expr -> bool
- val is_bv_srem0 : expr -> bool
- val is_bv_urem0 : expr -> bool
- val is_bv_smod0 : expr -> bool
- val is_bv_ule : expr -> bool
- val is_bv_sle : expr -> bool
- val is_bv_uge : expr -> bool
- val is_bv_sge : expr -> bool
- val is_bv_ult : expr -> bool
- val is_bv_slt : expr -> bool
- val is_bv_ugt : expr -> bool
- val is_bv_sgt : expr -> bool
- val is_bv_and : expr -> bool
- val is_bv_or : expr -> bool
- val is_bv_not : expr -> bool
- val is_bv_xor : expr -> bool
- val is_bv_nand : expr -> bool
- val is_bv_nor : expr -> bool
- val is_bv_xnor : expr -> bool
- val is_bv_concat : expr -> bool
- val is_bv_signextension : expr -> bool
- val is_bv_zeroextension : expr -> bool
- val is_bv_extract : expr -> bool
- val is_bv_repeat : expr -> bool
- val is_bv_reduceor : expr -> bool
- val is_bv_reduceand : expr -> bool
- val is_bv_comp : expr -> bool
- val is_bv_shiftleft : expr -> bool
- val is_bv_shiftrightlogical : expr -> bool
- val is_bv_shiftrightarithmetic : expr -> bool
- val is_bv_rotateleft : expr -> bool
- val is_bv_rotateright : expr -> bool
- val is_bv_rotateleftextended : expr -> bool
- val is_bv_rotaterightextended : expr -> bool
- val is_int_to_bv : expr -> bool
- val is_bv_to_int : expr -> bool
- val is_bv_carry : expr -> bool
- val is_bv_xor3 : expr -> bool
+ val is_bv : Expr.expr -> bool
+ val is_bv_numeral : Expr.expr -> bool
+ val is_bv_bit1 : Expr.expr -> bool
+ val is_bv_bit0 : Expr.expr -> bool
+ val is_bv_uminus : Expr.expr -> bool
+ val is_bv_add : Expr.expr -> bool
+ val is_bv_sub : Expr.expr -> bool
+ val is_bv_mul : Expr.expr -> bool
+ val is_bv_sdiv : Expr.expr -> bool
+ val is_bv_udiv : Expr.expr -> bool
+ val is_bv_SRem : Expr.expr -> bool
+ val is_bv_urem : Expr.expr -> bool
+ val is_bv_smod : Expr.expr -> bool
+ val is_bv_sdiv0 : Expr.expr -> bool
+ val is_bv_udiv0 : Expr.expr -> bool
+ val is_bv_srem0 : Expr.expr -> bool
+ val is_bv_urem0 : Expr.expr -> bool
+ val is_bv_smod0 : Expr.expr -> bool
+ val is_bv_ule : Expr.expr -> bool
+ val is_bv_sle : Expr.expr -> bool
+ val is_bv_uge : Expr.expr -> bool
+ val is_bv_sge : Expr.expr -> bool
+ val is_bv_ult : Expr.expr -> bool
+ val is_bv_slt : Expr.expr -> bool
+ val is_bv_ugt : Expr.expr -> bool
+ val is_bv_sgt : Expr.expr -> bool
+ val is_bv_and : Expr.expr -> bool
+ val is_bv_or : Expr.expr -> bool
+ val is_bv_not : Expr.expr -> bool
+ val is_bv_xor : Expr.expr -> bool
+ val is_bv_nand : Expr.expr -> bool
+ val is_bv_nor : Expr.expr -> bool
+ val is_bv_xnor : Expr.expr -> bool
+ val is_bv_concat : Expr.expr -> bool
+ val is_bv_signextension : Expr.expr -> bool
+ val is_bv_zeroextension : Expr.expr -> bool
+ val is_bv_extract : Expr.expr -> bool
+ val is_bv_repeat : Expr.expr -> bool
+ val is_bv_reduceor : Expr.expr -> bool
+ val is_bv_reduceand : Expr.expr -> bool
+ val is_bv_comp : Expr.expr -> bool
+ val is_bv_shiftleft : Expr.expr -> bool
+ val is_bv_shiftrightlogical : Expr.expr -> bool
+ val is_bv_shiftrightarithmetic : Expr.expr -> bool
+ val is_bv_rotateleft : Expr.expr -> bool
+ val is_bv_rotateright : Expr.expr -> bool
+ val is_bv_rotateleftextended : Expr.expr -> bool
+ val is_bv_rotaterightextended : Expr.expr -> bool
+ val is_int_to_bv : Expr.expr -> bool
+ val is_bv_to_int : Expr.expr -> bool
+ val is_bv_carry : Expr.expr -> bool
+ val is_bv_xor3 : Expr.expr -> bool
val get_size : bitvec_sort -> int
val get_int : bitvec_num -> int
val to_string : bitvec_num -> string
- val mk_const : context -> symbol -> int -> bitvec_expr
+ val mk_const : context -> Symbol.symbol -> int -> bitvec_expr
val mk_const_s : context -> string -> int -> bitvec_expr
- val mk_not : context -> bitvec_expr -> expr
- val mk_redand : context -> bitvec_expr -> expr
- val mk_redor : context -> bitvec_expr -> expr
- val mk_and : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_or : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_xor : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_nand : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_nor : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_xnor : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_neg : context -> bitvec_expr -> expr
- val mk_add : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_sub : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_mul : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_udiv : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_sdiv : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_urem : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_srem : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_smod : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_ult : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_slt : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_ule : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_sle : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_uge : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_sge : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_ugt : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_sgt : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_concat : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_extract : context -> int -> int -> bitvec_expr -> expr
- val mk_sign_ext : context -> int -> bitvec_expr -> expr
- val mk_zero_ext : context -> int -> bitvec_expr -> expr
- val mk_repeat : context -> int -> bitvec_expr -> expr
- val mk_shl : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_lshr : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_ashr : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_rotate_left : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_rotate_right : context -> bitvec_expr -> bitvec_expr -> expr
- val mk_bv2int : context -> bitvec_expr -> bool -> int_expr
- val mk_add_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> bool_expr
- val mk_add_no_underflow : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_sub_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_sub_no_underflow : context -> bitvec_expr -> bitvec_expr -> bool -> bool_expr
- val mk_sdiv_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool_expr
- val mk_neg_no_overflow : context -> bitvec_expr -> bool_expr
- val mk_mul_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> bool_expr
- val mk_mul_no_underflow : context -> bitvec_expr -> bitvec_expr -> bool_expr
+ val mk_not : context -> bitvec_expr -> Expr.expr
+ val mk_redand : context -> bitvec_expr -> Expr.expr
+ val mk_redor : context -> bitvec_expr -> Expr.expr
+ val mk_and : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_or : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_xor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_nand : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_nor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_xnor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_neg : context -> bitvec_expr -> bitvec_expr
+ val mk_add : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_sub : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_mul : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_udiv : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_sdiv : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_urem : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_srem : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_smod : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_ult : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_slt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_ule : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sle : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_uge : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sge : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_ugt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sgt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_concat : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_extract : context -> int -> int -> bitvec_expr -> bitvec_expr
+ val mk_sign_ext : context -> int -> bitvec_expr -> bitvec_expr
+ val mk_zero_ext : context -> int -> bitvec_expr -> bitvec_expr
+ val mk_repeat : context -> int -> bitvec_expr -> bitvec_expr
+ val mk_shl : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_lshr : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_ashr : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_rotate_left : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_rotate_right : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
+ val mk_bv2int : context -> bitvec_expr -> bool -> Arithmetic.Integer.int_expr
+ val mk_add_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr
+ val mk_add_no_underflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sub_no_overflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_sub_no_underflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr
+ val mk_sdiv_no_overflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
+ val mk_neg_no_overflow : context -> bitvec_expr -> Boolean.bool_expr
+ val mk_mul_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr
+ val mk_mul_no_underflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr
val mk_numeral : context -> string -> int -> bitvec_num
end
module Proof :
sig
- val is_true : expr -> bool
- val is_asserted : expr -> bool
- val is_goal : expr -> bool
- val is_modus_ponens : expr -> bool
- val is_reflexivity : expr -> bool
- val is_symmetry : expr -> bool
- val is_transitivity : expr -> bool
- val is_Transitivity_star : expr -> bool
- val is_monotonicity : expr -> bool
- val is_quant_intro : expr -> bool
- val is_distributivity : expr -> bool
- val is_and_elimination : expr -> bool
- val is_or_elimination : expr -> bool
- val is_rewrite : expr -> bool
- val is_rewrite_star : expr -> bool
- val is_pull_quant : expr -> bool
- val is_pull_quant_star : expr -> bool
- val is_push_quant : expr -> bool
- val is_elim_unused_vars : expr -> bool
- val is_der : expr -> bool
- val is_quant_inst : expr -> bool
- val is_hypothesis : expr -> bool
- val is_lemma : expr -> bool
- val is_unit_resolution : expr -> bool
- val is_iff_true : expr -> bool
- val is_iff_false : expr -> bool
- val is_commutativity : expr -> bool
- val is_def_axiom : expr -> bool
- val is_def_intro : expr -> bool
- val is_apply_def : expr -> bool
- val is_iff_oeq : expr -> bool
- val is_nnf_pos : expr -> bool
- val is_nnf_neg : expr -> bool
- val is_nnf_star : expr -> bool
- val is_cnf_star : expr -> bool
- val is_skolemize : expr -> bool
- val is_modus_ponens_oeq : expr -> bool
- val is_theory_lemma : expr -> bool
+ val is_true : Expr.expr -> bool
+ val is_asserted : Expr.expr -> bool
+ val is_goal : Expr.expr -> bool
+ val is_modus_ponens : Expr.expr -> bool
+ val is_reflexivity : Expr.expr -> bool
+ val is_symmetry : Expr.expr -> bool
+ val is_transitivity : Expr.expr -> bool
+ val is_Transitivity_star : Expr.expr -> bool
+ val is_monotonicity : Expr.expr -> bool
+ val is_quant_intro : Expr.expr -> bool
+ val is_distributivity : Expr.expr -> bool
+ val is_and_elimination : Expr.expr -> bool
+ val is_or_elimination : Expr.expr -> bool
+ val is_rewrite : Expr.expr -> bool
+ val is_rewrite_star : Expr.expr -> bool
+ val is_pull_quant : Expr.expr -> bool
+ val is_pull_quant_star : Expr.expr -> bool
+ val is_push_quant : Expr.expr -> bool
+ val is_elim_unused_vars : Expr.expr -> bool
+ val is_der : Expr.expr -> bool
+ val is_quant_inst : Expr.expr -> bool
+ val is_hypothesis : Expr.expr -> bool
+ val is_lemma : Expr.expr -> bool
+ val is_unit_resolution : Expr.expr -> bool
+ val is_iff_true : Expr.expr -> bool
+ val is_iff_false : Expr.expr -> bool
+ val is_commutativity : Expr.expr -> bool
+ val is_def_axiom : Expr.expr -> bool
+ val is_def_intro : Expr.expr -> bool
+ val is_apply_def : Expr.expr -> bool
+ val is_iff_oeq : Expr.expr -> bool
+ val is_nnf_pos : Expr.expr -> bool
+ val is_nnf_neg : Expr.expr -> bool
+ val is_nnf_star : Expr.expr -> bool
+ val is_cnf_star : Expr.expr -> bool
+ val is_skolemize : Expr.expr -> bool
+ val is_modus_ponens_oeq : Expr.expr -> bool
+ val is_theory_lemma : Expr.expr -> bool
end
+
module Goal :
sig
+ type goal
+
val get_precision : goal -> Z3enums.goal_prec
val is_precise : goal -> bool
val is_underapproximation : goal -> bool
val is_overapproximation : goal -> bool
val is_garbage : goal -> bool
- val assert_ : goal -> bool_expr array -> unit
+ val assert_ : goal -> Boolean.bool_expr array -> unit
val is_inconsistent : goal -> bool
val get_depth : goal -> int
val reset : goal -> unit
val get_size : goal -> int
- val get_formulas : goal -> bool_expr array
+ val get_formulas : goal -> Boolean.bool_expr array
val get_num_exprs : goal -> int
val is_decided_sat : goal -> bool
val is_decided_unsat : goal -> bool
val translate : goal -> context -> goal
- val simplify : goal -> params option -> goal
+ val simplify : goal -> Params.params option -> goal
val mk_goal : context -> bool -> bool -> bool -> goal
val to_string : goal -> string
end
module Model :
sig
+ type model
module FuncInterp :
sig
-
+ type func_interp
+
module FuncEntry :
sig
- val get_value : func_entry -> expr
+ type func_entry
+
+ val get_value : func_entry -> Expr.expr
val get_num_args : func_entry -> int
- val get_args : func_entry -> expr array
+ val get_args : func_entry -> Expr.expr array
val to_string : func_entry -> string
end
val get_num_entries : func_interp -> int
- val get_entries : func_interp -> func_entry array
- val get_else : func_interp -> expr
+ val get_entries : func_interp -> FuncEntry.func_entry array
+ val get_else : func_interp -> Expr.expr
val get_arity : func_interp -> int
val to_string : func_interp -> string
end
- val get_const_interp : model -> func_decl -> expr option
- val get_const_interp_e : model -> expr -> expr option
- val get_func_interp : model -> func_decl -> func_interp option
+ val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option
+ val get_const_interp_e : model -> Expr.expr -> Expr.expr option
+ val get_func_interp : model -> FuncDecl.func_decl -> FuncInterp.func_interp option
val get_num_consts : model -> int
- val get_const_decls : model -> func_decl array
+ val get_const_decls : model -> FuncDecl.func_decl array
val get_num_funcs : model -> int
- val get_func_decls : model -> func_decl array
- val get_decls : model -> func_decl array
+ val get_func_decls : model -> FuncDecl.func_decl array
+ val get_decls : model -> FuncDecl.func_decl array
exception ModelEvaluationFailedException of string
- val eval : model -> expr -> bool -> expr
- val evaluate : model -> expr -> bool -> expr
+ val eval : model -> Expr.expr -> bool -> Expr.expr
+ val evaluate : model -> Expr.expr -> bool -> Expr.expr
val get_num_sorts : model -> int
- val get_sorts : model -> sort array
- val sort_universe : model -> sort -> ast_vector array
+ val get_sorts : model -> Sort.sort array
+ val sort_universe : model -> Sort.sort -> AST.ASTVector.ast_vector array
val to_string : model -> string
end
module Probe :
sig
- val apply : probe -> goal -> float
+ type probe
+
+ val apply : probe -> Goal.goal -> float
val get_num_probes : context -> int
val get_probe_names : context -> string array
val get_probe_description : context -> string -> string
@@ -838,19 +1179,22 @@ end
module Tactic :
sig
+ type tactic
module ApplyResult :
sig
+ type apply_result
+
val get_num_subgoals : apply_result -> int
- val get_subgoals : apply_result -> goal array
- val get_subgoal : apply_result -> int -> goal
- val convert_model : apply_result -> int -> model -> model
+ val get_subgoals : apply_result -> Goal.goal array
+ val get_subgoal : apply_result -> int -> Goal.goal
+ val convert_model : apply_result -> int -> Model.model -> Model.model
val to_string : apply_result -> string
end
val get_help : tactic -> string
- val get_param_descrs : tactic -> param_descrs
- val apply : tactic -> goal -> params option -> apply_result
+ val get_param_descrs : tactic -> Params.ParamDescrs.param_descrs
+ val apply : tactic -> Goal.goal -> Params.params option -> ApplyResult.apply_result
val get_num_tactics : context -> int
val get_tactic_names : context -> string array
val get_tactic_description : context -> string -> string
@@ -858,15 +1202,15 @@ sig
val and_then : context -> tactic -> tactic -> tactic array -> tactic
val or_else : context -> tactic -> tactic -> tactic
val try_for : context -> tactic -> int -> tactic
- val when_ : context -> probe -> tactic -> tactic
- val cond : context -> probe -> tactic -> tactic -> tactic
+ val when_ : context -> Probe.probe -> tactic -> tactic
+ val cond : context -> Probe.probe -> tactic -> tactic -> tactic
val repeat : context -> tactic -> int -> tactic
val skip : context -> tactic
val fail : context -> tactic
- val fail_if : context -> probe -> tactic
+ val fail_if : context -> Probe.probe -> tactic
val fail_if_not_decided : context -> tactic
- val using_params : context -> tactic -> params -> tactic
- val with_ : context -> tactic -> params -> tactic
+ val using_params : context -> tactic -> Params.params -> tactic
+ val with_ : context -> tactic -> Params.params -> tactic
val par_or : context -> tactic array -> tactic
val par_and_then : context -> tactic -> tactic -> tactic
val interrupt : context -> unit
@@ -874,13 +1218,19 @@ end
module Solver :
sig
+ type solver
+ type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
+
val string_of_status : status -> string
module Statistics :
sig
+ type statistics
module Entry :
sig
+ type statistics_entry
+
val get_key : statistics_entry -> string
val get_int : statistics_entry -> int
val get_float : statistics_entry -> float
@@ -892,59 +1242,61 @@ sig
val to_string : statistics -> string
val get_size : statistics -> int
- val get_entries : statistics -> statistics_entry array
+ val get_entries : statistics -> Entry.statistics_entry array
val get_keys : statistics -> string array
- val get : statistics -> string -> statistics_entry option
+ val get : statistics -> string -> Entry.statistics_entry option
end
val get_help : solver -> string
- val set_parameters : solver -> params -> unit
- val get_param_descrs : solver -> param_descrs
+ val set_parameters : solver -> Params.params -> unit
+ val get_param_descrs : solver -> Params.ParamDescrs.param_descrs
val get_num_scopes : solver -> int
val push : solver -> unit
val pop : solver -> int -> unit
val reset : solver -> unit
- val assert_ : solver -> bool_expr array -> unit
- val assert_and_track : solver -> bool_expr -> bool_expr -> unit
+ val assert_ : solver -> Boolean.bool_expr array -> unit
+ val assert_and_track : solver -> Boolean.bool_expr -> Boolean.bool_expr -> unit
val get_num_assertions : solver -> int
- val get_assertions : solver -> bool_expr array
- val check : solver -> bool_expr array -> status
- val get_model : solver -> model option
- val get_proof : solver -> expr option
- val get_unsat_core : solver -> ast_vector array
+ val get_assertions : solver -> Boolean.bool_expr array
+ val check : solver -> Boolean.bool_expr array -> status
+ val get_model : solver -> Model.model option
+ val get_proof : solver -> Expr.expr option
+ val get_unsat_core : solver -> AST.ASTVector.ast_vector array
val get_reason_unknown : solver -> string
- val get_statistics : solver -> statistics
- val mk_solver : context -> symbol option -> solver
+ val get_statistics : solver -> Statistics.statistics
+ val mk_solver : context -> Symbol.symbol option -> solver
val mk_solver_s : context -> string -> solver
val mk_simple_solver : context -> solver
- val mk_solver_t : context -> tactic -> solver
+ val mk_solver_t : context -> Tactic.tactic -> solver
val to_string : solver -> string
end
module Fixedpoint :
sig
+ type fixedpoint
+
val get_help : fixedpoint -> string
- val set_params : fixedpoint -> params -> unit
- val get_param_descrs : fixedpoint -> param_descrs
- val assert_ : fixedpoint -> bool_expr array -> unit
- val register_relation : fixedpoint -> func_decl -> unit
- val add_rule : fixedpoint -> bool_expr -> symbol option -> unit
- val add_fact : fixedpoint -> func_decl -> int array -> unit
- val query : fixedpoint -> bool_expr -> status
- val query_r : fixedpoint -> func_decl array -> status
+ val set_params : fixedpoint -> Params.params -> unit
+ val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs
+ val assert_ : fixedpoint -> Boolean.bool_expr array -> unit
+ val register_relation : fixedpoint -> FuncDecl.func_decl -> unit
+ val add_rule : fixedpoint -> Boolean.bool_expr -> Symbol.symbol option -> unit
+ val add_fact : fixedpoint -> FuncDecl.func_decl -> int array -> unit
+ val query : fixedpoint -> Boolean.bool_expr -> Solver.status
+ val query_r : fixedpoint -> FuncDecl.func_decl array -> Solver.status
val push : fixedpoint -> unit
val pop : fixedpoint -> unit
- val update_rule : fixedpoint -> bool_expr -> symbol -> unit
- val get_answer : fixedpoint -> expr option
+ val update_rule : fixedpoint -> Boolean.bool_expr -> Symbol.symbol -> unit
+ val get_answer : fixedpoint -> Expr.expr option
val get_reason_unknown : fixedpoint -> string
- val get_num_levels : fixedpoint -> func_decl -> int
- val get_cover_delta : fixedpoint -> int -> func_decl -> expr option
- val add_cover : fixedpoint -> int -> func_decl -> expr -> unit
+ val get_num_levels : fixedpoint -> FuncDecl.func_decl -> int
+ val get_cover_delta : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr option
+ val add_cover : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr -> unit
val to_string : fixedpoint -> string
- val set_predicate_representation : fixedpoint -> func_decl -> symbol array -> unit
- val to_string_q : fixedpoint -> bool_expr array -> string
- val get_rules : fixedpoint -> bool_expr array
- val get_assertions : fixedpoint -> bool_expr array
+ val set_predicate_representation : fixedpoint -> FuncDecl.func_decl -> Symbol.symbol array -> unit
+ val to_string_q : fixedpoint -> Boolean.bool_expr array -> string
+ val get_rules : fixedpoint -> Boolean.bool_expr array
+ val get_assertions : fixedpoint -> Boolean.bool_expr array
val mk_fixedpoint : context -> fixedpoint
end
@@ -958,19 +1310,19 @@ end
module SMT :
sig
- val benchmark_to_smtstring : context -> string -> string -> string -> string -> bool_expr array -> bool_expr -> string
- val parse_smtlib_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit
- val parse_smtlib_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> unit
+ val benchmark_to_smtstring : context -> string -> string -> string -> string -> Boolean.bool_expr array -> Boolean.bool_expr -> string
+ val parse_smtlib_string : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> unit
+ val parse_smtlib_file : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> unit
val get_num_smtlib_formulas : context -> int
- val get_smtlib_formulas : context -> bool_expr array
+ val get_smtlib_formulas : context -> Boolean.bool_expr array
val get_num_smtlib_assumptions : context -> int
- val get_smtlib_assumptions : context -> bool_expr array
+ val get_smtlib_assumptions : context -> Boolean.bool_expr array
val get_num_smtlib_decls : context -> int
- val get_smtlib_decls : context -> func_decl array
+ val get_smtlib_decls : context -> FuncDecl.func_decl array
val get_num_smtlib_sorts : context -> int
- val get_smtlib_sorts : context -> sort array
- val parse_smtlib2_string : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> bool_expr
- val parse_smtlib2_file : context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> bool_expr
+ val get_smtlib_sorts : context -> Sort.sort array
+ val parse_smtlib2_string : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> Boolean.bool_expr
+ val parse_smtlib2_file : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> Boolean.bool_expr
end
val set_global_param : string -> string -> unit