Zee3.StdLib.Sort (zee3 v0.3.0)

Standard SMT-LIB2 Sorts (Types) for the Zee3 DSL.

All functions return an AST node representing an S-Expression.

Summary

Creates an Array sort mapping a domain to a range. Generates SMT: (Array domain_sort range_sort)

bit_vec(size)

Creates a BitVector sort of a specific size. Generates SMT: (_ BitVec size)

bool()

float16()

float32()

float64()

float128()

Creates a custom FloatingPoint sort. eb: exponent bits, sb: significand bits. Generates SMT: (_ FloatingPoint eb sb)

int()

real()

reg_lan()

rounding_mode()

string()

Creates an Array sort mapping a domain to a range. Generates SMT: (Array domain_sort range_sort)

@spec bit_vec(integer() | Zee3.Smt2.t()) :: Zee3.Smt2.t()

Creates a BitVector sort of a specific size. Generates SMT: (_ BitVec size)

@spec bool() :: Zee3.Smt2.t()

@spec float16() :: Zee3.Smt2.t()

@spec float32() :: Zee3.Smt2.t()

@spec float64() :: Zee3.Smt2.t()

@spec float128() :: Zee3.Smt2.t()

@spec floating_point(integer() | Zee3.Smt2.t(), integer() | Zee3.Smt2.t()) ::
  Zee3.Smt2.t()

@spec floating_point(Zee3.Smt2.t(), Zee3.Smt2.t()) :: Zee3.Smt2.t()

Creates a custom FloatingPoint sort. eb: exponent bits, sb: significand bits. Generates SMT: (_ FloatingPoint eb sb)

@spec int() :: Zee3.Smt2.t()

@spec real() :: Zee3.Smt2.t()

@spec reg_lan() :: Zee3.Smt2.t()

@spec rounding_mode() :: Zee3.Smt2.t()

@spec string() :: Zee3.Smt2.t()