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

pub fn eval_apply( &self, func: Spur, evaluated_args: &[TermId], ) -> Option<TermId>

Evaluate a function application f(v1, …, vn) under this model.

First evaluates each argument to its model value, then looks up the function interpretation table. Falls back to else_value or sort default.

pub fn collect_universes_from_model( &mut self, quantifiers: &[QuantifiedFormula], manager: &TermManager, )

Collect the finite universe for each sort appearing in bound variables of the given quantifiers, by scanning ground terms in the current model.

For interpreted sorts (Int, Real, Bool, BV), collects values that actually appear in the model assignments. For uninterpreted sorts, uses existing universe or creates one from model values.

pub fn complete_function_interpretations(&mut self)

Complete all function interpretations by ensuring they have an else_value.

For each function f: S1 x … x Sn -> S that appears in the model:

• If it has explicit entries but no else_value, set else_value to the most common result value (or the sort default).
• If it has no entries at all, set else_value to the sort default.

IMPORTANT: For functions with EXPLICIT entries (finite interpretation from ground assertions), do NOT set else_value. Using “most common result” as else_value is unsound: it makes f(v) evaluate to a wrong value when v is not in the explicit entries, causing MBQI to generate a spurious False evaluation and add an empty SAT clause.

Only set else_value for completely uninterpreted functions (no entries).

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.