Struct MacroSolver 

pub struct MacroSolver { /* private fields */ }

Macro solver that identifies quantifiers that can be solved as macros

A quantifier can be solved as a macro if it has the form: ∀x. f(x) = body(x) where f is an uninterpreted function and body doesn’t contain f

Implementations

impl MacroSolver

pub fn new() -> Self

Create a new macro solver

pub fn solve_macros( &mut self, quantifiers: &[QuantifiedFormula], manager: &mut TermManager, ) -> Result<FxHashMap<Spur, FunctionInterpretation>, CompletionError>

Try to solve quantifiers as macros

pub fn stats(&self) -> &MacroStats

Get statistics

Trait Implementations

impl Debug for MacroSolver

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

Formats the value using the given formatter.

impl Default for MacroSolver

fn default() -> Self

Returns the “default value” for a type.