Aignet-lit->ipasir
Add clauses encoding the fanin cone of literal x of the aignet to the incremental solver.
- Signature
(aignet-lit->ipasir x use-muxes
aignet-refcounts sat-lits aignet ipasir)
→
(mv new-sat-lits new-ipasir)- 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.
- ipasir — Incremental solver instance containing the 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-ipasir — Incremental solver instance, updated 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.
See ipasir for information on the incremental solver interface.
