Struct QuantifierQueue 

pub struct QuantifierQueue { /* private fields */ }

Priority queue for quantifiers

Implementations

impl QuantifierQueue

pub fn new(heuristic: InstantiationHeuristic) -> Self

Create a new queue

pub fn push( &mut self, quantifier: QuantifiedFormula, model: &CompletedModel, manager: &TermManager, )

Add a quantifier to the queue

pub fn pop(&mut self) -> Option<QuantifiedFormula>

Pop the highest priority quantifier

pub fn is_empty(&self) -> bool

Check if empty

pub fn len(&self) -> usize

Get length

Trait Implementations

impl Debug for QuantifierQueue

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

Formats the value using the given formatter.