Crate z3_sys

Expand description

Z3

Z3 is a theorem prover from Microsoft Research.

This crate provides low-level bindings that provide no real affordances for usage from Rust and that mirror the C API.

For bindings that are easier to use from Rust, see the higher level bindings in the Z3 crate.

Example:

``````use z3_sys::*;

unsafe {
let cfg = Z3_mk_config();
let ctx = Z3_mk_context(cfg);

let a = Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx)));
let b = Z3_mk_not(ctx, Z3_mk_iff(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx)));
assert_eq!(Z3_mk_true(ctx), Z3_simplify(ctx, a));
assert_eq!(Z3_mk_true(ctx), Z3_simplify(ctx, b));

Z3_del_config(cfg);
Z3_del_context(ctx);
}``````

Functions

• Add a constant interpretation.
• Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0.
• Define the body of a recursive function.
• Return the value `a + b`.
• Return the value `a / b`.
• Return `true` if `a == b`, and `false` otherwise.
• Given a multivariate polynomial `p(x_0, ..., x_{n-1})`, return the sign of `p(a[0], ..., a[n-1])`.
• Return `true` if `a >= b`, and `false` otherwise.
• Return `true` if `a > b`, and `false` otherwise.
• Return `true` if `a` is negative, and `false` otherwise.
• Return `true` if `a` is positive, and `false` otherwise.
• Return `true` if `a` can be used as value in the Z3 real algebraic number package.
• Return `true` if `a` is zero, and `false` otherwise.
• Return `true` if `a <= b`, and `false` otherwise.
• Return `true` if `a < b`, and `false` otherwise.
• Return the value `a * b`.
• Return `true` if `a != b`, and `false` otherwise.
• Return the `a^k`
• Return the `a^(1/k)`
• Given a multivariate polynomial `p(x_0, ..., x_{n-1}, x_n)`, returns the roots of the univariate polynomial `p(a[0], ..., a[n-1], x_n)`.
• Return 1 if `a` is positive, 0 if `a` is zero, and -1 if `a` is negative.
• Return the value `a - b`.
• Convert a `Z3_app` into `Z3_ast`. This is just type casting.
• Append user-defined string to interaction log.
• Decrement the reference counter of the given `Z3_apply_result` object.
• Return the number of subgoals in the `Z3_apply_result` object returned by `Z3_tactic_apply`.
• Return one of the subgoals in the `Z3_apply_result` object returned by `Z3_tactic_apply`.
• Increment the reference counter of the given `Z3_apply_result` object.
• Convert the `Z3_apply_result` object returned by `Z3_tactic_apply` into a string.
• Return true if the map `m` contains the AST key `k`.
• Decrement the reference counter of the given AST map.
• Erase a key from the map.
• Return the value associated with the key `k`.
• Increment the reference counter of the given AST map.
• Store/Replace a new key, value pair in the given map.
• Return the keys stored in the given map.
• Remove all keys from the given map.
• Return the size of the given map.
• Convert the given map into a string.
• Convert the given AST node into a string.
• Decrement the reference counter of the given AST vector.
• Return the AST at position `i` in the AST vector `v`.
• Increment the reference counter of the given AST vector.
• Add the AST `a` in the end of the AST vector `v`. The size of `v` is increased by one.
• Resize the AST vector `v`.
• Update position `i` of the AST vector `v` with the AST `a`.
• Return the size of the given AST vector.
• Convert AST vector into a string.
• Translate the AST vector `v` from context `s` into an AST vector in context `t`.
• Convert the given benchmark into SMT-LIB formatted string.
• Close interaction log.
• Update record field with a value.
• Decrement the reference counter of the given AST. The context `c` should have been created using `Z3_mk_context_rc`. This function is a NOOP if `c` was created using `Z3_mk_context`.
• Delete the given configuration object.
• Reclaim memory allocated to constructor.
• Reclaim memory allocated for constructor list.
• Delete the given logical context.
• Disable tracing messages tagged as `tag` when Z3 is compiled in debug mode. It is a NOOP otherwise
• Enable tracing messages tagged as `tag` when Z3 is compiled in debug mode. It is a NOOP otherwise
• Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next evaluation builds on top of the previous call.
• Destroy all allocated resources.
• Set export callback for lemmas.
• Add property about the predicate `pred`. Add a property of predicate `pred` at `level`. It gets pushed forward when possible.
• Add a Database fact.
• Add an assumed invariant of predicate `pred`.
• Add a universal Horn clause as a named rule. The `horn_rule` should be of the form:
• Assert a constraint to the fixedpoint context.
• Decrement the reference counter of the given fixedpoint context.
• Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.
• Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string.
• Retrieve a formula that encodes satisfying answers to the query.
• Retrieve set of background assertions from fixedpoint context.
• Retrieve the current cover of `pred` up to `level` unfoldings. Return just the delta that is known at `level`. To obtain the full set of properties of `pred` one should query at `level`+1 , `level`+2 etc, and include `level`=-1.
• Retrieve a bottom-up (from query) sequence of ground facts
• Return a string describing all fixedpoint available parameters.
• Query the PDR engine for the maximal levels properties are known about predicate.
• Return the parameter description set for the given fixedpoint object.
• Retrieve reachable states of a predicate.
• Retrieve a string that describes the last status returned by `Z3_fixedpoint_query`.
• Obtain the list of rules along the counterexample trace.
• Retrieve set of rules from fixedpoint context.
• Obtain the list of rules along the counterexample trace.
• Retrieve statistics information from the last call to `Z3_fixedpoint_query`.
• Increment the reference counter of the given fixedpoint context
• Initialize the context with a user-defined state.
• Pose a query against the asserted rules.
• Pose a query against the asserted rules at the given level.
• Pose multiple queries against the asserted rules.
• Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.
• Set parameters on fixedpoint context.
• Configure the predicate representation.
• Register a callback for building terms based on the relational operators.
• Register a callback to destructive updates.
• Print the current rules and background axioms as a string.
• Update a named rule. A rule with the same name must have been previously created.
• Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
• Retrieves the exponent of a floating-point literal as a bit-vector expression.
• Return the exponent value of a floating-point numeral as a signed 64-bit integer
• Return the exponent value of a floating-point numeral as a string.
• Retrieves the sign of a floating-point literal.
• Retrieves the sign of a floating-point literal as a bit-vector expression.
• Retrieves the significand of a floating-point literal as a bit-vector expression.
• Return the significand value of a floating-point numeral as a string.
• Return the significand value of a floating-point numeral as a uint64.
• Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
• Checks whether a given floating-point numeral is a +oo or -oo.
• Checks whether a given floating-point numeral is a NaN.
• Checks whether a given floating-point numeral is negative.
• Checks whether a given floating-point numeral is normal.
• Checks whether a given floating-point numeral is positive.
• Checks whether a given floating-point numeral is subnormal.
• Checks whether a given floating-point numeral is +zero or -zero.
• Convert a `Z3_func_decl` into `Z3_ast`. This is just type casting.
• Convert the given func decl AST node into a string.
• Decrement the reference counter of the given `Z3_func_entry` object.
• Return an argument of a `Z3_func_entry` object.
• Return the number of arguments in a `Z3_func_entry` object.
• Return the value of this point.
• Increment the reference counter of the given `Z3_func_entry` object.
• add a function entry to a function interpretation.
• Decrement the reference counter of the given `Z3_func_interp` object.
• Return the arity (number of arguments) of the given function interpretation.
• Return the ‘else’ value of the given function interpretation.
• Return a “point” of the given function interpretation. It represents the value of `f` in a particular point.
• Return the number of entries in the given function interpretation.
• Increment the reference counter of the given `Z3_func_interp` object.
• Set the ‘else’ value of the given function interpretation.
• Return a lower bound for the given real algebraic number.
• Return an upper bound for the given real algebraic number.
• Return the i-th argument of the given application.
• Return the declaration of a constant or function application.
• Return the number of argument of an application. If `t` is an constant, then the number of arguments is 0.
• Alias for `Z3_get_domain_size`.
• Return the domain of the given array sort.
• Return the range of the given array sort.
• Return the function declaration `f` associated with a `(_ as_array f)` node.
• Return a hash code for the given AST.
• Return a unique identifier for `t`.
• Return the kind of the given AST.
• Return `Z3_L_TRUE` if `a` is true, `Z3_L_FALSE` if it is false, and `Z3_L_UNDEF` otherwise.
• Return the size of the given bit-vector sort.
• Return idx’th constructor.
• Return idx_a’th accessor for the idx_c’th constructor.
• Return number of constructors for datatype.
• Return idx’th recognizer.
• Return the expression value associated with an expression parameter.
• Return the double value associated with an double parameter.
• Return the expression value associated with an expression parameter.
• Return the integer value associated with an integer parameter.
• Return declaration kind corresponding to declaration.
• Return the constant declaration name as a symbol.
• Return the number of parameters associated with a declaration.
• Return the parameter type associated with a declaration.
• Return the rational value, as a string, associated with a rational parameter.
• Return the sort value associated with a sort parameter.
• Return the double value associated with an double parameter.
• Return the denominator (as a numeral AST) of a numeral AST of sort Real.
• Return the sort of the i-th parameter of the given function declaration.
• Return the number of parameters of the given declaration.
• Return the error code for the last API call.
• Return a string describing the given error code.
• Return the estimated allocated memory in bytes.
• Store the size of the sort in `r`. Return `false` if the call failed. That is, `Z3_get_sort_kind(s) == SortKind::FiniteDomain`
• Return a string that fully describes the version of Z3 in use.
• Return a unique identifier for `f`.
• Retrieve congruence class representatives for terms.
• Return index of de-Bruijn bound variable.
• Return the number of builtin probes available in Z3.
• Return the number of builtin tactics available in Z3.
• Return numeral as a string in decimal notation. The result has at most `precision` decimal places.
• Return numeral as a double.
• Similar to `Z3_get_numeral_string`, but only succeeds if the value can fit in a machine int. Return `true` if the call succeeded.
• Similar to `Z3_get_numeral_string`, but only succeeds if the value can fit in a machine `int64_t` int. Return `true` if the call succeeded.
• Similar to `Z3_get_numeral_string`, but only succeeds if the value can fit as a rational number as machine `int64_t` int. Return `true` if the call succeeded.
• Return numeral value, as a pair of 64 bit numbers if the representation fits.
• Return numeral value, as a string of a numeric constant term
• Similar to `Z3_get_numeral_string`, but only succeeds if the value can fit in a machine unsigned int. Return `true` if the call succeeded.
• Similar to `Z3_get_numeral_string` but only succeeds if the value can fit in a machine `uint64_t` int. Return `true` if the call succeeded.
• Return the numerator (as a numeral AST) of a numeral AST of sort Real.
• Return i’th ast in pattern.
• Return number of terms in pattern.
• Return the name of the `i` probe.
• Return body of quantifier.
• Return symbol of the i’th bound variable.
• Return sort of the i’th bound variable.
• Return i’th no_pattern.
• Return number of bound variables of quantifier.
• Return number of no_patterns used in quantifier.
• Return number of patterns used in quantifier.
• Return i’th pattern.
• Obtain weight of quantifier.
• Return the range of the given declaration.
• Return arity of relation.
• Return sort at i’th column of relation sort.
• Return the sort of an AST node.
• Return a unique identifier for `s`.
• Return the sort kind (e.g., array, tuple, int, bool, etc).
• Return the sort name as a symbol.
• Retrieve the string constant stored in `s`.
• Return the symbol int value.
• Return `SymbolKind::Int` if the symbol was constructed using `Z3_mk_int_symbol`, and `SymbolKind::String` if the symbol was constructed using `Z3_mk_string_symbol`.
• Return the symbol name.
• Return the name of the idx tactic.
• Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.
• Return the constructor declaration of the given tuple sort.
• Return the number of fields of the given tuple sort.
• Return Z3 version number information.
• Get a global (or module) parameter.
• Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).
• Set a global (or module) parameter. This setting is shared by all Z3 contexts.
• Add a new formula `a` to the given goal.
• Convert a model of the formulas of a goal to a model of an original goal. The model may be null, in which case the returned model is valid if the goal was established satisfiable.
• Decrement the reference counter of the given goal.
• Return the depth of the given goal. It tracks how many transformations were applied to it.
• Return a formula from the given goal.
• Increment the reference counter of the given goal.
• Return true if the given goal contains the formula `false`.
• Return true if the goal is empty, and it is precise or the product of a under approximation.
• Return true if the goal contains false, and it is precise or the product of an over approximation.
• Return the number of formulas, subformulas and terms in the given goal.
• Return the “precision” of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.
• Erase all formulas from the given goal.
• Return the number of formulas in the given goal.
• Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so the if caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.
• Convert a goal into a string.
• Copy a goal `g` from the context `source` to the context `target`.
• Increment the reference counter of the given AST. The context `c` should have been created using `Z3_mk_context_rc`. This function is a NOOP if `c` was created using `Z3_mk_context`.
• Interrupt the execution of a Z3 procedure.
• Return true if the given AST is a real algebraic number.
• The `(_ as-array f)` AST node is a construct for assigning interpretations for arrays in Z3.
• Compare terms.
• Compare terms.
• compare sorts.
• Determine if ast is a lambda expression.
• Determine if ast is an existential quantifier.
• Determine if quantifier is universal.
• Check if `s` is a regular expression sort.
• Check if `s` is a sequence sort.
• Determine if `s` is a string constant.
• Check if `s` is a string sort.
• Return true if the given expression `t` is well sorted.
• Create an AST node representing `args[0] + ... + args[num_args-1]`.
• Create an AST node representing `args[0] and ... and args[num_args-1]`.
• Create a constant or function application.
• Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
• Create array extensionality index given two arrays with the same sort. The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))
• Create an array type.
• Create an array type with N arguments
• Create array with the same interpretation as a function. The array satisfies the property (f x) = (select (_ as-array f) x) for every argument x.
• Return an empty mapping from AST to AST
• Return an empty AST vector.
• Pseudo-Boolean relations.
• Pseudo-Boolean relations.
• Create the Boolean type.
• Create a bound variable.
• Create an integer from the bit-vector argument `t1`. If `is_signed` is false, then the bit-vector `t1` is treated as unsigned. So the result is non-negative and in the range `[0..2^N-1]`, where N are the number of bits in `t1`. If `is_signed` is true, `t1` is treated as a signed bit-vector.
• create a bit-vector numeral from a vector of Booleans.
• Create a bit-vector type of the given size.
• Standard two’s complement addition.
• Create a predicate that checks that the bit-wise addition of `t1` and `t2` does not overflow.
• Create a predicate that checks that the bit-wise signed addition of `t1` and `t2` does not underflow.
• Bitwise and.
• Arithmetic shift right.
• Logical shift right.
• Standard two’s complement multiplication.
• Create a predicate that checks that the bit-wise multiplication of `t1` and `t2` does not overflow.
• Create a predicate that checks that the bit-wise signed multiplication of `t1` and `t2` does not underflow.
• Bitwise nand.
• Standard two’s complement unary minus.
• Check that bit-wise negation does not overflow when `t1` is interpreted as a signed bit-vector.
• Bitwise nor.
• Bitwise negation.
• Bitwise or.
• Take conjunction of bits in vector, return vector of length 1.
• Take disjunction of bits in vector, return vector of length 1.
• Two’s complement signed division.
• Create a predicate that checks that the bit-wise signed division of `t1` and `t2` does not overflow.
• Two’s complement signed greater than or equal to.
• Two’s complement signed greater than.
• Shift left.
• Two’s complement signed less than or equal to.
• Two’s complement signed less than.
• Two’s complement signed remainder (sign follows divisor).
• Two’s complement signed remainder (sign follows dividend).
• Standard two’s complement subtraction.
• Create a predicate that checks that the bit-wise signed subtraction of `t1` and `t2` does not overflow.
• Create a predicate that checks that the bit-wise subtraction of `t1` and `t2` does not underflow.
• Unsigned division.
• Unsigned greater than or equal to.
• Unsigned greater than.
• Unsigned less than or equal to.
• Unsigned less than.
• Unsigned remainder.
• Bitwise xnor.
• Bitwise exclusive-or.
• Concatenate the given bit-vectors.
• Create a configuration object for the Z3 context object.
• Declare and create a constant.
• Create the constant array.
• Create a constructor.
• Create list of constructors.
• Create a context using the given configuration.
• Create a context using the given configuration. This function is similar to `Z3_mk_context`. However, in the context returned by this function, the user is responsible for managing `Z3_ast` reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke `Z3_inc_ref` for any `Z3_ast` returned by Z3, and `Z3_dec_ref` whenever the `Z3_ast` is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
• Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
• Create mutually recursive datatypes.
• Create an AST node representing `distinct(args[0], ..., args[num_args-1])`.
• Create an AST node representing `arg1 div arg2`.
• Create the empty set.
• Create a enumeration sort.
• Create an AST node representing `l = r`.
• Create an exists formula. Similar to `Z3_mk_forall`.
• Rotate bits of `t1` to the left `t2` times.
• Rotate bits of `t1` to the right `t2` times.
• Extract the bits `high` down to `low` from a bit-vector of size `m` to yield a new bit-vector of size `n`, where `n = high - low + 1`.
• Create an AST node representing `false`.
• Create a named finite domain sort.
• Create a new fixedpoint context.
• Create a forall formula. It takes an expression `body` that contains bound variables of the same sorts as the sorts listed in the array `sorts`. The bound variables are de-Bruijn indices created using `Z3_mk_bound`. The array `decl_names` contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the `decl_names` and `sorts` array refers to the variable with index 0, the second to last element of `decl_names` and `sorts` refers to the variable with index 1, etc.
• Create a universal quantifier using a list of constants that will form the set of bound variables.
• Floating-point absolute value
• Floating-point division
• Floating-point equality.
• Floating-point fused multiply-add.
• Create an expression of FloatingPoint sort from three bit-vector expressions.
• Floating-point greater than or equal.
• Floating-point greater than.
• Create a floating-point infinity of sort `s`.
• Predicate indicating whether `t` is a floating-point number representing +oo or -oo.
• Predicate indicating whether `t` is a NaN.
• Predicate indicating whether `t` is a negative floating-point number.
• Predicate indicating whether `t` is a normal floating-point number.
• Predicate indicating whether `t` is a positive floating-point number.
• Predicate indicating whether `t` is a subnormal floating-point number.
• Predicate indicating whether `t` is a floating-point number with zero value, i.e., +zero or -zero.
• Floating-point less than or equal.
• Floating-point less than.
• Maximum of floating-point numbers.
• Minimum of floating-point numbers.
• Floating-point multiplication
• Create a floating-point NaN of sort `s`.
• Floating-point negation
• Create a numeral of FloatingPoint sort from a double.
• Create a numeral of FloatingPoint sort from a float.
• Create a numeral of FloatingPoint sort from a signed integer.
• Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
• Create a numeral of FloatingPoint sort from a sign bit and two integers.
• Floating-point remainder
• Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
• Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
• Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
• Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
• Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
• Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
• Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
• Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
• Create the RoundingMode sort.
• Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
• Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
• Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
• Create a FloatingPoint sort.
• Create the half-precision (16-bit) FloatingPoint sort.
• Create the single-precision (32-bit) FloatingPoint sort.
• Create the double-precision (64-bit) FloatingPoint sort.
• Create the quadruple-precision (128-bit) FloatingPoint sort.
• Create the double-precision (64-bit) FloatingPoint sort.
• Create the half-precision (16-bit) FloatingPoint sort.
• Create the quadruple-precision (128-bit) FloatingPoint sort.
• Create the single-precision (32-bit) FloatingPoint sort.
• Floating-point square root
• Floating-point subtraction
• Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
• Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
• Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
• Conversion of a term of real sort into a term of FloatingPoint sort.
• Conversion of a 2’s complement signed bit-vector term into a term of FloatingPoint sort.
• Conversion of a 2’s complement unsigned bit-vector term into a term of FloatingPoint sort.
• Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
• Conversion of a floating-point term into a real-numbered term.
• Conversion of a floating-point term into a signed bit-vector.
• Conversion of a floating-point term into an unsigned bit-vector.
• Create a floating-point zero of sort `s`.
• Declare and create a fresh constant.
• Declare a fresh constant or function.
• Create the full set.
• Declare a constant or function.
• Create greater than or equal to.
• Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
• Create greater than.
• Create an AST node representing `t1 iff t2`.
• Create an AST node representing `t1 implies t2`.
• Create a numeral of an int, bit-vector, or finite-domain sort.
• Create an `n` bit bit-vector from the integer argument `t1`.
• Coerce an integer to a real.
• Create a numeral of a int, bit-vector, or finite-domain sort.
• Create the integer type.
• Create a Z3 symbol using an integer.
• Integer to string conversion.
• Check if a real number is an integer.
• Create an AST node representing an if-then-else: `ite(t1, t2, t3)`.
• Create a lambda expression.
• Create a lambda expression using a list of constants that form the set of bound variables
• Create less than or equal to.
• Create a list sort
• Create less than.
• Map f on the argument arrays.
• Create an AST node representing `arg1 mod arg2`.
• Create a fresh model object. It has reference count 0.
• Create an AST node representing `args[0] * ... * args[num_args-1]`.
• Create an AST node representing `not(a)`.
• Create a numeral of a given sort.
• Create a new optimize context.
• Create an AST node representing `args[0] or ... or args[num_args-1]`.
• Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.
• Create a pattern for quantifier instantiation.
• Pseudo-Boolean relations.
• Pseudo-Boolean relations.
• Pseudo-Boolean relations.
• Create an AST node representing `arg1 ^ arg2`.
• Return a probe associated with the given name. The complete list of probes may be obtained using the procedures `Z3_get_num_probes` and `Z3_get_probe_name`. It may also be obtained using the command `(help-tactic)` in the SMT 2.0 front-end.
• Create a quantifier - universal or existential, with pattern hints. See the documentation for `Z3_mk_forall` for an explanation of the parameters.
• Create a universal or existential quantifier using a list of constants that will form the set of bound variables.
• Create a universal or existential quantifier using a list of constants that will form the set of bound variables.
• Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes
• Create the complement of the regular language `re`.
• Create the concatenation of the regular languages.
• Create an empty regular expression of sort `re`.
• Create an universal regular expression of sort `re`.
• Create the intersection of the regular languages.
• Create a regular expression loop. The supplied regular expression `r` is repeated between `lo` and `hi` times. The `lo` should be below `hi` with one execution: when supplying the value `hi` as 0, the meaning is to repeat the argument `r` at least `lo` number of times, and with an unbounded upper bound.
• Create the regular language `[re]`.
• Create the regular language `re+`.
• Create the range regular expression over two sequences of length 1.
• Create a regular expression sort out of a sequence sort.
• Create the regular language `re*`.
• Create the union of the regular languages.
• Create a real from a fraction.
• Coerce a real to an integer.
• Create the real type.
• Declare a recursive function
• Create an AST node representing `arg1 rem arg2`.
• Repeat the given bit-vector up length `i`.
• Rotate bits of `t1` to the left `i` times.
• Rotate bits of `t1` to the right `i` times.
• Array read. The argument `a` is the array and `i` is the index of the array that gets read.
• n-ary Array read. The argument `a` is the array and `idxs` are the indices of the array that gets read.
• Retrieve from `s` the unit sequence positioned at position `index`.
• Concatenate sequences.
• Check if `container` contains `containee`.
• Create an empty sequence of the sequence sort `seq`.
• Extract subsequence starting at `offset` of `length`.
• Check if `seq` is in the language generated by the regular expression `re`.
• Return index of first occurrence of `substr` in `s` starting from offset `offset`. If `s` does not contain `substr`, then the value is -1, if `offset` is the length of `s`, then the value is -1 as well. The function is under-specified if `offset` is negative or larger than the length of `s`.
• Return the length of the sequence `s`.
• Check if `prefix` is a prefix of `s`.
• Replace the first occurrence of `src` with `dst` in `s`.
• Create a sequence sort out of the sort for the elements.
• Check if `suffix` is a suffix of `s`.
• Create a regular expression that accepts the sequence `seq`.
• Create a unit sequence of `a`.
• Add an element to a set.
• Take the complement of a set.
• Remove an element to a set.
• Take the set difference between two sets.
• Take the intersection of a list of sets.
• Check for set membership.
• Create Set type.
• Check for subsetness of sets.
• Take the union of a list of sets.
• Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size `m+i`, where `m` is the size of the given bit-vector.
• Create a new incremental solver.
• Create a new solver. This solver is a “combined solver” (see combined_solver module) that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set.
• Create a new solver customized for the given logic. It behaves like `Z3_mk_solver` if the logic is unknown or unsupported.
• Create a new solver that is implemented using the given tactic. The solver supports the commands `Z3_solver_push` and `Z3_solver_pop`, but it will always solve each `Z3_solver_check` from scratch.
• Array update.
• n-ary Array update.
• Convert string to integer.
• Create a string constant out of the string that is passed in
• Create a sort for 8 bit strings.
• Create a Z3 symbol using a C string.
• Create an AST node representing `args[0] - ... - args[num_args - 1]`.
• Return a tactic associated with the given name.
• Create an AST node representing `true`.
• Create a tuple type.
• Create an AST node representing `- arg`.
• Create a free (uninterpreted) type using the given name (symbol).
• Create a numeral of a int, bit-vector, or finite-domain sort.
• Create a numeral of a int, bit-vector, or finite-domain sort.
• Create an AST node representing `t1 xor t2`.
• Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size `m+i`, where `m` is the size of the given bit-vector.
• Decrement the reference counter of the given model.
• Evaluate the AST node `t` in the given model. Return `true` if succeeded, and store the result in `v`.
• Extrapolates a model of a formula
• Return the i-th constant in the given model.
• Return the interpretation (i.e., assignment) of constant `a` in the model `m`.
• Return the declaration of the i-th function in the given model.
• Return the interpretation of the function `f` in the model `m`.
• Return the number of constants assigned by the given model.
• Return the number of function interpretations in the given model.
• Return the number of uninterpreted sorts that `m` assigns an interpretation to.
• Return an uninterpreted sort that `m` assigns an interpretation.
• Return the finite set of distinct values that represent the interpretation for sort `s`.
• Test if there exists an interpretation (i.e., assignment) for `a` in the model `m`.
• Increment the reference counter of the given model.
• Convert the given model into a string.
• Translate model from context `c` to context `dst`.
• Assert hard constraint to the optimization context.
• Assert soft constraint to the optimization context.
• Check consistency and produce optimal values.
• Decrement the reference counter of the given optimize context.
• Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
• Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
• Return the set of asserted formulas on the optimization context.
• Return a string containing a description of parameters accepted by optimize.
• Retrieve lower bound value or approximation for the i’th optimization objective.
• Retrieve lower bound value or approximation for the i’th optimization objective. The returned vector is of length 3. It always contains numerals. The three numerals are coefficients a, b, c and encode the result of `Z3_optimize_get_lower` a * infinity + b + c * epsilon.
• Retrieve the model for the last `Z3_optimize_check`.
• Return objectives on the optimization context. If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) …) If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.
• Return the parameter description set for the given optimize object.
• Retrieve a string that describes the last status returned by `Z3_optimize_check`.
• Retrieve statistics information from the last call to `Z3_optimize_check`
• Retrieve the unsat core for the last `Z3_optimize_check`.
• Retrieve upper bound value or approximation for the i’th optimization objective.
• Retrieve upper bound value or approximation for the i’th optimization objective.
• Increment the reference counter of the given optimize context
• Add a maximization constraint.
• Add a minimization constraint.
• Backtrack one level.
• Create a backtracking point.
• Set parameters on optimization context.
• Print the current context as a string.
• Decrement the reference counter of the given parameter description set.
• Retrieve documentation string corresponding to parameter name `s`.
• Return the kind associated with the given parameter name `n`.
• Return the number of parameters in the given parameter description set.
• Increment the reference counter of the given parameter description set.
• Return the number of parameters in the given parameter description set.
• Convert a parameter description set into a string. This function is mainly used for printing the contents of a parameter description set.
• Decrement the reference counter of the given parameter set.
• Increment the reference counter of the given parameter set.
• Add a Boolean parameter `k` with value `v` to the parameter set `p`.
• Add a double parameter `k` with value `v` to the parameter set `p`.
• Add a symbol parameter `k` with value `v` to the parameter set `p`.
• Add a unsigned parameter `k` with value `v` to the parameter set `p`.
• Convert a parameter set into a string. This function is mainly used for printing the contents of a parameter set.
• Validate the parameter set `p` against the parameter description set `d`.
• Similar to `Z3_parse_smtlib2_string`, but reads the benchmark from a file.
• Parse the given string using the SMT-LIB2 parser.
• Convert a `Z3_pattern` into `Z3_ast`. This is just type casting.
• Convert the given pattern AST node into a string.
• Return the nonzero subresultants of `p` and `q` with respect to the “variable” `x`.
• Return a probe that evaluates to “true” when `p1` and `p2` evaluates to true.
• Execute the probe over the goal. The probe always produce a double value. “Boolean” probes return 0.0 for false, and a value different from 0.0 for true.
• Return a probe that always evaluates to val.
• Decrement the reference counter of the given probe.
• Return a probe that evaluates to “true” when the value returned by `p1` is equal to the value returned by `p2`.
• Return a probe that evaluates to “true” when the value returned by `p1` is greater than or equal to the value returned by `p2`.
• Return a string containing a description of the probe with the given name.
• Return a probe that evaluates to “true” when the value returned by `p1` is greater than the value returned by `p2`.
• Increment the reference counter of the given probe.
• Return a probe that evaluates to “true” when the value returned by `p1` is less than or equal to the value returned by `p2`.
• Return a probe that evaluates to “true” when the value returned by `p1` is less than the value returned by `p2`.
• Return a probe that evaluates to “true” when `p` does not evaluate to true.
• Return a probe that evaluates to “true” when `p1` or `p2` evaluates to true.
• Best-effort quantifier elimination
• Project variables given a model
• Project variables given a model
• Query constructor for declared functions.
• Return the value `a + b`.
• Delete a RCF numeral created using the RCF API.
• Return the value `a / b`.
• Return `true` if `a == b`.
• Return `true` if `a >= b`.
• Extract the “numerator” and “denominator” of the given RCF numeral.
• Return `true` if `a > b`.
• Return the value `1/a`.
• Return `true` if `a <= b`.
• Return `true` if `a < b`.
• Return e (Euler’s constant)
• Return a new infinitesimal that is smaller than all elements in the Z3 field.
• Return Pi
• Return a RCF rational using the given string.
• Store in roots the roots of the polynomial `a[n-1]*x^{n-1} + ... + a[0]`. The output vector `roots` must have size `n`. It returns the number of roots of the polynomial.
• Return a RCF small integer.
• Return the value `a * b`.
• Return the value `-a`.
• Return `true` if `a != b`.
• Convert the RCF numeral into a string in decimal notation.
• Convert the RCF numeral into a string.
• Return the value `a^k`.
• Return the value `a - b`.
• Reset all allocated resources.
• Select mode for the format used for pretty-printing AST nodes.
• Set an error.
• Register a Z3 error handler.
• Set a configuration parameter.
• Interface to simplifier.
• Interface to simplifier.
• Return a string describing all available parameters.
• Return the parameter description set for the simplify procedure.
• Assert a constraint into the solver.
• Assert a constraint `a` into the solver, and track it (in the unsat) core using the Boolean constant `p`.
• Check whether the assertions in a given solver are consistent or not.
• Check whether the assertions in the given solver and optional assumptions are consistent or not.
• Extract a next cube for a solver. The last cube is the constant `true` or `false`. The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.
• Decrement the reference counter of the given solver.
• load solver assertions from a file.
• load solver assertions from a string.
• Return the set of asserted formulas on the solver.
• retrieve consequences from solver that determine values of the supplied function symbols.
• Return a string describing all solver available parameters.
• Retrieve the model for the last `Z3_solver_check`
• Return the set of non units in the solver state.
• Return the number of backtracking points.
• Return the parameter description set for the given solver object.
• Retrieve the proof for the last `Z3_solver_check`
• Return a brief justification for an “unknown” result (i.e., `Z3_L_UNDEF`) for the commands `Z3_solver_check`
• Return statistics for the given solver.
• Return the set of units modulo model conversion.
• Retrieve the unsat core for the last `Z3_solver_check_assumptions` The unsat core is a subset of the assumptions `a`.
• Ad-hoc method for importing model conversion from solver.
• Increment the reference counter of the given solver.
• Backtrack `n` backtracking points.
• Create a backtracking point.
• Remove all assertions from the solver.
• Set the given solver using the given parameters.
• Convert a solver into a string.
• Copy a solver `s` from the context `source` to the context `target`.
• Convert a `Z3_sort` into `Z3_ast`. This is just type casting.
• Convert the given sort AST node into a string.
• Decrement the reference counter of the given statistics object.
• Return the double value of the given statistical data.
• Return the key (a string) for a particular statistical data.
• Return the unsigned value of the given statistical data.
• Increment the reference counter of the given statistics object.
• Return `true` if the given statistical data is a double.
• Return `true` if the given statistical data is a unsigned integer.
• Return the number of statistical data in `s`.
• Convert a statistics into a string.
• Substitute every occurrence of `from[i]` in `a` with `to[i]`, for `i` smaller than `num_exprs`.
• Substitute the free variables in `a` with the expressions in `to`.
• Return a tactic that applies `t1` to a given goal and `t2` to every subgoal produced by `t1`.
• Apply tactic `t` to the goal `g`.
• Apply tactic `t` to the goal `g` using the parameter set `p`.
• Return a tactic that applies `t1` to a given goal if the probe `p` evaluates to true, and `t2` if `p` evaluates to false.
• Decrement the reference counter of the given tactic.
• Return a tactic that always fails.
• Return a tactic that fails if the probe `p` evaluates to false.
• Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).
• Return a string containing a description of the tactic with the given name.
• Return a string containing a description of parameters accepted by the given tactic.
• Return the parameter description set for the given tactic object.
• Increment the reference counter of the given tactic.
• Return a tactic that first applies `t1` to a given goal, if it fails then returns the result of `t2` applied to the given goal.
• Return a tactic that applies `t1` to a given goal and then `t2` to every subgoal produced by `t1`. The subgoals are processed in parallel.
• Return a tactic that applies the given tactics in parallel.
• Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
• Return a tactic that just return the given goal.
• Return a tactic that applies `t` to a given goal for `ms` milliseconds. If `t` does not terminate in `ms` milliseconds, then it fails.
• Return a tactic that applies `t` using the given set of parameters.
• Return a tactic that applies `t` to a given goal is the probe `p` evaluates to true. If `p` evaluates to false, then the new tactic behaves like the skip tactic.
• Convert an `ast` into an `Z3_app`. This is just type casting.
• Convert an AST into a `Z3_func_decl`. This is just type casting.
• Enable/disable printing warning messages to the console.
• Translate/Copy the AST `a` from context `source` to context `target`.
• Set a value of a context parameter.
• Update the arguments of term `a` using the arguments `args`.