		Search-engine friendly clone of the ACL2 documentation.

Aignet-ipasir

Using the ipasir interface to run SAT checks on aignet nodes

Aignet-vals-sat-care-masks-rec: Mark a subset of inputs and registers that, when assigned the same values as in the input assignment, produce the same value on the given id.
Aignet-vals-sat-care-masks-lits: Mark a subset of inputs and registers that, when assigned the same values as in the input assignment, produce the same value on the given lits.
Aignet-lits-ipasir-sat-minimize: Check satisfiability of a literal, and minimize the satisfying assignment if satisfiable.
Aignet-lit-ipasir-sat-minimize: Check satisfiability of a literal, and minimize the satisfying assignment if satisfiable.
Aignet-lits-ipasir-sat-check: Performs a single SAT check to determine whether the input AIGNET literal can have the value 1.
Aignet-get-ipasir-ctrex-regvals: Records the register values for a satisfying assignment from an ipasir SAT check.
Aignet-get-ipasir-ctrex-invals: Records the input values for a satisfying assignment from an ipasir SAT check.
Aignet-lit->ipasir: Add clauses encoding the fanin cone of literal x of the aignet to the incremental solver.