Default Negation in a Rule

This module defines a class rneg_c. Its objects represent default negations in rules. They basically consist of a list of literals (where the literals are considered as conjunctively connected). However, if the default negation should be ground (i.e. not contain variables), a pointer to the corresponding gneg_c-object is stored in addition. The class gneg_c represents ground default negations that appear in conditional facts. It is more efficient to compute the ground default negation only once and store it in this object instead of doing this every time the rule is applied. And input specifications that do not use variables should not pay the price for them.

Note that there are actually three different classes for default negations:

• Default negations in input formulas are represented by objects of the class fml_c.
• Default negations in conditional facts are represented by objects of the class gneg_c.
• Default negations in hyperresolution derivation rules are represented by objects of this class.

Actually, objects of this class represent lists of default negations since they contain a pointer to the next default negation in the same rule. Earlier, I had a separate class for lists of default negations (called rnegs_c), but since each rneg_c-object belongs only to a single rule this was an unncessary complication of the code. In addition, the method for getting the first list element was called get_head (in the sense of head vs. tail), which was quite confusing ("head" is also head of a rule).

rneg_c:

rneg_c(lit_t *lits, rvars_t vars);;
This method creates a new object of this class by translating a list of literal from an input formula into the "rule default negation" format. The list of input literals is represented as an array of pointers to these literals terminated by a NIL pointer. This method 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. However, any such variable is unsafe (violates the allowedness/range-restriction condition). Therefore these variables are also added to the set of unsafe variables, see unsafe_c).

is_ground:

bool_t is_ground(void) const;
This method returns BOOL_TRUE if the default negation is ground, i.e. does not contain any variables. In this case, get_neg can be used (see below).

get_lits:

rlits_t get_lits(void) const;
This method returns the list of literals inside the default negation.

get_ground:

gneg_t get_gneg(void) const;
This method returns the gneg_c-object corresponding to this default negation. It can only be used if this default negation does not contain any variables.

get_next:

rneg_c* get_next(void) const;
Get the next default negation in the same rule. DT>set_next:

void set_next(rneg_c* next);
This method sets the pointer to the next default negation in the same rule. It can only be called if the next-link is currently NIL, i.e. if this is the last list element.

print:

void print(rvars_t vars) const;
This method prints the default negation. The set of variables in the rule is needed in order to replace the variable offset numbers stored in the rule literals by variable names.

print_list:

void print_list(rvars_t vars) const;
This method prints the default negation including the following ones that can be reached via the "next"-pointers. Since the objects for the default negations contain only the variable offsets, the list of variables in the rule is needed in order to print the variable names.

• Header File (rneg.h)
• Source File (rneg.cxx)