This module defines a class unsafe_c which is used to temporarily store all unsafe variables in the current formula. Unsafe variables are those variables that violate the allowedness/range-striction condition, i.e. that appear in the head or negative body literals, but that do not appear in a positive body literal.
This module is only used for printing an error message. It seemed better to print an error message that lists all unsafe variables in the formula than to print only one, because the first unsafe variable that is discovered is not necessarily the first one that the user wrote. If only the first discovered variable would be listed in the error message, the user might wonder why this variable is incorrect while similar other variables are apperently correct.
This class has no instances,
all methods are declared as static (class methods).
At the beginning of the translation of an input formula into clauses
the method
reset is called,
that initializes the unsafe variable set to the empty set.
When unsafe variables are discovered,
they can be added to the set with the method add_var.
The method can be called several times for the same variable,
it will be added only once.
Finally,
one can check with the method is_empty
whether the variable set is still empty.
If not,
the input formula violates the allowedness/range-restriction condition.
Then the method print
can be called to print the set of unsafe variables.
Class Methods:
void reset(void);
This method initializes the set managed by this module
to the empty set.
It must be called before any of the other methods below.
It can be called any number of times
(there is no memory leak if an existing set is emptied).
static void add_var(var_t var);
This method adds a variable to the current set of
unsafe variables.
It is possible to call the method more than once for the same variable,
the variable will be added only once.
static bool_t is_empty();
This method returns BOOL_TRUE
if the set of unsafe variables is currently empty,
i.e. the allowedness/range-restriction condition is not violated.
Otherwise BOOL_FALSE is returned
(then the condition is violated,
i.e. the current input formula is illegal).
static void print(void);
This method prints the lists of variables
(separated by commas, terminated with fullstop).
Implementation:
Stefan Brass
(sbrass@sis.pitt.edu),
October 2, 2001.
[HTML 3.2 Checked]