mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

ML API: refactoring

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-06-03 19:12:00 +01:00
parent aaa835484f
commit b81bae76b2
2 changed files with 73 additions and 116 deletions
Download patch file Download diff file Expand all files Collapse all files

74
src/api/ml/z3.ml
View file

@ -7,6 +7,8 @@
open Z3enums open Z3enums
exception Error = Z3native.Exception
(* Some helpers. *) (* Some helpers. *)
let null = Z3native.mk_null() let null = Z3native.mk_null()
let is_null o = (Z3native.is_null o) let is_null o = (Z3native.is_null o)
@ -283,7 +285,7 @@ struct
Z3native.ast_map_to_string (z3obj_gnc x) (z3obj_gno x) Z3native.ast_map_to_string (z3obj_gnc x) (z3obj_gno x)
end end
let get_hash_code ( x : ast ) = Z3native.get_ast_hash (z3obj_gnc x) (z3obj_gno x) let hash ( x : ast ) = Z3native.get_ast_hash (z3obj_gnc x) (z3obj_gno x)
let get_id ( x : ast ) = Z3native.get_ast_id (z3obj_gnc x) (z3obj_gno x) let get_id ( x : ast ) = Z3native.get_ast_id (z3obj_gnc x) (z3obj_gno x)
let get_ast_kind ( x : ast ) = (ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc x) (z3obj_gno x))) let get_ast_kind ( x : ast ) = (ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc x) (z3obj_gno x)))
@ -304,7 +306,7 @@ struct
let to_sexpr ( x : ast ) = Z3native.ast_to_string (z3obj_gnc x) (z3obj_gno x) let to_sexpr ( x : ast ) = Z3native.ast_to_string (z3obj_gnc x) (z3obj_gno x)
let ( = ) ( a : ast ) ( b : ast ) = (a == b) || let equal ( a : ast ) ( b : ast ) = (a == b) ||
if (z3obj_gnc a) != (z3obj_gnc b) then if (z3obj_gnc a) != (z3obj_gnc b) then
false false
else else
@ -314,8 +316,6 @@ struct
if (get_id a) < (get_id b) then -1 else if (get_id a) < (get_id b) then -1 else
if (get_id a) > (get_id b) then 1 else if (get_id a) > (get_id b) then 1 else
0 0
let ( < ) (a : ast) (b : ast) = (compare a b)
let translate ( x : ast ) ( to_ctx : context ) = let translate ( x : ast ) ( to_ctx : context ) =
if (z3obj_gnc x) == (context_gno to_ctx) then if (z3obj_gnc x) == (context_gno to_ctx) then
@ -361,7 +361,7 @@ struct
let f ( e : sort ) = match e with Sort(a) -> (AST.ptr_of_ast a) in let f ( e : sort ) = match e with Sort(a) -> (AST.ptr_of_ast a) in
Array.of_list (List.map f a) Array.of_list (List.map f a)
let ( = ) : sort -> sort -> bool = fun a b -> let equal : sort -> sort -> bool = fun a b ->
(a == b) || (a == b) ||
if (gnc a) != (gnc b) then if (gnc a) != (gnc b) then
false false
@ -424,7 +424,7 @@ sig
val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl
val mk_const_decl_s : context -> string -> Sort.sort -> func_decl val mk_const_decl_s : context -> string -> Sort.sort -> func_decl
val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl
val ( = ) : func_decl -> func_decl -> bool val equal : func_decl -> func_decl -> bool
val to_string : func_decl -> string val to_string : func_decl -> string
val get_id : func_decl -> int val get_id : func_decl -> int
val get_arity : func_decl -> int val get_arity : func_decl -> int
@ -498,7 +498,7 @@ end = struct
let get_float ( x : parameter ) = let get_float ( x : parameter ) =
match x with match x with
| P_Dbl(x) -> x | P_Dbl(x) -> x
| _ -> raise (Z3native.Exception "parameter is not a double") | _ -> raise (Z3native.Exception "parameter is not a float")
let get_symbol ( x : parameter ) = let get_symbol ( x : parameter ) =
match x with match x with
@ -545,7 +545,7 @@ end = struct
create_pdr ctx prefix [] range create_pdr ctx prefix [] range
let ( = ) ( a : func_decl ) ( b : func_decl ) = (a == b) || let equal ( a : func_decl ) ( b : func_decl ) = (a == b) ||
if (gnc a) != (gnc b) then if (gnc a) != (gnc b) then
false false
else else
@ -605,12 +605,8 @@ sig
end end
val add_bool : params -> Symbol.symbol -> bool -> unit val add_bool : params -> Symbol.symbol -> bool -> unit
val add_int : params -> Symbol.symbol -> int -> unit val add_int : params -> Symbol.symbol -> int -> unit
val add_double : params -> Symbol.symbol -> float -> unit val add_float : params -> Symbol.symbol -> float -> unit
val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
val add_s_bool : params -> string -> bool -> unit
val add_s_int : params -> string -> int -> unit
val add_s_double : params -> string -> float -> unit
val add_s_symbol : params -> string -> Symbol.symbol -> unit
val mk_params : context -> params val mk_params : context -> params
val to_string : params -> string val to_string : params -> string
end = struct end = struct
@ -650,24 +646,12 @@ end = struct
let add_int ( x : params ) (name : Symbol.symbol ) ( value : int ) = let add_int ( x : params ) (name : Symbol.symbol ) ( value : int ) =
Z3native.params_set_uint (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value Z3native.params_set_uint (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value
let add_double ( x : params ) ( name : Symbol.symbol ) ( value : float ) = let add_float ( x : params ) ( name : Symbol.symbol ) ( value : float ) =
Z3native.params_set_double (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value Z3native.params_set_double (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value
let add_symbol ( x : params ) ( name : Symbol.symbol ) ( value : Symbol.symbol ) = let add_symbol ( x : params ) ( name : Symbol.symbol ) ( value : Symbol.symbol ) =
Z3native.params_set_symbol (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) (Symbol.gno value) Z3native.params_set_symbol (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) (Symbol.gno value)
let add_s_bool ( x : params ) ( name : string ) ( value : bool ) =
add_bool x (Symbol.mk_string (z3obj_gc x) name) value
let add_s_int ( x : params) ( name : string ) ( value : int ) =
add_int x (Symbol.mk_string (z3obj_gc x) name) value
let add_s_double ( x : params ) ( name : string ) ( value : float ) =
add_double x (Symbol.mk_string (z3obj_gc x) name) value
let add_s_symbol ( x : params ) ( name : string ) ( value : Symbol.symbol ) =
add_symbol x (Symbol.mk_string (z3obj_gc x) name) value
let mk_params ( ctx : context ) = let mk_params ( ctx : context ) =
let res : params = { m_ctx = ctx ; let res : params = { m_ctx = ctx ;
m_n_obj = null ; m_n_obj = null ;
@ -734,8 +718,6 @@ sig
val is_xor : expr -> bool val is_xor : expr -> bool
val is_not : expr -> bool val is_not : expr -> bool
val is_implies : expr -> bool val is_implies : expr -> bool
val is_label : expr -> bool
val is_label_lit : expr -> bool
val is_oeq : expr -> bool val is_oeq : expr -> bool
val mk_const : context -> Symbol.symbol -> Sort.sort -> expr val mk_const : context -> Symbol.symbol -> Sort.sort -> expr
val mk_const_s : context -> string -> Sort.sort -> expr val mk_const_s : context -> string -> Sort.sort -> expr
@ -857,8 +839,6 @@ end = struct
let is_xor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR) let is_xor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR)
let is_not ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_NOT) let is_not ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_NOT)
let is_implies ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES) let is_implies ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES)
let is_label ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL)
let is_label_lit ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL_LIT)
let is_oeq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_OEQ) let is_oeq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_OEQ)
let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) = let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) =
@ -1530,20 +1510,20 @@ struct
let mk_real2int ( ctx : context ) ( t : expr ) = let mk_real2int ( ctx : context ) ( t : expr ) =
(expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (Expr.gno t))) (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (Expr.gno t)))
end
module AlgebraicNumber = module AlgebraicNumber =
struct struct
let to_upper ( x : expr ) ( precision : int ) = let to_upper ( x : expr ) ( precision : int ) =
expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision) expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision)
let to_lower ( x : expr ) precision = let to_lower ( x : expr ) precision =
expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision) expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision)
let to_decimal_string ( x : expr ) ( precision : int ) = let to_decimal_string ( x : expr ) ( precision : int ) =
Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision
let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x) let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
end
end end
let is_int ( x : expr ) = let is_int ( x : expr ) =
@ -2052,13 +2032,11 @@ 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 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 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) (mk_list f n_funcs) @ (mk_list g n_consts)
exception ModelEvaluationFailedException of string
let eval ( x : model ) ( t : expr ) ( completion : bool ) = 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 let (r, v) = (Z3native.model_eval (z3obj_gnc x) (z3obj_gno x) (Expr.gno t) completion) in
if not r then if not r then
raise (ModelEvaluationFailedException "evaluation failed") None
else else
expr_of_ptr (z3obj_gc x) v expr_of_ptr (z3obj_gc x) v
@ -2353,7 +2331,7 @@ struct
if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then
(Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i))
else else
(Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) (Entry.create_sd k (Z3native.stats_get_float_value (z3obj_gnc x) (z3obj_gno x) i))
) in ) in
mk_list f n mk_list f n

115
src/api/ml/z3.mli
View file

@ -5,6 +5,11 @@
@author CM Wintersteiger (cwinter) 2012-12-17 @author CM Wintersteiger (cwinter) 2012-12-17
*) *)
(** General Z3 exceptions
Many functions in this API may throw an exception; if they do, it is this one.*)
exception Error
(** Context objects. (** Context objects.
Most interactions with Z3 are interpreted in some context; many users will only Most interactions with Z3 are interpreted in some context; many users will only
@ -188,7 +193,7 @@ sig
(** The AST's hash code. (** The AST's hash code.
@return A hash code *) @return A hash code *)
val get_hash_code : ast -> int val hash : ast -> int
(** A unique identifier for the AST (unique among all ASTs). *) (** A unique identifier for the AST (unique among all ASTs). *)
val get_id : ast -> int val get_id : ast -> int
@ -220,15 +225,12 @@ sig
(** Comparison operator. (** Comparison operator.
@return True if the two ast's are from the same context @return True if the two ast's are from the same context
and represent the same sort; false otherwise. *) and represent the same sort; false otherwise. *)
val ( = ) : ast -> ast -> bool val equal : ast -> ast -> bool
(** Object Comparison. (** 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 val compare : ast -> ast -> int
(** Operator < *)
val ( < ) : ast -> ast -> int
(** Translates (copies) the AST to another context. (** 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 val translate : ast -> context -> ast
@ -263,7 +265,7 @@ sig
(** Comparison operator. (** Comparison operator.
@return True if the two sorts are from the same context @return True if the two sorts are from the same context
and represent the same sort; false otherwise. *) and represent the same sort; false otherwise. *)
val ( = ) : sort -> sort -> bool val equal : sort -> sort -> bool
(** Returns a unique identifier for the sort. *) (** Returns a unique identifier for the sort. *)
val get_id : sort -> int val get_id : sort -> int
@ -310,7 +312,7 @@ sig
(** The int value of the parameter.*) (** The int value of the parameter.*)
val get_int : parameter -> int val get_int : parameter -> int
(** The double value of the parameter.*) (** The float value of the parameter.*)
val get_float : parameter -> float val get_float : parameter -> float
(** The Symbol.Symbol value of the parameter.*) (** The Symbol.Symbol value of the parameter.*)
@ -351,7 +353,7 @@ sig
(** Comparison operator. (** Comparison operator.
@return True if a and b are from the same context and represent the same func_decl; false otherwise. *) @return True if a and b are from the same context and represent the same func_decl; false otherwise. *)
val ( = ) : func_decl -> func_decl -> bool val equal : func_decl -> func_decl -> bool
(** A string representations of the function declaration. *) (** A string representations of the function declaration. *)
val to_string : func_decl -> string val to_string : func_decl -> string
@ -423,23 +425,11 @@ sig
val add_int : params -> Symbol.symbol -> int -> unit val add_int : params -> Symbol.symbol -> int -> unit
(** Adds a parameter setting. *) (** Adds a parameter setting. *)
val add_double : params -> Symbol.symbol -> float -> unit val add_float : params -> Symbol.symbol -> float -> unit
(** Adds a parameter setting. *) (** Adds a parameter setting. *)
val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
(** Adds a parameter setting. *)
val add_s_bool : params -> string -> bool -> unit
(** Adds a parameter setting. *)
val add_s_int : params -> string -> int -> unit
(** Adds a parameter setting. *)
val add_s_double : params -> string -> float -> unit
(** Adds a parameter setting. *)
val add_s_symbol : params -> string -> Symbol.symbol -> unit
(** Creates a new parameter set *) (** Creates a new parameter set *)
val mk_params : context -> params val mk_params : context -> params
@ -583,16 +573,7 @@ sig
(** Indicates whether the term is an implication *) (** Indicates whether the term is an implication *)
val is_implies : Expr.expr -> bool val is_implies : Expr.expr -> bool
(** Indicates whether the term is a label (used by the Boogie Verification condition generator).
The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula. *)
val is_label : Expr.expr -> bool
(** Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
A label literal has a set of string parameters. It takes no arguments.
let is_label_lit ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL_LIT) *)
val is_label_lit : Expr.expr -> bool
(** Indicates whether the term is a binary equivalence modulo namings. (** Indicates whether the term is a binary equivalence modulo namings.
This binary predicate is used in proof terms. This binary predicate is used in proof terms.
It captures equisatisfiability and equivalence modulo renamings. *) It captures equisatisfiability and equivalence modulo renamings. *)
@ -1261,29 +1242,29 @@ sig
The semantics of this function follows the SMT-LIB standard for the function to_int. The semantics of this function follows the SMT-LIB standard for the function to_int.
The argument must be of real sort. *) The argument must be of real sort. *)
val mk_real2int : context -> Expr.expr -> Expr.expr val mk_real2int : context -> Expr.expr -> Expr.expr
end
(** Algebraic Numbers *)
(** Algebraic Numbers *) module AlgebraicNumber :
module AlgebraicNumber : sig
sig (** Return a upper bound for a given real algebraic number.
(** Return a upper bound for a given real algebraic number. The interval isolating the number is smaller than 1/10^precision.
The interval isolating the number is smaller than 1/10^precision. {!is_algebraic_number}
{!is_algebraic_number} @return A numeral Expr of sort Real *)
@return A numeral Expr of sort Real *) val to_upper : Expr.expr -> int -> Expr.expr
val to_upper : Expr.expr -> int -> Expr.expr
(** Return a lower bound for the given real algebraic number.
(** Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision.
The interval isolating the number is smaller than 1/10^precision. {!is_algebraic_number}
{!is_algebraic_number} @return A numeral Expr of sort Real *)
@return A numeral Expr of sort Real *) val to_lower : Expr.expr -> int -> Expr.expr
val to_lower : Expr.expr -> int -> Expr.expr
(** Returns a string representation in decimal notation.
(** Returns a string representation in decimal notation. The result has at most as many decimal places as the int argument provided.*)
The result has at most as many decimal places as the int argument provided.*) val to_decimal_string : Expr.expr -> int -> string
val to_decimal_string : Expr.expr -> int -> string
(** Returns a string representation of the numeral. *)
(** Returns a string representation of the numeral. *) val to_string : Expr.expr -> string
val to_string : Expr.expr -> string end
end end
(** Indicates whether the term is of integer sort. *) (** Indicates whether the term is of integer sort. *)
@ -2389,19 +2370,16 @@ sig
(** All symbols that have an interpretation in the model. *) (** All symbols that have an interpretation in the model. *)
val get_decls : model -> FuncDecl.func_decl list val get_decls : model -> FuncDecl.func_decl list
(** A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. *)
exception ModelEvaluationFailedException of string
(** Evaluates an expression in the current model. (** Evaluates an expression in the current model.
This function may fail if the argument contains quantifiers, This function may fail if the argument contains quantifiers,
is partial (MODEL_PARTIAL enabled), or if it is not well-sorted. is partial (MODEL_PARTIAL enabled), or if it is not well-sorted.
In this case a <c>ModelEvaluationFailedException</c> is thrown. In this case a <c>ModelEvaluationFailedException</c> is thrown.
*) *)
val eval : model -> Expr.expr -> bool -> Expr.expr val eval : model -> Expr.expr -> bool -> Expr.expr option
(** Alias for <c>eval</c>. *) (** Alias for <c>eval</c>. *)
val evaluate : model -> Expr.expr -> bool -> Expr.expr val evaluate : model -> Expr.expr -> bool -> Expr.expr option
(** The number of uninterpreted sorts that the model has an interpretation for. *) (** The number of uninterpreted sorts that the model has an interpretation for. *)
val get_num_sorts : model -> int val get_num_sorts : model -> int
@ -2438,7 +2416,7 @@ sig
type probe type probe
(** Execute the probe over the goal. (** Execute the probe over the goal.
<returns>A probe always produce a double value. <returns>A probe always produce a float value.
"Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns> *) "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns> *)
val apply : probe -> Goal.goal -> float val apply : probe -> Goal.goal -> float
@ -2637,7 +2615,7 @@ sig
(** True if the entry is uint-valued. *) (** True if the entry is uint-valued. *)
val is_int : statistics_entry -> bool val is_int : statistics_entry -> bool
(** True if the entry is double-valued. *) (** True if the entry is float-valued. *)
val is_float : statistics_entry -> bool val is_float : statistics_entry -> bool
(** The string representation of the the entry's value. *) (** The string representation of the the entry's value. *)
@ -2954,10 +2932,11 @@ val get_global_param : string -> string option
{!set_global_param} {!set_global_param}
*) *)
val global_param_reset_all : unit val global_param_reset_all : unit -> unit
(** Enable/disable printing of warning messages to the console. (** Enable/disable printing of warning messages to the console.
Note that this function is static and effects the behaviour of Note that this function is static and effects the behaviour of
all contexts globally. *) all contexts globally. *)
val toggle_warning_messages : bool -> unit val toggle_warning_messages : bool -> unit