Argument Term in a Rule

• This is the first occurrence of the variable, i.e. the variable is currently free (not bound to a value). In the hyperresolution step, a value will be assigned when such a term is matched with an argument term in a fact.
• This is not the first occurrence of a variable, i.e. the variable is already bound to a value. In the hyperresolution step, the current value of the variable will be compared with the corresponding argument term in the fact.
• This is an anonymous variable, i.e. the only occurrence of the variable. This is very similar to the first case, but it is not necessary to actually assign a value since it would never be used. So anonymous variables can simply be skipped.

Note that there are other classes for argument terms in input formulas (class term_c), and for argument terms in facts (class farg_c). It was a difficult decision to make these three classes instead of a single generic term class. The problem is the different treatment of variables: Facts contain no variables at all, and in the input formulas, the distinction between free and bound occurrences of variables is not meaningful: When the formula is translated into clauses, the same variable occurrence can be free in one clause, and bound in another. Of course, it would have been possible to determine the free/bound status at runtime, but then backtracking would have been more difficult (we would need a trail as in Prolog). Therefore I believe that separating the three kinds of terms is in the end the easiest and cleanest solution, although there is some duplication of code that is not nice.

rarg_c:

rarg_c(term_t term, rvars_t vars, bool_t binding);
This method transforms a given term (from an input formula) into an object of this class (argument term of a rule). In order to do this, it needs the set of variables in the current rule. If the input term should be a variable that does not yet occur in vars, it will be added. If binding is BOOL_FALSE, any variables that do not already appear in vars will be added to the set of unsafe variables, see unsafe_c. Note that anonymous variables are not caught in this way, since there is no var_c object for them. So the parser must do an additional test for anonymous variables in non-binding contexts.

is_free:

bool_t is_free() const;
This method returns BOOL_TRUE if this term is a free variable (i.e. this is the first occurrence of the variable in the rule, it is not yet bound to a value). Otherwise is_free returns BOOL_FALSE.

is_bound:

bool_t is_bound() const;
This method returns BOOL_TRUE if this term is a bound variable (i.e. this is not the first occurrence of the variable in the rule, it is already bound to a value). Otherwise is_bound returns BOOL_FALSE.

is_anon:

bool_t is_anon(void) const;
This method returns BOOL_TRUE if this term is an anonymous variable. Otherwise it returns BOOL_FALSE.

is_cnst:

bool_t is_cnst(void) const;
This method returns BOOL_TRUE if this term is a constant (symbolic constant/atom or integer). Otherwise it returns BOOL_FALSE.

get_offset:

int get_offset(void) const;
This method may only be called if this term is a non-anonymous variable (bound or free). It then returns the offset of this variable in the binding frame used in the hyperresolution step.

get_cnst:

farg_t get_cnst(void) const;
This method may only be called if this term is a constant (symbolic constant/atom or integer). It then returns a pointer to the constant (represented as an object of class farg_c).

print:

void print(rvars_t vars) const;
This method prints the term. Since the term does not itself contain the variable names, only their offsets, it needs access to the list of variables in the current rule.

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