Z3Context

Gets or sets a reference to a rounding mode for floating-point operations performed on Z3FloatingPoint instances created by this context.

Changes to this value change the rounding mode that is passed to the underlying Z3_mk_fpa_* methods that are generated via overloaded operators on Z3FloatingPoint instances.

Defaults to NearestTiesToEven rounding mode, if not configured.

Return the error code for the last API call.

Return true if the last API call resulted in an error.

Return the number of builtin probes available in Z3.

Return the number of builtin tactics available in Z3.

Return a string describing the given error code.

Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.

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 new optimize context.

Return a string describing all available parameters.

Return the parameter description set for the simplify procedure.

Interface to simplifier.

Provides an interface to the AST simplifier used by Z3. It returns an AST object which is equal to the argument. The returned AST is simplified using algebraic simplification rules, such as constant propagation (propagating true/false over logical connectives).

Interface to simplifier.

Provides an interface to the AST simplifier used by Z3. This procedure is similar to #Z3_simplify, but the behavior of the simplifier can be configured using the given parameter set.

Select mode for the format used for pretty-printing AST nodes.

The default mode for pretty printing AST nodes is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3AstPrintMode.printSmtlibFull. To print shared common subexpressions only once, use the Z3AstPrintMode.printLowLevel mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3AstPrintMode.printSmtlib2Compliant.

Convert the given benchmark into SMT-LIB formatted string.

Return Z3_INT_SYMBOL if the symbol was constructed using makeIntSymbol, and Z3_STRING_SYMBOL if the symbol was constructed using makeStringSymbol.

Return the symbol int value.

Return the symbol name.

Return the sort name as a symbol.

Return the sort kind (e.g., array, tuple, int, bool, etc).

Return the size of the given bit-vector sort.

Returns true if ast can be used as value in the Z3 real algebraic number package.

Returns true if ast is positive, false otherwise.

Returns true if ast is negative, false otherwise.

Returns true if ast is zero, false otherwise.

Returns 1 if ast is positive, 0 if ast is zero, and -1 if it is negative.

Return the value lhs + rhs.

Return the value lhs - rhs.

Return the value lhs * rhs.

Return the value lhs / rhs.

Return the ast^(1/k)

Return the ast^k

Return true if lhs < rhs, false otherwise.

Return true if lhs > rhs, false otherwise.

Return true if lhs <= rhs, false otherwise.

Return true if lhs >= rhs, false otherwise.

Return true if lhs == rhs, false otherwise.

Return true if lhs != rhs, false otherwise.

Given a multivariate polynomial polynomial(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial polynomial(a[0], ..., a[n-1], x_n).

Given a multivariate polynomial polynomial(x_0, ..., x_{n-1}), return the sign of polynomial(a[0], ..., a[n-1]).

Return the coefficients of the defining polynomial.

Return which root of the polynomial the algebraic number represents.

Create an AST node representing args[0] + ... + args[num_args-1].

All arguments must have int or real sort.

Create an AST node representing args[0] * ... * args[num_args-1].

All arguments must have int or real sort.

Create an AST node representing args[0] + ... + args[num_args-1].

All arguments must have int or real sort.

Create an AST node representing - arg. The arguments must have int or real type.

Create an AST node representing arg1 div arg2.

The arguments must either both have int type or both have real type. If the arguments have int type, then the result type is an int type, otherwise the the result type is real.

Create an AST node representing arg1 mod arg2.

The arguments must have int type.

Create an AST node representing arg1 rem arg2.

The arguments must have int type.

Create an AST node representing arg1 ^ arg2.

The arguments must have int or real type.

Create less than. The nodes t1 and t2 must have the same sort, and must be int or real.

Create less than or equal to. The nodes t1 and t2 must have the same sort, and must be int or real.

Create greater than. The nodes t1 and t2 must have the same sort, and must be int or real.

Create greater than or equal to. The nodes t1 and t2 must have the same sort, and must be int or real.

Create division predicate.

The nodes t1 and t2 must be of integer sort. The predicate is true when t1 divides t2. For the predicate to be part of linear integer arithmetic, the first argument t1 must be a non-zero integer.

Coerce an integer to a real.

There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.

You can take the floor of a real by creating an auxiliary integer constant k and and asserting mk_int2real(k) <= t1 < mk_int2real(k)+1.

The node t1 must have sort integer.

Coerce a real to an integer.

The semantics of this function follows the SMT-LIB standard for the function to_int

Coerce an integer to a float.

Coerce an integer to a float.

sort must be a float sort

Check if a real number is an integer.

Array read.

The argument a is the array and i is the index of the array that gets read.

The node a must have an array sort [domain -> range], and i must have the sort domain. The sort of the result is range.

• makeArraySort
• makeStore

Array read.

Type-erased version.

The argument a is the array and i is the index of the array that gets read.

The node a must have an array sort [domain -> range], and i must have the sort domain. The sort of the result is range.

• makeArraySort
• makeStore

n-ary Array read.

The argument a is the array and idxs are the indices of the array that gets read.

n-ary Array read.

Type-erased version.

The argument a is the array and idxs are the indices of the array that gets read.

Array update.

The node a must have an array sort [domain -> range], i must have sort domain, v must have sort range. The sort of the result is [domain -> range]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a (with respect to select) on all indices except for i, where it maps to v (and the select of a with respect to i may be a different value).

Array update.

Type-erased version.

The node a must have an array sort [domain -> range], i must have sort domain, v must have sort range. The sort of the result is [domain -> range]. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a (with respect to select) on all indices except for i, where it maps to v (and the select of a with respect to i may be a different value).

n-ary Array update.

n-ary Array update.

Type-erased version

Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value value.

Create the constant array.

Type-erased version

The resulting term is an array, such that a select on an arbitrary index produces the value value.

Map f on the argument arrays.

The n nodes args must be of array sorts [domain_i -> range_i]. The function declaration f must have type range_1 .. range_n -> range. v must have sort range. The sort of the result is [domain_i -> range].

Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Type-erased version.

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.

Create predicate that holds if Boolean array set has k elements set to true.

Creates a bit vector out of a given integer value.

Creates a bit vector out of a given integer value.

Bitwise negation.

The node t1 must have a bit-vector sort.

Take conjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

Take disjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

Bitwise and.

The nodes t1 and t2 must have the same bit-vector sort.

Bitwise or.

The nodes t1 and t2 must have the same bit-vector sort.

Bitwise exclusive-or.

The nodes t1 and t2 must have the same bit-vector sort.

Bitwise nand.

The nodes t1 and t2 must have the same bit-vector sort.

Bitwise nor.

The nodes t1 and t2 must have the same bit-vector sort.

Bitwise xnor.

The nodes t1 and t2 must have the same bit-vector sort.

Standard two’s complement unary minus.

The node t1 must have bit-vector sort.

Standard two’s complement addition.

The nodes t1 and t2 must have the same bit-vector sort.

Standard two’s complement subtraction.

The nodes t1 and t2 must have the same bit-vector sort.

Standard two’s complement multiplication.

The nodes t1 and t2 must have the same bit-vector sort.

Unsigned division.

It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined.

Two’s complement signed division.

It is defined in the following way:

• The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0.

• The ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Unsigned remainder.

It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Two’s complement signed remainder (sign follows dividend).

It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Two’s complement signed remainder (sign follows divisor).

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Unsigned less than.

The nodes t1 and t2 must have the same bit-vector sort.

Two’s complement signed less than.

It abbreviates:

(or (and (= (extract[|m-1|:|m-1|] t1) bit1)
        (= (extract[|m-1|:|m-1|] t2) bit0))
    (and (= (extract[|m-1|:|m-1|] t1) (extract[|m-1|:|m-1|] t2))
        (bvult t1 t2)))

The nodes t1 and t2 must have the same bit-vector sort.

Unsigned less than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Two’s complement signed less than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Unsigned greater than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Two’s complement signed greater than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Unsigned greater than.

The nodes t1 and t2 must have the same bit-vector sort.

Two’s complement signed greater than.

The nodes t1 and t2 must have the same bit-vector sort.

Concatenate the given bit-vectors.

The nodes t1 and t2 must have (possibly different) bit-vector sorts

The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

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.

The node t1 must have a bit-vector sort.

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.

The node t1 must have a bit-vector sort.

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.

The node t1 must have a bit-vector sort.

Repeat the given bit-vector up length i.

The node t1 must have a bit-vector sort.

Shift left.

It is equivalent to multiplication by 2^x where x is the value of the second argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

Logical shift right.

It is equivalent to unsigned division by 2^x where x is the value of the second argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

Arithmetic shift right.

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

Rotate bits of t1 to the left i times.

The node t1 must have a bit-vector sort.

Rotate bits of t1 to the right i times.

The node t1 must have a bit-vector sort.

Rotate bits of t1 to the left t2 times.

The nodes t1 and t2 must have the same bit-vector sort.

Rotate bits of t1 to the right t2 times.

The nodes t1 and t2 must have the same bit-vector sort.

Create an n bit bit-vector from the integer argument t1.

The resulting bit-vector has n bits, where the i'th bit (counting from 0 to n-1) is 1 if (t1 div 2^i) mod 2 is 1.

The node t1 must have integer sort.

Create an integer from the bit-vector argument t1.

If isSigned 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 isSigned is true, t1 is treated as a signed bit-vector.

The node t1 must have a bit-vector sort.

Create an integer from the bit-vector argument t1.

If isSigned 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 isSigned is true, t1 is treated as a signed bit-vector.

The node t1 must have a bit-vector sort.

Type-erased version.

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Create a predicate that checks that the bit-wise addition of t1 and t2 does not underflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not overflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not underflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

The node t1 must have bit-vector sort. The returned node is of sort Bool.

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not underflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Create a bit-vector numeral from a vector of Booleans.

Declare a constant or function.

After declaring a constant or function, the function makeApp() can be used to create a constant or function application.

Create a constant or function application.

Declare and create a constant.

This function is a shorthand for:

let symbol = context.makeStringSymbol(name)
let decl = context.makeFuncDecl(name: symbol, domain: [], range: sort)
let n = context.makeApply(decl, args: [])

Declare and create a constant.

This function is a shorthand for:

let decl = context.makeFuncDecl(name: name, domain: [], range: sort)
let n = context.makeApply(decl, args: [])

Declare and create a constant.

This function is a shorthand for:

let symbol = context.makeStringSymbol(name)
let n = context.makeConstant(name: symbol, sort: sort.getSort(self)).unsafeCastTo<T>()

Declare and create a constant.

This function is a shorthand for:

let symbol = context.makeStringSymbol(name)
let n = context.makeConstant(name: symbol, sort: sort.getSort(self)).unsafeCastTo<T>()

Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration. If prefix is different from nil, then the name generate by Z3 will start with prefix.

Declare and create a fresh constant.

This function is a shorthand for:

let decl = context.makeFreshFuncDecl(prefix: prefix, domain: [], range: sort)
let n = context.makeApply(decl, args: [])

Declare a recursive function

After declaring recursive function, it should be associated with a recursive definition addRecDef. The function makeApply() can be used to create a constant or function application.

Define the body of a recursive function.

After declaring a recursive function or a collection of mutually recursive functions, use this function to provide the definition for the recursive function.

Create a new fixedpoint context.

Create the RoundingMode sort.

Create a numeral of RoundingMode sort which represents the NearestTiesToEven 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 NearestTiesToAway rounding mode.

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Create a numeral of RoundingMode sort which represents the TowardZero 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 a floating-point NaN of sort sort.

Create a floating-point NaN of sort sort.

Create a floating-point infinity of sort sort.

When negative is true, -oo will be generated instead of +oo.

Create a floating-point infinity of sort sort.

When negative is true, -oo will be generated instead of +oo.

Create a floating-point zero of sort sort.

When negative is true, -zero will be generated instead of +zero.

Create a floating-point zero of sort sort.

When negative is true, -zero will be generated instead of +zero.

Create an expression of FloatingPoint sort from three bit-vector expressions.

This is the operator named fp' in the SMT FP theory definition. Note thatsgn` is required to be a bit-vector of size 1. Significand and exponent are required to be longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. The exponent is assumed to be in IEEE-754 biased representation.