Ipasir-formula
Tools for constructing the ipasir formula.
We provide several helper functions for constructing formulas:
- ipasir-add-*ary add a fixed-length clause to the formula
- ipasir-add-list adds a clause from a list to the formula
- ipasir-set-* add clauses restricting the literal out to be
assigned the given logical function of the other input literals
These all have a guard saying that the current new-clause of the ipasir
stobj must be empty, and they preserve this property unconditionally.
Subtopics
- Ipasir-set-mux
- Add clauses restricting out to be (if test then else).
- Ipasir-cancel-new-clause
- Identity function in execution; in the logic, ensures that the new-clause
field of the ipasir is empty, which it must be by the guard.
- Ipasir-cancel-assumption
- Identity function in execution; in the logic, ensures that the assumption
field of the ipasir is empty, which it must be by the guard.
- Ipasir-set-xor
- Add clauses restricting out to be the XOR of in1 and in2.
- Ipasir-set-and
- Add clauses restricting out to be the AND of in1 and in2.
- Ipasir-set-iff
- Add clauses restricting out to be the IFF of in1 and in2.
- Ipasir-add-binary
- Add a binary clause to the formula
- Ipasir-add-4ary
- Add a 4-literal clause to the formula
- Ipasir-set-or
- Add clauses restricting out to be the OR of in1 and in2.
- Ipasir-add-ternary
- Add a ternary clause to the formula
- Ipasir-set-buf
- Add clauses restricting out to have the same value as in.
- Ipasir-add-unary
- Add a unary clause to the formula, permanently restricting the given literal to be true.
- Ipasir-add-clauses
- Add a list of clauses to the formula
- Ipasir-add-list
- Add a clause (given as a list of literals) to the formula
- Ipasir-add-clauses-ordered
- Add a list of clauses to the formula
- Ipasir-add-list-ordered
- Add a clause (given as a list of literals) to the formula
- Ipasir-add-empty
- Add an empty clause. Likely useless because the solver is then unsat forever.
