Struct MBQISolver 

pub struct MBQISolver { /* private fields */ }

Model-Based Quantifier Instantiation solver

Implementations

impl MBQISolver

pub fn new() -> Self

Create a new MBQI solver

pub fn with_limit(max_total: usize) -> Self

Create with custom instantiation limit

pub fn set_enabled(&mut self, enabled: bool)

Enable or disable MBQI

pub fn is_enabled(&self) -> bool

Check if MBQI is enabled

pub fn clear(&mut self)

Clear all state

pub fn add_quantifier(&mut self, term: TermId, manager: &TermManager)

Add a quantified formula to track

pub fn add_candidate(&mut self, term: TermId, sort: SortId)

Register a candidate term for instantiation

pub fn collect_ground_terms(&mut self, term: TermId, manager: &TermManager)

Collect ground terms from a formula for use as instantiation candidates

pub fn get_candidates(&self, sort: SortId) -> &[TermId]

Get candidates for a given sort

pub fn at_limit(&self) -> bool

Check if we’ve reached the instantiation limit

pub fn check_with_model( &mut self, model: &FxHashMap<TermId, TermId>, manager: &mut TermManager, ) -> MBQIResult

Perform MBQI with the given model

This is the main entry point for MBQI. Given a partial model from the main solver, it tries to find counterexamples to universal quantifiers and generates instantiation lemmas.

pub fn stats(&self) -> MBQIStats

Get statistics about MBQI

Trait Implementations

impl Debug for MBQISolver

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

Formats the value using the given formatter.

impl Default for MBQISolver

fn default() -> Self

Returns the “default value” for a type.