		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Ipasir$a

Datatype for the logical model of an ipasir incremental SAT solver.

This is a product type introduced by fty::defprod.

Fields

formula — satlink::lit-list-list: Permanent formula
assumption — satlink::lit-list: Current assumption, if status is :input, or assumption before latest solve, if status is :unsat.
new-clause — satlink::lit-list: Partial clause to add to the formula
status — ipasir-status-p: Current status, determining which operations are allowed
solution — satlink::lit-list: Satisfying assignment from solver, when status = :sat, or subset of assumptions sufficient to prove unsat, when status = :unsat
solved-assumption — satlink::lit-list: Assumption that was proved unsatisfiable, if status is :unsat.
callback-count — natp: Number of times a callback function has been called during solve
history: Collects the history of all operations on this solver, so we can never execute the solver the same way twice

See ipasir.

Subtopics

Ipasir$a-p: Recognizer for ipasir$a structures.
Ipasir$a-fix: Fixing function for ipasir$a structures.
Ipasir-set-limit$a: Logic form of ipasir-set-limit. See ipasir for usage.
Ipasir-add-lit$a: Logic form of ipasir-add-lit. See ipasir for usage.
Ipasir-assume$a: Logic form of ipasir-assume. See ipasir for usage.
Ipasir-init$a: Logic form of ipasir-init. See ipasir for usage.
Make-ipasir$a: Basic constructor macro for ipasir$a structures.
Ipasir-finalize-clause$a: Logic form of ipasir-finalize-clause. See ipasir for usage.
Ipasir-reinit$a: Logic form of ipasir-reinit. See ipasir for usage.
Ipasir-input$a: Logic form of ipasir-input. See ipasir for usage.
Ipasir$a-equiv: Basic equivalence relation for ipasir$a structures.
Ipasir-val$a: Logic form of ipasir-val. See ipasir for usage.
Ipasir-release$a: Logic form of ipasir-release. See ipasir for usage.
Ipasir$a->solved-assumption: Get the solved-assumption field from a ipasir$a.
Ipasir-failed$a: Logic form of ipasir-failed. See ipasir for usage.
Change-ipasir$a: Modifying constructor for ipasir$a structures.
Ipasir$a->new-clause: Get the new-clause field from a ipasir$a.
Ipasir$a->callback-count: Get the callback-count field from a ipasir$a.
Ipasir$a->assumption: Get the assumption field from a ipasir$a.
Ipasir$a->status: Get the status field from a ipasir$a.
Ipasir$a->solution: Get the solution field from a ipasir$a.
Ipasir$a->formula: Get the formula field from a ipasir$a.
Ipasir$a->history: Get the history field from a ipasir$a.
Ipasir-callback-count$a: Logic form of ipasir-callback-count. See ipasir for usage.
Ipasir-solved-assumption$a
Ipasir-some-history$a
Ipasir-get-assumption$a
Ipasir-empty-new-clause$a
Ipasir-get-status$a
Create-ipasir$a
Ipasir-solve$a: Logic form of ipasir-solve. See ipasir for usage.