Struct Model 

pub struct Model { /* private fields */ }

A model (assignment to variables)

Implementations

impl Model

pub fn new() -> Self

Create a new empty model

pub fn get(&self, term: TermId) -> Option<TermId>

Get the value of a term in the model

pub fn set(&mut self, term: TermId, value: TermId)

Set a value in the model

pub fn minimize(&self, essential_vars: &[TermId]) -> Model

Minimize the model by removing redundant assignments Returns a new minimized model containing only essential assignments

pub fn size(&self) -> usize

Get the number of assignments in the model

pub fn assignments(&self) -> &FxHashMap<TermId, TermId>

Get the assignments map (for MBQI integration)

pub fn eval(&self, term: TermId, manager: &mut TermManager) -> TermId

Evaluate a term in this model Returns the simplified/evaluated term

impl Model

pub fn pretty_print(&self, manager: &TermManager) -> String

Pretty print the model in SMT-LIB2 format

Trait Implementations

impl Clone for Model

fn clone(&self) -> Model

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Model

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

Formats the value using the given formatter.

impl Default for Model

fn default() -> Self

Returns the “default value” for a type.