8.12
4.1 cnf
| (require karp/lib/cnf) | package: Karp |
Boolean Formulas in Conjunctive Normal Form
type-descriptor / syntax
(cnf #:arity arity)
(cnf clause ...)
clause = (literal-first literal-next ...) literal-first = literal literal-next = ∨ literal literal = variable | (¬ variable)
arity : natural?
variable : symbol?
type-descriptor:
procedure: create a cnf with clauses.
NOT available inside verifier definitions
value-descriptor / procedure
(variables-of a-cnf)
(variables-of c)
a-cnf : value-descriptor? CNF?
c : cnf? clause?
Get the set of variables of the CNF or clause c when used outside
decision-problem.
procedure
(literals-of c) → (setof literal?)
c : clause?
Get the set of literals of clause c.
procedure
(neg l) → literal?
l : literal? or symbol?
Get the negation of a literal l. When l is a variable
(i.e., symbol), a negative literal with underlying variable l is
produced.
procedure
(underlying-var l) → symbol?
l : literal?
Get the underlying variable of literal l.
procedure
(positive-literal? l) → boolean?
l : literal?
Test if literal l is a positive literal.
procedure
(negative-literal? l) → boolean?
l : literal?
Test if literal l is a negative literal.
procedure
(literal-neg-of? l1 l2) → boolean?
l1 : literal? l2 : literal?
Test if literal l1 is the negation of l2.
procedure
(same-variable? l1 l2) → boolean?
l1 : literal? l2 : literal?
Test if literals l1 and l2 have the same variable.
procedure
(clauses-of c) → (setof clauses)
c : cnf?
Get the set of all clauses of CNF c.