Zee3.Smt2 (zee3 v0.6.0)

Copy Markdown

Summary

Types

smt2_like()

A value which is either an Smt2 value or a literal that can be unambiguously be converted into an Smt2 value.

t()

An Smt2 value, which can be serialized and sent to Z3.

Functions

bit_vec16_from_integer(integer)

Encode an integer as a bit vector with 16 bits.

bit_vec32_from_integer(integer)

Encode an integer as a bit vector with 32 bits.

bit_vec64_from_integer(integer)

Encode an integer as a bit vector with 64 bits.

bit_vec(value)

An Smt2 bit vector.

bit_vec_from_integer(integer, length)

Encode an integer as a bit vector with a given length.

call(name, args)

An Smt2 function call. If some of the arguments of the function call are literals, they are converted into Smt2 values.

from_ex(ast)

Create a Smt2 value from a formula in Elixir code.

from_ex_ast(ast)
integer(value)

An Smt2 integer.

is_smt2(e)
list(value)

An Smt2 list. If some of the arguments of the list literals, they are converted into Smt2 values.

serialize(x)
serialize_multiple(nodes)
string(value)

An Smt2 string.

symbol(value)

An Smt2 symbol.

to_smt2(bool)

Convert a literal into a Smt2 value. If the value is already an Smt2 value it is unchanged.

Types

smt2_like()

@type smt2_like() :: t() | integer() | boolean() | list() | bitstring()

A value which is either an Smt2 value or a literal that can be unambiguously be converted into an Smt2 value.

t()

@type t() ::
  Zee3.Smt2.Int.t()
  | Zee3.Smt2.Real.t()
  | Zee3.Smt2.Symbol.t()
  | Zee3.Smt2.String.t()
  | Zee3.Smt2.BitVec.t()
  | Zee3.Smt2.List.t()

An Smt2 value, which can be serialized and sent to Z3.

Functions

bit_vec16_from_integer(integer)

@spec bit_vec16_from_integer(non_neg_integer()) :: t()

Encode an integer as a bit vector with 16 bits.

bit_vec32_from_integer(integer)

@spec bit_vec32_from_integer(non_neg_integer()) :: t()

Encode an integer as a bit vector with 32 bits.

bit_vec64_from_integer(integer)

@spec bit_vec64_from_integer(non_neg_integer()) :: t()

Encode an integer as a bit vector with 64 bits.

bit_vec(value)

@spec bit_vec(bitstring()) :: t()

An Smt2 bit vector.

bit_vec_from_integer(integer, length)

@spec bit_vec_from_integer(non_neg_integer(), pos_integer()) :: t()

Encode an integer as a bit vector with a given length.

call(name, args)

@spec call(binary(), [smt2_like()]) :: t()

An Smt2 function call. If some of the arguments of the function call are literals, they are converted into Smt2 values.

from_ex(ast)

(macro)

Create a Smt2 value from a formula in Elixir code.

The code inside this macro call is converted the following way:

  • The macro calls use Zee3.StdLib before creating the AST, which means elixir functions will be interpreted as if they were in a Zee3.program/2 macro body.
  • Elixir variables (a, b, ...) are converted into symbols

Examples

iex(1)> require Zee3.Smt2, as: Smt2
Zee3.Smt2

iex(2)> Smt2.from_ex(a)
#Zee3.Smt2.Symbol<a>

iex(3)> Smt2.from_ex(a + b)
#Zee3.Smt2.List<(+ a b)>

iex(4)> Smt2.from_ex(x or y or z)
#Zee3.Smt2.List<(or x y z)>

iex(5)> Smt2.from_ex(x <- a and b and c)
#Zee3.Smt2.List<(=> (and a b c) x)>

from_ex_ast(ast)

integer(value)

@spec integer(integer()) :: t()

An Smt2 integer.

is_smt2(e)

(macro)

list(value)

@spec list([smt2_like()]) :: t()

An Smt2 list. If some of the arguments of the list literals, they are converted into Smt2 values.

serialize(x)

serialize_multiple(nodes)

string(value)

@spec string(binary()) :: t()

An Smt2 string.

symbol(value)

@spec symbol(binary()) :: t()

An Smt2 symbol.

to_smt2(bool)

@spec to_smt2(smt2_like()) :: t()

Convert a literal into a Smt2 value. If the value is already an Smt2 value it is unchanged.