Crate aws_smt_ir 

Intermediate representation for SMT-LIB formulas.

Re-exports

pub use smt2parser::concrete::Command as Smt2ParserCommand;

pub use smt2parser::concrete::SyntaxBuilder;

pub use smt2parser::CommandStream;

pub use logic::Logic;

pub use term::*;

pub use types::*;

Modules

ackermann

cnf

eliminate

fold

Traits for transforming Terms into other terms.

logic

Representations of SMT-LIB logics.

model

smt2parser

This crate provides a generic parser for SMT2 commands, as specified by the SMT-LIB-2 standard.

term

Intermediate representation for SMT-LIB terms.

types

visit

Traits for visiting Terms.

Macros

args

Creates a SmallVec containing the arguments.

try_break

Unwraps a ControlFlow or propagates its Break value. This replaces the Try implementation that would be used with std::ops::ControlFlow.

Structs

Ctx

Ctx tracks the global context of a script (e.g. defined sorts and functions), along with local context inside of terms (e.g. variables bound by let, forall, exists).

FreshVarError

Script

Script represents an entire SMT-LIB script i.e. sequence of commands.

Enums

ParseError

Functions

chained

Applies each to each adjacent pair of arguments in args, corresponding to the :chainable SMT-LIB attribute.

pairwise

Applies each to each distinct pair of arguments in args, corresponding to the :pairwise SMT-LIB attribute.

parse_commands

Parses an SMT-LIB file, returning an iterator of parsed SMT-LIB commands.

try_chained

Applies a fallible function to each adjacent pair of arguments in args, corresponding to the :chainable SMT-LIB attribute.

try_pairwise

Applies a fallible function to each distinct pair of arguments in args, corresponding to the :pairwise SMT-LIB attribute.

Type Aliases

Void

An uninhabited type, useful for defining theories that contain no operations beyond those in SMT-LIB’s Core theory.