| clausify_prepare | dnf | miniscope | skolemize |
| cnf | formula_copy_share | miniscope_formula | unique_quantified_vars |
| cnf_max_clauses | formula_ident_share | remove_universal_quantifiers |
Formula clausify_prepare(Formula f);This routine gets a formula all ready for translation into clauses. The sequence of transformations is
Formula cnf(Formula f);
int cnf_max_clauses(Formula f);Given an NNF formula, return the maximum number of clauses that it can produce. (The maximum happens if no simplification occurs.)
Formula dnf(Formula f);
Formula formula_copy_share(Formula f);This function returns a copy of the given formula. All subformulas, including the atoms, are copied.
BOOL formula_ident_share(Formula f, Formula g);This Boolean function checks if two formulas are identical. The routine term_ident() checks identity of atoms.
The test is for strict identity---it does not consider renamability of bound variables, permutability of AND or OR, or symmetry of IFF or equality.
Formula miniscope(Formula f);
Formula miniscope_formula(Formula f, unsigned mega_fid_call_limit);
Formula remove_universal_quantifiers(Formula f);For each universally quantified variable in the given formula,
Formula skolemize(Formula f);This routine Skolemizes an NNF formula. The quantified variables need not be named in any particular way. If there are universally quantified variables with the same name, one in the scope of another, the inner variable will be renamed. (Existential nodes are removed.)
Formula unique_quantified_vars(Formula f);Rename quantified variables, if necessary, so that each is unique. This works for any formula.
If you wish to rename a quantified variable only if it occurs in the scope of of a quantified variable with the same name, you can use the routine eliminate_rebinding() instead.
(This could be a void routine, because none of the formula nodes is changed.)