Index of values

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

kind [Z3.Symbol]

The kind of the symbol (int or string)

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

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

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]