mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
ML API: moved more objects into normal types.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
6257c56901
commit
3347d7ca8c
|
|
@ -14,7 +14,6 @@ open Z3.Tactic.ApplyResult
|
|||
open Z3.Probe
|
||||
open Z3.Solver
|
||||
open Z3.Arithmetic
|
||||
open Z3.Fixedpoints
|
||||
|
||||
exception TestFailedException of string
|
||||
|
||||
|
|
|
|||
450
src/api/ml/z3.ml
450
src/api/ml/z3.ml
|
|
@ -656,70 +656,6 @@ let tacticaton (a : tactic array) =
|
|||
let f (e : tactic) = e#gno in
|
||||
Array.map f a
|
||||
|
||||
(** Function interpretation entry objects *)
|
||||
class func_entry ctx =
|
||||
object (self)
|
||||
inherit z3object ctx None as super
|
||||
method cnstr_obj obj = (self#sno ctx obj) ; self
|
||||
method incref nc o = Z3native.func_entry_inc_ref nc o
|
||||
method decref nc o = Z3native.func_entry_dec_ref nc o
|
||||
end
|
||||
|
||||
(** Function interpretation objects *)
|
||||
class func_interp ctx =
|
||||
object (self)
|
||||
inherit z3object ctx None as super
|
||||
method cnstr_obj obj = (self#sno ctx obj) ; self
|
||||
method incref nc o = Z3native.func_interp_inc_ref nc o
|
||||
method decref nc o = Z3native.func_interp_dec_ref nc o
|
||||
end
|
||||
|
||||
(** Tactic application result objects *)
|
||||
class apply_result ctx =
|
||||
object (self)
|
||||
inherit z3object ctx None as super
|
||||
method cnstr_obj obj = (self#sno ctx obj) ; self
|
||||
method incref nc o = Z3native.apply_result_inc_ref nc o
|
||||
method decref nc o = Z3native.apply_result_dec_ref nc o
|
||||
end
|
||||
|
||||
(** Probe objects *)
|
||||
class probe ctx =
|
||||
object (self)
|
||||
inherit z3object ctx None as super
|
||||
method cnstr_obj obj = (self#sno ctx obj) ; self
|
||||
method incref nc o = Z3native.probe_inc_ref nc o
|
||||
method decref nc o = Z3native.probe_dec_ref nc o
|
||||
end
|
||||
|
||||
(** Statistical value objects *)
|
||||
class statistics_entry =
|
||||
object (self)
|
||||
val mutable m_key : string = ""
|
||||
val mutable m_is_int = false
|
||||
val mutable m_is_float = false
|
||||
val mutable m_int = 0
|
||||
val mutable m_float = 0.0
|
||||
|
||||
method cnstr_si k v =
|
||||
m_key <- k;
|
||||
m_is_int <- true;
|
||||
m_int <- v;
|
||||
self
|
||||
|
||||
method cnstr_sd k v =
|
||||
m_key <- k;
|
||||
m_is_float <- true;
|
||||
m_float <- v;
|
||||
self
|
||||
|
||||
method key = m_key
|
||||
method int = m_int
|
||||
method float = m_float
|
||||
method is_int = m_is_int
|
||||
method is_float = m_is_float
|
||||
end
|
||||
|
||||
|
||||
type z3_native_object = {
|
||||
m_ctx : context ;
|
||||
|
|
@ -4353,7 +4289,7 @@ struct
|
|||
type model = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let model_cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let res : model = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.model_inc_ref ;
|
||||
|
|
@ -4370,6 +4306,18 @@ struct
|
|||
*)
|
||||
module FuncInterp =
|
||||
struct
|
||||
type func_interp = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let res : func_interp = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.func_interp_inc_ref ;
|
||||
dec_ref = Z3native.func_interp_dec_ref } in
|
||||
(z3obj_sno res ctx no) ;
|
||||
(z3obj_cnstr res) ;
|
||||
res
|
||||
(**/**)
|
||||
|
||||
(** Function interpretations entries
|
||||
|
||||
|
|
@ -4377,23 +4325,36 @@ struct
|
|||
*)
|
||||
module FuncEntry =
|
||||
struct
|
||||
type func_entry = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let res : func_entry = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.func_entry_inc_ref ;
|
||||
dec_ref = Z3native.func_entry_dec_ref } in
|
||||
(z3obj_sno res ctx no) ;
|
||||
(z3obj_cnstr res) ;
|
||||
res
|
||||
(**/**)
|
||||
|
||||
(**
|
||||
Return the (symbolic) value of this entry.
|
||||
*)
|
||||
let get_value ( x : func_entry ) =
|
||||
create_expr x#gc (Z3native.func_entry_get_value x#gnc x#gno)
|
||||
create_expr (z3obj_gc x) (Z3native.func_entry_get_value (z3obj_gnc x) (z3obj_gno x))
|
||||
|
||||
(**
|
||||
The number of arguments of the entry.
|
||||
*)
|
||||
let get_num_args ( x : func_entry ) = Z3native.func_entry_get_num_args x#gnc x#gno
|
||||
let get_num_args ( x : func_entry ) = Z3native.func_entry_get_num_args (z3obj_gnc x) (z3obj_gno x)
|
||||
|
||||
(**
|
||||
The arguments of the function entry.
|
||||
*)
|
||||
let get_args ( x : func_entry ) =
|
||||
let n = (get_num_args x) in
|
||||
let f i = (create_expr x#gc (Z3native.func_entry_get_arg x#gnc x#gno i)) in
|
||||
let f i = (create_expr (z3obj_gc x) (Z3native.func_entry_get_arg (z3obj_gnc x) (z3obj_gno x) i)) in
|
||||
Array.init n f
|
||||
|
||||
(**
|
||||
|
|
@ -4408,25 +4369,25 @@ struct
|
|||
(**
|
||||
The number of entries in the function interpretation.
|
||||
*)
|
||||
let get_num_entries ( x: func_interp ) = Z3native.func_interp_get_num_entries x#gnc x#gno
|
||||
let get_num_entries ( x: func_interp ) = Z3native.func_interp_get_num_entries (z3obj_gnc x) (z3obj_gno x)
|
||||
|
||||
(**
|
||||
The entries in the function interpretation
|
||||
*)
|
||||
let get_entries ( x : func_interp ) =
|
||||
let n = (get_num_entries x) in
|
||||
let f i = ((new func_entry x#gc)#cnstr_obj (Z3native.func_interp_get_entry x#gnc x#gno i)) in
|
||||
let f i = (FuncEntry.cnstr (z3obj_gc x) (Z3native.func_interp_get_entry (z3obj_gnc x) (z3obj_gno x) i)) in
|
||||
Array.init n f
|
||||
|
||||
(**
|
||||
The (symbolic) `else' value of the function interpretation.
|
||||
*)
|
||||
let get_else ( x : func_interp ) = create_expr x#gc (Z3native.func_interp_get_else x#gnc x#gno)
|
||||
let get_else ( x : func_interp ) = create_expr (z3obj_gc x) (Z3native.func_interp_get_else (z3obj_gnc x) (z3obj_gno x))
|
||||
|
||||
(**
|
||||
The arity of the function interpretation
|
||||
*)
|
||||
let get_arity ( x : func_interp ) = Z3native.func_interp_get_arity x#gnc x#gno
|
||||
let get_arity ( x : func_interp ) = Z3native.func_interp_get_arity (z3obj_gnc x) (z3obj_gno x)
|
||||
|
||||
(**
|
||||
A string representation of the function interpretation.
|
||||
|
|
@ -4486,7 +4447,7 @@ struct
|
|||
| _ -> raise (Z3native.Exception "Constant functions do not have a function interpretation; use ConstInterp");
|
||||
else
|
||||
let n = (Z3native.model_get_func_interp (z3obj_gnc x) (z3obj_gno x) f#gno) in
|
||||
if (Z3native.is_null n) then None else Some ((new func_interp (z3obj_gc x))#cnstr_obj n)
|
||||
if (Z3native.is_null n) then None else Some (FuncInterp.cnstr (z3obj_gc x) n)
|
||||
|
||||
(** The number of constants that have an interpretation in the model. *)
|
||||
let get_num_consts ( x : model ) = Z3native.model_get_num_consts (z3obj_gnc x) (z3obj_gno x)
|
||||
|
|
@ -4579,6 +4540,130 @@ struct
|
|||
end
|
||||
|
||||
|
||||
(** Probes
|
||||
|
||||
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide
|
||||
which solver and/or preprocessing step will be used.
|
||||
The complete list of probes may be obtained using the procedures <c>Context.NumProbes</c>
|
||||
and <c>Context.ProbeNames</c>.
|
||||
It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end.
|
||||
*)
|
||||
module Probe =
|
||||
struct
|
||||
type probe = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let res : probe = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.probe_inc_ref ;
|
||||
dec_ref = Z3native.probe_dec_ref } in
|
||||
(z3obj_sno res ctx no) ;
|
||||
(z3obj_cnstr res) ;
|
||||
res
|
||||
(**/**)
|
||||
|
||||
(**
|
||||
Execute the probe over the goal.
|
||||
<returns>A probe always produce a double value.
|
||||
"Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns>
|
||||
*)
|
||||
let apply ( x : probe ) (g : goal) =
|
||||
Z3native.probe_apply (z3obj_gnc x) (z3obj_gno x) g#gno
|
||||
|
||||
(**
|
||||
The number of supported Probes.
|
||||
*)
|
||||
let get_num_probes ( ctx : context ) =
|
||||
Z3native.get_num_probes (context_gno ctx)
|
||||
|
||||
(**
|
||||
The names of all supported Probes.
|
||||
*)
|
||||
let get_probe_names ( ctx : context ) =
|
||||
let n = (get_num_probes ctx) in
|
||||
let f i = (Z3native.get_probe_name (context_gno ctx) i) in
|
||||
Array.init n f
|
||||
|
||||
(**
|
||||
Returns a string containing a description of the probe with the given name.
|
||||
*)
|
||||
let get_probe_description ( ctx : context ) ( name : string ) =
|
||||
Z3native.probe_get_descr (context_gno ctx) name
|
||||
|
||||
(**
|
||||
Creates a new Probe.
|
||||
*)
|
||||
let mk_probe ( ctx : context ) ( name : string ) =
|
||||
(cnstr ctx (Z3native.mk_probe (context_gno ctx) name))
|
||||
|
||||
(**
|
||||
Create a probe that always evaluates to <paramref name="val"/>.
|
||||
*)
|
||||
let const ( ctx : context ) ( v : float ) =
|
||||
(cnstr ctx (Z3native.probe_const (context_gno ctx) v))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is less than the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let lt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(cnstr ctx (Z3native.probe_lt (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2)))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is greater than the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let gt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(cnstr ctx (Z3native.probe_gt (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2)))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is less than or equal the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let le ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(cnstr ctx (Z3native.probe_le (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2)))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is greater than or equal the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let ge ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(cnstr ctx (Z3native.probe_ge (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2)))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is equal to the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let eq ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(cnstr ctx (Z3native.probe_eq (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2)))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value <paramref name="p1"/>
|
||||
and <paramref name="p2"/> evaluate to "true".
|
||||
*)
|
||||
(* CMW: and is a keyword *)
|
||||
let and_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(cnstr ctx (Z3native.probe_and (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2)))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value <paramref name="p1"/>
|
||||
or <paramref name="p2"/> evaluate to "true".
|
||||
*)
|
||||
(* CMW: or is a keyword *)
|
||||
let or_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(cnstr ctx (Z3native.probe_or (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2)))
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value <paramref name="p"/>
|
||||
does not evaluate to "true".
|
||||
*)
|
||||
(* CMW: is not a keyword? *)
|
||||
let not_ ( ctx : context ) ( p : probe ) =
|
||||
(cnstr ctx (Z3native.probe_not (context_gno ctx) (z3obj_gno p)))
|
||||
end
|
||||
|
||||
|
||||
(** Tactics
|
||||
|
||||
Tactics are the basic building block for creating custom solvers for specific problem domains.
|
||||
|
|
@ -4594,29 +4679,42 @@ struct
|
|||
tactic to a goal. It contains the subgoals that were produced. *)
|
||||
module ApplyResult =
|
||||
struct
|
||||
type apply_result = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let res : apply_result = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.apply_result_inc_ref ;
|
||||
dec_ref = Z3native.apply_result_dec_ref } in
|
||||
(z3obj_sno res ctx no) ;
|
||||
(z3obj_cnstr res) ;
|
||||
res
|
||||
(**/**)
|
||||
|
||||
(** The number of Subgoals. *)
|
||||
let get_num_subgoals ( x : apply_result ) =
|
||||
Z3native.apply_result_get_num_subgoals x#gnc x#gno
|
||||
Z3native.apply_result_get_num_subgoals (z3obj_gnc x) (z3obj_gno x)
|
||||
|
||||
(** Retrieves the subgoals from the apply_result. *)
|
||||
let get_subgoals ( x : apply_result ) =
|
||||
let n = (get_num_subgoals x) in
|
||||
let f i = (new goal x#gc)#cnstr_obj (Z3native.apply_result_get_subgoal x#gnc x#gno i) in
|
||||
let f i = (new goal (z3obj_gc x))#cnstr_obj (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) in
|
||||
Array.init n f
|
||||
|
||||
(** Retrieves the subgoals from the apply_result. *)
|
||||
let get_subgoal ( x : apply_result ) ( i : int ) =
|
||||
(new goal x#gc)#cnstr_obj (Z3native.apply_result_get_subgoal x#gnc x#gno i)
|
||||
(new goal (z3obj_gc x))#cnstr_obj (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i)
|
||||
|
||||
(** Convert a model for the subgoal <paramref name="i"/> into a model for the original
|
||||
goal <c>g</c>, that the ApplyResult was obtained from.
|
||||
#return A model for <c>g</c>
|
||||
*)
|
||||
let convert_model ( x : apply_result ) ( i : int ) ( m : Model.model ) =
|
||||
Model.model_cnstr x#gc (Z3native.apply_result_convert_model x#gnc x#gno i (z3obj_gno m))
|
||||
Model.cnstr (z3obj_gc x) (Z3native.apply_result_convert_model (z3obj_gnc x) (z3obj_gno x) i (z3obj_gno m))
|
||||
|
||||
(** A string representation of the ApplyResult. *)
|
||||
let to_string ( x : apply_result ) = Z3native.apply_result_to_string x#gnc x#gno
|
||||
let to_string ( x : apply_result ) = Z3native.apply_result_to_string (z3obj_gnc x) (z3obj_gno x)
|
||||
end
|
||||
|
||||
(** A string containing a description of parameters accepted by the tactic. *)
|
||||
|
|
@ -4630,8 +4728,8 @@ end
|
|||
(** Apply the tactic to the goal. *)
|
||||
let apply ( x : tactic ) ( g : goal ) ( p : params option ) =
|
||||
match p with
|
||||
| None -> (new apply_result x#gc)#cnstr_obj (Z3native.tactic_apply x#gnc x#gno g#gno)
|
||||
| Some (pn) -> (new apply_result x#gc)#cnstr_obj (Z3native.tactic_apply_ex x#gnc x#gno g#gno pn#gno)
|
||||
| None -> (ApplyResult.cnstr x#gc (Z3native.tactic_apply x#gnc x#gno g#gno))
|
||||
| Some (pn) -> (ApplyResult.cnstr x#gc (Z3native.tactic_apply_ex x#gnc x#gno g#gno pn#gno))
|
||||
|
||||
(**
|
||||
The number of supported tactics.
|
||||
|
|
@ -4695,15 +4793,15 @@ end
|
|||
If <paramref name="p"/> evaluates to false, then the new tactic behaves like the <c>skip</c> tactic.
|
||||
*)
|
||||
(* CMW: when is a keyword *)
|
||||
let when_ ( ctx : context ) ( p : probe ) ( t : tactic ) =
|
||||
(new tactic ctx)#cnstr_obj (Z3native.tactic_when (context_gno ctx) p#gno t#gno)
|
||||
let when_ ( ctx : context ) ( p : Probe.probe ) ( t : tactic ) =
|
||||
(new tactic ctx)#cnstr_obj (Z3native.tactic_when (context_gno ctx) (z3obj_gno p) t#gno)
|
||||
|
||||
(**
|
||||
Create a tactic that applies <paramref name="t1"/> to a given goal if the probe
|
||||
<paramref name="p"/> evaluates to true and <paramref name="t2"/> otherwise.
|
||||
*)
|
||||
let cond ( ctx : context ) ( p : probe ) ( t1 : tactic ) ( t2 : tactic ) =
|
||||
(new tactic ctx)#cnstr_obj (Z3native.tactic_cond (context_gno ctx) p#gno t1#gno t2#gno)
|
||||
let cond ( ctx : context ) ( p : Probe.probe ) ( t1 : tactic ) ( t2 : tactic ) =
|
||||
(new tactic ctx)#cnstr_obj (Z3native.tactic_cond (context_gno ctx) (z3obj_gno p) t1#gno t2#gno)
|
||||
|
||||
(**
|
||||
Create a tactic that keeps applying <paramref name="t"/> until the goal is not
|
||||
|
|
@ -4727,8 +4825,8 @@ end
|
|||
(**
|
||||
Create a tactic that fails if the probe <paramref name="p"/> evaluates to false.
|
||||
*)
|
||||
let fail_if ( ctx : context ) ( p : probe ) =
|
||||
(new tactic ctx)#cnstr_obj (Z3native.tactic_fail_if (context_gno ctx) p#gno)
|
||||
let fail_if ( ctx : context ) ( p : Probe.probe ) =
|
||||
(new tactic ctx)#cnstr_obj (Z3native.tactic_fail_if (context_gno ctx) (z3obj_gno p))
|
||||
|
||||
(**
|
||||
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
|
||||
|
|
@ -4771,116 +4869,6 @@ end
|
|||
Z3native.interrupt (context_gno ctx)
|
||||
end
|
||||
|
||||
(** Probes
|
||||
|
||||
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide
|
||||
which solver and/or preprocessing step will be used.
|
||||
The complete list of probes may be obtained using the procedures <c>Context.NumProbes</c>
|
||||
and <c>Context.ProbeNames</c>.
|
||||
It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end.
|
||||
*)
|
||||
module Probe =
|
||||
struct
|
||||
(**
|
||||
Execute the probe over the goal.
|
||||
<returns>A probe always produce a double value.
|
||||
"Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns>
|
||||
*)
|
||||
let apply ( x : probe ) (g : goal) =
|
||||
Z3native.probe_apply x#gnc x#gno g#gno
|
||||
|
||||
(**
|
||||
The number of supported Probes.
|
||||
*)
|
||||
let get_num_probes ( ctx : context ) =
|
||||
Z3native.get_num_probes (context_gno ctx)
|
||||
|
||||
(**
|
||||
The names of all supported Probes.
|
||||
*)
|
||||
let get_probe_names ( ctx : context ) =
|
||||
let n = (get_num_probes ctx) in
|
||||
let f i = (Z3native.get_probe_name (context_gno ctx) i) in
|
||||
Array.init n f
|
||||
|
||||
(**
|
||||
Returns a string containing a description of the probe with the given name.
|
||||
*)
|
||||
let get_probe_description ( ctx : context ) ( name : string ) =
|
||||
Z3native.probe_get_descr (context_gno ctx) name
|
||||
|
||||
(**
|
||||
Creates a new Probe.
|
||||
*)
|
||||
let mk_probe ( ctx : context ) ( name : string ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.mk_probe (context_gno ctx) name)
|
||||
|
||||
(**
|
||||
Create a probe that always evaluates to <paramref name="val"/>.
|
||||
*)
|
||||
let const ( ctx : context ) ( v : float ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_const (context_gno ctx) v)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is less than the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let lt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_lt (context_gno ctx) p1#gno p2#gno)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is greater than the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let gt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_gt (context_gno ctx) p1#gno p2#gno)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is less than or equal the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let le ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_le (context_gno ctx) p1#gno p2#gno)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is greater than or equal the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let ge ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_ge (context_gno ctx) p1#gno p2#gno)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
|
||||
is equal to the value returned by <paramref name="p2"/>
|
||||
*)
|
||||
let eq ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_eq (context_gno ctx) p1#gno p2#gno)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value <paramref name="p1"/>
|
||||
and <paramref name="p2"/> evaluate to "true".
|
||||
*)
|
||||
(* CMW: and is a keyword *)
|
||||
let and_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_and (context_gno ctx) p1#gno p2#gno)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value <paramref name="p1"/>
|
||||
or <paramref name="p2"/> evaluate to "true".
|
||||
*)
|
||||
(* CMW: or is a keyword *)
|
||||
let or_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_or (context_gno ctx) p1#gno p2#gno)
|
||||
|
||||
(**
|
||||
Create a probe that evaluates to "true" when the value <paramref name="p"/>
|
||||
does not evaluate to "true".
|
||||
*)
|
||||
(* CMW: is not a keyword? *)
|
||||
let not_ ( ctx : context ) ( p : probe ) =
|
||||
(new probe ctx)#cnstr_obj (Z3native.probe_not (context_gno ctx) p#gno)
|
||||
end
|
||||
|
||||
|
||||
(** Solvers *)
|
||||
module Solver =
|
||||
|
|
@ -4888,7 +4876,7 @@ struct
|
|||
type solver = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let solver_cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let res : solver = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.solver_inc_ref ;
|
||||
|
|
@ -4911,7 +4899,7 @@ struct
|
|||
type statistics = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let statistics_cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let cnstr ( ctx : context ) ( no : Z3native.ptr ) =
|
||||
let res : statistics = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.stats_inc_ref ;
|
||||
|
|
@ -4922,25 +4910,55 @@ struct
|
|||
(**/**)
|
||||
|
||||
(**
|
||||
Statistical data is organized into pairs of [Key, Entry], where every
|
||||
Entry is either a <c>DoubleEntry</c> or a <c>UIntEntry</c>
|
||||
Statistical data is organized into pairs of \[Key, Entry\], where every
|
||||
Entry is either a floating point or integer value.
|
||||
|
||||
*)
|
||||
module Entry =
|
||||
struct
|
||||
type statistics_entry = {
|
||||
mutable m_key : string;
|
||||
mutable m_is_int : bool ;
|
||||
mutable m_is_float : bool ;
|
||||
mutable m_int : int ;
|
||||
mutable m_float : float }
|
||||
|
||||
(**/**)
|
||||
let cnstr_si k v =
|
||||
let res : statistics_entry = {
|
||||
m_key = k ;
|
||||
m_is_int = true ;
|
||||
m_is_float = false ;
|
||||
m_int = v ;
|
||||
m_float = 0.0
|
||||
} in
|
||||
res
|
||||
|
||||
let cnstr_sd k v =
|
||||
let res : statistics_entry = {
|
||||
m_key = k ;
|
||||
m_is_int = false ;
|
||||
m_is_float = true ;
|
||||
m_int = 0 ;
|
||||
m_float = v
|
||||
} in
|
||||
res
|
||||
(**/**)
|
||||
|
||||
(** The key of the entry. *)
|
||||
let get_key (x : statistics_entry) = x#key
|
||||
let get_key (x : statistics_entry) = x.m_key
|
||||
|
||||
(** The int-value of the entry. *)
|
||||
let get_int (x : statistics_entry) = x#int
|
||||
let get_int (x : statistics_entry) = x.m_int
|
||||
|
||||
(** The float-value of the entry. *)
|
||||
let get_float (x : statistics_entry) = x#float
|
||||
let get_float (x : statistics_entry) = x.m_float
|
||||
|
||||
(** True if the entry is uint-valued. *)
|
||||
let is_int (x : statistics_entry) = x#is_int
|
||||
let is_int (x : statistics_entry) = x.m_is_int
|
||||
|
||||
(** True if the entry is double-valued. *)
|
||||
let is_float (x : statistics_entry) = x#is_float
|
||||
let is_float (x : statistics_entry) = x.m_is_float
|
||||
|
||||
(** The string representation of the the entry's value. *)
|
||||
let to_string_value (x : statistics_entry) =
|
||||
|
|
@ -4967,9 +4985,9 @@ struct
|
|||
let f i = (
|
||||
let k = Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i in
|
||||
if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then
|
||||
((new statistics_entry)#cnstr_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i))
|
||||
(Entry.cnstr_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i))
|
||||
else
|
||||
((new statistics_entry)#cnstr_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i))
|
||||
(Entry.cnstr_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i))
|
||||
) in
|
||||
Array.init n f
|
||||
|
||||
|
|
@ -5087,7 +5105,7 @@ struct
|
|||
if (Z3native.is_null q) then
|
||||
None
|
||||
else
|
||||
Some (Model.model_cnstr (z3obj_gc x) q)
|
||||
Some (Model.cnstr (z3obj_gc x) q)
|
||||
|
||||
(**
|
||||
The proof of the last <c>Check</c>.
|
||||
|
|
@ -5125,7 +5143,7 @@ struct
|
|||
Solver statistics.
|
||||
*)
|
||||
let get_statistics ( x : solver ) =
|
||||
(Statistics.statistics_cnstr (z3obj_gc x) (Z3native.solver_get_statistics (z3obj_gnc x) (z3obj_gno x)))
|
||||
(Statistics.cnstr (z3obj_gc x) (Z3native.solver_get_statistics (z3obj_gnc x) (z3obj_gno x)))
|
||||
|
||||
(**
|
||||
Creates a new (incremental) solver.
|
||||
|
|
@ -5136,8 +5154,8 @@ struct
|
|||
*)
|
||||
let mk_solver ( ctx : context ) ( logic : symbol option) =
|
||||
match logic with
|
||||
| None -> (solver_cnstr ctx (Z3native.mk_solver (context_gno ctx)))
|
||||
| Some (x) -> (solver_cnstr ctx (Z3native.mk_solver_for_logic (context_gno ctx) x#gno))
|
||||
| None -> (cnstr ctx (Z3native.mk_solver (context_gno ctx)))
|
||||
| Some (x) -> (cnstr ctx (Z3native.mk_solver_for_logic (context_gno ctx) x#gno))
|
||||
|
||||
(**
|
||||
Creates a new (incremental) solver.
|
||||
|
|
@ -5150,7 +5168,7 @@ struct
|
|||
Creates a new (incremental) solver.
|
||||
*)
|
||||
let mk_simple_solver ( ctx : context ) =
|
||||
(solver_cnstr ctx (Z3native.mk_simple_solver (context_gno ctx)))
|
||||
(cnstr ctx (Z3native.mk_simple_solver (context_gno ctx)))
|
||||
|
||||
(**
|
||||
Creates a solver that is implemented using the given tactic.
|
||||
|
|
@ -5159,7 +5177,7 @@ struct
|
|||
will always solve each check from scratch.
|
||||
*)
|
||||
let mk_solver_t ( ctx : context ) ( t : tactic ) =
|
||||
(solver_cnstr ctx (Z3native.mk_solver_from_tactic (context_gno ctx) t#gno))
|
||||
(cnstr ctx (Z3native.mk_solver_from_tactic (context_gno ctx) t#gno))
|
||||
|
||||
(**
|
||||
A string representation of the solver.
|
||||
|
|
@ -5169,12 +5187,12 @@ end
|
|||
|
||||
|
||||
(** Fixedpoint solving *)
|
||||
module Fixedpoints =
|
||||
module Fixedpoint =
|
||||
struct
|
||||
type fixedpoint = z3_native_object
|
||||
|
||||
(**/**)
|
||||
let fixedpoint_cnstr ( ctx : context ) =
|
||||
let cnstr ( ctx : context ) =
|
||||
let res : fixedpoint = { m_ctx = ctx ;
|
||||
m_n_obj = null ;
|
||||
inc_ref = Z3native.fixedpoint_inc_ref ;
|
||||
|
|
@ -5354,7 +5372,7 @@ struct
|
|||
(**
|
||||
Create a Fixedpoint context.
|
||||
*)
|
||||
let mk_fixedpoint ( ctx : context ) = fixedpoint_cnstr ctx
|
||||
let mk_fixedpoint ( ctx : context ) = cnstr ctx
|
||||
end
|
||||
|
||||
(** Global and context options
|
||||
|
|
|
|||
Loading…
Reference in a new issue