Trait EncodeToSMT 

pub trait EncodeToSMT<T, C> {
    // Required method
    fn encode_to_smt_with_ctx(
        &self,
        solver: &SMTSolver,
        ctx: &C,
    ) -> Result<SMTExpr, SMTSolverError>;
}

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

If this trait is implemented for a type T, expressions of type T can be encoded into an SMT expression, using the given SMT solver and context of type C. This trait does not restrict the type of the context.

Required Methods

fn encode_to_smt_with_ctx( &self, solver: &SMTSolver, ctx: &C, ) -> Result<SMTExpr, SMTSolverError>

Encode the type into an SMT expression

Encode the expression of type T into an SMT expression using the given SMT solver and context of type C.

Implementations on Foreign Types

impl<T, U> EncodeToSMT<BooleanExpression<T>, U> for BooleanExpression<T>

where U: SMTVariableContext<T> + SMTVariableContext<Parameter>, T: DeclaresVariable + Atomic,

fn encode_to_smt_with_ctx( &self, solver: &SMTSolver, ctx: &U, ) -> Result<SExpr, SMTSolverError>

impl<T, U> EncodeToSMT<IntegerExpression<T>, U> for IntegerExpression<T>

where U: SMTVariableContext<T> + SMTVariableContext<Parameter>, T: DeclaresVariable + Atomic,

fn encode_to_smt_with_ctx( &self, solver: &SMTSolver, ctx: &U, ) -> Result<SExpr, SMTSolverError>

Implementors