Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Ipasir
Ipasir$a
Building-an-ipasir-solver-library
Ipasir-formula
Ipasir-bump-activity-vars$a
Ipasir-set$a
Ipasir-bump-activity-vars$c
Ipasir-get$a
Ipasir-set-limit$c
Ipasir-failed$c
Ipasir-assume$c
Ipasir-add-lit$c
Ipasir-val$c
Ipasir-set$c
With-local-ipasir
Ipasir-solve$c
Ipasir-init$c
Ipasir-finalize-clause$c
Ipasir-some-history$c
Ipasir-solved-assumption$c
Ipasir-release$c
Ipasir-reinit$c
Ipasir-input$c
Ipasir-get$c
Ipasir-get-status$c
Ipasir-get-curr-stats$c
Ipasir-get-assumption$c
Ipasir-empty-new-clause$c
Ipasir-callback-count$c
Ipasir-val
Ipasir-solve
Ipasir-set-limit
Ipasir-reinit
Ipasir-failed
Ipasir-callback-count
Ipasir-release
Ipasir-input
Ipasir-init
Ipasir-finalize-clause
Ipasir-assume
Ipasir-add-lit
Aignet
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
Ipasir
Ipasir-failed
Check whether a literal is in the current unsatisfiable assumption core.
See
ipasir
for details.