Struct ModelCompleter 

pub struct ModelCompleter { /* private fields */ }

Model completer that takes partial models and makes them complete

Implementations

impl ModelCompleter

pub fn new() -> Self

Create a new model completer

pub fn complete( &mut self, partial_model: &FxHashMap<TermId, TermId>, quantifiers: &[QuantifiedFormula], manager: &mut TermManager, ) -> Result<CompletedModel, CompletionError>

Complete a partial model using the Ge & de Moura (2009) approach.

Steps:

1. Start from the partial SAT+theory model
2. Extract function interpretations from Apply terms in the model
3. Try to solve macro quantifiers (forall x. f(x) = body)
4. Fix incomplete function interpretations (add else values)
5. Handle uninterpreted sorts (create finite universes)
6. Collect universes for all sorts from ground terms in model
7. Set default values for every sort
8. Ensure every function has a complete interpretation

pub fn stats(&self) -> &CompletionStats

Get completion statistics

Trait Implementations

impl Debug for ModelCompleter

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

Formats the value using the given formatter.

impl Default for ModelCompleter

fn default() -> Self

Returns the “default value” for a type.