diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 344e542f7..b1e40fcac 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -338,7 +338,7 @@ struct else ast_of_ptr to_ctx (Z3native.translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) - let wrap ( ctx : context ) ( ptr : Z3native.ptr ) = ast_of_ptr ctx ptr + let wrap_ast ( ctx : context ) ( ptr : Z3native.ptr ) = ast_of_ptr ctx ptr let unwrap_ast ( x : ast ) = (z3obj_gno x) end @@ -744,6 +744,7 @@ sig val is_not : expr -> bool val is_implies : expr -> bool val is_label : expr -> bool + val is_label_lit : 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 @@ -794,257 +795,97 @@ end = struct let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (Array.length args) (expr_aton args) in expr_of_ptr ctx o - (** - Returns a simplified version of the expression. - @param p A set of parameters to configure the simplifier - - *) let simplify ( x : expr ) ( p : Params.params option ) = match p with | None -> expr_of_ptr (c_of_expr x) (Z3native.simplify (nc_of_expr x) (ptr_of_expr x)) | Some pp -> expr_of_ptr (c_of_expr x) (Z3native.simplify_ex (nc_of_expr x) (ptr_of_expr x) (z3obj_gno pp)) - (** - a string describing all available parameters to Expr.Simplify. - *) let get_simplify_help ( ctx : context ) = Z3native.simplify_get_help (context_gno ctx) - (** - Retrieves parameter descriptions for simplifier. - *) let get_simplify_parameter_descrs ( ctx : context ) = Params.ParamDescrs.param_descrs_of_ptr ctx (Z3native.simplify_get_param_descrs (context_gno ctx)) - - (** - The function declaration of the function that is applied in this expression. - *) let get_func_decl ( x : expr ) = FuncDecl.func_decl_of_ptr (c_of_expr x) (Z3native.get_app_decl (nc_of_expr x) (ptr_of_expr x)) - (** - Indicates whether the expression is the true or false expression - or something else (L_UNDEF). - *) let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (nc_of_expr x) (ptr_of_expr x)) - (** - The number of arguments of the expression. - *) let get_num_args ( x : expr ) = Z3native.get_app_num_args (nc_of_expr x) (ptr_of_expr x) - (** - The arguments of the expression. - *) let get_args ( x : expr ) = let n = (get_num_args x) in let f i = expr_of_ptr (c_of_expr x) (Z3native.get_app_arg (nc_of_expr x) (ptr_of_expr x) i) in Array.init n f - (** - Update the arguments of the expression using the arguments - The number of new arguments should coincide with the current number of arguments. - *) let update ( x : expr ) args = if (Array.length args <> (get_num_args x)) then raise (Z3native.Exception "Number of arguments does not match") else expr_of_ptr (c_of_expr x) (Z3native.update_term (nc_of_expr x) (ptr_of_expr x) (Array.length args) (expr_aton args)) - (** - 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]. - *) let substitute ( x : expr ) from to_ = if (Array.length from) <> (Array.length to_) then raise (Z3native.Exception "Argument sizes do not match") else expr_of_ptr (c_of_expr x) (Z3native.substitute (nc_of_expr x) (ptr_of_expr x) (Array.length from) (expr_aton from) (expr_aton to_)) - (** - Substitute every occurrence of from in the expression with to. - - *) let substitute_one ( x : expr ) from to_ = substitute ( x : expr ) [| from |] [| to_ |] - (** - Substitute the free variables in the expression with the expressions in - - For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term to[i]. - *) let substitute_vars ( x : expr ) to_ = expr_of_ptr (c_of_expr x) (Z3native.substitute_vars (nc_of_expr x) (ptr_of_expr x) (Array.length to_) (expr_aton to_)) - (** - Translates (copies) the term to the Context . - @param ctx A context - @return A copy of the term which is associated with - *) let translate ( x : expr ) to_ctx = if (c_of_expr x) == to_ctx then x else expr_of_ptr to_ctx (Z3native.translate (nc_of_expr x) (ptr_of_expr x) (context_gno to_ctx)) - (** - Returns a string representation of the expression. - *) let to_string ( x : expr ) = Z3native.ast_to_string (nc_of_expr x) (ptr_of_expr x) - (** - Indicates whether the term is a numeral - *) let is_numeral ( x : expr ) = (Z3native.is_numeral_ast (nc_of_expr x) (ptr_of_expr x)) - (** - Indicates whether the term is well-sorted. - @return True if the term is well-sorted, false otherwise. - *) let is_well_sorted ( x : expr ) = Z3native.is_well_sorted (nc_of_expr x) (ptr_of_expr x) - (** - The Sort of the term. - *) let get_sort ( x : expr ) = sort_of_ptr (c_of_expr x) (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x)) - (** - Indicates whether the term has Boolean sort. - *) let is_bool ( x : expr ) = (match x with Expr(a) -> (AST.is_expr a)) && (Z3native.is_eq_sort (nc_of_expr x) (Z3native.mk_bool_sort (nc_of_expr x)) (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x))) - (** - Indicates whether the term represents a constant. - *) let is_const ( x : expr ) = (match x with Expr(a) -> (AST.is_expr a)) && (get_num_args x) == 0 && (FuncDecl.get_domain_size (get_func_decl x)) == 0 - - (** - Indicates whether the term is the constant true. - *) + let is_true ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_TRUE) - - (** - Indicates whether the term is the constant false. - *) let is_false ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_FALSE) - - (** - Indicates whether the term is an equality predicate. - *) let is_eq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_EQ) - - (** - Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). - *) let is_distinct ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_DISTINCT) - - (** - Indicates whether the term is a ternary if-then-else term - *) let is_ite ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_ITE) - - (** - Indicates whether the term is an n-ary conjunction - *) let is_and ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_AND) - - (** - Indicates whether the term is an n-ary disjunction - *) let is_or ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_OR) - - (** - Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) - *) let is_iff ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IFF) - - (** - Indicates whether the term is an exclusive or - *) let is_xor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR) - - (** - Indicates whether the term is a negation - *) let is_not ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_NOT) - - (** - Indicates whether the term is an implication - *) let is_implies ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES) - - (** - 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. - *) let is_label ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL) - - (** - 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) - *) - - (** - 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. - *) + 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) - (** - Creates a new Constant of sort and named . - *) 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)) - - (** - Creates a new Constant of sort and named . - *) let mk_const_s ( ctx : context ) ( name : string ) ( range : sort ) = mk_const ctx (Symbol.mk_string ctx name) range - - (** - Creates a constant from the func_decl . - @param f An expression of a 0-arity function - *) let mk_const_f ( ctx : context ) ( f : FuncDecl.func_decl ) = Expr.expr_of_func_app ctx f [||] - (** - Creates a fresh constant of sort and a - name prefixed with . - *) let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : sort ) = expr_of_ptr ctx (Z3native.mk_fresh_const (context_gno ctx) prefix (Sort.gno range)) - (** - Create a new function application. - *) let mk_app ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : expr array ) = expr_of_func_app ctx f args - (** - Create a numeral of a given sort. - @param v A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*. - @param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. - @return A Term with value and sort - *) let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : sort ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno ty)) - (** - 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. - @param v Value of the numeral - @param ty Sort of the numeral - @return A Term with value and type - *) let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : sort ) = expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty)) end @@ -1052,7 +893,6 @@ end open FuncDecl open Expr -(** Boolean expressions *) module Boolean = struct type bool_sort = BoolSort of Sort.sort @@ -1091,97 +931,53 @@ struct let mk_sort ( ctx : context ) = BoolSort(sort_of_ptr ctx (Z3native.mk_bool_sort (context_gno ctx))) - (** - Create a Boolean constant. - *) let mk_const ( ctx : context ) ( name : Symbol.symbol ) = let s = (match (mk_sort ctx) with BoolSort(q) -> q) in BoolExpr(Expr.mk_const ctx name s) - (** - Create a Boolean constant. - *) let mk_const_s ( ctx : context ) ( name : string ) = mk_const ctx (Symbol.mk_string ctx name) - (** - The true Term. - *) let mk_true ( ctx : context ) = bool_expr_of_ptr ctx (Z3native.mk_true (context_gno ctx)) - (** - The false Term. - *) let mk_false ( ctx : context ) = bool_expr_of_ptr ctx (Z3native.mk_false (context_gno ctx)) - (** - Creates a Boolean value. - *) let mk_val ( ctx : context ) ( value : bool ) = if value then mk_true ctx else mk_false ctx - (** - Creates the equality = . - *) let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) = bool_expr_of_ptr ctx (Z3native.mk_eq (context_gno ctx) (ptr_of_expr x) (ptr_of_expr y)) - (** - Creates a distinct term. - *) let mk_distinct ( ctx : context ) ( args : expr array ) = bool_expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (Array.length args) (expr_aton args)) - (** - Mk an expression representing not(a). - *) let mk_not ( ctx : context ) ( a : bool_expr ) = bool_expr_of_ptr ctx (Z3native.mk_not (context_gno ctx) (gno a)) - (** - Create an expression representing an if-then-else: ite(t1, t2, t3). - @param t1 An expression with Boolean sort - @param t2 An expression - @param t3 An expression with the same sort as - *) let mk_ite ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) ( t3 : bool_expr ) = bool_expr_of_ptr ctx (Z3native.mk_ite (context_gno ctx) (gno t1) (gno t2) (gno t3)) - (** - Create an expression representing t1 iff t2. - *) let mk_iff ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = bool_expr_of_ptr ctx (Z3native.mk_iff (context_gno ctx) (gno t1) (gno t2)) - (** - Create an expression representing t1 -> t2. - *) let mk_implies ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = bool_expr_of_ptr ctx (Z3native.mk_implies (context_gno ctx) (gno t1) (gno t2)) - (** - Create an expression representing t1 xor t2. - *) + let mk_xor ( ctx : context ) ( t1 : bool_expr ) ( t2 : bool_expr ) = bool_expr_of_ptr ctx (Z3native.mk_xor (context_gno ctx) (gno t1) (gno t2)) - (** - Create an expression representing the AND of args - *) let mk_and ( ctx : context ) ( args : bool_expr array ) = let f x = (ptr_of_expr (expr_of_bool_expr x)) in bool_expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (Array.length args) (Array.map f args)) - (** - Create an expression representing the OR of args - *) let mk_or ( ctx : context ) ( args : bool_expr array ) = let f x = (ptr_of_expr (expr_of_bool_expr x)) in bool_expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (Array.length args) (Array.map f args)) end -(** Quantifier expressions *) + module Quantifier = struct type quantifier = Quantifier of expr @@ -1200,12 +996,6 @@ struct let gnc ( x : quantifier ) = match (x) with Quantifier(e) -> (nc_of_expr e) let gno ( x : quantifier ) = match (x) with Quantifier(e) -> (ptr_of_expr e) - (** Quantifier patterns - - Patterns comprise a list of terms. The list should be - non-empty. If the list comprises of more than one term, it is - also called a multi-pattern. - *) module Pattern = struct type pattern = Pattern of ast @@ -1220,155 +1010,68 @@ struct let gnc ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gnc a) let gno ( x : pattern ) = match (x) with Pattern(a) -> (z3obj_gno a) - (** - The number of terms in the pattern. - *) let get_num_terms ( x : pattern ) = Z3native.get_pattern_num_terms (gnc x) (gno x) - (** - The terms in the pattern. - *) let get_terms ( x : pattern ) = let n = (get_num_terms x) in let f i = (expr_of_ptr (gc x) (Z3native.get_pattern (gnc x) (gno x) i)) in Array.init n f - (** - A string representation of the pattern. - *) let to_string ( x : pattern ) = Z3native.pattern_to_string (gnc x) (gno x) end - (** - 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. - *) let get_index ( x : expr ) = if not (AST.is_var (match x with Expr.Expr(a) -> a)) then raise (Z3native.Exception "Term is not a bound variable.") else Z3native.get_index_value (nc_of_expr x) (ptr_of_expr x) - (** - Indicates whether the quantifier is universal. - *) let is_universal ( x : quantifier ) = Z3native.is_quantifier_forall (gnc x) (gno x) - (** - Indicates whether the quantifier is existential. - *) let is_existential ( x : quantifier ) = not (is_universal x) - (** - The weight of the quantifier. - *) let get_weight ( x : quantifier ) = Z3native.get_quantifier_weight (gnc x) (gno x) - (** - The number of patterns. - *) let get_num_patterns ( x : quantifier ) = Z3native.get_quantifier_num_patterns (gnc x) (gno x) - (** - The patterns. - *) let get_patterns ( x : quantifier ) = let n = (get_num_patterns x) in let f i = Pattern.Pattern (z3_native_object_of_ast_ptr (gc x) (Z3native.get_quantifier_pattern_ast (gnc x) (gno x) i)) in Array.init n f - (** - The number of no-patterns. - *) let get_num_no_patterns ( x : quantifier ) = Z3native.get_quantifier_num_no_patterns (gnc x) (gno x) - (** - The no-patterns. - *) let get_no_patterns ( x : quantifier ) = let n = (get_num_patterns x) in let f i = Pattern.Pattern (z3_native_object_of_ast_ptr (gc x) (Z3native.get_quantifier_no_pattern_ast (gnc x) (gno x) i)) in Array.init n f - (** - The number of bound variables. - *) let get_num_bound ( x : quantifier ) = Z3native.get_quantifier_num_bound (gnc x) (gno x) - (** - The symbols for the bound variables. - *) let get_bound_variable_names ( x : quantifier ) = let n = (get_num_bound x) in let f i = (Symbol.create (gc x) (Z3native.get_quantifier_bound_name (gnc x) (gno x) i)) in Array.init n f - (** - The sorts of the bound variables. - *) let get_bound_variable_sorts ( x : quantifier ) = let n = (get_num_bound x) in let f i = (sort_of_ptr (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) i)) in Array.init n f - (** - The body of the quantifier. - *) let get_body ( x : quantifier ) = Boolean.bool_expr_of_ptr (gc x) (Z3native.get_quantifier_body (gnc x) (gno x)) - (** - Creates a new bound variable. - @param index The de-Bruijn index of the variable - @param ty The sort of the variable - *) let mk_bound ( ctx : context ) ( index : int ) ( ty : sort ) = expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) - (** - Create a quantifier pattern. - *) let mk_pattern ( ctx : context ) ( terms : expr array ) = if (Array.length terms) == 0 then raise (Z3native.Exception "Cannot create a pattern from zero terms") else Pattern.Pattern(z3_native_object_of_ast_ptr ctx (Z3native.mk_pattern (context_gno ctx) (Array.length terms) (expr_aton terms))) - (** - Create a universal Quantifier. - - Creates a forall formula, where is the weight, - is an array of patterns, is an array - with the sorts of the bound variables, is an array with the - 'names' of the bound variables, and is the body of the - quantifier. Quantifiers are associated with weights indicating - the importance of using the quantifier during instantiation. - - @param sorts the sorts of the bound variables. - @param names names of the bound variables - @param body the body of the quantifier. - @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. - @param patterns array containing the patterns created using MkPattern. - @param noPatterns array containing the anti-patterns created using MkPattern. - @param quantifierID optional symbol to track quantifier. - @param skolemID optional symbol to track skolem constants. - *) let mk_forall ( ctx : context ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (Array.length sorts) != (Array.length names) then raise (Z3native.Exception "Number of sorts does not match number of names") @@ -1390,9 +1093,6 @@ struct (let f x = (Symbol.gno x) in (Array.map f names)) (ptr_of_expr body))) - (** - Create a universal Quantifier. - *) let mk_forall_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const (context_gno ctx) true @@ -1410,10 +1110,6 @@ struct (Array.length nopatterns) (expr_aton nopatterns) (ptr_of_expr body))) - (** - Create an existential Quantifier. - - *) let mk_exists ( ctx : context ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (Array.length sorts) != (Array.length names) then raise (Z3native.Exception "Number of sorts does not match number of names") @@ -1435,9 +1131,6 @@ struct (let f x = (Symbol.gno x) in (Array.map f names)) (ptr_of_expr body))) - (** - Create an existential Quantifier. - *) let mk_exists_const ( ctx : context ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if ((Array.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier_const (context_gno ctx) false @@ -1455,19 +1148,12 @@ struct (Array.length nopatterns) (expr_aton nopatterns) (ptr_of_expr body))) - (** - Create a Quantifier. - *) let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : sort array ) ( names : Symbol.symbol array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (universal) then (mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id) else (mk_exists ctx sorts names body weight patterns nopatterns quantifier_id skolem_id) - - (** - Create a Quantifier. - *) let mk_quantifier ( ctx : context ) ( universal : bool ) ( bound_constants : expr array ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern array ) ( nopatterns : expr array ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) = if (universal) then mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id @@ -1475,7 +1161,7 @@ struct mk_exists_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id end -(** Functions to manipulate Array expressions *) + module Array_ = struct type array_sort = ArraySort of sort @@ -1516,144 +1202,46 @@ struct let egnc ( x : array_expr ) = match (x) with ArrayExpr(Expr(e)) -> (z3obj_gnc e) let egno ( x : array_expr ) = match (x) with ArrayExpr(Expr(e)) -> (z3obj_gno e) - (** - Create a new array sort. - *) let mk_sort ( ctx : context ) ( domain : sort ) ( range : sort ) = array_sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range)) - (** - 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. - *) let is_store ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) - - (** - Indicates whether the term is an array select. - *) let is_select ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SELECT) - - (** - 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. - *) let is_constant_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONST_ARRAY) - - (** - Indicates whether the term is a default array. - For example default(const(v)) = v. The function is unary. - *) let is_default_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_DEFAULT) - - (** - 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. - *) let is_array_map ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_MAP) - - (** - 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. - *) let is_as_array ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) - - (** - Indicates whether the term is of an array sort. - *) let is_array ( x : expr ) = (Z3native.is_app (nc_of_expr x) (ptr_of_expr x)) && ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x)))) == ARRAY_SORT) - (** The domain of the array sort. *) let get_domain ( x : array_sort ) = Sort.sort_of_ptr (sgc x) (Z3native.get_array_sort_domain (sgnc x) (sgno x)) - - (** The range of the array sort. *) let get_range ( x : array_sort ) = Sort.sort_of_ptr (sgc x) (Z3native.get_array_sort_range (sgnc x) (sgno x)) - (** - Create an array constant. - *) let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort ) ( range : sort ) = ArrayExpr(Expr.mk_const ctx name (match (mk_sort ctx domain range) with ArraySort(s) -> s)) - (** - Create an array constant. - *) let mk_const_s ( ctx : context ) ( name : string ) ( domain : sort ) ( range : sort ) = mk_const ctx (Symbol.mk_string ctx name) domain range - (** - 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. - - - *) let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) = - array_expr_of_ptr ctx (Z3native.mk_select (context_gno ctx) (egno a) (ptr_of_expr i)) - - (** - 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). - - - *) - let mk_select ( ctx : context ) ( a : array_expr ) ( i : expr ) ( v : expr ) = + array_expr_of_ptr ctx (Z3native.mk_select (context_gno ctx) (egno a) (ptr_of_expr i)) + + let mk_store ( ctx : context ) ( a : array_expr ) ( i : expr ) ( v : expr ) = array_expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (egno a) (ptr_of_expr i) (ptr_of_expr v)) - (** - Create a constant array. - - The resulting term is an array, such that a selecton an arbitrary index - produces the value v. - - - *) let mk_const_array ( ctx : context ) ( domain : sort ) ( v : expr ) = array_expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (ptr_of_expr v)) - (** - 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]. - - - - *) let mk_map ( ctx : context ) ( f : func_decl ) ( args : array_expr array ) = let m x = (ptr_of_expr (expr_of_array_expr x)) in array_expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (Array.length args) (Array.map m args)) - (** - Access the array default value. - - Produces the default range value, for arrays that can be represented as - finite maps with a default range value. - *) let mk_term_array ( ctx : context ) ( arg : array_expr ) = array_expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (egno arg)) end -(** Functions to manipulate Set expressions *) + module Set = struct type set_sort = SetSort of sort @@ -1664,100 +1252,49 @@ struct let sort_of_set_sort s = match s with SetSort(x) -> x - (** - Indicates whether the term is set union - *) - let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) - - (** - Indicates whether the term is set intersection - *) - let is_intersect ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) - - (** - Indicates whether the term is set difference - *) - let is_difference ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) - - (** - Indicates whether the term is set complement - *) - let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) - - (** - Indicates whether the term is set subset - *) - let is_subset ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) - - (** - Create a set type. - *) let mk_sort ( ctx : context ) ( ty : sort ) = set_sort_of_ptr ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty)) - (** - Create an empty set. - *) + let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) + let is_intersect ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) + let is_difference ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) + let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) + let is_subset ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) + + let mk_empty ( ctx : context ) ( domain : sort ) = (expr_of_ptr ctx (Z3native.mk_empty_set (context_gno ctx) (Sort.gno domain))) - (** - Create the full set. - *) let mk_full ( ctx : context ) ( domain : sort ) = expr_of_ptr ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain)) - (** - Add an element to the set. - *) let mk_set_add ( ctx : context ) ( set : expr ) ( element : expr ) = expr_of_ptr ctx (Z3native.mk_set_add (context_gno ctx) (ptr_of_expr set) (ptr_of_expr element)) - (** - Remove an element from a set. - *) let mk_del ( ctx : context ) ( set : expr ) ( element : expr ) = expr_of_ptr ctx (Z3native.mk_set_del (context_gno ctx) (ptr_of_expr set) (ptr_of_expr element)) - (** - Take the union of a list of sets. - *) let mk_union ( ctx : context ) ( args : expr array ) = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (Array.length args) (expr_aton args)) - (** - Take the intersection of a list of sets. - *) let mk_intersection ( ctx : context ) ( args : expr array ) = expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (Array.length args) (expr_aton args)) - (** - Take the difference between two sets. - *) let mk_difference ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = expr_of_ptr ctx (Z3native.mk_set_difference (context_gno ctx) (ptr_of_expr arg1) (ptr_of_expr arg2)) - (** - Take the complement of a set. - *) let mk_complement ( ctx : context ) ( arg : expr ) = expr_of_ptr ctx (Z3native.mk_set_complement (context_gno ctx) (ptr_of_expr arg)) - (** - Check for set membership. - *) let mk_membership ( ctx : context ) ( elem : expr ) ( set : expr ) = expr_of_ptr ctx (Z3native.mk_set_member (context_gno ctx) (ptr_of_expr elem) (ptr_of_expr set)) - (** - Check for subsetness of sets. - *) let mk_subset ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = expr_of_ptr ctx (Z3native.mk_set_subset (context_gno ctx) (ptr_of_expr arg1) (ptr_of_expr arg2)) end -(** Functions to manipulate Finite Domain expressions *) + module FiniteDomain = struct type finite_domain_sort = FiniteDomainSort of sort @@ -1774,41 +1311,28 @@ struct let gnc ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort(s)) -> (z3obj_gnc s) let gno ( x : finite_domain_sort ) = match (x) with FiniteDomainSort(Sort(s))-> (z3obj_gno s) - (** - Create a new finite domain sort. - *) let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) = let s = (sort_of_ptr ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size)) in FiniteDomainSort(s) - (** - Create a new finite domain sort. - *) let mk_sort_s ( ctx : context ) ( name : string ) ( size : int ) = mk_sort ctx (Symbol.mk_string ctx name) size - (** - Indicates whether the term is of an array sort. - *) let is_finite_domain ( x : expr ) = let nc = (nc_of_expr x) in (Z3native.is_app (nc_of_expr x) (ptr_of_expr x)) && (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc (ptr_of_expr x))) == FINITE_DOMAIN_SORT) - (** - Indicates whether the term is a less than predicate over a finite domain. - *) let is_lt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT) - (** The size of the finite domain sort. *) let get_size ( x : finite_domain_sort ) = let (r, v) = (Z3native.get_finite_domain_sort_size (gnc x) (gno x)) in if r then v else raise (Z3native.Exception "Conversion failed.") end -(** Functions to manipulate Relation expressions *) + module Relation = struct type relation_sort = RelationSort of sort @@ -1830,119 +1354,27 @@ struct let gno ( x : relation_sort ) = match (x) with RelationSort(Sort(s))-> (z3obj_gno s) - (** - Indicates whether the term is of a relation sort. - *) let is_relation ( x : expr ) = let nc = (nc_of_expr x) in ((Z3native.is_app (nc_of_expr x) (ptr_of_expr x)) && (sort_kind_of_int (Z3native.get_sort_kind nc (Z3native.get_sort nc (ptr_of_expr x))) == RELATION_SORT)) - (** - 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. - *) let is_store ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_STORE) - - (** - Indicates whether the term is an empty relation - *) let is_empty ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_EMPTY) - - (** - Indicates whether the term is a test for the emptiness of a relation - *) let is_is_empty ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_IS_EMPTY) - - (** - Indicates whether the term is a relational join - *) let is_join ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_JOIN) - - (** - Indicates whether the term is the union or convex hull of two relations. - The function takes two arguments. - *) let is_union ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_UNION) - - (** - Indicates whether the term is the widening of two relations - The function takes two arguments. - *) let is_widen ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_WIDEN) - - (** - Indicates whether the term is a projection of columns (provided as numbers in the parameters). - The function takes one argument. - *) let is_project ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_PROJECT) - - (** - 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. - *) let is_filter ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_FILTER) - - (** - 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. - *) let is_negation_filter ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_NEGATION_FILTER) - - (** - 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. - *) let is_rename ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_RENAME) - - (** - Indicates whether the term is the complement of a relation - *) let is_complement ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_COMPLEMENT) - - (** - 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. - *) let is_select ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT) - - (** - 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 - to perform destructive updates to the first argument. - *) let is_clone ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_CLONE) - (** The arity of the relation sort. *) let get_arity ( x : relation_sort ) = Z3native.get_relation_arity (gnc x) (gno x) - (** The sorts of the columns of the relation sort. *) let get_column_sorts ( x : relation_sort ) = let n = get_arity x in let f i = (sort_of_ptr (gc x) (Z3native.get_relation_column (gnc x) (gno x) i)) in @@ -1950,7 +1382,7 @@ struct end -(** Functions to manipulate Datatype expressions *) + module Datatype = struct type datatype_sort = DatatypeSort of sort @@ -1983,14 +1415,10 @@ struct let sgnc ( x : datatype_sort ) = match (x) with DatatypeSort(Sort(s)) -> (z3obj_gnc s) let sgno ( x : datatype_sort ) = match (x) with DatatypeSort(Sort(s))-> (z3obj_gno s) - - (** Constructors *) module Constructor = struct type constructor = z3_native_object - let _counts = Hashtbl.create 0 - let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : sort array ) ( sort_refs : int array ) = let n = (Array.length field_names) in if n != (Array.length sorts) then @@ -2009,42 +1437,29 @@ struct m_n_obj = null ; inc_ref = z3obj_nil_ref ; dec_ref = z3obj_nil_ref} in - Hashtbl.add _counts no n ; (z3obj_sno no ctx ptr) ; (z3obj_create no) ; let f = fun o -> Z3native.del_constructor (z3obj_gnc o) (z3obj_gno o) in Gc.finalise f no ; no + + let get_num_fields ( x : constructor ) = Z3native.get_arity (z3obj_gnc x) (z3obj_gno x) - let get_n ( x : constructor ) = (Hashtbl.find _counts x) - - let rec constructor_decl ( x : constructor ) = - let (a, _, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (Hashtbl.find _counts x)) in + let get_constructor_decl ( x : constructor ) = + let (a, _, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in func_decl_of_ptr (z3obj_gc x) a - let rec tester_decl ( x : constructor ) = - let (_, b, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (Hashtbl.find _counts x)) in + let get_tester_decl ( x : constructor ) = + let (_, b, _) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in func_decl_of_ptr (z3obj_gc x) b - - let rec accessor_decls ( x : constructor ) = - let (_, _, c) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (Hashtbl.find _counts x)) in + + let get_accessor_decls ( x : constructor ) = + let (_, _, c) = (Z3native.query_constructor (z3obj_gnc x) (z3obj_gno x) (get_num_fields x)) in let f y = func_decl_of_ptr (z3obj_gc x) y in Array.map f c - (** The number of fields of the constructor. *) - let get_num_fields ( x : constructor ) = get_n x - - (** The function declaration of the constructor. *) - let get_constructor_decl ( x : constructor ) = constructor_decl x - - (** The function declaration of the tester. *) - let get_tester_decl ( x : constructor ) = tester_decl x - - (** The function declarations of the accessors *) - let get_accessor_decls ( x : constructor ) = accessor_decls x end - (** Constructor list objects *) module ConstructorList = struct type constructor_list = z3_native_object @@ -2062,54 +1477,21 @@ struct res end - (* DATATYPES *) - (** - Create a datatype constructor. - @param name constructor name - @param recognizer name of recognizer function. - @param fieldNames names of the constructor fields. - @param sorts field sorts, 0 if the field sort refers to a recursive sort. - @param sortRefs reference to datatype sort that is an argument to the 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. - *) let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : sort array ) ( sort_refs : int array ) = Constructor.create ctx name recognizer field_names sorts sort_refs - (** - Create a datatype constructor. - @param name constructor name - @param recognizer name of recognizer function. - @param fieldNames names of the constructor fields. - @param sorts field sorts, 0 if the field sort refers to a recursive sort. - @param sortRefs reference to datatype sort that is an argument to the 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. - *) let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( sorts : sort array ) ( sort_refs : int array ) = mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs - - (** - Create a new datatype sort. - *) let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : Constructor.constructor array ) = let f x = (z3obj_gno x) in let (x,_) = (Z3native.mk_datatype (context_gno ctx) (Symbol.gno name) (Array.length constructors) (Array.map f constructors)) in sort_of_ptr ctx x - (** - Create a new datatype sort. - *) let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : Constructor.constructor array ) = mk_sort ctx (Symbol.mk_string ctx name) constructors - (** - Create mutually recursive datatypes. - @param names names of datatype sorts - @param c list of constructors, one list per sort. - *) let mk_sorts ( ctx : context ) ( names : Symbol.symbol array ) ( c : Constructor.constructor array array ) = let n = (Array.length names) in let f e = (AST.ptr_of_ast (ConstructorList.create ctx e)) in @@ -2119,7 +1501,6 @@ struct let g e = (sort_of_ptr ctx e) in (Array.map g r) - (** Create mutually recursive data-types. *) let mk_sorts_s ( ctx : context ) ( names : string array ) ( c : Constructor.constructor array array ) = mk_sorts ctx ( @@ -2128,22 +1509,18 @@ struct ) c - (** The number of constructors of the datatype sort. *) let get_num_constructors ( x : datatype_sort ) = Z3native.get_datatype_sort_num_constructors (sgnc x) (sgno x) - (** The range of the array sort. *) let get_constructors ( x : datatype_sort ) = let n = (get_num_constructors x) in let f i = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) i) in Array.init n f - (** The recognizers. *) let get_recognizers ( x : datatype_sort ) = let n = (get_num_constructors x) in let f i = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) i) in Array.init n f - (** The constructor accessors. *) let get_accessors ( x : datatype_sort ) = let n = (get_num_constructors x) in let f i = ( @@ -2155,7 +1532,7 @@ struct Array.init n f end -(** Functions to manipulate Enumeration expressions *) + module Enumeration = struct type enum_sort = EnumSort of sort @@ -2171,27 +1548,19 @@ struct let sgnc ( x : enum_sort ) = match (x) with EnumSort(Sort(s)) -> (z3obj_gnc s) let sgno ( x : enum_sort ) = match (x) with EnumSort(Sort(s))-> (z3obj_gno s) - (** - Create a new enumeration sort. - *) let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( enum_names : Symbol.symbol array ) = let f x = Symbol.gno x in let (a, b, c) = (Z3native.mk_enumeration_sort (context_gno ctx) (Symbol.gno name) (Array.length enum_names) (Array.map f enum_names)) in sort_of_ptr ctx a b c - (** - Create a new enumeration sort. - *) let mk_sort_s ( ctx : context ) ( name : string ) ( enum_names : string array ) = mk_sort ctx (Symbol.mk_string ctx name) (Symbol.mk_strings ctx enum_names) - (** The function declarations of the constants in the enumeration. *) let get_const_decls ( x : enum_sort ) = let n = Z3native.get_datatype_sort_num_constructors (sgnc x) (sgno x) in let f i = (func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) i)) in Array.init n f - (** The test predicates for the constants in the enumeration. *) let get_tester_decls ( x : enum_sort ) = let n = Z3native.get_datatype_sort_num_constructors (sgnc x) (sgno x) in let f i = (func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) i)) in @@ -2199,7 +1568,7 @@ struct end -(** Functions to manipulate List expressions *) + module List_ = struct type list_sort = ListSort of sort @@ -2214,46 +1583,36 @@ struct let sgc ( x : list_sort ) = match (x) with ListSort(Sort(s)) -> (z3obj_gc s) let sgnc ( x : list_sort ) = match (x) with ListSort(Sort(s)) -> (z3obj_gnc s) let sgno ( x : list_sort ) = match (x) with ListSort(Sort(s))-> (z3obj_gno s) - - - (** Create a new list sort. *) + let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : sort ) = let (r, a, b, c, d, e, f) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) (Sort.gno elem_sort)) in sort_of_ptr ctx r a b c d e f - (** Create a new list sort. *) let mk_list_s ( ctx : context ) (name : string) elem_sort = mk_sort ctx (Symbol.mk_string ctx name) elem_sort - (** The declaration of the nil function of this list sort. *) let get_nil_decl ( x : list_sort ) = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) 0) - (** The declaration of the isNil function of this list sort. *) let get_is_nil_decl ( x : list_sort ) = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) 0) - (** The declaration of the cons function of this list sort. *) let get_cons_decl ( x : list_sort ) = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor (sgnc x) (sgno x) 1) - (** The declaration of the isCons function of this list sort. *) let get_is_cons_decl ( x : list_sort ) = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_recognizer (sgnc x) (sgno x) 1) - (** The declaration of the head function of this list sort. *) let get_head_decl ( x : list_sort ) = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor_accessor (sgnc x) (sgno x) 1 0) - (** The declaration of the tail function of this list sort. *) let get_tail_decl ( x : list_sort ) = func_decl_of_ptr (sgc x) (Z3native.get_datatype_sort_constructor_accessor (sgnc x) (sgno x) 1 1) - (** The empty list. *) let nil ( x : list_sort ) = expr_of_func_app (sgc x) (get_nil_decl x) [||] end -(** Functions to manipulate Tuple expressions *) + module Tuple = struct type tuple_sort = TupleSort of sort @@ -2268,30 +1627,24 @@ struct let sgnc ( x : tuple_sort ) = match (x) with TupleSort(Sort(s)) -> (z3obj_gnc s) let sgno ( x : tuple_sort ) = match (x) with TupleSort(Sort(s))-> (z3obj_gno s) - - (** Create a new tuple sort. *) let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( field_names : Symbol.symbol array ) ( field_sorts : sort array ) = let f x = Symbol.gno x in let f2 x = ptr_of_ast (ast_of_sort x) in - let (r, a, b) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (Array.length field_names) (Array.map f field_names) (Array.map f2 field_sorts)) in - (* CMW: leaks a,b? *) + let (r, _, _) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (Array.length field_names) (Array.map f field_names) (Array.map f2 field_sorts)) in sort_of_ptr ctx r - (** The constructor function of the tuple. *) let get_mk_decl ( x : tuple_sort ) = func_decl_of_ptr (sgc x) (Z3native.get_tuple_sort_mk_decl (sgnc x) (sgno x)) - (** The number of fields in the tuple. *) let get_num_fields ( x : tuple_sort ) = Z3native.get_tuple_sort_num_fields (sgnc x) (sgno x) - (** The field declarations. *) let get_field_decls ( x : tuple_sort ) = let n = get_num_fields x in let f i = func_decl_of_ptr (sgc x) (Z3native.get_tuple_sort_field_decl (sgnc x) (sgno x) i) in Array.init n f end -(** Functions to manipulate arithmetic expressions *) + module rec Arithmetic : sig type arith_sort = ArithSort of Sort.sort @@ -2516,84 +1869,37 @@ end = struct let ngnc ( x : int_num ) = match (x) with IntNum(e) -> (egnc e) let ngno ( x : int_num ) = match (x) with IntNum(e) -> (egno e) - - (** Create a new integer sort. *) let mk_sort ( ctx : context ) = int_sort_of_ptr ctx (Z3native.mk_int_sort (context_gno ctx)) - (** Retrieve the int value. *) let get_int ( x : int_num ) = let (r, v) = Z3native.get_numeral_int (ngnc x) (ngno x) in if r then v else raise (Z3native.Exception "Conversion failed.") - (** Returns a string representation of the numeral. *) let to_string ( x : int_num ) = Z3native.get_numeral_string (ngnc x) (ngno x) - (** - Creates an integer constant. - *) let mk_int_const ( ctx : context ) ( name : Symbol.symbol ) = IntExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with IntSort(ArithSort(s)) -> s))) - (** - Creates an integer constant. - *) let mk_int_const_s ( ctx : context ) ( name : string ) = mk_int_const ctx (Symbol.mk_string ctx name) - (** - Create an expression representing t1 mod t2. - The arguments must have int type. - *) let mk_mod ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = int_expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (egno t1) (egno t2)) - (** - Create an expression representing t1 rem t2. - The arguments must have int type. - *) let mk_rem ( ctx : context ) ( t1 : int_expr ) ( t2 : int_expr ) = int_expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (egno t1) (egno t2)) - (** - Create an integer numeral. - @param v A string representing the Term value in decimal notation. - *) let mk_int_numeral_s ( ctx : context ) ( v : string ) = int_num_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx))) - (** - Create an integer numeral. - @param v value of the numeral. - @return A Term with value and sort Integer - *) let mk_int_numeral_i ( ctx : context ) ( v : int ) = int_num_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (sgno (mk_sort ctx))) - (** - 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. - *) let mk_int2real ( ctx : context ) ( t : int_expr ) = Real.real_expr_of_arith_expr (arith_expr_of_expr (Expr.expr_of_ptr ctx (Z3native.mk_int2real (context_gno ctx) (egno t)))) - (** - Create an bit bit-vector from the 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. - *) let mk_int2bv ( ctx : context ) ( n : int ) ( t : int_expr ) = BitVector.bitvec_expr_of_expr (Expr.expr_of_ptr ctx (Z3native.mk_int2bv (context_gno ctx) n (egno t))) end @@ -2677,76 +1983,41 @@ end = struct let ngno ( x : rat_num ) = match (x) with RatNum(e) -> (egno e) - (** Create a real sort. *) let mk_sort ( ctx : context ) = real_sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx)) - (** The numerator of a rational numeral. *) let get_numerator ( x : rat_num ) = Integer.int_num_of_ptr (ngc x) (Z3native.get_numerator (ngnc x) (ngno x)) - (** The denominator of a rational numeral. *) let get_denominator ( x : rat_num ) = Integer.int_num_of_ptr (ngc x) (Z3native.get_denominator (ngnc x) (ngno x)) - (** Returns a string representation in decimal notation. - The result has at most decimal places.*) let to_decimal_string ( x : rat_num ) ( precision : int ) = Z3native.get_numeral_decimal_string (ngnc x) (ngno x) precision - (** Returns a string representation of the numeral. *) let to_string ( x : rat_num ) = Z3native.get_numeral_string (ngnc x) (ngno x) - (** Creates a real constant. *) let mk_real_const ( ctx : context ) ( name : Symbol.symbol ) = RealExpr(ArithExpr(Expr.mk_const ctx name (match (mk_sort ctx) with RealSort(ArithSort(s)) -> s))) - (** Creates a real constant. *) let mk_real_const_s ( ctx : context ) ( name : string ) = mk_real_const ctx (Symbol.mk_string ctx name) - (** - Create a real from a fraction. - - @param num numerator of rational. - @param den denominator of rational. - @return A Term with value / and sort Real - - *) let mk_numeral_nd ( ctx : context ) ( num : int ) ( den : int) = if (den == 0) then raise (Z3native.Exception "Denominator is zero") else rat_num_of_ptr ctx (Z3native.mk_real (context_gno ctx) num den) - (** - Create a real numeral. - @param v A string representing the Term value in decimal notation. - @return A Term with value and sort Real - *) let mk_numeral_s ( ctx : context ) ( v : string ) = rat_num_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (mk_sort ctx))) - (** - Create a real numeral. - - @param v value of the numeral. - @return A Term with value and sort Real - *) let mk_numeral_i ( ctx : context ) ( v : int ) = rat_num_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (sgno (mk_sort ctx))) - (** Creates an expression that checks whether a real number is an integer. *) let mk_is_integer ( ctx : context ) ( t : real_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (egno t))) - (** - 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. - *) let mk_real2int ( ctx : context ) ( t : real_expr ) = Integer.int_expr_of_arith_expr (arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (egno t)))) end @@ -2782,208 +2053,97 @@ end = struct let ngno ( x : algebraic_num ) = match (x) with AlgebraicNum(e) -> (egno e) - (** - Return a upper bound for a given real algebraic number. - The interval isolating the number is smaller than 1/10^. - - @param precision the precision of the result - @return A numeral Expr of sort Real - *) let to_upper ( x : algebraic_num ) ( precision : int ) = Real.rat_num_of_ptr (ngc x) (Z3native.get_algebraic_number_upper (ngnc x) (ngno x) precision) - (** - Return a lower bound for the given real algebraic number. - The interval isolating the number is smaller than 1/10^. - - @param precision the precision of the result - @return A numeral Expr of sort Real - *) let to_lower ( x : algebraic_num ) precision = Real.rat_num_of_ptr (ngc x) (Z3native.get_algebraic_number_lower (ngnc x) (ngno x) precision) - (** Returns a string representation in decimal notation. - The result has at most decimal places.*) let to_decimal_string ( x : algebraic_num ) ( precision : int ) = Z3native.get_numeral_decimal_string (ngnc x) (ngno x) precision - (** Returns a string representation of the numeral. *) let to_string ( x : algebraic_num ) = Z3native.get_numeral_string (ngnc x) (ngno x) end - (** - Indicates whether the term is of integer sort. - *) let is_int ( x : expr ) = (Z3native.is_numeral_ast (nc_of_expr x) (nc_of_expr x)) && ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (nc_of_expr x)))) == INT_SORT) - (** - Indicates whether the term is an arithmetic numeral. - *) let is_arithmetic_numeral ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM) - (** - Indicates whether the term is a less-than-or-equal - *) let is_le ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE) - (** - Indicates whether the term is a greater-than-or-equal - *) let is_ge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE) - (** - Indicates whether the term is a less-than - *) let is_lt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LT) - (** - Indicates whether the term is a greater-than - *) let is_gt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GT) - (** - Indicates whether the term is addition (binary) - *) let is_add ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ADD) - (** - Indicates whether the term is subtraction (binary) - *) let is_sub ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SUB) - (** - Indicates whether the term is a unary minus - *) let is_uminus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UMINUS) - (** - Indicates whether the term is multiplication (binary) - *) let is_mul ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MUL) - (** - Indicates whether the term is division (binary) - *) let is_div ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_DIV) - (** - Indicates whether the term is integer division (binary) - *) let is_idiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IDIV) - (** - Indicates whether the term is remainder (binary) - *) let is_remainder ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REM) - (** - Indicates whether the term is modulus (binary) - *) let is_modulus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_MOD) - (** - Indicates whether the term is a coercion of integer to real (unary) - *) let is_inttoreal ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL) - (** - Indicates whether the term is a coercion of real to integer (unary) - *) let is_real_to_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT) - (** - Indicates whether the term is a check that tests whether a real is integral (unary) - *) let is_real_is_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT) - (** - Indicates whether the term is of sort real. - *) let is_real ( x : expr ) = ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (nc_of_expr x)))) == REAL_SORT) - - (** - Indicates whether the term is an integer numeral. - *) let is_int_numeral ( x : expr ) = (Expr.is_numeral x) && (is_int x) - (** - Indicates whether the term is a real numeral. - *) let is_rat_num ( x : expr ) = (Expr.is_numeral x) && (is_real x) - (** - Indicates whether the term is an algebraic number - *) let is_algebraic_number ( x : expr ) = Z3native.is_algebraic_number (nc_of_expr x) (nc_of_expr x) - (** - Create an expression representing t[0] + t[1] + .... - *) let mk_add ( ctx : context ) ( t : arith_expr array ) = let f x = (ptr_of_expr (expr_of_arith_expr x)) in arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_add (context_gno ctx) (Array.length t) (Array.map f t))) - (** - Create an expression representing t[0] * t[1] * .... - *) let mk_mul ( ctx : context ) ( t : arith_expr array ) = let f x = (ptr_of_expr (expr_of_arith_expr x)) in arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_mul (context_gno ctx) (Array.length t) (Array.map f t))) - (** - Create an expression representing t[0] - t[1] - .... - *) let mk_sub ( ctx : context ) ( t : arith_expr array ) = let f x = (ptr_of_expr (expr_of_arith_expr x)) in arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_sub (context_gno ctx) (Array.length t) (Array.map f t))) - (** - Create an expression representing -t. - *) let mk_unary_minus ( ctx : context ) ( t : arith_expr ) = arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_unary_minus (context_gno ctx) (egno t))) - (** - Create an expression representing t1 / t2. - *) let mk_div ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_div (context_gno ctx) (egno t1) (egno t2))) - (** - Create an expression representing t1 ^ t2. - *) let mk_power ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = arith_expr_of_expr (expr_of_ptr ctx (Z3native.mk_power (context_gno ctx) (egno t1) (egno t2))) - (** - Create an expression representing t1 < t2 - *) let mk_lt ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_lt (context_gno ctx) (egno t1) (egno t2))) - (** - Create an expression representing t1 <= t2 - *) let mk_le ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_le (context_gno ctx) (egno t1) (egno t2))) - (** - Create an expression representing t1 > t2 - *) let mk_gt ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_gt (context_gno ctx) (egno t1) (egno t2))) - (** - Create an expression representing t1 >= t2 - *) let mk_ge ( ctx : context ) ( t1 : arith_expr ) ( t2 : arith_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_ge (context_gno ctx) (egno t1) (egno t2))) end -(** Functions to manipulate bit-vector expressions *) + and BitVector : sig type bitvec_sort = BitVecSort of Sort.sort @@ -3089,8 +2249,10 @@ sig val mk_shl : context -> bitvec_expr -> bitvec_expr -> bitvec_expr val mk_lshr : context -> bitvec_expr -> bitvec_expr -> bitvec_expr val mk_ashr : context -> bitvec_expr -> bitvec_expr -> bitvec_expr - val mk_rotate_left : context -> bitvec_expr -> bitvec_expr -> bitvec_expr - val mk_rotate_right : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + val mk_rotate_left : context -> int -> bitvec_expr -> bitvec_expr + val mk_rotate_right : context -> int -> bitvec_expr -> bitvec_expr + val mk_ext_rotate_left : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + val mk_ext_rotate_right : context -> bitvec_expr -> bitvec_expr -> bitvec_expr val mk_bv2int : context -> bitvec_expr -> bool -> Arithmetic.Integer.int_expr val mk_add_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr val mk_add_no_underflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr @@ -3154,1225 +2316,213 @@ end = struct let ngno ( x : bitvec_num ) = match (x) with BitVecNum(e) -> (egno e) - (** - Create a new bit-vector sort. - *) let mk_sort ( ctx : context ) size = bitvec_sort_of_ptr ctx (Z3native.mk_bv_sort (context_gno ctx) size) - - (** - Indicates whether the terms is of bit-vector sort. - *) let is_bv ( x : expr ) = ((sort_kind_of_int (Z3native.get_sort_kind (nc_of_expr x) (Z3native.get_sort (nc_of_expr x) (ptr_of_expr x)))) == BV_SORT) - - (** - Indicates whether the term is a bit-vector numeral - *) let is_bv_numeral ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNUM) - - (** - Indicates whether the term is a one-bit bit-vector with value one - *) let is_bv_bit1 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT1) - - (** - Indicates whether the term is a one-bit bit-vector with value zero - *) let is_bv_bit0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BIT0) - - (** - Indicates whether the term is a bit-vector unary minus - *) let is_bv_uminus ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNEG) - - (** - Indicates whether the term is a bit-vector addition (binary) - *) let is_bv_add ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BADD) - - (** - Indicates whether the term is a bit-vector subtraction (binary) - *) let is_bv_sub ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSUB) - - (** - Indicates whether the term is a bit-vector multiplication (binary) - *) let is_bv_mul ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BMUL) - - (** - Indicates whether the term is a bit-vector signed division (binary) - *) let is_bv_sdiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV) - - (** - Indicates whether the term is a bit-vector unsigned division (binary) - *) let is_bv_udiv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV) - - (** - Indicates whether the term is a bit-vector signed remainder (binary) - *) let is_bv_SRem ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM) - - (** - Indicates whether the term is a bit-vector unsigned remainder (binary) - *) let is_bv_urem ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM) - - (** - Indicates whether the term is a bit-vector signed modulus - *) let is_bv_smod ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD) - - (** - Indicates whether the term is a bit-vector signed division by zero - *) let is_bv_sdiv0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSDIV0) - - (** - Indicates whether the term is a bit-vector unsigned division by zero - *) let is_bv_udiv0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUDIV0) - - (** - Indicates whether the term is a bit-vector signed remainder by zero - *) let is_bv_srem0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSREM0) - - (** - Indicates whether the term is a bit-vector unsigned remainder by zero - *) let is_bv_urem0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BUREM0) - - (** - Indicates whether the term is a bit-vector signed modulus by zero - *) let is_bv_smod0 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSMOD0) - - (** - Indicates whether the term is an unsigned bit-vector less-than-or-equal - *) let is_bv_ule ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULEQ) - - (** - Indicates whether the term is a signed bit-vector less-than-or-equal - *) let is_bv_sle ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLEQ) - - (** - Indicates whether the term is an unsigned bit-vector greater-than-or-equal - *) let is_bv_uge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGEQ) - - (** - Indicates whether the term is a signed bit-vector greater-than-or-equal - *) let is_bv_sge ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGEQ) - - (** - Indicates whether the term is an unsigned bit-vector less-than - *) let is_bv_ult ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ULT) - - (** - Indicates whether the term is a signed bit-vector less-than - *) let is_bv_slt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SLT) - - (** - Indicates whether the term is an unsigned bit-vector greater-than - *) let is_bv_ugt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_UGT) - - (** - Indicates whether the term is a signed bit-vector greater-than - *) let is_bv_sgt ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SGT) - - (** - Indicates whether the term is a bit-wise AND - *) let is_bv_and ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BAND) - - (** - Indicates whether the term is a bit-wise OR - *) let is_bv_or ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BOR) - - (** - Indicates whether the term is a bit-wise NOT - *) let is_bv_not ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOT) - - (** - Indicates whether the term is a bit-wise XOR - *) let is_bv_xor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXOR) - - (** - Indicates whether the term is a bit-wise NAND - *) let is_bv_nand ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNAND) - - (** - Indicates whether the term is a bit-wise NOR - *) let is_bv_nor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNOR) - - (** - Indicates whether the term is a bit-wise XNOR - *) let is_bv_xnor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BXNOR) - - (** - Indicates whether the term is a bit-vector concatenation (binary) - *) let is_bv_concat ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONCAT) - - (** - Indicates whether the term is a bit-vector sign extension - *) let is_bv_signextension ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SIGN_EXT) - - (** - Indicates whether the term is a bit-vector zero extension - *) let is_bv_zeroextension ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ZERO_EXT) - - (** - Indicates whether the term is a bit-vector extraction - *) let is_bv_extract ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXTRACT) - - (** - Indicates whether the term is a bit-vector repetition - *) let is_bv_repeat ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_REPEAT) - - (** - Indicates whether the term is a bit-vector reduce OR - *) let is_bv_reduceor ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDOR) - - (** - Indicates whether the term is a bit-vector reduce AND - *) let is_bv_reduceand ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BREDAND) - - (** - Indicates whether the term is a bit-vector comparison - *) let is_bv_comp ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BCOMP) - - (** - Indicates whether the term is a bit-vector shift left - *) let is_bv_shiftleft ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BSHL) - - (** - Indicates whether the term is a bit-vector logical shift right - *) let is_bv_shiftrightlogical ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BLSHR) - - (** - Indicates whether the term is a bit-vector arithmetic shift left - *) let is_bv_shiftrightarithmetic ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BASHR) - - (** - Indicates whether the term is a bit-vector rotate left - *) let is_bv_rotateleft ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_LEFT) - - (** - Indicates whether the term is a bit-vector rotate right - *) let is_bv_rotateright ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_RIGHT) - - (** - 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. - *) let is_bv_rotateleftextended ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_LEFT) - - (** - 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. - *) - let is_bv_rotaterightextended ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) - - (** - 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. - *) + let is_bv_rotaterightextended ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) let is_int_to_bv ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV) - - (** - 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. - *) let is_bv_to_int ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT) - - (** - 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))) - *) let is_bv_carry ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY) - - (** - 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) - *) let is_bv_xor3 ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3) - - (** The size of a bit-vector sort. *) let get_size (x : bitvec_sort ) = Z3native.get_bv_sort_size (sgnc x) (sgno x) - - (** Retrieve the int value. *) let get_int ( x : bitvec_num ) = let (r, v) = Z3native.get_numeral_int (ngnc x) (ngno x) in if r then v else raise (Z3native.Exception "Conversion failed.") - - (** Returns a string representation of the numeral. *) let to_string ( x : bitvec_num ) = Z3native.get_numeral_string (ngnc x) (ngno x) - - (** - Creates a bit-vector constant. - *) let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) = BitVecExpr(Expr.mk_const ctx name (match (BitVector.mk_sort ctx size) with BitVecSort(s) -> s)) - - (** - Creates a bit-vector constant. - *) let mk_const_s ( ctx : context ) ( name : string ) ( size : int ) = mk_const ctx (Symbol.mk_string ctx name) size - - (** - Bitwise negation. - The argument must have a bit-vector sort. - *) let mk_not ( ctx : context ) ( t : bitvec_expr ) = expr_of_ptr ctx (Z3native.mk_bvnot (context_gno ctx) (egno t)) - - (** - Take conjunction of bits in a vector,vector of length 1. - The argument must have a bit-vector sort. - *) let mk_redand ( ctx : context ) ( t : bitvec_expr) = expr_of_ptr ctx (Z3native.mk_bvredand (context_gno ctx) (egno t)) - - (** - Take disjunction of bits in a vector,vector of length 1. - The argument must have a bit-vector sort. - *) let mk_redor ( ctx : context ) ( t : bitvec_expr) = expr_of_ptr ctx (Z3native.mk_bvredor (context_gno ctx) (egno t)) - - (** - Bitwise conjunction. - The arguments must have a bit-vector sort. - *) let mk_and ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvand (context_gno ctx) (egno t1) (egno t2)) - - (** - Bitwise disjunction. - The arguments must have a bit-vector sort. - *) let mk_or ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvor (context_gno ctx) (egno t1) (egno t2)) - - (** - Bitwise XOR. - The arguments must have a bit-vector sort. - *) let mk_xor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvxor (context_gno ctx) (egno t1) (egno t2)) - - (** - Bitwise NAND. - The arguments must have a bit-vector sort. - *) let mk_nand ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvnand (context_gno ctx) (egno t1) (egno t2)) - - (** - Bitwise NOR. - The arguments must have a bit-vector sort. - *) let mk_nor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvnor (context_gno ctx) (egno t1) (egno t2)) - - (** - Bitwise XNOR. - The arguments must have a bit-vector sort. - *) let mk_xnor ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvxnor (context_gno ctx) (egno t1) (egno t2)) - - (** - Standard two's complement unary minus. - The arguments must have a bit-vector sort. - *) let mk_neg ( ctx : context ) ( t : bitvec_expr) = bitvec_expr_of_ptr ctx (Z3native.mk_bvneg (context_gno ctx) (egno t)) - - (** - Two's complement addition. - The arguments must have the same bit-vector sort. - *) let mk_add ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvadd (context_gno ctx) (egno t1) (egno t2)) - - (** - Two's complement subtraction. - The arguments must have the same bit-vector sort. - *) let mk_sub ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvsub (context_gno ctx) (egno t1) (egno t2)) - - (** - Two's complement multiplication. - The arguments must have the same bit-vector sort. - *) let mk_mul ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvmul (context_gno ctx) (egno t1) (egno t2)) - - (** - 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. - *) let mk_udiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvudiv (context_gno ctx) (egno t1) (egno t2)) - - (** - Signed division. - - 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 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. - *) let mk_sdiv ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvsdiv (context_gno ctx) (egno t1) (egno t2)) - - (** - 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. - *) let mk_urem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvurem (context_gno ctx) (egno t1) (egno t2)) - - (** - 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. - - If t2 is zero, then the result is undefined. - The arguments must have the same bit-vector sort. - *) let mk_srem ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvsrem (context_gno ctx) (egno t1) (egno t2)) - - (** - 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. - *) let mk_smod ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvsmod (context_gno ctx) (egno t1) (egno t2)) - - (** - Unsigned less-than - - The arguments must have the same bit-vector sort. - *) let mk_ult ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvult (context_gno ctx) (egno t1) (egno t2))) - - (** - Two's complement signed less-than - - The arguments must have the same bit-vector sort. - *) let mk_slt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvslt (context_gno ctx) (egno t1) (egno t2))) - - (** - Unsigned less-than or equal to. - - The arguments must have the same bit-vector sort. - *) let mk_ule ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvule (context_gno ctx) (egno t1) (egno t2))) - - (** - Two's complement signed less-than or equal to. - - The arguments must have the same bit-vector sort. - *) let mk_sle ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsle (context_gno ctx) (egno t1) (egno t2))) - - (** - Unsigned greater than or equal to. - - The arguments must have the same bit-vector sort. - *) let mk_uge ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvuge (context_gno ctx) (egno t1) (egno t2))) - - (** - Two's complement signed greater than or equal to. - - The arguments must have the same bit-vector sort. - *) let mk_sge ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (egno t1) (egno t2))) - - (** - Unsigned greater-than. - - The arguments must have the same bit-vector sort. - *) let mk_ugt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (egno t1) (egno t2))) - - (** - Two's complement signed greater-than. - - The arguments must have the same bit-vector sort. - *) let mk_sgt ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (egno t1) (egno t2))) - - (** - 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). - *) let mk_concat ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (egno t1) (egno t2)) - - (** - Bit-vector extraction. - - Extract the bits down to from a bitvector of - size m to yield a new bitvector of size n, where - n = high - low + 1. - The argument must have a bit-vector sort. - *) let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_extract (context_gno ctx) high low (egno t)) - - (** - 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. - The argument must have a bit-vector sort. - *) let mk_sign_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_sign_ext (context_gno ctx) i (egno t)) - - (** - 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. - The argument must have a bit-vector sort. - *) let mk_zero_ext ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_zero_ext (context_gno ctx) i (egno t)) - - (** - Bit-vector repetition. - - The argument must have a bit-vector sort. - *) let mk_repeat ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (egno t)) - - (** - Shift left. - - - It is equivalent to multiplication by 2^x where \c x is the value of . - - 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. - *) let mk_shl ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (egno t1) (egno t2)) - - - (** - Logical shift right - - It is equivalent to unsigned division by 2^x where \c x is the value of . - - 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. - *) let mk_lshr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (egno t1) (egno t2)) - - (** - 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. - - 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. - *) let mk_ashr ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_bvashr (context_gno ctx) (egno t1) (egno t2)) - - (** - Rotate Left. - - Rotate bits of \c t to the left \c i times. - The argument must have a bit-vector sort. - *) let mk_rotate_left ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_rotate_left (context_gno ctx) i (egno t)) - - (** - Rotate Right. - - Rotate bits of \c t to the right \c i times. - The argument must have a bit-vector sort. - *) let mk_rotate_right ( ctx : context ) ( i : int ) ( t : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_rotate_right (context_gno ctx) i (egno t)) - - (** - Rotate Left. - - Rotate bits of to the left times. - The arguments must have the same bit-vector sort. - *) - let mk_rotate_left ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + let mk_ext_rotate_left ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (egno t1) (egno t2)) - - (** - Rotate Right. - - - Rotate bits of to the right times. - The arguments must have the same bit-vector sort. - *) - let mk_rotate_right ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = + let mk_ext_rotate_right ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = bitvec_expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (egno t1) (egno t2)) - - (** - 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 . - If \c is_signed is true, \c t1 is treated as a signed bit-vector. - - 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 bit-vector sort. - *) let mk_bv2int ( ctx : context ) ( t : bitvec_expr ) ( signed : bool ) = Arithmetic.Integer.int_expr_of_ptr ctx (Z3native.mk_bv2int (context_gno ctx) (egno t) signed) - - (** - Create a predicate that checks that the bit-wise addition does not overflow. - - The arguments must be of bit-vector sort. - *) let mk_add_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (egno t1) (egno t2) signed)) - - (** - Create a predicate that checks that the bit-wise addition does not underflow. - - The arguments must be of bit-vector sort. - *) let mk_add_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (egno t1) (egno t2))) - - (** - Create a predicate that checks that the bit-wise subtraction does not overflow. - - The arguments must be of bit-vector sort. - *) let mk_sub_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (egno t1) (egno t2))) - - (** - Create a predicate that checks that the bit-wise subtraction does not underflow. - - The arguments must be of bit-vector sort. - *) let mk_sub_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (egno t1) (egno t2) signed)) - - (** - Create a predicate that checks that the bit-wise signed division does not overflow. - - The arguments must be of bit-vector sort. - *) let mk_sdiv_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) (egno t1) (egno t2))) - - (** - Create a predicate that checks that the bit-wise negation does not overflow. - - The arguments must be of bit-vector sort. - *) let mk_neg_no_overflow ( ctx : context ) ( t : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (egno t))) - - (** - Create a predicate that checks that the bit-wise multiplication does not overflow. - - The arguments must be of bit-vector sort. - *) let mk_mul_no_overflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) ( signed : bool) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (egno t1) (egno t2) signed)) - - (** - Create a predicate that checks that the bit-wise multiplication does not underflow. - - The arguments must be of bit-vector sort. - *) let mk_mul_no_underflow ( ctx : context ) ( t1 : bitvec_expr ) ( t2 : bitvec_expr ) = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (egno t1) (egno t2))) - - (** - Create a bit-vector numeral. - - @param v A string representing the value in decimal notation. - @param size the size of the bit-vector - *) let mk_numeral ( ctx : context ) ( v : string ) ( size : int) = bitvec_num_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (sgno (BitVector.mk_sort ctx size))) end -(** Functions to manipulate proof expressions *) + module Proof = struct - (** - Indicates whether the term is a Proof for the expression 'true'. - *) let is_true ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE) - - (** - Indicates whether the term is a proof for a fact asserted by the user. - *) let is_asserted ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ASSERTED) - - (** - Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. - *) let is_goal ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_GOAL) - - (** - 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). - *) let is_modus_ponens ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS) - - (** - 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'. - *) let is_reflexivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REFLEXIVITY) - - (** - 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. - *) let is_symmetry ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SYMMETRY) - - (** - 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) - *) let is_transitivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY) - - (** - 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. - *) let is_Transitivity_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRANSITIVITY_STAR) - - - (** - 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. - *) let is_monotonicity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MONOTONICITY) - - (** - 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)) - *) let is_quant_intro ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INTRO) - - (** - 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. - *) let is_distributivity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DISTRIBUTIVITY) - - (** - 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 - *) let is_and_elimination ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_AND_ELIM) - - (** - 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) - *) let is_or_elimination ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NOT_OR_ELIM) - - (** - 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) - *) let is_rewrite ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE) - - (** - 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) - *) let is_rewrite_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_REWRITE_STAR) - - (** - 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. - *) let is_pull_quant ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT) - - (** - 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 - *) let is_pull_quant_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PULL_QUANT_STAR) - - (** - 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 - *) - let is_push_quant ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_PUSH_QUANT) - - (** - 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. - *) - let is_elim_unused_vars ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ELIM_UNUSED_VARS) - - (** - 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. - *) - let is_der ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DER) - - (** - Indicates whether the term is a proof for quantifier instantiation - - A proof of (or (not (forall (x) (P x))) (P a)) - *) let is_quant_inst ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_QUANT_INST) - - (** - Indicates whether the term is a hypthesis marker. - Mark a hypothesis in a natural deduction style proof. - *) let is_hypothesis ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_HYPOTHESIS) - - (** - 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. - *) let is_lemma ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_LEMMA) - - (** - 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') - *) let is_unit_resolution ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_UNIT_RESOLUTION) - - (** - Indicates whether the term is a proof by iff-true - - T1: p - [iff-true T1]: (iff p true) - *) let is_iff_true ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_TRUE) - - (** - Indicates whether the term is a proof by iff-false - - T1: (not p) - [iff-false T1]: (iff p false) - *) let is_iff_false ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_FALSE) - - (** - 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. - *) let is_commutativity ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_COMMUTATIVITY) (* *) - - (** - 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). - *) let is_def_axiom ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_AXIOM) - - (** - 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) - *) let is_def_intro ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_DEF_INTRO) - - (** - 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. - *) let is_apply_def ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_APPLY_DEF) - - (** - Indicates whether the term is a proof iff-oeq - - T1: (iff p q) - [iff~ T1]: (~ p q) - *) let is_iff_oeq ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_IFF_OEQ) - - (** - 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'. - *) let is_nnf_pos ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_POS) - - (** - 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'))) - *) let is_nnf_neg ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_NEG) - - (** - 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. - *) let is_nnf_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_NNF_STAR) - - (** - 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. - *) let is_cnf_star ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_CNF_STAR) - - (** - 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. - *) let is_skolemize ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_SKOLEMIZE) - - (** - 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 - *) let is_modus_ponens_oeq ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_MODUS_PONENS_OEQ) - - (** - 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. - *) let is_theory_lemma ( x : expr ) = (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TH_LEMMA) end -(** Goals - - A goal (aka problem). A goal is essentially a - of formulas, that can be solved and/or transformed using - tactics and solvers. *) module Goal = struct type goal = z3_native_object @@ -4386,76 +2536,52 @@ struct (z3obj_create res) ; res - - (** The precision of the goal. - - Goals can be transformed using over and under approximations. - An under approximation is applied when the objective is to find a model for a given goal. - An over approximation is applied when the objective is to find a proof for a given goal. - *) let get_precision ( x : goal ) = goal_prec_of_int (Z3native.goal_precision (z3obj_gnc x) (z3obj_gno x)) - (** Indicates whether the goal is precise. *) let is_precise ( x : goal ) = (get_precision x) == GOAL_PRECISE - (** Indicates whether the goal is an under-approximation. *) let is_underapproximation ( x : goal ) = (get_precision x) == GOAL_UNDER - (** Indicates whether the goal is an over-approximation. *) let is_overapproximation ( x : goal ) = (get_precision x) == GOAL_OVER - (** Indicates whether the goal is garbage (i.e., the product of over- and under-approximations). *) let is_garbage ( x : goal ) = (get_precision x) == GOAL_UNDER_OVER - (** Adds the constraints to the given goal. *) - (* CMW: assert seems to be a keyword. *) let assert_ ( x : goal ) ( constraints : Boolean.bool_expr array ) = let f e = Z3native.goal_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e) in ignore (Array.map f constraints) ; () - (** Indicates whether the goal contains `false'. *) let is_inconsistent ( x : goal ) = Z3native.goal_inconsistent (z3obj_gnc x) (z3obj_gno x) - (** The depth of the goal. - This tracks how many transformations were applied to it. *) let get_depth ( x : goal ) = Z3native.goal_depth (z3obj_gnc x) (z3obj_gno x) - (** Erases all formulas from the given goal. *) let reset ( x : goal ) = Z3native.goal_reset (z3obj_gnc x) (z3obj_gno x) - (** The number of formulas in the goal. *) let get_size ( x : goal ) = Z3native.goal_size (z3obj_gnc x) (z3obj_gno x) - (** The formulas in the goal. *) let get_formulas ( x : goal ) = let n = get_size x in let f i = (Boolean.bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i))) in Array.init n f - (** The number of formulas, subformulas and terms in the goal. *) let get_num_exprs ( x : goal ) = Z3native.goal_num_exprs (z3obj_gnc x) (z3obj_gno x) - (** Indicates whether the goal is empty, and it is precise or the product of an under approximation. *) let is_decided_sat ( x : goal ) = Z3native.goal_is_decided_sat (z3obj_gnc x) (z3obj_gno x) - (** Indicates whether the goal contains `false', and it is precise or the product of an over approximation. *) let is_decided_unsat ( x : goal ) = Z3native.goal_is_decided_unsat (z3obj_gnc x) (z3obj_gno x) - (** Translates (copies) the Goal to the target Context . *) let translate ( x : goal ) ( to_ctx : context ) = create to_ctx (Z3native.goal_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) - (** Simplifies the goal. Essentially invokes the `simplify' tactic on the goal. *) let simplify ( x : goal ) ( p : Params.params option ) = let tn = Z3native.mk_tactic (z3obj_gnc x) "simplify" in Z3native.tactic_inc_ref (z3obj_gnc x) tn ; @@ -4473,27 +2599,13 @@ struct Z3native.tactic_dec_ref (z3obj_gnc x) tn ; create (z3obj_gc x) res - - (** - Creates a new Goal. - - Note that the Context must have been created with proof generation support if - is set to true here. - @param models Indicates whether model generation should be enabled. - @param unsat_cores Indicates whether unsat core generation should be enabled. - @param proofs Indicates whether proof generation should be enabled. - *) let mk_goal ( ctx : context ) ( models : bool ) ( unsat_cores : bool ) ( proofs : bool ) = create ctx (Z3native.mk_goal (context_gno ctx) models unsat_cores proofs) - (** A string representation of the Goal. *) let to_string ( x : goal ) = Z3native.goal_to_string (z3obj_gnc x) (z3obj_gno x) end -(** Models - - A Model contains interpretations (assignments) of constants and functions. *) module Model = struct type model = z3_native_object @@ -4507,12 +2619,6 @@ struct (z3obj_create res) ; res - - (** Function interpretations - - A function interpretation is represented as a finite map and an 'else'. - Each entry in the finite map represents the value of a function given a set of arguments. - *) module FuncInterp = struct type func_interp = z3_native_object @@ -4526,11 +2632,6 @@ struct (z3obj_create res) ; res - - (** Function interpretations entries - - An Entry object represents an element in the finite map used to a function interpretation. - *) module FuncEntry = struct type func_entry = z3_native_object @@ -4544,61 +2645,33 @@ struct (z3obj_create res) ; res - - (** - Return the (symbolic) value of this entry. - *) let get_value ( x : func_entry ) = expr_of_ptr (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 (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 = (expr_of_ptr (z3obj_gc x) (Z3native.func_entry_get_arg (z3obj_gnc x) (z3obj_gno x) i)) in Array.init n f - (** - A string representation of the function entry. - *) let to_string ( x : func_entry ) = let a = (get_args x) in let f c p = (p ^ (Expr.to_string c) ^ ", ") in "[" ^ Array.fold_right f a ((Expr.to_string (get_value x)) ^ "]") end - (** - The number of entries in the function interpretation. - *) 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 = (FuncEntry.create (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 ) = expr_of_ptr (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 (z3obj_gnc x) (z3obj_gno x) - (** - A string representation of the function interpretation. - *) let to_string ( x : func_interp ) = let f c p = ( let n = (FuncEntry.get_num_args c) in @@ -4613,9 +2686,6 @@ struct Array.fold_right f (get_entries x) ("else -> " ^ (Expr.to_string (get_else x)) ^ "]") end - (** Retrieves the interpretation (the assignment) of in the model. - A function declaration of zero arity - An expression if the function has an interpretation in the model, null otherwise. *) let get_const_interp ( x : model ) ( f : func_decl ) = if (FuncDecl.get_arity f) != 0 || (sort_kind_of_int (Z3native.get_sort_kind (FuncDecl.gnc f) (Z3native.get_range (FuncDecl.gnc f) (FuncDecl.gno f)))) == ARRAY_SORT then @@ -4627,16 +2697,9 @@ struct else Some (expr_of_ptr (z3obj_gc x) np) - (** Retrieves the interpretation (the assignment) of in the model. - A Constant - An expression if the constant has an interpretation in the model, null otherwise. - *) let get_const_interp_e ( x : model ) ( a : expr ) = get_const_interp x (Expr.get_func_decl a) - (** Retrieves the interpretation (the assignment) of a non-constant in the model. - A function declaration of non-zero arity - A FunctionInterpretation if the function has an interpretation in the model, null otherwise. *) let rec get_func_interp ( x : model ) ( f : func_decl ) = let sk = (sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc x) (Z3native.get_range (FuncDecl.gnc f) (FuncDecl.gno f)))) in if (FuncDecl.get_arity f) == 0 then @@ -4659,23 +2722,18 @@ struct (** 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) - (** The function declarations of the constants in the model. *) let get_const_decls ( x : model ) = let n = (get_num_consts x) in let f i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f - - (** The number of function interpretations in the model. *) let get_num_funcs ( x : model ) = Z3native.model_get_num_funcs (z3obj_gnc x) (z3obj_gno x) - (** The function declarations of the function interpretations in the model. *) let get_func_decls ( x : model ) = let n = (get_num_consts x) in let f i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f - (** All symbols that have an interpretation in the model. *) let get_decls ( x : model ) = let n_funcs = (get_num_funcs x) in let n_consts = (get_num_consts x ) in @@ -4683,24 +2741,8 @@ struct let g i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in Array.append (Array.init n_funcs f) (Array.init n_consts g) - (** A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. *) exception ModelEvaluationFailedException of string - (** - Evaluates the expression in the current model. - - - This function may fail if contains quantifiers, - is partial (MODEL_PARTIAL enabled), or if is not well-sorted. - In this case a ModelEvaluationFailedException is thrown. - - An expression - - When this flag is enabled, a model value will be assigned to any constant - or function that does not have an interpretation in the model. - - The evaluation of in the model. - *) let eval ( x : model ) ( t : expr ) ( completion : bool ) = let (r, v) = (Z3native.model_eval (z3obj_gnc x) (z3obj_gno x) (ptr_of_expr t) completion) in if not r then @@ -4708,53 +2750,26 @@ struct else expr_of_ptr (z3obj_gc x) v - (** Alias for eval. *) let evaluate ( x : model ) ( t : expr ) ( completion : bool ) = eval x t completion - (** The number of uninterpreted sorts that the model has an interpretation for. *) let get_num_sorts ( x : model ) = Z3native.model_get_num_sorts (z3obj_gnc x) (z3obj_gno x) - (** The uninterpreted sorts that the model has an interpretation for. - - Z3 also provides an intepretation for uninterpreted sorts used in a formula. - The interpretation for a sort is a finite set of distinct values. We say this finite set is - the "universe" of the sort. - - - *) let get_sorts ( x : model ) = let n = (get_num_sorts x) in let f i = (sort_of_ptr (z3obj_gc x) (Z3native.model_get_sort (z3obj_gnc x) (z3obj_gno x) i)) in Array.init n f - - (** The finite set of distinct values that represent the interpretation for sort . - - An uninterpreted sort - An array of expressions, where each is an element of the universe of - *) let sort_universe ( x : model ) ( s : sort ) = let n_univ = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in let n = (AST.ASTVector.get_size n_univ) in let f i = (AST.ASTVector.get n_univ i) in Array.init n f - - (** Conversion of models to strings. - A string representation of the model. - *) + let to_string ( x : model ) = Z3native.model_to_string (z3obj_gnc x) (z3obj_gno x) 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 Context.NumProbes - and Context.ProbeNames. - It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. -*) module Probe = struct type probe = z3_native_object @@ -4769,114 +2784,52 @@ struct res - (** - Execute the probe over the goal. - A probe always produce a double value. - "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. - *) let apply ( x : probe ) ( g : Goal.goal ) = Z3native.probe_apply (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g) - (** - 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 ) = (create ctx (Z3native.mk_probe (context_gno ctx) name)) - (** - Create a probe that always evaluates to . - *) let const ( ctx : context ) ( v : float ) = (create ctx (Z3native.probe_const (context_gno ctx) v)) - (** - Create a probe that evaluates to "true" when the value returned by - is less than the value returned by - *) let lt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = (create 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 - is greater than the value returned by - *) let gt ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = (create 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 - is less than or equal the value returned by - *) let le ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = (create 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 - is greater than or equal the value returned by - *) let ge ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = (create 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 - is equal to the value returned by - *) let eq ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = (create ctx (Z3native.probe_eq (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) - (** - Create a probe that evaluates to "true" when the value - and evaluate to "true". - *) - (* CMW: and is a keyword *) let and_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = (create ctx (Z3native.probe_and (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) - (** - Create a probe that evaluates to "true" when the value - or evaluate to "true". - *) - (* CMW: or is a keyword *) let or_ ( ctx : context ) ( p1 : probe ) ( p2 : probe ) = (create ctx (Z3native.probe_or (context_gno ctx) (z3obj_gno p1) (z3obj_gno p2))) - (** - Create a probe that evaluates to "true" when the value - does not evaluate to "true". - *) - (* CMW: is not a keyword? *) let not_ ( ctx : context ) ( p : probe ) = (create 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. - The complete list of tactics may be obtained using Context.get_num_tactics - and Context.get_tactic_names. - It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. -*) module Tactic = struct type tactic = z3_native_object @@ -4890,11 +2843,6 @@ struct (z3obj_create res) ; res - - (** Tactic application results - - ApplyResult objects represent the result of an application of a - tactic to a goal. It contains the subgoals that were produced. *) module ApplyResult = struct type apply_result = z3_native_object @@ -4908,75 +2856,46 @@ struct (z3obj_create res) ; res - - (** The number of Subgoals. *) let get_num_subgoals ( x : apply_result ) = 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 = Goal.create (z3obj_gc x) (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 ) = Goal.create (z3obj_gc x) (Z3native.apply_result_get_subgoal (z3obj_gnc x) (z3obj_gno x) i) - (** Convert a model for the subgoal into a model for the original - goal g, that the ApplyResult was obtained from. - #return A model for g - *) let convert_model ( x : apply_result ) ( i : int ) ( m : Model.model ) = Model.create (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 (z3obj_gnc x) (z3obj_gno x) end - (** A string containing a description of parameters accepted by the tactic. *) let get_help ( x : tactic ) = Z3native.tactic_get_help (z3obj_gnc x) (z3obj_gno x) - (** Retrieves parameter descriptions for Tactics. *) let get_param_descrs ( x : tactic ) = Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.tactic_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) - (** Apply the tactic to the goal. *) let apply ( x : tactic ) ( g : Goal.goal ) ( p : Params.params option ) = match p with | None -> (ApplyResult.create (z3obj_gc x) (Z3native.tactic_apply (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g))) | Some (pn) -> (ApplyResult.create (z3obj_gc x) (Z3native.tactic_apply_ex (z3obj_gnc x) (z3obj_gno x) (z3obj_gno g) (z3obj_gno pn))) - (** - The number of supported tactics. - *) let get_num_tactics ( ctx : context ) = Z3native.get_num_tactics (context_gno ctx) - (** - The names of all supported tactics. - *) let get_tactic_names ( ctx : context ) = let n = (get_num_tactics ctx ) in let f i = (Z3native.get_tactic_name (context_gno ctx) i) in Array.init n f - - (** - Returns a string containing a description of the tactic with the given name. - *) let get_tactic_description ( ctx : context ) ( name : string ) = Z3native.tactic_get_descr (context_gno ctx) name - (** - Creates a new Tactic. - *) let mk_tactic ( ctx : context ) ( name : string ) = create ctx (Z3native.mk_tactic (context_gno ctx) name) - (** - Create a tactic that applies to a Goal and - then to every subgoal produced by . - *) let and_then ( ctx : context ) ( t1 : tactic ) ( t2 : tactic ) ( ts : tactic array ) = let f p c = (match p with | None -> (Some (z3obj_gno c)) @@ -4988,106 +2907,50 @@ struct let o = (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t2) x) in create ctx (Z3native.tactic_and_then (context_gno ctx) (z3obj_gno t1) o) - (** - Create a tactic that first applies to a Goal and - if it fails then returns the result of applied to the Goal. - *) let or_else ( ctx : context ) ( t1 : tactic ) ( t2 : tactic ) = create ctx (Z3native.tactic_or_else (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) - (** - Create a tactic that applies to a goal for milliseconds. - - If does not terminate within milliseconds, then it fails. - *) let try_for ( ctx : context ) ( t : tactic ) ( ms : int ) = create ctx (Z3native.tactic_try_for (context_gno ctx) (z3obj_gno t) ms) - (** - Create a tactic that applies to a given goal if the probe - evaluates to true. - - If evaluates to false, then the new tactic behaves like the skip tactic. - *) - (* CMW: when is a keyword *) let when_ ( ctx : context ) ( p : Probe.probe ) ( t : tactic ) = create ctx (Z3native.tactic_when (context_gno ctx) (z3obj_gno p) (z3obj_gno t)) - (** - Create a tactic that applies to a given goal if the probe - evaluates to true and otherwise. - *) let cond ( ctx : context ) ( p : Probe.probe ) ( t1 : tactic ) ( t2 : tactic ) = create ctx (Z3native.tactic_cond (context_gno ctx) (z3obj_gno p) (z3obj_gno t1) (z3obj_gno t2)) - (** - Create a tactic that keeps applying until the goal is not - modified anymore or the maximum number of iterations is reached. - *) let repeat ( ctx : context ) ( t : tactic ) ( max : int ) = create ctx (Z3native.tactic_repeat (context_gno ctx) (z3obj_gno t) max) - (** - Create a tactic that just returns the given goal. - *) let skip ( ctx : context ) = create ctx (Z3native.tactic_skip (context_gno ctx)) - (** - Create a tactic always fails. - *) let fail ( ctx : context ) = create ctx (Z3native.tactic_fail (context_gno ctx)) - (** - Create a tactic that fails if the probe evaluates to false. - *) let fail_if ( ctx : context ) ( p : Probe.probe ) = create ctx (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) - or trivially unsatisfiable (i.e., contains `false'). - *) let fail_if_not_decided ( ctx : context ) = create ctx (Z3native.tactic_fail_if_not_decided (context_gno ctx)) - (** - Create a tactic that applies using the given set of parameters . - *) let using_params ( ctx : context ) ( t : tactic ) ( p : Params.params ) = create ctx (Z3native.tactic_using_params (context_gno ctx) (z3obj_gno t) (z3obj_gno p)) - (** - Create a tactic that applies using the given set of parameters . - Alias for UsingParams*) - (* CMW: with is a keyword *) let with_ ( ctx : context ) ( t : tactic ) ( p : Params.params ) = using_params ctx t p - (** - Create a tactic that applies the given tactics in parallel. - *) let par_or ( ctx : context ) ( t : tactic array ) = create ctx (Z3native.tactic_par_or (context_gno ctx) (Array.length t) (array_to_native t)) - (** - Create a tactic that applies to a given goal and then - to every subgoal produced by . The subgoals are processed in parallel. - *) let par_and_then ( ctx : context ) ( t1 : tactic ) ( t2 : tactic ) = create ctx (Z3native.tactic_par_and_then (context_gno ctx) (z3obj_gno t1) (z3obj_gno t2)) - (** - Interrupt the execution of a Z3 procedure. - This procedure can be used to interrupt: solvers, simplifiers and tactics. - *) let interrupt ( ctx : context ) = Z3native.interrupt (context_gno ctx) end -(** Solvers *) module Solver = struct type solver = z3_native_object @@ -5102,13 +2965,11 @@ struct (z3obj_create res) ; res - let string_of_status ( s : status) = match s with | UNSATISFIABLE -> "unsatisfiable" | SATISFIABLE -> "satisfiable" | _ -> "unknown" - (** Objects that track statistical information about solvers. *) module Statistics = struct type statistics = z3_native_object @@ -5123,11 +2984,6 @@ struct res - (** - 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 = { @@ -5158,22 +3014,11 @@ struct res - (** The key of the entry. *) let get_key (x : statistics_entry) = x.m_key - - (** The int-value of the entry. *) - let get_int (x : statistics_entry) = x.m_int - - (** The float-value of the entry. *) + let get_int (x : statistics_entry) = x.m_int let get_float (x : statistics_entry) = x.m_float - - (** True if the entry is uint-valued. *) let is_int (x : statistics_entry) = x.m_is_int - - (** True if the entry is double-valued. *) 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) = if (is_int x) then string_of_int (get_int x) @@ -5181,18 +3026,13 @@ struct string_of_float (get_float x) else raise (Z3native.Exception "Unknown statistical entry type") - - (** The string representation of the entry (key and value) *) let to_string ( x : statistics_entry ) = (get_key x) ^ ": " ^ (to_string_value x) end - (** A string representation of the statistical data. *) let to_string ( x : statistics ) = Z3native.stats_to_string (z3obj_gnc x) (z3obj_gno x) - (** The number of statistical data. *) let get_size ( x : statistics ) = Z3native.stats_size (z3obj_gnc x) (z3obj_gno x) - (** The data entries. *) let get_entries ( x : statistics ) = let n = (get_size x ) in let f i = ( @@ -5204,129 +3044,56 @@ struct ) in Array.init n f - (** - The statistical counters. - *) let get_keys ( x : statistics ) = let n = (get_size x) in let f i = (Z3native.stats_get_key (z3obj_gnc x) (z3obj_gno x) i) in Array.init n f - (** The value of a particular statistical counter. *) let get ( x : statistics ) ( key : string ) = let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in Array.fold_left f None (get_entries x) end - (** - A string that describes all available solver parameters. - *) let get_help ( x : solver ) = Z3native.solver_get_help (z3obj_gnc x) (z3obj_gno x) - (** - Sets the solver parameters. - *) let set_parameters ( x : solver ) ( p : Params.params )= Z3native.solver_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) - (** - Retrieves parameter descriptions for solver. - *) let get_param_descrs ( x : solver ) = Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.solver_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) - (** - The current number of backtracking points (scopes). - - - *) let get_num_scopes ( x : solver ) = Z3native.solver_get_num_scopes (z3obj_gnc x) (z3obj_gno x) - (** - Creates a backtracking point. - - *) let push ( x : solver ) = Z3native.solver_push (z3obj_gnc x) (z3obj_gno x) - (** - Backtracks backtracking points. - Note that an exception is thrown if is not smaller than NumScopes - - *) let pop ( x : solver ) ( n : int ) = Z3native.solver_pop (z3obj_gnc x) (z3obj_gno x) n - (** - Resets the Solver. - This removes all assertions from the solver. - *) let reset ( x : solver ) = Z3native.solver_reset (z3obj_gnc x) (z3obj_gno x) - (** - Assert a constraint (or multiple) into the solver. - *) let assert_ ( x : solver ) ( constraints : Boolean.bool_expr array ) = let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e)) in ignore (Array.map f constraints) - (** - * 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 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 - * and the Boolean literals - * provided using with assumptions. - *) - let assert_and_track ( x : solver ) ( cs : Boolean.bool_expr array ) ( ps : Boolean.bool_expr array ) = + let assert_and_track_a ( x : solver ) ( cs : Boolean.bool_expr array ) ( ps : Boolean.bool_expr array ) = if ((Array.length cs) != (Array.length ps)) then raise (Z3native.Exception "Argument size mismatch") else let f i e = (Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e) (Boolean.gno (Array.get ps i))) in ignore (Array.iteri f cs) - (** - * 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 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 - * and the Boolean literals - * provided using with assumptions. - *) let assert_and_track ( x : solver ) ( c : Boolean.bool_expr ) ( p : Boolean.bool_expr ) = Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) (Boolean.gno c) (Boolean.gno p) - (** - The number of assertions in the solver. - *) let get_num_assertions ( x : solver ) = let a = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in (AST.ASTVector.get_size a) - - (** - The set of asserted formulas. - *) let get_assertions ( x : solver ) = let a = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in let n = (AST.ASTVector.get_size a) in let f i = Boolean.bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in Array.init n f - (** - Checks whether the assertions in the solver are consistent or not. - - - - - *) let check ( x : solver ) ( assumptions : Boolean.bool_expr array) = let r = if ((Array.length assumptions) == 0) then @@ -5340,12 +3107,6 @@ struct | L_FALSE -> UNSATISFIABLE | _ -> UNKNOWN - (** - 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. - *) let get_model ( x : solver ) = let q = Z3native.solver_get_model (z3obj_gnc x) (z3obj_gno x) in if (Z3native.is_null q) then @@ -5353,12 +3114,6 @@ struct else Some (Model.create (z3obj_gc x) q) - (** - 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. - *) let get_proof ( x : solver ) = let q = Z3native.solver_get_proof (z3obj_gnc x) (z3obj_gno x) in if (Z3native.is_null q) then @@ -5366,73 +3121,35 @@ struct else Some (expr_of_ptr (z3obj_gc x) q) - (** - 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. - *) let get_unsat_core ( x : solver ) = let cn = AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in let n = (AST.ASTVector.get_size cn) in let f i = (AST.ASTVector.get cn i) in Array.init n f - (** - A brief justification of why the last call to Check returned UNKNOWN. - *) let get_reason_unknown ( x : solver ) = Z3native.solver_get_reason_unknown (z3obj_gnc x) (z3obj_gno x) - - (** - Solver statistics. - *) let get_statistics ( x : solver ) = (Statistics.create (z3obj_gc x) (Z3native.solver_get_statistics (z3obj_gnc x) (z3obj_gno x))) - (** - 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. - *) let mk_solver ( ctx : context ) ( logic : Symbol.symbol option ) = match logic with | None -> (create ctx (Z3native.mk_solver (context_gno ctx))) | Some (x) -> (create ctx (Z3native.mk_solver_for_logic (context_gno ctx) (Symbol.gno x))) - (** - Creates a new (incremental) solver. - - *) let mk_solver_s ( ctx : context ) ( logic : string ) = mk_solver ctx (Some (Symbol.mk_string ctx logic)) - (** - Creates a new (incremental) solver. - *) let mk_simple_solver ( ctx : context ) = (create ctx (Z3native.mk_simple_solver (context_gno ctx))) - (** - 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. - *) let mk_solver_t ( ctx : context ) ( t : Tactic.tactic ) = (create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t))) - (** - A string representation of the solver. - *) let to_string ( x : solver ) = Z3native.solver_to_string (z3obj_gnc x) (z3obj_gno x) end -(** Fixedpoint solving *) module Fixedpoint = struct type fixedpoint = z3_native_object @@ -5447,70 +3164,37 @@ struct res - (** - A string that describes all available fixedpoint solver parameters. - *) let get_help ( x : fixedpoint ) = Z3native.fixedpoint_get_help (z3obj_gnc x) (z3obj_gno x) - (** - Sets the fixedpoint solver parameters. - *) let set_params ( x : fixedpoint ) ( p : Params.params )= Z3native.fixedpoint_set_params (z3obj_gnc x) (z3obj_gno x) (z3obj_gno p) - (** - Retrieves parameter descriptions for Fixedpoint solver. - *) let get_param_descrs ( x : fixedpoint ) = Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x)) - (** - Assert a constraints into the fixedpoint solver. - *) let assert_ ( x : fixedpoint ) ( constraints : Boolean.bool_expr array ) = let f e = (Z3native.fixedpoint_assert (z3obj_gnc x) (z3obj_gno x) (Boolean.gno e)) in ignore (Array.map f constraints) ; () - (** - Register predicate as recursive relation. - *) let register_relation ( x : fixedpoint ) ( f : func_decl ) = Z3native.fixedpoint_register_relation (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) - (** - Add rule into the fixedpoint solver. - *) let add_rule ( x : fixedpoint ) ( rule : Boolean.bool_expr ) ( name : Symbol.symbol option ) = match name with | None -> Z3native.fixedpoint_add_rule (z3obj_gnc x) (z3obj_gno x) (Boolean.gno rule) null | Some(y) -> Z3native.fixedpoint_add_rule (z3obj_gnc x) (z3obj_gno x) (Boolean.gno rule) (Symbol.gno y) - (** - Add table fact to the fixedpoint solver. - *) let add_fact ( x : fixedpoint ) ( pred : func_decl ) ( args : int array ) = Z3native.fixedpoint_add_fact (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno pred) (Array.length args) args - (** - 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. - *) let query ( x : fixedpoint ) ( query : Boolean.bool_expr ) = match (lbool_of_int (Z3native.fixedpoint_query (z3obj_gnc x) (z3obj_gno x) (Boolean.gno query))) with | L_TRUE -> Solver.SATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE | _ -> Solver.UNKNOWN - (** - 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. - *) let query_r ( x : fixedpoint ) ( relations : func_decl array ) = let f x = ptr_of_ast (ast_of_func_decl x) in match (lbool_of_int (Z3native.fixedpoint_query_relations (z3obj_gnc x) (z3obj_gno x) (Array.length relations) (Array.map f relations))) with @@ -5518,32 +3202,15 @@ struct | L_FALSE -> Solver.UNSATISFIABLE | _ -> Solver.UNKNOWN - (** - Creates a backtracking point. - - *) let push ( x : fixedpoint ) = Z3native.fixedpoint_push (z3obj_gnc x) (z3obj_gno x) - (** - Backtrack one backtracking point. - - Note that an exception is thrown if Pop is called without a corresponding Push - - *) let pop ( x : fixedpoint ) = Z3native.fixedpoint_pop (z3obj_gnc x) (z3obj_gno x) - (** - Update named rule into in the fixedpoint solver. - *) let update_rule ( x : fixedpoint ) ( rule : Boolean.bool_expr ) ( name : Symbol.symbol ) = Z3native.fixedpoint_update_rule (z3obj_gnc x) (z3obj_gno x) (Boolean.gno rule) (Symbol.gno name) - (** - Retrieve satisfying instance or instances of solver, - or definitions for the recursive predicates that show unsatisfiability. - *) let get_answer ( x : fixedpoint ) = let q = (Z3native.fixedpoint_get_answer (z3obj_gnc x) (z3obj_gno x)) in if (Z3native.is_null q) then @@ -5551,21 +3218,12 @@ struct else Some (expr_of_ptr (z3obj_gc x) q) - (** - Retrieve explanation why fixedpoint engine returned status Unknown. - *) let get_reason_unknown ( x : fixedpoint ) = Z3native.fixedpoint_get_reason_unknown (z3obj_gnc x) (z3obj_gno x) - (** - Retrieve the number of levels explored for a given predicate. - *) let get_num_levels ( x : fixedpoint ) ( predicate : func_decl ) = Z3native.fixedpoint_get_num_levels (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno predicate) - (** - Retrieve the cover of a predicate. - *) let get_cover_delta ( x : fixedpoint ) ( level : int ) ( predicate : func_decl ) = let q = (Z3native.fixedpoint_get_cover_delta (z3obj_gnc x) (z3obj_gno x) level (FuncDecl.gno predicate)) in if (Z3native.is_null q) then @@ -5573,82 +3231,40 @@ struct else Some (expr_of_ptr (z3obj_gc x) q) - (** - Add property about the predicate. - The property is added at level. - *) let add_cover ( x : fixedpoint ) ( level : int ) ( predicate : func_decl ) ( property : expr ) = Z3native.fixedpoint_add_cover (z3obj_gnc x) (z3obj_gno x) level (FuncDecl.gno predicate) (ptr_of_expr property) - (** - Retrieve internal string representation of fixedpoint object. - *) let to_string ( x : fixedpoint ) = Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) 0 [||] - (** - Instrument the Datalog engine on which table representation to use for recursive predicate. - *) let set_predicate_representation ( x : fixedpoint ) ( f : func_decl ) ( kinds : Symbol.symbol array ) = let f2 x = (Symbol.gno x) in Z3native.fixedpoint_set_predicate_representation (z3obj_gnc x) (z3obj_gno x) (FuncDecl.gno f) (Array.length kinds) (Array.map f2 kinds) - (** - Convert benchmark given as set of axioms, rules and queries to a string. - *) let to_string_q ( x : fixedpoint ) ( queries : Boolean.bool_expr array ) = let f x = ptr_of_expr (Boolean.expr_of_bool_expr x) in Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (Array.length queries) (Array.map f queries) - (** - Retrieve set of rules added to fixedpoint context. - *) let get_rules ( x : fixedpoint ) = let v = (AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in let n = (AST.ASTVector.get_size v) in let f i = Boolean.bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in Array.init n f - (** - Retrieve set of assertions added to fixedpoint context. - *) let get_assertions ( x : fixedpoint ) = let v = (AST.ASTVector.ast_vector_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in let n = (AST.ASTVector.get_size v) in let f i = Boolean.bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in Array.init n f - (** - Create a Fixedpoint context. - *) let mk_fixedpoint ( ctx : context ) = create ctx end -(** Global and context options - - Note: This module contains functions that set parameters/options for context - objects as well as functions that set options that are used globally, across - contexts.*) module Options = struct - (** - Update a mutable configuration parameter. - - The list of all configuration parameters can be obtained using the Z3 executable: - z3.exe -ini? - Only a few configuration parameters are mutable once the context is created. - An exception is thrown when trying to modify an immutable parameter. - - *) let update_param_value ( ctx : context ) ( id : string) ( value : string )= Z3native.update_param_value (context_gno ctx) id value - (** - Get a configuration parameter. - - Returns None if the parameter value does not exist. - - *) let get_param_value ( ctx : context ) ( id : string ) = let (r, v) = (Z3native.get_param_value (context_gno ctx) id) in if not r then @@ -5656,62 +3272,21 @@ struct else Some v - (** - 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. - - - - - *) let set_print_mode ( ctx : context ) ( value : ast_print_mode ) = Z3native.set_ast_print_mode (context_gno ctx) (int_of_ast_print_mode value) - (** - Enable/disable printing of warning messages to the console. - - Note that this function is static and effects the behaviour of - all contexts globally. - *) let toggle_warning_messages ( enabled: bool ) = Z3native.toggle_warning_messages enabled end -(** Functions for handling SMT and SMT2 expressions and files *) + module SMT = struct - (** - Convert a benchmark into an SMT-LIB formatted string. - - @param name Name of the benchmark. The argument is optional. - @param logic The benchmark logic. - @param status The status string (sat, unsat, or unknown) - @param attributes Other attributes, such as source, difficulty or category. - @param assumptions Auxiliary assumptions. - @param formula Formula to be checked for consistency in conjunction with assumptions. - @return A string representation of the benchmark. - *) let benchmark_to_smtstring ( ctx : context ) ( name : string ) ( logic : string ) ( status : string ) ( attributes : string ) ( assumptions : Boolean.bool_expr array ) ( formula : Boolean.bool_expr ) = Z3native.benchmark_to_smtlib_string (context_gno ctx) name logic status attributes (Array.length assumptions) (let f x = ptr_of_expr (Boolean.expr_of_bool_expr x) in (Array.map f assumptions)) (Boolean.gno formula) - (** - Parse the given string using the SMT-LIB parser. - - The symbol table of the parser can be initialized using the given sorts and declarations. - The symbols in the arrays and - don't need to match the names of the sorts and declarations in the arrays - and . This is a useful feature since we can use arbitrary names to - reference sorts and declarations. - *) let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in @@ -5728,10 +3303,6 @@ struct (let f x = Symbol.gno x in (Array.map f decl_names)) (let f x = FuncDecl.gno x in (Array.map f decls)) - (** - Parse the given file using the SMT-LIB parser. - - *) let parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in @@ -5748,65 +3319,34 @@ struct (let f x = Symbol.gno x in (Array.map f decl_names)) (let f x = FuncDecl.gno x in (Array.map f decls)) - (** - The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) let get_num_smtlib_formulas ( ctx : context ) = Z3native.get_smtlib_num_formulas (context_gno ctx) - (** - The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) let get_smtlib_formulas ( ctx : context ) = let n = (get_num_smtlib_formulas ctx ) in let f i = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_formula (context_gno ctx) i)) in Array.init n f - - (** - The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) let get_num_smtlib_assumptions ( ctx : context ) = Z3native.get_smtlib_num_assumptions (context_gno ctx) - (** - The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) let get_smtlib_assumptions ( ctx : context ) = let n = (get_num_smtlib_assumptions ctx ) in let f i = Boolean.bool_expr_of_expr (expr_of_ptr ctx (Z3native.get_smtlib_assumption (context_gno ctx) i)) in Array.init n f - (** - The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) let get_num_smtlib_decls ( ctx : context ) = Z3native.get_smtlib_num_decls (context_gno ctx) - (** - The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) let get_smtlib_decls ( ctx : context ) = let n = (get_num_smtlib_decls ctx) in let f i = func_decl_of_ptr ctx (Z3native.get_smtlib_decl (context_gno ctx) i) in Array.init n f - (** - The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) let get_num_smtlib_sorts ( ctx : context ) = Z3native.get_smtlib_num_sorts (context_gno ctx) - - (** - The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - *) + 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 Array.init n f - (** - Parse the given string using the SMT-LIB2 parser. - - - @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. - *) let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in @@ -5823,10 +3363,6 @@ struct (let f x = Symbol.gno x in (Array.map f decl_names)) (let f x = FuncDecl.gno x in (Array.map f decls)))) - (** - Parse the given file using the SMT-LIB2 parser. - - *) let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol array ) ( sorts : sort array ) ( decl_names : Symbol.symbol array ) ( decls : func_decl array ) = let csn = (Array.length sort_names) in let cs = (Array.length sorts) in @@ -5845,34 +3381,9 @@ struct end -(* Global functions *) - -(** - * 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 - * when Z3_params objects are not provided. - * The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. - * The character '.' is a delimiter (more later). - * The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. - * Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". - * This function can be used to set parameters for a specific Z3 module. - * This can be done by using .. - * For example: - * (set_global_param "pp.decimal" "true") - * will set the parameter "decimal" in the module "pp" to true. -*) let set_global_param ( id : string ) ( value : string ) = (Z3native.global_param_set id value) -(** - * 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. - * This function cannot be invoked simultaneously from different threads without synchronization. - * The result string stored in param_value is stored in a shared location. -*) let get_global_param ( id : string ) = let (r, v) = (Z3native.global_param_get id) in if not r then @@ -5880,11 +3391,5 @@ let get_global_param ( id : string ) = else Some v -(** - * Restore the value of all global (and module) parameters. - * - * This command will not affect already created objects (such as tactics and solvers) - * -*) let global_param_reset_all = Z3native.global_param_reset_all diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 87318d2a7..49a78f724 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -5,8 +5,6 @@ @author CM Wintersteiger (cwinter) 2012-12-17 *) - - (** Context objects. Most interactions with Z3 are interpreted in some context; many users will only @@ -39,17 +37,14 @@ val mk_context : (string * string) list -> context module Log : sig (** Open an interaction log file. - @param filename the name of the file to open. - @return True if opening the log file succeeds, false otherwise. - *) + @return True if opening the log file succeeds, false otherwise. *) (* CMW: "open" seems to be a reserved keyword? *) val open_ : string -> bool (** Closes the interaction log. *) val close : unit - (** Appends a user-provided string to the interaction log. - @param s the string to append*) + (** Appends a user-provided string to the interaction log. *) val append : string -> unit end @@ -102,12 +97,10 @@ sig (** A string representation of the symbol. *) val to_string : symbol -> string - (** - Creates a new symbol using an integer. + (** Creates a new symbol using an integer. Not all integers can be passed to this function. - The legal range of unsigned integers is 0 to 2^30-1. - *) + The legal range of unsigned integers is 0 to 2^30-1. *) val mk_int : context -> int -> symbol (** Creates a new symbol using a string. *) @@ -135,30 +128,21 @@ sig (** Retrieves the i-th object in the vector. - @param i Index - @return An AST - *) + @return An AST *) val get : ast_vector -> int -> ast (** Sets the i-th object in the vector. *) val set : ast_vector -> int -> ast -> unit - (** Resize the vector to . - @param newSize The new size of the vector. *) + (** Resize the vector to a new size. *) val resize : ast_vector -> int -> unit - (** - Add the AST to the back of the vector. The size - is increased by 1. - @param a An AST - *) + (** Add an ast to the back of the vector. The size + is increased by 1. *) val push : ast_vector -> ast -> unit - (** - Translates all ASTs in the vector to . - @param to_ctx A context - @return A new ASTVector - *) + (** Translates all ASTs in the vector to another context. + @return A new ASTVector *) val translate : ast_vector -> context -> ast_vector (** Retrieves a string representation of the vector. *) @@ -170,29 +154,18 @@ sig sig type ast_map - (** Checks whether the map contains the key . - @param k An AST - @return True if is a key in the map, false otherwise. *) + (** Checks whether the map contains a key. + @return True if the key in the map, false otherwise. *) val contains : ast_map -> ast -> bool - (** Finds the value associated with the key . - - This function signs an error when is not a key in the map. - @param k An AST - *) + (** Finds the value associated with the key. + This function signs an error when the key is not a key in the map. *) val find : ast_map -> ast -> ast - (** - Stores or replaces a new key/value pair in the map. - @param k The key AST - @param v The value AST - *) + (** Stores or replaces a new key/value pair in the map. *) val insert : ast_map -> ast -> ast -> unit - (** - Erases the key from the map. - @param k An AST - *) + (** Erases the key from the map.*) val erase : ast_map -> ast -> unit (** Removes all keys from the map. *) @@ -208,10 +181,8 @@ sig val to_string : ast_map -> string end - (** - The AST's hash code. - @return A hash code - *) + (** The AST's hash code. + @return A hash code *) val get_hash_code : ast -> int (** A unique identifier for the AST (unique among all ASTs). *) @@ -241,56 +212,39 @@ sig (** A string representation of the AST in s-expression notation. *) val to_sexpr : ast -> string - (** - Comparison operator. - @param a An AST - @param b An AST - @return True if and are from the same context - and represent the same sort; false otherwise. - *) + (** Comparison operator. + @return True if the two ast's are from the same context + and represent the same sort; false otherwise. *) val ( = ) : ast -> ast -> bool - (** - Object Comparison. - @param other Another ast - @return Negative if the object should be sorted before , positive if after else zero. - *) + (** Object Comparison. + @return Negative if the first ast should be sorted before the second, positive if after else zero. *) val compare : ast -> ast -> int (** Operator < *) val ( < ) : ast -> ast -> int - (** - Translates (copies) the AST to the Context . - @param ctx A context - @return A copy of the AST which is associated with - *) + (** Translates (copies) the AST to another context. + @return A copy of the AST which is associated with the other context. *) val translate : ast -> context -> ast - (** - Wraps an AST. + (** Wraps an AST. - This function is used for transitions between native and - managed objects. Note that must be a - native object obtained from Z3 (e.g., through ) + 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., - . - - @param nativeObject The native pointer to wrap. - *) - val wrap : context -> Z3native.z3_ast -> ast + Z3native.inc_ref). *) + val wrap_ast : context -> Z3native.z3_ast -> ast - (** - Unwraps an AST. - This function is used for transitions between native and + (** 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., - ). - - @param a The AST to unwrap. - *) + Z3native.inc_ref). + {!wrap_ast} *) val unwrap_ast : ast -> Z3native.ptr end @@ -307,13 +261,9 @@ sig val sort_of_uninterpreted_sort : uninterpreted_sort -> sort val uninterpreted_sort_of_sort : sort -> uninterpreted_sort - (** - Comparison operator. - @param a A sort - @param b A sort - @return True if and are from the same context - and represent the same sort; false otherwise. - *) + (** Comparison operator. + @return True if the two sorts are from the same context + and represent the same sort; false otherwise. *) val ( = ) : sort -> sort -> bool (** Returns a unique identifier for the sort. *) @@ -385,9 +335,7 @@ sig (** Creates a new function declaration. *) val mk_func_decl_s : context -> string -> Sort.sort array -> Sort.sort -> func_decl - (** Creates a fresh function declaration with a name prefixed with . - - *) + (** Creates a fresh function declaration with a name prefixed with a prefix string. *) val mk_fresh_func_decl : context -> string -> Sort.sort array -> Sort.sort -> func_decl @@ -397,16 +345,13 @@ sig (** Creates a new constant function declaration. *) val mk_const_decl_s : context -> string -> Sort.sort -> func_decl - (** Creates a fresh constant function declaration with a name prefixed with . - - *) + (** Creates a fresh constant function declaration with a name prefixed with a prefix string. + {!mk_func_decl} + {!mk_func_decl} *) val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl (** Comparison operator. - @param a A func_decl - @param b A func_decl - @return True if and 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 (** A string representations of the function declaration. *) @@ -419,7 +364,7 @@ sig val get_arity : func_decl -> int (** The size of the domain of the function declaration - *) + {!get_arity} *) val get_domain_size : func_decl -> int (** The domain of the function declaration *) @@ -440,8 +385,7 @@ sig (** The parameters of the function declaration *) val get_parameters : func_decl -> Parameter.parameter list - (** Create expression that applies function to arguments. - @param args The arguments *) + (** Create expression that applies function to arguments. *) val apply : func_decl -> Expr.expr array -> Expr.expr end @@ -504,54 +448,153 @@ sig val to_string : params -> string end +(** General Expressions (terms) *) and Expr : sig - (** General Expressions (Terms) *) type expr = Expr of AST.ast val ast_of_expr : Expr.expr -> AST.ast val expr_of_ast : AST.ast -> Expr.expr + (** Returns a simplified version of the expression. + {!get_simplify_help} *) val simplify : Expr.expr -> Params.params option -> expr + + (** A string describing all available parameters to Expr.Simplify. *) val get_simplify_help : context -> string + + (** Retrieves parameter descriptions for simplifier. *) val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs + + (** 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 + + (** The arguments of the expression. *) val get_args : Expr.expr -> Expr.expr array + + (** Update the arguments of the expression using an array of expressions. + The number of new arguments should coincide with the current number of arguments. *) val update : Expr.expr -> Expr.expr array -> 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]. *) val substitute : Expr.expr -> Expr.expr array -> Expr.expr array -> expr + + (** Substitute every occurrence of from in the expression with to. + {!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]. *) val substitute_vars : Expr.expr -> Expr.expr array -> expr + + (** Translates (copies) the term to another 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. *) val to_string : Expr.expr -> string + + (** Indicates whether the term is a numeral *) val is_numeral : Expr.expr -> bool + + (** Indicates whether the term is well-sorted. + @return True if the term is well-sorted, false otherwise. *) val is_well_sorted : Expr.expr -> bool + + (** 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 + + (** Indicates whether the term is the constant true. *) val is_true : Expr.expr -> bool + + (** Indicates whether the term is the constant false. *) val is_false : Expr.expr -> bool + + (** Indicates whether the term is an equality predicate. *) val is_eq : Expr.expr -> bool + + (** Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). *) val is_distinct : Expr.expr -> bool + + (** Indicates whether the term is a ternary if-then-else term *) val is_ite : Expr.expr -> bool + + (** Indicates whether the term is an n-ary conjunction *) val is_and : Expr.expr -> bool + + (** Indicates whether the term is an n-ary disjunction *) val is_or : Expr.expr -> bool + + (** Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) *) val is_iff : Expr.expr -> bool + + (** Indicates whether the term is an exclusive or *) val is_xor : Expr.expr -> bool + + (** Indicates whether the term is a negation *) val is_not : Expr.expr -> bool + + (** Indicates whether the term is an implication *) 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. + 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 array -> 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 type bool_sort = BoolSort of Sort.sort @@ -562,23 +605,53 @@ sig val bool_sort_of_sort : Sort.sort -> bool_sort val bool_expr_of_expr : Expr.expr -> bool_expr + (** Create a Boolean sort *) val mk_sort : context -> bool_sort + + (** Create a Boolean constant. *) val mk_const : context -> Symbol.symbol -> bool_expr + + (** Create a Boolean constant. *) val mk_const_s : context -> string -> bool_expr + + (** The true Term. *) val mk_true : context -> bool_expr + + (** The false Term. *) val mk_false : context -> bool_expr + + (** Creates a Boolean value. *) val mk_val : context -> bool -> bool_expr + + (** Creates the equality between two expr's. *) val mk_eq : context -> Expr.expr -> Expr.expr -> bool_expr + + (** Creates a distinct term. *) val mk_distinct : context -> Expr.expr array -> bool_expr + + (** Mk an expression representing not(a). *) val mk_not : context -> bool_expr -> bool_expr + + (** Create an expression representing an if-then-else: ite(t1, t2, t3). *) val mk_ite : context -> bool_expr -> bool_expr -> bool_expr -> bool_expr + + (** Create an expression representing t1 iff t2. *) val mk_iff : context -> bool_expr -> bool_expr -> bool_expr + + (** Create an expression representing t1 -> t2. *) val mk_implies : context -> bool_expr -> bool_expr -> bool_expr + + (** Create an expression representing t1 xor t2. *) val mk_xor : context -> bool_expr -> bool_expr -> bool_expr + + (** Create an expression representing the AND of args *) val mk_and : context -> bool_expr array -> bool_expr + + (** Create an expression representing the OR of args *) val mk_or : context -> bool_expr array -> bool_expr end +(** Quantifier expressions *) module Quantifier : sig type quantifier = Quantifier of Expr.expr @@ -586,7 +659,11 @@ sig val expr_of_quantifier : quantifier -> Expr.expr val quantifier_of_expr : Expr.expr -> quantifier + (** Quantifier patterns + Patterns comprise a list of terms. The list should be + non-empty. If the list comprises of more than one term, it is + also called a multi-pattern. *) module Pattern : sig type pattern = Pattern of AST.ast @@ -594,65 +671,94 @@ sig val ast_of_pattern : pattern -> AST.ast val pattern_of_ast : AST.ast -> pattern + (** The number of terms in the pattern. *) val get_num_terms : pattern -> int + + (** The terms in the pattern. *) val get_terms : pattern -> Expr.expr array + + (** A string representation of the pattern. *) val to_string : pattern -> string end + + (** 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. *) val get_index : Expr.expr -> int + + (** Indicates whether the quantifier is universal. *) val is_universal : quantifier -> bool + + (** Indicates whether the quantifier is existential. *) val is_existential : quantifier -> bool + + (** The weight of the quantifier. *) val get_weight : quantifier -> int + + (** The number of patterns. *) val get_num_patterns : quantifier -> int + + (** The patterns. *) val get_patterns : quantifier -> Pattern.pattern array + + (** The number of no-patterns. *) val get_num_no_patterns : quantifier -> int + + (** The no-patterns. *) val get_no_patterns : quantifier -> Pattern.pattern array - val get_num_bound : quantifier -> int + + (** 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 array + + (** The sorts of the bound variables. *) val get_bound_variable_sorts : quantifier -> Sort.sort array + + (** The body of the quantifier. *) val get_body : quantifier -> Boolean.bool_expr + + (** Creates a new bound variable. *) val mk_bound : context -> int -> Sort.sort -> Expr.expr + + (** Create a quantifier pattern. *) val mk_pattern : context -> Expr.expr array -> Pattern.pattern - val mk_forall : - context -> - Sort.sort array -> - Symbol.symbol array -> - Expr.expr -> - int option -> - Pattern.pattern array -> - Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier - val mk_forall_const : - context -> - Expr.expr array -> - Expr.expr -> - int option -> - Pattern.pattern array -> - Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier - val mk_exists : - context -> - Sort.sort array -> - Symbol.symbol array -> - Expr.expr -> - int option -> - Pattern.pattern array -> - Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier - val mk_exists_const : - context -> - Expr.expr array -> - Expr.expr -> - int option -> - Pattern.pattern array -> - Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier - val mk_quantifier : - context -> - bool -> - Expr.expr array -> - Expr.expr -> - int option -> - Pattern.pattern array -> - Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier + + (** Create a universal Quantifier. *) + val mk_forall : context -> Sort.sort array -> Symbol.symbol array -> Expr.expr -> int option -> Pattern.pattern array -> Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier + + (** Create a universal Quantifier. *) + val mk_forall_const : context -> Expr.expr array -> Expr.expr -> int option -> Pattern.pattern array -> Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier + + (** Create an existential Quantifier. *) + val mk_exists : context -> Sort.sort array -> Symbol.symbol array -> Expr.expr -> int option -> Pattern.pattern array -> Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier + + (** Create an existential Quantifier. *) + val mk_exists_const : context -> Expr.expr array -> Expr.expr -> int option -> Pattern.pattern array -> Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier + + (** Create a Quantifier. *) + val mk_quantifier : context -> Sort.sort array -> Symbol.symbol array -> Expr.expr -> int option -> Pattern.pattern array -> Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier + + (** Create a Quantifier. *) + val mk_quantifier : context -> bool -> Expr.expr array -> Expr.expr -> int option -> Pattern.pattern array -> Expr.expr array -> Symbol.symbol option -> Symbol.symbol option -> quantifier end +(** Functions to manipulate Array expressions *) module Array_ : sig type array_sort = ArraySort of Sort.sort @@ -664,48 +770,159 @@ sig val array_expr_of_expr : Expr.expr -> array_expr + (** Create a new array sort. *) val mk_sort : context -> Sort.sort -> Sort.sort -> array_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. *) 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. *) 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. *) 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. *) 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. *) val is_as_array : Expr.expr -> bool + + (** Indicates whether the term is of an array sort. *) val is_array : Expr.expr -> bool + + (** The domain of the array sort. *) val get_domain : array_sort -> Sort.sort + + (** The range of the array sort. *) val get_range : array_sort -> Sort.sort + + (** Create an array constant. *) val mk_const : context -> Symbol.symbol -> Sort.sort -> Sort.sort -> array_expr + + (** Create an array constant. *) val mk_const_s : context -> string -> Sort.sort -> Sort.sort -> array_expr - val mk_select : context -> array_expr -> Expr.expr -> Expr.expr -> array_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. + {!Array_.mk_sort} + {!mk_store} *) + val mk_select : context -> array_expr -> Expr.expr -> array_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). + {!Array_.mk_sort} + {!mk_select} *) + val mk_store : context -> array_expr -> Expr.expr -> Expr.expr -> array_expr + + (** Create a constant array. + + The resulting term is an array, such that a selecton an arbitrary index + produces the value v. + {!Array_.mk_sort} + {!mk_select} *) val mk_const_array : context -> Sort.sort -> Expr.expr -> array_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]. + {!Array_.mk_sort} + {!mk_select} + {!mk_store} *) val mk_map : context -> FuncDecl.func_decl -> array_expr array -> array_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. *) val mk_term_array : context -> array_expr -> array_expr end +(** Functions to manipulate Set expressions *) module Set : sig type set_sort = SetSort of Sort.sort val sort_of_set_sort : set_sort -> Sort.sort - val is_union : Expr.expr -> bool - val is_intersect : Expr.expr -> bool - val is_difference : Expr.expr -> bool - val is_complement : Expr.expr -> bool - val is_subset : Expr.expr -> bool + (** Create a set type. *) val mk_sort : context -> Sort.sort -> set_sort + + (** Indicates whether the term is set union *) + val is_union : Expr.expr -> bool + + (** Indicates whether the term is set intersection *) + val is_intersect : Expr.expr -> bool + + (** Indicates whether the term is set difference *) + val is_difference : Expr.expr -> bool + + (** Indicates whether the term is set complement *) + val is_complement : Expr.expr -> bool + + (** Indicates whether the term is set subset *) + val is_subset : Expr.expr -> bool + + (** Create an empty set. *) val mk_empty : context -> Sort.sort -> Expr.expr + + (** Create the full set. *) val mk_full : context -> Sort.sort -> Expr.expr + + (** Add an element to the set. *) val mk_set_add : context -> Expr.expr -> Expr.expr -> Expr.expr + + (** Remove an element from a set. *) val mk_del : context -> Expr.expr -> Expr.expr -> Expr.expr + + (** Take the union of a list of sets. *) val mk_union : context -> Expr.expr array -> Expr.expr + + (** Take the intersection of a list of sets. *) val mk_intersection : context -> Expr.expr array -> Expr.expr + + (** Take the difference between two sets. *) val mk_difference : context -> Expr.expr -> Expr.expr -> Expr.expr + + (** Take the complement of a set. *) val mk_complement : context -> Expr.expr -> Expr.expr + + (** Check for set membership. *) val mk_membership : context -> Expr.expr -> Expr.expr -> Expr.expr + + (** Check for subsetness of sets. *) val mk_subset : context -> Expr.expr -> Expr.expr -> Expr.expr end +(** Functions to manipulate Finite Domain expressions *) module FiniteDomain : sig type finite_domain_sort = FiniteDomainSort of Sort.sort @@ -713,13 +930,24 @@ sig val sort_of_finite_domain_sort : finite_domain_sort -> Sort.sort val finite_domain_sort_of_sort : Sort.sort -> finite_domain_sort + (** Create a new finite domain sort. *) val mk_sort : context -> Symbol.symbol -> int -> finite_domain_sort + + (** Create a new finite domain sort. *) val mk_sort_s : context -> string -> int -> finite_domain_sort + + (** Indicates whether the term is of an array sort. *) val is_finite_domain : Expr.expr -> bool + + (** Indicates whether the term is a less than predicate over a finite domain. *) val is_lt : Expr.expr -> bool + + (** The size of the finite domain sort. *) val get_size : finite_domain_sort -> int end + +(** Functions to manipulate Relation expressions *) module Relation : sig type relation_sort = RelationSort of Sort.sort @@ -727,24 +955,92 @@ sig val sort_of_relation_sort : relation_sort -> Sort.sort val relation_sort_of_sort : Sort.sort -> relation_sort + (** Indicates whether the term is of a relation sort. *) 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. *) val is_store : Expr.expr -> bool + + (** Indicates whether the term is an empty relation *) val is_empty : Expr.expr -> bool + + (** Indicates whether the term is a test for the emptiness of a relation *) val is_is_empty : Expr.expr -> bool + + (** Indicates whether the term is a relational join *) val is_join : Expr.expr -> bool + + (** Indicates whether the term is the union or convex hull of two relations. + 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. *) 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. *) 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. *) 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. *) 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. *) 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. *) 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. *) val is_clone : Expr.expr -> bool + + (** The arity of the relation sort. *) val get_arity : relation_sort -> int + + (** The sorts of the columns of the relation sort. *) val get_column_sorts : relation_sort -> relation_sort array end +(** Functions to manipulate Datatype expressions *) module Datatype : sig type datatype_sort = DatatypeSort of Sort.sort @@ -755,74 +1051,136 @@ sig val expr_of_datatype_expr : datatype_expr -> Expr.expr val datatype_expr_of_expr : Expr.expr -> datatype_expr + (** Datatype Constructors *) module Constructor : sig - (** Constructors *) type constructor - val get_n : constructor -> int - val constructor_decl : constructor -> FuncDecl.func_decl - val tester_decl : constructor -> FuncDecl.func_decl - val accessor_decls : constructor -> FuncDecl.func_decl array + (** 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 array 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. *) val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol array -> Sort.sort array -> int array -> 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. *) val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol array -> Sort.sort array -> int array -> Constructor.constructor + + (** Create a new datatype sort. *) val mk_sort : context -> Symbol.symbol -> Constructor.constructor array -> datatype_sort + + (** Create a new datatype sort. *) val mk_sort_s : context -> string -> Constructor.constructor array -> datatype_sort + + (** Create mutually recursive datatypes. *) val mk_sorts : context -> Symbol.symbol array -> Constructor.constructor array array -> datatype_sort array + + (** Create mutually recursive data-types. *) val mk_sorts_s : context -> string array -> Constructor.constructor array array -> datatype_sort array + + + (** The number of constructors of the datatype sort. *) val get_num_constructors : datatype_sort -> int + + (** The constructors. *) val get_constructors : datatype_sort -> FuncDecl.func_decl array + + (** The recognizers. *) val get_recognizers : datatype_sort -> FuncDecl.func_decl array + + (** The constructor accessors. *) val get_accessors : datatype_sort -> FuncDecl.func_decl array array end +(** Functions to manipulate Enumeration expressions *) module Enumeration : sig type enum_sort = EnumSort of Sort.sort val sort_of_enum_sort : enum_sort -> Sort.sort + (** Create a new enumeration sort. *) val mk_sort : context -> Symbol.symbol -> Symbol.symbol array -> enum_sort + + (** Create a new enumeration sort. *) val mk_sort_s : context -> string -> string array -> enum_sort + + (** The function declarations of the constants in the enumeration. *) val get_const_decls : enum_sort -> FuncDecl.func_decl array + + (** The test predicates for the constants in the enumeration. *) val get_tester_decls : enum_sort -> FuncDecl.func_decl array end +(** Functions to manipulate List expressions *) module List_ : sig type list_sort = ListSort of Sort.sort val sort_of_list_sort : list_sort -> Sort.sort + (** Create a new list sort. *) val mk_sort : context -> Symbol.symbol -> Sort.sort -> list_sort + + (** Create a new list sort. *) val mk_list_s : context -> string -> Sort.sort -> list_sort + + (** The declaration of the nil function of this list sort. *) val get_nil_decl : list_sort -> FuncDecl.func_decl + + (** The declaration of the isNil function of this list sort. *) val get_is_nil_decl : list_sort -> FuncDecl.func_decl + + (** The declaration of the cons function of this list sort. *) val get_cons_decl : list_sort -> FuncDecl.func_decl + + (** The declaration of the isCons function of this list sort. *) val get_is_cons_decl : list_sort -> FuncDecl.func_decl + + (** The declaration of the head function of this list sort. *) val get_head_decl : list_sort -> FuncDecl.func_decl + + (** The declaration of the tail function of this list sort. *) val get_tail_decl : list_sort -> FuncDecl.func_decl + + (** The empty list. *) val nil : list_sort -> Expr.expr end +(** Functions to manipulate Tuple expressions *) module Tuple : sig type tuple_sort = TupleSort of Sort.sort val sort_of_tuple_sort : tuple_sort -> Sort.sort + (** Create a new tuple sort. *) val mk_sort : context -> Symbol.symbol -> Symbol.symbol array -> Sort.sort array -> tuple_sort + + (** The constructor function of the tuple. *) val get_mk_decl : tuple_sort -> FuncDecl.func_decl + + (** The number of fields in the tuple. *) val get_num_fields : tuple_sort -> int + + (** The field declarations. *) val get_field_decls : tuple_sort -> FuncDecl.func_decl array end +(** Functions to manipulate arithmetic expressions *) module rec Arithmetic : sig type arith_sort = ArithSort of Sort.sort @@ -833,6 +1191,7 @@ sig val expr_of_arith_expr : Arithmetic.arith_expr -> Expr.expr val arith_expr_of_expr : Expr.expr -> Arithmetic.arith_expr + (** Integer Arithmetic *) module rec Integer : sig type int_sort = IntSort of arith_sort @@ -845,20 +1204,59 @@ sig val int_expr_of_int_num : Arithmetic.Integer.int_num -> Arithmetic.Integer.int_expr val int_expr_of_arith_expr : Arithmetic.arith_expr -> Arithmetic.Integer.int_expr val int_num_of_int_expr : Arithmetic.Integer.int_expr -> Arithmetic.Integer.int_num - + + (** Create a new integer sort. *) val mk_sort : context -> int_sort + + (** Retrieve the int value. *) val get_int : int_num -> int + + (** Returns a string representation of the numeral. *) val to_string : int_num -> string + + (** Creates an integer constant. *) val mk_int_const : context -> Symbol.symbol -> int_expr + + (** Creates an integer constant. *) val mk_int_const_s : context -> string -> int_expr + + (** Create an expression representing t1 mod t2. + The arguments must have int type. *) val mk_mod : context -> int_expr -> int_expr -> int_expr + + (** Create an expression representing t1 rem t2. + The arguments must have int type. *) val mk_rem : context -> int_expr -> int_expr -> int_expr + + (** Create an integer numeral. *) val mk_int_numeral_s : context -> string -> int_num + + (** Create an integer numeral. + @return A Term with the given value and sort Integer *) val mk_int_numeral_i : context -> int -> int_num + + (** 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. *) val mk_int2real : context -> int_expr -> Real.real_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. *) val mk_int2bv : context -> int -> int_expr -> BitVector.bitvec_expr end + (** Real Arithmetic *) and Real : sig type real_sort = RealSort of arith_sort @@ -872,20 +1270,52 @@ sig val real_expr_of_arith_expr : Arithmetic.arith_expr -> Arithmetic.Real.real_expr val rat_num_of_real_expr : Arithmetic.Real.real_expr -> Arithmetic.Real.rat_num + (** Create a real sort. *) val mk_sort : context -> real_sort + + (** The numerator of a rational numeral. *) val get_numerator : rat_num -> Integer.int_num + + (** The denominator of a rational numeral. *) val get_denominator : rat_num -> Integer.int_num + + (** Returns a string representation in decimal notation. + The result has at most as many decimal places as indicated by the int argument.*) val to_decimal_string : rat_num -> int -> string + + (** Returns a string representation of the numeral. *) val to_string : rat_num -> string + + (** Creates a real constant. *) val mk_real_const : context -> Symbol.symbol -> real_expr + + (** Creates a real constant. *) val mk_real_const_s : context -> string -> real_expr + + (** Create a real numeral from a fraction. + @return A Term with rational value and sort Real + {!mk_numeral_s} *) val mk_numeral_nd : context -> int -> int -> rat_num + + (** Create a real numeral. + @return A Term with the given value and sort Real *) val mk_numeral_s : context -> string -> rat_num + + (** Create a real numeral. + @return A Term with the given value and sort Real *) val mk_numeral_i : context -> int -> rat_num + + (** Creates an expression that checks whether a real number is an integer. *) val mk_is_integer : context -> real_expr -> Boolean.bool_expr + + (** 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. *) val mk_real2int : context -> real_expr -> Integer.int_expr end + (** Algebraic Numbers *) and AlgebraicNumber : sig type algebraic_num = AlgebraicNum of arith_expr @@ -893,45 +1323,121 @@ sig val arith_expr_of_algebraic_num : Arithmetic.AlgebraicNumber.algebraic_num -> Arithmetic.arith_expr val algebraic_num_of_arith_expr : Arithmetic.arith_expr -> Arithmetic.AlgebraicNumber.algebraic_num + (** Return a upper bound for a given real algebraic number. + The interval isolating the number is smaller than 1/10^precision. + {!is_algebraic_number} + @return A numeral Expr of sort Real *) val to_upper : algebraic_num -> int -> Real.rat_num + + (** Return a lower bound for the given real algebraic number. + The interval isolating the number is smaller than 1/10^precision. + {!is_algebraic_number} + @return A numeral Expr of sort Real *) val to_lower : algebraic_num -> int -> Real.rat_num + + (** Returns a string representation in decimal notation. + The result has at most as many decimal places as the int argument provided.*) val to_decimal_string : algebraic_num -> int -> string + + (** Returns a string representation of the numeral. *) val to_string : algebraic_num -> string end + (** Indicates whether the term is of integer sort. *) val is_int : Expr.expr -> bool + + (** Indicates whether the term is an arithmetic numeral. *) val is_arithmetic_numeral : Expr.expr -> bool + + (** Indicates whether the term is a less-than-or-equal *) val is_le : Expr.expr -> bool + + (** Indicates whether the term is a greater-than-or-equal *) val is_ge : Expr.expr -> bool + + (** Indicates whether the term is a less-than *) val is_lt : Expr.expr -> bool + + (** Indicates whether the term is a greater-than *) val is_gt : Expr.expr -> bool + + (** Indicates whether the term is addition (binary) *) val is_add : Expr.expr -> bool + + (** Indicates whether the term is subtraction (binary) *) val is_sub : Expr.expr -> bool + + (** Indicates whether the term is a unary minus *) val is_uminus : Expr.expr -> bool + + (** Indicates whether the term is multiplication (binary) *) val is_mul : Expr.expr -> bool + + (** Indicates whether the term is division (binary) *) val is_div : Expr.expr -> bool + + (** Indicates whether the term is integer division (binary) *) val is_idiv : Expr.expr -> bool + + (** Indicates whether the term is remainder (binary) *) val is_remainder : Expr.expr -> bool + + (** Indicates whether the term is modulus (binary) *) val is_modulus : Expr.expr -> bool + + (** Indicates whether the term is a coercion of integer to real (unary) *) val is_inttoreal : Expr.expr -> bool + + (** Indicates whether the term is a coercion of real to integer (unary) *) val is_real_to_int : Expr.expr -> bool + + (** Indicates whether the term is a check that tests whether a real is integral (unary) *) val is_real_is_int : Expr.expr -> bool + + (** Indicates whether the term is of sort real. *) val is_real : Expr.expr -> bool + + (** Indicates whether the term is an integer numeral. *) val is_int_numeral : Expr.expr -> bool + + (** Indicates whether the term is a real numeral. *) val is_rat_num : Expr.expr -> bool + + (** Indicates whether the term is an algebraic number *) val is_algebraic_number : Expr.expr -> bool + + (** Create an expression representing t[0] + t[1] + .... *) val mk_add : context -> arith_expr array -> arith_expr + + (** Create an expression representing t[0] * t[1] * .... *) val mk_mul : context -> arith_expr array -> arith_expr + + (** Create an expression representing t[0] - t[1] - .... *) val mk_sub : context -> arith_expr array -> arith_expr + + (** Create an expression representing -t. *) val mk_unary_minus : context -> arith_expr -> arith_expr + + (** Create an expression representing t1 / t2. *) val mk_div : context -> arith_expr -> arith_expr -> arith_expr + + (** Create an expression representing t1 ^ t2. *) val mk_power : context -> arith_expr -> arith_expr -> arith_expr + + (** Create an expression representing t1 < t2 *) val mk_lt : context -> arith_expr -> arith_expr -> Boolean.bool_expr + + (** Create an expression representing t1 <= t2 *) val mk_le : context -> arith_expr -> arith_expr -> Boolean.bool_expr + + (** Create an expression representing t1 > t2 *) val mk_gt : context -> arith_expr -> arith_expr -> Boolean.bool_expr + + (** Create an expression representing t1 >= t2 *) val mk_ge : context -> arith_expr -> arith_expr -> Boolean.bool_expr end +(** Functions to manipulate bit-vector expressions *) and BitVector : sig type bitvec_sort = BitVecSort of Sort.sort @@ -945,280 +1451,1229 @@ sig val bitvec_expr_of_expr : Expr.expr -> BitVector.bitvec_expr val bitvec_num_of_bitvec_expr : BitVector.bitvec_expr -> BitVector.bitvec_num + (** Create a new bit-vector sort. *) val mk_sort : context -> int -> bitvec_sort + + (** Indicates whether the terms is of bit-vector sort. *) val is_bv : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector numeral *) val is_bv_numeral : Expr.expr -> bool + + (** Indicates whether the term is a one-bit bit-vector with value one *) val is_bv_bit1 : Expr.expr -> bool + + (** Indicates whether the term is a one-bit bit-vector with value zero *) val is_bv_bit0 : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector unary minus *) val is_bv_uminus : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector addition (binary) *) val is_bv_add : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector subtraction (binary) *) val is_bv_sub : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector multiplication (binary) *) val is_bv_mul : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector signed division (binary) *) val is_bv_sdiv : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector unsigned division (binary) *) val is_bv_udiv : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector signed remainder (binary) *) val is_bv_SRem : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector unsigned remainder (binary) *) val is_bv_urem : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector signed modulus *) val is_bv_smod : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector signed division by zero *) val is_bv_sdiv0 : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector unsigned division by zero *) val is_bv_udiv0 : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector signed remainder by zero *) val is_bv_srem0 : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector unsigned remainder by zero *) val is_bv_urem0 : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector signed modulus by zero *) val is_bv_smod0 : Expr.expr -> bool + + (** Indicates whether the term is an unsigned bit-vector less-than-or-equal *) val is_bv_ule : Expr.expr -> bool + + (** Indicates whether the term is a signed bit-vector less-than-or-equal *) val is_bv_sle : Expr.expr -> bool + + (** Indicates whether the term is an unsigned bit-vector greater-than-or-equal *) val is_bv_uge : Expr.expr -> bool + + (** Indicates whether the term is a signed bit-vector greater-than-or-equal *) val is_bv_sge : Expr.expr -> bool + + (** Indicates whether the term is an unsigned bit-vector less-than *) val is_bv_ult : Expr.expr -> bool + + (** Indicates whether the term is a signed bit-vector less-than *) val is_bv_slt : Expr.expr -> bool + + (** Indicates whether the term is an unsigned bit-vector greater-than *) val is_bv_ugt : Expr.expr -> bool + + (** Indicates whether the term is a signed bit-vector greater-than *) val is_bv_sgt : Expr.expr -> bool + + (** Indicates whether the term is a bit-wise AND *) val is_bv_and : Expr.expr -> bool + + (** Indicates whether the term is a bit-wise OR *) val is_bv_or : Expr.expr -> bool + + (** Indicates whether the term is a bit-wise NOT *) val is_bv_not : Expr.expr -> bool + + (** Indicates whether the term is a bit-wise XOR *) val is_bv_xor : Expr.expr -> bool + + (** Indicates whether the term is a bit-wise NAND *) val is_bv_nand : Expr.expr -> bool + + (** Indicates whether the term is a bit-wise NOR *) val is_bv_nor : Expr.expr -> bool + + (** Indicates whether the term is a bit-wise XNOR *) val is_bv_xnor : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector concatenation (binary) *) val is_bv_concat : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector sign extension *) val is_bv_signextension : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector zero extension *) val is_bv_zeroextension : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector extraction *) val is_bv_extract : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector repetition *) val is_bv_repeat : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector reduce OR *) val is_bv_reduceor : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector reduce AND *) val is_bv_reduceand : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector comparison *) val is_bv_comp : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector shift left *) val is_bv_shiftleft : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector logical shift right *) val is_bv_shiftrightlogical : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector arithmetic shift left *) val is_bv_shiftrightarithmetic : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector rotate left *) val is_bv_rotateleft : Expr.expr -> bool + + (** Indicates whether the term is a bit-vector rotate right *) 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. *) 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. *) 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. *) + + (** 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. *) 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. *) 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))) *) 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) *) val is_bv_xor3 : Expr.expr -> bool + + (** The size of a bit-vector sort. *) val get_size : bitvec_sort -> int + + (** Retrieve the int value. *) val get_int : bitvec_num -> int + + (** Returns a string representation of the numeral. *) val to_string : bitvec_num -> string + + (** Creates a bit-vector constant. *) val mk_const : context -> Symbol.symbol -> int -> bitvec_expr + + (** Creates a bit-vector constant. *) val mk_const_s : context -> string -> int -> bitvec_expr + + (** Bitwise negation. + The argument must have a bit-vector sort. *) val mk_not : context -> bitvec_expr -> Expr.expr + + (** Take conjunction of bits in a vector,vector of length 1. + The argument must have a bit-vector sort. *) val mk_redand : context -> bitvec_expr -> Expr.expr + + (** Take disjunction of bits in a vector,vector of length 1. + The argument must have a bit-vector sort. *) val mk_redor : context -> bitvec_expr -> Expr.expr + + (** Bitwise conjunction. + The arguments must have a bit-vector sort. *) val mk_and : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Bitwise disjunction. + The arguments must have a bit-vector sort. *) val mk_or : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Bitwise XOR. + The arguments must have a bit-vector sort. *) val mk_xor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Bitwise NAND. + The arguments must have a bit-vector sort. *) val mk_nand : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Bitwise NOR. + The arguments must have a bit-vector sort. *) val mk_nor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Bitwise XNOR. + The arguments must have a bit-vector sort. *) val mk_xnor : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Standard two's complement unary minus. + The arguments must have a bit-vector sort. *) val mk_neg : context -> bitvec_expr -> bitvec_expr + + (** Two's complement addition. + The arguments must have the same bit-vector sort. *) val mk_add : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Two's complement subtraction. + The arguments must have the same bit-vector sort. *) val mk_sub : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Two's complement multiplication. + The arguments must have the same bit-vector sort. *) val mk_mul : context -> bitvec_expr -> bitvec_expr -> bitvec_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. *) val mk_udiv : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Signed division. + + 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 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. *) val mk_sdiv : context -> bitvec_expr -> bitvec_expr -> bitvec_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. *) val mk_urem : context -> bitvec_expr -> bitvec_expr -> bitvec_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. + + If t2 is zero, then the result is undefined. + The arguments must have the same bit-vector sort. *) val mk_srem : context -> bitvec_expr -> bitvec_expr -> bitvec_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. *) val mk_smod : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Unsigned less-than + + The arguments must have the same bit-vector sort. *) val mk_ult : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Two's complement signed less-than + + The arguments must have the same bit-vector sort. *) val mk_slt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Unsigned less-than or equal to. + + The arguments must have the same bit-vector sort. *) val mk_ule : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Two's complement signed less-than or equal to. + + The arguments must have the same bit-vector sort. *) val mk_sle : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Unsigned greater than or equal to. + + The arguments must have the same bit-vector sort. *) val mk_uge : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Two's complement signed greater than or equal to. + + The arguments must have the same bit-vector sort. *) val mk_sge : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Unsigned greater-than. + + The arguments must have the same bit-vector sort. *) val mk_ugt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Two's complement signed greater-than. + + The arguments must have the same bit-vector sort. *) val mk_sgt : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_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). *) val mk_concat : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Bit-vector extraction. + + Extract the bits between two limits from a bitvector of + size m to yield a new bitvector of size n, where + n = high - low + 1. *) val mk_extract : context -> int -> int -> bitvec_expr -> bitvec_expr + + (** 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. *) val mk_sign_ext : context -> int -> bitvec_expr -> bitvec_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. *) val mk_zero_ext : context -> int -> bitvec_expr -> bitvec_expr + + (** Bit-vector repetition. *) val mk_repeat : context -> int -> bitvec_expr -> bitvec_expr + + (** Shift left. + + It is equivalent to multiplication by 2^x where \c x is the value of 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.*) val mk_shl : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Logical shift right + + 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. + + The arguments must have a bit-vector sort. *) val mk_lshr : context -> bitvec_expr -> bitvec_expr -> bitvec_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. + + 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. *) val mk_ashr : context -> bitvec_expr -> bitvec_expr -> bitvec_expr - val mk_rotate_left : context -> bitvec_expr -> bitvec_expr -> bitvec_expr - val mk_rotate_right : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Rotate Left. + Rotate bits of \c t to the left \c i times. *) + val mk_rotate_left : context -> int -> bitvec_expr -> bitvec_expr + + (** Rotate Right. + Rotate bits of \c t to the right \c i times.*) + val mk_rotate_right : context -> int -> bitvec_expr -> bitvec_expr + + (** Rotate Left. + Rotate bits of the second argument to the left.*) + val mk_ext_rotate_left : context -> bitvec_expr -> bitvec_expr -> bitvec_expr + + (** Rotate Right. + Rotate bits of the second argument to the right. *) + val mk_ext_rotate_right : context -> bitvec_expr -> bitvec_expr -> bitvec_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. + If \c is_signed is true, \c t1 is treated as a signed bit-vector. + + 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.*) val mk_bv2int : context -> bitvec_expr -> bool -> Arithmetic.Integer.int_expr + + (** Create a predicate that checks that the bit-wise addition does not overflow. + + The arguments must be of bit-vector sort. *) val mk_add_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr + + (** Create a predicate that checks that the bit-wise addition does not underflow. + + The arguments must be of bit-vector sort. *) val mk_add_no_underflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Create a predicate that checks that the bit-wise subtraction does not overflow. + + The arguments must be of bit-vector sort. *) val mk_sub_no_overflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Create a predicate that checks that the bit-wise subtraction does not underflow. + + The arguments must be of bit-vector sort. *) val mk_sub_no_underflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_expr + + (** Create a predicate that checks that the bit-wise signed division does not overflow. + + The arguments must be of bit-vector sort. *) val mk_sdiv_no_overflow : context -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Create a predicate that checks that the bit-wise negation does not overflow. + + The arguments must be of bit-vector sort. *) val mk_neg_no_overflow : context -> bitvec_expr -> Boolean.bool_expr + + (** Create a predicate that checks that the bit-wise multiplication does not overflow. + + The arguments must be of bit-vector sort. *) val mk_mul_no_overflow : context -> bitvec_expr -> bitvec_expr -> bool -> Boolean.bool_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 -> bitvec_expr -> bitvec_expr -> Boolean.bool_expr + + (** Create a bit-vector numeral. *) val mk_numeral : context -> string -> int -> bitvec_num end +(** Functions to manipulate proof expressions *) module Proof : sig + (** Indicates whether the term is a Proof for the expression 'true'. *) val is_true : Expr.expr -> bool + + (** Indicates whether the term is a proof for a fact asserted by the user. *) val is_asserted : Expr.expr -> bool + + (** 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 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). *) 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'. *) 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. *) 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) *) 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. *) 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. *) 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)) *) 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. *) 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 *) 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) *) 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) *) 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) *) 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. *) 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 *) 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 *) 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. *) 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. *) 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)) *) val is_quant_inst : Expr.expr -> bool + + (** Indicates whether the term is a hypthesis marker. + 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. *) 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') *) 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) *) 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) *) 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. *) 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). *) 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) *) 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. *) val is_apply_def : Expr.expr -> bool + + (** Indicates whether the term is a proof iff-oeq + + 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'. *) 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'))) *) 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. *) 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. *) 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. *) 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 *) 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. *) val is_theory_lemma : Expr.expr -> bool end +(** Goals + A goal (aka problem). A goal is essentially a + of formulas, that can be solved and/or transformed using + tactics and solvers. *) module Goal : sig type goal + (** The precision of the goal. + + Goals can be transformed using over and under approximations. + An under approximation is applied when the objective is to find a model for a given goal. + An over approximation is applied when the objective is to find a proof for a given goal. *) val get_precision : goal -> Z3enums.goal_prec + + (** Indicates whether the goal is precise. *) val is_precise : goal -> bool + + (** Indicates whether the goal is an under-approximation. *) val is_underapproximation : goal -> bool + + (** Indicates whether the goal is an over-approximation. *) val is_overapproximation : goal -> bool + + (** 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. *) val assert_ : goal -> Boolean.bool_expr array -> 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 + + (** Erases all formulas from the given goal. *) val reset : goal -> unit + + (** The number of formulas in the goal. *) val get_size : goal -> int + + (** The formulas in the goal. *) val get_formulas : goal -> Boolean.bool_expr array + + (** The number of formulas, subformulas and terms in the goal. *) val get_num_exprs : goal -> int + + (** Indicates whether the goal is empty, and it is precise or the product of an under approximation. *) val is_decided_sat : goal -> bool + + (** Indicates whether the goal contains `false', and it is precise or the product of an over approximation. *) val is_decided_unsat : goal -> bool + + (** Translates (copies) the Goal to another context.. *) val translate : goal -> context -> goal + + (** Simplifies the goal. Essentially invokes the `simplify' tactic on the goal. *) 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 + + (** A string representation of the Goal. *) val to_string : goal -> string end +(** Models + + A Model contains interpretations (assignments) of constants and functions. *) module Model : sig type model + (** Function interpretations + + A function interpretation is represented as a finite map and an 'else'. + Each entry in the finite map represents the value of a function given a set of arguments. *) module FuncInterp : sig type func_interp - + + (** Function interpretations entries + + An Entry object represents an element in the finite map used to a function interpretation. *) module FuncEntry : sig type func_entry - + + (** Return the (symbolic) value of this entry. + *) val get_value : func_entry -> Expr.expr + + (** The number of arguments of the entry. + *) val get_num_args : func_entry -> int + + (** The arguments of the function entry. + *) val get_args : func_entry -> Expr.expr array + + (** A string representation of the function entry. + *) val to_string : func_entry -> string end + (** The number of entries in the function interpretation. *) val get_num_entries : func_interp -> int + + (** The entries in the function interpretation *) val get_entries : func_interp -> FuncEntry.func_entry array + + (** The (symbolic) `else' value of the function interpretation. *) val get_else : func_interp -> Expr.expr + + (** The arity of the function interpretation *) val get_arity : func_interp -> int + + (** A string representation of the function interpretation. *) val to_string : func_interp -> string end + (** Retrieves the interpretation (the assignment) of a func_decl in the model. + An expression if the function has an interpretation in the model, null otherwise. *) val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option + + (** Retrieves the interpretation (the assignment) of an expression in the model. + An expression if the constant has an interpretation in the model, null otherwise. *) val get_const_interp_e : model -> Expr.expr -> Expr.expr option + + (** Retrieves the interpretation (the assignment) of a non-constant func_decl in the model. + A FunctionInterpretation if the function has an interpretation in the model, null otherwise. *) val get_func_interp : model -> FuncDecl.func_decl -> FuncInterp.func_interp option + + (** The number of constant interpretations in the model. *) val get_num_consts : model -> int + + (** The function declarations of the constants in the model. *) val get_const_decls : model -> FuncDecl.func_decl array + + (** The number of function interpretations in the model. *) val get_num_funcs : model -> int + + (** The function declarations of the function interpretations in the model. *) val get_func_decls : model -> FuncDecl.func_decl array + + (** All symbols that have an interpretation in the model. *) val get_decls : model -> FuncDecl.func_decl array + + (** A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. *) exception ModelEvaluationFailedException of string + + (** Evaluates an expression in the current model. + + This function may fail if the argument contains quantifiers, + is partial (MODEL_PARTIAL enabled), or if it is not well-sorted. + In this case a ModelEvaluationFailedException is thrown. + *) val eval : model -> Expr.expr -> bool -> Expr.expr + + (** Alias for eval. *) val evaluate : model -> Expr.expr -> bool -> Expr.expr + + (** The number of uninterpreted sorts that the model has an interpretation for. *) val get_num_sorts : model -> int + + (** The uninterpreted sorts that the model has an interpretation for. + + Z3 also provides an intepretation for uninterpreted sorts used in a formula. + The interpretation for a sort is a finite set of distinct values. We say this finite set is + the "universe" of the sort. + {!get_num_sorts} + {!sort_universe} *) val get_sorts : model -> Sort.sort array + + (** The finite set of distinct values that represent the interpretation of a sort. + {!get_sorts} + @returns An array of expressions, where each is an element of the universe of the sort *) val sort_universe : model -> Sort.sort -> AST.ASTVector.ast_vector array + + (** Conversion of models to strings. + A string representation of the model. *) val to_string : model -> string 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 Context.NumProbes + and Context.ProbeNames. + It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. +*) module Probe : sig type probe + (** Execute the probe over the goal. + A probe always produce a double 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. *) val get_num_probes : context -> int + + (** The names of all supported Probes. *) val get_probe_names : context -> string array + + (** Returns a string containing a description of the probe with the given name. *) val get_probe_description : context -> string -> string + + (** Creates a new Probe. *) val mk_probe : context -> string -> probe + + (** Create a probe that always evaluates to a float value. *) val const : context -> float -> probe + + (** Create a probe that evaluates to "true" when the value returned by the first argument + is less than the value returned by second argument *) val lt : context -> probe -> probe -> probe + + (** Create a probe that evaluates to "true" when the value returned by the first argument + is greater than the value returned by second argument *) val gt : context -> probe -> probe -> probe + + (** Create a probe that evaluates to "true" when the value returned by the first argument + is less than or equal the value returned by second argument *) val le : context -> probe -> probe -> probe + + (** Create a probe that evaluates to "true" when the value returned by the first argument + is greater than or equal the value returned by second argument *) val ge : context -> probe -> probe -> probe + + + (** Create a probe that evaluates to "true" when the value returned by the first argument + is equal the value returned by second argument *) val eq : context -> probe -> probe -> probe + + (** Create a probe that evaluates to "true" when both of two probes evaluate to "true". *) val and_ : context -> probe -> probe -> probe + + (** Create a probe that evaluates to "true" when either of two probes evaluates to "true". *) val or_ : context -> probe -> probe -> probe + + (** Create a probe that evaluates to "true" when another probe does not evaluate to "true". *) val not_ : context -> probe -> probe end +(** Tactics + + Tactics are the basic building block for creating custom solvers for specific problem domains. + The complete list of tactics may be obtained using Context.get_num_tactics + and Context.get_tactic_names. + It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. +*) module Tactic : sig type tactic + (** Tactic application results + + ApplyResult objects represent the result of an application of a + tactic to a goal. It contains the subgoals that were produced. *) module ApplyResult : sig type apply_result + (** The number of Subgoals. *) val get_num_subgoals : apply_result -> int + + (** Retrieves the subgoals from the apply_result. *) val get_subgoals : apply_result -> Goal.goal array + + (** Retrieves a subgoal from the apply_result. *) val get_subgoal : apply_result -> int -> Goal.goal + + (** Convert a model for a subgoal into a model for the original + goal g, that the ApplyResult was obtained from. + #return A model for g *) val convert_model : apply_result -> int -> Model.model -> Model.model + + (** A string representation of the ApplyResult. *) val to_string : apply_result -> string end + (** A string containing a description of parameters accepted by the tactic. *) val get_help : tactic -> string + + (** Retrieves parameter descriptions for Tactics. *) val get_param_descrs : tactic -> Params.ParamDescrs.param_descrs + + (** Apply the tactic to the goal. *) val apply : tactic -> Goal.goal -> Params.params option -> ApplyResult.apply_result + + (** The number of supported tactics. *) val get_num_tactics : context -> int + + (** The names of all supported tactics. *) val get_tactic_names : context -> string array + + (** Returns a string containing a description of the tactic with the given name. *) val get_tactic_description : context -> string -> string + + (** Creates a new Tactic. *) 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. *) val and_then : context -> tactic -> tactic -> tactic array -> 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. *) 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. *) 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 + + (** Create a tactic that applies a tactic to a given goal if the probe + evaluates to true and another tactic otherwise. *) 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. *) val repeat : context -> tactic -> int -> tactic + + (** Create a tactic that just returns the given goal. *) val skip : context -> tactic + + (** Create a tactic always fails. *) val fail : context -> tactic + + (** Create a tactic that fails if the probe evaluates to false. *) 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'). *) 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*) val with_ : context -> tactic -> Params.params -> tactic + + (** Create a tactic that applies the given tactics in parallel. *) val par_or : context -> tactic array -> tactic + + (** Create a tactic that applies a tactic to a given goal and then another tactic + to every subgoal produced by the first one. The subgoals are processed in parallel. *) 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. *) val interrupt : context -> unit end +(** Solvers *) module Solver : sig type solver @@ -1226,108 +2681,388 @@ sig val string_of_status : status -> string + (** Objects that track statistical information about solvers. *) module Statistics : sig type statistics + (** Statistical data is organized into pairs of \[Key, Entry\], where every + Entry is either a floating point or integer value. + *) module Entry : sig type statistics_entry + (** The key of the entry. *) val get_key : statistics_entry -> string + + (** The int-value of the entry. *) val get_int : statistics_entry -> int + + (** The float-value of the entry. *) val get_float : statistics_entry -> float + + (** True if the entry is uint-valued. *) val is_int : statistics_entry -> bool + + (** True if the entry is double-valued. *) val is_float : statistics_entry -> bool + + (** 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 + (** A string representation of the statistical data. *) val to_string : statistics -> string + + (** The number of statistical data. *) val get_size : statistics -> int + + (** The data entries. *) val get_entries : statistics -> Entry.statistics_entry array + + (** The statistical counters. *) val get_keys : statistics -> string array + + (** The value of a particular statistical counter. *) val get : statistics -> string -> Entry.statistics_entry option end + (** A string that describes all available solver parameters. *) val get_help : solver -> string + + (** Sets the solver parameters. *) val set_parameters : solver -> Params.params -> unit + + (** Retrieves parameter descriptions for solver. *) val get_param_descrs : solver -> Params.ParamDescrs.param_descrs + + (** The current number of backtracking points (scopes). + {!pop} + {!push} *) val get_num_scopes : solver -> int + + (** Creates a backtracking point. + {!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} *) val pop : solver -> int -> unit + + (** Resets the Solver. + This removes all assertions from the solver. *) val reset : solver -> unit + + (** Assert a constraint (or multiple) into the solver. *) val assert_ : solver -> Boolean.bool_expr array -> 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. *) + val assert_and_track_a : solver -> Boolean.bool_expr array -> Boolean.bool_expr array -> 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. *) val assert_and_track : solver -> Boolean.bool_expr -> Boolean.bool_expr -> unit + + (** The number of assertions in the solver. *) val get_num_assertions : solver -> int + + (** The set of asserted formulas. *) val get_assertions : solver -> Boolean.bool_expr array + + (** Checks whether the assertions in the solver are consistent or not. + + {!Model} + {!get_unsat_core} + {!Proof} *) val check : solver -> Boolean.bool_expr array -> 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. *) 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. *) 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. *) val get_unsat_core : solver -> AST.ASTVector.ast_vector array + + (** A brief justification of why the last call to Check returned UNKNOWN. *) val get_reason_unknown : solver -> string + + (** Solver statistics. *) 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. *) val mk_solver : context -> Symbol.symbol option -> solver + + (** Creates a new (incremental) 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. *) val mk_solver_t : context -> Tactic.tactic -> solver + + (** A string representation of the solver. *) val to_string : solver -> string end +(** Fixedpoint solving *) module Fixedpoint : sig type fixedpoint + (** A string that describes all available fixedpoint solver parameters. *) val get_help : fixedpoint -> string + + (** Sets the fixedpoint solver parameters. *) val set_params : fixedpoint -> Params.params -> unit + + (** Retrieves parameter descriptions for Fixedpoint solver. *) val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs + + (** Assert a constraints into the fixedpoint solver. *) val assert_ : fixedpoint -> Boolean.bool_expr array -> unit + + (** Register predicate as recursive relation. *) val register_relation : fixedpoint -> FuncDecl.func_decl -> unit + + (** Add rule into the fixedpoint solver. *) val add_rule : fixedpoint -> Boolean.bool_expr -> Symbol.symbol option -> unit + + (** Add table fact to the fixedpoint solver. *) val add_fact : fixedpoint -> FuncDecl.func_decl -> int array -> 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. *) val query : fixedpoint -> Boolean.bool_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. *) val query_r : fixedpoint -> FuncDecl.func_decl array -> Solver.status + + (** Creates a backtracking point. + {!pop} *) val push : fixedpoint -> unit + + (** Backtrack one backtracking point. + + 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 -> Boolean.bool_expr -> Symbol.symbol -> unit + + (** Retrieve satisfying instance or instances of solver, + or definitions for the recursive predicates that show unsatisfiability. *) val get_answer : fixedpoint -> Expr.expr option + + (** Retrieve explanation why fixedpoint engine returned status Unknown. *) val get_reason_unknown : fixedpoint -> string + + (** Retrieve the number of levels explored for a given predicate. *) val get_num_levels : fixedpoint -> FuncDecl.func_decl -> int + + (** Retrieve the cover of a predicate. *) val get_cover_delta : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr option + + (** Add property about the predicate. + The property is added at level. *) val add_cover : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr -> unit + + (** Retrieve internal string representation of fixedpoint object. *) val to_string : fixedpoint -> string + + (** Instrument the Datalog engine on which table representation to use for recursive predicate. *) val set_predicate_representation : fixedpoint -> FuncDecl.func_decl -> Symbol.symbol array -> unit + + (** Convert benchmark given as set of axioms, rules and queries to a string. *) val to_string_q : fixedpoint -> Boolean.bool_expr array -> string + + (** Retrieve set of rules added to fixedpoint context. *) val get_rules : fixedpoint -> Boolean.bool_expr array + + (** Retrieve set of assertions added to fixedpoint context. *) val get_assertions : fixedpoint -> Boolean.bool_expr array + + (** Create a Fixedpoint context. *) val mk_fixedpoint : context -> fixedpoint end +(** Global and context options + + Note: This module contains functions that set parameters/options for context + objects as well as functions that set options that are used globally, across + contexts.*) module Options : sig + (** Update a mutable configuration parameter. + + The list of all configuration parameters can be obtained using the Z3 executable: + z3.exe -ini? + 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} *) 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} *) val set_print_mode : context -> Z3enums.ast_print_mode -> unit + + (** Enable/disable printing of warning messages to the console. + + Note that this function is static and effects the behaviour of + all contexts globally. *) val toggle_warning_messages : bool -> unit end +(** Functions for handling SMT and SMT2 expressions and files *) module SMT : sig + (** Convert a benchmark into an SMT-LIB formatted string. + + @return A string representation of the benchmark. *) val benchmark_to_smtstring : context -> string -> string -> string -> string -> Boolean.bool_expr array -> Boolean.bool_expr -> string + + (** Parse the given string using the SMT-LIB parser. + + The symbol table of the parser can be initialized using the given sorts and declarations. + The symbols in the arrays in the third and fifth argument + don't need to match the names of the sorts and declarations in the arrays in the fourth + and sixth argument. This is a useful feature since we can use arbitrary names to + reference sorts and declarations. *) val parse_smtlib_string : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> unit + + (** Parse the given file using the SMT-LIB parser. + {!parse_smtlib_string} *) val parse_smtlib_file : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> unit + + (** The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_num_smtlib_formulas : context -> int + + (** The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_smtlib_formulas : context -> Boolean.bool_expr array + + (** The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_num_smtlib_assumptions : context -> int + + (** The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_smtlib_assumptions : context -> Boolean.bool_expr array + + (** The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_num_smtlib_decls : context -> int + + (** The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_smtlib_decls : context -> FuncDecl.func_decl array + + (** The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_num_smtlib_sorts : context -> int + + (** The sort declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. *) val get_smtlib_sorts : context -> Sort.sort array + + (** 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. *) val parse_smtlib2_string : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> Boolean.bool_expr + + (** Parse the given file using the SMT-LIB2 parser. + {!parse_smtlib2_string} *) val parse_smtlib2_file : context -> string -> Symbol.symbol array -> Sort.sort array -> Symbol.symbol array -> FuncDecl.func_decl array -> Boolean.bool_expr 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 + when Z3_params objects are not provided. + The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. + The character '.' is a delimiter (more later). + The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. + Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". + This function can be used to set parameters for a specific Z3 module. + This can be done by using .. + For example: + (set_global_param "pp.decimal" "true") + will set the parameter "decimal" in the module "pp" to true. +*) 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. + This function cannot be invoked simultaneously from different threads without synchronization. + The result string stored in param_value is stored in a shared location. +*) val get_global_param : string -> string option + +(** Restore the value of all global (and module) parameters. + + This command will not affect already created objects (such as tactics and solvers) + {!set_global_param} +*) val global_param_reset_all : unit