Formula and(Formula a, Formula b);
BOOL clausal_formula(Formula f);
BOOL closed_formula(Formula f);
Ilist constants_in_formula(Formula f);
Plist copy_plist_of_formulas(Plist formulas);
Formula dual(Formula f);Change a formula into its dual. This is destructive.
BOOL dual_type(int op);
Formula eliminate_rebinding(Formula f);This routine renames quantified variables so that no quantified variable occurs in the scope of a quantified variable with the same name.
If you wish to rename variables so that each quantifer has a unique variable, you can use the routine unique_quantified_vars() instead.
The argument f is "used up" during the procedure.
(This could be a void routine, because none of the formula nodes is changed; I made it return the Formula so that it is consistent with its friends.)
Formula flatten_top(Formula f);
void formula_canon_eq(Formula f);For each equality in the formula, if the right side greater according to "term_compare_ncv", flip the equality.
BOOL formula_contains_attributes(Formula f);Does the formula or any of its subformulas contain attributes?
Formula formula_copy(Formula f);This function returns a copy of the given formula. All subformulas, including the atoms, are copied.
Formula formula_flatten(Formula f);This routine (recursively) flattens all AND and OR subformulas.
Formula formula_get(int arity, Ftype type);
BOOL formula_ident(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.
unsigned formula_megs(void);Return the approximate number of megabytes in use for storage of formulas.
void formula_set_variables(Formula f, int max_vars);This routine traverses a formula and changes the constants that should be variables, into variables. On input, the formula should have no variables. The new variables are numbered 0, 1, 2 ... according the the first occurrence, reading from the left.
A fatal error occurs if there are more than max_vars variables.
The intended is use is for input formulas that are built without regard to variable/constant distinction.
int formula_size(Formula f);How many nodes are in the formula. (Atomic formulae count as 1.)
Term formula_to_term(Formula f);
Formula formulas_to_conjunction(Plist formulas);Given a Plist of formulas, form a conjunction of the members. The formulas are not copied, and the Plist is not freed, so you may wish to call zap_plist after the call to this routine.
Note that the empty conjunction is TRUE.
Formula formulas_to_disjunction(Plist formulas);Given a Plist of formulas, form a disjunction of the members. The formulas are not copied, and the Plist is not freed, so you may wish to call zap_plist after the call to this routine.
Note that the empty disjunction is FALSE.
void fprint_formula(FILE *fp, Formula f);This routine prints a formula to a file. If you wish to have a formula printed without extra parentheses, you can call fprint_formula_term() instead.
void fprint_formula_mem(FILE *fp, BOOL heading);This routine prints (to FILE *fp) memory usage statistics for data types associated with the formula package. The Boolean argument heading tells whether to print a heading on the table.
void free_formula(Formula p);
BOOL free_variable(char *svar, Formula f);
I2list function_symbols_in_formula(Formula f, I2list g);Collect the multiset of function symbols in a formula.
I2list function_symbols_in_formulas(Plist lst);Collect the multiset of function symbols (including constants) in formulas in a Plist. An I2list of SYMNUMs is returned.
Formula get_quant_form(Ftype type, char *qvar, Formula subformula);
int greatest_qvar(Formula f);Return the greatest SYMNUM of a quantified variable in Formula f.
Recall that in Formulas, a quantified variable is represented as a constant (which is bound by the quantifier). If the formula has no quantified variables, return -1.
int greatest_symnum_in_formula(Formula f);Return the greatest SYMNUM of a any subterm. This includes quantifed variables that don't occur in any term.
This routine is intended to be used if you need malloc an array for indexing by SYMNUM.
unsigned hash_formula(Formula f);This is a simple hash function for formulas. It shifts symbols by 3 bits and does exclusive ORs.
Formula imp(Formula a, Formula b);
Formula impby(Formula a, Formula b);
BOOL literal_formula(Formula f);
Formula make_conjunction(Formula f);If the formula is not a conjunction, make it so.
Formula make_disjunction(Formula f);If the formula is not a dismunction, make it so.
Formula negate(Formula a);
Formula nnf(Formula f);Transform a formula into negation normal form (NNF). (NNF means that all propositional connectives have been rewritten in terms of AND, OR and NOT, and all negation signs ar up against atomic formulas).
This routine is destructive; a good way to call it is f = nnf(f).
Formula nnf2(Formula f, Fpref pref);Transform a formula into negation normal form (NNF). (NNF means that all propositional connectives have been rewritten in terms of AND, OR and NOT, and all negation signs ar up against atomic formulas).
The argument "pref" should be either CONJUNCTION or DISJUNCTION, and it specifies the preferred form to use when translating IFFs.
This rouine is destructive; a good way to call it is f = nnf2(f, CONJUNCTION).
Formula or(Formula a, Formula b);
void p_formula(Formula c);This routine prints a formula, followed by ".\n" and fflush, to stdout. If you wish to have a formula printed without extra parentheses, you can call p_formula_term() instead. If you don't want the newline, use fprint_formula() instead.
void p_formula_mem();This routine prints (to stdout) memory usage statistics for data types associated with the formula package.
BOOL positive_formula(Formula f);Ignoring quantifiers, does the formula consist of an atomic formula or the conjunction of atomic formulas?
BOOL quant_form(Formula f);
BOOL relation_in_formula(Formula f, int symnum);Collect the multiset of relation symbols in a formula.
I2list relation_symbols_in_formula(Formula f, I2list g);Collect the multiset of relation symbols in a formula.
I2list relation_symbols_in_formulas(Plist lst);Collect the multiset of relation symbols (including constants) in formulas in a Plist. An I2list of SYMNUMs is returned.
void rename_all_bound_vars(Formula f);
void rename_these_bound_vars(Formula f, Ilist vars);
BOOL subformula_contains_attributes(Formula f);Does any proper subformula contain attributes?
void subst_free_var(Formula f, Term target, Term replacement);In formula f, substitute free occurrences of target with replacement. The function term_ident() is used, and the target can be any term.
Formula term_to_formula(Term t);Assume that no subterm (of t) representing a formula is a term of type VARIABLE. The given Term is not changed.
Formula universal_closure(Formula f);Construct the universal closure of Formula f. The Formula is consumed during the construction.
void zap_formula(Formula f);Free a formula, including all of its subformulas, including its atoms. If a subformula as excess references, the refcount is decremented instead.
/* formula types */
typedef enum {
ATOM_FORM=0, AND_FORM, OR_FORM, NOT_FORM, IFF_FORM,
IMP_FORM, IMPBY_FORM, ALL_FORM, EXISTS_FORM} Ftype;
typedef struct formula * Formula;
struct formula {
Ftype type;
int arity;
char *qvar; /* quantified variable */
Formula *kids; /* for non-atoms */
Term atom; /* for atoms */
Attribute attributes; /* */
int excess_refs; /* count of extra references */
};
/* formula preference */
typedef enum { CONJUNCTION,
DISJUNCTION
} Fpref;
/* macros */
#define TRUE_FORMULA(f) ((f)->type == AND_FORM && (f)->arity == 0)
#define FALSE_FORMULA(f) ((f)->type == OR_FORM && (f)->arity == 0)