[SLP-Homepage] [Source Modules] [Manual] [Run] [Examples]

Positive Ground Literals (Ground Atomic Formulas, Facts)

This module defines a class glit_c. The objects of this class are positive ground literals, i.e. atomic formulas without variables. They are often also called "facts", but one has to be careful not to confuse them with "conditional facts" that are ground rules without positive body literals. Positive ground literals consist of

a predicate (a pointer to an object of the class atom_c) and
an argument list (a pointer to an object of the class garg_c or NIL for literals without arguments). The arguments are constants cnst_c (elements of class

Note that there are actually three different classes for literals:

Literals in input formulas are represented by objects of the class lit_c.
Literals in conditional facts are represented by objects of this class.
Literals in hyperresolution derivation rules are represented by objects of the class rlit_c.

This distinction was made because of the different status of variables in the three cases, see rarg_c. Basically, there is no nice and elegant solution, so I decided to accept some duplication of code for a more type-safe solution.

The class glit_c has several additional features for improving the performance:

It ensures that every positive ground literal is represented only once. Therefore, it is possible to compare pointers to glit_c-objects in order to check the equality of two ground literals.
Each positive ground literal can be linked to its occurrences in heads of conditional facts (positive occurrences) and occurrences in default negations (negative occurrencs).
Duplicates in sets of positive ground literals can be easily detected. For instance, when a head of a conditional fact is constructed (disjunction of positive ground literals), it is possible that the same positive ground literal is contained in the disjunctive contexts of matches for two body literals. If duplicates would not be detected, hyperresolution would not terminate. Sets of positive ground literals are also used for the conjunction inside a default negation.

Class Methods (Static Member Functions):

init:: static void init(void);
This method initializes the hash table for objects of this class to the empty set. It must be called before store is called. It must not be called again later since this would create a memory leak.
store (predicate and arguments):: static glit_c* store(atom_t pred, cnst_t *args);
This method searches the current set of positive ground literals for one that has the given predicate and arguments. The arguments args are represented as an array of pointers to constants (ground terms) terminated with a NIL pointer. If there is already a glit_c object with the given predicate and arguments, a pointer to that object is returned. Otherwise, a new object is constructed and a pointer to the new object is returned. Of course, the new object is entered into the hash table for finding it on future calls to store.
store (literal):: static glit_c* store(lit_t lit);
This method store is simply a convenient interface to the other method store above. The argument must be a literal that does not contain any variables. The predicate and constant arguments are extracted and the corresponding positive ground literal is created or retrieved.

Object Methods (Standard Functions for Literals):

get_pred:: atom_t get_pred(void) const;
This method returns the predicate of this ground literal.
get_args:: garg_t get_args(void) const;
This method returns the argument list of this ground literal.
is_answer_lit:: bool_t is_answer_lit(void) const;
This method returns BOOL_TRUE if this literal has the special predicate $answer.
print:: void print(void) const;
This method prints this ground literal. If the argument list is empty, it prints only the predicate. If the argument list is not empty, it prints the predicate and then the argument list in parentheses.

Object Methods (Functions for Managing Occurrences):

get_pos_occur:: class cf_hd_c* get_pos_occur(void) const;
This method returns the anchor to a list of occurrences of this positive ground literal in heads of conditional facts (positive occurrences).
set_pos_occur:: void set_pos_occur(class cf_hd_c* pos_occur);
This method sets the value returned by get_pos_occur (list of occurrences of this ground literal in heads of conditional facts).
inc_pos_occur:: void inc_pos_occur(void);
Whereas get_pos_occur returns a list of all occurrences of this positive ground literal in heads of conditional facts, this function is used to count only occurrences in conditional facts that do not contain a $answer-literal. Conditional facts about $answer are used to compute answers to the query, but they do not really belong to the residual program. Therefore any occurrences of ground literals in the heads of such facts are ignored when doing positive reduction. If this ground literal was on the positive reduction queue, it is removed from it.
dec_pos_occur:: void dec_pos_occur(void);
This function decrements the number of occurrences of this ground literal in the heads of conditional facts (where conditional facts about $answer are not counted). If the counter reaches 0, (and the ground literal was not already used for positive reduction), this ground literal is inserted into the positive reduction queue.
get_neg_occur:: class gneg_l_c* get_neg_occur(void) const;
This method returns the anchor to a list of occurrences of this positive ground literal in ground default negations (negative occurrences).
set_neg_occur:: void set_neg_occur(class gneg_l_c* neg_occur);
This method sets the value returned by get_neg_occur (list of occurrences of this ground literal in ground default negations).
get_dis_occur:: class mdis_e_c* get_dis_occur(void) const;
This method returns the anchor to a list of occurrences of this positive ground literal in disjunctions used in the minimal model generator (mgen_c, mdis_c).
set_dis_occur:: void set_dis_occur(class mdis_e_c* dis_occur);
This method sets the value returned by get_dis_occur (list of occurrences of this ground literal in disjunctions used in the minimal model generator).

Class and Object Methods (Functions for Avoiding Duplicates):

When a disjunction of positive ground literals in a head of a conditional fact is created, the same ground literal should not appear twice. In the same way, duplicate ground literals must be avoided in the conjunctions inside default negations. The algorithm for this is simple and efficient: Whenever a conditional fact or a default negation is created, a counter is incremented. The current value of this counter is stored in each positive ground literal that is used. So in order to check whether a ground literal was already used in the current disjunction/conjunction, one simply compares the current value of the counter with the value in the object.

dup_ck_begin:: static void dup_ck_begin(void);
This method opens a new set of positive ground literals. It simply increments the counter for the current set identification. The efficient algorithm for detecting duplicates can work only with one set at a time, sets cannot be nested. Therefore, after dup_ck_begin is called, it cannot be called again until dup_ck_end was called.
dup_ck_is_new:: bool_t dup_ck_is_new(void);
This method returns 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).
dup_ck_end:: static void dup_ck_end(void);
This method closes the current set so that dup_ck_begin can be called again. It is only needed to detect errors in the program code (nested sets). I earlier had two different counters for uses of the ground literal in disjunctive heads and conjunctive default negations (that were managed outside this module). When I decided to put this functionality into this module, I wanted to make sure that I detected any conflicts in the use of the now single counter. Otherwise dup_ck_end is not needed, the real work (incrementing the counter for the current set) is done in dup_ck_begin.

Class and Object Methods (Functions for Managing Critical Facts):

We call default negation literals "critical" if they still appear in the residual program. For these negations an expensive fixpoint computation must be done to compute the static semantics. Positive ground literals (facts) are called critical when they appear in a critical default negation. In the minimal model computation for the static semantics, only the truth value of critical facts must be determined. Since hopefully only a small subset of all facts are critical, it is a useful optimization to reduce the model computation in this way.

mark_critical:: void mark_critical(void);
The method mark_critical adds this object to the list of critical facts if it is not already on the list. So it is possible to call this method several times for the same object: All calls except the first one are basically ignored.
get_crit_facts:: static glit_c* get_crit_facts(void);
This class method returns the first element in the list of all positive ground literals that were marked as critical (i.e. the list anchor).
get_next_crit:: glit_c* get_next_crit(void) const;
This method returns the next element in the list of critical facts. Of course, it can only be called for critical facts.
get_prev_crit:: glit_c* get_prev_crit(void) const;
This method returns the previous element in the list of critical facts. Of course, it can only be called for critical facts.
print_crit_model:: static void print_crit_model(void);
This method prints the current interpretation for the critical facts. It can only be called when the set of critical facts is not empty. Furthermore, truth values of all critical facts must have been determined by calling set_true or set_false.

Object Methods (Functions for Managing Model Generator Truth Values):

The model generator (mgen_c) can mark facts as true or as false. As long as neither set_true nor set_false are called for a fact, its truth value is unknown. Then is_true and is_false both return "false". The model generator works with backtracking, so it must be able to return to a previous partial interpretation. This is implemented by managing a stack of facts that were assigned a truth value in the facts itself (using the link NextInterp). The class method get_interp_state returns the current partial interpretation, and interp_backtrack backtracks to a previously saved state.

set_true:: void set_true(void);
This method marks the fact as true, i.e. future calls to is_true will return true. One cannot change the truth value from false to true, so the truth value must be unknown or true before this method is called. If it is already true, the call is simply ignored.
set_false:: void set_false(void);
This method marks the fact as false, i.e. future calls to is_false will return true. The method may only be called if the current truth value of the object is unknown or false.
is_true:: bool_t is_true(void) const;
This method returns BOOL_TRUE if set_true was previously called, i.e. the model generator currently considers models in which this fact is true.
is_false:: bool_t is_false(void) const;
This method returns BOOL_TRUE if set_false was previously called, i.e. the model generator currently considers models in which this fact is false.
get_interp_state:: static glit_c* get_interp_state(void);
This method returns the current partial interpretation that can be later restored with interp_backtrack. Partial interpretation can only be restored in a stack (LIFO) manner: If get_interp_state first returns A, and later B, then B can only be restored before A. However, it is not required that B is restored at all, one can directly jump to A.
interp_backtrack:: static void interp_backtrack(glit_c* state);
This method restores a previous partial interpretation (state of assignments of truth values to facts) that was earlier saved with get_interp_state.

Implementation:

Stefan Brass (sbrass@sis.pitt.edu), April 6, 2002. [HTML 3.2 Checked]