A | |
| add [Z3.RCF] |
Addition
|
| 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_rec_def [Z3.FuncDecl] |
Registers a recursive function definition
|
| add_rule [Z3.Fixedpoint] |
Add rule into the fixedpoint solver.
|
| add_simplifier [Z3.Solver] |
Create a solver with simplifying pre-processing *
|
| add_soft [Z3.Optimize] |
Assert 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.Simplifier] |
Create a simplifier that applies one simplifier to a Goal and
then another one to every subgoal produced by the first one.
|
| 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_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] |
Check consistency and produce optimal values.
|
| check [Z3.Solver] |
Checks whether the assertions in the solver are consistent or not.
|
| close [Z3.Log] |
Closes the interaction log.
|
| coefficients [Z3.RCF] |
Extract the coefficients from an algebraic number.
|
| compare [Z3.Expr] |
Object Comparison.
|
| compare [Z3.AST] |
Object Comparison.
|
| 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.
|
D | |
| decl_kind_of_int [Z3enums] | |
| del [Z3.RCF] |
Delete a RCF numeral created using the RCF API.
|
| del_list [Z3.RCF] |
Delete RCF numerals created using the RCF API.
|
| del_root [Z3.RCF] | |
| del_roots [Z3.RCF] | |
| disable_trace [Z3] |
Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode.
|
| div [Z3.RCF] |
Division
|
E | |
| enable_trace [Z3] |
Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode.
|
| eq [Z3.RCF] |
equality
|
| 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] | |
| extension_index [Z3.RCF] |
Return the index of a field extension.
|
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 trivially satisfiable (i.e., empty)
or trivially unsatisfiable (i.e., contains `false').
|
| find [Z3.AST.ASTMap] |
Finds the value associated with the key.
|
| from_file [Z3.Optimize] |
Parse an SMT-LIB2 file with assertions, soft constraints and optimization
objectives.
|
| from_string [Z3.Optimize] |
Parse an SMT-LIB2 string with assertions, soft constraints and optimization
objectives.
|
| full_version [Z3.Version] |
A full version string.
|
G | |
| ge [Z3.RCF] |
greater-than or equal
|
| 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.Optimize] |
Return the set of asserted formulas on the optimization context.
|
| 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_coefficient [Z3.RCF] |
Extract a coefficient from an algebraic number.
|
| 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_estimated_alloc_size [Z3.Statistics] |
The estimated allocated memory in bytes.
|
| 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.Simplifier] |
A string containing a description of parameters accepted by the simplifier.
|
| 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-Bruijn index of a bound variable.
|
| get_int [Z3.Statistics.Entry] |
The int-value of the entry.
|
| get_int [Z3.FuncDecl.Parameter] |
The int value of the parameter.
|
| get_int [Z3.Symbol] |
The int value of the symbol.
|
| 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_simplifiers [Z3.Simplifier] |
The number of supported simplifiers.
|
| 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_bv [Z3.FloatingPoint] |
Return the exponent of a floating-point numeral as a bit-vector expression.
|
| 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_sign_bv [Z3.FloatingPoint] |
Return the sign of a floating-point numeral as a bit-vector expression.
|
| get_numeral_significand_bv [Z3.FloatingPoint] |
Return the significand value of a floating-point numeral as a bit-vector expression.
|
| 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_numerator_denominator [Z3.RCF] |
Extract the "numerator" and "denominator" of the given RCF numeral.
|
| get_objectives [Z3.Optimize] |
Return objectives on the optimization context.
|
| 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.Simplifier] |
Retrieves parameter descriptions for Simplifiers.
|
| 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_simplifier_description [Z3.Simplifier] |
Returns a string containing a description of the simplifier with the given name.
|
| get_simplifier_names [Z3.Simplifier] |
The names of all supported simplifiers.
|
| 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_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.Seq] |
retrieve string from string Expr.expr
|
| 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.RCF] |
greater-than
|
| 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 | |
| infinitesimal_name [Z3.RCF] |
Return the name of an infinitesimal.
|
| insert [Z3.AST.ASTMap] |
Stores or replaces a new key/value pair in the map.
|
| int_of_ast_kind [Z3enums] | |
| int_of_ast_print_mode [Z3enums] | |
| int_of_decl_kind [Z3enums] | |
| int_of_error_code [Z3enums] | |
| int_of_goal_prec [Z3enums] | |
| int_of_lbool [Z3enums] | |
| int_of_param_kind [Z3enums] | |
| int_of_parameter_kind [Z3enums] | |
| int_of_sort_kind [Z3enums] | |
| int_of_symbol_kind [Z3enums] | |
| interrupt [Z3.Solver] |
Solver local interrupt.
|
| interrupt [Z3.Tactic] |
Interrupt the execution of a Z3 procedure.
|
| interrupt [Z3] |
Interrupt the execution of a Z3 procedure.
|
| inv [Z3.RCF] |
Multiplicative Inverse
|
| 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 [Z3.RCF] |
Return \c true if \c a represents an algebraic number.
|
| 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_char_sort [Z3.Seq] |
test if sort is a char sort
|
| is_clone [Z3.Relation] |
Indicates whether the term is a relational clone (copy)
|
| 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 geq expression
|
| 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 hypothesis 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_infinitesimal [Z3.RCF] |
Return \c true if \c a represents an infinitesimal.
|
| 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_not [Z3.Boolean] |
Indicates whether the term is a negation
|
| is_numeral [Z3.Expr] |
Indicates whether the term is a numeral
|
| is_numeral_inf [Z3.FloatingPoint] |
Indicates whether a floating-point numeral is +oo or -oo.
|
| is_numeral_nan [Z3.FloatingPoint] |
Indicates whether a floating-point numeral is a NaN.
|
| is_numeral_negative [Z3.FloatingPoint] |
Indicates whether a floating-point numeral is negative.
|
| is_numeral_normal [Z3.FloatingPoint] |
Indicates whether a floating-point numeral is normal.
|
| is_numeral_positive [Z3.FloatingPoint] |
Indicates whether a floating-point numeral is positive.
|
| is_numeral_subnormal [Z3.FloatingPoint] |
Indicates whether a floating-point numeral is subnormal.
|
| is_numeral_zero [Z3.FloatingPoint] |
Indicates whether a floating-point numeral is +zero or -zero.
|
| 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 elimination 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_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_rational [Z3.RCF] |
Return \c true if \c a represents a rational number.
|
| is_re_sort [Z3.Seq] |
test if sort is a regular expression sort
|
| 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_seq_sort [Z3.Seq] |
test if sort is a sequence sort
|
| 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 [Z3.Seq] |
test if expression is a string
|
| is_string_sort [Z3.Seq] |
test if sort is a string sort (a sequence of 8-bit bit-vectors)
|
| 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_transcendental [Z3.RCF] |
Return \c true if \c a represents a transcendental number.
|
| 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.RCF] |
less-than or equal
|
| 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.RCF] |
less-than
|
| 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_array_ext [Z3.Z3Array] |
Create array extensionality index given two arrays with the same sort.
|
| 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_char [Z3.Seq] | mk_char ctx i converts an integer to a character
|
| mk_char_from_bv [Z3.Seq] | mk_char_from_bv ctx bv converts the bitvector bv to a character
|
| mk_char_is_digit [Z3.Seq] | mk_char_is_digit ctx c checks if the character c is a digit
|
| mk_char_le [Z3.Seq] | mk_char_le ctx lc rc compares two characters
|
| mk_char_sort [Z3.Seq] |
create char sort
|
| mk_char_to_bv [Z3.Seq] | mk_char_to_bv ctx c converts the character c to a bitvector
|
| mk_char_to_int [Z3.Seq] | mk_char_to_int ctx c converts the character c to an integer
|
| 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_e [Z3.RCF] |
Return e (Euler's constant)
|
| 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] |
Creates a fresh function declaration with a name prefixed with a prefix string.
|
| 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_infinitesimal [Z3.RCF] |
Return a new infinitesimal that is smaller than all elements in the Z3 field.
|
| 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_int_to_str [Z3.Seq] |
convert an integer expression to a string
|
| 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_lambda [Z3.Quantifier] |
Create a lambda binding where bound variables are given by symbols and sorts
|
| mk_lambda_const [Z3.Quantifier] |
Create a lambda binding.
|
| 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_pi [Z3.RCF] |
Return Pi
|
| 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_quantifier_const [Z3.Quantifier] |
Create a Quantifier.
|
| mk_rational [Z3.RCF] |
Return a RCF rational using the given string.
|
| mk_re_complement [Z3.Seq] |
the regular expression complement
|
| mk_re_concat [Z3.Seq] |
concatenation of regular expressions
|
| mk_re_empty [Z3.Seq] |
the regular expression that accepts no sequences
|
| mk_re_full [Z3.Seq] |
the regular expression that accepts all sequences
|
| mk_re_intersect [Z3.Seq] |
intersection of regular expressions
|
| mk_re_loop [Z3.Seq] |
bounded loop regular expression
|
| mk_re_option [Z3.Seq] |
optional regular expression
|
| mk_re_plus [Z3.Seq] |
regular expression plus
|
| mk_re_range [Z3.Seq] |
regular expression for the range between two characters
|
| mk_re_sort [Z3.Seq] |
create regular expression sorts over sequences of the argument sort
|
| mk_re_star [Z3.Seq] |
regular expression star
|
| mk_re_union [Z3.Seq] |
union of regular expressions
|
| mk_real2int [Z3.Arithmetic.Real] |
Coerce a real to an integer.
|
| mk_rec_func_decl [Z3.FuncDecl] |
Creates a function declaration that can be used in a recursive function definition.
|
| mk_rec_func_decl_s [Z3.FuncDecl] |
Creates a function declaration that can be used in a recursive function definition.
|
| 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_roots [Z3.RCF] |
Extract the roots of a polynomial.
|
| 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_sbv_to_str [Z3.Seq] | mk_sbv_to_str ctx sbv convert a signed bitvector sbv to a string
|
| 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_seq_at [Z3.Seq] |
a unit sequence at index provided by second argument
|
| mk_seq_concat [Z3.Seq] |
sequence concatenation
|
| mk_seq_contains [Z3.Seq] |
predicate if the first argument contains the second
|
| mk_seq_empty [Z3.Seq] |
the empty sequence over base sort
|
| mk_seq_extract [Z3.Seq] |
extract sub-sequence starting at index given by second argument and of length provided by third argument
|
| mk_seq_in_re [Z3.Seq] |
regular expression membership predicate
|
| mk_seq_index [Z3.Seq] |
index of the first occurrence of the second argument in the first
|
| mk_seq_last_index [Z3.Seq] | mk_seq_last_index ctx s substr occurence of substr in the sequence s
|
| mk_seq_length [Z3.Seq] |
length of a sequence
|
| mk_seq_nth [Z3.Seq] | mk_seq_nth ctx s index retrieves from s the element at position index.
|
| mk_seq_prefix [Z3.Seq] |
predicate if the first argument is a prefix of the second
|
| mk_seq_replace [Z3.Seq] |
replace first occurrence of second argument by third
|
| mk_seq_sort [Z3.Seq] |
create a sequence sort
|
| mk_seq_suffix [Z3.Seq] |
predicate if the first argument is a suffix of the second
|
| mk_seq_to_re [Z3.Seq] |
create regular expression that accepts the argument sequence
|
| mk_seq_unit [Z3.Seq] |
a unit sequence
|
| 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_simplifier [Z3.Simplifier] |
Creates a new Simplifier.
|
| mk_sle [Z3.BitVector] |
Two's complement signed less-than or equal to.
|
| mk_slt [Z3.BitVector] |
Two's complement signed less-than
|
| mk_small_int [Z3.RCF] |
Return a RCF small integer.
|
| 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_ref [Z3.Datatype] | |
| mk_sort_ref_p [Z3.Datatype] |
Create a forward reference to a parametric datatype sort.
|
| mk_sort_ref_ps [Z3.Datatype] |
Create a forward reference to a parametric datatype sort.
|
| mk_sort_ref_s [Z3.Datatype] | |
| 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_str_le [Z3.Seq] |
compare strings less-than-or-equal
|
| mk_str_lt [Z3.Seq] |
compare strings less-than
|
| mk_str_to_int [Z3.Seq] |
retrieve integer expression encoded in string
|
| mk_string [Z3.Seq] |
create a string literal
|
| mk_string [Z3.Symbol] |
Creates a new symbol using a string.
|
| mk_string_from_code [Z3.Seq] | mk_string_from_code ctx c convert code c to a string
|
| mk_string_sort [Z3.Seq] |
create string sort
|
| mk_string_to_code [Z3.Seq] | mk_string_to_code ctx s convert a unit length string s to integer code
|
| 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] |
Conversion of a floating-point term into an unsigned bit-vector.
|
| mk_true [Z3.Boolean] |
The true Term.
|
| mk_ubv_to_str [Z3.Seq] | mk_ubv_to_str ctx ubv convert a unsigned bitvector ubv to a string
|
| 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.
|
| mul [Z3.RCF] |
Multiplication
|
N | |
| neg [Z3.RCF] |
Negation
|
| neq [Z3.RCF] |
not equal
|
| nil [Z3.Z3List] |
The empty list.
|
| not_ [Z3.Probe] |
Create a probe that evaluates to "true" when another probe does not evaluate to "true".
|
| num_coefficients [Z3.RCF] |
Return the number of coefficients in an algebraic number.
|
| num_sign_condition_coefficients [Z3.RCF] |
Return the size of a sign condition polynomial.
|
| num_to_decimal_string [Z3.RCF] |
Convert the RCF numeral into a string in decimal notation.
|
| num_to_string [Z3.RCF] |
Convert the RCF numeral into a string.
|
| 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 until one of them succeeds (i.e., the first that doesn't fail).
|
| 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_string [Z3.Fixedpoint] |
Parse an SMT-LIB2 string with fixedpoint rules.
|
| pop [Z3.Optimize] |
Backtrack one backtracking point.
|
| pop [Z3.Solver] |
Backtracks a number of backtracking points.
|
| power [Z3.RCF] |
Power
|
| push [Z3.Optimize] |
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 | |
| 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.Memory] |
Reset all allocated resources *
|
| 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.
|
| root_interval [Z3.RCF] | |
| roots [Z3.RCF] | |
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.
|
| sign_condition_coefficient [Z3.RCF] |
Extract a sign condition polynomial coefficient from an algebraic number.
|
| sign_condition_sign [Z3.RCF] |
Extract the sign of a sign condition from an algebraic number.
|
| sign_conditions [Z3.RCF] |
Extract sign conditions from an algebraic number.
|
| 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] | |
| sub [Z3.RCF] |
Subtraction
|
| 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 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.
|
| transcendental_name [Z3.RCF] |
Return the name of a transcendental.
|
| translate [Z3.Solver] |
Create a clone of the current solver with respect to a context.
|
| 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 | |
| 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.Simplifier] |
Create a simplifier that applies a simplifier using the given set of parameters.
|
| 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.Simplifier] | |
| with_ [Z3.Tactic] |
Create a tactic that applies a tactic using the given set of parameters.
|