Zee3.StdLib.Sort (zee3 v0.5.0)

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

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

Summary

Types

t()

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

A Z3 Bool sort.

entity_id()

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

float16()

A Z3 Float16 (16-bit float) sort.

float32()

A Z3 Float32 (32-bit float) sort.

float64()

A Z3 Float64 (64-bit float) sort.

float128()

A Z3 Float128 (128-bit float) sort.

floating_point(eb, sb)

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

int()

A Z3 Int sort.

real()

A Z3 Real sort.

reg_lan()

A Z3 RegLang (regular language) sort.

rounding_mode()

A Z3 RoundingMode sort.

string()

A Z3 String sort.

Types

t()

@type t() :: Zee3.Smt2.t()

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

A Z3 Bool sort.

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

A Z3 Float16 (16-bit float) sort.

float32()

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

A Z3 Float32 (32-bit float) sort.

float64()

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

A Z3 Float64 (64-bit float) sort.

float128()

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

A Z3 Float128 (128-bit float) sort.

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

A Z3 Int sort.

real()

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

A Z3 Real sort.

reg_lan()

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

A Z3 RegLang (regular language) sort.

rounding_mode()

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

A Z3 RoundingMode sort.

string()

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

A Z3 String sort.