mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity
z3/src/api/ml/z3.mli
Christoph M. Wintersteiger 303b4e6735 ML API savepoint 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 17:08:11 +00:00

3069 lines
112 KiB
OCaml
Raw Blame History

(**
The Z3 ML/Ocaml Interface.
Copyright (C) 2012 Microsoft Corporation
@author CM Wintersteiger (cwinter) 2012-12-17
*)
(** Context objects.
Most interactions with Z3 are interpreted in some context; many users will only
require one such object, but power users may require more than one. To start using
Z3, do
<code>
let ctx = (mk_context []) in
(...)
</code>
where a list of pairs of strings may be passed to set options on
the context, e.g., like so:
<code>
let cfg = [("model", "true"); ("...", "...")] in
let ctx = (mk_context cfg) in
(...)
</code>
*)
type context
(** Create a context object *)
val mk_context : (string * string) list -> context
(** Interaction logging for Z3
Note that this is a global, static log and if multiple Context
objects are created, it logs the interaction with all of them. *)
module Log :
sig
(** Open an interaction log file.
@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. *)
val append : string -> unit
end
(** Version information *)
module Version :
sig
(** The major version. *)
val major : int
(** The minor version. *)
val minor : int
(** The build version. *)
val build : int
(** The revision. *)
val revision : int
(** A string representation of the version information. *)
val to_string : string
end
(** Symbols are used to name several term and type constructors *)
module Symbol :
sig
(** Numbered Symbols *)
type int_symbol
(** Named Symbols *)
type string_symbol
(** Symbols *)
type symbol = S_Int of int_symbol | S_Str of string_symbol
(** The kind of the symbol (int or string) *)
val kind : symbol -> Z3enums.symbol_kind
(** Indicates whether the symbol is of Int kind *)
val is_int_symbol : symbol -> bool
(** Indicates whether the symbol is of string kind. *)
val is_string_symbol : symbol -> bool
(** The int value of the symbol. *)
val get_int : int_symbol -> int
(** The string value of the symbol. *)
val get_string : string_symbol -> string
(** A string representation of the symbol. *)
val to_string : symbol -> string
(** 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. *)
val mk_int : context -> int -> symbol
(** Creates a new symbol using a string. *)
val mk_string : context -> string -> symbol
(** Create an array of symbols. *)
val mk_ints : context -> int array -> symbol array
(** Create an array of symbols. *)
val mk_strings : context -> string array -> symbol array
end
(** The abstract syntax tree (AST) module *)
module AST :
sig
type ast
(** Vectors of ASTs *)
module ASTVector :
sig
type ast_vector
(** The size of the vector *)
val get_size : ast_vector -> int
(**
Retrieves the i-th object in the vector.
@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 a new size. *)
val resize : ast_vector -> int -> unit
(** 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 another context.
@return A new ASTVector *)
val translate : ast_vector -> context -> ast_vector
(** Retrieves a string representation of the vector. *)
val to_string : ast_vector -> string
end
(** Map from AST to AST *)
module ASTMap :
sig
type ast_map
(** 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 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. *)
val insert : ast_map -> ast -> ast -> unit
(** Erases the key from the map.*)
val erase : ast_map -> ast -> unit
(** Removes all keys from the map. *)
val reset : ast_map -> unit
(** The size of the map *)
val get_size : ast_map -> int
(** The keys stored in the map. *)
val get_keys : ast_map -> ASTVector.ast_vector
(** Retrieves a string representation of the map.*)
val to_string : ast_map -> string
end
(** 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). *)
val get_id : ast -> int
(** The kind of the AST. *)
val get_ast_kind : ast -> Z3enums.ast_kind
(** Indicates whether the AST is an Expr *)
val is_expr : ast -> bool
(** Indicates whether the AST is a bound variable*)
val is_var : ast -> bool
(** Indicates whether the AST is a Quantifier *)
val is_quantifier : ast -> bool
(** Indicates whether the AST is a Sort *)
val is_sort : ast -> bool
(** Indicates whether the AST is a func_decl *)
val is_func_decl : ast -> bool
(** A string representation of the AST. *)
val to_string : ast -> string
(** A string representation of the AST in s-expression notation. *)
val to_sexpr : ast -> string
(** 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.
@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 another context.
@return A copy of the AST which is associated with the other context. *)
val translate : ast -> context -> ast
(** Wraps an AST.
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.,
<c>Z3native.inc_ref</c>). *)
val wrap_ast : context -> Z3native.z3_ast -> ast
(** 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.,
<c>Z3native.inc_ref</c>).
{!wrap_ast} *)
val unwrap_ast : ast -> Z3native.ptr
end
(** The Sort module implements type information for ASTs *)
module Sort :
sig
(** Sorts *)
type sort = Sort of AST.ast
(** Uninterpreted Sorts *)
type uninterpreted_sort = UninterpretedSort of sort
val ast_of_sort : sort -> AST.ast
val sort_of_uninterpreted_sort : uninterpreted_sort -> sort
val uninterpreted_sort_of_sort : sort -> uninterpreted_sort
(** 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. *)
val get_id : sort -> int
(** The kind of the sort. *)
val get_sort_kind : sort -> Z3enums.sort_kind
(** The name of the sort *)
val get_name : sort -> Symbol.symbol
(** A string representation of the sort. *)
val to_string : sort -> string
(** Create a new uninterpreted sort. *)
val mk_uninterpreted : context -> Symbol.symbol -> uninterpreted_sort
(** Create a new uninterpreted sort. *)
val mk_uninterpreted_s : context -> string -> uninterpreted_sort
end
(** Function declarations *)
module rec FuncDecl :
sig
type func_decl = FuncDecl of AST.ast
val ast_of_func_decl : FuncDecl.func_decl -> AST.ast
(** Parameters of Func_Decls *)
module Parameter :
sig
(** Parameters of func_decls *)
type parameter =
P_Int of int
| P_Dbl of float
| P_Sym of Symbol.symbol
| P_Srt of Sort.sort
| P_Ast of AST.ast
| P_Fdl of func_decl
| P_Rat of string
(** The kind of the parameter. *)
val get_kind : parameter -> Z3enums.parameter_kind
(** The int value of the parameter.*)
val get_int : parameter -> int
(** The double value of the parameter.*)
val get_float : parameter -> float
(** The Symbol.Symbol value of the parameter.*)
val get_symbol : parameter -> Symbol.symbol
(** The Sort value of the parameter.*)
val get_sort : parameter -> Sort.sort
(** The AST value of the parameter.*)
val get_ast : parameter -> AST.ast
(** The FunctionDeclaration value of the parameter.*)
val get_func_decl : parameter -> func_decl
(** The rational string value of the parameter.*)
val get_rational : parameter -> string
end
(** Creates a new function declaration. *)
val mk_func_decl : context -> Symbol.symbol -> Sort.sort array -> Sort.sort -> func_decl
(** 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 a prefix string. *)
val mk_fresh_func_decl : context -> string -> Sort.sort array -> Sort.sort -> func_decl
(** Creates a new constant function declaration. *)
val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl
(** 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 a prefix string.
{!mk_func_decl}
{!mk_func_decl} *)
val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl
(** Comparison operator.
@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. *)
val to_string : func_decl -> string
(** Returns a unique identifier for the function declaration. *)
val get_id : func_decl -> int
(** The arity of the function declaration *)
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 *)
val get_domain : func_decl -> Sort.sort array
(** The range of the function declaration *)
val get_range : func_decl -> Sort.sort
(** The kind of the function declaration. *)
val get_decl_kind : func_decl -> Z3enums.decl_kind
(** The name of the function declaration*)
val get_name : func_decl -> Symbol.symbol
(** The number of parameters of the function declaration *)
val get_num_parameters : func_decl -> int
(** The parameters of the function declaration *)
val get_parameters : func_decl -> Parameter.parameter list
(** Create expression that applies function to arguments. *)
val apply : func_decl -> Expr.expr array -> Expr.expr
end
(** Parameter sets (of Solvers, Tactics, ...)
A Params objects represents a configuration in the form of Symbol.symbol/value pairs. *)
and Params :
sig
type params
(** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *)
module ParamDescrs :
sig
type param_descrs
(** Validate a set of parameters. *)
val validate : param_descrs -> params -> unit
(** Retrieve kind of parameter. *)
val get_kind : param_descrs -> Symbol.symbol -> Z3enums.param_kind
(** Retrieve all names of parameters. *)
val get_names : param_descrs -> Symbol.symbol array
(** The size of the ParamDescrs. *)
val get_size : param_descrs -> int
(** Retrieves a string representation of the ParamDescrs. *)
val to_string : param_descrs -> string
end
(** Adds a parameter setting. *)
val add_bool : params -> Symbol.symbol -> bool -> unit
(** Adds a parameter setting. *)
val add_int : params -> Symbol.symbol -> int -> unit
(** Adds a parameter setting. *)
val add_double : params -> Symbol.symbol -> float -> unit
(** Adds a parameter setting. *)
val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
(** Adds a parameter setting. *)
val add_s_bool : params -> string -> bool -> unit
(** Adds a parameter setting. *)
val add_s_int : params -> string -> int -> unit
(** Adds a parameter setting. *)
val add_s_double : params -> string -> float -> unit
(** Adds a parameter setting. *)
val add_s_symbol : params -> string -> Symbol.symbol -> unit
(** Creates a new parameter set *)
val mk_params : context -> params
(** A string representation of the parameter set. *)
val to_string : params -> string
end
(** General Expressions (terms) *)
and Expr :
sig
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 <c>Expr.Simplify</c>. *)
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 <c>from[i]</c> in the expression with <c>to[i]</c>, for <c>i</c> smaller than <c>num_exprs</c>.
The result is the new expression. The arrays <c>from</c> and <c>to</c> must have size <c>num_exprs</c>.
For every <c>i</c> smaller than <c>num_exprs</c>, we must have that
sort of <c>from[i]</c> must be equal to sort of <c>to[i]</c>. *)
val substitute : Expr.expr -> Expr.expr array -> Expr.expr array -> expr
(** Substitute every occurrence of <c>from</c> in the expression with <c>to</c>.
{!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 <c>i</c> smaller than <c>num_exprs</c>, the variable with de-Bruijn index <c>i</c> is replaced with term <c>to[i]</c>. *)
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 <c>MakeNumeral</c> since it is not necessary to parse a string.
@return A Term with the given value and sort *)
val mk_numeral_int : context -> int -> Sort.sort -> expr
end
(** Boolean expressions *)
module Boolean :
sig
type bool_sort = BoolSort of Sort.sort
type bool_expr = BoolExpr of Expr.expr
val expr_of_bool_expr : bool_expr -> Expr.expr
val sort_of_bool_sort : bool_sort -> Sort.sort
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 <c>distinct</c> term. *)
val mk_distinct : context -> Expr.expr array -> bool_expr
(** Mk an expression representing <c>not(a)</c>. *)
val mk_not : context -> bool_expr -> bool_expr
(** Create an expression representing an if-then-else: <c>ite(t1, t2, t3)</c>. *)
val mk_ite : context -> bool_expr -> bool_expr -> bool_expr -> bool_expr
(** Create an expression representing <c>t1 iff t2</c>. *)
val mk_iff : context -> bool_expr -> bool_expr -> bool_expr
(** Create an expression representing <c>t1 -> t2</c>. *)
val mk_implies : context -> bool_expr -> bool_expr -> bool_expr
(** Create an expression representing <c>t1 xor t2</c>. *)
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
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
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.
<code>
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))
</code>
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
(** 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
(** 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
type array_expr = ArrayExpr of Expr.expr
val sort_of_array_sort : array_sort -> Sort.sort
val array_sort_of_sort : Sort.sort -> array_sort
val expr_of_array_expr : array_expr -> Expr.expr
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
(** Array read.
The argument <c>a</c> is the array and <c>i</c> is the index
of the array that gets read.
The node <c>a</c> must have an array sort <c>[domain -> range]</c>,
and <c>i</c> must have the sort <c>domain</c>.
The sort of the result is <c>range</c>.
{!Array_.mk_sort}
{!mk_store} *)
val mk_select : context -> array_expr -> Expr.expr -> array_expr
(** Array update.
The node <c>a</c> must have an array sort <c>[domain -> range]</c>,
<c>i</c> must have sort <c>domain</c>,
<c>v</c> must have sort range. The sort of the result is <c>[domain -> range]</c>.
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 <c>a</c>
(with respect to <c>select</c>)
on all indices except for <c>i</c>, where it maps to <c>v</c>
(and the <c>select</c> of <c>a</c> with
respect to <c>i</c> may be a different value).
{!Array_.mk_sort}
{!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 <c>select</c>on an arbitrary index
produces the value <c>v</c>.
{!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 <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
<c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
{!Array_.mk_sort}
{!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
(** 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
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
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 <c>n+1</c> arguments, where the first argument is the relation and the remaining <c>n</c> elements
correspond to the <c>n</c> 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 <c>n+1</c> arguments, where the first argument is a relation,
and the remaining <c>n</c> 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
type datatype_expr = DatatypeExpr of Expr.expr
val sort_of_datatype_sort : datatype_sort -> Sort.sort
val datatype_sort_of_sort : Sort.sort -> datatype_sort
val expr_of_datatype_expr : datatype_expr -> Expr.expr
val datatype_expr_of_expr : Expr.expr -> datatype_expr
(** Datatype Constructors *)
module Constructor :
sig
type constructor
(** 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
type arith_expr = ArithExpr of Expr.expr
val sort_of_arith_sort : Arithmetic.arith_sort -> Sort.sort
val arith_sort_of_sort : Sort.sort -> Arithmetic.arith_sort
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
type int_expr = IntExpr of arith_expr
type int_num = IntNum of int_expr
val arith_sort_of_int_sort : Arithmetic.Integer.int_sort -> Arithmetic.arith_sort
val int_sort_of_arith_sort : Arithmetic.arith_sort -> Arithmetic.Integer.int_sort
val arith_expr_of_int_expr : Arithmetic.Integer.int_expr -> Arithmetic.arith_expr
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 <c>t1 mod t2</c>.
The arguments must have int type. *)
val mk_mod : context -> int_expr -> int_expr -> int_expr
(** Create an expression representing <c>t1 rem t2</c>.
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 <c>k</c> and
and asserting <c>MakeInt2Real(k) <= t1 < MkInt2Real(k)+1</c>.
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
type real_expr = RealExpr of arith_expr
type rat_num = RatNum of real_expr
val arith_sort_of_real_sort : Arithmetic.Real.real_sort -> Arithmetic.arith_sort
val real_sort_of_arith_sort : Arithmetic.arith_sort -> Arithmetic.Real.real_sort
val arith_expr_of_real_expr : Arithmetic.Real.real_expr -> Arithmetic.arith_expr
val real_expr_of_rat_num : Arithmetic.Real.rat_num -> Arithmetic.Real.real_expr
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
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 <c>t[0] + t[1] + ...</c>. *)
val mk_add : context -> arith_expr array -> arith_expr
(** Create an expression representing <c>t[0] * t[1] * ...</c>. *)
val mk_mul : context -> arith_expr array -> arith_expr
(** Create an expression representing <c>t[0] - t[1] - ...</c>. *)
val mk_sub : context -> arith_expr array -> arith_expr
(** Create an expression representing <c>-t</c>. *)
val mk_unary_minus : context -> arith_expr -> arith_expr
(** Create an expression representing <c>t1 / t2</c>. *)
val mk_div : context -> arith_expr -> arith_expr -> arith_expr
(** Create an expression representing <c>t1 ^ t2</c>. *)
val mk_power : context -> arith_expr -> arith_expr -> arith_expr
(** Create an expression representing <c>t1 < t2</c> *)
val mk_lt : context -> arith_expr -> arith_expr -> Boolean.bool_expr
(** Create an expression representing <c>t1 <= t2</c> *)
val mk_le : context -> arith_expr -> arith_expr -> Boolean.bool_expr
(** Create an expression representing <c>t1 > t2</c> *)
val mk_gt : context -> arith_expr -> arith_expr -> Boolean.bool_expr
(** Create an expression representing <c>t1 >= t2</c> *)
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
type bitvec_expr = BitVecExpr of Expr.expr
type bitvec_num = BitVecNum of bitvec_expr
val sort_of_bitvec_sort : BitVector.bitvec_sort -> Sort.sort
val bitvec_sort_of_sort : Sort.sort -> BitVector.bitvec_sort
val expr_of_bitvec_expr : BitVector.bitvec_expr -> Expr.expr
val bitvec_expr_of_bitvec_num : BitVector.bitvec_num -> BitVector.bitvec_expr
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 <c>t1/t2</c> if \c t2 is
different from zero. If <c>t2</c> 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 <c>t1/t2</c> if \c t2 is different from zero, and <c>t1*t2 >= 0</c>.
- The \c ceiling of <c>t1/t2</c> if \c t2 is different from zero, and <c>t1*t2 < 0</c>.
If <c>t2</c> 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 <c>t1 - (t1 /u t2) * t2</c>, where <c>/u</c> represents unsigned division.
If <c>t2</c> 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 <c>t1 - (t1 /s t2) * t2</c>, where <c>/s</c> represents signed division.
The most significant bit (sign) of the result is equal to the most significant bit of \c t1.
If <c>t2</c> 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 <c>t2</c> 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 <c>n1+n2</c>, where <c>n1</c> (<c>n2</c>)
is the size of <c>t1</c> (<c>t2</c>). *)
val mk_concat : context -> bitvec_expr -> bitvec_expr -> bitvec_expr
(** Bit-vector extraction.
Extract the bits between two limits from a bitvector of
size <c>m</c> to yield a new bitvector of size <c>n</c>, where
<c>n = high - low + 1</c>. *)
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 <c>m+i</c>, 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 <c>m+i</c>, 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 <c>2^x</c> 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 <c>2^x</c> 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
(** 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 <c>[0..2^N-1]</c>, 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.
<returns>An expression if the function has an interpretation in the model, null otherwise.</returns> *)
val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option
(** Retrieves the interpretation (the assignment) of an expression in the model.
<returns>An expression if the constant has an interpretation in the model, null otherwise.</returns> *)
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.
<returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns> *)
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 <c>ModelEvaluationFailedException</c> is thrown.
*)
val eval : model -> Expr.expr -> bool -> Expr.expr
(** Alias for <c>eval</c>. *)
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.
<returns>A string representation of the model.</returns> *)
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 <c>Context.NumProbes</c>
and <c>Context.ProbeNames</c>.
It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end.
*)
module Probe :
sig
type probe
(** Execute the probe over the goal.
<returns>A probe always produce a double value.
"Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns> *)
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 <c>Context.get_num_tactics</c>
and <c>Context.get_tactic_names</c>.
It may also be obtained using the command <c>(help-tactics)</c> 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 <c>g</c>, that the ApplyResult was obtained from.
#return A model for <c>g</c> *)
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 <c>skip</c> 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 <c>UsingParams</c>*)
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
type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
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 <c>Check</c>.
The result is <c>None</c> if <c>Check</c> was not invoked before,
if its results was not <c>SATISFIABLE</c>, or if model production is not enabled. *)
val get_model : solver -> Model.model option
(** The proof of the last <c>Check</c>.
The result is <c>null</c> if <c>Check</c> was not invoked before,
if its results was not <c>UNSATISFIABLE</c>, or if proof production is disabled. *)
val get_proof : solver -> Expr.expr option
(** The unsat core of the last <c>Check</c>.
The unsat core is a subset of <c>Assertions</c>
The result is empty if <c>Check</c> was not invoked before,
if its results was not <c>UNSATISFIABLE</c>, 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 <c>Check</c> returned <c>UNKNOWN</c>. *)
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 <c>Push</c> and <c>Pop</c>, 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 <c>Push</c></remarks>
{!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 <tt>property</tt> about the <tt>predicate</tt>.
The property is added at <tt>level</tt>. *)
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:
<c>z3.exe -ini?</c>
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 <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
val get_num_smtlib_formulas : context -> int
(** The formulas parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
val get_smtlib_formulas : context -> Boolean.bool_expr array
(** The number of SMTLIB assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
val get_num_smtlib_assumptions : context -> int
(** The assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
val get_smtlib_assumptions : context -> Boolean.bool_expr array
(** The number of SMTLIB declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
val get_num_smtlib_decls : context -> int
(** The declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
val get_smtlib_decls : context -> FuncDecl.func_decl array
(** The number of SMTLIB sorts parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
val get_num_smtlib_sorts : context -> int
(** The sort declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>. *)
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 <module-name>.<parameter-name>.
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
View git blame Copy permalink