Zee3.StdLib.Sort (zee3 v0.4.0)

Copy Markdown

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

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

Summary

Functions

array(domain_sort, range_sort)

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

A special sort which serves as an alias for a BitVec of length 32.

float16()
float32()
float64()
float128()
floating_point(eb, sb)

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

int()
real()
reg_lan()
rounding_mode()
string()

Functions

array(domain_sort, range_sort)

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

bit_vec(size)

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

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

bool()

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

entity_id()

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

A special sort which serves as an alias for a BitVec of length 32.

This is meant to be used as the type of entity IDs for the datalog engine, which needs a finite sort, and defaulting to a BitVec of this size seems like a safe option.

float16()

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

float32()

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

float64()

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

float128()

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

floating_point(eb, sb)

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

int()

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

real()

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

reg_lan()

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

rounding_mode()

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

string()

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