Struct Instantiation 

pub struct Instantiation {
    pub quantifier: TermId,
    pub substitution: FxHashMap<Spur, TermId>,
    pub result: TermId,
    pub generation: u32,
    pub reason: InstantiationReason,
    pub cost: f64,
}

An instantiation of a quantified formula

Fields

quantifier: TermId

The quantifier that was instantiated

substitution: FxHashMap<Spur, TermId>

The substitution used (variable name -> term)

result: TermId

The resulting ground term (body with substitution applied)

generation: u32

Generation at which this instantiation was created

reason: InstantiationReason

Reason for instantiation (for proof generation)

cost: f64

Cost/weight of this instantiation

Implementations

impl Instantiation

pub fn new( quantifier: TermId, substitution: FxHashMap<Spur, TermId>, result: TermId, generation: u32, ) -> Self

Create a new instantiation

pub fn with_reason( quantifier: TermId, substitution: FxHashMap<Spur, TermId>, result: TermId, generation: u32, reason: InstantiationReason, ) -> Self

Create with reason

pub fn binding_key(&self) -> Vec<(Spur, TermId)>

Get the binding as a sorted vector for hashing

Trait Implementations

impl Clone for Instantiation

fn clone(&self) -> Instantiation

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Instantiation

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

Formats the value using the given formatter.