Zee3.Smt2 (zee3 v0.4.0)

Copy Markdown

Summary

Types

smt2_like()
t()

Functions

bit_vec16_from_integer(integer)
bit_vec32_from_integer(integer)
bit_vec64_from_integer(integer)
bit_vec(value)
bit_vec_from_integer(integer, length)
call(name, args)
integer(value)
is_smt2(e)
list(value)
serialize(x)
serialize_multiple(nodes)
string(value)
symbol(value)
to_smt2(bool)

Types

smt2_like()

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

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()

Functions

bit_vec16_from_integer(integer)

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

bit_vec32_from_integer(integer)

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

bit_vec64_from_integer(integer)

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

bit_vec(value)

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

bit_vec_from_integer(integer, length)

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

call(name, args)

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

integer(value)

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

is_smt2(e)

(macro)

list(value)

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

serialize(x)

serialize_multiple(nodes)

string(value)

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

symbol(value)

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

to_smt2(bool)

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