Module expression_encoding 

Encoding of expressions into SMTExpr

This module provides traits and types to encode boolean or integer expressions into SMT expressions. The encoding is done using the easy-smt crate, therefore the expressions are encoded into SExpr types.

Modules

config_ctx

This module defines the ConfigContext type which declares all SMT variables required to represent a configuration inside an SMT encoding

ctx_mgr

Manager for configurations that build a path

step_ctx

Module for encoding possible paths between configurations in a threshold automaton

ta_encoding

Helper functions to encode expression of a threshold automaton into SMT constraints

Structs

StaticSMTContext

A simple static context for encoding expressions related to threshold automata into SMT constraints and checking satisfiability

Enums

SMTSolverError

Error occurring in the interaction with the SMT solver

Traits

DeclaresVariable

Trait for types that have associated SMT variables

EncodeToSMT

Trait defining the encoding of type T into an SSMTExpr given a context

GetAssignment

Trait that allows to extract the assignment of a variable from the solution found by the SMT solver

SMTVariableContext

Trait of a context that provides mapping from type declaring SMT variables T to associated SMT expression