### 2 unstable releases

0.2.0 | Feb 23, 2023 |
---|---|

0.1.0 | Sep 16, 2022 |

#**40** in Science

**Apache-2.0**

250KB

6K
SLoC

# amzn-smt-ir

is a Rust library for working with SMT-LIB formulas.`amzn-smt-ir`

## Representation

### Logics

SMT-LIB logics are represented by the

trait, which encapsulates the type of
operations in the logic (more on this later) as well as whether quantifiers and uninterpreted
functions are allowed (corresponding to the `aws_smt_ir ::`Logic

`QF`

(**Q**uantifier-

**F**ree) and

`UF`

(including
**U**ninterpreted

**F**unctions) prefixes in SMT-LIB logic names.) Logics that wish to leave out non-

`Core`

operations, quantifiers, or uninterpreted functions can specify `aws_smt_ir``::`Void

as
the corresponding associated type -- since `Void`

is uninhabitable, it will be impossible at the
type level for terms in the resulting logic to contain the corresponding components.### Operations

*Note:* This library calls SMT functions "operations" to avoid confusion with Rust's

traits.`Fn`

SMT-LIB theory functions are represented as

s. For instance, a simplified version of SMT-LIB
`enum`

might look like the following:`Core`

`enum` `CoreOp`<Term> `{`
Not`(`Term`)``,`
And`(``Vec``<`Term`>``)``,`
Ite`(`Term`,` Term`,` Term`)``,`
`}`

This makes it possible to encode the distinctions between different functions at the type level e.g.
encoding that

is a unary function, `not`

is ternary, and `ite`

may take any number of
arguments (since it is annotated with `and`

).`:`left`-`assoc

*Note:* Indexed functions are defined as containing an array of indices as their first tuple field
e.g.

for the bit-vector `Extract ([IIndex; 2], Term)`

`extract`

function.Pre-defined

s and their corresponding operation types are defined in the `Logic`

module. Users can also define custom `aws_smt_ir ::`logic

`Logic`

s and operations using the provided derive macros to
implement the expected traits (see the "Derives" section).### Terms

Terms are represented by

, which represents an SMT term in logic `aws_smt_ir ::`Term

`<`L`:`Logic`>``L`

:`enum` `Term`<T: Logic> `{`
`///` A constant value.
Constant`(`IConst`)``,`
`///` A variable representing a value.
Variable`(``IVar``<``T``::`Var`>``)``,`
`///` An operation in SMT-LIB's Core theory.
CoreOp`(``ICoreOp``<`T`>``)``,`
`///` A non-Core operation.
OtherOp`(``IOp``<`T`>``)``,`
`///` An uninterpreted function.
`UF``(``IUF``<`T`>``)``,`
`///` Simultaneous let-binding e.g. `(let ((x true) (y false)) (and x y))`
Let`(``ILet``<`T`>``)``,`
`///` SMT-LIB `match` expression -- not yet supported
Match`(``IMatch``<`T`>``)``,`
`///` Quantified term.
Quantifier`(``IQuantifier``<`T`>``)``,`
`}`

*Note:* Because

is implicitly included in every logic, `Core`

s may be present in any type
of `CoreOp`

.`Term`

The

prefixes of type names signal that the types are interned to prevent duplication (also
called hash-consed). `I`

-prefixed types are
essentially pointers to a unique copy of the data they correspond to stored in a lookup table with
hashes as keys. When a value of one of these types is instantiated, the corresponding table is first
checked to see if it contains the value; if it does, a pointer to the existing copy is returned; if
not, the value is stored in the table and a pointer to the new copy is returned. `I`

-prefixed types
implement most of Rust's standard traits by delegating to the inner value, although `I`

and
`PartialEq`

are implemented with pointer equality (equivalent because there exists a unique copy of each
value).`Eq`

## Traversals

The library provides two patterns for traversing IR nodes.

### Computing

The

family of traits (`Visit`

, `Visitor`

, and `Visit`

) provide a visitor pattern for
traversing IR nodes and building up some result (stored in a `SuperVisit`

). See the traits' respective
docs for more details.`Visitor`

### Transforming

The

family of traits (`Fold`

, `Folder`

, and `Fold`

) provide a pattern for transforming
IR nodes into other IR nodes. See the traits' respective docs for more details.`SuperFold`

## Derives

The library provides three derive macros for generating trait implementations expected of types used
as operations (i.e. the

of an `L ::`Op

`L``:` Logic

):

: implements the`Operation`

trait, which determines how an operation is parsed from a function symbol and list of arguments, the`Operation`

trait, which allows for constructing an iterator of function arguments (used through the`Iterate`

trait), as well as`Args`

,`Debug`

, and`Display`

implementations for converting the type to`From`

and`IOp`

.`Term`

: implements the`Visit`

trait for performing the standard recursive traversal of an operation enum.`SuperVisit`

: implements the`Fold`

trait for performing the standard recursive transformation of an operation enum.`SuperFold`

#### Dependencies

~9.5MB

~150K SLoC