Zee3.StdLib (zee3 v0.3.0)

Copy Markdown

Defines the functions and macros which are available inside the body of the Zee3.program/2 macro.

The functions of this module are all pure in the sense that they don't mutate the state of the solver. All the functions (but not necessarily the macros) return a Zee3.Smt2 term which will be handled correctly by the stateful special forms inside the program. The result of these functions can always be serialized into syntactically correct SMT-LIB2 code, which can be sent directly to the Z3 solver using the low-level API.

Summary

Functions

lhs * rhs

Multiplication (compiles to variadic chain if possible).

lhs + rhs

Addition (compiles to variadic chain if possible).

-arg

Unary arithmetic negation.

lhs - rhs

Binary/variadic subtraction.

lhs / rhs

Division (compiles to variadic chain if possible).

a != b

Check that two terms are distinct.

lhs < rhs

Less than (compiles to variadic chain if possible).

lhs <= rhs

Less than or equal (compiles to variadic chain if possible).

a == b

Check that two terms are equal.

lhs > rhs

Greater than (compiles to variadic chain if possible).

lhs >= rhs

Greater than or equal (compiles to variadic chain if possible).

abs(arg)

Absolute value.

all_distinct(args)

Checks that all the arguments are distinct.

all_equal(args)

Check if all the arguments are equal.

lhs and rhs

Logical AND (compiles to variadic chain if possible).

bvadd(lhs, rhs)

Addition.

bvand(lhs, rhs)

Bitwise AND.

bvashr(lhs, rhs)

Arithmetic shift right.

bvcomp(lhs, rhs)

Bit vector comparison.

bvlshr(lhs, rhs)

Logical shift right.

bvmul(lhs, rhs)

Multiplication.

bvnand(lhs, rhs)

Bitwise NAND.

bvneg(arg)

Two's complement negation.

bvnor(lhs, rhs)

Bitwise NOR.

bvnot(arg)

Bitwise NOT.

bvor(lhs, rhs)

Bitwise OR.

bvsdiv(lhs, rhs)

Signed division.

bvsge(lhs, rhs)

Signed greater than or equal.

bvsgt(lhs, rhs)

Signed greater than.

bvshl(lhs, rhs)

Logical shift left.

bvsle(lhs, rhs)

Signed less than or equal.

bvslt(lhs, rhs)

Signed less than.

bvsmod(lhs, rhs)

Signed modulo.

bvsrem(lhs, rhs)

Signed remainder.

bvsub(lhs, rhs)

Subtraction.

bvudiv(lhs, rhs)

Unsigned division.

bvuge(lhs, rhs)

Unsigned greater than or equal.

bvugt(lhs, rhs)

Unsigned greater than.

bvule(lhs, rhs)

Unsigned less than or equal.

bvult(lhs, rhs)

Unsigned less than.

bvurem(lhs, rhs)

Unsigned remainder.

bvxnor(lhs, rhs)

Bitwise XNOR.

bvxor(lhs, rhs)

Bitwise XOR.

concat(lhs, rhs)

Concatenate two bitvectors.

distinct(args)

Mutually distinct (variadic).

div(lhs, rhs)

Euclidean integer division.

extract(arg)

Extract sub-vector (indices passed in symbol).

fp(a, b, c)

Floating point constructor from BVs.

fp_abs(arg)

Absolute value.

fp_add(a, b, c)

Addition (requires rounding mode).

fp_div(a, b, c)

Division (requires rounding mode).

fp_eq(lhs, rhs)

Equality.

fp_fma(a, b, c, d)

Fused multiply-add (requires rounding mode).

fp_geq(lhs, rhs)

Greater than or equal.

fp_gt(lhs, rhs)

Greater than.

fp_isInfinite(arg)

Is infinite.

fp_isNaN(arg)

Is Not a Number.

fp_isNegative(arg)

Is negative.

fp_isNormal(arg)

Is normal.

fp_isPositive(arg)

Is positive.

fp_isSubnormal(arg)

Is subnormal.

fp_isZero(arg)

Is zero.

fp_leq(lhs, rhs)

Less than or equal.

fp_lt(lhs, rhs)

Less than.

fp_max(lhs, rhs)

Maximum.

fp_min(lhs, rhs)

Minimum.

fp_mul(a, b, c)

Multiplication (requires rounding mode).

fp_neg(arg)

Negation.

fp_rem(lhs, rhs)

Remainder.

fp_roundToIntegral(lhs, rhs)

Round to integral (requires rounding mode).

fp_sqrt(lhs, rhs)

Square root (requires rounding mode).

fp_sub(a, b, c)

Subtraction (requires rounding mode).

fp_to_real(arg)

Convert to real.

fp_to_sbv(lhs, rhs)

Convert to signed bitvector (requires rounding mode).

fp_to_ubv(lhs, rhs)

Convert to unsigned bitvector (requires rounding mode).

if(condition, branches)

A reimplementation of the Kernel.if/2 macro that raises an error if one tries to pick a branch based on a Zee3.Smt2 value.

int_to_str(arg)

Convert integer to string.

is_int(arg)

Check if real is an integer.

ite(a, b, c)

If-then-else conditional.

mod(lhs, rhs)

Euclidean integer remainder.

not arg

Logical negation.

or(args)

Logical OR (variadic).

product(args)

Multiply the arguments.

re_all()

Regex language of all strings.

re_allchar()

Regex matching any single character.

re_comp(arg)

Regex complement.

re_concat(args)

Regex concatenation (variadic).

re_inter(args)

Regex intersection (variadic).

re_kleene_plus(arg)

Kleene plus.

re_kleene_star(arg)

Kleene star.

re_none()

Empty regex language.

re_opt(arg)

Optional regex.

re_range(lhs, rhs)

Character range.

re_union(args)

Regex union (variadic).

select(lhs, rhs)

Read value from array at index.

store(a, b, c)

Write value to array at index.

str_++(args)

String concatenation (variadic).

str_<(lhs, rhs)

Lexicographical less than.

str_<=(lhs, rhs)

Lexicographical less than or equal.

str_contains(lhs, rhs)

Check if string contains substring.

str_in_re(lhs, rhs)

Check if string matches regex.

str_indexof(a, b, c)

Find index of substring after offset.

str_len(arg)

String length.

str_prefixof(lhs, rhs)

Check if string is prefix.

str_replace(a, b, c)

Replace first occurrence.

str_replace_all(a, b, c)

Replace all occurrences.

str_replace_re(a, b, c)

Replace first regex match.

str_replace_re_all(a, b, c)

Replace all regex matches.

str_substr(a, b, c)

Extract substring (string, offset, length).

str_suffixof(lhs, rhs)

Check if string is suffix.

str_to_int(arg)

Convert string to integer.

str_to_re(arg)

Convert string to regex.

sum(args)

Sum the arguments.

to_fp(lhs, rhs)

Convert to float (requires rounding mode).

to_fp_unsigned(lhs, rhs)

Convert unsigned BV to float.

to_int(arg)

Cast real to integer.

to_real(arg)

Cast integer to real.

xor(args)

Logical exclusive OR (variadic).

Functions

lhs * rhs

@spec Zee3.Smt2.smt2_like() * Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Multiplication (compiles to variadic chain if possible).

Theories: Ints, Reals.

lhs + rhs

@spec Zee3.Smt2.smt2_like() + Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Addition (compiles to variadic chain if possible).

Theories: Ints, Reals.

-arg

@spec -Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Unary arithmetic negation.

Theories: Ints, Reals.

lhs - rhs

@spec Zee3.Smt2.smt2_like() - Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Binary/variadic subtraction.

Theories: Ints, Reals.

lhs / rhs

@spec Zee3.Smt2.smt2_like() / Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Division (compiles to variadic chain if possible).

Theories: Reals.

a != b

@spec Zee3.Smt2.smt2_like() != Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Check that two terms are distinct.

lhs < rhs

@spec Zee3.Smt2.smt2_like() < Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Less than (compiles to variadic chain if possible).

Theories: Ints, Reals.

lhs <= rhs

@spec Zee3.Smt2.smt2_like() <= Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Less than or equal (compiles to variadic chain if possible).

Theories: Ints, Reals.

a == b

@spec Zee3.Smt2.smt2_like() == Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Check that two terms are equal.

lhs > rhs

@spec Zee3.Smt2.smt2_like() > Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Greater than (compiles to variadic chain if possible).

Theories: Ints, Reals.

lhs >= rhs

@spec Zee3.Smt2.smt2_like() >= Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Greater than or equal (compiles to variadic chain if possible).

Theories: Ints, Reals.

abs(arg)

@spec abs(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Absolute value.

Theories: Ints.

all_distinct(args)

@spec all_distinct([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Checks that all the arguments are distinct.

all_equal(args)

@spec all_equal([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Check if all the arguments are equal.

lhs and rhs

@spec Zee3.Smt2.smt2_like() and Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Logical AND (compiles to variadic chain if possible).

Theories: Core.

bvadd(lhs, rhs)

@spec bvadd(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Addition.

Theories: FixedSizeBitVectors.

bvand(lhs, rhs)

@spec bvand(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bitwise AND.

Theories: FixedSizeBitVectors.

bvashr(lhs, rhs)

@spec bvashr(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Arithmetic shift right.

Theories: FixedSizeBitVectors.

bvcomp(lhs, rhs)

@spec bvcomp(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bit vector comparison.

Theories: FixedSizeBitVectors.

bvlshr(lhs, rhs)

@spec bvlshr(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Logical shift right.

Theories: FixedSizeBitVectors.

bvmul(lhs, rhs)

@spec bvmul(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Multiplication.

Theories: FixedSizeBitVectors.

bvnand(lhs, rhs)

@spec bvnand(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bitwise NAND.

Theories: FixedSizeBitVectors.

bvneg(arg)

@spec bvneg(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Two's complement negation.

Theories: FixedSizeBitVectors.

bvnor(lhs, rhs)

@spec bvnor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bitwise NOR.

Theories: FixedSizeBitVectors.

bvnot(arg)

@spec bvnot(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bitwise NOT.

Theories: FixedSizeBitVectors.

bvor(lhs, rhs)

@spec bvor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bitwise OR.

Theories: FixedSizeBitVectors.

bvsdiv(lhs, rhs)

@spec bvsdiv(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Signed division.

Theories: FixedSizeBitVectors.

bvsge(lhs, rhs)

@spec bvsge(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Signed greater than or equal.

Theories: FixedSizeBitVectors.

bvsgt(lhs, rhs)

@spec bvsgt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Signed greater than.

Theories: FixedSizeBitVectors.

bvshl(lhs, rhs)

@spec bvshl(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Logical shift left.

Theories: FixedSizeBitVectors.

bvsle(lhs, rhs)

@spec bvsle(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Signed less than or equal.

Theories: FixedSizeBitVectors.

bvslt(lhs, rhs)

@spec bvslt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Signed less than.

Theories: FixedSizeBitVectors.

bvsmod(lhs, rhs)

@spec bvsmod(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Signed modulo.

Theories: FixedSizeBitVectors.

bvsrem(lhs, rhs)

@spec bvsrem(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Signed remainder.

Theories: FixedSizeBitVectors.

bvsub(lhs, rhs)

@spec bvsub(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Subtraction.

Theories: FixedSizeBitVectors.

bvudiv(lhs, rhs)

@spec bvudiv(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Unsigned division.

Theories: FixedSizeBitVectors.

bvuge(lhs, rhs)

@spec bvuge(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Unsigned greater than or equal.

Theories: FixedSizeBitVectors.

bvugt(lhs, rhs)

@spec bvugt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Unsigned greater than.

Theories: FixedSizeBitVectors.

bvule(lhs, rhs)

@spec bvule(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Unsigned less than or equal.

Theories: FixedSizeBitVectors.

bvult(lhs, rhs)

@spec bvult(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Unsigned less than.

Theories: FixedSizeBitVectors.

bvurem(lhs, rhs)

@spec bvurem(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Unsigned remainder.

Theories: FixedSizeBitVectors.

bvxnor(lhs, rhs)

@spec bvxnor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bitwise XNOR.

Theories: FixedSizeBitVectors.

bvxor(lhs, rhs)

@spec bvxor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Bitwise XOR.

Theories: FixedSizeBitVectors.

concat(lhs, rhs)

@spec concat(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Concatenate two bitvectors.

Theories: FixedSizeBitVectors.

distinct(args)

@spec distinct([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Mutually distinct (variadic).

Theories: Core.

div(lhs, rhs)

@spec div(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Euclidean integer division.

Theories: Ints.

extract(arg)

@spec extract(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Extract sub-vector (indices passed in symbol).

Theories: FixedSizeBitVectors.

fp(a, b, c)

@spec fp(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Floating point constructor from BVs.

Theories: FloatingPoint.

fp_abs(arg)

@spec fp_abs(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Absolute value.

Theories: FloatingPoint.

fp_add(a, b, c)

@spec fp_add(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Addition (requires rounding mode).

Theories: FloatingPoint.

fp_div(a, b, c)

@spec fp_div(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Division (requires rounding mode).

Theories: FloatingPoint.

fp_eq(lhs, rhs)

@spec fp_eq(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Equality.

Theories: FloatingPoint.

fp_fma(a, b, c, d)

@spec fp_fma(
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like()
) ::
  Zee3.Smt2.t()

Fused multiply-add (requires rounding mode).

Theories: FloatingPoint.

fp_geq(lhs, rhs)

@spec fp_geq(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Greater than or equal.

Theories: FloatingPoint.

fp_gt(lhs, rhs)

@spec fp_gt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Greater than.

Theories: FloatingPoint.

fp_isInfinite(arg)

@spec fp_isInfinite(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Is infinite.

Theories: FloatingPoint.

fp_isNaN(arg)

@spec fp_isNaN(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Is Not a Number.

Theories: FloatingPoint.

fp_isNegative(arg)

@spec fp_isNegative(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Is negative.

Theories: FloatingPoint.

fp_isNormal(arg)

@spec fp_isNormal(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Is normal.

Theories: FloatingPoint.

fp_isPositive(arg)

@spec fp_isPositive(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Is positive.

Theories: FloatingPoint.

fp_isSubnormal(arg)

@spec fp_isSubnormal(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Is subnormal.

Theories: FloatingPoint.

fp_isZero(arg)

@spec fp_isZero(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Is zero.

Theories: FloatingPoint.

fp_leq(lhs, rhs)

@spec fp_leq(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Less than or equal.

Theories: FloatingPoint.

fp_lt(lhs, rhs)

@spec fp_lt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Less than.

Theories: FloatingPoint.

fp_max(lhs, rhs)

@spec fp_max(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Maximum.

Theories: FloatingPoint.

fp_min(lhs, rhs)

@spec fp_min(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Minimum.

Theories: FloatingPoint.

fp_mul(a, b, c)

@spec fp_mul(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Multiplication (requires rounding mode).

Theories: FloatingPoint.

fp_neg(arg)

@spec fp_neg(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Negation.

Theories: FloatingPoint.

fp_rem(lhs, rhs)

@spec fp_rem(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Remainder.

Theories: FloatingPoint.

fp_roundToIntegral(lhs, rhs)

@spec fp_roundToIntegral(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Round to integral (requires rounding mode).

Theories: FloatingPoint.

fp_sqrt(lhs, rhs)

@spec fp_sqrt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Square root (requires rounding mode).

Theories: FloatingPoint.

fp_sub(a, b, c)

@spec fp_sub(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Subtraction (requires rounding mode).

Theories: FloatingPoint.

fp_to_real(arg)

@spec fp_to_real(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert to real.

Theories: FloatingPoint.

fp_to_sbv(lhs, rhs)

@spec fp_to_sbv(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert to signed bitvector (requires rounding mode).

Theories: FloatingPoint.

fp_to_ubv(lhs, rhs)

@spec fp_to_ubv(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert to unsigned bitvector (requires rounding mode).

Theories: FloatingPoint.

if(condition, branches)

(macro)

A reimplementation of the Kernel.if/2 macro that raises an error if one tries to pick a branch based on a Zee3.Smt2 value.

If you're trying to pick a branch based on a Zee3.Smt2 value, you're probably making a mistake because all Zee3.Smt2 terms are considered true by the normal Kernel.if/2 macro.

If you want to pick a branch based on a condition inside Z3, you want to use the ite/3 function instead.

This macro is automatically imported inside the body of the Zee3.program do ... end macro. Apart from raising an error on Zee3.Smt2 terms, it behaves exactly as the Kernel.if/2 macro.

int_to_str(arg)

@spec int_to_str(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert integer to string.

Theories: Strings.

is_int(arg)

@spec is_int(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Check if real is an integer.

Theories: Reals_Ints.

ite(a, b, c)

@spec ite(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

If-then-else conditional.

Theories: Core.

mod(lhs, rhs)

@spec mod(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Euclidean integer remainder.

Theories: Ints.

not arg

@spec not Zee3.Smt2.smt2_like() :: Zee3.Smt2.t()

Logical negation.

Theories: Core.

or(args)

@spec or([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Logical OR (variadic).

Theories: Core.

product(args)

@spec product([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Multiply the arguments.

re_all()

Regex language of all strings.

Theories: Strings.

re_allchar()

Regex matching any single character.

Theories: Strings.

re_comp(arg)

@spec re_comp(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Regex complement.

Theories: Strings.

re_concat(args)

@spec re_concat([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Regex concatenation (variadic).

Theories: Strings.

re_inter(args)

@spec re_inter([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Regex intersection (variadic).

Theories: Strings.

re_kleene_plus(arg)

@spec re_kleene_plus(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Kleene plus.

Theories: Strings.

re_kleene_star(arg)

@spec re_kleene_star(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Kleene star.

Theories: Strings.

re_none()

Empty regex language.

Theories: Strings.

re_opt(arg)

@spec re_opt(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Optional regex.

Theories: Strings.

re_range(lhs, rhs)

@spec re_range(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Character range.

Theories: Strings.

re_union(args)

@spec re_union([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Regex union (variadic).

Theories: Strings.

select(lhs, rhs)

@spec select(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Read value from array at index.

Theories: ArraysEx.

store(a, b, c)

@spec store(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Write value to array at index.

Theories: ArraysEx.

str_++(args)

@spec str_ ++ [Zee3.Smt2.smt2_like()] :: Zee3.Smt2.t()

String concatenation (variadic).

Theories: Strings.

str_<(lhs, rhs)

@spec str_<(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Lexicographical less than.

Theories: Strings.

str_<=(lhs, rhs)

@spec str_<=(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Lexicographical less than or equal.

Theories: Strings.

str_contains(lhs, rhs)

@spec str_contains(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Check if string contains substring.

Theories: Strings.

str_in_re(lhs, rhs)

@spec str_in_re(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Check if string matches regex.

Theories: Strings.

str_indexof(a, b, c)

@spec str_indexof(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Find index of substring after offset.

Theories: Strings.

str_len(arg)

@spec str_len(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

String length.

Theories: Strings.

str_prefixof(lhs, rhs)

@spec str_prefixof(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Check if string is prefix.

Theories: Strings.

str_replace(a, b, c)

@spec str_replace(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Replace first occurrence.

Theories: Strings.

str_replace_all(a, b, c)

@spec str_replace_all(
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like()
) ::
  Zee3.Smt2.t()

Replace all occurrences.

Theories: Strings.

str_replace_re(a, b, c)

@spec str_replace_re(
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like()
) ::
  Zee3.Smt2.t()

Replace first regex match.

Theories: Strings.

str_replace_re_all(a, b, c)

@spec str_replace_re_all(
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like(),
  Zee3.Smt2.smt2_like()
) ::
  Zee3.Smt2.t()

Replace all regex matches.

Theories: Strings.

str_substr(a, b, c)

@spec str_substr(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) ::
  Zee3.Smt2.t()

Extract substring (string, offset, length).

Theories: Strings.

str_suffixof(lhs, rhs)

@spec str_suffixof(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Check if string is suffix.

Theories: Strings.

str_to_int(arg)

@spec str_to_int(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert string to integer.

Theories: Strings.

str_to_re(arg)

@spec str_to_re(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert string to regex.

Theories: Strings.

sum(args)

@spec sum([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Sum the arguments.

to_fp(lhs, rhs)

@spec to_fp(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert to float (requires rounding mode).

Theories: FloatingPoint.

to_fp_unsigned(lhs, rhs)

@spec to_fp_unsigned(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Convert unsigned BV to float.

Theories: FloatingPoint.

to_int(arg)

@spec to_int(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Cast real to integer.

Theories: Reals_Ints.

to_real(arg)

@spec to_real(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()

Cast integer to real.

Theories: Reals_Ints.

xor(args)

@spec xor([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t()

Logical exclusive OR (variadic).

Theories: Core.