Variable in a Rule

This module defines a class rvar_c. The objects of this class correspond to variables in rules. They contain a pointer to the corresponding var_c object (variable in input formula). In addition, each variable in a rule is assigned an offset in the binding frame (that stores variable values during the hyperresolution step). In general, one input formula is transformed into several internal clauses (conditional facts and rules). If the same variable appears in several such rules, several rvar_c objects will point to the same var_c object. The variable can have different offsets in different clauses. It is also necessary to store a flag that indicates whether the variable is bound in the current rule. "Bound" means that it appears in a positive body literal, so it does not violate the "allowedness" or "safety" condition. If an input formula is transformed into multiple clauses, it is again possible that the same variable is bound in one clause but not in another one.

It was a difficult decision to separate "Variable in a Formula" and "Variable in a Rule", but since offset and binding status have no meaning for input variables, and are known only after the translation into clauses, this seemed to be the cleanest solution.

In order not to produce too many classes, objects of this class already have a link to the next variable in the same rule.

rvar_c:

rvar_c(var_t var, int offset);
This method creates a new rule variable based on a formula variable. In addition, the offset of the variable in the binding frame for this rule must be specified. It should be 0 for the first variable, 1 for the second, and so on. The binding status is initialized to "unbound" and the pointer to the next variable is initially set to NIL.

get_var:

var_t get_var(void);
This method returns the formula variable on which this rule variable is based. For instance, the variable name is stored in the formula variable.

get_offset:

int get_offset(void);
This method returns the offset of the variable in the binding frame for the current rule (0,1,2,...).

is_bound:

bool_t is_bound(void);
This method returns BOOL_TRUE if the variable already occurs in a positive body literal and BOOL_FALSE otherwise.

make_bound:

void make_bound(void);
This method must be called if the variable occurs in a positive body literal in order to mark it as it bound. The constructor of this class initializes all variables to unbound. After the clause is constructed, all variables in it must be bound, or an error message is printed.

get_next:

rvar_c* get_next(void);
This method returns the next variable in the same rule (or 0 if there is none).

set_next:

void set_next(rvar_c* next);
This method is used to set the pointer to the next variable in the same rule. When the variable is constructed, this pointer is initialized to NIL. It may be set only once, i.e. it is an error to call this method for an object that has already a non-NIL pointer.

print:

void print(void);
This method prints the variable name followed by the offset of the variable.

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