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(var_t var, int offset)
;
var_t get_var(void)
;int get_offset(void)
;bool_t is_bound(void)
;BOOL_TRUE
if the variable already occurs in a positive body literal
and BOOL_FALSE
otherwise.
void make_bound(void)
;rvar_c* get_next(void)
;void set_next(rvar_c* next)
;void print(void)
;