pub trait WitnessIterator {
// Required method
fn witness(&mut self, clause: &[i32], witness: &[i32], id: u64) -> bool;
}Expand description
Allows to traverse all clauses on the extension stack together with their witness cubes. If the solver is inconsistent, i.e., an empty clause is found and the formula is unsatisfiable, then nothing is traversed.
The clauses traversed in ‘traverse_clauses’ together with the clauses on
the extension stack are logically equivalent to the original clauses.
See our SAT’19 paper for more details.
The witness literals can be used to extend and fix an assignment on the remaining clauses to satisfy the clauses on the extension stack too.
All derived units of non-frozen variables are included too.
If ‘witness’ returns false traversal aborts early.