pub trait Solvable: Sized + Clone {
type ModelInstance: Solvable;
// Required methods
fn read_from_model(
&self,
model: &Model,
model_completion: bool,
) -> Option<Self::ModelInstance>;
fn generate_constraint(&self, model: &Self::ModelInstance) -> Bool;
}Expand description
Indicates that a type can be evaluated from a Model and produce a Bool counterexample,
allowing usage in the Solver::solutions iterator pattern.
Specifically, types implementing this trait:
Required Associated Types§
Sourcetype ModelInstance: Solvable
type ModelInstance: Solvable
The type to be extracted from the Solver’s Model.
It will usually just be Self and must be Solvable. This is only an associated
type and not just hard-coded to Self to allow for passing both owned and borrowed
values into Solver::solutions, and to allow implementing this trait for types like
&[T].
Required Methods§
Sourcefn read_from_model(
&self,
model: &Model,
model_completion: bool,
) -> Option<Self::ModelInstance>
fn read_from_model( &self, model: &Model, model_completion: bool, ) -> Option<Self::ModelInstance>
Defines how to derive data derived from the implementing type (usually just a Self)
and a given Model.
Usually this just invokes Model::eval on some Asts and wraps
it up into the proper type.
Sourcefn generate_constraint(&self, model: &Self::ModelInstance) -> Bool
fn generate_constraint(&self, model: &Self::ModelInstance) -> Bool
Produce a Bool assertion ruling out the given model from the valuation of self.
This is used to advance the Solver in Solver::solutions. This is usually just a
disjunction (in case of multiple terms) of “not equal” assertions between self and model.
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.