blob: 4207913b5b147371237354ffa2575a1bb20f876f [file] [log] [blame]
/**************************************************************/
/* ********************************************************** */
/* * * */
/* * CLAUSES * */
/* * * */
/* * $Module: CLAUSE * */
/* * * */
/* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */
/* * MPI fuer Informatik * */
/* * * */
/* * This program is free software; you can redistribute * */
/* * it and/or modify it under the terms of the GNU * */
/* * General Public License as published by the Free * */
/* * Software Foundation; either version 2 of the License, * */
/* * or (at your option) any later version. * */
/* * * */
/* * This program is distributed in the hope that it will * */
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
/* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */
/* * License for more details. * */
/* * * */
/* * You should have received a copy of the GNU General * */
/* * Public License along with this program; if not, write * */
/* * to the Free Software Foundation, Inc., 59 Temple * */
/* * Place, Suite 330, Boston, MA 02111-1307 USA * */
/* * * */
/* * * */
/* $Revision$ * */
/* $State$ * */
/* $Date$ * */
/* $Author$ * */
/* * * */
/* * Contact: * */
/* * Christoph Weidenbach * */
/* * MPI fuer Informatik * */
/* * Stuhlsatzenhausweg 85 * */
/* * 66123 Saarbruecken * */
/* * Email: weidenb@mpi-sb.mpg.de * */
/* * Germany * */
/* * * */
/* ********************************************************** */
/**************************************************************/
/* $RCSfile$ */
#include "clause.h"
/**************************************************************/
/* Global variables and constants */
/**************************************************************/
/* Means weight of literal or clause is undefined */
const NAT clause_WEIGHTUNDEFINED = NAT_MAX;
int clause_CLAUSECOUNTER;
NAT clause_STAMPID;
/* The following array is used for bucket sort on clauses */
#define clause_MAXWEIGHT 20
LIST clause_SORT[clause_MAXWEIGHT+1];
/**************************************************************/
/* Inline functions */
/**************************************************************/
static __inline__ void clause_FreeLitArray(CLAUSE Clause)
{
NAT Length = clause_Length(Clause);
if (Length > 0)
memory_Free(Clause->literals, sizeof(LITERAL) * Length);
}
/**************************************************************/
/* Primitive literal functions */
/**************************************************************/
BOOL clause_LiteralIsLiteral(LITERAL Literal)
/*********************************************************
INPUT: A literal.
RETURNS: TRUE, if 'Literal' is not NULL and has a predicate
symbol as its atoms top symbol.
**********************************************************/
{
return ((Literal != NULL) &&
symbol_IsPredicate(clause_LiteralPredicate(Literal)));
}
NAT clause_LiteralComputeWeight(LITERAL Literal, FLAGSTORE Flags)
/*********************************************************
INPUT: A literal and a flag store.
RETURNS: The weight of the literal.
CAUTION: This function does not update the weight of the literal!
**********************************************************/
{
TERM Term;
int Bottom;
NAT Number;
#ifdef CHECK
if (!clause_LiteralIsLiteral(Literal)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralComputeWeight :");
misc_ErrorReport("Illegal Input. Input not a literal.");
misc_FinishErrorReport();
}
#endif
Term = clause_LiteralSignedAtom(Literal);
Bottom = stack_Bottom();
Number = 0;
do {
if (term_IsComplex(Term)) {
Number += flag_GetFlagValue(Flags, flag_FUNCWEIGHT);
stack_Push(term_ArgumentList(Term));
}
else
if (term_IsVariable(Term))
Number += flag_GetFlagValue(Flags, flag_VARWEIGHT);
else
Number += flag_GetFlagValue(Flags, flag_FUNCWEIGHT);
while (!stack_Empty(Bottom) && list_Empty(stack_Top()))
stack_Pop();
if (!stack_Empty(Bottom)) {
Term = (TERM) list_Car(stack_Top());
stack_RplacTop(list_Cdr(stack_Top()));
}
} while (!stack_Empty(Bottom));
return Number;
}
LITERAL clause_LiteralCreate(TERM Atom, CLAUSE Clause)
/**********************************************************
INPUT: A Pointer to a signed Predicate-Term and one to a
clause it shall belong to.
RETURNS: An appropriate literal where the other values
are set to default values.
MEMORY: A LITERAL_NODE is allocated.
CAUTION: The weight of the literal is not set correctly!
***********************************************************/
{
LITERAL Result;
#ifdef CHECK
if (!term_IsTerm(Atom)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralCreate:");
misc_ErrorReport("\n Illegal input. Input not a term.");
misc_FinishErrorReport();
}
if (!symbol_IsPredicate(term_TopSymbol(Atom)) &&
(term_TopSymbol(Atom) != fol_Not())) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralCreate:");
misc_ErrorReport("\n Illegal input. No predicate- or negated term.");
misc_FinishErrorReport();
}
#endif
Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE));
Result->atomWithSign = Atom;
Result->oriented = FALSE;
Result->weight = clause_WEIGHTUNDEFINED;
Result->maxLit = 0;
Result->owningClause = Clause;
return Result;
}
LITERAL clause_LiteralCreateNegative(TERM Atom, CLAUSE Clause)
/**********************************************************
INPUT: A Pointer to a unsigned Predicate-Term and one to a
clause it shall belong to.
RETURNS: An appropriate literal where the other values
are set to default values and the term gets a sign.
MEMORY: A LITERAL_NODE is allocated.
CAUTION: The weight of the literal is not set correctly!
***********************************************************/
{
LITERAL Result;
#ifdef CHECK
if (!term_IsTerm(Atom)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralCreateNegative:");
misc_ErrorReport("\n Illegal input. Input not an atom.");
misc_FinishErrorReport();
}
if (!symbol_IsPredicate(term_TopSymbol(Atom)) &&
(term_TopSymbol(Atom) != fol_Not())) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralCreateNegative:");
misc_ErrorReport("\n Illegal input. Input term not normalized.");
misc_FinishErrorReport();
}
#endif
Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE));
term_RplacSupertermList(Atom, list_Nil());
Result->atomWithSign = term_Create(fol_Not(), list_List(Atom));
Result->oriented = FALSE;
Result->maxLit = 0;
Result->weight = clause_WEIGHTUNDEFINED;
Result->owningClause = Clause;
return Result;
}
void clause_LiteralDelete(LITERAL Literal)
/*********************************************************
INPUT: A literal, which has an unshared Atom. For Shared
literals clause_LiteralDeleteFromSharing(Lit) is
available.
RETURNS: Nothing.
MEMORY: The Atom of 'Literal' is deleted and its memory
is freed as well as the LITERAL_NODE.
**********************************************************/
{
#ifdef CHECK
if (!clause_LiteralIsLiteral(Literal)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralDelete:");
misc_ErrorReport("\n Illegal input. Input not a literal.");
misc_FinishErrorReport();
}
#endif
term_Delete(clause_LiteralSignedAtom(Literal));
clause_LiteralFree(Literal);
}
void clause_LiteralInsertIntoSharing(LITERAL Lit, SHARED_INDEX ShIndex)
/**********************************************************
INPUT: A Literal with an unshared Atom and an Index.
RETURNS: The literal with a shared Atom inserted into the
'Index'.
MEMORY: Allocates TERM_NODE memory needed to insert 'Lit'
into the sharing and frees the memory of the
unshared Atom.
***********************************************************/
{
TERM Atom;
#ifdef CHECK
if (!clause_LiteralIsLiteral(Lit)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralInsertIntoSharing:");
misc_ErrorReport("\n Illegal literal input.");
misc_FinishErrorReport();
}
#endif
Atom = clause_LiteralAtom(Lit);
clause_LiteralSetAtom(Lit, sharing_Insert(Lit, Atom, ShIndex));
term_Delete(Atom);
}
void clause_LiteralDeleteFromSharing(LITERAL Lit, SHARED_INDEX ShIndex)
/**********************************************************
INPUT: A Literal and an 'Index'.
RETURNS: Nothing.
MEMORY: Deletes 'Lit' from Sharing, frees no more used
TERM memory and frees the LITERAL_NODE.
********************************************************/
{
TERM Atom;
#ifdef CHECK
if (!clause_LiteralIsLiteral(Lit)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralDeleteFromSharing:");
misc_ErrorReport("\n Illegal literal input.");
misc_FinishErrorReport();
}
#endif
Atom = clause_LiteralAtom(Lit);
if (clause_LiteralIsNegative(Lit)) {
list_Free(term_ArgumentList(clause_LiteralSignedAtom(Lit)));
term_Free(clause_LiteralSignedAtom(Lit));
}
sharing_Delete(Lit, Atom, ShIndex);
clause_LiteralFree(Lit);
}
static LIST clause_CopyLitInterval(CLAUSE Clause, int Start, int End)
/**************************************************************
INPUT: A clause and two integers representing
literal indices.
RETURNS: Copies of all literals in <Clause> with index i and
in the interval [Start:End] are prepended to <List>.
MEMORY: All atoms are copied.
***************************************************************/
{
TERM Atom;
LIST List;
List = list_Nil();
for ( ; Start <= End; Start++) {
Atom = term_Copy(clause_GetLiteralAtom(Clause, Start));
List = list_Cons(Atom, List);
}
return List;
}
static LIST clause_CopyLitIntervalExcept(CLAUSE Clause, int Start, int End,
int i)
/**************************************************************
INPUT: A clause and three integers representing
literal indeces.
RETURNS: A list of atoms from literals within the interval
[Start:End] except the literal at index <i>.
MEMORY: All atoms are copied.
***************************************************************/
{
TERM Atom;
LIST Result;
Result = list_Nil();
for ( ; End >= Start; End--)
if (End != i) {
Atom = term_Copy(clause_GetLiteralAtom(Clause, End));
Result = list_Cons(Atom, Result);
}
return Result;
}
LIST clause_CopyConstraint(CLAUSE Clause)
/**************************************************************
INPUT: A clause.
RETURNS: The list of copied constraint literals from <Clause>.
***************************************************************/
{
return clause_CopyLitInterval(Clause,
clause_FirstConstraintLitIndex(Clause),
clause_LastConstraintLitIndex(Clause));
}
LIST clause_CopyAntecedentExcept(CLAUSE Clause, int i)
/**************************************************************
INPUT: A clause.
RETURNS: A list containing copies of all antecedent literals
except <i>.
***************************************************************/
{
return clause_CopyLitIntervalExcept(Clause,
clause_FirstAntecedentLitIndex(Clause),
clause_LastAntecedentLitIndex(Clause),
i);
}
LIST clause_CopySuccedent(CLAUSE Clause)
/**************************************************************
INPUT: A clause.
RETURNS: The list of copied succedent literals from <Clause>.
***************************************************************/
{
return clause_CopyLitInterval(Clause,
clause_FirstSuccedentLitIndex(Clause),
clause_LastSuccedentLitIndex(Clause));
}
LIST clause_CopySuccedentExcept(CLAUSE Clause, int i)
/**************************************************************
INPUT: A clause.
RETURNS: A list containing copies of all succedent literals
except <i>.
***************************************************************/
{
return clause_CopyLitIntervalExcept(Clause,
clause_FirstSuccedentLitIndex(Clause),
clause_LastSuccedentLitIndex(Clause),
i);
}
/**************************************************************/
/* Specials */
/**************************************************************/
BOOL clause_IsUnorderedClause(CLAUSE Clause)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the invariants concerning splitting etc. hold
Invariants concerning maximality restrictions are not tested.
**********************************************************/
{
return ((Clause != NULL) &&
clause_CheckSplitLevel(Clause) &&
(clause_IsEmptyClause(Clause) ||
/* Check the first literal as a "random" sample */
clause_LiteralIsLiteral(clause_GetLiteral(Clause,clause_FirstLitIndex()))) &&
(clause_SplitLevel(Clause) == 0 || Clause->splitfield_length>0) &&
clause_DependsOnSplitLevel(Clause,clause_SplitLevel(Clause)));
}
BOOL clause_IsClause(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence)
/*********************************************************
INPUT: A clause, a flag store and a precedence.
RETURNS: TRUE, if literals are correctly ordered and the
invariants concerning splitting etc. hold
**********************************************************/
{
int i;
LITERAL ActLit;
if (!clause_IsUnorderedClause(Clause))
return FALSE;
for (i=clause_FirstAntecedentLitIndex(Clause);i<=clause_LastSuccedentLitIndex(Clause);i++) {
ActLit = clause_GetLiteral(Clause,i);
if (fol_IsEquality(clause_LiteralSignedAtom(ActLit))) {
ord_RESULT HelpRes;
HelpRes =
ord_Compare(term_FirstArgument(clause_LiteralSignedAtom(ActLit)),
term_SecondArgument(clause_LiteralSignedAtom(ActLit)),
FlagStore, Precedence);
if (ord_IsSmallerThan(HelpRes))
return FALSE;
}
}
return TRUE;
}
BOOL clause_ContainsPositiveEquations(CLAUSE Clause)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the clause contains a positive equality literal.
**********************************************************/
{
int i;
for (i = clause_FirstSuccedentLitIndex(Clause);
i < clause_Length(Clause);
i++)
if (clause_LiteralIsEquality(clause_GetLiteral(Clause, i)))
return TRUE;
return FALSE;
}
BOOL clause_ContainsNegativeEquations(CLAUSE Clause)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the clause contains a positive equality literal.
**********************************************************/
{
int i;
for (i = clause_FirstAntecedentLitIndex(Clause);
i < clause_FirstSuccedentLitIndex(Clause);
i++)
if (clause_LiteralIsEquality(clause_GetLiteral(Clause, i)))
return TRUE;
return FALSE;
}
int clause_ContainsFolAtom(CLAUSE Clause, BOOL *Prop, BOOL *Grd, BOOL *Monadic,
BOOL *NonMonadic)
/*********************************************************
INPUT: A clause.
RETURNS: The number of boolean variables changed.
If <*Prop> is FALSE and the clause contains a propositional
variable, it is changed to TRUE.
If <*Grd> is FALSE and the clause contains a non-propositional
ground atom, it is changed to TRUE.
If <*Monadic> is FALSE and the clause contains a monadic atom,
it is changed to TRUE.
If <*NonMonadic> is FALSE and the clause contains an at least
2-place non-equality atom, it is changed to TRUE.
**********************************************************/
{
int i,Result,Arity;
BOOL Ground;
Result = 0;
i = clause_FirstLitIndex();
while (Result < 4 &&
i < clause_Length(Clause) &&
(!(*Prop) || !(*Monadic) || !(*NonMonadic))) {
Arity = symbol_Arity(term_TopSymbol(clause_GetLiteralAtom(Clause,i)));
Ground = term_IsGround(clause_GetLiteralAtom(Clause,i));
if (!(*Prop) && Arity == 0) {
Result++;
*Prop = TRUE;
}
if (!(*Grd) && Arity > 0 && Ground &&
!fol_IsEquality(clause_GetLiteralAtom(Clause,i))) {
Result++;
*Grd = TRUE;
}
if (!(*Monadic) && Arity == 1 && !Ground) {
Result++;
*Monadic = TRUE;
}
if (!(*NonMonadic) && Arity > 1 && !Ground &&
!fol_IsEquality(clause_GetLiteralAtom(Clause,i))) {
Result++;
*NonMonadic = TRUE;
}
i++;
}
return Result;
}
BOOL clause_ContainsVariables(CLAUSE Clause)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the clause contains at least one variable
**********************************************************/
{
int i;
TERM Term;
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) {
Term = clause_GetLiteralAtom(Clause,i);
if (term_NumberOfVarOccs(Term)>0)
return TRUE;
}
return FALSE;
}
void clause_ContainsSortRestriction(CLAUSE Clause, BOOL *Sortres, BOOL *USortres)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the clause contains a negative monadic atom with
a variable argument
**********************************************************/
{
int i;
TERM Term;
for (i = clause_FirstLitIndex();
i <= clause_LastAntecedentLitIndex(Clause) && (!*Sortres || !*USortres);
i++) {
Term = clause_GetLiteralAtom(Clause,i);
if (symbol_IsBaseSort(term_TopSymbol(Term))) {
*USortres = TRUE;
if (symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))))
*Sortres = TRUE;
}
}
}
BOOL clause_ContainsFunctions(CLAUSE Clause)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the clause contains at least one function symbol
**********************************************************/
{
int i;
TERM Term;
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) {
Term = clause_GetLiteralAtom(Clause,i);
if (term_ContainsFunctions(Term))
return TRUE;
}
return FALSE;
}
BOOL clause_ContainsSymbol(CLAUSE Clause, SYMBOL Symbol)
/*********************************************************
INPUT: A clause and a symbol.
RETURNS: TRUE, if the clause contains the symbol
**********************************************************/
{
int i;
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++)
if (term_ContainsSymbol(clause_GetLiteralAtom(Clause,i), Symbol))
return TRUE;
return FALSE;
}
NAT clause_NumberOfSymbolOccurrences(CLAUSE Clause, SYMBOL Symbol)
/*********************************************************
INPUT: A clause and a symbol.
RETURNS: the number of occurrences of <Symbol> in <Clause>
**********************************************************/
{
int i;
NAT Result;
Result = 0;
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++)
Result += term_NumberOfSymbolOccurrences(clause_GetLiteralAtom(Clause,i), Symbol);
return Result;
}
BOOL clause_ImpliesFiniteDomain(CLAUSE Clause)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the clause consists of a positive disjunction
of equations, where each equation is of the form "x=t" for
some variable "x" and ground term "t"
**********************************************************/
{
int i;
TERM Term;
if (clause_FirstLitIndex() != clause_FirstSuccedentLitIndex(Clause))
return FALSE;
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) {
Term = clause_GetLiteralTerm(Clause,i);
if (!symbol_Equal(term_TopSymbol(Term),fol_Equality()) ||
(!symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))) &&
!symbol_IsVariable(term_TopSymbol(term_SecondArgument(Term)))) ||
(symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))) &&
!term_IsGround(term_SecondArgument(Term))) ||
(symbol_IsVariable(term_TopSymbol(term_SecondArgument(Term))) &&
!term_IsGround(term_FirstArgument(Term))))
return FALSE;
}
return TRUE;
}
BOOL clause_ImpliesNonTrivialDomain(CLAUSE Clause)
/*********************************************************
INPUT: A clause.
RETURNS: TRUE, if the clause consists of a negative equation
with two syntactically different arguments
**********************************************************/
{
if (clause_Length(Clause) == 1 &&
!clause_HasEmptyAntecedent(Clause) &&
clause_LiteralIsEquality(clause_FirstAntecedentLit(Clause)) &&
!term_Equal(term_FirstArgument(clause_LiteralAtom(clause_FirstAntecedentLit(Clause))),
term_SecondArgument(clause_LiteralAtom(clause_FirstAntecedentLit(Clause)))))
return TRUE;
return FALSE;
}
LIST clause_FiniteMonadicPredicates(LIST Clauses)
/*********************************************************
INPUT: A list of clauses.
RETURNS: A list of all predicate symbols that are guaranteed
to have a finite extension in any minimal Herbrand model.
These predicates must only positively occur
in unit clauses and must have a ground term argument.
**********************************************************/
{
LIST Result, NonFinite, Scan;
CLAUSE Clause;
int i, n;
SYMBOL Pred;
Result = list_Nil();
NonFinite = list_Nil();
for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) {
Clause = (CLAUSE)list_Car(Scan);
n = clause_Length(Clause);
for (i=clause_FirstSuccedentLitIndex(Clause);i<n;i++) {
Pred = term_TopSymbol(clause_GetLiteralAtom(Clause,i));
if (symbol_Arity(Pred) == 1 &&
!list_PointerMember(NonFinite, (POINTER)Pred)) {
if (term_NumberOfVarOccs(clause_GetLiteralAtom(Clause,i)) > 0 ||
n > 1) {
NonFinite = list_Cons((POINTER)Pred, NonFinite);
Result = list_PointerDeleteElement(Result, (POINTER)Pred);
}
else {
if (!list_PointerMember(Result, (POINTER)Pred))
Result = list_Cons((POINTER)Pred, Result);
}
}
}
}
list_Delete(NonFinite);
Result = list_PointerDeleteElement(Result, (POINTER)fol_Equality());
return Result;
}
NAT clause_NumberOfVarOccs(CLAUSE Clause)
/**************************************************************
INPUT: A Clause.
RETURNS: The number of variable occurrences in the clause.
***************************************************************/
{
int i,n;
NAT Result;
Result = 0;
n = clause_Length(Clause);
for (i = clause_FirstLitIndex(); i < n; i++)
Result += term_NumberOfVarOccs(clause_GetLiteralTerm(Clause,i));
return Result;
}
NAT clause_ComputeWeight(CLAUSE Clause, FLAGSTORE Flags)
/**************************************************************
INPUT: A clause and a flag store.
RETURNS: The Weight of the literals in the clause,
up to now the number of variable symbols plus
twice the number of signature symbols.
EFFECT: The weight of the literals is updated, but not the
weight of the clause!
***************************************************************/
{
int i, n;
NAT Weight;
LITERAL Lit;
Weight = 0;
n = clause_Length(Clause);
for (i = clause_FirstLitIndex(); i < n; i++) {
Lit = clause_GetLiteral(Clause, i);
clause_UpdateLiteralWeight(Lit, Flags);
Weight += clause_LiteralWeight(Lit);
}
return Weight;
}
NAT clause_ComputeTermDepth(CLAUSE Clause)
/**************************************************************
INPUT: A Clause.
RETURNS: Maximal depth of a literal in <Clause>.
***************************************************************/
{
int i,n;
NAT Depth,Help;
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_ComputeTermDepth:");
misc_ErrorReport("\n Illegal input. Input not a clause.");
misc_FinishErrorReport();
}
#endif
Depth = 0;
n = clause_Length(Clause);
for (i = clause_FirstLitIndex();i < n;i++) {
Help = term_Depth(clause_GetLiteralAtom(Clause,i));
if (Help > Depth)
Depth = Help;
}
return Depth;
}
NAT clause_MaxTermDepthClauseList(LIST Clauses)
/**************************************************************
INPUT: A list of clauses.
RETURNS: Maximal depth of a clause in <Clauses>.
***************************************************************/
{
NAT Depth,Help;
Depth = 0;
while (!list_Empty(Clauses)) {
Help = clause_ComputeTermDepth(list_Car(Clauses));
if (Help > Depth)
Depth = Help;
Clauses = list_Cdr(Clauses);
}
return Depth;
}
NAT clause_ComputeSize(CLAUSE Clause)
/**************************************************************
INPUT: A Clause.
RETURNS: The Size of the literals in the clause,
up to now the number of symbols.
***************************************************************/
{
int i,n;
NAT Size;
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_ComputeSize:");
misc_ErrorReport("\n Illegal input. Input not a clause.");
misc_FinishErrorReport();
}
#endif
Size = 0;
n = clause_Length(Clause);
for (i = clause_FirstLitIndex();i < n;i++)
Size += term_ComputeSize(clause_GetLiteralTerm(Clause,i));
return Size;
}
BOOL clause_WeightCorrect(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence)
/*********************************************************
INPUT: A clause, a flag store and a precedence.
RETURNS: TRUE iff the weight fields of the clause and its
literals are correct.
**********************************************************/
{
int i, n;
NAT Weight, Help;
LITERAL Lit;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_WeightCorrect:");
misc_ErrorReport("\n Illegal input. Input not a clause.");
misc_FinishErrorReport();
}
#endif
Weight = 0;
n = clause_Length(Clause);
for (i = clause_FirstLitIndex(); i < n; i++) {
Lit = clause_GetLiteral(Clause, i);
Help = clause_LiteralComputeWeight(Lit, Flags);
if (Help != clause_LiteralWeight(Lit))
return FALSE;
Weight += Help;
}
return (clause_Weight(Clause) == Weight);
}
LIST clause_InsertWeighed(CLAUSE Clause, LIST UsList, FLAGSTORE Flags,
PRECEDENCE Precedence)
/*********************************************************
INPUT: A clause, a list to insert the clause into,
a flag store and a precedence.
RETURNS: The list where the clause is inserted wrt its
weight (Weight(Car(list)) <= Weight(Car(Cdr(list)))).
MEMORY: A new listnode is allocated.
**********************************************************/
{
LIST Scan;
NAT Weight;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_InsertWeighted:");
misc_ErrorReport("\n Illegal input. Input not a clause.");
misc_FinishErrorReport();
}
#endif
Weight = clause_Weight(Clause);
Scan = UsList;
if (list_Empty(Scan) ||
(clause_Weight(list_Car(Scan)) > Weight)) {
return list_Cons(Clause, Scan);
} else {
while (!list_Empty(list_Cdr(Scan)) &&
(clause_Weight(list_Car(list_Cdr(Scan))) <= Weight)) {
Scan = list_Cdr(Scan);
}
list_Rplacd(Scan, list_Cons(Clause, list_Cdr(Scan)));
return UsList;
}
}
LIST clause_ListSortWeighed(LIST Clauses)
/*********************************************************
INPUT: A list of clauses.
RETURNS: The clause list sorted with respect to the weight
of clauses, minimal weight first.
EFFECT: The original list is destructively changed!
This function doesn't sort stable!
The function uses bucket sort for clauses with weight
smaller than clause_MAXWEIGHT, and the usual list sort
function for clauses with weight >= clause_MAXWEIGHT.
This implies the function uses time O(n-c + c*log c),
where n is the length of the list and c is the number
of clauses with weight >= clause_MAXWEIGHT.
For c=0 you get time O(n), for c=n you get time (n*log n).
**********************************************************/
{
int weight;
LIST Scan;
for (Scan=Clauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
weight = clause_Weight(list_Car(Scan));
if (weight < clause_MAXWEIGHT)
clause_SORT[weight] = list_Cons(list_Car(Scan),clause_SORT[weight]);
else
clause_SORT[clause_MAXWEIGHT] = list_Cons(list_Car(Scan),clause_SORT[clause_MAXWEIGHT]);
}
Scan = list_NumberSort(clause_SORT[clause_MAXWEIGHT],
(NAT (*)(POINTER)) clause_Weight);
clause_SORT[clause_MAXWEIGHT] = list_Nil();
for (weight = clause_MAXWEIGHT-1; weight >= 0; weight--) {
Scan = list_Nconc(clause_SORT[weight],Scan);
clause_SORT[weight] = list_Nil();
}
list_Delete(Clauses);
return Scan;
}
LITERAL clause_LiteralCopy(LITERAL Literal)
/*********************************************************
INPUT: A literal.
RETURNS: An unshared copy of the literal, where the owning
clause-slot is set to NULL.
MEMORY: Memory for a new LITERAL_NODE and all its TERMs
subterms is allocated.
**********************************************************/
{
LITERAL Result;
#ifdef CHECK
if (!clause_LiteralIsLiteral(Literal)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralCopy:");
misc_ErrorReport("\n Illegal input. Input not a literal.");
misc_FinishErrorReport();
}
#endif
Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE));
Result->atomWithSign = term_Copy(clause_LiteralSignedAtom(Literal));
Result->oriented = clause_LiteralIsOrientedEquality(Literal);
Result->maxLit = Literal->maxLit;
Result->weight = Literal->weight;
Result->owningClause = (POINTER)NULL;
return Result;
}
CLAUSE clause_Copy(CLAUSE Clause)
/*********************************************************
INPUT: A Clause.
RETURNS: An unshared copy of the Clause.
MEMORY: Memory for a new CLAUSE_NODE, LITERAL_NODE and
all its TERMs subterms is allocated.
**********************************************************/
{
CLAUSE Result;
int i,c,a,s,l;
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
Result->clausenumber = clause_Number(Clause);
Result->maxVar = clause_MaxVar(Clause);
Result->flags = Clause->flags;
clause_InitSplitData(Result);
Result->validlevel = clause_SplitLevel(Clause);
clause_SetSplitField(Result, Clause->splitfield, Clause->splitfield_length);
Result->depth = clause_Depth(Clause);
Result->weight = Clause->weight;
Result->parentCls = list_Copy(clause_ParentClauses(Clause));
Result->parentLits = list_Copy(clause_ParentLiterals(Clause));
Result->origin = clause_Origin(Clause);
Result->c = (c = clause_NumOfConsLits(Clause));
Result->a = (a = clause_NumOfAnteLits(Clause));
Result->s = (s = clause_NumOfSuccLits(Clause));
l = c + a + s;
if (l != 0)
Result->literals = (LITERAL *)memory_Malloc(l * sizeof(LITERAL));
for (i = 0; i < l; i++) {
clause_SetLiteral(Result, i,
clause_LiteralCopy(clause_GetLiteral(Clause, i)));
clause_LiteralSetOwningClause((Result->literals[i]), Result);
}
return Result;
}
SYMBOL clause_LiteralMaxVar(LITERAL Literal)
/*********************************************************
INPUT: A literal.
RETURNS: The maximal symbol of the literals variables,
if the literal is ground, symbol_GetInitialStandardVarCounter().
**********************************************************/
{
TERM Term;
int Bottom;
SYMBOL MaxSym,Help;
#ifdef CHECK
if (!clause_LiteralIsLiteral(Literal)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralMaxVar:");
misc_ErrorReport("\n Illegal input. Input not a literal.");
misc_FinishErrorReport();
}
#endif
Bottom = stack_Bottom();
MaxSym = symbol_GetInitialStandardVarCounter();
Term = clause_LiteralAtom(Literal);
do {
if (term_IsComplex(Term))
stack_Push(term_ArgumentList(Term));
else
if (term_IsVariable(Term))
MaxSym = ((MaxSym < (Help = term_TopSymbol(Term))) ?
Help : MaxSym);
while (!stack_Empty(Bottom) && list_Empty(stack_Top()))
stack_Pop();
if (!stack_Empty(Bottom)) {
Term = (TERM) list_Car(stack_Top());
stack_RplacTop(list_Cdr(stack_Top()));
}
} while (!stack_Empty(Bottom));
return MaxSym;
}
SYMBOL clause_AtomMaxVar(TERM Term)
/*********************************************************
INPUT: A term.
RETURNS: The maximal symbol of the lcontained variables,
if <Term> is ground, symbol_GetInitialStandardVarCounter().
**********************************************************/
{
int Bottom;
SYMBOL VarSym,Help;
Bottom = stack_Bottom();
VarSym = symbol_GetInitialStandardVarCounter();
do {
if (term_IsComplex(Term))
stack_Push(term_ArgumentList(Term));
else
if (term_IsVariable(Term))
VarSym = ((VarSym < (Help = term_TopSymbol(Term))) ?
Help : VarSym);
while (!stack_Empty(Bottom) && list_Empty(stack_Top()))
stack_Pop();
if (!stack_Empty(Bottom)) {
Term = (TERM)list_Car(stack_Top());
stack_RplacTop(list_Cdr(stack_Top()));
}
} while (!stack_Empty(Bottom));
return VarSym;
}
void clause_SetMaxLitFlags(CLAUSE Clause, FLAGSTORE FlagStore,
PRECEDENCE Precedence)
/**********************************************************
INPUT: A clause, a flag store and a precedence.
RETURNS: Nothing.
EFFECT: Sets the maxLit-flag for maximal literals.
***********************************************************/
{
int i,j,n,fa;
LITERAL ActLit,CompareLit;
BOOL Result, Twin;
ord_RESULT HelpRes;
n = clause_Length(Clause);
fa = clause_FirstAntecedentLitIndex(Clause);
clause_RemoveFlag(Clause,CLAUSESELECT);
for (i = clause_FirstLitIndex(); i < n; i++)
clause_LiteralFlagReset(clause_GetLiteral(Clause, i));
if (term_StampOverflow(clause_STAMPID))
for (i = clause_FirstLitIndex(); i < n; i++)
term_ResetTermStamp(clause_LiteralSignedAtom(clause_GetLiteral(Clause, i)));
term_StartStamp();
/*printf("\n Start: "); clause_Print(Clause);*/
for (i = fa; i < n; i++) {
ActLit = clause_GetLiteral(Clause, i);
if (!term_HasTermStamp(clause_LiteralSignedAtom(ActLit))) {
Result = TRUE;
Twin = FALSE;
for (j = fa; j < n && Result; j++)
if (i != j) {
CompareLit = clause_GetLiteral(Clause, j);
HelpRes = ord_LiteralCompare(clause_LiteralSignedAtom(ActLit),
clause_LiteralIsOrientedEquality(ActLit),
clause_LiteralSignedAtom(CompareLit),
clause_LiteralIsOrientedEquality(CompareLit),
FALSE, FlagStore, Precedence);
/*printf("\n\tWe compare: ");
fol_PrintDFG(clause_LiteralAtom(ActLit));
putchar(' ');
fol_PrintDFG(clause_LiteralAtom(CompareLit));
printf(" Result: "); ord_Print(HelpRes);*/
if (ord_IsEqual(HelpRes))
Twin = TRUE;
if (ord_IsSmallerThan(HelpRes))
Result = FALSE;
if (ord_IsGreaterThan(HelpRes))
term_SetTermStamp(clause_LiteralSignedAtom(CompareLit));
}
if (Result) {
clause_LiteralSetFlag(ActLit, MAXIMAL);
if (!Twin)
clause_LiteralSetFlag(ActLit, STRICTMAXIMAL);
}
}
}
term_StopStamp();
/*printf("\n End: "); clause_Print(Clause);*/
}
SYMBOL clause_SearchMaxVar(CLAUSE Clause)
/**********************************************************
INPUT: A clause.
RETURNS: The maximal symbol of the clauses variables.
If the clause is ground, symbol_GetInitialStandardVarCounter().
***********************************************************/
{
int i, n;
SYMBOL Help, MaxSym;
n = clause_Length(Clause);
MaxSym = symbol_GetInitialStandardVarCounter();
for (i = 0; i < n; i++) {
Help = clause_LiteralMaxVar(clause_GetLiteral(Clause, i));
if (Help > MaxSym)
MaxSym = Help;
}
return MaxSym;
}
void clause_RenameVarsBiggerThan(CLAUSE Clause, SYMBOL MinVar)
/**********************************************************
INPUT: A clause and a variable symbol.
RETURNS: The clause with variables renamed in a way, that
all vars are (excl.) bigger than MinVar.
***********************************************************/
{
int i,n;
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_RenameVarsBiggerThan:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
if (MinVar != symbol_GetInitialStandardVarCounter()) {
n = clause_Length(Clause);
term_StartMaxRenaming(MinVar);
for (i = clause_FirstLitIndex(); i < n; i++)
term_Rename(clause_GetLiteralTerm(Clause, i));
}
}
void clause_Normalize(CLAUSE Clause)
/**********************************************************
INPUT: A clause.
RETURNS: The term with normalized Variables, DESTRUCTIVE
on the variable subterms' topsymbols.
***********************************************************/
{
int i,n;
n = clause_Length(Clause);
term_StartMinRenaming();
for (i = clause_FirstLitIndex(); i < n; i++)
term_Rename(clause_GetLiteralTerm(Clause, i));
}
void clause_SubstApply(SUBST Subst, CLAUSE Clause)
/**********************************************************
INPUT: A clause.
RETURNS: Nothing.
EFFECTS: Applies the substitution to the clause.
***********************************************************/
{
int i,n;
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_SubstApply:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
n = clause_Length(Clause);
for (i=clause_FirstLitIndex(); i<n; i++)
clause_LiteralSetAtom(clause_GetLiteral(Clause, i),
subst_Apply(Subst,clause_GetLiteralAtom(Clause,i)));
}
void clause_ReplaceVariable(CLAUSE Clause, SYMBOL Var, TERM Term)
/**********************************************************
INPUT: A clause, a variable symbol, and a term.
RETURNS: Nothing.
EFFECTS: All occurences of the variable <Var> in <Clause>
are replaced by copies if <Term>.
CAUTION: The maximum variable of the clause is not updated!
***********************************************************/
{
int i, li;
#ifdef CHECK
if (!symbol_IsVariable(Var)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_ReplaceVariable: symbol is not a variable");
misc_FinishErrorReport();
}
#endif
li = clause_LastLitIndex(Clause);
for (i = clause_FirstLitIndex(); i <= li; i++)
term_ReplaceVariable(clause_GetLiteralAtom(Clause,i), Var, Term);
}
void clause_UpdateMaxVar(CLAUSE Clause)
/**********************************************************
INPUT: A clause.
RETURNS: Nothing.
EFFECTS: Actualizes the MaxVar slot wrt the actual literals.
***********************************************************/
{
clause_SetMaxVar(Clause, clause_SearchMaxVar(Clause));
}
void clause_OrientEqualities(CLAUSE Clause, FLAGSTORE FlagStore,
PRECEDENCE Precedence)
/**********************************************************
INPUT: An unshared clause, a flag store and a precedence.
RETURNS: Nothing.
EFFECTS: Reorders the arguments of equality literals
wrt. the ordering. Thus first arguments aren't smaller
after the application.
***********************************************************/
{
int i,length;
LITERAL EqLit;
ord_RESULT HelpRes;
/*printf("\n Clause: ");clause_Print(Clause);*/
length = clause_Length(Clause);
for (i = clause_FirstLitIndex(); i < length; i++) {
EqLit = clause_GetLiteral(Clause, i);
if (clause_LiteralIsEquality(EqLit)) {
HelpRes = ord_Compare(term_FirstArgument(clause_LiteralAtom(EqLit)),
term_SecondArgument(clause_LiteralAtom(EqLit)),
FlagStore, Precedence);
/*printf("\n\tWe compare: ");
fol_PrintDFG(term_FirstArgument(clause_LiteralAtom(EqLit)));
putchar(' ');
fol_PrintDFG(term_SecondArgument(clause_LiteralAtom(EqLit)));
printf("\nResult: "); ord_Print(HelpRes);*/
switch(HelpRes) {
case ord_SMALLER_THAN:
/* printf("\nSwapping: ");
term_Print(clause_LiteralAtom(EqLit)); DBG */
term_EqualitySwap(clause_LiteralAtom(EqLit));
clause_LiteralSetOrientedEquality(EqLit);
/* Swapped = TRUE; */
break;
case ord_GREATER_THAN:
clause_LiteralSetOrientedEquality(EqLit);
break;
default:
clause_LiteralSetNoOrientedEquality(EqLit);
break;
}
}
else
clause_LiteralSetNoOrientedEquality(EqLit);
}
}
void clause_InsertFlatIntoIndex(CLAUSE Clause, st_INDEX Index)
/**********************************************************
INPUT: An unshared clause and an index.
EFFECT: The atoms of <Clause> are inserted into the index.
A link from the atom to its literal via the supertermlist
is established.
***********************************************************/
{
int i,n;
LITERAL Lit;
TERM Atom ;
n = clause_Length(Clause);
for (i=clause_FirstLitIndex();i<n;i++) {
Lit = clause_GetLiteral(Clause,i);
Atom = clause_LiteralAtom(Lit);
term_RplacSupertermList(Atom, list_List(Lit));
st_EntryCreate(Index, Atom, Atom, cont_LeftContext());
}
}
void clause_DeleteFlatFromIndex(CLAUSE Clause, st_INDEX Index)
/**********************************************************
INPUT: An unshared clause and an index.
EFFECT: The clause is deleted from the index and deleted itself.
***********************************************************/
{
int i,n;
LITERAL Lit;
TERM Atom ;
n = clause_Length(Clause);
for (i=clause_FirstLitIndex();i<n;i++) {
Lit = clause_GetLiteral(Clause,i);
Atom = clause_LiteralAtom(Lit);
list_Delete(term_SupertermList(Atom));
term_RplacSupertermList(Atom, list_Nil());
st_EntryDelete(Index, Atom, Atom, cont_LeftContext());
}
clause_Delete(Clause);
}
void clause_DeleteClauseListFlatFromIndex(LIST Clauses, st_INDEX Index)
/**********************************************************
INPUT: An list of unshared clause and an index.
EFFECT: The clauses are deleted from the index and deleted itself.
The list is deleted.
***********************************************************/
{
LIST Scan;
for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan))
clause_DeleteFlatFromIndex(list_Car(Scan), Index);
list_Delete(Clauses);
}
/******************************************************************/
/* Some special functions used by hyper inference/reduction rules */
/******************************************************************/
static void clause_VarToSizeMap(SUBST Subst, NAT* Map, NAT MaxIndex)
/**************************************************************
INPUT: A substitution, an array <Map> of size <MaxIndex>+1.
RETURNS: Nothing.
EFFECT: The index i within the array corresponds to the index
of a variable x_i. For each variable x_i, 0<=i<=MaxIndex
the size of its substitution term is calculated
and written to Map[i].
***************************************************************/
{
NAT *Scan;
#ifdef CHECK
if (subst_Empty(Subst) || Map == NULL) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_VarToSizeMap: Illegal input.");
misc_FinishErrorReport();
}
#endif
/* Initialization */
for (Scan = Map + MaxIndex; Scan >= Map; Scan--)
*Scan = 1;
/* Compute the size of substitution terms */
for ( ; !subst_Empty(Subst); Subst = subst_Next(Subst))
Map[subst_Dom(Subst)] = term_ComputeSize(subst_Cod(Subst));
}
static NAT clause_ComputeTermSize(TERM Term, NAT* VarMap)
/**************************************************************
INPUT: A term and a an array of NATs.
RETURNS: The number of symbols in the term.
EFFECT: This function calculates the number of symbols in <Term>
with respect to some substitution s.
A naive way to do this is to apply the substitution
to a copy of the term, and to count the number of symbols
in the copied term.
We use a more sophisticated algorithm, that first stores
the size of every variable's substitution term in <VarMap>.
We then 'scan' the term and for a variable occurrence x_i
we simply add the corresponding value VarMap[i] to the result.
This way we avoid copying the term and the substitution terms,
which is especially useful if we reuse the VarMap several times.
***************************************************************/
{
NAT Stack, Size;
#ifdef CHECK
if (!term_IsTerm(Term)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_ComputeTermSize: Illegal input.");
misc_FinishErrorReport();
}
#endif
Size = 0;
Stack = stack_Bottom();
do {
if (VarMap!=NULL && symbol_IsVariable(term_TopSymbol(Term)))
Size += VarMap[symbol_VarIndex(term_TopSymbol(Term))];
else {
Size++;
if (term_IsComplex(Term))
stack_Push(term_ArgumentList(Term));
}
while (!stack_Empty(Stack) && list_Empty(stack_Top()))
stack_Pop();
if (!stack_Empty(Stack)) {
Term = list_Car(stack_Top());
stack_RplacTop(list_Cdr(stack_Top()));
}
} while (!stack_Empty(Stack));
return Size;
}
LIST clause_MoveBestLiteralToFront(LIST Literals, SUBST Subst, SYMBOL MaxVar,
BOOL (*Better)(LITERAL, NAT, LITERAL, NAT))
/**************************************************************
INPUT: A list of literals, a substitution, the maximum variable
from the domain of the substitution, and a comparison
function. The function <Better> will be called with two
literals L1 and L2 and two number S1 and S2, where Si is
the size of the atom of Li with respect to variable bindings
in <Subst>.
RETURNS: The same list.
EFFECT: This function moves the first literal L to the front of the
list, so that no other literal L' is better than L with respect
to the function <Better>.
The function exchanges only the literals, the order of list
items within the list is not changed.
***************************************************************/
{
NAT *Map, MapSize, BestSize, Size;
LIST Best, Scan;
#ifdef CHECK
if (!list_IsSetOfPointers(Literals)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_MoveBestLiteralToFront: List contains duplicates");
misc_FinishErrorReport();
}
#endif
if (list_Empty(Literals) || list_Empty(list_Cdr(Literals)))
/* < 2 list items, so nothing to do */
return Literals;
Map = NULL;
MapSize = 0;
if (!subst_Empty(Subst)) {
MapSize = symbol_VarIndex(MaxVar) + 1;
Map = memory_Malloc(sizeof(NAT)*MapSize);
clause_VarToSizeMap(Subst, Map, MapSize-1);
}
Best = Literals; /* Remember list item, not literal itself */
BestSize = clause_ComputeTermSize(clause_LiteralAtom(list_Car(Best)), Map);
for (Scan = list_Cdr(Literals); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
Size = clause_ComputeTermSize(clause_LiteralAtom(list_Car(Scan)), Map);
if (Better(list_Car(Scan), Size, list_Car(Best), BestSize)) {
/* Actual literal is better than the best encountered so far */
BestSize = Size;
Best = Scan;
}
}
if (Best != Literals) {
/* Move best literal to the front. We just exchange the literals. */
LITERAL h = list_Car(Literals);
list_Rplaca(Literals, list_Car(Best));
list_Rplaca(Best, h);
}
/* cleanup */
if (Map != NULL)
memory_Free(Map, sizeof(NAT)*MapSize);
return Literals;
}
/**************************************************************/
/* Literal Output Functions */
/**************************************************************/
void clause_LiteralPrint(LITERAL Literal)
/**************************************************************
INPUT: A Literal.
RETURNS: Nothing.
***************************************************************/
{
#ifdef CHECK
if (!clause_LiteralIsLiteral(Literal)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralPrint:");
misc_ErrorReport("\n Illegal input. Input not a literal.");
misc_FinishErrorReport();
}
#endif
term_PrintPrefix(clause_LiteralSignedAtom(Literal));
}
void clause_LiteralListPrint(LIST LitList)
/**************************************************************
INPUT: A list of literals.
RETURNS: Nothing.
SUMMARY: Prints the literals to stdout.
***************************************************************/
{
while (!(list_Empty(LitList))) {
clause_LiteralPrint(list_First(LitList));
LitList = list_Cdr(LitList);
if (!list_Empty(LitList))
putchar(' ');
}
}
void clause_LiteralPrintUnsigned(LITERAL Literal)
/**************************************************************
INPUT: A Literal.
RETURNS: Nothing.
SUMMARY:
***************************************************************/
{
#ifdef CHECK
if (!clause_LiteralIsLiteral(Literal)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralPrintUnsigned:");
misc_ErrorReport("\n Illegal input. Input not a literal.");
misc_FinishErrorReport();
}
#endif
term_PrintPrefix(clause_LiteralAtom(Literal));
fflush(stdout);
}
void clause_LiteralPrintSigned(LITERAL Literal)
/**************************************************************
INPUT: A Literal.
RETURNS: Nothing.
SUMMARY:
***************************************************************/
{
#ifdef CHECK
if (!clause_LiteralIsLiteral(Literal)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralPrintSigned:");
misc_ErrorReport("\n Illegal input. Input not a literal.");
misc_FinishErrorReport();
}
#endif
term_PrintPrefix(clause_LiteralSignedAtom(Literal));
fflush(stdout);
}
void clause_LiteralFPrint(FILE* File, LITERAL Lit)
/**************************************************************
INPUT: A file and a literal.
RETURNS: Nothing.
************************************************************/
{
term_FPrintPrefix(File, clause_LiteralSignedAtom(Lit));
}
LIST clause_GetLiteralSubSetList(CLAUSE Clause, int StartIndex, int EndIndex,
FLAGSTORE FlagStore, PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a start literal index, an end index, a
flag store and a precedence.
RETURNS: The list of literals between the start and the end
index.
It is a list of pointers, not a list of indices.
**************************************************************/
{
LIST Result;
int i;
#ifdef CHECK
if (!clause_IsClause(Clause, FlagStore, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
if ((StartIndex < clause_FirstLitIndex())
|| (EndIndex > clause_LastLitIndex(Clause))) {
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
misc_ErrorReport("\n Illegal input.");
misc_ErrorReport("\n Index out of range.");
misc_FinishErrorReport();
}
#endif
Result = list_Nil();
for (i=StartIndex;
i<=EndIndex;
i++) {
Result = list_Cons(clause_GetLiteral(Clause, i), Result);
}
return Result;
}
void clause_ReplaceLiteralSubSet(CLAUSE Clause, int StartIndex,
int EndIndex, LIST Replacement,
FLAGSTORE FlagStore, PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a start literal index, an end literal
index, a flag store and a precedence.
RETURNS: None.
EFFECT: Replaces the subset of literals in <Clause> with
indices between (and including) <StartIndex> and
<EndIndex> with literals from the <Replacement>
list.
**************************************************************/
{
int i;
LIST Scan;
#ifdef CHECK
if (!clause_IsClause(Clause, FlagStore, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
if ((StartIndex < clause_FirstLitIndex())
|| (EndIndex > clause_LastLitIndex(Clause))) {
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
misc_ErrorReport("\n Illegal input.");
misc_ErrorReport("\n Index out of range.");
misc_FinishErrorReport();
}
if (list_Length(Replacement) != (EndIndex - StartIndex + 1)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
misc_ErrorReport("\n Illegal input. Replacement list size");
misc_ErrorReport("\n and set size don't match");
misc_FinishErrorReport();
}
#endif
for (i = StartIndex, Scan = Replacement;
i <= EndIndex;
i++, Scan = list_Cdr(Scan)) {
clause_SetLiteral(Clause, i, list_Car(Scan));
}
}
static __inline__ BOOL clause_LiteralsCompare(LITERAL Left, LITERAL Right)
/**************************************************************
INPUT: Two literals.
RETURNS: TRUE if Left <= Right, FALSE otherwise.
EFFECT: Compares literals by comparing their terms' arities.
***************************************************************/
{
#ifdef CHECK
if (!(clause_LiteralIsLiteral(Left) && clause_LiteralIsLiteral(Right))) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_LiteralsCompare:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
return term_CompareAbstractLEQ(clause_LiteralSignedAtom(Left),
clause_LiteralSignedAtom(Right));
}
static __inline__ void clause_FixLiteralSubsetOrder(CLAUSE Clause,
int StartIndex,
int EndIndex,
FLAGSTORE FlagStore,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a start index, an end index a flag store
and a precedence.
RETURNS: None.
EFFECT: Sorts literals with indices between (and including)
<StartIndex> and <EndIndex> with respect to an abstract
list representation of terms that identifies function
symbols with their arity.
***************************************************************/
{
LIST literals;
#ifdef CHECK
if ((StartIndex < clause_FirstLitIndex())
|| (EndIndex > clause_LastLitIndex(Clause))) {
misc_ErrorReport("\n In clause_FixLiteralSubSetOrder:");
misc_ErrorReport("\n Illegal input.");
misc_ErrorReport("\n Index out of range.");
misc_FinishErrorReport();
}
#endif
/* Get the literals */
literals = clause_GetLiteralSubSetList(Clause, StartIndex, EndIndex, FlagStore, Precedence);
/* Sort them */
literals = list_Sort(literals, (BOOL (*) (POINTER, POINTER)) clause_LiteralsCompare);
/* Replace clause literals in subset with sorted literals */
clause_ReplaceLiteralSubSet(Clause, StartIndex, EndIndex, literals, FlagStore, Precedence);
list_Delete(literals);
}
void clause_FixLiteralOrder(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a flag store, and a precedence.
RETURNS: None.
EFFECT: Fixes literal order in a <Clause>. Different literal
types are ordered separately.
***************************************************************/
{
#ifdef CHECK
if (!clause_IsClause(Clause, FlagStore, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_FixLiteralOrder:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
/* Fix antecedent literal order */
clause_FixLiteralSubsetOrder(Clause,
clause_FirstAntecedentLitIndex(Clause),
clause_LastAntecedentLitIndex(Clause),
FlagStore, Precedence);
/* Fix succedent literal order */
clause_FixLiteralSubsetOrder(Clause,
clause_FirstSuccedentLitIndex(Clause),
clause_LastSuccedentLitIndex(Clause),
FlagStore, Precedence);
/* Fix constraint literal order */
clause_FixLiteralSubsetOrder(Clause,
clause_FirstConstraintLitIndex(Clause),
clause_LastConstraintLitIndex(Clause),
FlagStore, Precedence);
/* Normalize clause, to get variable names right. */
clause_Normalize(Clause);
}
static int clause_CompareByWeight(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by their weight.
***************************************************************/
{
NAT lweight, rweight;
int result;
lweight = clause_Weight(Left);
rweight = clause_Weight(Right);
if (lweight < rweight) {
result = -1;
}
else if (lweight > rweight) {
result = 1;
}
else {
result = 0;
}
return result;
}
static int clause_CompareByClausePartSize(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by the number of literals in
the antecedent, succedent and constraint.
***************************************************************/
{
int lsize, rsize;
lsize = clause_NumOfAnteLits(Left);
rsize = clause_NumOfAnteLits(Right);
if (lsize < rsize)
return -1;
else if (lsize > rsize)
return 1;
lsize = clause_NumOfSuccLits(Left);
rsize = clause_NumOfSuccLits(Right);
if (lsize < rsize)
return -1;
else if (lsize > rsize)
return 1;
lsize = clause_NumOfConsLits(Left);
rsize = clause_NumOfConsLits(Right);
if (lsize < rsize)
return -1;
else if (lsize > rsize)
return 1;
return 0;
}
void clause_CountSymbols(CLAUSE Clause)
/**************************************************************
INPUT: A clause.
RETURNS: None.
EFFECT: Counts the non-variable symbols in the clause, and
increases their counts accordingly.
***************************************************************/
{
int i;
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
LITERAL l;
TERM t;
l = clause_GetLiteral(Clause, i);
if (clause_LiteralIsPredicate(l)) {
SYMBOL S;
S = clause_LiteralPredicate(l);
symbol_SetCount(S, symbol_GetCount(S) + 1);
}
t = clause_GetLiteralAtom(Clause, i);
term_CountSymbols(t);
}
}
LIST clause_ListOfPredicates(CLAUSE Clause)
/**************************************************************
INPUT: A clause.
RETURNS: A list of symbols.
EFFECT: Creates a list of predicates occurring in the clause.
A predicate occurs several times in the list, if
it does so in the clause.
***************************************************************/
{
LIST preds;
int i;
preds = list_Nil();
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
LITERAL l;
l = clause_GetLiteral(Clause, i);
if (clause_LiteralIsPredicate(l)) {
preds = list_Cons((POINTER) clause_LiteralPredicate(l), preds);
}
}
return preds;
}
LIST clause_ListOfConstants(CLAUSE Clause)
/**************************************************************
INPUT: A clause.
RETURNS: A list of symbols.
EFFECT: Creates a list of constants occurring in the clause.
A constant occurs several times in the list, if
it does so in the clause.
***************************************************************/
{
LIST consts;
int i;
consts = list_Nil();
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
TERM t;
t = clause_GetLiteralAtom(Clause, i);
consts = list_Nconc(term_ListOfConstants(t), consts);
}
return consts;
}
LIST clause_ListOfVariables(CLAUSE Clause)
/**************************************************************
INPUT: A clause.
RETURNS: A list of variables.
EFFECT: Creates a list of variables occurring in the clause.
A variable occurs several times in the list, if
it does so in the clause.
***************************************************************/
{
LIST vars;
int i;
vars = list_Nil();
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
TERM t;
t = clause_GetLiteralAtom(Clause, i);
vars = list_Nconc(term_ListOfVariables(t), vars);
}
return vars;
}
LIST clause_ListOfFunctions(CLAUSE Clause)
/**************************************************************
INPUT: A clause.
RETURNS: A list of symbols.
EFFECT: Creates a list of functions occurring in the clause.
A function occurs several times in the list, if
it does so in the clause.
***************************************************************/
{
LIST funs;
int i;
funs = list_Nil();
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
TERM t;
t = clause_GetLiteralAtom(Clause, i);
funs = list_Nconc(term_ListOfFunctions(t), funs);
}
return funs;
}
static int clause_CompareByPredicateDistribution(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by the frequency of predicates.
***************************************************************/
{
LIST lpreds, rpreds;
int result;
lpreds = clause_ListOfPredicates(Left);
rpreds = clause_ListOfPredicates(Right);
result = list_CompareMultisetsByElementDistribution(lpreds, rpreds);
list_Delete(lpreds);
list_Delete(rpreds);
return result;
}
static int clause_CompareByConstantDistribution(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by the frequency of constants.
***************************************************************/
{
LIST lconsts, rconsts;
int result;
lconsts = clause_ListOfConstants(Left);
rconsts = clause_ListOfConstants(Right);
result = list_CompareMultisetsByElementDistribution(lconsts, rconsts);
list_Delete(lconsts);
list_Delete(rconsts);
return result;
}
static int clause_CompareByVariableDistribution(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by the frequency of variables.
***************************************************************/
{
LIST lvars, rvars;
int result;
lvars = clause_ListOfVariables(Left);
rvars = clause_ListOfVariables(Right);
result = list_CompareMultisetsByElementDistribution(lvars, rvars);
list_Delete(lvars);
list_Delete(rvars);
return result;
}
static int clause_CompareByFunctionDistribution(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by the frequency of functions.
***************************************************************/
{
LIST lfuns, rfuns;
int result;
lfuns = clause_ListOfFunctions(Left);
rfuns = clause_ListOfFunctions(Right);
result = list_CompareMultisetsByElementDistribution(lfuns, rfuns);
list_Delete(lfuns);
list_Delete(rfuns);
return result;
}
static int clause_CompareByDepth(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by their depth.
***************************************************************/
{
if (clause_Depth(Left) < clause_Depth(Right))
return -1;
else if (clause_Depth(Left) > clause_Depth(Right))
return 1;
return 0;
}
static int clause_CompareByMaxVar(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by their maximal variable.
***************************************************************/
{
if (clause_MaxVar(Left) < clause_MaxVar(Right))
return -1;
else if (clause_MaxVar(Left) > clause_MaxVar(Right))
return 1;
return 0;
}
static int clause_CompareByLiterals(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by comparing their literals
from left to right.
***************************************************************/
{
int firstlitleft, lastlitleft;
int firstlitright, lastlitright;
int i, j;
int result;
result = 0;
/* Compare sorted literals from right to left */
firstlitleft = clause_FirstLitIndex();
lastlitleft = clause_LastLitIndex(Left);
firstlitright = clause_FirstLitIndex();
lastlitright = clause_LastLitIndex(Right);
for (i = lastlitleft, j = lastlitright;
i >= firstlitleft && j >= firstlitright;
--i, --j) {
TERM lterm, rterm;
lterm = clause_GetLiteralTerm(Left, i);
rterm = clause_GetLiteralTerm(Right, j);
result = term_CompareAbstract(lterm, rterm);
if (result != 0)
break;
}
if (result == 0) {
/* All literals compared equal, so check if someone has
uncompared literals left over.
*/
if ( i > j) {
/* Left clause has uncompared literals left over. */
result = 1;
}
else if (i < j) {
/* Right clause has uncompared literals left over. */
result = -1;
}
}
return result;
}
static int clause_CompareBySymbolOccurences(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by comparing the occurrences of
symbols in their respective literals from left to
right. If a symbol occurs less frequently than
its positional equivalent in the other clause,
then the first clause is smaller.
***************************************************************/
{
int firstlitleft, lastlitleft;
int firstlitright, lastlitright;
int i, j;
int result;
result = 0;
/* Compare sorted literals from right to left */
firstlitleft = clause_FirstLitIndex();
lastlitleft = clause_LastLitIndex(Left);
firstlitright = clause_FirstLitIndex();
lastlitright = clause_LastLitIndex(Right);
for (i = lastlitleft, j = lastlitright;
i >= firstlitleft && j >= firstlitright;
--i, --j) {
TERM lterm, rterm;
LITERAL llit, rlit;
llit = clause_GetLiteral(Left, i);
rlit = clause_GetLiteral(Right, j);
if (clause_LiteralIsPredicate(llit)) {
if (clause_LiteralIsPredicate(rlit)) {
if (symbol_GetCount(clause_LiteralPredicate(llit))
< symbol_GetCount(clause_LiteralPredicate(rlit))) {
return -1;
}
else if (symbol_GetCount(clause_LiteralPredicate(llit))
> symbol_GetCount(clause_LiteralPredicate(rlit))) {
return 1;
}
}
}
lterm = clause_GetLiteralTerm(Left, i);
rterm = clause_GetLiteralTerm(Right, j);
result = term_CompareBySymbolOccurences(lterm, rterm);
if (result != 0)
break;
}
return result;
}
int clause_CompareAbstract(CLAUSE Left, CLAUSE Right)
/**************************************************************
INPUT: Two clauses.
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
EFFECT: Compares two clauses by their weight. If the weight
is equal, it compares the clauses by the arity of
their literals from right to left.
CAUTION: Expects clause literal order to be fixed.
***************************************************************/
{
typedef int (*CLAUSE_COMPARE_FUNCTION) (CLAUSE, CLAUSE);
static const CLAUSE_COMPARE_FUNCTION clause_compare_functions [] = {
clause_CompareByWeight,
clause_CompareByDepth,
clause_CompareByMaxVar,
clause_CompareByClausePartSize,
clause_CompareByLiterals,
clause_CompareBySymbolOccurences,
clause_CompareByPredicateDistribution,
clause_CompareByConstantDistribution,
clause_CompareByFunctionDistribution,
clause_CompareByVariableDistribution,
};
int result;
int i;
int functions;
result = 0;
functions = sizeof(clause_compare_functions)/sizeof(CLAUSE_COMPARE_FUNCTION);
for (i = 0; i < functions; i++) {
result = clause_compare_functions[i](Left, Right);
if ( result != 0) {
return result;
}
}
return 0;
}
/**************************************************************/
/* Clause functions */
/**************************************************************/
void clause_Init(void)
/**************************************************************
INPUT: None.
RETURNS: Nothing.
SUMMARY: Initializes the clause counter and other variables
from this module.
***************************************************************/
{
int i;
clause_SetCounter(1);
clause_STAMPID = term_GetStampID();
for (i = 0; i <= clause_MAXWEIGHT; i++)
clause_SORT[i] = list_Nil();
}
CLAUSE clause_CreateBody(int ClauseLength)
/**************************************************************
INPUT: The number of literals as integer.
RETURNS: A new generated clause node for 'ClauseLength'
MEMORY: Allocates a CLAUSE_NODE and the needed array for LITERALs.
*************************************************************/
{
CLAUSE Result;
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
Result->clausenumber = clause_IncreaseCounter();
Result->maxVar = symbol_GetInitialStandardVarCounter();
Result->flags = 0;
Result->depth = 0;
clause_InitSplitData(Result);
Result->weight = clause_WEIGHTUNDEFINED;
Result->parentCls = list_Nil();
Result->parentLits = list_Nil();
Result->c = 0;
Result->a = 0;
Result->s = 0;
if (ClauseLength != 0)
Result->literals =
(LITERAL *)memory_Malloc((ClauseLength) * sizeof(LITERAL));
clause_SetFromInput(Result);
return Result;
}
CLAUSE clause_Create(LIST Constraint, LIST Antecedent, LIST Succedent,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: Three lists of pointers to atoms, a flag store and
a precedence.
RETURNS: The new generated clause.
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
uses the terms from the lists, additionally allocates
termnodes for the fol_Not() in Const. and Ante.
*************************************************************/
{
CLAUSE Result;
int i, c, a, s;
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
Result->clausenumber = clause_IncreaseCounter();
Result->flags = 0;
Result->depth = 0;
Result->weight = clause_WEIGHTUNDEFINED;
clause_InitSplitData(Result);
Result->parentCls = list_Nil();
Result->parentLits = list_Nil();
Result->c = (c = list_Length(Constraint));
Result->a = (a = list_Length(Antecedent));
Result->s = (s = list_Length(Succedent));
if (!clause_IsEmptyClause(Result))
Result->literals =
(LITERAL *) memory_Malloc((c+a+s) * sizeof(LITERAL));
for (i = 0; i < c; i++) {
Result->literals[i] =
clause_LiteralCreate(term_Create(fol_Not(),
list_List((TERM)list_Car(Constraint))),Result);
Constraint = list_Cdr(Constraint);
}
a += c;
for ( ; i < a; i++) {
Result->literals[i] =
clause_LiteralCreate(term_Create(fol_Not(),
list_List((TERM)list_Car(Antecedent))), Result);
Antecedent = list_Cdr(Antecedent);
}
s += a;
for ( ; i < s; i++) {
Result->literals[i] =
clause_LiteralCreate((TERM) list_Car(Succedent), Result);
Succedent = list_Cdr(Succedent);
}
clause_OrientAndReInit(Result, Flags, Precedence);
clause_SetFromInput(Result);
return Result;
}
CLAUSE clause_CreateCrude(LIST Constraint, LIST Antecedent, LIST Succedent,
BOOL Con)
/**************************************************************
INPUT: Three lists of pointers to literals (!) and a Flag indicating
whether the clause comes from the conjecture part of of problem.
It is assumed that Constraint and Antecedent literals are negative,
whereas Succedent literals are positive.
RETURNS: The new generated clause, where a clause_OrientAndReInit has still
to be performed, i.e., variables are not normalized, maximal literal
flags not set, equations not oriented, the weight is not set.
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
uses the terms from the lists, additionally allocates
termnodes for the fol_Not() in Const. and Ante.
****************************************************************/
{
CLAUSE Result;
int i,c,a,s;
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
Result->clausenumber = clause_IncreaseCounter();
Result->flags = 0;
if (Con)
clause_SetFlag(Result, CONCLAUSE);
Result->depth = 0;
Result->weight = clause_WEIGHTUNDEFINED;
clause_InitSplitData(Result);
Result->parentCls = list_Nil();
Result->parentLits = list_Nil();
Result->c = (c = list_Length(Constraint));
Result->a = (a = list_Length(Antecedent));
Result->s = (s = list_Length(Succedent));
if (!clause_IsEmptyClause(Result))
Result->literals = (LITERAL *)memory_Malloc((c+a+s) * sizeof(LITERAL));
for (i = 0; i < c; i++) {
Result->literals[i] =
clause_LiteralCreate(list_Car(Constraint),Result);
Constraint = list_Cdr(Constraint);
}
a += c;
for ( ; i < a; i++) {
Result->literals[i] =
clause_LiteralCreate(list_Car(Antecedent), Result);
Antecedent = list_Cdr(Antecedent);
}
s += a;
for ( ; i < s; i++) {
Result->literals[i] = clause_LiteralCreate(list_Car(Succedent), Result);
Succedent = list_Cdr(Succedent);
}
clause_SetFromInput(Result);
return Result;
}
CLAUSE clause_CreateUnnormalized(LIST Constraint, LIST Antecedent,
LIST Succedent)
/**************************************************************
INPUT: Three lists of pointers to atoms.
RETURNS: The new generated clause.
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
uses the terms from the lists, additionally allocates
termnodes for the fol_Not() in Const. and Ante.
CAUTION: The weight of the clause is not set correctly and
equations are not oriented!
****************************************************************/
{
CLAUSE Result;
int i,c,a,s;
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
Result->clausenumber = clause_IncreaseCounter();
Result->flags = 0;
Result->depth = 0;
Result->weight = clause_WEIGHTUNDEFINED;
clause_InitSplitData(Result);
Result->parentCls = list_Nil();
Result->parentLits = list_Nil();
Result->c = (c = list_Length(Constraint));
Result->a = (a = list_Length(Antecedent));
Result->s = (s = list_Length(Succedent));
if (!clause_IsEmptyClause(Result)) {
Result->literals = (LITERAL *)memory_Malloc((c+a+s) * sizeof(LITERAL));
for (i = 0; i < c; i++) {
Result->literals[i] =
clause_LiteralCreate(term_Create(fol_Not(),
list_List(list_Car(Constraint))),
Result);
Constraint = list_Cdr(Constraint);
}
a += c;
for ( ; i < a; i++) {
Result->literals[i] =
clause_LiteralCreate(term_Create(fol_Not(),
list_List(list_Car(Antecedent))),
Result);
Antecedent = list_Cdr(Antecedent);
}
s += a;
for ( ; i < s; i++) {
Result->literals[i] =
clause_LiteralCreate((TERM)list_Car(Succedent), Result);
Succedent = list_Cdr(Succedent);
}
clause_UpdateMaxVar(Result);
}
return Result;
}
CLAUSE clause_CreateFromLiterals(LIST LitList, BOOL Sorts, BOOL Conclause,
BOOL Ordering, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A list of literals, three boolean flags indicating whether
sort constraint literals should be generated, whether the
clause is a conjecture clause, whether the ordering information
should be established, a flag store and a precedence.
RETURNS: The new generated clause.
EFFECT: The result clause will be normalized and the maximal
variable will be set. If <Ordering> is FALSE no additional
initializations will be done. This mode is intended for
the parser for creating clauses at a time when the ordering
and weight flags aren't determined finally.
Only if <Ordering> is TRUE the equations will be oriented,
the maximal literals will be marked and the clause weight
will be set correctly.
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
uses the terms from the lists.
****************************************************************/
{
CLAUSE Result;
LIST Antecedent,Succedent,Constraint;
TERM Atom;
Antecedent = list_Nil();
Succedent = list_Nil();
Constraint = list_Nil();
while (!list_Empty(LitList)) {
if (term_TopSymbol(list_Car(LitList)) == fol_Not()) {
Atom = term_FirstArgument(list_Car(LitList));
if (Sorts && symbol_IsBaseSort(term_TopSymbol(Atom)) && term_IsVariable(term_FirstArgument(Atom)))
Constraint = list_Cons(list_Car(LitList),Constraint);
else
Antecedent = list_Cons(list_Car(LitList),Antecedent);
}
else
Succedent = list_Cons(list_Car(LitList),Succedent);
LitList = list_Cdr(LitList);
}
Constraint = list_NReverse(Constraint);
Antecedent = list_NReverse(Antecedent);
Succedent = list_NReverse(Succedent);
Result = clause_CreateCrude(Constraint, Antecedent, Succedent, Conclause);
list_Delete(Constraint);
list_Delete(Antecedent);
list_Delete(Succedent);
if (Ordering)
clause_OrientAndReInit(Result, Flags, Precedence);
else {
clause_Normalize(Result);
clause_UpdateMaxVar(Result);
}
return Result;
}
void clause_SetSortConstraint(CLAUSE Clause, BOOL Strong, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A clause, a flag indicating whether also negative
monadic literals with a real term argument should be
put in the sort constraint, a flag store and a precedence.
RETURNS: Nothing.
EFFECT: Negative monadic literals are put in the sort constraint.
****************************************************************/
{
LITERAL ActLit,Help;
TERM ActAtom;
int i,k,NewConLits;
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_SetSortConstraint:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
i = clause_LastConstraintLitIndex(Clause);
NewConLits = 0;
for (k=clause_FirstAntecedentLitIndex(Clause);k<=clause_LastAntecedentLitIndex(Clause);k++) {
ActLit = clause_GetLiteral(Clause,k);
ActAtom = clause_LiteralAtom(ActLit);
if (symbol_IsBaseSort(term_TopSymbol(ActAtom)) &&
(Strong || term_IsVariable(term_FirstArgument(ActAtom)))) {
if (++i != k) {
Help = clause_GetLiteral(Clause,i);
clause_SetLiteral(Clause,i,ActLit);
clause_SetLiteral(Clause,k,Help);
}
NewConLits++;
}
}
clause_SetNumOfConsLits(Clause, clause_NumOfConsLits(Clause) + NewConLits);
clause_SetNumOfAnteLits(Clause, clause_NumOfAnteLits(Clause) - NewConLits);
clause_ReInit(Clause, Flags, Precedence);
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_SetSortConstraint:");
misc_ErrorReport("\n Illegal computations.");
misc_FinishErrorReport();
}
#endif
}
void clause_Delete(CLAUSE Clause)
/**************************************************************
INPUT: A Clause.
RETURNS: Nothing.
MEMORY: Frees the memory of the clause.
***************************************************************/
{
int i, n;
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) { /* Clause may be a byproduct of some hyper rule */
misc_StartErrorReport();
misc_ErrorReport("\n In clause_Delete:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
n = clause_Length(Clause);
for (i = 0; i < n; i++)
clause_LiteralDelete(clause_GetLiteral(Clause,i));
clause_FreeLitArray(Clause);
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
#ifdef CHECK
if ((Clause->splitfield != NULL) && (Clause->splitfield_length == 0))
{
misc_StartErrorReport();
misc_ErrorReport("\n In clause_Delete:");
misc_ErrorReport("\n Illegal splitfield_length.");
misc_FinishErrorReport();
}
if ((Clause->splitfield == NULL) && (Clause->splitfield_length != 0))
{
misc_StartErrorReport();
misc_ErrorReport("\n In clause_Delete:");
misc_ErrorReport("\n Illegal splitfield.");
misc_FinishErrorReport();
}
#endif
if (Clause->splitfield != NULL) {
memory_Free(Clause->splitfield,
sizeof(SPLITFIELDENTRY) * Clause->splitfield_length);
}
clause_Free(Clause);
}
/**************************************************************/
/* Functions to use the sharing for clauses. */
/**************************************************************/
void clause_InsertIntoSharing(CLAUSE Clause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: A Clause, an index, a flag store and a precedence.
RETURNS: Nothing.
SUMMARY: Inserts the unsigned atoms of 'Clause' into the sharing index.
***************************************************************/
{
int i, litnum;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_Delete:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
clause_Check(Clause, Flags, Precedence);
#endif
litnum = clause_Length(Clause);
for (i = 0; i < litnum; i++) {
clause_LiteralInsertIntoSharing(clause_GetLiteral(Clause,i), ShIndex);
}
}
void clause_DeleteFromSharing(CLAUSE Clause, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: A Clause, an Index, a flag store and a precedence.
RETURNS: Nothing.
SUMMARY: Deletes 'Clause' and all its literals from the sharing,
frees the memory of 'Clause'.
***************************************************************/
{
int i, length;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_DeleteFromSharing:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
length = clause_Length(Clause);
for (i = 0; i < length; i++)
clause_LiteralDeleteFromSharing(clause_GetLiteral(Clause,i),ShIndex);
clause_FreeLitArray(Clause);
list_Delete(clause_ParentClauses(Clause));
list_Delete(clause_ParentLiterals(Clause));
#ifdef CHECK
if ((Clause->splitfield != NULL) && (Clause->splitfield_length == 0))
{
misc_StartErrorReport();
misc_ErrorReport("\n In clause_DeleteFromSharing:");
misc_ErrorReport("\n Illegal splitfield_length.");
misc_FinishErrorReport();
}
if ((Clause->splitfield == NULL) && (Clause->splitfield_length != 0))
{
misc_StartErrorReport();
misc_ErrorReport("\n In clause_DeleteFromSharing:");
misc_ErrorReport("\n Illegal splitfield.");
misc_FinishErrorReport();
}
#endif
if (Clause->splitfield != NULL) {
memory_Free(Clause->splitfield,
sizeof(SPLITFIELDENTRY) * Clause->splitfield_length);
}
clause_Free(Clause);
}
void clause_MakeUnshared(CLAUSE Clause, SHARED_INDEX ShIndex)
/**************************************************************
INPUT: A Clause and an Index.
RETURNS: Nothing.
SUMMARY: Deletes the clauses literals from the sharing and
replaces them by unshared copies.
***************************************************************/
{
LITERAL ActLit;
TERM SharedAtom, AtomCopy;
int i,LastAnte,length;
#ifdef CHECK
if (!clause_IsUnorderedClause(Clause)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_MakeUnshared:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
LastAnte = clause_LastAntecedentLitIndex(Clause);
length = clause_Length(Clause);
for (i = clause_FirstLitIndex(); i <= LastAnte; i++) {
ActLit = clause_GetLiteral(Clause, i);
SharedAtom = clause_LiteralAtom(ActLit);
AtomCopy = term_Copy(SharedAtom);
sharing_Delete(ActLit, SharedAtom, ShIndex);
clause_LiteralSetNegAtom(ActLit, AtomCopy);
}
for ( ; i < length; i++) {
ActLit = clause_GetLiteral(Clause, i);
SharedAtom = clause_LiteralSignedAtom(ActLit);
AtomCopy = term_Copy(SharedAtom);
sharing_Delete(ActLit, SharedAtom, ShIndex);
clause_LiteralSetPosAtom(ActLit, AtomCopy);
}
}
void clause_MoveSharedClause(CLAUSE Clause, SHARED_INDEX Source,
SHARED_INDEX Destination, FLAGSTORE Flags,
PRECEDENCE Precedence)
/**************************************************************
INPUT: A Clause, two indexes, a flag store, and a precedence.
RETURNS: Nothing.
EFFECT: Deletes <Clause> from <Source> and inserts it into
<Destination>.
***************************************************************/
{
LITERAL Lit;
TERM Atom,Copy;
int i,length;
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_MoveSharedClause:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
length = clause_Length(Clause);
for (i = clause_FirstLitIndex(); i < length; i++) {
Lit = clause_GetLiteral(Clause, i);
Atom = clause_LiteralAtom(Lit);
Copy = term_Copy(Atom); /* sharing_Insert works destructively on <Copy>'s superterms */
clause_LiteralSetAtom(Lit, sharing_Insert(Lit, Copy, Destination));
sharing_Delete(Lit, Atom, Source);
term_Delete(Copy);
}
}
void clause_DeleteSharedLiteral(CLAUSE Clause, int Indice, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: A Clause, a literals indice, an Index, a flag store
and a precedence.
RETURNS: Nothing.
SUMMARY: Deletes the shared literal from the clause.
MEMORY: Various.
***************************************************************/
{
#ifdef CHECK
if (!clause_IsClause(Clause, Flags, Precedence)) {
misc_StartErrorReport();
misc_ErrorReport("\n In clause_DeleteSharedLiteral:");
misc_ErrorReport("\n Illegal input.");
misc_FinishErrorReport();
}
#endif
clause_MakeUnshared(Clause, ShIndex);
clause_DeleteLiteral(Clause, Indice, Flags, Precedence);
clause_InsertIntoSharing(Clause, ShIndex, Flags, Precedence);
}
void clause_DeleteClauseList(LIST ClauseList)
/**************************************************************
INPUT: A list of unshared clauses.
RETURNS: Nothing.
SUMMARY: Deletes all clauses in the list and the list.
MEMORY: Frees the lists and the clauses' memory.
***************************************************************/
{
LIST Scan;
for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan))
if (clause_Exists(list_Car(Scan)))
clause_Delete(list_Car(Scan));
list_Delete(ClauseList);
}
void clause_DeleteSharedClauseList(LIST ClauseList, SHARED_INDEX ShIndex,
FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************
INPUT: A list of clauses, an index, a flag store and
a precedence.
RETURNS: Nothing.
SUMMARY: Deletes all clauses in the list from the sharing.
MEMORY: Frees the lists and the clauses' memory.
***************************************************************/
{
LIST Scan;
for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan))