Conjunction.
Abstract type for logical gates used when constructing a CNF formula.
Equivalence.
Implication.
If-then-else.
Negation.
Disjunction.
Equivalence.
Represents an input gate of the circuit.
Asserts that a certain literal must be true.
Asserts that a collection of literals are all equal, implemented using a loop of implications.
Asserts that a collection of literals are all equal, implemented using a loop of implications.
l1 = l2 = ... = ln := l1 -> l2 & ... & ln -> l1
list of literals of size >= 2
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the assertion on and off
The optional switching literal
An itetator on the gate variables of the formula.
Declares a literal as an output of the circuit.
Declares a literal as an output of the circuit.
Encodes the equation
Encodes the equation
x = And(a1, ... ,an)
as clauses:
( x, ~a1, ... , ~an) ( ~x, a1 ) ... ( ~x, an )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Iff(p, q)
as clauses:
( ~x, ~p, q ) ( ~x, p, ~q ) ( x, ~p, ~q ) ( x, p, q )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Implies(p, q)
as clauses:
(~x, ~p, q ) ( x, p ) ( x, ~q )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Ite(s, t, f)
as clauses:
( x, ~s, ~t ) ( ~x, ~s, t ) ( x, s, ~f ) ( ~x, s, f ) ( x, ~t, ~f ) ( ~x, f, t )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Not(p)
as clauses:
(~x, ~p) (x, p)
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Or(a1, ... , an)
as clauses:
( ~x, a1, ... , an) ( x, ~a1) ... ( x, ~an)
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Xor(p, q)
as clauses:
( ~x, p, q ) ( ~x, ~p, ~q ) ( x, p, ~q ) ( x, ~p, q )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
A gate Map indexed by literals.
An itetator on gate literal definitions.
An itetator on the gate variables of the formula.
True iff the literal is not a gate.
True iff the literal or its complement is defined as a gate.
True iff the literal was previously declared as a circuit input.
the number of gates of the formula.
The number of gates of the formula.
the number of gates of the formula.
the number of gates of the formula.
An iterator on the gate variables of the formula.
An interface for building circuit-like formulas on top of CNF formulas.