Evaluate if predicate is constant.

Return nat if this is a constant natural number.

Return any bounding information we have about the term

Return integer if this is a constant integer.

Return any bounding information we have about the term

Return rational if this is a constant value.

Return any bounding information we have about the term

Return complex if this is a constant value.

Return a bitvector if this is a constant bitvector.

If we have bounds information about the term, return unsigned upper and lower bounds as integers

If we have bounds information about the term, return signed upper and lower bounds as integers

Return the string value if this is a constant string

Return the unique element value if this is a constant array, such as one made with constantArray.

Return the struct fields if this is a concrete struct.

Get type of expression.

Get the width of a bitvector

Print a sym expression for debugging or display purposes.

Get the argument types of a function.

Get the return type of a function.

Retrieve the configuration object corresponding to this solver interface.

Install an action that will be invoked before and after calls to backend solvers. This action is primarily intended to be used for logging/profiling/debugging purposes. Passing Nothing to this function disables logging.

Get the currently-installed solver log listener, if one has been installed.

Provide the given even to the currently installed solver log listener, if any.

Get statistics on execution from the initialization of the symbolic interface to this point. May return zeros if gathering statistics isn't supported.

Get current location of program for term creation purposes.

Set current location of program for term creation purposes.

Return true if two expressions are equal. The default implementation dispatches eqPred, bvEq, natEq, intEq, realEq, cplxEq, structEq, or arrayEq, depending on the type.

Take the if-then-else of two expressions. The default implementation dispatches itePred, bvIte, natIte, intIte, realIte, cplxIte, structIte, or arrayIte, depending on the type.

Given a symbolic expression, annotate it with a unique identifier that can be used to maintain a connection with the given term. The SymAnnotation is intended to be used as the key in a hash table or map to additional data can be maintained alongside the terms. The returned SymExpr has the same semantics as the arugmnent, but has embedded in it the SymAnnotation value so that it can be used later during term traversals.

Note, the returned annotation is not necessarily fresh; if an already-annotated term is passed in, the same annotation value will be returned.

Constant true predicate

Constant false predicate

Boolean negation

Boolean conjunction

Boolean disjunction

Boolean implication

Exclusive-or operation

Equality of boolean values

If-then-else on a predicate.

A natural number literal.

Add two natural numbers.

Subtract one number from another.

The result is undefined if this would result in a negative number.

Multiply one number by another.

natDiv sym x y performs division on naturals.

The result is undefined if y equals 0.

natDiv and natMod satisfy the property that given

  d <- natDiv sym x y
  m <- natMod sym x y

and y > 0, we have that y * d + m = x and m < y.

natMod sym x y returns x mod y.

See natDiv for a description of the properties the return value is expected to satisfy.

If-then-else applied to natural numbers.

Equality predicate for natural numbers.

natLe sym x y returns true if x <= y.

natLt sym x y returns true if x < y.

Create an integer literal.

Negate an integer.

Add two integers.

Subtract one integer from another.

Multiply one integer by another.

If-then-else applied to integers.

Integer equality.

Integer less-than-or-equal.

Integer less-than.

Compute the absolute value of an integer.

intDiv x y computes the integer division of x by y. This division is interpreted the same way as the SMT-Lib integer theory, which states that div and mod are the unique Eucledian division operations satisfying the following for all y /= 0:

• x * (div x y) + (mod x y) == x

•  0 <= mod x y < abs y

The value of intDiv x y is undefined when y = 0.

Integer division requires nonlinear support whenever the divisor is not a constant.

Note: div x y is floor (x/y) when y is positive (regardless of sign of x) and ceiling (x/y) when y is negative. This is neither of the more common "round toward zero" nor "round toward -inf" definitions.

Some useful theorems that are true of this division/modulus pair: * mod x y == mod x (- y) == mod x (abs y) * div x (-y) == -(div x y)

intMod x y computes the integer modulus of x by y. See intDiv for more details.

The value of intMod x y is undefined when y = 0.

Integer modulus requires nonlinear support whenever the divisor is not a constant.

intDivisible x k is true whenever x is an integer divisible by the known natural number k. In other words `divisible x k` holds if there exists an integer z such that `x = k*z`.

Create a bitvector with the given width and value.

Concatenate two bitvectors.

Select a subsequence from a bitvector.

2's complement negation.

Add two bitvectors.

Subtract one bitvector from another.

Multiply one bitvector by another.

Unsigned bitvector division.

The result of bvUdiv x y is undefined when y is zero, but is otherwise equal to floor( x / y ).

Unsigned bitvector remainder.

The result of bvUrem x y is undefined when y is zero, but is otherwise equal to x - (bvUdiv x y) * y.

Signed bitvector division. The result is truncated to zero.

The result of bvSdiv x y is undefined when y is zero, but is equal to floor(x/y) when x and y have the same sign, and equal to ceiling(x/y) when x and y have opposite signs.

NOTE! However, that there is a corner case when dividing MIN_INT by -1, in which case an overflow condition occurs, and the result is instead MIN_INT.

Signed bitvector remainder.

The result of bvSrem x y is undefined when y is zero, but is otherwise equal to x - (bvSdiv x y) * y.

Returns true if the corresponding bit in the bitvector is set.

Return true if bitvector is negative.

If-then-else applied to bitvectors.

Return true if bitvectors are equal.

Return true if bitvectors are distinct.

Unsigned less-than.

Unsigned less-than-or-equal.

Unsigned greater-than-or-equal.

Unsigned greater-than.

Signed less-than.

Signed greater-than.

Signed less-than-or-equal.

Signed greater-than-or-equal.

returns true if the given bitvector is non-zero.

Left shift. The shift amount is treated as an unsigned value.

Logical right shift. The shift amount is treated as an unsigned value.

Arithmetic right shift. The shift amount is treated as an unsigned value.

Rotate left. The rotate amount is treated as an unsigned value.

Rotate right. The rotate amount is treated as an unsigned value.

Zero-extend a bitvector.

Sign-extend a bitvector.

Truncate a bitvector.

Bitwise logical and.

Bitwise logical or.

Bitwise logical exclusive or.

Bitwise complement.

bvSet sym v i p returns a bitvector v' where bit i of v' is set to p, and the bits at the other indices are the same as in v.

bvFill sym w p returns a bitvector w-bits long where every bit is given by the boolean value of p.

Return the bitvector of the desired width with all 0 bits; this is the minimum unsigned integer.

Return the bitvector of the desired width with all bits set; this is the maximum unsigned integer.

Return the bitvector representing the largest 2's complement signed integer of the given width. This consists of all bits set except the MSB.

Return the bitvector representing the smallest 2's complement signed integer of the given width. This consists of all 0 bits except the MSB, which is set.

Return the number of 1 bits in the input.

Return the number of consecutive 0 bits in the input, starting from the most significant bit position. If the input is zero, all bits are counted as leading.

Return the number of consecutive 0 bits in the input, starting from the least significant bit position. If the input is zero, all bits are counted as leading.

Unsigned add with overflow bit.

Signed add with overflow bit. Overflow is true if positive + positive = negative, or if negative + negative = positive.

Unsigned subtract with overflow bit. Overflow is true if x < y.

Signed subtract with overflow bit. Overflow is true if positive - negative = negative, or if negative - positive = positive.

Compute the carryless multiply of the two input bitvectors. This operation is essentially the same as a standard multiply, except that the partial addends are simply XOR'd together instead of using a standard adder. This operation is useful for computing on GF(2^n) polynomials.

unsignedWideMultiplyBV sym x y multiplies two unsigned w bit numbers x and y.

It returns a pair containing the top w bits as the first element, and the lower w bits as the second element.

Compute the unsigned multiply of two values with overflow bit.

signedWideMultiplyBV sym x y multiplies two signed w bit numbers x and y.

It returns a pair containing the top w bits as the first element, and the lower w bits as the second element.

Compute the signed multiply of two values with overflow bit.

Create a struct from an assignment of expressions.

Get the value of a specific field in a struct.

Check if two structs are equal.

Take the if-then-else of two structures.

Create an array where each element has the same value.

Create an array from an arbitrary symbolic function.

Arrays created this way can typically not be compared for equality when provided to backend solvers.

Create an array by mapping a function over one or more existing arrays.

Update an array at a specific location.

Return element in array.

Create an array from a map of concrete indices to values.

This is implemented, but designed to be overridden for efficiency.

Update an array at specific concrete indices.

This is implemented, but designed to be overriden for efficiency.

If-then-else applied to arrays.

Return true if two arrays are equal.

Note that in the backend, arrays do not have a fixed number of elements, so this equality requires that arrays are equal on all elements.

Return true if all entries in the array are true.

Return true if the array has the value true at every index satisfying the given predicate.

Convert a natural number to an integer.

Convert an integer to a real number.

Convert the unsigned value of a bitvector to a natural.

Return the unsigned value of the given bitvector as an integer.

Return the signed value of the given bitvector as an integer.

Return 1 if the predicate is true; 0 otherwise.

Convert a natural number to a real number.

Convert an unsigned bitvector to a real number.

Convert an signed bitvector to a real number.

Round a real number to an integer.

Numbers are rounded to the nearest integer, with rounding away from zero when two integers are equi-distant (e.g., 1.5 rounds to 2).

Round a real number to an integer.

Numbers are rounded to the neareset integer, with rounding toward even values when two integers are equi-distant (e.g., 2.5 rounds to 2).

Round down to the nearest integer that is at most this value.

Round up to the nearest integer that is at least this value.

Round toward zero. This is floor(x) when x is positive and celing(x) when x is negative.

Convert an integer to a bitvector. The result is the unique bitvector whose value (signed or unsigned) is congruent to the input integer, modulo 2^w.

This operation has the following properties: * bvToInteger (integerToBv x w) == mod x (2^w) * bvToInteger (integerToBV x w) == x when 0 <= x < 2^w. * sbvToInteger (integerToBV x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1) * sbvToInteger (integerToBV x w) == x when -2^(w-1) <= x < 2^(w-1) * integerToBV (bvToInteger y) w == y when y is a SymBV sym w * integerToBV (sbvToInteger y) w == y when y is a SymBV sym w

Convert an integer to a natural number.

For negative integers, the result is undefined.

Convert a real number to an integer.

The result is undefined if the given real number does not represent an integer.

Convert a real number to a natural number.

The result is undefined if the given real number does not represent a natural number.

Convert a real number to an unsigned bitvector.

Numbers are rounded to the nearest representable number, with rounding away from zero when two integers are equi-distant (e.g., 1.5 rounds to 2). When the real is negative the result is zero.

Convert a real number to a signed bitvector.

Numbers are rounded to the nearest representable number, with rounding away from zero when two integers are equi-distant (e.g., 1.5 rounds to 2).

Convert an integer to the nearest signed bitvector.

Numbers are rounded to the nearest representable number.

Convert an integer to the nearest unsigned bitvector.

Numbers are rounded to the nearest representable number.

Convert a signed bitvector to the nearest signed bitvector with the given width. If the resulting width is smaller, this clamps the value to min-int or max-int when necessary.

Convert an unsigned bitvector to the nearest unsigned bitvector with the given width (clamp on overflow).

Convert an signed bitvector to the nearest unsigned bitvector with the given width (clamp on overflow).

Convert an unsigned bitvector to the nearest signed bitvector with the given width (clamp on overflow).

Create an empty string literal

Create a concrete string literal

Check the equality of two strings

If-then-else on strings

Concatenate two strings

Test if the first string contains the second string as a substring

Test if the first string is a prefix of the second string

Test if the first string is a suffix of the second string

Return the first position at which the second string can be found as a substring in the first string, starting from the given index. If no such position exists, return a negative value.

Compute the length of a string

stringSubstring s off len extracts the substring of s starting at index off and having length len. The result of this operation is undefined if off and len do not specify a valid substring of s; in particular, we must have off+len <= length(s).

Return real number 0.

Create a constant real literal.

Make a real literal from a scientific value. May be overridden if we want to avoid the overhead of converting scientific value to rational.

Check equality of two real numbers.

Check non-equality of two real numbers.

Check <= on two real numbers.

Check < on two real numbers.

Check >= on two real numbers.

Check > on two real numbers.

If-then-else on real numbers.

Negate a real number.

Add two real numbers.

Multiply two real numbers.

Subtract one real from another.

realSq sym x returns x * x.

realDiv sym x y returns term equivalent to x/y.

The result is undefined when y is zero.

realMod x y returns the value of x - y * floor(x / y) when y is not zero and x when y is zero.

Predicate that holds if the real number is an exact integer.

Return true if the real is non-negative.

realSqrt sym x returns sqrt(x). Result is undefined if x is negative.

realAtan2 sym y x returns the arctangent of y/x with a range of -pi to pi; this corresponds to the angle between the positive x-axis and the line from the origin (x,y).

When x is 0 this returns pi/2 * sgn y.

When x and y are both zero, this function is undefined.

Return value denoting pi.

Natural logarithm. realLog x is undefined for x <= 0.

Natural exponentiation

Sine trig function

Cosine trig function

Tangent trig function. realTan x is undefined when cos x = 0, i.e., when x = pi/2 + k*pi for some integer k.

Hyperbolic sine

Hyperbolic cosine

Hyperbolic tangent

Return absolute value of the real number.

realHypot x y returns sqrt(x^2 + y^2).

Return floating point number +0.

Return floating point number -0.

Return floating point NaN.

Return floating point +infinity.

Return floating point -infinity.

Create a floating point literal from a rational literal.

Negate a floating point number.

Return the absolute value of a floating point number.

Compute the square root of a floating point number.

Add two floating point numbers.

Subtract two floating point numbers.

Multiply two floating point numbers.

Divide two floating point numbers.

Compute the reminder: x - y * n, where n in Z is nearest to x / y.

Return the min of two floating point numbers.

Return the max of two floating point numbers.

Compute the fused multiplication and addition: (x * y) + z.

Check logical equality of two floating point numbers.

NOTE! This does NOT accurately represent the equality test on floating point values typically found in programming languages. See floatFpEq instead.

Check logical non-equality of two floating point numbers.

NOTE! This does NOT accurately represent the non-equality test on floating point values typically found in programming languages. See floatFpEq instead.

Check IEEE-754 equality of two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not equal to itself! Moreover, positive and negative 0 will compare equal, despite having different bit patterns.

This test is most appropriate for interpreting the equality tests of typical languages using floating point. Moreover, not-equal tests are usually the negation of this test, rather than the floatFpNe test below.

Check IEEE-754 non-equality of two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not distinct from any other value! Moreover, positive and negative 0 will not compare distinct, despite having different bit patterns.

This test usually does NOT correspond to the not-equal tests found in programming languages. Instead, one generally takes the logical negation of the floatFpEq test.

Check IEEE-754 <= on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not less-than-or-equal-to any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

Check IEEE-754 < on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not less-than any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

Check IEEE-754 >= on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not greater-than-or-equal-to any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

Check IEEE-754 > on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not greater-than any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

Test if a floating-point value is NaN.

Test if a floating-point value is (positive or negative) infinity.

Test if a floaint-point value is (positive or negative) zero.

Test if a floaint-point value is positive. NOTE! NaN is considered neither positive nor negative.

Test if a floaint-point value is negative. NOTE! NaN is considered neither positive nor negative.

Test if a floaint-point value is subnormal.

Test if a floaint-point value is normal.

If-then-else on floating point numbers.

Change the precision of a floating point number.

Round a floating point number to an integral value.

Convert from binary representation in IEEE 754-2008 format to floating point.

Convert from floating point from to the binary representation in IEEE 754-2008 format.

NOTE! NaN has multiple representations, i.e. all bit patterns where the exponent is 0b1..1 and the significant is not 0b0..0. This functions returns the representation of positive "quiet" NaN, i.e. the bit pattern where the sign is 0b0, the exponent is 0b1..1, and the significant is 0b10..0.

Convert a unsigned bitvector to a floating point number.

Convert a signed bitvector to a floating point number.

Convert a real number to a floating point number.

Convert a floating point number to a unsigned bitvector.

Convert a floating point number to a signed bitvector.

Convert a floating point number to a real number.

Create a complex from cartesian coordinates.

getRealPart x returns the real part of x.

getImagPart x returns the imaginary part of x.

Convert a complex number into the real and imaginary part.

Create a constant complex literal.

Create a complex from a real value.

If-then-else on complex values.

Negate a complex number.

Add two complex numbers together.

Subtract one complex number from another.

Multiply two complex numbers together.

Compute the magnitude of a complex number.

Return the principal square root of a complex number.

Compute sine of a complex number.

Compute cosine of a complex number.

Compute tangent of a complex number. cplxTan x is undefined when cplxCos x is 0, which occurs only along the real line in the same conditions where realCos x is 0.

hypotCplx x y returns sqrt(abs(x)^2 + abs(y)^2).

roundCplx x rounds complex number to nearest integer. Numbers with a fractional part of 0.5 are rounded away from 0. Imaginary and real parts are rounded independently.

cplxFloor x rounds to nearest integer less than or equal to x. Imaginary and real parts are rounded independently.

cplxCeil x rounds to nearest integer greater than or equal to x. Imaginary and real parts are rounded independently.

conjReal x returns the complex conjugate of the input.

Returns exponential of a complex number.

Check equality of two complex numbers.

Check non-equality of two complex numbers.