Literal (Atomic Formula) in a Rule

This module defines a class rlit_c. Its objects represent literals (actually, atomic formulas) in rules. They consist of

• a predicate (a pointer to an object of the class atom_c) and
• an argument list (a pointer to an object of the class rargs_c or NIL for literals without arguments).

As an additional optimization, ground literals (literals without variables) are treated specially: In this case, the fact_c object corresponding to the literal is computed and stored in addition to the predicate and the argument list. Facts can be tested for equality by comparing their addresses, which is faster than comparing the predicate and all arguments.

Note that there are actually three different classes for literals:

• Literals in input formulas are represented by objects of the class lit_c.
• Literals in conditional facts are represented by objects of the class glit_c.
• Literals in hyperresolution derivation rules are represented by objects of this class.

rlit_c:

rlit_c(lit_t lit, rvars_t vars, bool_t binding);;
This method creates a new object of this class by translating a literal from an input formula into the "rule literal" format. It needs the list of variables in the current rule to put the correct binding frame offsets into the argument terms. If the input literal contains variables that do not yet appear in vars, they are automatically added. If in this case binding is BOOL_FALSE, they are also added to the set of unsafe variables (that violate the allowedness/range-restriction condition, see unsafe_c). That means the positive body literals must be translated first with binding=BOOL_TRUE in order to initialize vars. After that, the head literals and default negations can be translated with binding=BOOL_FALSE. They are not supposed to add variables to vars, and if they do, these variables will be flagged as "unsafe".

is_ground:

bool_t is_ground(void) const;
This method returns BOOL_TRUE if the literal is ground, i.e. does not contain any variables. In this case, get_fact can be used (see below). Otherwise (the literal contains variables) BOOL_FALSE is returned.

get_pred:

atom_t get_pred(void) const;
This method returns the predicate of the literal. It can be used for ground and non-ground literals, although for ground literals, it is more efficient to work directly with facts.

get_args:

rargs_t get_args(void) const;
This method returns the argument list of this literal. It can be used for ground and non-ground literals, although for ground literals, it is more efficient to work directly with facts.

get_ground:

glit_t get_ground(void) const;
This method can only be used if the literal is ground. It then returns the glit_c-object corresponding to this literal.

print:

void print(rvars_t vars) const;
This method prints this literal. If the argument list is empty, it prints only the predicate. If the argument list is not empty, it prints the predicate and then the argument list in parentheses. The list of variables in the rule is needed in order to translate the variable offsets (which stored in the argument list) into variable names.