Skip to main content

ConfigFromSMT

taco_smt_encoder::expression_encoding::config_ctx

Trait ConfigFromSMT 

Source 
pub trait ConfigFromSMT:
    SMTVariableContext<Parameter>
    + SMTVariableContext<Location>
    + SMTVariableContext<Variable> {
    // Provided method
    fn get_assigned_configuration(
        &self,
        solver: &mut SMTSolver,
        res: SMTSolution,
    ) -> Result<Configuration, SMTSolverError> { ... }
}
Expand description

Trait for Context

Provided Methods§

Source

fn get_assigned_configuration( &self, solver: &mut SMTSolver, res: SMTSolution, ) -> Result<Configuration, SMTSolverError>

Extract the assignment found by the SMT solver

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§