Aignet-lit->cnf
Add clauses encoding the fanin cone of literal x of the aignet to the cnf.
- Signature
(aignet-lit->cnf x use-muxes aignet-refcounts sat-lits aignet cnf)
→
(mv new-sat-lits new-cnf)
- Arguments
- x — Literal to encode in the CNF.
Guard (litp x).
- use-muxes — Flag saying whether to recognize muxes and encode them specially.
- aignet-refcounts — Reference counts of aignet nodes.
- sat-lits — Records assignment of SAT variables to aignet nodes.
- aignet — AIG network.
- cnf — Accumulated formula.
- Returns
- new-sat-lits — Updated assignment of SAT variables to aignet nodes.
Type (implies (sat-lits-wfp sat-lits aignet)
(sat-lits-wfp new-sat-lits aignet))
.
- new-cnf — CNF with additional clauses for the fanin cone of x.
Assumes that aignet nodes that have SAT variables assigned in
sat-lits already have their fanin cones encoded, and maintains that invariant.
