This module defines a class gneg_c.
The objects of this class are ground default negations,
i.e. formulas of the form
not(p1 & ... & pn)
where the pi
are ground atomic formulas
(objects of the class glit_c).
Ground default negations appear as conditions
in conditional facts (see cf_c),
but they also appear in rules in case the default negation is ground
(see rneg_c).
So a gneg_c-object basically contains a list
of positive ground literals.
Of course,
the same ground literal cannot appear twice in the same default negation,
and the sequence of occurrence is irrelevant.
So a default negation really contains a set of ground literals.
In addition,
an efficient access from a positive ground literal
to the default negations in which it appears
is also supported
(see glit_c).
Therefore,
a many-to-many relationship between positive ground literals
and ground default negations is managed
(by means of the class gneg_f_c below).
This class has three additional features that improve the performance:
gneg_c-object.
gneg_c-object contains the anchor
of a list of conditional facts
in which the default negation occurs.
gneg_c-objects
can be detected efficiently.
This is needed when conditions of conditional facts
are constructed.
static gneg_c* store(glit_t *lits);lits are represented
as an array of pointers to
glit_c-objects
terminated with a NIL pointer.
It is important that no ground literal appears twice in this list.
If there is already a gneg_c-object
consisting of the given literals
a pointer to that object is returned.
The sequence of literals is not relevant for the comparison.
Otherwise,
a new object is constructed
and a pointer to the new object is returned.
Of course,
the new object is remembered for future calls to store.
static gneg_c* store(lit_t lits*);store is simply a convenient
interface to the other method store above.
The argument is an array of pointers to
lit_c-objects
terminated with a NIL-pointer.
The literals must not contain any variables.
Duplicates are allowed,
this method eliminates them when it translates
the lit_c-objects
into glit_c-objects.
After this translation,
the other method store is called
to create or retrieve the ground default negation.
static void print_all(void);gneg_c-objects (ground default negations).
In HTML mode,
the output is printed as an unordered list.
class gneg_l_c* get_elems(void) const;void print(void) const;not p,
otherwise parentheses will be used:
not(p1 & ... & pn).
bool_t is_conjunctive(void) const;BOOL_TRUE
if this default negation consists of more than one literal.
It returns BOOL_FALSE
if the negation consists of a single literal,
i.e. is of the form not p.
class cf_cn_c* get_occur(void) const;cf_cn_c
is an auxillary class that is defined
together with the class for conditional facts,
see cf_c.
It implements a many-to-many relationship
between ground default negations and conditional facts.
void set_occur(class cf_cn_c *occur);
When a disjunction of ground default negations
in the condtion part of a conditional fact is created,
the same ground literal should not appear twice.
The algorithm for this is simple and efficient:
Whenever a conditional fact is created,
the method dup_ck_begin
is called which increments a global counter
("current set number", class attribute).
Each gneg_c-object also contains a counter value.
The method dup_ck_is_new
checks whether the counter value in the object
is equal to the current value of the global counter.
If the two are equal,
the ground default negation is already a member of the current set.
Otherwise it is new.
In that case,
the counter in the object is set to the current value
of the global counter
so that the next time this object is accessed
it is detected as duplicate.
static void dup_ck_begin(void);dup_ck_begin is called,
it cannot be called again until dup_ck_end
was called.
bool_t dup_ck_is_new(void);BOOL_TRUE
the first time it is called for an object
after dup_ck_begin was called.
However,
each time it is called thereafter for the same object,
it returns BOOL_FALSE
(until dup_ck_begin is called again).
static void dup_ck_end(void);dup_ck_begin can be called again.
It is only needed to detect errors in the program code
(nested sets).
static int number_crit_neg(void);number_crit_neg
assigns a unique number (starting from 0)
to each of the distinct critical default negation literals.
It returns the number of such literals
(one higher than the largest assigned number).
This class does not have direct access to the residual program,
but it assumes that if the last call to set_occur
assigns a non-NIL list of occurrences,
the default negation literal does still occur in the residual
program.
Of course,
number_crit_neg must be called after the residual
program is computed.
The critical default negation literals are also stored in an
internal array, to support a fast access by number.
Therefore,
there is the possibility of an overflow.
If that happens,
this procedure prints an error message and exits the program.
Finally,
this procedure also marks the facts (positive ground literals)
inside the critical default negations as critical, too.
Only for these facts minimal models must be computed.
static inline gneg_c* get_crit_neg(int no);gneg_c-object
for a given number.
The number will normally be the result of a previous call
to get_no,
but the caller can also rely on the fact that numbers are assigned
sequentially by number_crit_neg
(from 0 to one below the result of the call to
number_crit_neg).
inline int get_no(void);number_crit_neg
has assigned the numbers,
and it may only be called for critical default negation literals,
i.e. default negations that occur in the residual program.
Objects of the class gneg_l_c
implement the many-to-many relationship "occurs in"
between ground literals and ground default negations.
It can also be seen as the list of elements (ground literals)
inside a ground default negation.
Objects of this class have the following methods
that may be interesting outside this module:
gneg_c *get_neg(void) const;glit_t get_lit(void) const;gneg_l_c *get_next_neg_elem(void) const;gneg_l_c *get_next_lit_occur(void) const;