Index of values


A
add [Z3.Optimize]
Assert a constraints into the optimize solver.
add [Z3.Fixedpoint]
Assert a constraints into the fixedpoint solver.
add [Z3.Solver]
Assert a constraint (or multiple) into the solver.
add [Z3.Goal]
Adds the constraints to the given goal.
add_bool [Z3.Params]
Adds a parameter setting.
add_cover [Z3.Fixedpoint]
Add <tt>property</tt> about the <tt>predicate</tt>.
add_fact [Z3.Fixedpoint]
Add table fact to the fixedpoint solver.
add_float [Z3.Params]
Adds a parameter setting.
add_int [Z3.Params]
Adds a parameter setting.
add_rule [Z3.Fixedpoint]
Add rule into the fixedpoint solver.
add_soft [Z3.Optimize]
Asssert a soft constraint.
add_symbol [Z3.Params]
Adds a parameter setting.
and_ [Z3.Probe]
Create a probe that evaluates to "true" when both of two probes evaluate to "true".
and_then [Z3.Tactic]
Create a tactic that applies one tactic to a Goal and then another one to every subgoal produced by the first one.
append [Z3.Log]
Appends a user-provided string to the interaction log.
apply [Z3.Tactic]
Apply the tactic to the goal.
apply [Z3.Probe]
Execute the probe over the goal.
apply [Z3.FuncDecl]
Create expression that applies function to arguments.
as_expr [Z3.Goal]
Goal to BoolExpr conversion.
assert_and_track [Z3.Solver]
* Assert a constraint (c) into the solver, and track it (in the unsat) core * using the Boolean constant p.
assert_and_track_l [Z3.Solver]
* Assert multiple constraints (cs) into the solver, and track them (in the * unsat) core * using the Boolean constants in ps.
ast_kind_of_int [Z3enums]
ast_of_expr [Z3.Expr]
ast_of_func_decl [Z3.FuncDecl]
ast_of_pattern [Z3.Quantifier.Pattern]
ast_of_sort [Z3.Sort]
ast_print_mode_of_int [Z3enums]

B
benchmark_to_smtstring [Z3.SMT]
Convert a benchmark into an SMT-LIB formatted string.
build [Z3.Version]
The build version.

C
check [Z3.Optimize]
Checks whether the assertions in the context are satisfiable and solves objectives.
check [Z3.Solver]
Checks whether the assertions in the solver are consistent or not.
check_interpolant [Z3.Interpolation]
Check the correctness of an interpolant.
close [Z3.Log]
Closes the interaction log.
compare [Z3.Expr]
Object Comparison.
compare [Z3.AST]
Object Comparison.
compute_interpolant [Z3.Interpolation]
Computes an interpolant.
cond [Z3.Tactic]
Create a tactic that applies a tactic to a given goal if the probe evaluates to true and another tactic otherwise.
const [Z3.Probe]
Create a probe that always evaluates to a float value.
contains [Z3.AST.ASTMap]
Checks whether the map contains a key.
convert_model [Z3.Tactic.ApplyResult]
Convert a model for a subgoal into a model for the original goal g, that the ApplyResult was obtained from.

D
decl_kind_of_int [Z3enums]
disable_trace [Z3]
Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode.

E
enable_trace [Z3]
Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode.
eq [Z3.Probe]
Create a probe that evaluates to "true" when the value returned by the first argument is equal the value returned by second argument
equal [Z3.Expr]
Comparison operator.
equal [Z3.FuncDecl]
Comparison operator.
equal [Z3.Sort]
Comparison operator.
equal [Z3.AST]
Comparison operator.
erase [Z3.AST.ASTMap]
Erases the key from the map.
error_code_of_int [Z3enums]
eval [Z3.Model]
Evaluates an expression in the current model.
evaluate [Z3.Model]
Alias for eval.
expr_of_ast [Z3.Expr]
expr_of_quantifier [Z3.Quantifier]

F
fail [Z3.Tactic]
Create a tactic always fails.
fail_if [Z3.Tactic]
Create a tactic that fails if the probe evaluates to false.
fail_if_not_decided [Z3.Tactic]
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').
find [Z3.AST.ASTMap]
Finds the value associated with the key.

G
ge [Z3.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
get [Z3.Statistics]
The value of a particular statistical counter.
get [Z3.AST.ASTVector]
Retrieves the i-th object in the vector.
get_accessor_decls [Z3.Datatype.Constructor]
The function declarations of the accessors
get_accessors [Z3.Datatype]
The constructor accessors.
get_answer [Z3.Fixedpoint]
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.
get_args [Z3.Model.FuncInterp.FuncEntry]
The arguments of the function entry.
get_args [Z3.Expr]
The arguments of the expression.
get_arity [Z3.Model.FuncInterp]
The arity of the function interpretation
get_arity [Z3.Relation]
The arity of the relation sort.
get_arity [Z3.FuncDecl]
The arity of the function declaration
get_assertions [Z3.Fixedpoint]
Retrieve set of assertions added to fixedpoint context.
get_assertions [Z3.Solver]
The set of asserted formulas.
get_ast [Z3.FuncDecl.Parameter]
The AST value of the parameter.
get_ast_kind [Z3.AST]
The kind of the AST.
get_big_int [Z3.Arithmetic.Integer]
Get a big_int from an integer numeral
get_body [Z3.Quantifier]
The body of the quantifier.
get_bool_value [Z3.Boolean]
Indicates whether the expression is the true or false expression or something else (L_UNDEF).
get_bound_variable_names [Z3.Quantifier]
The symbols for the bound variables.
get_bound_variable_sorts [Z3.Quantifier]
The sorts of the bound variables.
get_column_sorts [Z3.Relation]
The sorts of the columns of the relation sort.
get_cons_decl [Z3.Z3List]
The declaration of the cons function of this list sort.
get_const [Z3.Enumeration]
Retrieves the inx'th constant in the enumeration.
get_const_decl [Z3.Enumeration]
Retrieves the inx'th constant declaration in the enumeration.
get_const_decls [Z3.Model]
The function declarations of the constants in the model.
get_const_decls [Z3.Enumeration]
The function declarations of the constants in the enumeration.
get_const_interp [Z3.Model]
Retrieves the interpretation (the assignment) of a func_decl in the model.
get_const_interp_e [Z3.Model]
Retrieves the interpretation (the assignment) of an expression in the model.
get_constructor_decl [Z3.Datatype.Constructor]
The function declaration of the constructor.
get_constructors [Z3.Datatype]
The constructors.
get_consts [Z3.Enumeration]
The constants in the enumeration.
get_cover_delta [Z3.Fixedpoint]
Retrieve the cover of a predicate.
get_decl_kind [Z3.FuncDecl]
The kind of the function declaration.
get_decls [Z3.Model]
All symbols that have an interpretation in the model.
get_denominator [Z3.Arithmetic.Real]
The denominator of a rational numeral.
get_depth [Z3.Goal]
The depth of the goal.
get_domain [Z3.Z3Array]
The domain of the array sort.
get_domain [Z3.FuncDecl]
The domain of the function declaration
get_domain_size [Z3.FuncDecl]
The size of the domain of the function declaration FuncDecl.get_arity
get_ebits [Z3.FloatingPoint]
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
get_else [Z3.Model.FuncInterp]
The (symbolic) `else' value of the function interpretation.
get_entries [Z3.Statistics]
The data entries.
get_entries [Z3.Model.FuncInterp]
The entries in the function interpretation
get_field_decls [Z3.Tuple]
The field declarations.
get_float [Z3.Statistics.Entry]
The float-value of the entry.
get_float [Z3.FuncDecl.Parameter]
The float value of the parameter.
get_formulas [Z3.Goal]
The formulas in the goal.
get_func_decl [Z3.Expr]
The function declaration of the function that is applied in this expression.
get_func_decl [Z3.FuncDecl.Parameter]
The FunctionDeclaration value of the parameter.
get_func_decls [Z3.Model]
The function declarations of the function interpretations in the model.
get_func_interp [Z3.Model]
Retrieves the interpretation (the assignment) of a non-constant func_decl in the model.
get_global_param [Z3]
Get a global (or module) parameter.
get_head_decl [Z3.Z3List]
The declaration of the head function of this list sort.
get_help [Z3.Optimize]
A string that describes all available optimize solver parameters.
get_help [Z3.Fixedpoint]
A string that describes all available fixedpoint solver parameters.
get_help [Z3.Solver]
A string that describes all available solver parameters.
get_help [Z3.Tactic]
A string containing a description of parameters accepted by the tactic.
get_id [Z3.FuncDecl]
Returns a unique identifier for the function declaration.
get_id [Z3.Sort]
Returns a unique identifier for the sort.
get_id [Z3.AST]
A unique identifier for the AST (unique among all ASTs).
get_index [Z3.Quantifier]
The de-Burijn index of a bound variable.
get_int [Z3.Statistics.Entry]
The int-value of the entry.
get_int [Z3.BitVector]
Retrieve the int value.
get_int [Z3.Arithmetic.Integer]
Retrieve the int value.
get_int [Z3.FuncDecl.Parameter]
The int value of the parameter.
get_int [Z3.Symbol]
The int value of the symbol.
get_interpolant [Z3.Interpolation]
Gets an interpolant.
get_interpolation_profile [Z3.Interpolation]
Retrieves an interpolation profile.
get_is_cons_decl [Z3.Z3List]
The declaration of the isCons function of this list sort.
get_is_nil_decl [Z3.Z3List]
The declaration of the isNil function of this list sort.
get_key [Z3.Statistics.Entry]
The key of the entry.
get_keys [Z3.Statistics]
The statistical counters.
get_keys [Z3.AST.ASTMap]
The keys stored in the map.
get_kind [Z3.Params.ParamDescrs]
Retrieve kind of parameter.
get_kind [Z3.FuncDecl.Parameter]
The kind of the parameter.
get_lower [Z3.Optimize]
Retrieve lower bound in current model for handle
get_mk_decl [Z3.Tuple]
The constructor function of the tuple.
get_model [Z3.Optimize]
Retrieve model from satisfiable context
get_model [Z3.Solver]
The model of the last Check.
get_name [Z3.FuncDecl]
The name of the function declaration
get_name [Z3.Sort]
The name of the sort
get_names [Z3.Params.ParamDescrs]
Retrieve all names of parameters.
get_nil_decl [Z3.Z3List]
The declaration of the nil function of this list sort.
get_no_patterns [Z3.Quantifier]
The no-patterns.
get_num_args [Z3.Model.FuncInterp.FuncEntry]
The number of arguments of the entry.
get_num_args [Z3.Expr]
The number of arguments of the expression.
get_num_assertions [Z3.Solver]
The number of assertions in the solver.
get_num_bound [Z3.Quantifier]
The number of bound variables.
get_num_constructors [Z3.Datatype]
The number of constructors of the datatype sort.
get_num_consts [Z3.Model]
The number of constant interpretations in the model.
get_num_entries [Z3.Model.FuncInterp]
The number of entries in the function interpretation.
get_num_exprs [Z3.Goal]
The number of formulas, subformulas and terms in the goal.
get_num_fields [Z3.Tuple]
The number of fields in the tuple.
get_num_fields [Z3.Datatype.Constructor]
The number of fields of the constructor.
get_num_funcs [Z3.Model]
The number of function interpretations in the model.
get_num_levels [Z3.Fixedpoint]
Retrieve the number of levels explored for a given predicate.
get_num_no_patterns [Z3.Quantifier]
The number of no-patterns.
get_num_parameters [Z3.FuncDecl]
The number of parameters of the function declaration
get_num_patterns [Z3.Quantifier]
The number of patterns.
get_num_probes [Z3.Probe]
The number of supported Probes.
get_num_scopes [Z3.Solver]
The current number of backtracking points (scopes).
get_num_smtlib_assumptions [Z3.SMT]
The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_num_smtlib_decls [Z3.SMT]
The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_num_smtlib_formulas [Z3.SMT]
The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_num_smtlib_sorts [Z3.SMT]
The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_num_sorts [Z3.Model]
The number of uninterpreted sorts that the model has an interpretation for.
get_num_subgoals [Z3.Tactic.ApplyResult]
The number of Subgoals.
get_num_tactics [Z3.Tactic]
The number of supported tactics.
get_num_terms [Z3.Quantifier.Pattern]
The number of terms in the pattern.
get_numeral_exponent_int [Z3.FloatingPoint]
Return the exponent value of a floating-point numeral as a signed integer
get_numeral_exponent_string [Z3.FloatingPoint]
Return the exponent value of a floating-point numeral as a string
get_numeral_sign [Z3.FloatingPoint]
Retrieves the sign of a floating-point literal.
get_numeral_significand_string [Z3.FloatingPoint]
Return the significand value of a floating-point numeral as a string.
get_numeral_significand_uint [Z3.FloatingPoint]
Return the significand value of a floating-point numeral as a uint64.
get_numerator [Z3.Arithmetic.Real]
The numerator of a rational numeral.
get_param_descrs [Z3.Optimize]
Retrieves parameter descriptions for Optimize solver.
get_param_descrs [Z3.Fixedpoint]
Retrieves parameter descriptions for Fixedpoint solver.
get_param_descrs [Z3.Solver]
Retrieves parameter descriptions for solver.
get_param_descrs [Z3.Tactic]
Retrieves parameter descriptions for Tactics.
get_parameters [Z3.FuncDecl]
The parameters of the function declaration
get_patterns [Z3.Quantifier]
The patterns.
get_precision [Z3.Goal]
The precision of the goal.
get_probe_description [Z3.Probe]
Returns a string containing a description of the probe with the given name.
get_probe_names [Z3.Probe]
The names of all supported Probes.
get_proof [Z3.Solver]
The proof of the last Check.
get_range [Z3.Z3Array]
The range of the array sort.
get_range [Z3.FuncDecl]
The range of the function declaration
get_ratio [Z3.Arithmetic.Real]
Get a ratio from a real numeral
get_rational [Z3.FuncDecl.Parameter]
The rational string value of the parameter.
get_reason_unknown [Z3.Optimize]
Retrieve explanation why optimize engine returned status Unknown.
get_reason_unknown [Z3.Fixedpoint]
Retrieve explanation why fixedpoint engine returned status Unknown.
get_reason_unknown [Z3.Solver]
A brief justification of why the last call to Check returned UNKNOWN.
get_recognizers [Z3.Datatype]
The recognizers.
get_rules [Z3.Fixedpoint]
Retrieve set of rules added to fixedpoint context.
get_sbits [Z3.FloatingPoint]
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
get_simplify_help [Z3.Expr]
A string describing all available parameters to Expr.Simplify.
get_simplify_parameter_descrs [Z3.Expr]
Retrieves parameter descriptions for simplifier.
get_size [Z3.Statistics]
The number of statistical data.
get_size [Z3.Goal]
The number of formulas in the goal.
get_size [Z3.BitVector]
The size of a bit-vector sort.
get_size [Z3.FiniteDomain]
The size of the finite domain sort.
get_size [Z3.Params.ParamDescrs]
The size of the ParamDescrs.
get_size [Z3.AST.ASTMap]
The size of the map
get_size [Z3.AST.ASTVector]
The size of the vector
get_smtlib_assumptions [Z3.SMT]
The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_smtlib_decls [Z3.SMT]
The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_smtlib_formulas [Z3.SMT]
The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_smtlib_sorts [Z3.SMT]
The sort declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
get_sort [Z3.Expr]
The Sort of the term.
get_sort [Z3.FuncDecl.Parameter]
The Sort value of the parameter.
get_sort_kind [Z3.Sort]
The kind of the sort.
get_sorts [Z3.Model]
The uninterpreted sorts that the model has an interpretation for.
get_statistics [Z3.Optimize]
Retrieve statistics information from the last call to check
get_statistics [Z3.Fixedpoint]
Retrieve statistics information from the last call to #Z3_fixedpoint_query.
get_statistics [Z3.Solver]
Solver statistics.
get_string [Z3.Symbol]
The string value of the symbol.
get_subgoal [Z3.Tactic.ApplyResult]
Retrieves a subgoal from the apply_result.
get_subgoals [Z3.Tactic.ApplyResult]
Retrieves the subgoals from the apply_result.
get_symbol [Z3.FuncDecl.Parameter]
The Symbol.Symbol value of the parameter.
get_tactic_description [Z3.Tactic]
Returns a string containing a description of the tactic with the given name.
get_tactic_names [Z3.Tactic]
The names of all supported tactics.
get_tail_decl [Z3.Z3List]
The declaration of the tail function of this list sort.
get_terms [Z3.Quantifier.Pattern]
The terms in the pattern.
get_tester_decl [Z3.Enumeration]
Retrieves the inx'th tester/recognizer declaration in the enumeration.
get_tester_decl [Z3.Datatype.Constructor]
The function declaration of the tester.
get_tester_decls [Z3.Enumeration]
The test predicates for the constants in the enumeration.
get_unsat_core [Z3.Solver]
The unsat core of the last Check.
get_upper [Z3.Optimize]
Retrieve upper bound in current model for handle
get_value [Z3.Model.FuncInterp.FuncEntry]
Return the (symbolic) value of this entry.
get_weight [Z3.Quantifier]
The weight of the quantifier.
global_param_reset_all [Z3]
goal_prec_of_int [Z3enums]
gt [Z3.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

H
hash [Z3.AST]
The AST's hash code.

I
insert [Z3.AST.ASTMap]
Stores or replaces a new key/value pair in the map.
int_of_ast_kind [Z3enums]
Convert ast_kind to int
int_of_ast_print_mode [Z3enums]
Convert ast_print_mode to int
int_of_decl_kind [Z3enums]
Convert decl_kind to int
int_of_error_code [Z3enums]
Convert error_code to int
int_of_goal_prec [Z3enums]
Convert goal_prec to int
int_of_lbool [Z3enums]
Convert lbool to int
int_of_param_kind [Z3enums]
Convert param_kind to int
int_of_parameter_kind [Z3enums]
Convert parameter_kind to int
int_of_sort_kind [Z3enums]
Convert sort_kind to int
int_of_symbol_kind [Z3enums]
Convert symbol_kind to int
interrupt [Z3.Tactic]
Interrupt the execution of a Z3 procedure.
is_Transitivity_star [Z3.Proof]
Indicates whether the term is a proof by condensed transitivity of a relation
is_abs [Z3.FloatingPoint]
Indicates whether an expression is a floating-point abs expression
is_add [Z3.FloatingPoint]
Indicates whether an expression is a floating-point add expression
is_add [Z3.Arithmetic]
Indicates whether the term is addition (binary)
is_algebraic_number [Z3.Arithmetic]
Indicates whether the term is an algebraic number
is_and [Z3.Boolean]
Indicates whether the term is an n-ary conjunction
is_and_elimination [Z3.Proof]
Indicates whether the term is a proof by elimination of AND
is_apply_def [Z3.Proof]
Indicates whether the term is a proof for application of a definition
is_arithmetic_numeral [Z3.Arithmetic]
Indicates whether the term is an arithmetic numeral.
is_array [Z3.Z3Array]
Indicates whether the term is of an array sort.
is_array_map [Z3.Z3Array]
Indicates whether the term is an array map.
is_as_array [Z3.Z3Array]
Indicates whether the term is an as-array term.
is_asserted [Z3.Proof]
Indicates whether the term is a proof for a fact asserted by the user.
is_bool [Z3.Boolean]
Indicates whether the term has Boolean sort.
is_bv [Z3.BitVector]
Indicates whether the terms is of bit-vector sort.
is_bv2int [Z3.BitVector]
Indicates whether the term is a coercion from integer to bit-vector This function is not supported by the decision procedures.
is_bv_SRem [Z3.BitVector]
Indicates whether the term is a bit-vector signed remainder (binary)
is_bv_add [Z3.BitVector]
Indicates whether the term is a bit-vector addition (binary)
is_bv_and [Z3.BitVector]
Indicates whether the term is a bit-wise AND
is_bv_bit0 [Z3.BitVector]
Indicates whether the term is a one-bit bit-vector with value zero
is_bv_bit1 [Z3.BitVector]
Indicates whether the term is a one-bit bit-vector with value one
is_bv_carry [Z3.BitVector]
Indicates whether the term is a bit-vector carry Compute the carry bit in a full-adder.
is_bv_comp [Z3.BitVector]
Indicates whether the term is a bit-vector comparison
is_bv_concat [Z3.BitVector]
Indicates whether the term is a bit-vector concatenation (binary)
is_bv_extract [Z3.BitVector]
Indicates whether the term is a bit-vector extraction
is_bv_mul [Z3.BitVector]
Indicates whether the term is a bit-vector multiplication (binary)
is_bv_nand [Z3.BitVector]
Indicates whether the term is a bit-wise NAND
is_bv_nor [Z3.BitVector]
Indicates whether the term is a bit-wise NOR
is_bv_not [Z3.BitVector]
Indicates whether the term is a bit-wise NOT
is_bv_numeral [Z3.BitVector]
Indicates whether the term is a bit-vector numeral
is_bv_or [Z3.BitVector]
Indicates whether the term is a bit-wise OR
is_bv_reduceand [Z3.BitVector]
Indicates whether the term is a bit-vector reduce AND
is_bv_reduceor [Z3.BitVector]
Indicates whether the term is a bit-vector reduce OR
is_bv_repeat [Z3.BitVector]
Indicates whether the term is a bit-vector repetition
is_bv_rotateleft [Z3.BitVector]
Indicates whether the term is a bit-vector rotate left
is_bv_rotateleftextended [Z3.BitVector]
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.
is_bv_rotateright [Z3.BitVector]
Indicates whether the term is a bit-vector rotate right
is_bv_rotaterightextended [Z3.BitVector]
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.
is_bv_sdiv [Z3.BitVector]
Indicates whether the term is a bit-vector signed division (binary)
is_bv_sdiv0 [Z3.BitVector]
Indicates whether the term is a bit-vector signed division by zero
is_bv_sge [Z3.BitVector]
Indicates whether the term is a signed bit-vector greater-than-or-equal
is_bv_sgt [Z3.BitVector]
Indicates whether the term is a signed bit-vector greater-than
is_bv_shiftleft [Z3.BitVector]
Indicates whether the term is a bit-vector shift left
is_bv_shiftrightarithmetic [Z3.BitVector]
Indicates whether the term is a bit-vector arithmetic shift left
is_bv_shiftrightlogical [Z3.BitVector]
Indicates whether the term is a bit-vector logical shift right
is_bv_signextension [Z3.BitVector]
Indicates whether the term is a bit-vector sign extension
is_bv_sle [Z3.BitVector]
Indicates whether the term is a signed bit-vector less-than-or-equal
is_bv_slt [Z3.BitVector]
Indicates whether the term is a signed bit-vector less-than
is_bv_smod [Z3.BitVector]
Indicates whether the term is a bit-vector signed modulus
is_bv_smod0 [Z3.BitVector]
Indicates whether the term is a bit-vector signed modulus by zero
is_bv_srem0 [Z3.BitVector]
Indicates whether the term is a bit-vector signed remainder by zero
is_bv_sub [Z3.BitVector]
Indicates whether the term is a bit-vector subtraction (binary)
is_bv_udiv [Z3.BitVector]
Indicates whether the term is a bit-vector unsigned division (binary)
is_bv_udiv0 [Z3.BitVector]
Indicates whether the term is a bit-vector unsigned division by zero
is_bv_uge [Z3.BitVector]
Indicates whether the term is an unsigned bit-vector greater-than-or-equal
is_bv_ugt [Z3.BitVector]
Indicates whether the term is an unsigned bit-vector greater-than
is_bv_ule [Z3.BitVector]
Indicates whether the term is an unsigned bit-vector less-than-or-equal
is_bv_ult [Z3.BitVector]
Indicates whether the term is an unsigned bit-vector less-than
is_bv_uminus [Z3.BitVector]
Indicates whether the term is a bit-vector unary minus
is_bv_urem [Z3.BitVector]
Indicates whether the term is a bit-vector unsigned remainder (binary)
is_bv_urem0 [Z3.BitVector]
Indicates whether the term is a bit-vector unsigned remainder by zero
is_bv_xnor [Z3.BitVector]
Indicates whether the term is a bit-wise XNOR
is_bv_xor [Z3.BitVector]
Indicates whether the term is a bit-wise XOR
is_bv_xor3 [Z3.BitVector]
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)
is_bv_zeroextension [Z3.BitVector]
Indicates whether the term is a bit-vector zero extension
is_clone [Z3.Relation]
Indicates whether the term is a relational clone (copy)
is_cnf_star [Z3.Proof]
Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
is_commutativity [Z3.Proof]
Indicates whether the term is a proof by commutativity
is_complement [Z3.Relation]
Indicates whether the term is the complement of a relation
is_complement [Z3.Set]
Indicates whether the term is set complement
is_const [Z3.Expr]
Indicates whether the term represents a constant.
is_constant_array [Z3.Z3Array]
Indicates whether the term is a constant array.
is_decided_sat [Z3.Goal]
Indicates whether the goal is empty, and it is precise or the product of an under approximation.
is_decided_unsat [Z3.Goal]
Indicates whether the goal contains `false', and it is precise or the product of an over approximation.
is_def_axiom [Z3.Proof]
Indicates whether the term is a proof for Tseitin-like axioms
is_def_intro [Z3.Proof]
Indicates whether the term is a proof for introduction of a name
is_default_array [Z3.Z3Array]
Indicates whether the term is a default array.
is_der [Z3.Proof]
Indicates whether the term is a proof for destructive equality resolution
is_difference [Z3.Set]
Indicates whether the term is set difference
is_distinct [Z3.Boolean]
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
is_distributivity [Z3.Proof]
Indicates whether the term is a distributivity proof object.
is_div [Z3.FloatingPoint]
Indicates whether an expression is a floating-point div expression
is_div [Z3.Arithmetic]
Indicates whether the term is division (binary)
is_elim_unused_vars [Z3.Proof]
Indicates whether the term is a proof for elimination of unused variables.
is_empty [Z3.Relation]
Indicates whether the term is an empty relation
is_eq [Z3.FloatingPoint]
Indicates whether an expression is a floating-point eq expression
is_eq [Z3.Boolean]
Indicates whether the term is an equality predicate.
is_existential [Z3.Quantifier]
Indicates whether the quantifier is existential.
is_expr [Z3.AST]
Indicates whether the AST is an Expr
is_false [Z3.Boolean]
Indicates whether the term is the constant false.
is_filter [Z3.Relation]
Indicates whether the term is a relation filter
is_finite_domain [Z3.FiniteDomain]
Indicates whether the term is of an array sort.
is_float [Z3.Statistics.Entry]
True if the entry is float-valued.
is_fma [Z3.FloatingPoint]
Indicates whether an expression is a floating-point fma expression
is_fp [Z3.FloatingPoint]
Indicates whether the terms is of floating-point sort.
is_fprm [Z3.FloatingPoint.RoundingMode]
Indicates whether the terms is of floating-point rounding mode sort.
is_func_decl [Z3.AST]
Indicates whether the AST is a func_decl
is_garbage [Z3.Goal]
Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
is_ge [Z3.Arithmetic]
Indicates whether the term is a greater-than-or-equal
is_geq [Z3.FloatingPoint]
Indicates whether an expression is a floating-point geqexpression
is_goal [Z3.Proof]
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
is_gt [Z3.FloatingPoint]
Indicates whether an expression is a floating-point gt expression
is_gt [Z3.Arithmetic]
Indicates whether the term is a greater-than
is_hypothesis [Z3.Proof]
Indicates whether the term is a hypthesis marker.
is_idiv [Z3.Arithmetic]
Indicates whether the term is integer division (binary)
is_iff [Z3.Boolean]
Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
is_iff_false [Z3.Proof]
Indicates whether the term is a proof by iff-false
is_iff_oeq [Z3.Proof]
Indicates whether the term is a proof iff-oeq
is_iff_true [Z3.Proof]
Indicates whether the term is a proof by iff-true
is_implies [Z3.Boolean]
Indicates whether the term is an implication
is_inconsistent [Z3.Goal]
Indicates whether the goal contains `false'.
is_int [Z3.Statistics.Entry]
True if the entry is uint-valued.
is_int [Z3.Arithmetic]
Indicates whether the term is of integer sort.
is_int2bv [Z3.BitVector]
Indicates whether the term is a coercion from bit-vector to integer This function is not supported by the decision procedures.
is_int2real [Z3.Arithmetic]
Indicates whether the term is a coercion of integer to real (unary)
is_int_numeral [Z3.Arithmetic]
Indicates whether the term is an integer numeral.
is_int_symbol [Z3.Symbol]
Indicates whether the symbol is of Int kind
is_intersect [Z3.Set]
Indicates whether the term is set intersection
is_is_empty [Z3.Relation]
Indicates whether the term is a test for the emptiness of a relation
is_is_infinite [Z3.FloatingPoint]
Indicates whether an expression is a floating-point is_infinite expression
is_is_nan [Z3.FloatingPoint]
Indicates whether an expression is a floating-point is_nan expression
is_is_negative [Z3.FloatingPoint]
Indicates whether an expression is a floating-point is_negative expression
is_is_normal [Z3.FloatingPoint]
Indicates whether an expression is a floating-point is_normal expression
is_is_positive [Z3.FloatingPoint]
Indicates whether an expression is a floating-point is_positive expression
is_is_subnormal [Z3.FloatingPoint]
Indicates whether an expression is a floating-point is_subnormal expression
is_is_zero [Z3.FloatingPoint]
Indicates whether an expression is a floating-point is_zero expression
is_ite [Z3.Boolean]
Indicates whether the term is a ternary if-then-else term
is_join [Z3.Relation]
Indicates whether the term is a relational join
is_le [Z3.Arithmetic]
Indicates whether the term is a less-than-or-equal
is_lemma [Z3.Proof]
Indicates whether the term is a proof by lemma
is_leq [Z3.FloatingPoint]
Indicates whether an expression is a floating-point leq expression
is_lt [Z3.FloatingPoint]
Indicates whether an expression is a floating-point lt expression
is_lt [Z3.Arithmetic]
Indicates whether the term is a less-than
is_lt [Z3.FiniteDomain]
Indicates whether the term is a less than predicate over a finite domain.
is_max [Z3.FloatingPoint]
Indicates whether an expression is a floating-point max expression
is_min [Z3.FloatingPoint]
Indicates whether an expression is a floating-point min expression
is_modulus [Z3.Arithmetic]
Indicates whether the term is modulus (binary)
is_modus_ponens [Z3.Proof]
Indicates whether the term is proof via modus ponens
is_modus_ponens_oeq [Z3.Proof]
Indicates whether the term is a proof by modus ponens for equi-satisfiability.
is_monotonicity [Z3.Proof]
Indicates whether the term is a monotonicity proof object.
is_mul [Z3.FloatingPoint]
Indicates whether an expression is a floating-point mul expression
is_mul [Z3.Arithmetic]
Indicates whether the term is multiplication (binary)
is_neg [Z3.FloatingPoint]
Indicates whether an expression is a floating-point neg expression
is_negation_filter [Z3.Relation]
Indicates whether the term is an intersection of a relation with the negation of another.
is_nnf_neg [Z3.Proof]
Indicates whether the term is a proof for a negative NNF step
is_nnf_pos [Z3.Proof]
Indicates whether the term is a proof for a positive NNF step
is_nnf_star [Z3.Proof]
Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
is_not [Z3.Boolean]
Indicates whether the term is a negation
is_numeral [Z3.Expr]
Indicates whether the term is a numeral
is_oeq [Z3.Proof]
Indicates whether the term is a binary equivalence modulo namings.
is_or [Z3.Boolean]
Indicates whether the term is an n-ary disjunction
is_or_elimination [Z3.Proof]
Indicates whether the term is a proof by eliminiation of not-or
is_overapproximation [Z3.Goal]
Indicates whether the goal is an over-approximation.
is_precise [Z3.Goal]
Indicates whether the goal is precise.
is_project [Z3.Relation]
Indicates whether the term is a projection of columns (provided as numbers in the parameters).
is_pull_quant [Z3.Proof]
Indicates whether the term is a proof for pulling quantifiers out.
is_pull_quant_star [Z3.Proof]
Indicates whether the term is a proof for pulling quantifiers out.
is_push_quant [Z3.Proof]
Indicates whether the term is a proof for pushing quantifiers in.
is_quant_inst [Z3.Proof]
Indicates whether the term is a proof for quantifier instantiation
is_quant_intro [Z3.Proof]
Indicates whether the term is a quant-intro proof
is_quantifier [Z3.AST]
Indicates whether the AST is a Quantifier
is_rat_numeral [Z3.Arithmetic]
Indicates whether the term is a real numeral.
is_real [Z3.Arithmetic]
Indicates whether the term is of sort real.
is_real2int [Z3.Arithmetic]
Indicates whether the term is a coercion of real to integer (unary)
is_real_is_int [Z3.Arithmetic]
Indicates whether the term is a check that tests whether a real is integral (unary)
is_reflexivity [Z3.Proof]
Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
is_relation [Z3.Relation]
Indicates whether the term is of a relation sort.
is_rem [Z3.FloatingPoint]
Indicates whether an expression is a floating-point rem expression
is_remainder [Z3.Arithmetic]
Indicates whether the term is remainder (binary)
is_rename [Z3.Relation]
Indicates whether the term is the renaming of a column in a relation
is_rewrite [Z3.Proof]
Indicates whether the term is a proof by rewriting
is_rewrite_star [Z3.Proof]
Indicates whether the term is a proof by rewriting
is_round_to_integral [Z3.FloatingPoint]
Indicates whether an expression is a floating-point round_to_integral expression
is_select [Z3.Relation]
Indicates whether the term is a relational select
is_select [Z3.Z3Array]
Indicates whether the term is an array select.
is_skolemize [Z3.Proof]
Indicates whether the term is a proof for a Skolemization step
is_sort [Z3.AST]
Indicates whether the AST is a Sort
is_sqrt [Z3.FloatingPoint]
Indicates whether an expression is a floating-point sqrt expression
is_store [Z3.Relation]
Indicates whether the term is an relation store
is_store [Z3.Z3Array]
Indicates whether the term is an array store.
is_string_symbol [Z3.Symbol]
Indicates whether the symbol is of string kind.
is_sub [Z3.FloatingPoint]
Indicates whether an expression is a floating-point sub expression
is_sub [Z3.Arithmetic]
Indicates whether the term is subtraction (binary)
is_subset [Z3.Set]
Indicates whether the term is set subset
is_symmetry [Z3.Proof]
Indicates whether the term is proof by symmetricity of a relation
is_theory_lemma [Z3.Proof]
Indicates whether the term is a proof for theory lemma
is_to_fp [Z3.FloatingPoint]
Indicates whether an expression is a floating-point to_fp expression
is_to_fp_unsigned [Z3.FloatingPoint]
Indicates whether an expression is a floating-point to_fp_unsigned expression
is_to_ieee_bv [Z3.FloatingPoint]
Indicates whether an expression is a floating-point to_ieee_bv expression
is_to_real [Z3.FloatingPoint]
Indicates whether an expression is a floating-point to_real expression
is_to_sbv [Z3.FloatingPoint]
Indicates whether an expression is a floating-point to_sbv expression
is_to_ubv [Z3.FloatingPoint]
Indicates whether an expression is a floating-point to_ubv expression
is_transitivity [Z3.Proof]
Indicates whether the term is a proof by transitivity of a relation
is_true [Z3.Proof]
Indicates whether the term is a Proof for the expression 'true'.
is_true [Z3.Boolean]
Indicates whether the term is the constant true.
is_uminus [Z3.Arithmetic]
Indicates whether the term is a unary minus
is_underapproximation [Z3.Goal]
Indicates whether the goal is an under-approximation.
is_union [Z3.Relation]
Indicates whether the term is the union or convex hull of two relations.
is_union [Z3.Set]
Indicates whether the term is set union
is_unit_resolution [Z3.Proof]
Indicates whether the term is a proof by unit resolution
is_universal [Z3.Quantifier]
Indicates whether the quantifier is universal.
is_var [Z3.AST]
Indicates whether the AST is a bound variable
is_well_sorted [Z3.Expr]
Indicates whether the term is well-sorted.
is_widen [Z3.Relation]
Indicates whether the term is the widening of two relations The function takes two arguments.
is_xor [Z3.Boolean]
Indicates whether the term is an exclusive or

K
kind [Z3.Symbol]
The kind of the symbol (int or string)

L
lbool_of_int [Z3enums]
le [Z3.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
lt [Z3.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

M
major [Z3.Version]
The major version.
maximize [Z3.Optimize]
Add maximization objective.
minimize [Z3.Optimize]
Add minimization objective.
minor [Z3.Version]
The minor version.
mk_abs [Z3.FloatingPoint]
Floating-point absolute value
mk_add [Z3.FloatingPoint]
Floating-point addition
mk_add [Z3.BitVector]
Two's complement addition.
mk_add [Z3.Arithmetic]
Create an expression representing t[0] + t[1] + ....
mk_add_no_overflow [Z3.BitVector]
Create a predicate that checks that the bit-wise addition does not overflow.
mk_add_no_underflow [Z3.BitVector]
Create a predicate that checks that the bit-wise addition does not underflow.
mk_and [Z3.BitVector]
Bitwise conjunction.
mk_and [Z3.Boolean]
Create an expression representing the AND of args
mk_app [Z3.Expr]
Create a new function application.
mk_ashr [Z3.BitVector]
Arithmetic shift right
mk_ast_map [Z3.AST.ASTMap]
Create an empty mapping from AST to AST
mk_ast_vector [Z3.AST.ASTVector]
Create an empty AST vector
mk_bound [Z3.Quantifier]
Creates a new bound variable.
mk_bv2int [Z3.BitVector]
Create an integer from the bit-vector argument
mk_complement [Z3.Set]
Take the complement of a set.
mk_concat [Z3.BitVector]
Bit-vector concatenation.
mk_const [Z3.FloatingPoint]
Creates a floating-point constant.
mk_const [Z3.BitVector]
Creates a bit-vector constant.
mk_const [Z3.Arithmetic.Real]
Creates a real constant.
mk_const [Z3.Arithmetic.Integer]
Creates an integer constant.
mk_const [Z3.Z3Array]
Create an array constant.
mk_const [Z3.Boolean]
Create a Boolean constant.
mk_const [Z3.Expr]
Creates a new constant.
mk_const_array [Z3.Z3Array]
Create a constant array.
mk_const_decl [Z3.FuncDecl]
Creates a new constant function declaration.
mk_const_decl_s [Z3.FuncDecl]
Creates a new constant function declaration.
mk_const_f [Z3.Expr]
Creates a constant from the func_decl.
mk_const_s [Z3.FloatingPoint]
Creates a floating-point constant.
mk_const_s [Z3.BitVector]
Creates a bit-vector constant.
mk_const_s [Z3.Arithmetic.Real]
Creates a real constant.
mk_const_s [Z3.Arithmetic.Integer]
Creates an integer constant.
mk_const_s [Z3.Z3Array]
Create an array constant.
mk_const_s [Z3.Boolean]
Create a Boolean constant.
mk_const_s [Z3.Expr]
Creates a new constant.
mk_constructor [Z3.Datatype]
Create a datatype constructor.
mk_constructor_s [Z3.Datatype]
Create a datatype constructor.
mk_context [Z3]
Create a context object The following parameters can be set:
mk_del [Z3.Set]
Remove an element from a set.
mk_difference [Z3.Set]
Take the difference between two sets.
mk_distinct [Z3.Boolean]
Creates a distinct term.
mk_div [Z3.FloatingPoint]
Floating-point division
mk_div [Z3.Arithmetic]
Create an expression representing t1 / t2.
mk_empty [Z3.Set]
Create an empty set.
mk_eq [Z3.FloatingPoint]
Floating-point equality.
mk_eq [Z3.Boolean]
Creates the equality between two expr's.
mk_exists [Z3.Quantifier]
Create an existential Quantifier.
mk_exists_const [Z3.Quantifier]
Create an existential Quantifier.
mk_ext_rotate_left [Z3.BitVector]
Rotate Left.
mk_ext_rotate_right [Z3.BitVector]
Rotate Right.
mk_extract [Z3.BitVector]
Bit-vector extraction.
mk_false [Z3.Boolean]
The false Term.
mk_fixedpoint [Z3.Fixedpoint]
Create a Fixedpoint context.
mk_fma [Z3.FloatingPoint]
Floating-point fused multiply-add.
mk_forall [Z3.Quantifier]
Create a universal Quantifier.
mk_forall_const [Z3.Quantifier]
Create a universal Quantifier.
mk_fp [Z3.FloatingPoint]
Create an expression of FloatingPoint sort from three bit-vector expressions.
mk_fresh_const [Z3.Expr]
Creates a fresh constant with a name prefixed with a string.
mk_fresh_const_decl [Z3.FuncDecl]
Creates a fresh constant function declaration with a name prefixed with a prefix string.
mk_fresh_func_decl [Z3.FuncDecl]
mk_full [Z3.Set]
Create the full set.
mk_func_decl [Z3.FuncDecl]
Creates a new function declaration.
mk_func_decl_s [Z3.FuncDecl]
Creates a new function declaration.
mk_ge [Z3.Arithmetic]
Create an expression representing t1 >= t2
mk_geq [Z3.FloatingPoint]
Floating-point greater than or equal.
mk_goal [Z3.Goal]
Creates a new Goal.
mk_gt [Z3.FloatingPoint]
Floating-point greater than.
mk_gt [Z3.Arithmetic]
Create an expression representing t1 > t2
mk_iff [Z3.Boolean]
Create an expression representing t1 iff t2.
mk_implies [Z3.Boolean]
Create an expression representing t1 -> t2.
mk_inf [Z3.FloatingPoint]
Create a floating-point infinity of a given FloatingPoint sort.
mk_int [Z3.Symbol]
Creates a new symbol using an integer.
mk_int2bv [Z3.Arithmetic.Integer]
Create an n-bit bit-vector from an integer argument.
mk_int2real [Z3.Arithmetic.Integer]
Coerce an integer to a real.
mk_interpolant [Z3.Interpolation]
Create an AST node marking a formula position for interpolation.
mk_interpolation_context [Z3.Interpolation]
The interpolation context is suitable for generation of interpolants.
mk_intersection [Z3.Set]
Take the intersection of a list of sets.
mk_ints [Z3.Symbol]
Create a list of symbols.
mk_is_infinite [Z3.FloatingPoint]
Predicate indicating whether t is a floating-point number representing +oo or -oo.
mk_is_integer [Z3.Arithmetic.Real]
Creates an expression that checks whether a real number is an integer.
mk_is_nan [Z3.FloatingPoint]
Predicate indicating whether t is a NaN.
mk_is_negative [Z3.FloatingPoint]
Predicate indicating whether t is a negative floating-point number.
mk_is_normal [Z3.FloatingPoint]
Predicate indicating whether t is a normal floating-point number.
mk_is_positive [Z3.FloatingPoint]
Predicate indicating whether t is a positive floating-point number.
mk_is_subnormal [Z3.FloatingPoint]
Predicate indicating whether t is a subnormal floating-point number.
mk_is_zero [Z3.FloatingPoint]
Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
mk_ite [Z3.Boolean]
Create an expression representing an if-then-else: ite(t1, t2, t3).
mk_le [Z3.Arithmetic]
Create an expression representing t1 <= t2
mk_leq [Z3.FloatingPoint]
Floating-point less than or equal.
mk_list_s [Z3.Z3List]
Create a new list sort.
mk_lshr [Z3.BitVector]
Logical shift right
mk_lt [Z3.FloatingPoint]
Floating-point less than.
mk_lt [Z3.Arithmetic]
Create an expression representing t1 < t2
mk_map [Z3.Z3Array]
Maps f on the argument arrays.
mk_max [Z3.FloatingPoint]
Maximum of floating-point numbers.
mk_membership [Z3.Set]
Check for set membership.
mk_min [Z3.FloatingPoint]
Minimum of floating-point numbers.
mk_mod [Z3.Arithmetic.Integer]
Create an expression representing t1 mod t2.
mk_mul [Z3.FloatingPoint]
Floating-point multiplication
mk_mul [Z3.BitVector]
Two's complement multiplication.
mk_mul [Z3.Arithmetic]
Create an expression representing t[0] * t[1] * ....
mk_mul_no_overflow [Z3.BitVector]
Create a predicate that checks that the bit-wise multiplication does not overflow.
mk_mul_no_underflow [Z3.BitVector]
Create a predicate that checks that the bit-wise multiplication does not underflow.
mk_nan [Z3.FloatingPoint]
Create a floating-point NaN of a given FloatingPoint sort.
mk_nand [Z3.BitVector]
Bitwise NAND.
mk_neg [Z3.FloatingPoint]
Floating-point negation
mk_neg [Z3.BitVector]
Standard two's complement unary minus.
mk_neg_no_overflow [Z3.BitVector]
Create a predicate that checks that the bit-wise negation does not overflow.
mk_nor [Z3.BitVector]
Bitwise NOR.
mk_not [Z3.BitVector]
Bitwise negation.
mk_not [Z3.Boolean]
Mk an expression representing not(a).
mk_numeral [Z3.BitVector]
Create a bit-vector numeral.
mk_numeral_f [Z3.FloatingPoint]
Create a numeral of FloatingPoint sort from a float.
mk_numeral_i [Z3.FloatingPoint]
Create a numeral of FloatingPoint sort from a signed integer.
mk_numeral_i [Z3.Arithmetic.Real]
Create a real numeral.
mk_numeral_i [Z3.Arithmetic.Integer]
Create an integer numeral.
mk_numeral_i_u [Z3.FloatingPoint]
Create a numeral of FloatingPoint sort from a sign bit and two integers.
mk_numeral_int [Z3.Expr]
Create a numeral of a given sort.
mk_numeral_nd [Z3.Arithmetic.Real]
Create a real numeral from a fraction.
mk_numeral_s [Z3.FloatingPoint]
Create a numeral of FloatingPoint sort from a string
mk_numeral_s [Z3.Arithmetic.Real]
Create a real numeral.
mk_numeral_s [Z3.Arithmetic.Integer]
Create an integer numeral.
mk_numeral_string [Z3.Expr]
Create a numeral of a given sort.
mk_opt [Z3.Optimize]
Create a Optimize context.
mk_or [Z3.BitVector]
Bitwise disjunction.
mk_or [Z3.Boolean]
Create an expression representing the OR of args
mk_params [Z3.Params]
Creates a new parameter set
mk_pattern [Z3.Quantifier]
Create a quantifier pattern.
mk_power [Z3.Arithmetic]
Create an expression representing t1 ^ t2.
mk_probe [Z3.Probe]
Creates a new Probe.
mk_quantifier [Z3.Quantifier]
Create a Quantifier.
mk_real2int [Z3.Arithmetic.Real]
Coerce a real to an integer.
mk_redand [Z3.BitVector]
Take conjunction of bits in a vector,vector of length 1.
mk_redor [Z3.BitVector]
Take disjunction of bits in a vector,vector of length 1.
mk_rem [Z3.FloatingPoint]
Floating-point remainder
mk_rem [Z3.Arithmetic.Integer]
Create an expression representing t1 rem t2.
mk_repeat [Z3.BitVector]
Bit-vector repetition.
mk_rna [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
mk_rne [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
mk_rotate_left [Z3.BitVector]
Rotate Left.
mk_rotate_right [Z3.BitVector]
Rotate Right.
mk_round_nearest_ties_to_away [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
mk_round_nearest_ties_to_even [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
mk_round_to_integral [Z3.FloatingPoint]
Floating-point roundToIntegral.
mk_round_toward_negative [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
mk_round_toward_positive [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
mk_round_toward_zero [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
mk_rtn [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
mk_rtp [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
mk_rtz [Z3.FloatingPoint.RoundingMode]
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
mk_sdiv [Z3.BitVector]
Signed division.
mk_sdiv_no_overflow [Z3.BitVector]
Create a predicate that checks that the bit-wise signed division does not overflow.
mk_select [Z3.Z3Array]
Array read.
mk_set_add [Z3.Set]
Add an element to the set.
mk_sge [Z3.BitVector]
Two's complement signed greater than or equal to.
mk_sgt [Z3.BitVector]
Two's complement signed greater-than.
mk_shl [Z3.BitVector]
Shift left.
mk_sign_ext [Z3.BitVector]
Bit-vector sign extension.
mk_simple_solver [Z3.Solver]
Creates a new (incremental) solver.
mk_sle [Z3.BitVector]
Two's complement signed less-than or equal to.
mk_slt [Z3.BitVector]
Two's complement signed less-than
mk_smod [Z3.BitVector]
Two's complement signed remainder (sign follows divisor).
mk_solver [Z3.Solver]
Creates a new (incremental) solver.
mk_solver_s [Z3.Solver]
Creates a new (incremental) solver.
mk_solver_t [Z3.Solver]
Creates a solver that is implemented using the given tactic.
mk_sort [Z3.FloatingPoint.RoundingMode]
Create the RoundingMode sort.
mk_sort [Z3.FloatingPoint]
Create a FloatingPoint sort.
mk_sort [Z3.BitVector]
Create a new bit-vector sort.
mk_sort [Z3.Arithmetic.Real]
Create a real sort.
mk_sort [Z3.Arithmetic.Integer]
Create a new integer sort.
mk_sort [Z3.Tuple]
Create a new tuple sort.
mk_sort [Z3.Z3List]
Create a new list sort.
mk_sort [Z3.Enumeration]
Create a new enumeration sort.
mk_sort [Z3.Datatype]
Create a new datatype sort.
mk_sort [Z3.FiniteDomain]
Create a new finite domain sort.
mk_sort [Z3.Set]
Create a set type.
mk_sort [Z3.Z3Array]
Create a new array sort.
mk_sort [Z3.Boolean]
Create a Boolean sort
mk_sort_128 [Z3.FloatingPoint]
Create the quadruple-precision (128-bit) FloatingPoint sort.
mk_sort_16 [Z3.FloatingPoint]
Create the half-precision (16-bit) FloatingPoint sort.
mk_sort_32 [Z3.FloatingPoint]
Create the single-precision (32-bit) FloatingPoint sort.
mk_sort_64 [Z3.FloatingPoint]
Create the double-precision (64-bit) FloatingPoint sort.
mk_sort_double [Z3.FloatingPoint]
Create the double-precision (64-bit) FloatingPoint sort.
mk_sort_half [Z3.FloatingPoint]
Create the half-precision (16-bit) FloatingPoint sort.
mk_sort_quadruple [Z3.FloatingPoint]
Create the quadruple-precision (128-bit) FloatingPoint sort.
mk_sort_s [Z3.Enumeration]
Create a new enumeration sort.
mk_sort_s [Z3.Datatype]
Create a new datatype sort.
mk_sort_s [Z3.FiniteDomain]
Create a new finite domain sort.
mk_sort_single [Z3.FloatingPoint]
Create the single-precision (32-bit) FloatingPoint sort.
mk_sorts [Z3.Datatype]
Create mutually recursive datatypes.
mk_sorts_s [Z3.Datatype]
Create mutually recursive data-types.
mk_sqrt [Z3.FloatingPoint]
Floating-point square root
mk_srem [Z3.BitVector]
Signed remainder.
mk_store [Z3.Z3Array]
Array update.
mk_string [Z3.Symbol]
Creates a new symbol using a string.
mk_strings [Z3.Symbol]
Create a list of symbols.
mk_sub [Z3.FloatingPoint]
Floating-point subtraction
mk_sub [Z3.BitVector]
Two's complement subtraction.
mk_sub [Z3.Arithmetic]
Create an expression representing t[0] - t[1] - ....
mk_sub_no_overflow [Z3.BitVector]
Create a predicate that checks that the bit-wise subtraction does not overflow.
mk_sub_no_underflow [Z3.BitVector]
Create a predicate that checks that the bit-wise subtraction does not underflow.
mk_subset [Z3.Set]
Check for subsetness of sets.
mk_tactic [Z3.Tactic]
Creates a new Tactic.
mk_term_array [Z3.Z3Array]
Access the array default value.
mk_to_fp_bv [Z3.FloatingPoint]
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
mk_to_fp_float [Z3.FloatingPoint]
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
mk_to_fp_int_real [Z3.FloatingPoint]
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
mk_to_fp_real [Z3.FloatingPoint]
Conversion of a term of real sort into a term of FloatingPoint sort.
mk_to_fp_signed [Z3.FloatingPoint]
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
mk_to_fp_unsigned [Z3.FloatingPoint]
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
mk_to_ieee_bv [Z3.FloatingPoint]
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
mk_to_real [Z3.FloatingPoint]
Conversion of a floating-point term into a real-numbered term.
mk_to_sbv [Z3.FloatingPoint]
Conversion of a floating-point term into a signed bit-vector.
mk_to_ubv [Z3.FloatingPoint]
C1onversion of a floating-point term into an unsigned bit-vector.
mk_true [Z3.Boolean]
The true Term.
mk_udiv [Z3.BitVector]
Unsigned division.
mk_uge [Z3.BitVector]
Unsigned greater than or equal to.
mk_ugt [Z3.BitVector]
Unsigned greater-than.
mk_ule [Z3.BitVector]
Unsigned less-than or equal to.
mk_ult [Z3.BitVector]
Unsigned less-than
mk_unary_minus [Z3.Arithmetic]
Create an expression representing -t.
mk_uninterpreted [Z3.Sort]
Create a new uninterpreted sort.
mk_uninterpreted_s [Z3.Sort]
Create a new uninterpreted sort.
mk_union [Z3.Set]
Take the union of a list of sets.
mk_urem [Z3.BitVector]
Unsigned remainder.
mk_val [Z3.Boolean]
Creates a Boolean value.
mk_xnor [Z3.BitVector]
Bitwise XNOR.
mk_xor [Z3.BitVector]
Bitwise XOR.
mk_xor [Z3.Boolean]
Create an expression representing t1 xor t2.
mk_zero [Z3.FloatingPoint]
Create a floating-point zero of a given FloatingPoint sort.
mk_zero_ext [Z3.BitVector]
Bit-vector zero extension.

N
nil [Z3.Z3List]
The empty list.
not_ [Z3.Probe]
Create a probe that evaluates to "true" when another probe does not evaluate to "true".
numeral_to_string [Z3.FloatingPoint]
Returns a string representation of a numeral.
numeral_to_string [Z3.BitVector]
Returns a string representation of a numeral.
numeral_to_string [Z3.Arithmetic.Real.AlgebraicNumber]
Returns a string representation of a numeral.
numeral_to_string [Z3.Arithmetic.Real]
Returns a string representation of a numeral.
numeral_to_string [Z3.Arithmetic.Integer]
Returns a string representation of a numeral.

O
open_ [Z3.Log]
Open an interaction log file.
or_ [Z3.Probe]
Create a probe that evaluates to "true" when either of two probes evaluates to "true".
or_else [Z3.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.

P
par_and_then [Z3.Tactic]
Create a tactic that applies a tactic to a given goal and then another tactic to every subgoal produced by the first one.
par_or [Z3.Tactic]
Create a tactic that applies the given tactics in parallel.
param_kind_of_int [Z3enums]
parameter_kind_of_int [Z3enums]
parse_file [Z3.Fixedpoint]
Parse an SMT-LIB2 file with fixedpoint rules.
parse_smtlib2_file [Z3.SMT]
Parse the given file using the SMT-LIB2 parser.
parse_smtlib2_string [Z3.SMT]
Parse the given string using the SMT-LIB2 parser.
parse_smtlib_file [Z3.SMT]
Parse the given file using the SMT-LIB parser.
parse_smtlib_string [Z3.SMT]
Parse the given string using the SMT-LIB parser.
parse_string [Z3.Fixedpoint]
Parse an SMT-LIB2 string with fixedpoint rules.
pattern_of_ast [Z3.Quantifier.Pattern]
pop [Z3.Optimize]
Backtrack one backtracking point.
pop [Z3.Fixedpoint]
Backtrack one backtracking point.
pop [Z3.Solver]
Backtracks a number of backtracking points.
push [Z3.Optimize]
Creates a backtracking point.
push [Z3.Fixedpoint]
Creates a backtracking point.
push [Z3.Solver]
Creates a backtracking point.
push [Z3.AST.ASTVector]
Add an ast to the back of the vector.

Q
quantifier_of_expr [Z3.Quantifier]
query [Z3.Fixedpoint]
Query the fixedpoint solver.
query_r [Z3.Fixedpoint]
Query the fixedpoint solver.

R
read_interpolation_problem [Z3.Interpolation]
Read an interpolation problem from file.
register_relation [Z3.Fixedpoint]
Register predicate as recursive relation.
repeat [Z3.Tactic]
Create a tactic that keeps applying one tactic until the goal is not modified anymore or the maximum number of iterations is reached.
reset [Z3.Solver]
Resets the Solver.
reset [Z3.Goal]
Erases all formulas from the given goal.
reset [Z3.AST.ASTMap]
Removes all keys from the map.
resize [Z3.AST.ASTVector]
Resize the vector to a new size.
revision [Z3.Version]
The revision.

S
set [Z3.AST.ASTVector]
Sets the i-th object in the vector.
set_global_param [Z3]
Set a global (or module) parameter, which is shared by all Z3 contexts.
set_parameters [Z3.Optimize]
Sets the optimize solver parameters.
set_parameters [Z3.Fixedpoint]
Sets the fixedpoint solver parameters.
set_parameters [Z3.Solver]
Sets the solver parameters.
set_predicate_representation [Z3.Fixedpoint]
Instrument the Datalog engine on which table representation to use for recursive predicate.
set_print_mode [Z3.Params]
Selects the format used for pretty-printing expressions.
simplify [Z3.Goal]
Simplifies the goal.
simplify [Z3.Expr]
Returns a simplified version of the expression.
skip [Z3.Tactic]
Create a tactic that just returns the given goal.
sort_kind_of_int [Z3enums]
sort_universe [Z3.Model]
The finite set of distinct values that represent the interpretation of a sort.
string_of_status [Z3.Solver]
substitute [Z3.Expr]
Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.
substitute_one [Z3.Expr]
Substitute every occurrence of from in the expression with to.
substitute_vars [Z3.Expr]
Substitute the free variables in the expression with the expressions in the expr array
symbol_kind_of_int [Z3enums]

T
to_decimal_string [Z3.Arithmetic.Real.AlgebraicNumber]
Returns a string representation in decimal notation.
to_decimal_string [Z3.Arithmetic.Real]
Returns a string representation in decimal notation.
to_expr_list [Z3.AST.ASTVector]
Translates the ASTVector into an (Expr.expr list)
to_list [Z3.AST.ASTVector]
Translates the ASTVector into an (Ast.ast list)
to_lower [Z3.Arithmetic.Real.AlgebraicNumber]
Return a lower bound for the given real algebraic number.
to_sexpr [Z3.AST]
A string representation of the AST in s-expression notation.
to_string [Z3.Optimize]
Retrieve SMT-LIB string representation of optimize object.
to_string [Z3.Fixedpoint]
Retrieve internal string representation of fixedpoint object.
to_string [Z3.Solver]
A string representation of the solver.
to_string [Z3.Statistics.Entry]
The string representation of the entry (key and value)
to_string [Z3.Statistics]
A string representation of the statistical data.
to_string [Z3.Tactic.ApplyResult]
A string representation of the ApplyResult.
to_string [Z3.Model.FuncInterp.FuncEntry]
A string representation of the function entry.
to_string [Z3.Model.FuncInterp]
A string representation of the function interpretation.
to_string [Z3.Model]
Conversion of models to strings.
to_string [Z3.Goal]
A string representation of the Goal.
to_string [Z3.Quantifier.Pattern]
A string representation of the pattern.
to_string [Z3.Quantifier]
A string representation of the quantifier.
to_string [Z3.Expr]
Returns a string representation of the expression.
to_string [Z3.Params.ParamDescrs]
Retrieves a string representation of the ParamDescrs.
to_string [Z3.Params]
A string representation of the parameter set.
to_string [Z3.FuncDecl]
A string representations of the function declaration.
to_string [Z3.Sort]
A string representation of the sort.
to_string [Z3.AST.ASTMap]
Retrieves a string representation of the map.
to_string [Z3.AST.ASTVector]
Retrieves a string representation of the vector.
to_string [Z3.AST]
A string representation of the AST.
to_string [Z3.Symbol]
A string representation of the symbol.
to_string [Z3.Version]
A string representation of the version information.
to_string_q [Z3.Fixedpoint]
Convert benchmark given as set of axioms, rules and queries to a string.
to_string_value [Z3.Statistics.Entry]
The string representation of the the entry's value.
to_upper [Z3.Arithmetic.Real.AlgebraicNumber]
Return a upper bound for a given real algebraic number.
toggle_warning_messages [Z3]
Enable/disable printing of warning messages to the console.
translate [Z3.Goal]
Translates (copies) the Goal to another context..
translate [Z3.Expr]
Translates (copies) the term to another context.
translate [Z3.AST.ASTVector]
Translates all ASTs in the vector to another context.
translate [Z3.AST]
Translates (copies) the AST to another context.
try_for [Z3.Tactic]
Create a tactic that applies one tactic to a goal for some time (in milliseconds).

U
unwrap_ast [Z3.AST]
Unwraps an AST.
update [Z3.Expr]
Update the arguments of the expression using an array of expressions.
update_param_value [Z3.Params]
Update a mutable configuration parameter.
update_rule [Z3.Fixedpoint]
Update named rule into in the fixedpoint solver.
using_params [Z3.Tactic]
Create a tactic that applies a tactic using the given set of parameters.

V
validate [Z3.Params.ParamDescrs]
Validate a set of parameters.

W
when_ [Z3.Tactic]
Create a tactic that applies one tactic to a given goal if the probe evaluates to true.
with_ [Z3.Tactic]
Create a tactic that applies a tactic using the given set of parameters.
wrap_ast [Z3.AST]
Wraps an AST.
write_interpolation_problem [Z3.Interpolation]
Write an interpolation problem to file suitable for reading with Z3_read_interpolation_problem.