Struct Model 

pub struct Model { /* private fields */ }

Model for the constraints inserted into the logical context.

Implementations

impl Model

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

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

pub fn get_const_interp<T: Ast>(&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>

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,

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

Trait Implementations

impl Debug for Model

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

Formats the value using the given formatter.

impl Display for Model

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

Formats the value using the given formatter.

impl Drop for Model

fn drop(&mut self)

Executes the destructor for this type.

impl<'a> IntoIterator for &'a Model

type Item = FuncDecl

The type of the elements being iterated over.

type IntoIter = ModelIter<'a>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl Translate for Model

fn translate(&self, dest: &Context) -> Model