Crate taco_smt_encoder 

Interface to interact with SMT solvers

The module mostly reuses the easy-smt crate to interact with the SMT solvers. Easy-smt starts SMT solvers by starting the SMT solver as a subprocess in interactive mode. This crate provides a higher-level interface to encode boolean expressions and utility functions to start and configure popular SMT solvers.

Modules

expression_encoding

Encoding of expressions into SMTExpr

Structs

SMTSolverBuilder

Builder to create new SMTSolver instances

SMTSolverBuilderCfg

Configuration for a SMTSolverBuilder

Enums

GetVersionError 🔒

Error that can occur when constructing a new SMT solver builder

SMTSolution

Result of an SMT query

SMTSolverBuilderError

Error that can occur when creating a new SMTSolverBuilder

SMTSolverOption

Type for options that can be supplied to an SMT solver

Constants

CVC5_ARGS

Option to set CVC5 in quiet mode, use SMT-LIB2 language and force logic to LIA

CVC5_PRG

cvc5 command

Z3_ARGS

Option to set Z3 in SMT-LIB2 language and interactive mode

Z3_PRG

Z3 command

Traits

ProvidesSMTSolverBuilder

Trait for structures provide SMTSolverBuilders

ProvidesSMTSolverBuilderCfg

Trait for types that can provide an SMTSolverBuilderCfg

SMTSolverContext

Trait indicating that the a type holds an SMTSolver

Functions

default_set_lia 🔒

Function to get the default value for the set_lia field

get_smt_solver_version 🔒

Calls solver and attempts to parse the version of the SMT solver that is used

parse_smt_solver_version 🔒

This function attempts to parse the version number from the output of the --version command.

Type Aliases

CompatibilityCheck 🔒

Type for functions that check the compatibility of the SMT solver version

SMTExpr

SMT expression

SMTSolver

Interface to interact with SMT solver