Struct Proof 

pub struct Proof<'a> {
    pub hypothesis: Hypothesis,
    pub heap: QueryHeap<'a>,
    /* private fields */
}

The proof search engine.

Maintains a goal stack and iteratively resolves goals against the predicate table and the current hypothesis. Call Proof::prove repeatedly to enumerate solutions via backtracking.

Fields

hypothesis: Hypothesis

heap: QueryHeap<'a>

Implementations

impl<'a> Proof<'a>

pub fn new(heap: QueryHeap<'a>, goals: &[usize]) -> Self

pub fn with_hypothesis( heap: QueryHeap<'a>, goals: &[usize], hypothesis: Hypothesis, ) -> Self

Create a new proof with an existing hypothesis (for negation-as-failure checks)

pub fn prove( &mut self, predicate_table: &PredicateTable, config: Config, ) -> bool