Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Ipasir
Aignet
Base-api
Aignet-construction
Representation
Aignet-copy-init
Aignet-simplify-marked-with-tracking
Aignet-cnf
Aignet-lit->cnf
Aignet-ipasir
Aignet-vals-sat-care-masks-rec
Aignet-vals-sat-care-masks-lits
Aignet-lits-ipasir-sat-minimize
Aignet-lit-ipasir-sat-minimize
Aignet-lits-ipasir-sat-check
Aignet-get-ipasir-ctrex-regvals
Aignet-get-ipasir-ctrex-invals
Aignet-lit->ipasir
Aignet-simplify-with-tracking
Aignet-complete-copy
Aignet-eval
Semantics
Aignet-transforms
Aignet-simplify-marked
Aignet-read-aiger
Aignet-write-aiger
Aignet-abc-interface
Utilities
Aig
Satlink
Truth
Ubdds
Bdd
Faig
Bed
4v
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Aignet-cnf
Aignet-ipasir
Using the
ipasir
interface to run SAT checks on aignet nodes
Subtopics
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.