Module smt

Module smt 

Source

Structs§

IntTheoryIter
An iterator over the variants of IntTheory
MatrixTheoryIter
An iterator over the variants of MatrixTheory
Smt
A SolverAdaptor for interacting with SMT solvers, specifically Z3.
TheoryConfig
A collection of theories to use for encoding various CO AST constructs.

Enums§

IntTheory
The theory to use when encoding CO integers through the SMT solver adaptor.
MatrixTheory
The theory to use when encoding CO integers through the SMT solver adaptor.