Home  •  Docs  •  Download  •  •  FAQ  •  Awards  •  Status  •  MSR 

An Efficient SMT Solver
module Z3: sig end
 
L_FALSE 
 
L_UNDEF 
 
L_TRUE 
 
INT_SYMBOL 
 
STRING_SYMBOL 
 
PARAMETER_INT 
 
PARAMETER_DOUBLE 
 
PARAMETER_RATIONAL 
 
PARAMETER_SYMBOL 
 
PARAMETER_SORT 
 
PARAMETER_AST 
 
PARAMETER_FUNC_DECL 
 
UNINTERPRETED_SORT 
 
BOOL_SORT 
 
INT_SORT 
 
REAL_SORT 
 
BV_SORT 
 
ARRAY_SORT 
 
DATATYPE_SORT 
 
RELATION_SORT 
 
FINITE_DOMAIN_SORT 
 
UNKNOWN_SORT 
 
NUMERAL_AST 
 
APP_AST 
 
VAR_AST 
 
QUANTIFIER_AST 
 
SORT_AST 
 
FUNC_DECL_AST 
 
UNKNOWN_AST 
 
OP_TRUE 
 
OP_FALSE 
 
OP_EQ 
 
OP_DISTINCT 
 
OP_ITE 
 
OP_AND 
 
OP_OR 
 
OP_IFF 
 
OP_XOR 
 
OP_NOT 
 
OP_IMPLIES 
 
OP_OEQ 
 
OP_ANUM 
 
OP_AGNUM 
 
OP_LE 
 
OP_GE 
 
OP_LT 
 
OP_GT 
 
OP_ADD 
 
OP_SUB 
 
OP_UMINUS 
 
OP_MUL 
 
OP_DIV 
 
OP_IDIV 
 
OP_REM 
 
OP_MOD 
 
OP_TO_REAL 
 
OP_TO_INT 
 
OP_IS_INT 
 
OP_POWER 
 
OP_STORE 
 
OP_SELECT 
 
OP_CONST_ARRAY 
 
OP_ARRAY_MAP 
 
OP_ARRAY_DEFAULT 
 
OP_SET_UNION 
 
OP_SET_INTERSECT 
 
OP_SET_DIFFERENCE 
 
OP_SET_COMPLEMENT 
 
OP_SET_SUBSET 
 
OP_AS_ARRAY 
 
OP_BNUM 
 
OP_BIT1 
 
OP_BIT0 
 
OP_BNEG 
 
OP_BADD 
 
OP_BSUB 
 
OP_BMUL 
 
OP_BSDIV 
 
OP_BUDIV 
 
OP_BSREM 
 
OP_BUREM 
 
OP_BSMOD 
 
OP_BSDIV0 
 
OP_BUDIV0 
 
OP_BSREM0 
 
OP_BUREM0 
 
OP_BSMOD0 
 
OP_ULEQ 
 
OP_SLEQ 
 
OP_UGEQ 
 
OP_SGEQ 
 
OP_ULT 
 
OP_SLT 
 
OP_UGT 
 
OP_SGT 
 
OP_BAND 
 
OP_BOR 
 
OP_BNOT 
 
OP_BXOR 
 
OP_BNAND 
 
OP_BNOR 
 
OP_BXNOR 
 
OP_CONCAT 
 
OP_SIGN_EXT 
 
OP_ZERO_EXT 
 
OP_EXTRACT 
 
OP_REPEAT 
 
OP_BREDOR 
 
OP_BREDAND 
 
OP_BCOMP 
 
OP_BSHL 
 
OP_BLSHR 
 
OP_BASHR 
 
OP_ROTATE_LEFT 
 
OP_ROTATE_RIGHT 
 
OP_EXT_ROTATE_LEFT 
 
OP_EXT_ROTATE_RIGHT 
 
OP_INT2BV 
 
OP_BV2INT 
 
OP_CARRY 
 
OP_XOR3 
 
OP_PR_UNDEF 
 
OP_PR_TRUE 
 
OP_PR_ASSERTED 
 
OP_PR_GOAL 
 
OP_PR_MODUS_PONENS 
 
OP_PR_REFLEXIVITY 
 
OP_PR_SYMMETRY 
 
OP_PR_TRANSITIVITY 
 
OP_PR_TRANSITIVITY_STAR 
 
OP_PR_MONOTONICITY 
 
OP_PR_QUANT_INTRO 
 
OP_PR_DISTRIBUTIVITY 
 
OP_PR_AND_ELIM 
 
OP_PR_NOT_OR_ELIM 
 
OP_PR_REWRITE 
 
OP_PR_REWRITE_STAR 
 
OP_PR_PULL_QUANT 
 
OP_PR_PULL_QUANT_STAR 
 
OP_PR_PUSH_QUANT 
 
OP_PR_ELIM_UNUSED_VARS 
 
OP_PR_DER 
 
OP_PR_QUANT_INST 
 
OP_PR_HYPOTHESIS 
 
OP_PR_LEMMA 
 
OP_PR_UNIT_RESOLUTION 
 
OP_PR_IFF_TRUE 
 
OP_PR_IFF_FALSE 
 
OP_PR_COMMUTATIVITY 
 
OP_PR_DEF_AXIOM 
 
OP_PR_DEF_INTRO 
 
OP_PR_APPLY_DEF 
 
OP_PR_IFF_OEQ 
 
OP_PR_NNF_POS 
 
OP_PR_NNF_NEG 
 
OP_PR_NNF_STAR 
 
OP_PR_CNF_STAR 
 
OP_PR_SKOLEMIZE 
 
OP_PR_MODUS_PONENS_OEQ 
 
OP_PR_TH_LEMMA 
 
OP_RA_STORE 
 
OP_RA_EMPTY 
 
OP_RA_IS_EMPTY 
 
OP_RA_JOIN 
 
OP_RA_UNION 
 
OP_RA_WIDEN 
 
OP_RA_PROJECT 
 
OP_RA_FILTER 
 
OP_RA_NEGATION_FILTER 
 
OP_RA_RENAME 
 
OP_RA_COMPLEMENT 
 
OP_RA_SELECT 
 
OP_RA_CLONE 
 
OP_FD_LT 
 
OP_LABEL 
 
OP_LABEL_LIT 
 
OP_UNINTERPRETED 
 
NO_FAILURE 
 
UNKNOWN 
 
TIMEOUT 
 
MEMOUT_WATERMARK 
 
CANCELED 
 
NUM_CONFLICTS 
 
THEORY 
 
QUANTIFIERS 
 
PRINT_SMTLIB_FULL 
 
PRINT_LOW_LEVEL 
 
PRINT_SMTLIB_COMPLIANT 
 
PRINT_SMTLIB2_COMPLIANT 
 
OK 
 
SORT_ERROR 
 
IOB 
 
INVALID_ARG 
 
PARSER_ERROR 
 
NO_PARSER 
 
INVALID_PATTERN 
 
MEMOUT_FAIL 
 
FILE_ACCESS_ERROR 
 
INTERNAL_FATAL 
 
INVALID_USAGE 
 
DEC_REF_ERROR 
 
EXCEPTION 
 
GOAL_PRECISE 
 
GOAL_UNDER 
 
GOAL_OVER 
 
GOAL_UNDER_OVER 
Types

Most of the types in the API are abstract.
config
: a configuration object used to initialize logical contexts.
context
: logical context. This is the main Z3 datastructure.
symbol
: a Lisplike symbol. It is used to name types, constants, and functions. A symbol can be created using
string or integers.
ast
: abstract syntax tree node. That is, the datastructure used in Z3 to represent terms, formulas and types.
sort
: a kind of AST used to represent types.
app
: a kind of AST used to represent constant and function declarations.
pattern
: a kind of AST used to represent pattern and multipatterns used to guide quantifier instantiation.
model
: a model for the constraints asserted into the logical context.lbool
Lifted Boolean type: false
, undefined
, true
.symbol
In Z3, a symbol can be represented using integers and strings (See Z3.get_symbol_kind
).
Z3.mk_int_symbol
Z3.mk_string_symbol
parameter_kind
The different kinds of parameters that can be associated with function symbols.
Z3.get_decl_num_parameters
Z3.get_decl_parameter_kind
sort_kind
The different kinds of Z3 types (See Z3.get_sort_kind
).ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
decl_kind
The different kinds of interpreted function kinds.
f
(a1,..,a_n)i
= f(a1i
,...,a_ni
) for every i.
mp T1 T2
: q
The second antecedents may also be a proof for (iff p q).
symmetry T1
: (R s t)
T1 is the antecedent of this proof object.
trans T1 T2
: (R t u)
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.
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.
quantintro T1
: (~ (forall (x) p) (forall (x) q))
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.
andelim T1
: l_i
notorelim T1
: (not l_i)
Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)
x_1 ... x_m
... p_nx_1 ... x_m
))
(and (forall (x_1 ... x_m) p_1x_1 ... x_m
)
...
(forall (x_1 ... x_m) p_nx_1 ... x_m
)))
This proof object has no antecedents.
x_1 ... x_n
)
(forall (x_1 ... x_n) px_1 ... x_n
))
x
)) Pt
)
if x does not occur in t.
Several variables can be eliminated simultaneously.
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.
unitresolution T1 ... T(n+1)
: (or l_1' ... l_m')
ifftrue T1
: (iff p true)
ifffalse T1
: (iff p false)
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.
defintro
: (and (or n (not e)) (or (not n) e))
or:
defintro
: (or (not n) e)
when e only occurs positively.
When e is of the form (ite cond th el):
defintro
: (and (or (not cond) (= n th)) (or cond (= n el)))
Otherwise:
defintro
: (= n e)
applydef T1
: F ~ n
F is 'equivalent' to n, given that T1 is a proof that
n is a name for F.
iff~ T1
: (~ p q)
nnfpos 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
nnfpos T1
: (~ (forall (x T) q) (forall (x T) q_new))
(b) When recursively creating NNF over Boolean formulas, where the toplevel
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'.
nnfneg 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
nnfneg 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'
nnfneg T1 T2 T3 T4
: (~ (not (iff s_1 s_2))
(and (or r_1 r_2) (or r_1' r_2')))
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
sk
: (~ (not (forall x (p x y))) (not (p (sk y) y)))
sk
: (~ (exists x (p x y)) (p (sk y) y))
This proof object has no antecedents.
mp~ T1 T2
: q
n+1
arguments, where the first argument is the relation and the remaining n
elements
correspond to the n
columns of the relation.
where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.
n+1
arguments, where the first argument is a relation,
and the remaining n
arguments correspond to a record.
OP_RA_UNION
to perform destructive updates to the first argument.
search_failure
The different kinds of search failure types.
ast_print_mode
Z3 pretty printing modes (See Z3.set_ast_print_mode
).
error_code
Z3 error codes
goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.
Create configuration

Configurations are created in order to assign parameters prior to creating contexts for Z3 interaction. For example, if the users wishes to use model generation, then call:
set_param_value cfg "MODEL" "true"
Z3.mk_context_x
instead of using
explicit configuration objects. The function Z3.mk_context_x
receives an array of string pairs. This array represents the
configuration options.
Z3.set_param_value
The list of all configuration parameters can be obtained using the Z3 executable:
z3.exe ini?
Z3.mk_config
Create context

After a context is created, the configuration cannot be changed,
although some parameters can be changed using Z3.update_param_value
.
All main interaction with Z3 happens in the context of a context
.
Z3.mk_context_x
instead of using
explicit configuration objects. The function Z3.mk_context_x
receives an array of string pairs. This array represents the
configuration options.Z3.mk_context
. However,
in the context returned by this function, the user
is responsible for managing ast reference counters.
Managing reference counters is a burden and errorprone,
but allows the user to use the memory more efficiently.
The user must invoke Z3.inc_ref
for any ast returned
by Z3, and Z3.dec_ref
whenever the ast is not needed
anymore. This idiom is similar to the one used in
BDD (binary decision diagrams) packages such as CUDD.
Remark: sort, func_decl, app, pattern are ast's.
After a context is created, the configuration cannot be changed.
All main interaction with Z3 happens in the context of a context
.
c
should have been created using Z3.mk_context_rc
.
This function is a NOOP if c
was created using Z3.mk_context
.c
should have been created using Z3.mk_context_rc
.
This function is a NOOP if c
was created using Z3.mk_context
.The list of all configuration parameters can be obtained using the Z3 executable:
z3.exe ini?
Only a few configuration parameters are mutable once the context is created. The error handler is invoked when trying to modify an immutable parameter.
Z3.set_param_value
Returns None
if the parameter value does not exist.
Z3.mk_config
Z3.set_param_value
Parameters

k
with value v
to the parameter set p
.k
with value v
to the parameter set p
.k
with value v
to the parameter set p
.k
with value v
to the parameter set p
.Symbols

Symbols are used to name several term and type constructors.
NB. Not all integers can be passed to this function. The legal range of unsigned int integers is 0 to 2^301.
Z3.mk_string_symbol
Symbols are used to name several term and type constructors.
Z3.mk_int_symbol
Sorts

Two free types are considered the same iff the have the same name.
This type is used to create propositional variables and predicates.
This type is not the int type found in programming languages.
A machine integer can be represented using bitvectors. The function
Z3.mk_bv_sort
creates a bitvector type.
Z3.mk_bv_sort
This type is not a floating point number.
Z3 does not have support for floating point numbers yet.
This type can also be seen as a machine integer.
To create constants that belong to the finite domain, use the APIs for creating numerals and pass a numeric constant together with the sort returned by this call.
Z3.get_finite_domain_sort_size.
We usually represent the array type as: domain > range
.
Arrays are usually used to model the heap/memory in software verification.
Z3.mk_select
Z3.mk_store
context >
symbol >
symbol array >
sort array > sort * func_decl * func_decl array
mk_tuple_sort c name field_names field_sorts
creates a tuple with a constructor named name
,
a n
fields, where n
is the size of the arrays field_names
and field_sorts
.
context >
symbol >
symbol array > sort * func_decl array * func_decl array
mk_enumeration_sort c enums
creates an enumeration sort with enumeration names enums
,
it also returns n
predicates, where n
is the number of enums
corresponding
to testing whether an element is one of the enumerants.
context >
symbol >
sort >
sort * func_decl * func_decl * func_decl * func_decl *
func_decl * func_decl
mk_list_sort c name elem_sort
creates a list sort of name
, over elements of sort elem_sort
.
context >
symbol >
symbol > symbol array > sort array > int array > constructor
Each constructor inside the constructor list must be independently reclaimed using Z3.del_constructor
.
context >
symbol array >
constructor_list array > sort array * constructor_list array
Constants and Applications

mk_func_decl c n d r
creates a function with name n
, domain d
, and range r
.
The arity of the function is the size of the array d
.
mk_const c s t
is a shorthand for mk_app c (mk_func_decl c s [] t) []
Z3.mk_func_decl
Z3.mk_app
Z3 will generate an unique name for this function declaration.
Z3.mk_func_decl
mk_fresh_const c p t
is a shorthand for mk_app c (mk_fresh_func_decl c p [] t) []
.
Z3.mk_func_decl
Z3.mk_app
Propositional Logic and Equality

true
.false
. mk_eq c l r
]
Create an AST node representing l = r .
The nodes l
and r
must have the same type.
mk_distinct c [ t_1; ...; t_n ]
] Create an AST
node represeting a distinct construct. It is used for declaring
the arguments t_i pairwise distinct.
The distinct
construct is used for declaring the arguments pairwise distinct.
That is, Forall 0 <= i < j < num_args. not argsi
= argsj
.
All arguments must have the same sort.
mk_not c a
]
Create an AST node representing not(a) .
The node a
must have Boolean sort.
mk_ite c t1 t2 t2
]
Create an AST node representing an ifthenelse: ite(t1, t2,
t3) .
The node t1
must have Boolean sort, t2
and t3
must have the same sort.
The sort of the new node is equal to the sort of t2
and t3
.
mk_iff c t1 t2
]
Create an AST node representing t1 iff t2 .
The nodes t1
and t2
must have Boolean sort.
mk_implies c t1 t2
]
Create an AST node representing t1 implies t2 .
The nodes t1
and t2
must have Boolean sort.
mk_xor c t1 t2
]
Create an AST node representing t1 xor t2 .
The nodes t1
and t2
must have Boolean sort.
mk_and c [ t_1; ...; t_n ]
] Create the conjunction: t_1 and ... and t_n.
All arguments must have Boolean sort.
mk_or c [ t_1; ...; t_n ]
] Create the disjunction: t_1 or ... or t_n.
All arguments must have Boolean sort.
Arithmetic: Integers and Reals

mk_add c [ t_1; ...; t_n ]
] Create the term: t_1 + ... + t_n.
All arguments must have int or real sort.
mk_mul c [ t_1; ...; t_n ]
] Create the term: t_1 * ... * t_n.
All arguments must have int or real sort.
mk_sub c [ t_1; ...; t_n ]
] Create the term: t_1  ...  t_n.
All arguments must have int or real sort.
mk_unary_minus c arg
] Create the term:  arg.
The arguments must have int or real type.
mk_div c t_1 t_2
] Create the term: t_1 div t_2.
The arguments must either both have int type or both have real type.
If the arguments have int type, then the result type is an int type, otherwise the
the result type is real.
mk_mod c t_1 t_2
] Create the term: t_1 mod t_2.
The arguments must have int type.
mk_rem c t_1 t_2
] Create the term: t_1 rem t_2.
The arguments must have int type.
mk_lt c t1 t2
]
Create less than.
The nodes t1
and t2
must have the same sort, and must be int or real.
mk_le c t1 t2
]
Create less than or equal to.
The nodes t1
and t2
must have the same sort, and must be int or real.
mk_gt c t1 t2
]
Create greater than.
The nodes t1
and t2
must have the same sort, and must be int or real.
mk_ge c t1 t2
]
Create greater than or equal to.
The nodes t1
and t2
must have the same sort, and must be int or real.
mk_int2real c t1
]
Coerce an integer to a real.
There is also a converse operation exposed. It follows the semantics prescribed by the SMTLIB standard.
You can take the floor of a real by
creating an auxiliary integer constant k
and
and asserting mk_int2real(k) <= t1 < mk_int2real(k)+1 .
The node t1
must have sort integer.
Z3.mk_real2int
Z3.mk_is_int
mk_real2int c t1
]
Coerce a real to an integer.
The semantics of this function follows the SMTLIB standard for the function to_int
Z3.mk_int2real
Z3.mk_is_int
mk_is_int c t1
]
Check if a real number is an integer.
Z3.mk_int2real
Z3.mk_real2int
Bitvectors

mk_bvnot c t1
]
Bitwise negation.
The node t1
must have a bitvector sort.
mk_bvredand c t1
]
Take conjunction of bits in vector, return vector of length 1.
The node t1
must have a bitvector sort.
mk_bvredor c t1
]
Take disjunction of bits in vector, return vector of length 1.
The node t1
must have a bitvector sort.
mk_bvand c t1 t2
]
Bitwise and.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvor c t1 t2
]
Bitwise or.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvxor c t1 t2
]
Bitwise exclusiveor.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvnand c t1 t2
]
Bitwise nand.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvnor c t1 t2
]
Bitwise nor.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvxnor c t1 t2
]
Bitwise xnor.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvneg c t1
]
Standard two's complement unary minus.
The node t1
must have bitvector sort.
mk_bvadd c t1 t2
]
Standard two's complement addition.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsub c t1 t2
]
Standard two's complement subtraction.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvmul c t1 t2
]
Standard two's complement multiplication.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvudiv c t1 t2
]
Unsigned division.
It is defined as the floor
of t1/t2 if t2
is
different from zero. If t2 is zero, then the result
is undefined.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsdiv c t1 t2
]
Two's complement signed division.
It is defined in the following way:
floor
of t1/t2 if t2
is different from zero, and t1*t2 >= 0 .
ceiling
of t1/t2 if t2
is different from zero, and t1*t2 < 0 .
The nodes t1
and t2
must have the same bitvector sort.
mk_bvurem c t1 t2
]
Unsigned remainder.
It is defined as t1  (t1 /u t2) * t2 , where /u represents unsigned int division.
If t2 is zero, then the result is undefined.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsrem c t1 t2
]
Two's complement signed remainder (sign follows dividend).
It is defined as t1  (t1 /s t2) * t2 , where /s represents signed division.
The most significant bit (sign) of the result is equal to the most significant bit of t1
.
If t2 is zero, then the result is undefined.
The nodes t1
and t2
must have the same bitvector sort.
Z3.mk_bvsmod
mk_bvsmod c t1 t2
]
Two's complement signed remainder (sign follows divisor).
If t2 is zero, then the result is undefined.
The nodes t1
and t2
must have the same bitvector sort.
Z3.mk_bvsrem
mk_bvult c t1 t2
]
Unsigned less than.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvslt c t1 t2
]
Two's complement signed less than.
It abbreviates:
(or (and (= (extract[m1:m1] t1) bit1) (= (extract[m1:m1] t2) bit0)) (and (= (extract[m1:m1] t1) (extract[m1:m1] t2)) (bvult t1 t2)))
The nodes t1
and t2
must have the same bitvector sort.
mk_bvule c t1 t2
]
Unsigned less than or equal to.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsle c t1 t2
]
Two's complement signed less than or equal to.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvuge c t1 t2
]
Unsigned greater than or equal to.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsge c t1 t2
]
Two's complement signed greater than or equal to.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvugt c t1 t2
]
Unsigned greater than.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsgt c t1 t2
]
Two's complement signed greater than.
The nodes t1
and t2
must have the same bitvector sort.
mk_concat c t1 t2
]
Concatenate the given bitvectors.
The nodes t1
and t2
must have (possibly different) bitvector sorts
The result is a bitvector of size n1+n2 , where n1
(n2)
is the size
of t1
(t2)
.
mk_extract c high low t1
]
Extract the bits high
down to low
from a bitvector of
size m
to yield a new bitvector of size n
, where n =
high  low + 1 .
The node t1
must have a bitvector sort.
mk_sign_ext c i t1
]
Signextend of the given bitvector to the (signed) equivalent bitvector of
size m+i , where m
is the size of the given
bitvector.
The node t1
must have a bitvector sort.
mk_zero_ext c i t1
]
Extend the given bitvector with zeros to the (unsigned int) equivalent
bitvector of size m+i , where m
is the size of the
given bitvector.
The node t1
must have a bitvector sort.
mk_repeat c i t1
]
Repeat the given bitvector up length i .
The node t1
must have a bitvector sort.
mk_bvshl c t1 t2
]
Shift left.
It is equivalent to multiplication by 2^x where 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 nodes t1
and t2
must have the same bitvector sort.
mk_bvlshr c t1 t2
]
Logical shift right.
It is equivalent to unsigned int division by 2^x where 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 nodes t1
and t2
must have the same bitvector sort.
mk_bvashr c t1 t2
]
Arithmetic shift right.
It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The nodes t1
and t2
must have the same bitvector sort.
mk_rotate_left c i t1
]
Rotate bits of t1
to the left i
times.
The node t1
must have a bitvector sort.
mk_rotate_right c i t1
]
Rotate bits of t1
to the right i
times.
The node t1
must have a bitvector sort.
mk_ext_rotate_left c t1 t2
]
Rotate bits of t1
to the left t2
times.
The nodes t1
and t2
must have the same bitvector sort.
mk_ext_rotate_right c t1 t2
]
Rotate bits of t1
to the right t2
times.
The nodes t1
and t2
must have the same bitvector sort.
mk_int2bv c n t1
]
Create an n
bit bitvector from the integer argument t1
.
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 node t1
must have integer sort.
mk_bv2int c t1 is_signed
]
Create an integer from the bitvector argument t1
.
If is_signed
is false, then the bitvector t1
is treated as unsigned int.
So the result is nonnegative
and in the range 0..2^N1
, where N are the number of bits in t1
.
If is_signed
is true, t1
is treated as a signed bitvector.
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 node t1
must have a bitvector sort.
mk_bvadd_no_overflow c t1 t2 is_signed
]
Create a predicate that checks that the bitwise addition
of t1
and t2
does not overflow.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvadd_no_underflow c t1 t2
]
Create a predicate that checks that the bitwise signed addition
of t1
and t2
does not underflow.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsub_no_overflow c t1 t2
]
Create a predicate that checks that the bitwise signed subtraction
of t1
and t2
does not overflow.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsub_no_underflow c t1 t2 is_signed
]
Create a predicate that checks that the bitwise subtraction
of t1
and t2
does not underflow.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvsdiv_no_overflow c t1 t2
]
Create a predicate that checks that the bitwise signed division
of t1
and t2
does not overflow.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvneg_no_overflow c t1
]
Check that bitwise negation does not overflow when
t1
is interpreted as a signed bitvector.
The node t1
must have bitvector sort.
mk_bvmul_no_overflow c t1 t2 is_signed
]
Create a predicate that checks that the bitwise multiplication
of t1
and t2
does not overflow.
The nodes t1
and t2
must have the same bitvector sort.
mk_bvmul_no_underflow c t1 t2
]
Create a predicate that checks that the bitwise signed multiplication
of t1
and t2
does not underflow.
The nodes t1
and t2
must have the same bitvector sort.
Arrays

mk_select c a i
]
Array read.
The argument a
is the array and i
is the index of the array that gets read.
The node a
must have an array sort domain > range
,
and i
must have the sort domain
.
The sort of the result is range
.
Z3.mk_array_sort
Z3.mk_store
mk_store c a i v
]
Array update.
The node a
must have an array sort domain > range
, i
must have sort domain
,
v
must have sort range. The sort of the result is domain > range
.
The semantics of this function is given by the theory of arrays described in the SMTLIB
standard. See http:
The result of this function is an array that is equal to a
(with respect to select)
on all indices except for i
, where it maps to v
(and the select
of a
with
respect to i
may be a different value).
Z3.mk_array_sort
Z3.mk_select
The resulting term is an array, such that a select
on an arbitrary index
produces the value v
.
mk_map f n args
]
map f on the the argument arrays.
The n
nodes args
must be of array sorts domain_i > range_i
.
The function declaration f
must have type range_1 .. range_n > range .
v
must have sort range. The sort of the result is domain_i > range
.
Z3.mk_array_sort
Z3.mk_store
Z3.mk_select
Sets

The first argument must be a set, the second an element.
The first argument must be a set, the second an element.
The first argument should be an element type of the set.
Numerals

This function can be use to create numerals that fit in a machine integer.
It is slightly faster than Z3.mk_numeral
since it is not necessary to parse a string.
Z3.mk_numeral
This function can be use to create numerals that fit in a machine long long integer.
It is slightly faster than Z3.mk_numeral
since it is not necessary to parse a string.
Z3.mk_numeral
Quantifiers

Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.
Patterns comprise a list of terms. The list should be nonempty. If the list comprises of more than one term, it is a called a multipattern.
In general, one can pass in a list of (multi)patterns in the quantifier constructor.
Z3.mk_forall
Z3.mk_exists
Bound variables are indexed by deBruijn indices. It is perhaps easiest to explain the meaning of deBruijn indices by indicating the compilation process from nondeBruijn formulas to deBruijn format.
abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) abs1(x, x, n) = b_n abs1(y, x, n) = y abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
The last line is significant: the index of a bound variable is different depending
on the scope in which it appears. The deeper x appears, the higher is its
index.
body
that contains bound variables
of the same sorts as the sorts listed in the array sorts
. The bound variables are deBruijn indices created
using Z3.mk_bound
. The array decl_names
contains the names that the quantified formula uses for the
bound variables. Z3 applies the convention that the last element in the decl_names
and sorts
array
refers to the variable with index 0, the second to last element of decl_names
and sorts
refers
to the variable with index 1, etc.
mk_forall c w p t n b
creates a forall formula, where
w
is the weight, p
is an array of patterns, t
is an array
with the sorts of the bound variables, n
is an array with the
'names' of the bound variables, and b
is the body of the
quantifier. Quantifiers are associated with weights indicating
the importance of using the quantifier during
instantiation.
Z3.mk_forall
.
Z3.mk_pattern
Z3.mk_bound
Z3.mk_forall
Z3.mk_quantifier
context >
bool >
int >
pattern array > sort array > symbol array > ast > ast
Z3.mk_forall
for an explanation of the parameters.context >
bool >
int >
symbol >
symbol >
pattern array >
ast array > sort array > symbol array > ast > ast
Z3.mk_forall_const
.
Summary: Create an existential quantifier using a list of constants that
will form the set of bound variables.
context >
bool >
int >
symbol >
symbol >
app array > pattern array > ast array > ast > ast
Accessors

Symbols

INT_SYMBOL
if the symbol was constructed
using Z3.mk_int_symbol
, and STRING_SYMBOL
if the symbol
was constructed using Z3.mk_string_symbol
. get_symbol_int c s
]
Return the symbol int value.
Z3.mk_int_symbol
get_symbol_string c s
]
Return the symbol name.
Z3.mk_string_symbol
Sorts

sort
into ast
.
Z3.sort_to_ast c s
can be replaced by (s :> Z3.ast)
.s
.Bitvectors

get_bv_sort_size c t
]
Return the size of the given bitvector sort.
Z3.mk_bv_sort
Z3.get_sort_kind
Finite Domains

r
. Return None
if the call failed.
That is, get_sort_kind(s) == FINITE_DOMAIN_SORTArrays

get_array_sort_domain c t
]
Return the domain of the given array sort.
Z3.mk_array_sort
Z3.get_sort_kind
get_array_sort_range c t
]
Return the range of the given array sort.
Z3.mk_array_sort
Z3.get_sort_kind
Datatypes

get_tuple_sort_mk_decl c t
]
Return the constructor declaration of the given tuple
sort.
Z3.mk_tuple_sort
Z3.get_sort_kind
get_tuple_sort_num_fields c t
]
Return the number of fields of the given tuple sort.
Z3.get_tuple_sort
, which
returns a tuple: tuple constructor, and an array of the tuple sort fields.
Z3.mk_tuple_sort
Z3.get_sort_kind
get_tuple_sort_field_decl c t i
]
Return the ith field declaration (i.e., projection function declaration)
of the given tuple sort.
Z3.get_tuple_sort
, which
returns a tuple: tuple constructor, and an array of the tuple sort fields.
Z3.mk_tuple_sort
Z3.get_sort_kind
Z3.get_datatype_sort_constructor
Z3.get_datatype_sort_recognizer
Z3.get_datatype_sort_constructor_accessor
Z3.get_datatype_sort_num_constructors
Z3.get_datatype_sort_recognizer
Z3.get_datatype_sort_constructor_accessor
Z3.get_datatype_sort_num_constructors
Z3.get_datatype_sort_constructor
Z3.get_datatype_sort_constructor_accessor
Z3.get_datatype_sort_num_constructors
Z3.get_datatype_sort_constructor
Z3.get_datatype_sort_recognizer
Relations

Z3.get_relation_column
Z3.get_relation_arity
Function Declarations

func_decl
into ast
.
Z3.func_decl_to_ast c f
can be replaced by (f :> Z3.ast)
.f
. get_domain c d i
]
Return the sort of the ith parameter of the given function declaration.
Z3.get_domain_size
get_range c d
]
Return the range of the given declaration.
If d
is a constant (i.e., has zero arguments), then this
function returns the sort of the constant.
Applications

app
into ast
.
Z3.app_to_ast c a
can be replaced by (a :> Z3.ast)
. get_app_num_args c a
]
Return the number of argument of an application. If t
is an constant, then the number of arguments is 0. get_app_arg c a i
]
Return the ith argument of the given application.
Terms

t
.
Implicitly used by Pervasives.compare
for values of type ast
, app
, sort
, func_decl
, and pattern
.Hashtbl.hash
for values of type ast
, app
, sort
, func_decl
, and pattern
.
The AST node must be a constant, application, numeral, bound variable, or quantifier.
t
is well sorted.a
is true, L_FALSE if it is false, and L_UNDEF otherwise.context > ast > bool
val is_numeral_ast : context > ast > bool
val is_algebraic_number : context > ast > bool
ast
into an APP_AST
.
get_ast_kind c a == [APP_AST]
get_ast_kind c a == FUNC_DECL_AST
Numerals

precision
decimal places.
get_numeral_int c v
]
Similar to Z3.get_numeral_string
, but only succeeds if
the value can fit in a machine int. Return TRUE if the call succeeded.
Z3.get_numeral_string
get_numeral_int64 c v
]
Similar to Z3.get_numeral_string
, but only succeeds if
the value can fit in a machine long long int. Return TRUE if the call succeeded.
Z3.get_numeral_string
get_numeral_rational_int64 c x y
]
Similar to Z3.get_numeral_string
, but only succeeds if
the value can fit as a reational number as machine long long int. Return TRUE if the call succeeded.
Z3.get_numeral_string
Patterns

Z3.pattern_to_ast c p
can be replaced by (p :> Z3.ast)
.Quantifiers

Simplification

Provides an interface to the AST simplifier used by Z3.
Provides an interface to the AST simplifier used by Z3.
This procedure is similar to Z3.simplify
, but the behavior of the simplifier
can be configured using the given parameter set.
Modifiers

a
using the arguments args
.
The number of arguments num_args
should coincide
with the number of arguments to a
.
If a
is a quantifier, then num_args has to be 1.i
in a
with toi
, for i
smaller than num_exprs
.
The result is the new AST. The arrays from
and to
must have size num_exprs
.
For every i
smaller than num_exprs
, we must have that sort of fromi
must be equal to sort of toi
.a
with the expressions in to
.
For every i
smaller than num_exprs
, the variable with deBruijn index i
is replaced with term toi
.a
from context source
to context target
.
AST a
must have been created using context source
.
Models

a
in the model m
.
Return None
,
if the model does not assign an interpretation for a
.
That should be interpreted as: the value of a
does not matter.
f
in the model m
.
Return None
,
if the model does not assign an interpretation for f
.
That should be interpreted as: the f
does not matter.
Z3.get_model_constants
.
Z3.model_get_const_decl
model_get_const_decl c m i
]
Return the ith constant in the given model.
Z3.eval
A function interpretation is represented as a finite map and an 'else' value.
Each entry in the finite map represents the value of a function given a set of arguments.
model_get_func_decl c m i
]
Return the declaration of the ith function in the given model.
Z3.model_get_num_funcs
eval c m t
]
Evaluate the AST node t
in the given model.
Return None
if the term was not successfully evaluated.
If model_completion
is TRUE, then Z3 will assign an interpretation for any constant or function that does
not have an interpretation in m
. These constants and functions were essentially don't cares.
The evaluation may fail for the following reasons:
t
contains a quantifier.
m
is partial, that is, it doesn't have a complete interpretation for uninterpreted functions.
That is, the option MODEL_PARTIAL=true was used.
t
is type incorrect.m
assigs an interpretation to.
Z3 also provides an intepretation for uninterpreted sorts used in a formua.
The interpretation for a sort s
is a finite set of distinct values. We say this finite set is
the "universe" of s
.
Z3.model_get_sort
Z3.model_get_sort_universe
m
assigns an interpretation.
Z3.model_get_num_sorts
Z3.model_get_sort_universe
s
.
Z3.model_get_num_sorts
Z3.model_get_sort
i
we have that (select (_ asarray f) i) is equal to (f i) .
This procedure returns TRUE if the a
is an asarray
AST node.
Z3 current solvers have minimal support for as_array
nodes.
Z3.get_as_array_func_decl
f
associated with a (_ as_array f) node.
Z3.is_as_array
A function interpretation is represented as a finite map and an 'else' value.
Each entry in the finite map represents the value of a function given a set of arguments.
This procedure return the number of element in the finite map of f
.
f
in a particular point.
Z3.func_interp_get_num_entries
A function interpretation is represented as a finite map and an 'else' value.
This procedure returns the 'else' value.
A func_entry object represents an element in the finite map used to encode a function interpretation.
Z3.func_interp_get_entry
Z3.func_interp_get_entry
Interaction logging.

The interaction log is opened using open_log.
It contains the formulas that are checked using Z3.
You can use this command to append comments, for instance.
Warnings are printed after passing true
, warning messages are
suppressed after calling this method with false
.
String conversion

The default mode for pretty printing AST nodes is to produce SMTLIB 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 SMTLIB standards and uses let expressions to share common subexpressions use PRINT_SMTLIB_COMPLIANT.
Z3.ast_to_string
Z3.pattern_to_string
Z3.func_decl_to_string
Z3.pattern_to_string
Z3.sort_to_string
context > pattern > string
val sort_to_string : context > sort > string
val func_decl_to_string : context > func_decl > string
val model_to_string : context > model > string
context >
string > string > string > string > ast array > ast > string
Parser interface

context >
string >
symbol array >
sort array > symbol array > func_decl array > unit
parse_smtlib_string c str sort_names sorts decl_names decls
]
Parse the given string using the SMTLIB parser.
The symbol table of the parser can be initialized using the given sorts and declarations.
The symbols in the arrays sort_names
and decl_names
don't need to match the names
of the sorts and declarations in the arrays sorts
and decls
. This is an useful feature
since we can use arbitrary names to reference sorts and declarations defined using the C API.
The formulas, assumptions and declarations defined in str
can be extracted using the functions:
Z3.get_smtlib_num_formulas
, Z3.get_smtlib_formula
, Z3.get_smtlib_num_assumptions
, Z3.get_smtlib_assumption
,
Z3.get_smtlib_num_decls
, and Z3.get_smtlib_decl
.
context >
string >
symbol array >
sort array > symbol array > func_decl array > unit
Z3.parse_smtlib_string
, but reads the benchmark from a file.Z3.parse_smtlib_string
or Z3.parse_smtlib_file
. get_smtlib_formula c i
]
Return the ith formula parsed by the last call to Z3.parse_smtlib_string
or Z3.parse_smtlib_file
.
Z3.parse_smtlib_string
or Z3.parse_smtlib_file
. get_smtlib_assumption c i
]
Return the ith assumption parsed by the last call to Z3.parse_smtlib_string
or Z3.parse_smtlib_file
.
Z3.parse_smtlib_string
or Z3.parse_smtlib_file
. get_smtlib_decl c i
]
Return the ith declaration parsed by the last call to Z3.parse_smtlib_string
or Z3.parse_smtlib_file
.
get_smtlib_sort c i
]
Return the ith sort parsed by the last call to Z3.parse_smtlib_string
or Z3.parse_smtlib_file
.
get_smtlib_error c
]
Retrieve that last error message information generated from parsing. parse_z3_string c str
]
Parse the given string using the Z3 native parser.
Return the conjunction of asserts made in the input.
Z3.parse_z3_string
, but reads the benchmark from a file.context >
string >
symbol array >
sort array > symbol array > func_decl array > ast
parse_smtlib2_string c str
]
Parse the given string using the SMTLIB2 parser.
It returns a formula comprising of the conjunction of assertions in the scope
(up to push/pop) at the end of the string.
context >
string >
symbol array >
sort array > symbol array > func_decl array > ast
Z3.parse_smtlib2_string
, but reads the benchmark from a file.Miscellaneous

Use this facility on outof memory errors.
It allows discharging the previous state and resuming afresh.
Any pointers previously returned by the API
become invalid.
External Theory Plugins

th_name
.
A theory must be created before asserting any assertion to the given context.t
is deleted.
This callback should be used to delete external datastructures associated with the given theory.
Z3.mk_theory
f
is invoked by Z3's simplifier.s_1
and s_2
is an interpreted sort of the given theory.
The callback f
is invoked by Z3's simplifier.s_1
, ..., s_n
is an interpreted sort of the given theory.
The callback f
is invoked by Z3's simplifier.
n
added to the logical context at search level n
,
will remain in the logical context until this level is backtracked.s
, where s
is an interpreted sort of the theory \c
t, is finally added into the logical context. Note that, not
every expression contained in an asserted expression is
actually added into the logical context because it may be
simplified during a preprocessing step.
n
added to the logical context at search level n
,
will remain in the logical context until this level is backtracked.
When a casesplit is created we say the search level is increased.
When a casesplit is backtracked we say the search level is decreased.
If the theory returns false
,
Z3 will assume that theory is giving up,
and it will assume that it was not possible to decide if the asserted constraints
are satisfiable or not.
An axiom added at search level n
will remain in the logical context until
level n
is backtracked.
The callbacks for push (Z3.set_push_callback
) and pop
(Z3.set_pop_callback
) can be used to track when the search
level is increased (i.e., new casesplit) and decreased (i.e.,
casesplit is backtracked).
Z3 tracks the theory axioms asserted. So, multiple assertions of the same axiom are
ignored.
lhs
and rhs
have the same interpretation
in the model being built by theory t
. If lhs = rhs is inconsistent with other theories,
then the logical context will backtrack.
For more information, see the paper "ModelBased Theory Combination" in the Z3 website.
Z3.theory_assert_axiom
.
By default, the simplification of theory specific operators is disabled.
That is, the reduce theory callbacks are not invoked for theory axioms.
The default behavior is useful when asserting axioms stating properties of theory operators.n
.n
.
The elements in an equivalence class are organized in a circular list. You can traverse the list by calling this function multiple times using the result from the previous call. This is illustrated in the code snippet below.
ast curr = n; do curr = theory_get_eqc_next(theory, curr); while (curr != n);
n
that are operators of the given theory.TRUE
if n
is an interpreted theory value.TRUE
if d
is an interpreted theory declaration.Z3.set_new_elem_callback
.
Z3.set_new_app_callback
.
Fixedpoint facilities

horn_rule
should be of the form:
horn_rule ::= (forall (boundvars) horn_rule)  (=> atoms horn_rule)  atom
The constraints are used as background axioms when the fixedpoint engine uses the PDR mode.
They are ignored for standard Datalog mode.
query ::= (exists (boundvars) query)  literals
query returns
Z3.fixedpoint_get_answer
.
The queries are encoded as relations (function declarations).
query returns
Z3.fixedpoint_get_answer
.
When used in Datalog mode, the returned answer is a disjunction of conjuncts. Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction.
The previous call to fixedpoint_query must have returned L_TRUE.
Z3.fixedpoint_query
.
Use this method when Z3.fixedpoint_query
returns L_UNDEF.
Z3.fixedpoint_query
.context > fixedpoint > func_decl > symbol array > unit
It sets the predicate to use a set of domains given by the list of symbols.
The domains given by the list of symbols must belong to a set
of builtin domains.
AST vectors

i
in the AST vector v
.
i
of the AST vector v
with the AST a
.
v
.a
in the end of the AST vector v
. The size of v
is increased by one.v
from context s
into an AST vector in context t
.AST maps

m
contains the AST key k
.k
.
The procedure invokes the error handler if k
is not in the map.
Goals

If models == true, then model generation is enabled for the new goal.
If unsat_cores == true, then unsat core generation is enabled for the new goal.
If proofs == true, then proof generation is enabled for the new goal. Remark, the
Z3 context c must have been created with proof generation support.
a
to the given goal.false
.
g
from the context source
to a the context target
.Tactics and Probes

Z3.get_num_tactics
and Z3.get_tactic_name
.
It may also be obtained using the command (helptactics) in the SMT 2.0 frontend.
Tactics are the basic building block for creating custom solvers for specific problem domains.
Z3.get_num_probes
and Z3.get_probe_name
.
It may also be obtained using the command (helptactics) in the SMT 2.0 frontend.
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.
t1
to a given goal and t2
to every subgoal produced by t1.t1
to a given goal,
if it fails then returns the result of t2
applied to the given goal.t1
to a given goal and then t2
to every subgoal produced by t1. The subgoals are processed in parallel.t
to a given goal for ms
milliseconds.
If t
does not terminate in ms
milliseconds, then it fails.t
to a given goal is the probe p
evaluates to true.
If p
evaluates to false, then the new tactic behaves like the skip tactic.t1
to a given goal if the probe p
evaluates to true,
and t2
if p
evaluates to false.t
until the goal is not modified anymore or the maximum
number of iterations max
is reached.p
evaluates to false.t
using the given set of parameters.p1
is less than the value returned by p2
.
p1
is greater than the value returned by p2
.
p1
is less than or equal to the value returned by p2
.
p1
is greater than or equal to the value returned by p2
.
p1
is equal to the value returned by p2
.
p1
and p2
evaluates to true.
p1
or p2
evaluates to true.
p
does not evaluate to true.
t
to the goal g
.t
to the goal g
using the parameter set p
.apply_result
object.apply_result
object.apply_result
object returned by Z3.tactic_apply
.
apply_result_get_subgoal(c
, r, i) into a model for the original goal g
.
Where g
is the goal used to create r
using tactic_apply(c
, t, g).Solvers

Z3.mk_solver
if the logic is unknown or unsupported.Z3.solver_push
and Z3.solver_pop
, but it
will always solve each Z3.solver_check
from scratch.The solver contains a stack of assertions.
Z3.solver_pop
n
backtracking points.
Z3.solver_push
The functions Z3.solver_check
and Z3.solver_check_assumptions
should be
used to check whether the logical context is consistent or not.
The function Z3.solver_get_model
retrieves a model if the
assertions are not unsatisfiable (i.e., the result is not \c
L_FALSE) and model construction is enabled.
The function Z3.solver_get_proof
retrieves a proof if proof
generation was enabled when the context was created, and the
assertions are unsatisfiable (i.e., the result is L_FALSE)
.
The function Z3.solver_get_unsat_core
retrieves the subset of the
assumptions used in the unsatisfiability proof produced by Z3.
Z3.solver_check
Z3.solver_check
or Z3.solver_check_assumptions
The error handler is invoked if a model is not available because
the commands above were not invoked for the given solver, or if the result was L_FALSE
.
Z3.solver_check
or Z3.solver_check_assumptions
The error handler is invoked if proof generation is not enabled,
or if the commands above were not invoked for the given solver,
or if the result was different from L_FALSE
.
Z3.solver_check_assumptions
The unsat core is a subset of the assumptions a
.Z3.solver_check
and Z3.solver_check_assumptions
Statistics

s
.
Deprecated Injective functions API

Z3.assert_cnstr
, Z3.check_assumptions
, etc.Deprecated Constraints API

Z3.mk_solver_for_logic
Z3.check
, Z3.check_and_get_model
, Z3.check_assumptions
and Z3.push
.
Return TRUE
if the logic was changed successfully, and FALSE
otherwise.Z3.solver_push
The logical context can be viewed as a stack of contexts. The scope level is the number of elements on this stack. The stack of contexts is simulated using trail (undo) stacks.
Z3.pop
Z3.solver_pop
Restores the context from the top of the stack, and pops it off the
stack. Any changes to the logical context (by Z3.assert_cnstr
or
other functions) between the matching Z3.push
and pop
operators are flushed, and the context is completely restored to
what it was right before the Z3.push
.
Z3.push
Z3.solver_get_num_scopes
.It retrieves the number of scopes that have been pushed, but not yet popped.
Z3.solver_assert
After one assertion, the logical context may become inconsistent.
The functions Z3.check
or Z3.check_and_get_model
should be
used to check whether the logical context is consistent or not.
Z3.check
Z3.check_and_get_model
Z3.solver_check
If the logical context is not unsatisfiable (i.e., the return value is different from L_FALSE)
and model construction is enabled (see Z3.mk_config
),
then a valid model is returned. Otherwise, it is unsafe to use the returned model.
Z3.mk_config
).
Z3.check
Z3.solver_check
The function Z3.check_and_get_model
should be used when models are needed.
Z3.check_and_get_model
context >
ast array >
int > ast array > lbool * model * ast * int * ast array
Z3.solver_check_assumptions
If the logical context is not unsatisfiable (i.e., the return value is different from L_FALSE)
,
and model construction is enabled (see Z3.mk_config
),
then a valid model is returned. Otherwise, it is unsafe to use the returned model.
The function can be used for relying on Z3 to identify equal terms under the current set of assumptions. The array of terms and array of class identifiers should have the same length. The class identifiers are numerals that are assigned to the same value for their corresponding terms if the current context forces the terms to be equal. You cannot deduce that terms corresponding to different numerals must be all different, (especially when using nonconvex theories). All implied equalities are returned by this call. This means that two terms map to the same class identifier if and only if the current context implies that they are equal.
A sideeffect of the function is a satisfiability check. The function return L_FALSE if the current assertions are not satisfiable.
Z3.check_and_get_model
Z3.check
Deprecated Search control API

Z3.interrupt
instead.
Notifies the current check to abort and return.
This method should be called from a different thread
than the one performing the check.
Z3.solver_get_reason_unknown
If a call to Z3.check
or Z3.check_and_get_model
returns L_UNDEF,
use this facility to determine the more detailed cause of search failure.
Deprecated Labels API

Z3.del_literals
Z3.get_num_literals
Z3.get_label_symbol
Z3.get_literal
Z3.del_literals
Z3.get_num_literals
Z3.get_label_symbol
Z3.get_literal
Z3.del_literals
Z3.get_num_literals
Z3.get_label_symbol
Z3.get_literal
Z3.get_relevant_labels
Z3.get_relevant_labels
The disabled label is not going to be used when blocking the subsequent search.
Z3.block_literals
Deprecated Model API

Z3.model_get_num_consts
Z3.get_model_constants
.
Z3.get_model_constant
Z3.model_get_const_decl
get_model_constant c m i
]
Return the ith constant in the given model.
Z3.get_model_constants
.
Z3.model_get_num_funcs
A function interpretation is represented as a finite map and an 'else' value.
Each entry in the finite map represents the value of a function given a set of arguments.
Z3.model_get_func_decl
get_model_func_decl c m i
]
Return the declaration of the ith function in the given model.
Z3.get_model_num_funcs
Z3.model_eval
or Z3.model_get_func_interp
Z3.is_as_array
is_array_value c v
]
Determine whether the term encodes an array value.
A term encodes an array value if it is a nested sequence of
applications of store on top of a constant array.
The indices to the stores have to be values (for example, integer constants)
so that equality between the indices can be evaluated.
Array values are useful for representing interpretations for arrays.
Return the number of entries mapping to nondefault values of the array.
context >
model >
ast >
ast array > ast array > ast array * ast array * ast
Z3.get_as_array_func_decl
get_array_value c v
]
An array values is represented as a dictionary plus a
default (else) value. This function returns the array graph.
get_model_func_else c m i
]
Return the 'else' value of the ith function interpretation in the given model.
A function interpretation is represented as a finite map and an 'else' value.
Z3.get_model_funcs
.
Z3.get_model_num_funcs
Z3.get_model_func_num_entries
Z3.get_model_func_entry_num_args
Z3.get_model_func_entry_arg
get_model_func_num_entries c m i
]
Return the number of entries of the ith function interpretation in the given model.
A function interpretation is represented as a finite map and an 'else' value.
Z3.get_model_funcs
.
Z3.get_model_num_funcs
Z3.get_model_func_else
Z3.get_model_func_entry_num_args
Z3.get_model_func_entry_arg
get_model_func_entry_num_args c m i j
]
Return the number of arguments of the jth entry of the ith function interpretation in the given
model.
A function interpretation is represented as a finite map and an 'else' value. This function returns the jth entry of this map.
An entry represents the value of a function given a set of arguments.
Z3.get_model_funcs
.
Z3.get_model_num_funcs
Z3.get_model_func_num_entries
Z3.get_model_func_entry_arg
get_model_func_entry_arg c m i j k
]
Return the kth argument of the jth entry of the ith function interpretation in the given
model.
A function interpretation is represented as a finite map and an 'else' value. This function returns the jth entry of this map.
An entry represents the value of a function given a set of arguments.
Z3.get_model_funcs
.
Z3.get_model_num_funcs
Z3.get_model_func_num_entries
Z3.get_model_func_entry_num_args
get_model_func_entry_value c m i j
]
Return the return value of the jth entry of the ith function interpretation in the given
model.
A function interpretation is represented as a finite map and an 'else' value. This function returns the jth entry of this map.
An entry represents the value of a function given a set of arguments.
Z3.get_model_funcs
.
Z3.get_model_num_funcs
Z3.get_model_func_num_entries
Z3.model_eval
eval c m t
]
Evaluate the AST node t
in the given model.
Return a pair: Boolean and value. The Boolean is true if the term was successfully evaluated.
The evaluation may fail for the following reasons:
t
contains a quantifier.
m
is partial, that is, it doesn't have a complete interpretation for uninterpreted functions.
That is, the option MODEL_PARTIAL=true was used.
t
is type incorrect.Z3.model_eval
and Z3.substitute_vars
Provides direct way to evaluate declarations
without going over terms.
Deprecated String conversion API

This function is mainly used for debugging purposes. It displays
the internal structure of a logical context.
Z3.stats_to_string
when using the new solver API.
This function is mainly used for debugging purposes. It displays
statistics of the search activity.
This function can be used for debugging purposes. It returns a conjunction
of formulas that are assigned to true in the current context.
This conjunction will contain not only the assertions that are set to true
under the current assignment, but will also include additional literals
if there has been a call to Z3.check
or Z3.check_and_get_model
.
ML Extensions

mk_context_x configs
] is a shorthand for the context with configurations in configs
. get_app_args c a
] is the array of arguments of an application. If t
is a constant, then the array is empty.
Z3.get_app_num_args
Z3.get_app_arg
get_app_args c d
] is the array of parameters of d
.
Z3.get_domain_size
Z3.get_domain
get_array_sort c t
] is the domain and the range of t
.
Z3.get_array_sort_domain
Z3.get_array_sort_range
get_tuple_sort c ty
] is the pair (mk_decl, fields)
where mk_decl
is the constructor declaration of ty
, and fields
is the array of fields in ty
.
Z3.get_tuple_sort_mk_decl
Z3.get_tuple_sort_num_fields
Z3.get_tuple_sort_field_decl
type
datatype_constructor_refined = {

constructor : 

recognizer : 

accessors : 
datatype_constructor_refined
] is the refinement of a datatype constructor.
It contains the constructor declaration, recognizer, and list of accessor functions.
get_datatype_sort c ty
] is the array of triples (constructor, recognizer, fields)
where constructor
is the constructor declaration of ty
, recognizer
is the recognizer for the constructor
, and fields
is the array of fields in ty
.
Z3.get_datatype_sort_num_constructors
Z3.get_datatype_sort_constructor
Z3.get_datatype_sort_recognizer
Z3.get_datatype_sort_constructor_accessor
context > sort > datatype_constructor_refined array
val get_model_constants : context > model > func_decl array
get_model_constants c m
] is the array of constants in the model m
.
Z3.get_model_num_constants
Z3.get_model_constant
get_model_func_entry c m i j
] is the j
'th entry in the i
'th function in the model m
.
Z3.get_model_func_entry_num_args
Z3.get_model_func_entry_arg
Z3.get_model_func_entry_value
get_model_func_entries c m i
] is the array of entries in the i
'th function in the model m
.
Z3.get_model_func_num_entries
Z3.get_model_func_entry
get_model_funcs c m
] is the array of functions in the model m
. Each function is represented by the triple (decl, entries, else)
, where decl
is the declaration name for the function, entries
is the array of entries in the function, and else
is the default (else) value for the function.
Z3.get_model_num_funcs
Z3.get_model_func_decl
Z3.get_model_func_entries
Z3.get_model_func_else
get_smtlib_formulas c
] is the array of formulas created by a preceding call to Z3.parse_smtlib_string
or Z3.parse_smtlib_file
.
Recommend use Z3.parse_smtlib_string_x
or Z3.parse_smtlib_file_x
for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_string_x
Z3.parse_smtlib_file_x
Z3.parse_smtlib_string
Z3.parse_smtlib_file
Z3.get_smtlib_num_formulas
Z3.get_smtlib_formula
get_smtlib_assumptions c
] is the array of assumptions created by a preceding call to Z3.parse_smtlib_string
or Z3.parse_smtlib_file
.
Recommend use Z3.parse_smtlib_string_x
or Z3.parse_smtlib_file_x
for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_string_x
Z3.parse_smtlib_file_x
Z3.parse_smtlib_string
Z3.parse_smtlib_file
Z3.get_smtlib_num_assumptions
Z3.get_smtlib_assumption
get_smtlib_decls c
] is the array of declarations created by a preceding call to Z3.parse_smtlib_string
or Z3.parse_smtlib_file
.
Recommend use Z3.parse_smtlib_string_x
or Z3.parse_smtlib_file_x
for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_string_x
Z3.parse_smtlib_file_x
Z3.parse_smtlib_string
Z3.parse_smtlib_file
Z3.get_smtlib_num_decls
Z3.get_smtlib_decl
get_smtlib_parse_results c
] is the triple (get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c)
.
Recommend use Z3.parse_smtlib_string_x
or Z3.parse_smtlib_file_x
for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_string_x
Z3.parse_smtlib_file_x
Z3.parse_smtlib_string
Z3.parse_smtlib_file
Z3.get_smtlib_formulas
Z3.get_smtlib_assumptions
Z3.get_smtlib_decls
context >
string >
symbol array >
sort array > symbol array > func_decl array > ast
parse_smtlib_string_formula c ...
] calls (parse_smtlib_string c ...)
and returns the single formula produced.
Recommended for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_file_formula
Z3.parse_smtlib_string_x
context >
string >
symbol array >
sort array > symbol array > func_decl array > ast
parse_smtlib_file_formula c ...
] calls (parse_smtlib_file c ...)
and returns the single formula produced.
Recommended for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_file_formula
Z3.parse_smtlib_file_x
context >
string >
symbol array >
sort array >
symbol array >
func_decl array > ast array * ast array * func_decl array
parse_smtlib_string_x c ...
] is (parse_smtlib_string c ...; get_smtlib_parse_results c)
Recommended for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_file_x
Z3.parse_smtlib_string
Z3.get_smtlib_parse_results
context >
string >
symbol array >
sort array >
symbol array >
func_decl array > ast array * ast array * func_decl array
parse_smtlib_file_x c ...
] is (parse_smtlib_file c ...; get_smtlib_parse_results c)
Recommended for functional style interface to the SMTLIB parser.
Z3.parse_smtlib_string_x
Z3.parse_smtlib_file
Z3.get_smtlib_parse_results
 
Symbol_int of 
 
Symbol_string of 
 
Symbol_unknown 
symbol_refined
] is the refinement of a Z3.symbol
.
Z3.symbol_refine
Z3.get_symbol_kind
symbol_refine c s
] is the refined symbol of s
.
Z3.symbol_refined
Z3.get_symbol_kind
sort_refined
] is the refinement of a Z3.sort
.
Z3.sort_refine
Z3.get_sort_kind
 
Sort_uninterpreted of 
 
Sort_bool 
 
Sort_int 
 
Sort_real 
 
Sort_bv of 
 
Sort_array of 
 
Sort_datatype of 
 
Sort_relation 
 
Sort_finite_domain 
 
Sort_unknown of 
 
Forall 
 
Exists 
 
Numeral_small of 
 
Numeral_large of 
numeral_refined
] is the refinement of a numeral .
Numerals whose fractional representation can be fit with
64 bit integers are treated as small.
 
Term_app of 
 
Term_quantifier of 
 
Term_numeral of 
 
Term_var of 
mk_theory c name
] create a custom theory.set_delete_callback th cb
] set callback when theory gets deleted.set_reduce_app_callback th cb
] set callback for simplifying theory terms.set_reduce_eq_callback th cb
] set callback for simplifying equalities over theory terms.set_reduce_distinct_callback th cb
] set callback for simplifying disequalities over theory terms.set_new_app_callback th cb
] set callback for registering new application.set_new_elem_callback th cb
] set callback for registering new element.
set_init_search_callback th cb
] set callback when Z3 starts searching for a satisfying assignment.set_push_callback th cb
] set callback for a logical context push.set_pop_callback th cb
] set callback for a logical context pop.set_restart_callback th cb
] set callback for search restart.theory > (unit > unit) > unit
val set_final_check_callback : theory > (unit > bool) > unit
val set_new_eq_callback : theory > (ast > ast > unit) > unit
val set_new_diseq_callback : theory > (ast > ast > unit) > unit
val set_new_assignment_callback : theory > (ast > bool > unit) > unit
val set_new_relevant_callback : theory > (ast > unit) > unit