| clause_to_formula | formula_to_clause | formula_to_literal | |
| clausify_formula | formula_to_clauses | formula_to_literals |
Formula clause_to_formula(Topform c);Return an entirely new formula.
Plist clausify_formula(Formula f);This routine translates a Formula f into a Plist of clauses. The translation includes Skolemization, so the result should be unsatisfiable iff f is unsatisfiable. The variables in each clause are renumbered. If there are more than MAX_VARS variables in a clause, a fatal error occurs.
Formula f is not changed.
Topform formula_to_clause(Formula f);This routine takes a Formula f and returns a Topform representation. If f is not an atom, literal, or disjunction of literals, the returned clause will be NULL or not well formed.
The returned clause is an entirely new copy, and the given formula is not changed.
Plist formula_to_clauses(Formula f);This routine takes a Formula f and returns a Plist of clauses representation. If f is not an atom, literal, or disjunction of literals, or a conjunction of those things, the clauses in the returned list may be NULL or not well formed.
The returned clauses are entirely new copies, and the given formula is not changed.
Literals formula_to_literal(Formula f);This routine takes a Formula f and returns a Literals representation. If the formula is not an ATOM_FORM or the negation of an ATOM_FORM, NULL is returned.
The returned literal is an entirely new copy, and the given formula is not changed.
Literals formula_to_literals(Formula f);