Module rsmt2::print

Traits your types must implement so that rsmt2 can use them.

Most of the ...2Smt traits take some notion of information. This lets you change how printing behaves by passing some print-time info to commands like Solver::assert.

Technical note: this can be useful to avoid duplicating expressions, for instance if you are doing k-induction and don’t want to actually build an expression each time you want to assert the transition relation with variables distinct from previous ones. Instead, you can just pass the k as print-info and print variables differently based on that.

Re-exports

pub use crate::errors::*;

pub use crate::prelude::*;

Structs

NamedExpr

Wraps an expression and a symbol. Symbol is understood as the name of the expression.

Traits

AdtDecl

Gathers data for an ADT declaration.

AdtVariant

Stores data for a variant of an ADT.

AdtVariantField

Contains data for a field of a variant of an ADT.

Expr2Smt

An expression printable in the SMT-LIB 2 standard given some info.

FunDef

Function definition data.

Sort2Smt

A sort printable in the SMT-LIB 2 standard.

Sym2Smt

A symbol printable in the SMT-LIB 2 standard given some info.

SymAndSort

A symbol and a sort, implemented by by symbol/sort pairs.

Functions

write_str

Writes a string.

Type Definitions

Model

Type of a model.