Struct CompletedModel 

pub struct CompletedModel {
    pub assignments: FxHashMap<TermId, TermId>,
    pub function_interps: FxHashMap<Spur, FunctionInterpretation>,
    pub universes: FxHashMap<SortId, Vec<TermId>>,
    pub defaults: FxHashMap<SortId, TermId>,
    pub generation: u32,
}

A completed model that assigns values to all relevant terms

Fields

assignments: FxHashMap<TermId, TermId>

Term assignments (term -> value)

function_interps: FxHashMap<Spur, FunctionInterpretation>

Function interpretations

universes: FxHashMap<SortId, Vec<TermId>>

Universes for uninterpreted sorts (sort -> finite set of values)

defaults: FxHashMap<SortId, TermId>

Default values for each sort

generation: u32

Generation number

Implementations

impl CompletedModel

pub fn new() -> Self

Create a new empty completed model

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

Get the value of a term in this model

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

Set the value of a term

pub fn universe(&self, sort: SortId) -> Option<&[TermId]>

Get the universe for a sort

pub fn add_to_universe(&mut self, sort: SortId, value: TermId)

Add a value to a sort’s universe

pub fn default_value(&self, sort: SortId) -> Option<TermId>

Get the default value for a sort

pub fn set_default(&mut self, sort: SortId, value: TermId)

Set the default value for a sort

pub fn has_uninterpreted_sort(&self, sort: SortId) -> bool

Check if a sort has an uninterpreted universe

Trait Implementations

impl Clone for CompletedModel

fn clone(&self) -> CompletedModel

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CompletedModel

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

Formats the value using the given formatter.

impl Default for CompletedModel

fn default() -> Self

Returns the “default value” for a type.