# `Zee3.StdLib` 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. # `*` ```elixir @spec Zee3.Smt2.smt2_like() * Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Multiplication (compiles to variadic chain if possible). *Theories*: Ints, Reals. # `+` ```elixir @spec Zee3.Smt2.smt2_like() + Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Addition (compiles to variadic chain if possible). *Theories*: Ints, Reals. # `-` ```elixir @spec -Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Unary arithmetic negation. *Theories*: Ints, Reals. # `-` ```elixir @spec Zee3.Smt2.smt2_like() - Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Binary/variadic subtraction. *Theories*: Ints, Reals. # `/` ```elixir @spec Zee3.Smt2.smt2_like() / Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Division (compiles to variadic chain if possible). *Theories*: Reals. # `!=` ```elixir @spec Zee3.Smt2.smt2_like() != Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Check that two terms are distinct. # `<` ```elixir @spec Zee3.Smt2.smt2_like() < Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Less than (compiles to variadic chain if possible). *Theories*: Ints, Reals. # `<=` ```elixir @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. # `==` ```elixir @spec Zee3.Smt2.smt2_like() == Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Check that two terms are equal. # `>` ```elixir @spec Zee3.Smt2.smt2_like() > Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Greater than (compiles to variadic chain if possible). *Theories*: Ints, Reals. # `>=` ```elixir @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` ```elixir @spec abs(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Absolute value. *Theories*: Ints. # `all_distinct` ```elixir @spec all_distinct([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Checks that all the arguments are distinct. # `all_equal` ```elixir @spec all_equal([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Check if all the arguments are equal. # `and` ```elixir @spec Zee3.Smt2.smt2_like() and Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Logical AND (compiles to variadic chain if possible). *Theories*: Core. # `bvadd` ```elixir @spec bvadd(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Addition. *Theories*: FixedSizeBitVectors. # `bvand` ```elixir @spec bvand(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bitwise AND. *Theories*: FixedSizeBitVectors. # `bvashr` ```elixir @spec bvashr(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Arithmetic shift right. *Theories*: FixedSizeBitVectors. # `bvcomp` ```elixir @spec bvcomp(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bit vector comparison. *Theories*: FixedSizeBitVectors. # `bvlshr` ```elixir @spec bvlshr(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Logical shift right. *Theories*: FixedSizeBitVectors. # `bvmul` ```elixir @spec bvmul(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Multiplication. *Theories*: FixedSizeBitVectors. # `bvnand` ```elixir @spec bvnand(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bitwise NAND. *Theories*: FixedSizeBitVectors. # `bvneg` ```elixir @spec bvneg(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Two's complement negation. *Theories*: FixedSizeBitVectors. # `bvnor` ```elixir @spec bvnor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bitwise NOR. *Theories*: FixedSizeBitVectors. # `bvnot` ```elixir @spec bvnot(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bitwise NOT. *Theories*: FixedSizeBitVectors. # `bvor` ```elixir @spec bvor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bitwise OR. *Theories*: FixedSizeBitVectors. # `bvsdiv` ```elixir @spec bvsdiv(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Signed division. *Theories*: FixedSizeBitVectors. # `bvsge` ```elixir @spec bvsge(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Signed greater than or equal. *Theories*: FixedSizeBitVectors. # `bvsgt` ```elixir @spec bvsgt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Signed greater than. *Theories*: FixedSizeBitVectors. # `bvshl` ```elixir @spec bvshl(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Logical shift left. *Theories*: FixedSizeBitVectors. # `bvsle` ```elixir @spec bvsle(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Signed less than or equal. *Theories*: FixedSizeBitVectors. # `bvslt` ```elixir @spec bvslt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Signed less than. *Theories*: FixedSizeBitVectors. # `bvsmod` ```elixir @spec bvsmod(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Signed modulo. *Theories*: FixedSizeBitVectors. # `bvsrem` ```elixir @spec bvsrem(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Signed remainder. *Theories*: FixedSizeBitVectors. # `bvsub` ```elixir @spec bvsub(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Subtraction. *Theories*: FixedSizeBitVectors. # `bvudiv` ```elixir @spec bvudiv(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Unsigned division. *Theories*: FixedSizeBitVectors. # `bvuge` ```elixir @spec bvuge(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Unsigned greater than or equal. *Theories*: FixedSizeBitVectors. # `bvugt` ```elixir @spec bvugt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Unsigned greater than. *Theories*: FixedSizeBitVectors. # `bvule` ```elixir @spec bvule(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Unsigned less than or equal. *Theories*: FixedSizeBitVectors. # `bvult` ```elixir @spec bvult(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Unsigned less than. *Theories*: FixedSizeBitVectors. # `bvurem` ```elixir @spec bvurem(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Unsigned remainder. *Theories*: FixedSizeBitVectors. # `bvxnor` ```elixir @spec bvxnor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bitwise XNOR. *Theories*: FixedSizeBitVectors. # `bvxor` ```elixir @spec bvxor(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Bitwise XOR. *Theories*: FixedSizeBitVectors. # `concat` ```elixir @spec concat(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Concatenate two bitvectors. *Theories*: FixedSizeBitVectors. # `distinct` ```elixir @spec distinct([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Mutually distinct (variadic). *Theories*: Core. # `div` ```elixir @spec div(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Euclidean integer division. *Theories*: Ints. # `extract` ```elixir @spec extract(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Extract sub-vector (indices passed in symbol). *Theories*: FixedSizeBitVectors. # `fp` ```elixir @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` ```elixir @spec fp_abs(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Absolute value. *Theories*: FloatingPoint. # `fp_add` ```elixir @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` ```elixir @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` ```elixir @spec fp_eq(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Equality. *Theories*: FloatingPoint. # `fp_fma` ```elixir @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` ```elixir @spec fp_geq(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Greater than or equal. *Theories*: FloatingPoint. # `fp_gt` ```elixir @spec fp_gt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Greater than. *Theories*: FloatingPoint. # `fp_isInfinite` ```elixir @spec fp_isInfinite(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Is infinite. *Theories*: FloatingPoint. # `fp_isNaN` ```elixir @spec fp_isNaN(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Is Not a Number. *Theories*: FloatingPoint. # `fp_isNegative` ```elixir @spec fp_isNegative(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Is negative. *Theories*: FloatingPoint. # `fp_isNormal` ```elixir @spec fp_isNormal(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Is normal. *Theories*: FloatingPoint. # `fp_isPositive` ```elixir @spec fp_isPositive(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Is positive. *Theories*: FloatingPoint. # `fp_isSubnormal` ```elixir @spec fp_isSubnormal(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Is subnormal. *Theories*: FloatingPoint. # `fp_isZero` ```elixir @spec fp_isZero(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Is zero. *Theories*: FloatingPoint. # `fp_leq` ```elixir @spec fp_leq(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Less than or equal. *Theories*: FloatingPoint. # `fp_lt` ```elixir @spec fp_lt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Less than. *Theories*: FloatingPoint. # `fp_max` ```elixir @spec fp_max(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Maximum. *Theories*: FloatingPoint. # `fp_min` ```elixir @spec fp_min(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Minimum. *Theories*: FloatingPoint. # `fp_mul` ```elixir @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` ```elixir @spec fp_neg(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Negation. *Theories*: FloatingPoint. # `fp_rem` ```elixir @spec fp_rem(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Remainder. *Theories*: FloatingPoint. # `fp_roundToIntegral` ```elixir @spec fp_roundToIntegral(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Round to integral (requires rounding mode). *Theories*: FloatingPoint. # `fp_sqrt` ```elixir @spec fp_sqrt(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Square root (requires rounding mode). *Theories*: FloatingPoint. # `fp_sub` ```elixir @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` ```elixir @spec fp_to_real(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Convert to real. *Theories*: FloatingPoint. # `fp_to_sbv` ```elixir @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` ```elixir @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` *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` ```elixir @spec int_to_str(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Convert integer to string. *Theories*: Strings. # `is_int` ```elixir @spec is_int(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Check if real is an integer. *Theories*: Reals_Ints. # `ite` ```elixir @spec ite(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` If-then-else conditional. *Theories*: Core. # `mod` ```elixir @spec mod(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Euclidean integer remainder. *Theories*: Ints. # `not` ```elixir @spec not Zee3.Smt2.smt2_like() :: Zee3.Smt2.t() ``` Logical negation. *Theories*: Core. # `or` ```elixir @spec or([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Logical OR (variadic). *Theories*: Core. # `product` ```elixir @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` ```elixir @spec re_comp(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Regex complement. *Theories*: Strings. # `re_concat` ```elixir @spec re_concat([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Regex concatenation (variadic). *Theories*: Strings. # `re_inter` ```elixir @spec re_inter([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Regex intersection (variadic). *Theories*: Strings. # `re_kleene_plus` ```elixir @spec re_kleene_plus(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Kleene plus. *Theories*: Strings. # `re_kleene_star` ```elixir @spec re_kleene_star(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Kleene star. *Theories*: Strings. # `re_none` Empty regex language. *Theories*: Strings. # `re_opt` ```elixir @spec re_opt(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Optional regex. *Theories*: Strings. # `re_range` ```elixir @spec re_range(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Character range. *Theories*: Strings. # `re_union` ```elixir @spec re_union([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Regex union (variadic). *Theories*: Strings. # `select` ```elixir @spec select(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Read value from array at index. *Theories*: ArraysEx. # `store` ```elixir @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_++` ```elixir @spec str_ ++ [Zee3.Smt2.smt2_like()] :: Zee3.Smt2.t() ``` String concatenation (variadic). *Theories*: Strings. # `str_<` ```elixir @spec str_<(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Lexicographical less than. *Theories*: Strings. # `str_<=` ```elixir @spec str_<=(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Lexicographical less than or equal. *Theories*: Strings. # `str_contains` ```elixir @spec str_contains(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Check if string contains substring. *Theories*: Strings. # `str_in_re` ```elixir @spec str_in_re(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Check if string matches regex. *Theories*: Strings. # `str_indexof` ```elixir @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` ```elixir @spec str_len(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` String length. *Theories*: Strings. # `str_prefixof` ```elixir @spec str_prefixof(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Check if string is prefix. *Theories*: Strings. # `str_replace` ```elixir @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` ```elixir @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` ```elixir @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` ```elixir @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` ```elixir @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` ```elixir @spec str_suffixof(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Check if string is suffix. *Theories*: Strings. # `str_to_int` ```elixir @spec str_to_int(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Convert string to integer. *Theories*: Strings. # `str_to_re` ```elixir @spec str_to_re(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Convert string to regex. *Theories*: Strings. # `sum` ```elixir @spec sum([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Sum the arguments. # `to_fp` ```elixir @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` ```elixir @spec to_fp_unsigned(Zee3.Smt2.smt2_like(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Convert unsigned BV to float. *Theories*: FloatingPoint. # `to_int` ```elixir @spec to_int(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Cast real to integer. *Theories*: Reals_Ints. # `to_real` ```elixir @spec to_real(Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t() ``` Cast integer to real. *Theories*: Reals_Ints. # `xor` ```elixir @spec xor([Zee3.Smt2.smt2_like()]) :: Zee3.Smt2.t() ``` Logical exclusive OR (variadic). *Theories*: Core. --- *Consult [api-reference.md](api-reference.md) for complete listing*