Modules
Boolean expression representation and manipulation for SAT solving.
Behaviour for defining expression rewrite rules.
Rewrite rule that applies absorption laws to simplify expressions.
Rewrite rule that applies boolean annihilator laws.
Rewrite rule that applies associativity optimizations to simplify expressions.
Rewrite rule that applies commutativity laws to normalize expression order.
Rewrite rule that applies complement laws to simplify expressions.
Rewrite rule that applies the consensus theorem to eliminate redundant clauses.
Rewrite rule that applies De Morgan's laws to expressions.
Rewrite rule that applies the distributive law to convert expressions to CNF.
Rewrite rule that applies distributivity-based simplifications to expressions.
Rewrite rule that applies idempotent laws to simplify expressions.
Rewrite rule that applies boolean identity laws to simplify expressions.
Rewrite rule that applies negation laws to simplify expressions.
Rewrite rule that detects common tautology patterns.
Rewrite rule that applies unit resolution to propagate unit clauses.
A module for representing and manipulating satisfiability formulas in Conjunctive Normal Form (CNF).
Tseitin transformation from a boolean Crux.Expression into CNF.
This module provides an interface to a SAT solver.