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 Definitions

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