diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index c037a9263..051a54696 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -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) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 5c9c56dbf..c554d7564 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -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 MakeNumeral 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 not(a). *) + val mk_not : context -> Expr.expr -> Expr.expr + + (** Create an expression representing an if-then-else: ite(t1, t2, t3). *) + val mk_ite : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (** Create an expression representing t1 iff t2. *) + val mk_iff : context -> Expr.expr -> Expr.expr -> Expr.expr + + (** Create an expression representing t1 -> t2. *) + val mk_implies : context -> Expr.expr -> Expr.expr -> Expr.expr + + (** Create an expression representing t1 xor t2. *) + 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 distinct 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 MakeNumeral 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 distinct term. *) - val mk_distinct : context -> Expr.expr list -> Expr.expr - - (** Mk an expression representing not(a). *) - val mk_not : context -> Expr.expr -> Expr.expr - - (** Create an expression representing an if-then-else: ite(t1, t2, t3). *) - val mk_ite : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr - - (** Create an expression representing t1 iff t2. *) - val mk_iff : context -> Expr.expr -> Expr.expr -> Expr.expr - - (** Create an expression representing t1 -> t2. *) - val mk_implies : context -> Expr.expr -> Expr.expr -> Expr.expr - - (** Create an expression representing t1 xor t2. *) - 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 a must have an array sort [domain -> range], and i must have the sort domain. The sort of the result is range. - {!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 i, where it maps to v (and the select of a with respect to i 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 selecton an arbitrary index produces the value v. - {!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 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]. - {!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.