Struct lrs::Clause

pub struct Clause {
    pub terms: Vec<Term>,
}

Represents a logical equation in conjunctive normal form Consists of a finite collection of Terms of symbols chained via OR that are chained in the clause with AND operations.

Fields

terms: Vec<Term>

Methods

impl Clause

fn insert(&mut self, term: Term)

Insert a term naively into an clause

fn reduce(&mut self) -> Operation

Run a single reduce step and return the exact reduce operation