GetAssignment

taco_smt_encoder::expression_encoding

Trait GetAssignment 

Source 
pub trait GetAssignment<T>: SMTVariableContext<T> + SMTSolverContext
where
    T: DeclaresVariable,
{
    // Provided method
    fn get_assignment(
        &mut self,
        res: SMTSolution,
        var: &T,
    ) -> Result<Option<u64>, SMTSolverError> { ... }
}
Expand description

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

This trait is implemented by contexts allowing to extract the solution found by the SMT solver for a given variable.

Provided Methods§

Source

fn get_assignment( &mut self, res: SMTSolution, var: &T, ) -> Result<Option<u64>, SMTSolverError>

Get the assigned solution of the variable

This function returns the assignment of the variable from the SMT solver. If the query is unsatisfiable, it returns None. If the query is satisfiable, it returns the assigned value.

Returns an error if the connection to the SMT solver broke.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§