Struct Model

pub struct Model<'ctx> { /* private fields */ }

Model for the constraints inserted into the logical context.

Implementations

impl<'ctx> Model<'ctx>

pub fn of_solver(slv: &Solver<'ctx>) -> Option<Model<'ctx>>

pub fn of_optimize(opt: &Optimize<'ctx>) -> Option<Model<'ctx>>

pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Model<'dest_ctx>

Translate model to context dest

pub fn get_const_interp<T: Ast<'ctx>>(&self, ast: &T) -> Option<T>

Returns the interpretation of the given ast in the Model Returns None if there is no interpretation in the Model

pub fn get_func_interp(&self, f: &FuncDecl<'_>) -> Option<FuncInterp<'ctx>>

Returns the interpretation of the given f in the Model Returns None if there is no interpretation in the Model

pub fn eval<T>(&self, ast: &T, model_completion: bool) -> Option<T>

where T: Ast<'ctx>,

pub fn iter(&'ctx self) -> ModelIter<'ctx>

Trait Implementations

impl<'ctx> Debug for Model<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Display for Model<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for Model<'ctx>

fn drop(&mut self)

Executes the destructor for this type.

impl<'ctx> IntoIterator for &'ctx Model<'ctx>

type Item = FuncDecl<'ctx>

The type of the elements being iterated over.

type IntoIter = ModelIter<'ctx>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.