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.
|