mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +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 2014-04-16 12:55:23 +01:00
parent f319a77a4c
commit 3d9ad51aae
2 changed files with 119 additions and 133 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1,5 +1,5 @@
(**
The Z3 ML/Ocaml Interface.
The Z3 ML/OCaml Interface.
Copyright (C) 2012 Microsoft Corporation
@author CM Wintersteiger (cwinter) 2012-12-17
@ -698,7 +698,6 @@ sig
val get_simplify_help : context -> string
val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs
val get_func_decl : expr -> FuncDecl.func_decl
val get_bool_value : expr -> Z3enums.lbool
val get_num_args : expr -> int
val get_args : expr -> expr list
val update : expr -> expr list -> expr
@ -710,20 +709,7 @@ sig
val is_numeral : expr -> bool
val is_well_sorted : expr -> bool
val get_sort : expr -> Sort.sort
val is_bool : expr -> bool
val is_const : expr -> bool
val is_true : expr -> bool
val is_false : expr -> bool
val is_eq : expr -> bool
val is_distinct : expr -> bool
val is_ite : expr -> bool
val is_and : expr -> bool
val is_or : expr -> bool
val is_iff : expr -> bool
val is_xor : expr -> bool
val is_not : expr -> bool
val is_implies : expr -> bool
val is_oeq : expr -> bool
val mk_const : context -> Symbol.symbol -> Sort.sort -> expr
val mk_const_s : context -> string -> Sort.sort -> expr
val mk_const_f : context -> FuncDecl.func_decl -> expr
@ -782,9 +768,7 @@ end = struct
let get_simplify_parameter_descrs ( ctx : context ) =
Params.ParamDescrs.param_descrs_of_ptr ctx (Z3native.simplify_get_param_descrs (context_gno ctx))
let get_func_decl ( x : expr ) = FuncDecl.func_decl_of_ptr (Expr.gc x) (Z3native.get_app_decl (gnc x) (gno x))
let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (gnc x) (gno x))
let get_func_decl ( x : expr ) = FuncDecl.func_decl_of_ptr (Expr.gc x) (Z3native.get_app_decl (gnc x) (gno x))
let get_num_args ( x : expr ) = Z3native.get_app_num_args (gnc x) (gno x)
@ -823,29 +807,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_bool ( x : expr ) = (match x with Expr(a) -> (AST.is_expr a)) &&
(Z3native.is_eq_sort (gnc x)
(Z3native.mk_bool_sort (gnc x))
(Z3native.get_sort (gnc x) (gno x)))
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 is_true ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_TRUE)
let is_false ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_FALSE)
let is_eq ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_EQ)
let is_distinct ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_DISTINCT)
let is_ite ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_ITE)
let is_and ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_AND)
let is_or ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_OR)
let is_iff ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_IFF)
let is_xor ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR)
let is_not ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_NOT)
let is_implies ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES)
let is_oeq ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_OEQ)
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))
@ -888,12 +854,6 @@ struct
let mk_val ( ctx : context ) ( value : bool ) =
if value then mk_true ctx else mk_false ctx
let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) =
expr_of_ptr ctx (Z3native.mk_eq (context_gno ctx) (Expr.gno x) (Expr.gno y))
let mk_distinct ( ctx : context ) ( args : expr list ) =
expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args))
let mk_not ( ctx : context ) ( a : expr ) =
expr_of_ptr ctx (Z3native.mk_not (context_gno ctx) (gno a))
@ -917,6 +877,31 @@ struct
let mk_or ( ctx : context ) ( args : expr list ) =
let f x = (Expr.gno (x)) in
expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args)))
let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) =
expr_of_ptr ctx (Z3native.mk_eq (context_gno ctx) (Expr.gno x) (Expr.gno y))
let mk_distinct ( ctx : context ) ( args : expr list ) =
expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args))
let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (gnc x) (gno x))
let is_bool ( x : expr ) = (match x with Expr(a) -> (AST.is_expr a)) &&
(Z3native.is_eq_sort (gnc x)
(Z3native.mk_bool_sort (gnc x))
(Z3native.get_sort (gnc x) (gno x)))
let is_true ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_TRUE)
let is_false ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_FALSE)
let is_eq ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_EQ)
let is_distinct ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_DISTINCT)
let is_ite ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_ITE)
let is_and ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_AND)
let is_or ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_OR)
let is_iff ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_IFF)
let is_xor ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR)
let is_not ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_NOT)
let is_implies ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES)
end
@ -1784,6 +1769,7 @@ struct
let is_true ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE)
let is_asserted ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ASSERTED)
let is_goal ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_GOAL)
let is_oeq ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_OEQ)
let is_modus_ponens ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS)
let is_reflexivity ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REFLEXIVITY)
let is_symmetry ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SYMMETRY)

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

@ -1,5 +1,5 @@
(**
The Z3 ML/Ocaml Interface.
The Z3 ML/OCaml Interface.
Copyright (C) 2012 Microsoft Corporation
@author CM Wintersteiger (cwinter) 2012-12-17
@ -488,10 +488,6 @@ sig
(** The function declaration of the function that is applied in this expression. *)
val get_func_decl : Expr.expr -> FuncDecl.func_decl
(** Indicates whether the expression is the true or false expression
or something else (L_UNDEF). *)
val get_bool_value : Expr.expr -> Z3enums.lbool
(** The number of arguments of the expression. *)
val get_num_args : Expr.expr -> int
@ -535,11 +531,88 @@ sig
(** The Sort of the term. *)
val get_sort : Expr.expr -> Sort.sort
(** Indicates whether the term has Boolean sort. *)
val is_bool : Expr.expr -> bool
(** 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 *)
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 <c>MakeNumeral</c> since it is not necessary to parse a string.
@return A Term with the given value and sort *)
val mk_numeral_int : context -> int -> Sort.sort -> expr
end
(** Boolean expressions; Propositional logic and equality *)
module Boolean :
sig
(** Create a Boolean sort *)
val mk_sort : context -> Sort.sort
(** Create a Boolean constant. *)
val mk_const : context -> Symbol.symbol -> Expr.expr
(** Create a Boolean constant. *)
val mk_const_s : context -> string -> Expr.expr
(** The true Term. *)
val mk_true : context -> Expr.expr
(** The false Term. *)
val mk_false : context -> Expr.expr
(** Creates a Boolean value. *)
val mk_val : context -> bool -> Expr.expr
(** Mk an expression representing <c>not(a)</c>. *)
val mk_not : context -> Expr.expr -> Expr.expr
(** Create an expression representing an if-then-else: <c>ite(t1, t2, t3)</c>. *)
val mk_ite : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing <c>t1 iff t2</c>. *)
val mk_iff : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing <c>t1 -> t2</c>. *)
val mk_implies : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing <c>t1 xor t2</c>. *)
val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing the AND of args *)
val mk_and : context -> Expr.expr list -> Expr.expr
(** Create an expression representing the OR of args *)
val mk_or : context -> Expr.expr list -> Expr.expr
(** Creates the equality between two expr's. *)
val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Creates a <c>distinct</c> term. *)
val mk_distinct : context -> Expr.expr list -> Expr.expr
(** Indicates whether the expression is the true or false expression
or something else (L_UNDEF). *)
val get_bool_value : Expr.expr -> Z3enums.lbool
(** Indicates whether the term has Boolean sort. *)
val is_bool : Expr.expr -> bool
(** Indicates whether the term is the constant true. *)
val is_true : Expr.expr -> bool
@ -573,84 +646,6 @@ sig
(** Indicates whether the term is an implication *)
val is_implies : 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. *)
val is_oeq : 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 goven 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 <c>MakeNumeral</c> since it is not necessary to parse a string.
@return A Term with the given value and sort *)
val mk_numeral_int : context -> int -> Sort.sort -> expr
end
(** Boolean expressions *)
module Boolean :
sig
(** Create a Boolean sort *)
val mk_sort : context -> Sort.sort
(** Create a Boolean constant. *)
val mk_const : context -> Symbol.symbol -> Expr.expr
(** Create a Boolean constant. *)
val mk_const_s : context -> string -> Expr.expr
(** The true Term. *)
val mk_true : context -> Expr.expr
(** The false Term. *)
val mk_false : context -> Expr.expr
(** Creates a Boolean value. *)
val mk_val : context -> bool -> Expr.expr
(** Creates the equality between two expr's. *)
val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Creates a <c>distinct</c> term. *)
val mk_distinct : context -> Expr.expr list -> Expr.expr
(** Mk an expression representing <c>not(a)</c>. *)
val mk_not : context -> Expr.expr -> Expr.expr
(** Create an expression representing an if-then-else: <c>ite(t1, t2, t3)</c>. *)
val mk_ite : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing <c>t1 iff t2</c>. *)
val mk_iff : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing <c>t1 -> t2</c>. *)
val mk_implies : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing <c>t1 xor t2</c>. *)
val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Create an expression representing the AND of args *)
val mk_and : context -> Expr.expr list -> Expr.expr
(** Create an expression representing the OR of args *)
val mk_or : context -> Expr.expr list -> Expr.expr
end
(** Quantifier expressions *)
@ -817,7 +812,7 @@ sig
The node <c>a</c> must have an array sort <c>[domain -> range]</c>,
and <c>i</c> must have the sort <c>domain</c>.
The sort of the result is <c>range</c>.
{!Array.mk_sort}
{!Z3Array.mk_sort}
{!mk_store} *)
val mk_select : context -> Expr.expr -> Expr.expr -> Expr.expr
@ -833,7 +828,7 @@ sig
on all indices except for <c>i</c>, where it maps to <c>v</c>
(and the <c>select</c> of <c>a</c> with
respect to <c>i</c> may be a different value).
{!Array.mk_sort}
{!Z3Array.mk_sort}
{!mk_select} *)
val mk_store : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
@ -841,7 +836,7 @@ sig
The resulting term is an array, such that a <c>select</c>on an arbitrary index
produces the value <c>v</c>.
{!Array.mk_sort}
{!Z3Array.mk_sort}
{!mk_select} *)
val mk_const_array : context -> Sort.sort -> Expr.expr -> Expr.expr
@ -850,7 +845,7 @@ sig
Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
<c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
{!Array.mk_sort}
{!Z3Array.mk_sort}
{!mk_select}
{!mk_store} *)
val mk_map : context -> FuncDecl.func_decl -> Expr.expr list -> Expr.expr
@ -1837,6 +1832,11 @@ sig
(** Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. *)
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. *)
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.