[SLP-Homepage]
[Source Modules]
[Manual]
[Run]
[Examples]
Literal (Atomic Formula) in an Input Formula
This module defines a class lit_c.
Its objects represent literals (actually, atomic formulas)
in input formulas.
They 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 tlist_c
or NIL for literals without arguments).
Note that there are actually three different classes
for literals:
- Literals in input formulas are represented by objects
of this class.
- Literals in conditional facts are represented by objects
of the class fact_c.
- 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.
Construction:
- lit_c:
-
lit_c(atom_t predicate, tlist_t args);
This method creates a new literal
with a given predicate and argument list.
Object Methods:
- get_pred:
-
atom_t get_pred(void) const;
This method returns the predicate of this literal.
- get_args:
-
tlist_t get_args(void) const;
This method returns the argument list of this literal.
- print:
-
void print(rvars_t vars) const;
This method prints this 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.
- contains_anon:
-
bool_t contains_anon(void) const;
This method returns BOOL_TRUE
if the literal contains an anonymous variable as argument.
This is needed for the safety (allowedness, range restriction) check:
Such literals are only allowed in rule bodies
(i.e. in a negative context).
- check_safety:
-
bool_t check_safety(void);
This method checks whether this literal contains
non-anonymous variables among its arguments.
All such variables are added to the set of unsafe variables.
This is needed for the safety (allowedness, range restriction) check:
If a clause has no positive body literals,
i.e. can be classified as a conditional fact,
it must not contain any variables.
If the safety check is passed
(no non-anonymous variables),
BOOL_TRUE is returned,
otherwise BOOL_FALSE.
Note that the parser must additionally check
for anonymous variables.
Implementation:
Stefan Brass
(sbrass@sis.pitt.edu),
October 2, 2001.
[HTML 3.2 Checked]