pub trait Congruence {
// Required methods
fn name(&self) -> &str;
fn canonicalize(&self, clauses: &CanonClauses) -> (CanonClauses, Twist);
}Expand description
An equivalence relation on cofactors, given by a canonical representative of each class plus the
Twist realizing the merge. To be a sound certificate substrate it must be a congruence:
its twists are literal renamings (bijection + polarity flips), which preserve (un)satisfiability,
so isomorphism-invariance of UNSAT makes the local check sound. Two cofactors are ~-equivalent
iff canonicalize returns the same representative.
Required Methods§
Sourcefn canonicalize(&self, clauses: &CanonClauses) -> (CanonClauses, Twist)
fn canonicalize(&self, clauses: &CanonClauses) -> (CanonClauses, Twist)
The canonical representative of clauses’s class, and the twist mapping clauses onto it
(i.e. apply_twist(clauses, twist) == representative).