diff --git a/scripts/update_api.py b/scripts/update_api.py
index fba194bac..4669b78fc 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -334,6 +334,8 @@ def param2ml(p):
return "ptr"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s array" % type2ml(param_type(p))
+ elif k == OUT_MANAGED_ARRAY:
+ return "%s array" % type2ml(param_type(p));
else:
return type2ml(param_type(p))
@@ -1067,7 +1069,7 @@ def ml_method_name(name):
return name[3:] # Remove Z3_
def is_out_param(p):
- if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
+ if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY:
return True
else:
return False
@@ -1411,6 +1413,8 @@ def mk_ml():
type2str(param_type(param)),
type2str(param_type(param)),
param_array_capacity_pos(param)))
+ elif k == OUT_MANAGED_ARRAY:
+ ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
@@ -1449,7 +1453,7 @@ def mk_ml():
else:
ml_wrapper.write(', ')
k = param_kind(param)
- if k == OUT or k == INOUT:
+ if k == OUT or k == INOUT or k == OUT_MANAGED_ARRAY:
ml_wrapper.write('&_a%s' % i)
else:
ml_wrapper.write('_a%i' % i)
@@ -1465,6 +1469,8 @@ def mk_ml():
if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p)))
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { value t; %s Store_field(_a%s_val, _i, t); }\n' % (param_array_capacity_pos(p), ml_set_wrap(param_type(p), 't', '_a' + str(i) + '[_i]'), i))
+ elif param_kind(p) == OUT_MANAGED_ARRAY:
+ ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
elif is_out_param(p):
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
i = i + 1
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 013101398..2b54a1113 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -165,7 +165,7 @@ struct
let symbol_lton ( a : symbol list ) =
let f ( e : symbol ) = (gno e) in
Array.of_list (List.map f a)
-
+
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
let is_string_symbol ( o : symbol ) = (kind o) == STRING_SYMBOL
@@ -213,7 +213,7 @@ struct
module ASTVector =
struct
type ast_vector = z3_native_object
-
+
let create ( ctx : context ) ( no : Z3native.ptr ) =
let res : ast_vector = { m_ctx = ctx ;
m_n_obj = null ;
@@ -224,7 +224,7 @@ struct
res
let mk_ast_vector ( ctx : context ) = (create ctx (Z3native.mk_ast_vector (context_gno ctx)))
-
+
let get_size ( x : ast_vector ) =
Z3native.ast_vector_size (z3obj_gnc x) (z3obj_gno x)
@@ -259,7 +259,7 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
-
+
let mk_ast_map ( ctx : context ) = (create ctx (Z3native.mk_ast_map (context_gno ctx)))
let astmap_of_ptr ( ctx : context ) ( no : Z3native.ptr ) =
@@ -330,7 +330,7 @@ struct
if (get_id a) < (get_id b) then -1 else
if (get_id a) > (get_id b) then 1 else
0
-
+
let translate ( x : ast ) ( to_ctx : context ) =
if (z3obj_gnc x) == (context_gno to_ctx) then
x
@@ -366,7 +366,7 @@ struct
| UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered")
let ast_of_sort s = match s with Sort(x) -> x
-
+
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))
@@ -378,7 +378,7 @@ struct
let sort_option_lton ( a : sort option list ) =
let f ( e : sort option ) = match e with None -> null | Some(Sort(a)) -> (AST.ptr_of_ast a) in
Array.of_list (List.map f a)
-
+
let equal : sort -> sort -> bool = fun a b ->
(a == b) ||
if (gnc a) != (gnc b) then
@@ -629,7 +629,6 @@ sig
val to_string : params -> string
val update_param_value : context -> string -> string -> unit
- val get_param_value : context -> string -> string option
val set_print_mode : context -> Z3enums.ast_print_mode -> unit
end = struct
type params = z3_native_object
@@ -688,13 +687,6 @@ end = struct
let update_param_value ( ctx : context ) ( id : string) ( value : string )=
Z3native.update_param_value (context_gno ctx) id value
- let get_param_value ( ctx : context ) ( id : string ) =
- let (r, v) = (Z3native.get_param_value (context_gno ctx) id) in
- if not r then
- None
- else
- Some v
-
let set_print_mode ( ctx : context ) ( value : ast_print_mode ) =
Z3native.set_ast_print_mode (context_gno ctx) (int_of_ast_print_mode value)
end
@@ -826,11 +818,11 @@ end = struct
let is_well_sorted ( x : expr ) = Z3native.is_well_sorted (gnc x) (gno x)
let get_sort ( x : expr ) = sort_of_ptr (Expr.gc x) (Z3native.get_sort (gnc x) (gno x))
-
+
let is_const ( x : expr ) = (match x with Expr(a) -> (AST.is_app a)) &&
(get_num_args x) == 0 &&
(FuncDecl.get_domain_size (get_func_decl x)) == 0
-
+
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))
@@ -851,7 +843,7 @@ end = struct
expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty))
let equal ( a : expr ) ( b : expr ) = AST.equal (ast_of_expr a) (ast_of_expr b)
-
+
let compare a b = AST.compare (ast_of_expr a) (ast_of_expr b)
end
@@ -941,7 +933,7 @@ struct
raise (Z3native.Exception "Invalid coercion")
else
Quantifier(e)
-
+
let gc ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gc e)
let gnc ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gnc e)
let gno ( x : quantifier ) = match (x) with Quantifier(e) -> (Expr.gno e)
@@ -949,13 +941,13 @@ 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? *)
+ (* 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)
@@ -1258,11 +1250,11 @@ struct
module Constructor =
struct
type constructor = z3_native_object
-
+
module FieldNumTable = Hashtbl.Make(struct
- type t = AST.ast
- let equal x y = AST.compare x y = 0
- let hash = AST.hash
+ type t = AST.ast
+ let equal x y = AST.compare x y = 0
+ let hash = AST.hash
end)
let _field_nums = FieldNumTable.create 0
@@ -1291,7 +1283,7 @@ struct
Gc.finalise f no ;
FieldNumTable.add _field_nums no n ;
no
-
+
let get_num_fields ( x : constructor ) = FieldNumTable.find _field_nums x
let get_constructor_decl ( x : constructor ) =
@@ -1613,16 +1605,16 @@ struct
let mk_sub ( ctx : context ) ( t : expr list ) =
let f x = (Expr.gno x) in
- (expr_of_ptr ctx (Z3native.mk_sub (context_gno ctx) (List.length t) (Array.of_list (List.map f t))))
+ (expr_of_ptr ctx (Z3native.mk_sub (context_gno ctx) (List.length t) (Array.of_list (List.map f t))))
let mk_unary_minus ( ctx : context ) ( t : expr ) =
- (expr_of_ptr ctx (Z3native.mk_unary_minus (context_gno ctx) (Expr.gno t)))
+ (expr_of_ptr ctx (Z3native.mk_unary_minus (context_gno ctx) (Expr.gno t)))
let mk_div ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
- (expr_of_ptr ctx (Z3native.mk_div (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
+ (expr_of_ptr ctx (Z3native.mk_div (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
let mk_power ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
- (expr_of_ptr ctx (Z3native.mk_power (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
+ (expr_of_ptr ctx (Z3native.mk_power (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
(expr_of_ptr ctx (Z3native.mk_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
@@ -1893,7 +1885,7 @@ struct
let get_formulas ( x : goal ) =
let n = get_size x in
let f i = ((expr_of_ptr (z3obj_gc x)
- (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i))) in
+ (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i))) in
mk_list f n
let get_num_exprs ( x : goal ) = Z3native.goal_num_exprs (z3obj_gnc x) (z3obj_gno x)
@@ -2065,7 +2057,7 @@ struct
let f i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in
let g i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in
(mk_list f n_funcs) @ (mk_list g n_consts)
-
+
let eval ( x : model ) ( t : expr ) ( completion : bool ) =
let (r, v) = (Z3native.model_eval (z3obj_gnc x) (z3obj_gno x) (Expr.gno t) completion) in
if not r then
@@ -2316,7 +2308,7 @@ struct
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 ;
@@ -2644,7 +2636,7 @@ struct
mk_list f n
let get_num_smtlib_sorts ( ctx : context ) = Z3native.get_smtlib_num_sorts (context_gno ctx)
-
+
let get_smtlib_sorts ( ctx : context ) =
let n = (get_num_smtlib_sorts ctx) in
let f i = (sort_of_ptr ctx (Z3native.get_smtlib_sort (context_gno ctx) i)) in
@@ -2683,6 +2675,65 @@ struct
(let f x = FuncDecl.gno x in (Array.of_list (List.map f decls)))))
end
+module Interpolation =
+struct
+ let mk_interpolant ( ctx : context ) ( a : expr ) =
+ (expr_of_ptr ctx (Z3native.mk_interpolant (context_gno ctx) (Expr.gno a)))
+
+ let mk_interpolation_context ( settings : ( string * string ) list ) =
+ let cfg = Z3native.mk_config () in
+ let f e = (Z3native.set_param_value cfg (fst e) (snd e)) in
+ (List.iter f settings) ;
+ let v = Z3native.mk_interpolation_context cfg in
+ Z3native.del_config(cfg) ;
+ Z3native.set_ast_print_mode v (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ;
+ Z3native.set_internal_error_handler v ;
+ let res = { m_n_ctx = v; m_n_obj_cnt = 0 } in
+ let f = fun o -> dispose_context o in
+ Gc.finalise f res;
+ res
+
+ let get_interpolant ( ctx : context ) ( pf : expr ) ( pat: expr ) ( p : Params.params ) =
+ (ASTVector.create ctx (Z3native.get_interpolant (context_gno ctx) (Expr.gno pf) (Expr.gno pat) (z3obj_gno p)))
+
+ let compute_interpolant ( ctx : context ) ( pat : expr ) ( p : Params.params ) =
+ let (r, interp, model) = (Z3native.compute_interpolant (context_gno ctx) (Expr.gno pat) (z3obj_gno p)) in
+ match (lbool_of_int r) with
+ | L_TRUE -> ((ASTVector.create ctx interp), (Model.create ctx model))
+ | _ -> raise (Z3native.Exception "Error computing interpolant.")
+
+ let get_interpolation_profile ( ctx : context ) =
+ (Z3native.interpolation_profile (context_gno ctx))
+
+ let read_interpolation_problem ( ctx : context ) ( filename : string ) =
+ let (r, num, cnsts, parents, error, num_theory, theory) = (Z3native.read_interpolation_problem (context_gno ctx) filename) in
+ match r with
+ | 0 -> raise (Z3native.Exception "Interpolation problem could not be read.")
+ | _ ->
+ let f1 i = (expr_of_ptr ctx (Array.get cnsts i)) in
+ let f2 i = (Array.get parents i) in
+ let f3 i = (expr_of_ptr ctx (Array.get theory i)) in
+ ((mk_list f1 num),
+ (mk_list f2 num),
+ (mk_list f3 num_theory))
+
+ let check_interpolant ( ctx : context ) ( num : int ) ( cnsts : Expr.expr list ) ( parents : int list ) ( interps : Expr.expr list ) ( num_theory : int ) ( theory : Expr.expr list ) =
+ let (r, str) = (Z3native.check_interpolant (context_gno ctx)
+ num
+ (let f x = Expr.gno x in (Array.of_list (List.map f cnsts)))
+ (Array.of_list parents)
+ (let f x = Expr.gno x in (Array.of_list (List.map f interps)))
+ num_theory
+ (let f x = Expr.gno x in (Array.of_list (List.map f theory)))) in
+ match (lbool_of_int r) with
+ | L_UNDEF -> raise (Z3native.Exception "Interpolant could not be verified.")
+ | L_FALSE -> raise (Z3native.Exception "Interpolant could not be verified.")
+ | _ -> ()
+
+ let write_interpolation_problem ( ctx : context ) ( num : int ) ( cnsts : Expr.expr list ) ( parents : int list ) ( filename : string ) ( num_theory : int ) ( theory : Expr.expr list ) =
+ (Z3native.write_interpolation_problem (context_gno ctx) num (expr_lton cnsts) (Array.of_list parents) filename num_theory (expr_lton theory)) ;
+ ()
+end
let set_global_param ( id : string ) ( value : string ) =
(Z3native.global_param_set id value)
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 1342bb4bc..b2f0939d0 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -149,11 +149,11 @@ sig
val resize : ast_vector -> int -> unit
(** Add an ast to the back of the vector. The size
- is increased by 1. *)
+ is increased by 1. *)
val push : ast_vector -> ast -> unit
(** Translates all ASTs in the vector to another context.
- @return A new ASTVector *)
+ @return A new ASTVector *)
val translate : ast_vector -> context -> ast_vector
(** Retrieves a string representation of the vector. *)
@@ -196,7 +196,7 @@ sig
end
(** The AST's hash code.
- @return A hash code *)
+ @return A hash code *)
val hash : ast -> int
(** A unique identifier for the AST (unique among all ASTs). *)
@@ -227,34 +227,34 @@ sig
val to_sexpr : ast -> string
(** Comparison operator.
- @return True if the two ast's are from the same context
- and represent the same sort; false otherwise. *)
+ @return True if the two ast's are from the same context
+ and represent the same sort; false otherwise. *)
val equal : ast -> ast -> bool
(** Object Comparison.
- @return Negative if the first ast should be sorted before the second, positive if after else zero. *)
+ @return Negative if the first ast should be sorted before the second, positive if after else zero. *)
val compare : ast -> ast -> int
(** Translates (copies) the AST to another context.
- @return A copy of the AST which is associated with the other context. *)
+ @return A copy of the AST which is associated with the other context. *)
val translate : ast -> context -> 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.,
- [Z3native.inc_ref]).
- {!wrap_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.,
+ [Z3native.inc_ref]).
+ {!wrap_ast} *)
val unwrap_ast : ast -> Z3native.ptr
(** Wraps an AST.
- This function is used for transitions between native and
- managed objects. Note that the native ast that is passed must be a
- native object obtained from Z3 (e.g., through {!unwrap_ast})
- and that it must have a correct reference count (see e.g.,
+ This function is used for transitions between native and
+ managed objects. Note that the native ast that is passed must be a
+ native object obtained from Z3 (e.g., through {!unwrap_ast})
+ and that it must have a correct reference count (see e.g.,
[Z3native.inc_ref]). *)
val wrap_ast : context -> Z3native.z3_ast -> ast
end
@@ -267,8 +267,8 @@ sig
val ast_of_sort : sort -> AST.ast
(** Comparison operator.
- @return True if the two sorts are from the same context
- and represent the same sort; false otherwise. *)
+ @return True if the two sorts are from the same context
+ and represent the same sort; false otherwise. *)
val equal : sort -> sort -> bool
(** Returns a unique identifier for the sort. *)
@@ -441,33 +441,26 @@ sig
val to_string : params -> string
(** Update a mutable configuration parameter.
-
- The list of all configuration parameters can be obtained using the Z3 executable:
- [z3.exe -p]
- Only a few configuration parameters are mutable once the context is created.
- An exception is thrown when trying to modify an immutable parameter.
- {!get_param_value} *)
+
+ The list of all configuration parameters can be obtained using the Z3 executable:
+ [z3.exe -p]
+ Only a few configuration parameters are mutable once the context is created.
+ An exception is thrown when trying to modify an immutable parameter. *)
val update_param_value : context -> string -> string -> unit
-
- (** Get a configuration parameter.
-
- Returns None if the parameter value does not exist.
- {!update_param_value} *)
- val get_param_value : context -> string -> string option
-
+
(** Selects the format used for pretty-printing expressions.
-
- The default mode for pretty printing expressions is to produce
- SMT-LIB style output where common subexpressions are printed
- at each occurrence. The mode is called PRINT_SMTLIB_FULL.
- To print shared common subexpressions only once,
- use the PRINT_LOW_LEVEL mode.
- To print in way that conforms to SMT-LIB standards and uses let
- expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT.
- {!AST.to_string}
- {!Quantifier.Pattern.to_string}
- {!FuncDecl.to_string}
- {!Sort.to_string} *)
+
+ The default mode for pretty printing expressions is to produce
+ SMT-LIB style output where common subexpressions are printed
+ at each occurrence. The mode is called PRINT_SMTLIB_FULL.
+ To print shared common subexpressions only once,
+ use the PRINT_LOW_LEVEL mode.
+ To print in way that conforms to SMT-LIB standards and uses let
+ expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT.
+ {!AST.to_string}
+ {!Quantifier.Pattern.to_string}
+ {!FuncDecl.to_string}
+ {!Sort.to_string} *)
val set_print_mode : context -> Z3enums.ast_print_mode -> unit
end
@@ -480,7 +473,7 @@ sig
val expr_of_ast : AST.ast -> Expr.expr
(** Returns a simplified version of the expression.
- {!get_simplify_help} *)
+ {!get_simplify_help} *)
val simplify : Expr.expr -> Params.params option -> expr
(** A string describing all available parameters to [Expr.Simplify]. *)
@@ -503,23 +496,23 @@ sig
val update : Expr.expr -> Expr.expr list -> expr
(** Substitute every occurrence of [from[i]] in the expression with [to[i]], for [i] smaller than [num_exprs].
-
- The result is the new expression. The arrays [from] and [to] must have size [num_exprs].
- For every [i] smaller than [num_exprs], we must have that
- sort of [from[i]] must be equal to sort of [to[i]]. *)
+
+ The result is the new expression. The arrays [from] and [to] must have size [num_exprs].
+ For every [i] smaller than [num_exprs], we must have that
+ sort of [from[i]] must be equal to sort of [to[i]]. *)
val substitute : Expr.expr -> Expr.expr list -> Expr.expr list -> expr
(** Substitute every occurrence of [from] in the expression with [to].
- {!substitute} *)
+ {!substitute} *)
val substitute_one : Expr.expr -> Expr.expr -> Expr.expr -> expr
(** Substitute the free variables in the expression with the expressions in the expr array
- For every [i] smaller than [num_exprs], the variable with de-Bruijn index [i] is replaced with term [to[i]]. *)
+ For every [i] smaller than [num_exprs], the variable with de-Bruijn index [i] is replaced with term [to[i]]. *)
val substitute_vars : Expr.expr -> Expr.expr list -> expr
(** Translates (copies) the term to another context.
- @return A copy of the term which is associated with the other context *)
+ @return A copy of the term which is associated with the other context *)
val translate : Expr.expr -> context -> expr
(** Returns a string representation of the expression. *)
@@ -529,7 +522,7 @@ sig
val is_numeral : Expr.expr -> bool
(** Indicates whether the term is well-sorted.
- @return True if the term is well-sorted, false otherwise. *)
+ @return True if the term is well-sorted, false otherwise. *)
val is_well_sorted : Expr.expr -> bool
(** The Sort of the term. *)
@@ -537,26 +530,26 @@ sig
(** Indicates whether the term represents a constant. *)
val is_const : Expr.expr -> bool
-
+
(** Creates a new constant. *)
val mk_const : context -> Symbol.symbol -> Sort.sort -> expr
-
+
(** Creates a new constant. *)
val mk_const_s : context -> string -> Sort.sort -> expr
-
+
(** Creates a constant from the func_decl. *)
val mk_const_f : context -> FuncDecl.func_decl -> expr
-
+
(** Creates a fresh constant with a name prefixed with a string. *)
val mk_fresh_const : context -> string -> Sort.sort -> expr
-
+
(** Create a new function application. *)
val mk_app : context -> FuncDecl.func_decl -> Expr.expr list -> expr
-
+
(** Create a numeral of a given sort.
- @return A Term with the given value and sort *)
+ @return A Term with the given value and sort *)
val mk_numeral_string : context -> string -> Sort.sort -> expr
-
+
(** Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer.
It is slightly faster than [MakeNumeral] since it is not necessary to parse a string.
@return A Term with the given value and sort *)
@@ -692,21 +685,21 @@ sig
(** The de-Burijn index of a bound variable.
-
- Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
- the meaning of de-Bruijn indices by indicating the compilation process from
- non-de-Bruijn formulas to de-Bruijn format.
-
- abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
- abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
- abs1(x, x, n) = b_n
- abs1(y, x, n) = y
- abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
- abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
-
- The last line is significant: the index of a bound variable is different depending
- on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its
- index. *)
+
+ Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
+ the meaning of de-Bruijn indices by indicating the compilation process from
+ non-de-Bruijn formulas to de-Bruijn format.
+
+ abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
+ abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
+ abs1(x, x, n) = b_n
+ abs1(y, x, n) = y
+ abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
+ abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
+
+ The last line is significant: the index of a bound variable is different depending
+ on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its
+ index. *)
val get_index : Expr.expr -> int
(** Indicates whether the quantifier is universal. *)
@@ -723,19 +716,19 @@ sig
(** The patterns. *)
val get_patterns : quantifier -> Pattern.pattern list
-
- (** The number of no-patterns. *)
+
+ (** The number of no-patterns. *)
val get_num_no_patterns : quantifier -> int
(** The no-patterns. *)
val get_no_patterns : quantifier -> Pattern.pattern list
- (** The number of bound variables. *)
- val get_num_bound : quantifier -> int
-
- (** The symbols for the bound variables. *)
+ (** The number of bound variables. *)
+ val get_num_bound : quantifier -> int
+
+ (** The symbols for the bound variables. *)
val get_bound_variable_names : quantifier -> Symbol.symbol list
-
+
(** The sorts of the bound variables. *)
val get_bound_variable_sorts : quantifier -> Sort.sort list
@@ -767,7 +760,7 @@ sig
val mk_quantifier : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier
(** A string representation of the quantifier. *)
- val to_string : quantifier -> string
+ val to_string : quantifier -> string
end
(** Functions to manipulate Array expressions *)
@@ -777,28 +770,28 @@ sig
val mk_sort : context -> Sort.sort -> Sort.sort -> Sort.sort
(** Indicates whether the term is an array store.
- It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
- Array store takes at least 3 arguments. *)
+ It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j).
+ Array store takes at least 3 arguments. *)
val is_store : Expr.expr -> bool
(** Indicates whether the term is an array select. *)
val is_select : Expr.expr -> bool
(** Indicates whether the term is a constant array.
- For example, select(const(v),i) = v holds for every v and i. The function is unary. *)
+ For example, select(const(v),i) = v holds for every v and i. The function is unary. *)
val is_constant_array : Expr.expr -> bool
(** Indicates whether the term is a default array.
- For example default(const(v)) = v. The function is unary. *)
+ For example default(const(v)) = v. The function is unary. *)
val is_default_array : Expr.expr -> bool
(** Indicates whether the term is an array map.
- It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. *)
+ It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. *)
val is_array_map : Expr.expr -> bool
(** Indicates whether the term is an as-array term.
- An as-array term is n array value that behaves as the function graph of the
- function passed as parameter. *)
+ An as-array term is n array value that behaves as the function graph of the
+ function passed as parameter. *)
val is_as_array : Expr.expr -> bool
(** Indicates whether the term is of an array sort. *)
@@ -806,66 +799,66 @@ sig
(** The domain of the array sort. *)
val get_domain : Sort.sort -> Sort.sort
-
+
(** The range of the array sort. *)
val get_range : Sort.sort -> Sort.sort
-
+
(** Create an array constant. *)
val mk_const : context -> Symbol.symbol -> Sort.sort -> Sort.sort -> Expr.expr
-
+
(** Create an array constant. *)
val mk_const_s : context -> string -> Sort.sort -> Sort.sort -> Expr.expr
-
+
(** Array read.
-
- The argument [a] is the array and [i] is the index
- of the array that gets read.
-
- The node [a] must have an array sort [[domain -> range]],
- and [i] must have the sort [domain].
- The sort of the result is [range].
- {!Z3Array.mk_sort}
- {!mk_store} *)
+
+ The argument [a] is the array and [i] is the index
+ of the array that gets read.
+
+ The node [a] must have an array sort [[domain -> range]],
+ and [i] must have the sort [domain].
+ The sort of the result is [range].
+ {!Z3Array.mk_sort}
+ {!mk_store} *)
val mk_select : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Array update.
-
- The node [a] must have an array sort [[domain -> range]],
- [i] must have sort [domain],
- [v] must have sort range. The sort of the result is [[domain -> range]].
- The semantics of this function is given by the theory of arrays described in the SMT-LIB
- standard. See http://smtlib.org for more details.
- The result of this function is an array that is equal to [a]
- (with respect to [select])
- on all indices except for [i], where it maps to [v]
- (and the [select] of [a] with
- respect to [i] may be a different value).
- {!Z3Array.mk_sort}
- {!mk_select} *)
+
+ The node [a] must have an array sort [[domain -> range]],
+ [i] must have sort [domain],
+ [v] must have sort range. The sort of the result is [[domain -> range]].
+ The semantics of this function is given by the theory of arrays described in the SMT-LIB
+ standard. See http://smtlib.org for more details.
+ The result of this function is an array that is equal to [a]
+ (with respect to [select])
+ on all indices except for [i], where it maps to [v]
+ (and the [select] of [a] with
+ respect to [i] may be a different value).
+ {!Z3Array.mk_sort}
+ {!mk_select} *)
val mk_store : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
(** Create a constant array.
-
- The resulting term is an array, such that a [select]on an arbitrary index
- produces the value [v].
- {!Z3Array.mk_sort}
- {!mk_select} *)
+
+ The resulting term is an array, such that a [select]on an arbitrary index
+ produces the value [v].
+ {!Z3Array.mk_sort}
+ {!mk_select} *)
val mk_const_array : context -> Sort.sort -> Expr.expr -> Expr.expr
(** Maps f on the argument arrays.
-
- Eeach element of [args] must be of an array sort [[domain_i -> range_i]].
- The function declaration [f] must have type [ range_1 .. range_n -> range].
- [v] must have sort range. The sort of the result is [[domain_i -> range]].
- {!Z3Array.mk_sort}
- {!mk_select}
- {!mk_store} *)
+
+ Eeach element of [args] must be of an array sort [[domain_i -> range_i]].
+ The function declaration [f] must have type [ range_1 .. range_n -> range].
+ [v] must have sort range. The sort of the result is [[domain_i -> range]].
+ {!Z3Array.mk_sort}
+ {!mk_select}
+ {!mk_store} *)
val mk_map : context -> FuncDecl.func_decl -> Expr.expr list -> Expr.expr
(** Access the array default value.
-
- Produces the default range value, for arrays that can be represented as
- finite maps with a default range value. *)
+
+ Produces the default range value, for arrays that can be represented as
+ finite maps with a default range value. *)
val mk_term_array : context -> Expr.expr -> Expr.expr
end
@@ -948,10 +941,10 @@ sig
val is_relation : Expr.expr -> bool
(** Indicates whether the term is an relation store
-
- Insert a record into a relation.
- The function takes [n+1] arguments, where the first argument is the relation and the remaining [n] elements
- correspond to the [n] columns of the relation. *)
+
+ Insert a record into a relation.
+ The function takes [n+1] arguments, where the first argument is the relation and the remaining [n] elements
+ correspond to the [n] columns of the relation. *)
val is_store : Expr.expr -> bool
(** Indicates whether the term is an empty relation *)
@@ -964,62 +957,62 @@ sig
val is_join : Expr.expr -> bool
(** Indicates whether the term is the union or convex hull of two relations.
- The function takes two arguments. *)
+ The function takes two arguments. *)
val is_union : Expr.expr -> bool
(** Indicates whether the term is the widening of two relations
- The function takes two arguments. *)
+ The function takes two arguments. *)
val is_widen : Expr.expr -> bool
(** Indicates whether the term is a projection of columns (provided as numbers in the parameters).
- The function takes one argument. *)
+ The function takes one argument. *)
val is_project : Expr.expr -> bool
(** Indicates whether the term is a relation filter
-
- Filter (restrict) a relation with respect to a predicate.
- The first argument is a relation.
- The second argument is a predicate with free de-Brujin indices
- corresponding to the columns of the relation.
- So the first column in the relation has index 0. *)
+
+ Filter (restrict) a relation with respect to a predicate.
+ The first argument is a relation.
+ The second argument is a predicate with free de-Brujin indices
+ corresponding to the columns of the relation.
+ So the first column in the relation has index 0. *)
val is_filter : Expr.expr -> bool
(** Indicates whether the term is an intersection of a relation with the negation of another.
-
- Intersect the first relation with respect to negation
- of the second relation (the function takes two arguments).
- Logically, the specification can be described by a function
-
- target = filter_by_negation(pos, neg, columns)
-
- where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that
- target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with
- ( x : expr ) on the columns c1, d1, .., cN, dN. *)
+
+ Intersect the first relation with respect to negation
+ of the second relation (the function takes two arguments).
+ Logically, the specification can be described by a function
+
+ target = filter_by_negation(pos, neg, columns)
+
+ where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that
+ target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with
+ ( x : expr ) on the columns c1, d1, .., cN, dN. *)
val is_negation_filter : Expr.expr -> bool
(** Indicates whether the term is the renaming of a column in a relation
-
- The function takes one argument.
- The parameters contain the renaming as a cycle. *)
+
+ The function takes one argument.
+ The parameters contain the renaming as a cycle. *)
val is_rename : Expr.expr -> bool
(** Indicates whether the term is the complement of a relation *)
val is_complement : Expr.expr -> bool
(** Indicates whether the term is a relational select
-
- Check if a record is an element of the relation.
- The function takes [n+1] arguments, where the first argument is a relation,
- and the remaining [n] arguments correspond to a record. *)
+
+ Check if a record is an element of the relation.
+ The function takes [n+1] arguments, where the first argument is a relation,
+ and the remaining [n] arguments correspond to a record. *)
val is_select : Expr.expr -> bool
(** Indicates whether the term is a relational clone (copy)
-
- Create a fresh copy (clone) of a relation.
- The function is logically the identity, but
- in the context of a register machine allows
- for terms of kind {!is_union}
- to perform destructive updates to the first argument. *)
+
+ Create a fresh copy (clone) of a relation.
+ The function is logically the identity, but
+ in the context of a register machine allows
+ for terms of kind {!is_union}
+ to perform destructive updates to the first argument. *)
val is_clone : Expr.expr -> bool
(** The arity of the relation sort. *)
@@ -1039,25 +1032,25 @@ sig
(** The number of fields of the constructor. *)
val get_num_fields : constructor -> int
-
+
(** The function declaration of the constructor. *)
val get_constructor_decl : constructor -> FuncDecl.func_decl
(** The function declaration of the tester. *)
val get_tester_decl : constructor -> FuncDecl.func_decl
-
+
(** The function declarations of the accessors *)
val get_accessor_decls : constructor -> FuncDecl.func_decl list
end
(** Create a datatype constructor.
- if the corresponding sort reference is 0, then the value in sort_refs should be an index
- referring to one of the recursive datatypes that is declared. *)
+ 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. *)
val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
(** Create a datatype constructor.
- if the corresponding sort reference is 0, then the value in sort_refs should be an index
- referring to one of the recursive datatypes that is declared. *)
+ 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. *)
val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
(** Create a new datatype sort. *)
@@ -1078,7 +1071,7 @@ sig
(** The constructors. *)
val get_constructors : Sort.sort -> FuncDecl.func_decl list
-
+
(** The recognizers. *)
val get_recognizers : Sort.sort -> FuncDecl.func_decl list
@@ -1174,38 +1167,38 @@ sig
val mk_const_s : context -> string -> Expr.expr
(** Create an expression representing [t1 mod t2].
- The arguments must have int type. *)
+ The arguments must have int type. *)
val mk_mod : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing [t1 rem t2].
- The arguments must have int type. *)
+ The arguments must have int type. *)
val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an integer numeral. *)
val mk_numeral_s : context -> string -> Expr.expr
(** Create an integer numeral.
- @return A Term with the given value and sort Integer *)
+ @return A Term with the given value and sort Integer *)
val mk_numeral_i : context -> int -> Expr.expr
(** Coerce an integer to a real.
-
-
- There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
-
- You can take the floor of a real by creating an auxiliary integer Term [k] and
- and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1].
- The argument must be of integer sort. *)
+
+
+ There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
+
+ You can take the floor of a real by creating an auxiliary integer Term [k] and
+ and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1].
+ The argument must be of integer sort. *)
val mk_int2real : context -> Expr.expr -> Expr.expr
(** Create an n-bit bit-vector from an integer argument.
-
-
- NB. This function is essentially treated as uninterpreted.
- So you cannot expect Z3 to precisely reflect the semantics of this function
- when solving constraints with this function.
-
- The argument must be of integer sort. *)
+
+
+ NB. This function is essentially treated as uninterpreted.
+ So you cannot expect Z3 to precisely reflect the semantics of this function
+ when solving constraints with this function.
+
+ The argument must be of integer sort. *)
val mk_int2bv : context -> int -> Expr.expr -> Expr.expr
end
@@ -1238,16 +1231,16 @@ sig
val mk_const_s : context -> string -> Expr.expr
(** Create a real numeral from a fraction.
- @return A Term with rational value and sort Real
- {!mk_numeral_s} *)
+ @return A Term with rational value and sort Real
+ {!mk_numeral_s} *)
val mk_numeral_nd : context -> int -> int -> Expr.expr
(** Create a real numeral.
- @return A Term with the given value and sort Real *)
+ @return A Term with the given value and sort Real *)
val mk_numeral_s : context -> string -> Expr.expr
(** Create a real numeral.
- @return A Term with the given value and sort Real *)
+ @return A Term with the given value and sort Real *)
val mk_numeral_i : context -> int -> Expr.expr
(** Creates an expression that checks whether a real number is an integer. *)
@@ -1255,8 +1248,8 @@ sig
(** Coerce a real to an integer.
- The semantics of this function follows the SMT-LIB standard for the function to_int.
- The argument must be of real sort. *)
+ The semantics of this function follows the SMT-LIB standard for the function to_int.
+ The argument must be of real sort. *)
val mk_real2int : context -> Expr.expr -> Expr.expr
(** Algebraic Numbers *)
@@ -1522,34 +1515,34 @@ sig
val is_bv_rotateright : Expr.expr -> bool
(** Indicates whether the term is a bit-vector rotate left (extended)
- Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. *)
+ Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. *)
val is_bv_rotateleftextended : Expr.expr -> bool
(** Indicates whether the term is a bit-vector rotate right (extended)
- Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. *)
+ Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. *)
val is_bv_rotaterightextended : Expr.expr -> bool
-
+
(** Indicates whether the term is a coercion from integer to bit-vector
- This function is not supported by the decision procedures. Only the most
- rudimentary simplification rules are applied to this function. *)
+ This function is not supported by the decision procedures. Only the most
+ rudimentary simplification rules are applied to this function. *)
(** Indicates whether the term is a coercion from bit-vector to integer
- This function is not supported by the decision procedures. Only the most
- rudimentary simplification rules are applied to this function. *)
+ This function is not supported by the decision procedures. Only the most
+ rudimentary simplification rules are applied to this function. *)
val is_int_to_bv : Expr.expr -> bool
(** Indicates whether the term is a coercion from integer to bit-vector
- This function is not supported by the decision procedures. Only the most
- rudimentary simplification rules are applied to this function. *)
+ This function is not supported by the decision procedures. Only the most
+ rudimentary simplification rules are applied to this function. *)
val is_bv_to_int : Expr.expr -> bool
(** Indicates whether the term is a bit-vector carry
- Compute the carry bit in a full-adder. The meaning is given by the
- equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) *)
+ Compute the carry bit in a full-adder. The meaning is given by the
+ equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) *)
val is_bv_carry : Expr.expr -> bool
-
+
(** Indicates whether the term is a bit-vector ternary XOR
- The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) *)
+ The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) *)
val is_bv_xor3 : Expr.expr -> bool
(** The size of a bit-vector sort. *)
@@ -1557,7 +1550,7 @@ sig
(** Retrieve the int value. *)
val get_int : Expr.expr -> int
-
+
(** Returns a string representation of the numeral. *)
val to_string : Expr.expr -> string
@@ -1568,146 +1561,145 @@ sig
val mk_const_s : context -> string -> int -> Expr.expr
(** Bitwise negation.
- The argument must have a bit-vector sort. *)
+ The argument must have a bit-vector sort. *)
val mk_not : context -> Expr.expr -> Expr.expr
(** Take conjunction of bits in a vector,vector of length 1.
- The argument must have a bit-vector sort. *)
+ The argument must have a bit-vector sort. *)
val mk_redand : context -> Expr.expr -> Expr.expr
(** Take disjunction of bits in a vector,vector of length 1.
- The argument must have a bit-vector sort. *)
+ The argument must have a bit-vector sort. *)
val mk_redor : context -> Expr.expr -> Expr.expr
(** Bitwise conjunction.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_and : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Bitwise disjunction.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_or : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Bitwise XOR.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Bitwise NAND.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_nand : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Bitwise NOR.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_nor : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Bitwise XNOR.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_xnor : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Standard two's complement unary minus.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_neg : context -> Expr.expr -> Expr.expr
(** Two's complement addition.
- The arguments must have the same bit-vector sort. *)
+ The arguments must have the same bit-vector sort. *)
val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Two's complement subtraction.
- The arguments must have the same bit-vector sort. *)
+ The arguments must have the same bit-vector sort. *)
val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Two's complement multiplication.
- The arguments must have the same bit-vector sort. *)
+ The arguments must have the same bit-vector sort. *)
val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Unsigned division.
-
-
- It is defined as the floor of [t1/t2] if \c t2 is
- different from zero. If [t2] is zero, then the result
- is undefined.
- The arguments must have the same bit-vector sort. *)
+
+ It is defined as the floor of [t1/t2] if \c t2 is
+ different from zero. If [t2] is zero, then the result
+ is undefined.
+ The arguments must have the same bit-vector sort. *)
val mk_udiv : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Signed division.
-
- It is defined in the following way:
+
+ It is defined in the following way:
- - The \c floor of [t1/t2] if \c t2 is different from zero, and [t1*t2 >= 0].
+ - The \c floor of [t1/t2] if \c t2 is different from zero, and [t1*t2 >= 0].
- - The \c ceiling of [t1/t2] if \c t2 is different from zero, and [t1*t2 < 0].
+ - The \c ceiling of [t1/t2] if \c t2 is different from zero, and [t1*t2 < 0].
- If [t2] is zero, then the result is undefined.
- The arguments must have the same bit-vector sort. *)
+ If [t2] is zero, then the result is undefined.
+ The arguments must have the same bit-vector sort. *)
val mk_sdiv : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Unsigned remainder.
-
- It is defined as [t1 - (t1 /u t2) * t2], where [/u] represents unsigned division.
- If [t2] is zero, then the result is undefined.
- The arguments must have the same bit-vector sort. *)
+
+ It is defined as [t1 - (t1 /u t2) * t2], where [/u] represents unsigned division.
+ If [t2] is zero, then the result is undefined.
+ The arguments must have the same bit-vector sort. *)
val mk_urem : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Signed remainder.
-
- It is defined as [t1 - (t1 /s t2) * t2], where [/s] represents signed division.
- The most significant bit (sign) of the result is equal to the most significant bit of \c t1.
+
+ It is defined as [t1 - (t1 /s t2) * t2], where [/s] represents signed division.
+ The most significant bit (sign) of the result is equal to the most significant bit of \c t1.
- If [t2] is zero, then the result is undefined.
- The arguments must have the same bit-vector sort. *)
+ If [t2] is zero, then the result is undefined.
+ The arguments must have the same bit-vector sort. *)
val mk_srem : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Two's complement signed remainder (sign follows divisor).
-
- If [t2] is zero, then the result is undefined.
- The arguments must have the same bit-vector sort. *)
+
+ If [t2] is zero, then the result is undefined.
+ The arguments must have the same bit-vector sort. *)
val mk_smod : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Unsigned less-than
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_ult : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Two's complement signed less-than
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_slt : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Unsigned less-than or equal to.
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_ule : context -> Expr.expr -> Expr.expr -> Expr.expr
-
+
(** Two's complement signed less-than or equal to.
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_sle : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Unsigned greater than or equal to.
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_uge : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Two's complement signed greater than or equal to.
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_sge : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Unsigned greater-than.
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_ugt : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Two's complement signed greater-than.
-
- The arguments must have the same bit-vector sort. *)
+
+ The arguments must have the same bit-vector sort. *)
val mk_sgt : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Bit-vector concatenation.
-
- The arguments must have a bit-vector sort.
- @return
- The result is a bit-vector of size [n1+n2], where [n1] ([n2])
- is the size of [t1] ([t2]). *)
+
+ The arguments must have a bit-vector sort.
+ @return
+ The result is a bit-vector of size [n1+n2], where [n1] ([n2])
+ is the size of [t1] ([t2]). *)
val mk_concat : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Bit-vector extraction.
@@ -1719,17 +1711,17 @@ sig
(** Bit-vector sign extension.
- Sign-extends the given bit-vector to the (signed) equivalent bitvector of
- size [m+i], where \c m is the size of the given bit-vector. *)
+ Sign-extends the given bit-vector to the (signed) equivalent bitvector of
+ size [m+i], where \c m is the size of the given bit-vector. *)
val mk_sign_ext : context -> int -> Expr.expr -> Expr.expr
(** Bit-vector zero extension.
- Extend the given bit-vector with zeros to the (unsigned) equivalent
- bitvector of size [m+i], where \c m is the size of the
- given bit-vector. *)
+ Extend the given bit-vector with zeros to the (unsigned) equivalent
+ bitvector of size [m+i], where \c m is the size of the
+ given bit-vector. *)
val mk_zero_ext : context -> int -> Expr.expr -> Expr.expr
-
+
(** Bit-vector repetition. *)
val mk_repeat : context -> int -> Expr.expr -> Expr.expr
@@ -1743,27 +1735,27 @@ sig
val mk_shl : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Logical shift right
-
- It is equivalent to unsigned division by [2^x] where \c x is the value of the third argument.
+
+ It is equivalent to unsigned division by [2^x] where \c x is the value of the third argument.
- NB. The semantics of shift operations varies between environments. This
- definition does not necessarily capture directly the semantics of the
- programming language or assembly architecture you are modeling.
+ NB. The semantics of shift operations varies between environments. This
+ definition does not necessarily capture directly the semantics of the
+ programming language or assembly architecture you are modeling.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_lshr : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Arithmetic shift right
-
- It is like logical shift right except that the most significant
- bits of the result always copy the most significant bit of the
- second argument.
+
+ It is like logical shift right except that the most significant
+ bits of the result always copy the most significant bit of the
+ second argument.
- NB. The semantics of shift operations varies between environments. This
- definition does not necessarily capture directly the semantics of the
- programming language or assembly architecture you are modeling.
+ NB. The semantics of shift operations varies between environments. This
+ definition does not necessarily capture directly the semantics of the
+ programming language or assembly architecture you are modeling.
- The arguments must have a bit-vector sort. *)
+ The arguments must have a bit-vector sort. *)
val mk_ashr : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Rotate Left.
@@ -1783,7 +1775,7 @@ sig
val mk_ext_rotate_right : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an integer from the bit-vector argument
-
+
If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned.
So the result is non-negative and in the range [[0..2^N-1]], where
N are the number of bits in the argument.
@@ -1795,45 +1787,45 @@ sig
val mk_bv2int : context -> Expr.expr -> bool -> Expr.expr
(** Create a predicate that checks that the bit-wise addition does not overflow.
-
- The arguments must be of bit-vector sort. *)
+
+ The arguments must be of bit-vector sort. *)
val mk_add_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr
(** Create a predicate that checks that the bit-wise addition does not underflow.
-
- The arguments must be of bit-vector sort. *)
+
+ The arguments must be of bit-vector sort. *)
val mk_add_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create a predicate that checks that the bit-wise subtraction does not overflow.
-
- The arguments must be of bit-vector sort. *)
+
+ The arguments must be of bit-vector sort. *)
val mk_sub_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create a predicate that checks that the bit-wise subtraction does not underflow.
-
- The arguments must be of bit-vector sort. *)
+
+ The arguments must be of bit-vector sort. *)
val mk_sub_no_underflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr
(** Create a predicate that checks that the bit-wise signed division does not overflow.
-
- The arguments must be of bit-vector sort. *)
+
+ The arguments must be of bit-vector sort. *)
val mk_sdiv_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create a predicate that checks that the bit-wise negation does not overflow.
-
- The arguments must be of bit-vector sort. *)
+
+ The arguments must be of bit-vector sort. *)
val mk_neg_no_overflow : context -> Expr.expr -> Expr.expr
(** Create a predicate that checks that the bit-wise multiplication does not overflow.
-
- The arguments must be of bit-vector sort. *)
+
+ The arguments must be of bit-vector sort. *)
val mk_mul_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr
(** Create a predicate that checks that the bit-wise multiplication does not underflow.
-
- The arguments must be of bit-vector sort. *)
- val mk_mul_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr
+ The arguments must be of bit-vector sort. *)
+ val mk_mul_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr
+
(** Create a bit-vector numeral. *)
val mk_numeral : context -> string -> int -> Expr.expr
end
@@ -1851,389 +1843,389 @@ sig
val is_goal : Expr.expr -> bool
(** Indicates whether the term is a binary equivalence modulo namings.
- This binary predicate is used in proof terms.
- It captures equisatisfiability and equivalence modulo renamings. *)
+ This binary predicate is used in proof terms.
+ It captures equisatisfiability and equivalence modulo renamings. *)
val is_oeq : Expr.expr -> bool
(** Indicates whether the term is proof via modus ponens
-
- Given a proof for p and a proof for (implies p q), produces a proof for q.
- T1: p
- T2: (implies p q)
- [mp T1 T2]: q
- The second antecedents may also be a proof for (iff p q). *)
+
+ Given a proof for p and a proof for (implies p q), produces a proof for q.
+ T1: p
+ T2: (implies p q)
+ [mp T1 T2]: q
+ The second antecedents may also be a proof for (iff p q). *)
val is_modus_ponens : Expr.expr -> bool
(** Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
- This proof object has no antecedents.
- The only reflexive relations that are used are
- equivalence modulo namings, equality and equivalence.
- That is, R is either '~', '=' or 'iff'. *)
+ This proof object has no antecedents.
+ The only reflexive relations that are used are
+ equivalence modulo namings, equality and equivalence.
+ That is, R is either '~', '=' or 'iff'. *)
val is_reflexivity : Expr.expr -> bool
(** Indicates whether the term is proof by symmetricity of a relation
-
- Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).
- T1: (R t s)
- [symmetry T1]: (R s t)
- T1 is the antecedent of this proof object. *)
+
+ Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).
+ T1: (R t s)
+ [symmetry T1]: (R s t)
+ T1 is the antecedent of this proof object. *)
val is_symmetry : Expr.expr -> bool
(** Indicates whether the term is a proof by transitivity of a relation
-
- Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
- for (R t u).
- T1: (R t s)
- T2: (R s u)
- [trans T1 T2]: (R t u) *)
+
+ Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
+ for (R t u).
+ T1: (R t s)
+ T2: (R s u)
+ [trans T1 T2]: (R t u) *)
val is_transitivity : Expr.expr -> bool
(** Indicates whether the term is a proof by condensed transitivity of a relation
-
- Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
- It combines several symmetry and transitivity proofs.
- Example:
- T1: (R a b)
- T2: (R c b)
- T3: (R c d)
- [trans* T1 T2 T3]: (R a d)
- R must be a symmetric and transitive relation.
-
- Assuming that this proof object is a proof for (R s t), then
- a proof checker must check if it is possible to prove (R s t)
- using the antecedents, symmetry and transitivity. That is,
- if there is a path from s to t, if we view every
- antecedent (R a b) as an edge between a and b. *)
+
+ Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+ It combines several symmetry and transitivity proofs.
+ Example:
+ T1: (R a b)
+ T2: (R c b)
+ T3: (R c d)
+ [trans* T1 T2 T3]: (R a d)
+ R must be a symmetric and transitive relation.
+
+ Assuming that this proof object is a proof for (R s t), then
+ a proof checker must check if it is possible to prove (R s t)
+ using the antecedents, symmetry and transitivity. That is,
+ if there is a path from s to t, if we view every
+ antecedent (R a b) as an edge between a and b. *)
val is_Transitivity_star : Expr.expr -> bool
(** Indicates whether the term is a monotonicity proof object.
-
- T1: (R t_1 s_1)
- ...
- Tn: (R t_n s_n)
- [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
- Remark: if t_i == s_i, then the antecedent Ti is suppressed.
- That is, reflexivity proofs are supressed to save space. *)
+
+ T1: (R t_1 s_1)
+ ...
+ Tn: (R t_n s_n)
+ [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
+ Remark: if t_i == s_i, then the antecedent Ti is suppressed.
+ That is, reflexivity proofs are supressed to save space. *)
val is_monotonicity : Expr.expr -> bool
(** Indicates whether the term is a quant-intro proof
-
- Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
- T1: (~ p q)
- [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) *)
+
+ Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
+ T1: (~ p q)
+ [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) *)
val is_quant_intro : Expr.expr -> bool
(** Indicates whether the term is a distributivity proof object.
-
- Given that f (= or) distributes over g (= and), produces a proof for
- (= (f a (g c d))
- (g (f a c) (f a d)))
- If f and g are associative, this proof also justifies the following equality:
- (= (f (g a b) (g c d))
- (g (f a c) (f a d) (f b c) (f b d)))
- where each f and g can have arbitrary number of arguments.
-
- This proof object has no antecedents.
- Remark. This rule is used by the CNF conversion pass and
- instantiated by f = or, and g = and. *)
+
+ Given that f (= or) distributes over g (= and), produces a proof for
+ (= (f a (g c d))
+ (g (f a c) (f a d)))
+ If f and g are associative, this proof also justifies the following equality:
+ (= (f (g a b) (g c d))
+ (g (f a c) (f a d) (f b c) (f b d)))
+ where each f and g can have arbitrary number of arguments.
+
+ This proof object has no antecedents.
+ Remark. This rule is used by the CNF conversion pass and
+ instantiated by f = or, and g = and. *)
val is_distributivity : Expr.expr -> bool
(** Indicates whether the term is a proof by elimination of AND
-
- Given a proof for (and l_1 ... l_n), produces a proof for l_i
- T1: (and l_1 ... l_n)
- [and-elim T1]: l_i *)
+
+ Given a proof for (and l_1 ... l_n), produces a proof for l_i
+ T1: (and l_1 ... l_n)
+ [and-elim T1]: l_i *)
val is_and_elimination : Expr.expr -> bool
(** Indicates whether the term is a proof by eliminiation of not-or
-
- Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
- T1: (not (or l_1 ... l_n))
- [not-or-elim T1]: (not l_i) *)
+
+ Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
+ T1: (not (or l_1 ... l_n))
+ [not-or-elim T1]: (not l_i) *)
val is_or_elimination : Expr.expr -> bool
(** Indicates whether the term is a proof by rewriting
-
- A proof for a local rewriting step (= t s).
- The head function symbol of t is interpreted.
-
- This proof object has no antecedents.
- The conclusion of a rewrite rule is either an equality (= t s),
- an equivalence (iff t s), or equi-satisfiability (~ t s).
- Remark: if f is bool, then = is iff.
-
- Examples:
- (= (+ ( x : expr ) 0) x)
- (= (+ ( x : expr ) 1 2) (+ 3 x))
- (iff (or ( x : expr ) false) x) *)
+
+ A proof for a local rewriting step (= t s).
+ The head function symbol of t is interpreted.
+
+ This proof object has no antecedents.
+ The conclusion of a rewrite rule is either an equality (= t s),
+ an equivalence (iff t s), or equi-satisfiability (~ t s).
+ Remark: if f is bool, then = is iff.
+
+ Examples:
+ (= (+ ( x : expr ) 0) x)
+ (= (+ ( x : expr ) 1 2) (+ 3 x))
+ (iff (or ( x : expr ) false) x) *)
val is_rewrite : Expr.expr -> bool
(** Indicates whether the term is a proof by rewriting
-
- A proof for rewriting an expression t into an expression s.
- This proof object is used if the parameter PROOF_MODE is 1.
- This proof object can have n antecedents.
- The antecedents are proofs for equalities used as substitution rules.
- The object is also used in a few cases if the parameter PROOF_MODE is 2.
- The cases are:
- - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
- - When converting bit-vectors to Booleans (BIT2BOOL=true)
- - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) *)
+
+ A proof for rewriting an expression t into an expression s.
+ This proof object is used if the parameter PROOF_MODE is 1.
+ This proof object can have n antecedents.
+ The antecedents are proofs for equalities used as substitution rules.
+ The object is also used in a few cases if the parameter PROOF_MODE is 2.
+ The cases are:
+ - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
+ - When converting bit-vectors to Booleans (BIT2BOOL=true)
+ - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) *)
val is_rewrite_star : Expr.expr -> bool
(** Indicates whether the term is a proof for pulling quantifiers out.
-
- A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *)
+
+ A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *)
val is_pull_quant : Expr.expr -> bool
(** Indicates whether the term is a proof for pulling quantifiers out.
-
- A proof for (iff P Q) where Q is in prenex normal form.
- This proof object is only used if the parameter PROOF_MODE is 1.
- This proof object has no antecedents *)
+
+ A proof for (iff P Q) where Q is in prenex normal form.
+ This proof object is only used if the parameter PROOF_MODE is 1.
+ This proof object has no antecedents *)
val is_pull_quant_star : Expr.expr -> bool
(** Indicates whether the term is a proof for pushing quantifiers in.
-
- A proof for:
- (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
- (and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
- ...
- (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
- This proof object has no antecedents *)
+
+ A proof for:
+ (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
+ (and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
+ ...
+ (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
+ This proof object has no antecedents *)
val is_push_quant : Expr.expr -> bool
(** Indicates whether the term is a proof for elimination of unused variables.
-
- A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
- (forall (x_1 ... x_n) p[x_1 ... x_n]))
-
- It is used to justify the elimination of unused variables.
- This proof object has no antecedents. *)
+
+ A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
+ (forall (x_1 ... x_n) p[x_1 ... x_n]))
+
+ It is used to justify the elimination of unused variables.
+ This proof object has no antecedents. *)
val is_elim_unused_vars : Expr.expr -> bool
(** Indicates whether the term is a proof for destructive equality resolution
-
- A proof for destructive equality resolution:
- (iff (forall (x) (or (not (= ( x : expr ) t)) P[x])) P[t])
- if ( x : expr ) does not occur in t.
-
- This proof object has no antecedents.
-
- Several variables can be eliminated simultaneously. *)
+
+ A proof for destructive equality resolution:
+ (iff (forall (x) (or (not (= ( x : expr ) t)) P[x])) P[t])
+ if ( x : expr ) does not occur in t.
+
+ This proof object has no antecedents.
+
+ Several variables can be eliminated simultaneously. *)
val is_der : Expr.expr -> bool
-
+
(** Indicates whether the term is a proof for quantifier instantiation
-
- A proof of (or (not (forall (x) (P x))) (P a)) *)
+
+ A proof of (or (not (forall (x) (P x))) (P a)) *)
val is_quant_inst : Expr.expr -> bool
(** Indicates whether the term is a hypthesis marker.
- Mark a hypothesis in a natural deduction style proof. *)
+ Mark a hypothesis in a natural deduction style proof. *)
val is_hypothesis : Expr.expr -> bool
(** Indicates whether the term is a proof by lemma
-
- T1: false
- [lemma T1]: (or (not l_1) ... (not l_n))
-
- This proof object has one antecedent: a hypothetical proof for false.
- It converts the proof in a proof for (or (not l_1) ... (not l_n)),
- when T1 contains the hypotheses: l_1, ..., l_n. *)
+
+ T1: false
+ [lemma T1]: (or (not l_1) ... (not l_n))
+
+ This proof object has one antecedent: a hypothetical proof for false.
+ It converts the proof in a proof for (or (not l_1) ... (not l_n)),
+ when T1 contains the hypotheses: l_1, ..., l_n. *)
val is_lemma : Expr.expr -> bool
(** Indicates whether the term is a proof by unit resolution
-
- T1: (or l_1 ... l_n l_1' ... l_m')
- T2: (not l_1)
- ...
- T(n+1): (not l_n)
- [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') *)
+
+ T1: (or l_1 ... l_n l_1' ... l_m')
+ T2: (not l_1)
+ ...
+ T(n+1): (not l_n)
+ [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') *)
val is_unit_resolution : Expr.expr -> bool
(** Indicates whether the term is a proof by iff-true
-
- T1: p
- [iff-true T1]: (iff p true) *)
+
+ T1: p
+ [iff-true T1]: (iff p true) *)
val is_iff_true : Expr.expr -> bool
(** Indicates whether the term is a proof by iff-false
-
- T1: (not p)
- [iff-false T1]: (iff p false) *)
+
+ T1: (not p)
+ [iff-false T1]: (iff p false) *)
val is_iff_false : Expr.expr -> bool
(** Indicates whether the term is a proof by commutativity
-
- [comm]: (= (f a b) (f b a))
-
- f is a commutative operator.
-
- This proof object has no antecedents.
- Remark: if f is bool, then = is iff. *)
+
+ [comm]: (= (f a b) (f b a))
+
+ f is a commutative operator.
+
+ This proof object has no antecedents.
+ Remark: if f is bool, then = is iff. *)
val is_commutativity : Expr.expr -> bool
(** Indicates whether the term is a proof for Tseitin-like axioms
-
- Proof object used to justify Tseitin's like axioms:
-
- (or (not (and p q)) p)
- (or (not (and p q)) q)
- (or (not (and p q r)) p)
- (or (not (and p q r)) q)
- (or (not (and p q r)) r)
- ...
- (or (and p q) (not p) (not q))
- (or (not (or p q)) p q)
- (or (or p q) (not p))
- (or (or p q) (not q))
- (or (not (iff p q)) (not p) q)
- (or (not (iff p q)) p (not q))
- (or (iff p q) (not p) (not q))
- (or (iff p q) p q)
- (or (not (ite a b c)) (not a) b)
- (or (not (ite a b c)) a c)
- (or (ite a b c) (not a) (not b))
- (or (ite a b c) a (not c))
- (or (not (not a)) (not a))
- (or (not a) a)
-
- This proof object has no antecedents.
- Note: all axioms are propositional tautologies.
- Note also that 'and' and 'or' can take multiple arguments.
- You can recover the propositional tautologies by
- unfolding the Boolean connectives in the axioms a small
- bounded number of steps (=3). *)
+
+ Proof object used to justify Tseitin's like axioms:
+
+ (or (not (and p q)) p)
+ (or (not (and p q)) q)
+ (or (not (and p q r)) p)
+ (or (not (and p q r)) q)
+ (or (not (and p q r)) r)
+ ...
+ (or (and p q) (not p) (not q))
+ (or (not (or p q)) p q)
+ (or (or p q) (not p))
+ (or (or p q) (not q))
+ (or (not (iff p q)) (not p) q)
+ (or (not (iff p q)) p (not q))
+ (or (iff p q) (not p) (not q))
+ (or (iff p q) p q)
+ (or (not (ite a b c)) (not a) b)
+ (or (not (ite a b c)) a c)
+ (or (ite a b c) (not a) (not b))
+ (or (ite a b c) a (not c))
+ (or (not (not a)) (not a))
+ (or (not a) a)
+
+ This proof object has no antecedents.
+ Note: all axioms are propositional tautologies.
+ Note also that 'and' and 'or' can take multiple arguments.
+ You can recover the propositional tautologies by
+ unfolding the Boolean connectives in the axioms a small
+ bounded number of steps (=3). *)
val is_def_axiom : Expr.expr -> bool
(** Indicates whether the term is a proof for introduction of a name
-
- Introduces a name for a formula/term.
- Suppose e is an expression with free variables x, and def-intro
- introduces the name n(x). The possible cases are:
-
- When e is of Boolean type:
- [def-intro]: (and (or n (not e)) (or (not n) e))
-
- or:
- [def-intro]: (or (not n) e)
- when e only occurs positively.
-
- When e is of the form (ite cond th el):
- [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))
-
- Otherwise:
- [def-intro]: (= n e) *)
+
+ Introduces a name for a formula/term.
+ Suppose e is an expression with free variables x, and def-intro
+ introduces the name n(x). The possible cases are:
+
+ When e is of Boolean type:
+ [def-intro]: (and (or n (not e)) (or (not n) e))
+
+ or:
+ [def-intro]: (or (not n) e)
+ when e only occurs positively.
+
+ When e is of the form (ite cond th el):
+ [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))
+
+ Otherwise:
+ [def-intro]: (= n e) *)
val is_def_intro : Expr.expr -> bool
(** Indicates whether the term is a proof for application of a definition
-
- [apply-def T1]: F ~ n
- F is 'equivalent' to n, given that T1 is a proof that
- n is a name for F. *)
+
+ [apply-def T1]: F ~ n
+ F is 'equivalent' to n, given that T1 is a proof that
+ n is a name for F. *)
val is_apply_def : Expr.expr -> bool
(** Indicates whether the term is a proof iff-oeq
-
- T1: (iff p q)
- [iff~ T1]: (~ p q) *)
+
+ T1: (iff p q)
+ [iff~ T1]: (~ p q) *)
val is_iff_oeq : Expr.expr -> bool
(** Indicates whether the term is a proof for a positive NNF step
-
- Proof for a (positive) NNF step. Example:
-
- T1: (not s_1) ~ r_1
- T2: (not s_2) ~ r_2
- T3: s_1 ~ r_1'
- T4: s_2 ~ r_2'
- [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2)
- (and (or r_1 r_2') (or r_1' r_2)))
-
- The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:
- (a) When creating the NNF of a positive force quantifier.
- The quantifier is retained (unless the bound variables are eliminated).
- Example
- T1: q ~ q_new
- [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
-
- (b) When recursively creating NNF over Boolean formulas, where the top-level
- connective is changed during NNF conversion. The relevant Boolean connectives
- for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
- NNF_NEG furthermore handles the case where negation is pushed
- over Boolean connectives 'and' and 'or'. *)
+
+ Proof for a (positive) NNF step. Example:
+
+ T1: (not s_1) ~ r_1
+ T2: (not s_2) ~ r_2
+ T3: s_1 ~ r_1'
+ T4: s_2 ~ r_2'
+ [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2)
+ (and (or r_1 r_2') (or r_1' r_2)))
+
+ The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:
+ (a) When creating the NNF of a positive force quantifier.
+ The quantifier is retained (unless the bound variables are eliminated).
+ Example
+ T1: q ~ q_new
+ [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
+
+ (b) When recursively creating NNF over Boolean formulas, where the top-level
+ connective is changed during NNF conversion. The relevant Boolean connectives
+ for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
+ NNF_NEG furthermore handles the case where negation is pushed
+ over Boolean connectives 'and' and 'or'. *)
val is_nnf_pos : Expr.expr -> bool
(** Indicates whether the term is a proof for a negative NNF step
-
- Proof for a (negative) NNF step. Examples:
-
- T1: (not s_1) ~ r_1
- ...
- Tn: (not s_n) ~ r_n
- [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
- and
- T1: (not s_1) ~ r_1
- ...
- Tn: (not s_n) ~ r_n
- [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
- and
- T1: (not s_1) ~ r_1
- T2: (not s_2) ~ r_2
- T3: s_1 ~ r_1'
- T4: s_2 ~ r_2'
- [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
- (and (or r_1 r_2) (or r_1' r_2'))) *)
+
+ Proof for a (negative) NNF step. Examples:
+
+ T1: (not s_1) ~ r_1
+ ...
+ Tn: (not s_n) ~ r_n
+ [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
+ and
+ T1: (not s_1) ~ r_1
+ ...
+ Tn: (not s_n) ~ r_n
+ [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
+ and
+ T1: (not s_1) ~ r_1
+ T2: (not s_2) ~ r_2
+ T3: s_1 ~ r_1'
+ T4: s_2 ~ r_2'
+ [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
+ (and (or r_1 r_2) (or r_1' r_2'))) *)
val is_nnf_neg : Expr.expr -> bool
(** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
-
- A proof for (~ P Q) where Q is in negation normal form.
-
- This proof object is only used if the parameter PROOF_MODE is 1.
-
- This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
+
+ A proof for (~ P Q) where Q is in negation normal form.
+
+ This proof object is only used if the parameter PROOF_MODE is 1.
+
+ This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
val is_nnf_star : Expr.expr -> bool
(** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
-
- A proof for (~ P Q) where Q is in conjunctive normal form.
- This proof object is only used if the parameter PROOF_MODE is 1.
- This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
+
+ A proof for (~ P Q) where Q is in conjunctive normal form.
+ This proof object is only used if the parameter PROOF_MODE is 1.
+ This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
val is_cnf_star : Expr.expr -> bool
(** Indicates whether the term is a proof for a Skolemization step
-
- Proof for:
-
- [sk]: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y)))
- [sk]: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y))
-
- This proof object has no antecedents. *)
+
+ Proof for:
+
+ [sk]: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y)))
+ [sk]: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y))
+
+ This proof object has no antecedents. *)
val is_skolemize : Expr.expr -> bool
(** Indicates whether the term is a proof by modus ponens for equi-satisfiability.
-
- Modus ponens style rule for equi-satisfiability.
- T1: p
- T2: (~ p q)
- [mp~ T1 T2]: q *)
+
+ Modus ponens style rule for equi-satisfiability.
+ T1: p
+ T2: (~ p q)
+ [mp~ T1 T2]: q *)
val is_modus_ponens_oeq : Expr.expr -> bool
(** Indicates whether the term is a proof for theory lemma
-
- Generic proof for theory lemmas.
-
- The theory lemma function comes with one or more parameters.
- The first parameter indicates the name of the theory.
- For the theory of arithmetic, additional parameters provide hints for
- checking the theory lemma.
- The hints for arithmetic are:
- - farkas - followed by rational coefficients. Multiply the coefficients to the
- inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
- - triangle-eq - Indicates a lemma related to the equivalence:
- (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
- - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. *)
+
+ Generic proof for theory lemmas.
+
+ The theory lemma function comes with one or more parameters.
+ The first parameter indicates the name of the theory.
+ For the theory of arithmetic, additional parameters provide hints for
+ checking the theory lemma.
+ The hints for arithmetic are:
+ - farkas - followed by rational coefficients. Multiply the coefficients to the
+ inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
+ - triangle-eq - Indicates a lemma related to the equivalence:
+ (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
+ - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. *)
val is_theory_lemma : Expr.expr -> bool
end
@@ -2265,12 +2257,12 @@ sig
(** Indicates whether the goal is garbage (i.e., the product of over- and under-approximations). *)
val is_garbage : goal -> bool
- (** Adds the constraints to the given goal. *)
+ (** Adds the constraints to the given goal. *)
val add : goal -> Expr.expr list -> unit
-
+
(** Indicates whether the goal contains `false'. *)
val is_inconsistent : goal -> bool
-
+
(** The depth of the goal.
This tracks how many transformations were applied to it. *)
val get_depth : goal -> int
@@ -2300,7 +2292,7 @@ sig
val simplify : goal -> Params.params option -> goal
(** Creates a new Goal.
-
+
Note that the Context must have been created with proof generation support if
the fourth argument is set to true here. *)
val mk_goal : context -> bool -> bool -> bool -> goal
@@ -2323,7 +2315,7 @@ sig
module FuncInterp :
sig
type func_interp
-
+
(** Function interpretations entries
An Entry object represents an element in the finite map used to a function interpretation. *)
@@ -2418,7 +2410,7 @@ sig
{!get_sorts}
@return A list of expressions, where each is an element of the universe of the sort *)
val sort_universe : model -> Sort.sort -> AST.ast list
-
+
(** Conversion of models to strings.
@return A string representation of the model. *)
val to_string : model -> string
@@ -2437,8 +2429,8 @@ sig
type probe
(** Execute the probe over the goal.
- @return A probe always produce a float value.
- "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. *)
+ @return A probe always produce a float value.
+ "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. *)
val apply : probe -> Goal.goal -> float
(** The number of supported Probes. *)
@@ -2546,21 +2538,21 @@ sig
val mk_tactic : context -> string -> tactic
(** Create a tactic that applies one tactic to a Goal and
- then another one to every subgoal produced by the first one. *)
+ then another one to every subgoal produced by the first one. *)
val and_then : context -> tactic -> tactic -> tactic list -> tactic
(** Create a tactic that first applies one tactic to a Goal and
- if it fails then returns the result of another tactic applied to the Goal. *)
+ if it fails then returns the result of another tactic applied to the Goal. *)
val or_else : context -> tactic -> tactic -> tactic
(** Create a tactic that applies one tactic to a goal for some time (in milliseconds).
-
- If the tactic does not terminate within the timeout, then it fails. *)
+
+ If the tactic does not terminate within the timeout, then it fails. *)
val try_for : context -> tactic -> int -> tactic
(** Create a tactic that applies one tactic to a given goal if the probe
evaluates to true.
-
+
If the probe evaluates to false, then the new tactic behaves like the [skip] tactic. *)
val when_ : context -> Probe.probe -> tactic -> tactic
@@ -2569,7 +2561,7 @@ sig
val cond : context -> Probe.probe -> tactic -> tactic -> tactic
(** Create a tactic that keeps applying one tactic until the goal is not
- modified anymore or the maximum number of iterations is reached. *)
+ modified anymore or the maximum number of iterations is reached. *)
val repeat : context -> tactic -> int -> tactic
(** Create a tactic that just returns the given goal. *)
@@ -2582,14 +2574,14 @@ sig
val fail_if : context -> Probe.probe -> tactic
(** Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
- or trivially unsatisfiable (i.e., contains `false'). *)
+ or trivially unsatisfiable (i.e., contains `false'). *)
val fail_if_not_decided : context -> tactic
(** Create a tactic that applies a tactic using the given set of parameters. *)
val using_params : context -> tactic -> Params.params -> tactic
(** Create a tactic that applies a tactic using the given set of parameters.
- Alias for [UsingParams]*)
+ Alias for [UsingParams]*)
val with_ : context -> tactic -> Params.params -> tactic
(** Create a tactic that applies the given tactics in parallel. *)
@@ -2600,7 +2592,7 @@ sig
val par_and_then : context -> tactic -> tactic -> tactic
(** Interrupt the execution of a Z3 procedure.
- This procedure can be used to interrupt: solvers, simplifiers and tactics. *)
+ This procedure can be used to interrupt: solvers, simplifiers and tactics. *)
val interrupt : context -> unit
end
@@ -2618,8 +2610,8 @@ sig
type statistics
(** Statistical data is organized into pairs of \[Key, Entry\], where every
- Entry is either a floating point or integer value.
- *)
+ Entry is either a floating point or integer value.
+ *)
module Entry :
sig
type statistics_entry
@@ -2641,7 +2633,7 @@ sig
(** The string representation of the the entry's value. *)
val to_string_value : statistics_entry -> string
-
+
(** The string representation of the entry (key and value) *)
val to_string : statistics_entry -> string
end
@@ -2672,49 +2664,49 @@ sig
val get_param_descrs : solver -> Params.ParamDescrs.param_descrs
(** The current number of backtracking points (scopes).
- {!pop}
- {!push} *)
+ {!pop}
+ {!push} *)
val get_num_scopes : solver -> int
(** Creates a backtracking point.
- {!pop} *)
+ {!pop} *)
val push : solver -> unit
(** Backtracks a number of backtracking points.
- Note that an exception is thrown if the integer is not smaller than {!get_num_scopes}
- {!push} *)
+ Note that an exception is thrown if the integer is not smaller than {!get_num_scopes}
+ {!push} *)
val pop : solver -> int -> unit
(** Resets the Solver.
- This removes all assertions from the solver. *)
+ This removes all assertions from the solver. *)
val reset : solver -> unit
(** Assert a constraint (or multiple) into the solver. *)
val add : solver -> Expr.expr list -> unit
(** * Assert multiple constraints (cs) into the solver, and track them (in the
- * unsat) core
- * using the Boolean constants in ps.
- *
- * This API is an alternative to {!check} with assumptions for
- * extracting unsat cores.
- * Both APIs can be used in the same solver. The unsat core will contain a
- * combination
- * of the Boolean variables provided using {!assert_and_track}
- * and the Boolean literals
- * provided using {!check} with assumptions. *)
+ * unsat) core
+ * using the Boolean constants in ps.
+ *
+ * This API is an alternative to {!check} with assumptions for
+ * extracting unsat cores.
+ * Both APIs can be used in the same solver. The unsat core will contain a
+ * combination
+ * of the Boolean variables provided using {!assert_and_track}
+ * and the Boolean literals
+ * provided using {!check} with assumptions. *)
val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit
(** * Assert a constraint (c) into the solver, and track it (in the unsat) core
- * using the Boolean constant p.
- *
- * This API is an alternative to {!check} with assumptions for
- * extracting unsat cores.
- * Both APIs can be used in the same solver. The unsat core will contain a
- * combination
- * of the Boolean variables provided using {!assert_and_track}
- * and the Boolean literals
- * provided using {!check} with assumptions. *)
+ * using the Boolean constant p.
+ *
+ * This API is an alternative to {!check} with assumptions for
+ * extracting unsat cores.
+ * Both APIs can be used in the same solver. The unsat core will contain a
+ * combination
+ * of the Boolean variables provided using {!assert_and_track}
+ * and the Boolean literals
+ * provided using {!check} with assumptions. *)
val assert_and_track : solver -> Expr.expr -> Expr.expr -> unit
(** The number of assertions in the solver. *)
@@ -2724,29 +2716,29 @@ sig
val get_assertions : solver -> Expr.expr list
(** Checks whether the assertions in the solver are consistent or not.
-
- {!Model}
- {!get_unsat_core}
- {!Proof} *)
+
+ {!Model}
+ {!get_unsat_core}
+ {!Proof} *)
val check : solver -> Expr.expr list -> status
(** The model of the last [Check].
-
- The result is [None] if [Check] was not invoked before,
- if its results was not [SATISFIABLE], or if model production is not enabled. *)
+
+ The result is [None] if [Check] was not invoked before,
+ if its results was not [SATISFIABLE], or if model production is not enabled. *)
val get_model : solver -> Model.model option
(** The proof of the last [Check].
-
- The result is [null] if [Check] was not invoked before,
- if its results was not [UNSATISFIABLE], or if proof production is disabled. *)
+
+ The result is [null] if [Check] was not invoked before,
+ if its results was not [UNSATISFIABLE], or if proof production is disabled. *)
val get_proof : solver -> Expr.expr option
(** The unsat core of the last [Check].
-
- The unsat core is a subset of [Assertions]
- The result is empty if [Check] was not invoked before,
- if its results was not [UNSATISFIABLE], or if core production is disabled. *)
+
+ The unsat core is a subset of [Assertions]
+ The result is empty if [Check] was not invoked before,
+ if its results was not [UNSATISFIABLE], or if core production is disabled. *)
val get_unsat_core : solver -> AST.ast list
(** A brief justification of why the last call to [Check] returned [UNKNOWN]. *)
@@ -2756,23 +2748,23 @@ sig
val get_statistics : solver -> Statistics.statistics
(** Creates a new (incremental) solver.
-
- This solver also uses a set of builtin tactics for handling the first
- check-sat command, and check-sat commands that take more than a given
- number of milliseconds to be solved. *)
+
+ This solver also uses a set of builtin tactics for handling the first
+ check-sat command, and check-sat commands that take more than a given
+ number of milliseconds to be solved. *)
val mk_solver : context -> Symbol.symbol option -> solver
(** Creates a new (incremental) solver.
- {!mk_solver} *)
+ {!mk_solver} *)
val mk_solver_s : context -> string -> solver
(** Creates a new (incremental) solver. *)
val mk_simple_solver : context -> solver
(** Creates a solver that is implemented using the given tactic.
-
- The solver supports the commands [Push] and [Pop], but it
- will always solve each check from scratch. *)
+
+ The solver supports the commands [Push] and [Pop], but it
+ will always solve each check from scratch. *)
val mk_solver_t : context -> Tactic.tactic -> solver
(** A string representation of the solver. *)
@@ -2806,32 +2798,32 @@ sig
val add_fact : fixedpoint -> FuncDecl.func_decl -> int list -> unit
(** Query the fixedpoint solver.
- A query is a conjunction of constraints. The constraints may include the recursively defined relations.
- 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. *)
+ A query is a conjunction of constraints. The constraints may include the recursively defined relations.
+ 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. *)
val query : fixedpoint -> Expr.expr -> Solver.status
(** Query the fixedpoint solver.
- A query is an array of relations.
- The query is satisfiable if there is an instance of some relation that is non-empty.
- The query is unsatisfiable if there are no derivations satisfying any of the relations. *)
+ A query is an array of relations.
+ The query is satisfiable if there is an instance of some relation that is non-empty.
+ The query is unsatisfiable if there are no derivations satisfying any of the relations. *)
val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status
(** Creates a backtracking point.
- {!pop} *)
+ {!pop} *)
val push : fixedpoint -> unit
(** Backtrack one backtracking point.
- Note that an exception is thrown if Pop is called without a corresponding [Push]
- {!push} *)
+ Note that an exception is thrown if Pop is called without a corresponding [Push]
+ {!push} *)
val pop : fixedpoint -> unit
(** Update named rule into in the fixedpoint solver. *)
val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit
(** Retrieve satisfying instance or instances of solver,
- or definitions for the recursive predicates that show unsatisfiability. *)
+ or definitions for the recursive predicates that show unsatisfiability. *)
val get_answer : fixedpoint -> Expr.expr option
(** Retrieve explanation why fixedpoint engine returned status Unknown. *)
@@ -2844,7 +2836,7 @@ sig
val get_cover_delta : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr option
(** Add property about the predicate.
- The property is added at level. *)
+ The property is added at level. *)
val add_cover : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr -> unit
(** Retrieve internal string representation of fixedpoint object. *)
@@ -2871,7 +2863,7 @@ module SMT :
sig
(** Convert a benchmark into an SMT-LIB formatted string.
- @return A string representation of the benchmark. *)
+ @return A string representation of the benchmark. *)
val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string
(** Parse the given string using the SMT-LIB parser.
@@ -2884,7 +2876,7 @@ sig
val parse_smtlib_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
(** Parse the given file using the SMT-LIB parser.
- {!parse_smtlib_string} *)
+ {!parse_smtlib_string} *)
val parse_smtlib_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> unit
(** The number of SMTLIB formulas parsed by the last call to [ParseSMTLIBString] or [ParseSMTLIBFile]. *)
@@ -2913,15 +2905,61 @@ sig
(** Parse the given string using the SMT-LIB2 parser.
- {!parse_smtlib_string}
- @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *)
+ {!parse_smtlib_string}
+ @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *)
val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
(** Parse the given file using the SMT-LIB2 parser.
- {!parse_smtlib2_string} *)
+ {!parse_smtlib2_string} *)
val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
end
+(** Interpolation *)
+module Interpolation :
+sig
+
+ (** Create an AST node marking a formula position for interpolation.
+ The expression must have Boolean sort. *)
+ val mk_interpolant : context -> Expr.expr -> Expr.expr
+
+ (** The interpolation context is suitable for generation of interpolants.
+ For more information on interpolation please refer
+ too the C/C++ API, which is well documented. *)
+ val mk_interpolation_context : (string * string) list -> context
+
+ (** Gets an interpolant.
+ For more information on interpolation please refer
+ too the C/C++ API, which is well documented. *)
+ val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> AST.ASTVector.ast_vector
+
+ (** Computes an interpolant.
+ For more information on interpolation please refer
+ too the C/C++ API, which is well documented. *)
+ val compute_interpolant : context -> Expr.expr -> Params.params -> (AST.ASTVector.ast_vector * Model.model)
+
+ (** Retrieves an interpolation profile.
+ For more information on interpolation please refer
+ too the C/C++ API, which is well documented. *)
+ val get_interpolation_profile : context -> string
+
+ (** Read an interpolation problem from file.
+ For more information on interpolation please refer
+ too the C/C++ API, which is well documented. *)
+ val read_interpolation_problem : context -> string -> (Expr.expr list * int list * Expr.expr list)
+
+ (** Check the correctness of an interpolant.
+ For more information on interpolation please refer
+ too the C/C++ API, which is well documented. *)
+ val check_interpolant : context -> int -> Expr.expr list -> int list -> Expr.expr list -> int -> Expr.expr list -> unit
+
+ (** Write an interpolation problem to file suitable for reading with
+ Z3_read_interpolation_problem.
+ For more information on interpolation please refer
+ too the C/C++ API, which is well documented. *)
+ val write_interpolation_problem : context -> int -> Expr.expr list -> int list -> string -> int -> Expr.expr list -> unit
+
+end
+
(** Set a global (or module) parameter, which is shared by all Z3 contexts.
When a Z3 module is initialized it will use the value of these parameters
@@ -2939,9 +2977,9 @@ end
val set_global_param : string -> string -> unit
(** Get a global (or module) parameter.
-
+
Returns None if the parameter does not exist.
- The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
+ The caller must invoke #Z3_global_param_del_value to delete the value returned at param_value.
This function cannot be invoked simultaneously from different threads without synchronization.
The result string stored in param_value is stored in a shared location.
*)