« back to all changes in this revision
Viewing changes to SPASS/clause.c
- browse files at revision 4
- compare with another revision
- compare with revision 1
- download diff
- download tarball
- view history from revision 4
- Committer: Bazaar Package Importer
- Author(s): Roland Stigge
- Date: 2010-06-27 18:59:28 UTC
- mfrom: (1.1.1 upstream)
- Revision ID: james.westby@ubuntu.com-20100627185928-kdjuqghv04rxyqmc
Tags: 3.7-1
New upstream release
- files added:
- .pc
- .pc/debian-changes-3.7-1
- .pc/debian-changes-3.7-1/doc
- .pc/debian-changes-3.7-1/doc/man
- .pc/debian-changes-3.7-1/doc/texinfo
- SPASS
- debian/patches
- debian/source
- doc
- doc/handbook
- doc/html
- doc/man
- doc/syntax
- doc/texinfo
- doc/tutorial
- examples
- lib
- m4
- scripts
- files removed:
- debian/SPASS.1
- files modified:
- debian/changelog
added
removed
SPASS/clause.c
1
/**************************************************************/
2
/* ********************************************************** */
3
/* * * */
4
/* * CLAUSES * */
5
/* * * */
6
/* * $Module: CLAUSE * */
7
/* * * */
8
/* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */
9
/* * MPI fuer Informatik * */
10
/* * * */
11
/* * This program is free software; you can redistribute * */
12
/* * it and/or modify it under the terms of the FreeBSD * */
13
/* * Licence. * */
14
/* * * */
15
/* * This program is distributed in the hope that it will * */
16
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
17
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
18
/* * FOR A PARTICULAR PURPOSE. See the LICENCE file * */
19
/* * for more details. * */
20
/* * * */
21
/* * * */
22
/* $Revision: 1.15 $ * */
23
/* $State: Exp $ * */
24
/* $Date: 2010-02-22 14:09:57 $ * */
25
/* $Author: weidenb $ * */
26
/* * * */
27
/* * Contact: * */
28
/* * Christoph Weidenbach * */
29
/* * MPI fuer Informatik * */
30
/* * Stuhlsatzenhausweg 85 * */
31
/* * 66123 Saarbruecken * */
32
/* * Email: spass@mpi-inf.mpg.de * */
33
/* * Germany * */
34
/* * * */
35
/* ********************************************************** */
36
/**************************************************************/
37
38
39
/* $RCSfile: clause.c,v $ */
40
41
#include "clause.h"
42
43
/**************************************************************/
44
/* Global variables and constants */
45
/**************************************************************/
46
47
/* Means weight of literal or clause is undefined */
48
const NAT clause_WEIGHTUNDEFINED = NAT_MAX;
49
50
int clause_CLAUSECOUNTER;
51
NAT clause_STAMPID;
52
53
/* The following array is used for bucket sort on clauses */
54
#define clause_MAXWEIGHT 20
55
LIST clause_SORT[clause_MAXWEIGHT+1];
56
57
/**************************************************************/
58
/* Inline functions */
59
/**************************************************************/
60
61
static __inline__ void clause_FreeLitArray(CLAUSE Clause)
62
{
63
NAT Length = clause_Length(Clause);
64
if (Length > 0)
65
memory_Free(Clause->literals, sizeof(LITERAL) * Length);
66
}
67
68
69
/**************************************************************/
70
/* Primitive literal functions */
71
/**************************************************************/
72
73
BOOL clause_LiteralIsLiteral(LITERAL Literal)
74
/*********************************************************
75
INPUT: A literal.
76
RETURNS: TRUE, if 'Literal' is not NULL and has a predicate
77
symbol as its atoms top symbol.
78
**********************************************************/
79
{
80
return ((Literal != NULL) &&
81
symbol_IsPredicate(clause_LiteralPredicate(Literal)));
82
}
83
84
NAT clause_LiteralComputeWeight(LITERAL Literal, FLAGSTORE Flags)
85
/*********************************************************
86
INPUT: A literal and a flag store.
87
RETURNS: The weight of the literal.
88
CAUTION: This function does not update the weight of the literal!
89
**********************************************************/
90
{
91
TERM Term;
92
int Bottom;
93
NAT Number;
94
95
#ifdef CHECK
96
if (!clause_LiteralIsLiteral(Literal)) {
97
misc_StartErrorReport();
98
misc_ErrorReport("\n In clause_LiteralComputeWeight :");
99
misc_ErrorReport("Illegal Input. Input not a literal.");
100
misc_FinishErrorReport();
101
}
102
#endif
103
104
Term = clause_LiteralSignedAtom(Literal);
105
Bottom = stack_Bottom();
106
Number = 0;
107
108
do {
109
if (term_IsComplex(Term)) {
110
Number += flag_GetFlagIntValue(Flags, flag_FUNCWEIGHT);
111
stack_Push(term_ArgumentList(Term));
112
}
113
else
114
if (term_IsVariable(Term))
115
Number += flag_GetFlagIntValue(Flags, flag_VARWEIGHT);
116
else
117
Number += flag_GetFlagIntValue(Flags, flag_FUNCWEIGHT);
118
119
while (!stack_Empty(Bottom) && list_Empty(stack_Top()))
120
stack_Pop();
121
if (!stack_Empty(Bottom)) {
122
Term = (TERM) list_Car(stack_Top());
123
stack_RplacTop(list_Cdr(stack_Top()));
124
}
125
} while (!stack_Empty(Bottom));
126
127
return Number;
128
129
}
130
131
LITERAL clause_LiteralCreate(TERM Atom, CLAUSE Clause)
132
/**********************************************************
133
INPUT: A Pointer to a signed Predicate-Term and one to a
134
clause it shall belong to.
135
RETURNS: An appropriate literal where the other values
136
are set to default values.
137
MEMORY: A LITERAL_NODE is allocated.
138
CAUTION: The weight of the literal is not set correctly!
139
***********************************************************/
140
{
141
LITERAL Result;
142
143
#ifdef CHECK
144
if (!term_IsTerm(Atom)) {
145
misc_StartErrorReport();
146
misc_ErrorReport("\n In clause_LiteralCreate:");
147
misc_ErrorReport("\n Illegal input. Input not a term.");
148
misc_FinishErrorReport();
149
}
150
if (!symbol_IsPredicate(term_TopSymbol(Atom)) &&
151
(term_TopSymbol(Atom) != fol_Not())) {
152
misc_StartErrorReport();
153
misc_ErrorReport("\n In clause_LiteralCreate:");
154
misc_ErrorReport("\n Illegal input. No predicate- or negated term.");
155
misc_FinishErrorReport();
156
}
157
#endif
158
159
Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE));
160
161
Result->atomWithSign = Atom;
162
Result->oriented = FALSE;
163
Result->weight = clause_WEIGHTUNDEFINED;
164
Result->maxLit = 0;
165
Result->owningClause = Clause;
166
167
return Result;
168
}
169
170
171
LITERAL clause_LiteralCreateNegative(TERM Atom, CLAUSE Clause)
172
/**********************************************************
173
INPUT: A Pointer to a unsigned Predicate-Term and one to a
174
clause it shall belong to.
175
RETURNS: An appropriate literal where the other values
176
are set to default values and the term gets a sign.
177
MEMORY: A LITERAL_NODE is allocated.
178
CAUTION: The weight of the literal is not set correctly!
179
***********************************************************/
180
{
181
LITERAL Result;
182
183
#ifdef CHECK
184
if (!term_IsTerm(Atom)) {
185
misc_StartErrorReport();
186
misc_ErrorReport("\n In clause_LiteralCreateNegative:");
187
misc_ErrorReport("\n Illegal input. Input not an atom.");
188
misc_FinishErrorReport();
189
}
190
if (!symbol_IsPredicate(term_TopSymbol(Atom)) &&
191
(term_TopSymbol(Atom) != fol_Not())) {
192
misc_StartErrorReport();
193
misc_ErrorReport("\n In clause_LiteralCreateNegative:");
194
misc_ErrorReport("\n Illegal input. Input term not normalized.");
195
misc_FinishErrorReport();
196
}
197
#endif
198
199
Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE));
200
201
term_RplacSupertermList(Atom, list_Nil());
202
203
Result->atomWithSign = term_Create(fol_Not(), list_List(Atom));
204
Result->oriented = FALSE;
205
Result->maxLit = 0;
206
Result->weight = clause_WEIGHTUNDEFINED;
207
Result->owningClause = Clause;
208
209
return Result;
210
}
211
212
213
void clause_LiteralDelete(LITERAL Literal)
214
/*********************************************************
215
INPUT: A literal, which has an unshared Atom. For Shared
216
literals clause_LiteralDeleteFromSharing(Lit) is
217
available.
218
RETURNS: Nothing.
219
MEMORY: The Atom of 'Literal' is deleted and its memory
220
is freed as well as the LITERAL_NODE.
221
**********************************************************/
222
{
223
#ifdef CHECK
224
if (!clause_LiteralIsLiteral(Literal)) {
225
misc_StartErrorReport();
226
misc_ErrorReport("\n In clause_LiteralDelete:");
227
misc_ErrorReport("\n Illegal input. Input not a literal.");
228
misc_FinishErrorReport();
229
}
230
#endif
231
232
term_Delete(clause_LiteralSignedAtom(Literal));
233
234
clause_LiteralFree(Literal);
235
}
236
237
238
void clause_LiteralInsertIntoSharing(LITERAL Lit, SHARED_INDEX ShIndex)
239
/**********************************************************
240
INPUT: A Literal with an unshared Atom and an Index.
241
RETURNS: The literal with a shared Atom inserted into the
242
'Index'.
243
MEMORY: Allocates TERM_NODE memory needed to insert 'Lit'
244
into the sharing and frees the memory of the
245
unshared Atom.
246
***********************************************************/
247
{
248
249
TERM Atom;
250
251
#ifdef CHECK
252
if (!clause_LiteralIsLiteral(Lit)) {
253
misc_StartErrorReport();
254
misc_ErrorReport("\n In clause_LiteralInsertIntoSharing:");
255
misc_ErrorReport("\n Illegal literal input.");
256
misc_FinishErrorReport();
257
}
258
#endif
259
260
Atom = clause_LiteralAtom(Lit);
261
262
clause_LiteralSetAtom(Lit, sharing_Insert(Lit, Atom, ShIndex));
263
264
term_Delete(Atom);
265
}
266
267
268
void clause_LiteralDeleteFromSharing(LITERAL Lit, SHARED_INDEX ShIndex)
269
/**********************************************************
270
INPUT: A Literal and an 'Index'.
271
RETURNS: Nothing.
272
MEMORY: Deletes 'Lit' from Sharing, frees no more used
273
TERM memory and frees the LITERAL_NODE.
274
********************************************************/
275
{
276
277
TERM Atom;
278
279
#ifdef CHECK
280
if (!clause_LiteralIsLiteral(Lit)) {
281
misc_StartErrorReport();
282
misc_ErrorReport("\n In clause_LiteralDeleteFromSharing:");
283
misc_ErrorReport("\n Illegal literal input.");
284
misc_FinishErrorReport();
285
}
286
#endif
287
288
Atom = clause_LiteralAtom(Lit);
289
290
if (clause_LiteralIsNegative(Lit)) {
291
list_Free(term_ArgumentList(clause_LiteralSignedAtom(Lit)));
292
term_Free(clause_LiteralSignedAtom(Lit));
293
}
294
295
sharing_Delete(Lit, Atom, ShIndex);
296
297
clause_LiteralFree(Lit);
298
299
}
300
301
302
NAT clause_GetNumberOfInstances(TERM Term, SHARED_INDEX Index)
303
/**************************************************************
304
INPUT: A (!) shared term and a shared index. The term has to be
305
part of the index.
306
RETURNS: How many clauses contain a literal that is an instance of <Atom>.
307
***************************************************************/
308
{
309
NAT Result;
310
TERM Instance;
311
LIST Scan;
312
313
Result = 0;
314
Instance = st_ExistInstance(cont_LeftContext(), sharing_Index(Index), Term);
315
if (term_IsAtom(Term)) {
316
while (Instance != NULL) {
317
for (Scan=sharing_NAtomDataList(Instance);!list_Empty(Scan);Scan=list_Cdr(Scan))
318
if (!clause_GetFlag(clause_LiteralOwningClause(list_Car(Scan)), MARK)) {
319
clause_SetFlag(clause_LiteralOwningClause(list_Car(Scan)), MARK);
320
Result++;
321
}
322
Instance = st_NextCandidate();
323
}
324
}
325
else {
326
while (Instance != NULL) {
327
Scan = sharing_GetDataList(Instance, Index);
328
for ( ; !list_Empty(Scan); Scan = list_Pop(Scan))
329
if (!clause_GetFlag(clause_LiteralOwningClause(list_Car(Scan)), MARK)) {
330
clause_SetFlag(clause_LiteralOwningClause(list_Car(Scan)), MARK);
331
Result++;
332
}
333
Instance = st_NextCandidate();
334
}
335
}
336
return Result;
337
}
338
339
340
static LIST clause_CopyLitInterval(CLAUSE Clause, int Start, int End)
341
/**************************************************************
342
INPUT: A clause and two integers representing
343
literal indices.
344
RETURNS: Copies of all literals in <Clause> with index i and
345
in the interval [Start:End] are prepended to <List>.
346
MEMORY: All atoms are copied.
347
***************************************************************/
348
{
349
TERM Atom;
350
LIST List;
351
352
List = list_Nil();
353
354
for ( ; Start <= End; Start++) {
355
Atom = term_Copy(clause_GetLiteralAtom(Clause, Start));
356
List = list_Cons(Atom, List);
357
}
358
359
return List;
360
}
361
362
363
static LIST clause_CopyLitIntervalExcept(CLAUSE Clause, int Start, int End,
364
int i)
365
/**************************************************************
366
INPUT: A clause and three integers representing
367
literal indeces.
368
RETURNS: A list of atoms from literals within the interval
369
[Start:End] except the literal at index <i>.
370
MEMORY: All atoms are copied.
371
***************************************************************/
372
{
373
TERM Atom;
374
LIST Result;
375
376
Result = list_Nil();
377
for ( ; End >= Start; End--)
378
if (End != i) {
379
Atom = term_Copy(clause_GetLiteralAtom(Clause, End));
380
Result = list_Cons(Atom, Result);
381
}
382
return Result;
383
}
384
385
386
LIST clause_CopyConstraint(CLAUSE Clause)
387
/**************************************************************
388
INPUT: A clause.
389
RETURNS: The list of copied constraint literals from <Clause>.
390
***************************************************************/
391
{
392
return clause_CopyLitInterval(Clause,
393
clause_FirstConstraintLitIndex(Clause),
394
clause_LastConstraintLitIndex(Clause));
395
}
396
397
398
LIST clause_CopyAntecedentExcept(CLAUSE Clause, int i)
399
/**************************************************************
400
INPUT: A clause.
401
RETURNS: A list containing copies of all antecedent literals
402
except <i>.
403
***************************************************************/
404
{
405
return clause_CopyLitIntervalExcept(Clause,
406
clause_FirstAntecedentLitIndex(Clause),
407
clause_LastAntecedentLitIndex(Clause),
408
i);
409
}
410
411
LIST clause_CopySuccedent(CLAUSE Clause)
412
/**************************************************************
413
INPUT: A clause.
414
RETURNS: The list of copied succedent literals from <Clause>.
415
***************************************************************/
416
{
417
return clause_CopyLitInterval(Clause,
418
clause_FirstSuccedentLitIndex(Clause),
419
clause_LastSuccedentLitIndex(Clause));
420
}
421
422
423
LIST clause_CopySuccedentExcept(CLAUSE Clause, int i)
424
/**************************************************************
425
INPUT: A clause.
426
RETURNS: A list containing copies of all succedent literals
427
except <i>.
428
***************************************************************/
429
{
430
return clause_CopyLitIntervalExcept(Clause,
431
clause_FirstSuccedentLitIndex(Clause),
432
clause_LastSuccedentLitIndex(Clause),
433
i);
434
}
435
436
437
/**************************************************************/
438
/* Specials */
439
/**************************************************************/
440
441
BOOL clause_IsUnorderedClause(CLAUSE Clause)
442
/*********************************************************
443
INPUT: A clause.
444
RETURNS: TRUE, if the invariants concerning splitting etc. hold
445
Invariants concerning maximality restrictions are not tested.
446
**********************************************************/
447
{
448
return ((Clause != NULL) &&
449
clause_CheckSplitLevel(Clause) &&
450
(clause_IsEmptyClause(Clause) ||
451
/* Check the first literal as a "random" sample */
452
clause_LiteralIsLiteral(clause_GetLiteral(Clause,clause_FirstLitIndex()))) &&
453
(clause_SplitLevel(Clause) == 0 || Clause->splitfield_length>0) &&
454
clause_DependsOnSplitLevel(Clause,clause_SplitLevel(Clause)));
455
}
456
457
458
BOOL clause_IsClauseAux(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence,
459
BOOL VarIsConst)
460
/*********************************************************
461
INPUT: A clause, a flag store and a precedence and a flag.
462
RETURNS: TRUE, if literals are correctly ordered and the
463
invariants concerning splitting etc. hold
464
CAUTION: If <VarIsConst> is set to TRUE variables are
465
interpreted as constants
466
**********************************************************/
467
{
468
int i;
469
LITERAL ActLit;
470
471
if (!clause_IsUnorderedClause(Clause))
472
return FALSE;
473
474
for (i=clause_FirstAntecedentLitIndex(Clause);i<=clause_LastSuccedentLitIndex(Clause);i++) {
475
ActLit = clause_GetLiteral(Clause,i);
476
477
if (!clause_LiteralIsLiteral(ActLit))
478
return FALSE;
479
480
if (fol_IsEquality(clause_LiteralAtom(ActLit))) {
481
ord_RESULT HelpRes;
482
483
HelpRes =
484
ord_CompareAux(term_FirstArgument(clause_LiteralAtom(ActLit)),
485
term_SecondArgument(clause_LiteralAtom(ActLit)),
486
FlagStore, Precedence, VarIsConst);
487
488
if (ord_IsSmallerThan(HelpRes))
489
return FALSE;
490
}
491
}
492
493
return TRUE;
494
}
495
496
497
BOOL clause_IsClause(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence)
498
/*********************************************************
499
INPUT: A clause, a flag store and a precedence.
500
RETURNS: TRUE, if literals are correctly ordered and the
501
invariants concerning splitting etc. hold
502
**********************************************************/
503
{
504
return clause_IsClauseAux(Clause, FlagStore, Precedence, FALSE);
505
}
506
507
508
BOOL clause_IsClauseSkolem(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence)
509
/*********************************************************
510
INPUT: A clause, a flag store and a precedence.
511
RETURNS: TRUE, if literals are correctly ordered and the
512
invariants concerning splitting etc. hold
513
CAUTION: Variables of <Clause> are interpreted as
514
constants
515
**********************************************************/
516
{
517
return clause_IsClauseAux(Clause, FlagStore, Precedence, TRUE);
518
}
519
520
521
522
BOOL clause_ContainsPositiveEquations(CLAUSE Clause)
523
/*********************************************************
524
INPUT: A clause.
525
RETURNS: TRUE, if the clause contains a positive equality literal.
526
**********************************************************/
527
{
528
int i;
529
530
for (i = clause_FirstSuccedentLitIndex(Clause);
531
i < clause_Length(Clause);
532
i++)
533
if (clause_LiteralIsEquality(clause_GetLiteral(Clause, i)))
534
return TRUE;
535
536
return FALSE;
537
}
538
539
540
BOOL clause_ContainsNegativeEquations(CLAUSE Clause)
541
/*********************************************************
542
INPUT: A clause.
543
RETURNS: TRUE, if the clause contains a positive equality literal.
544
**********************************************************/
545
{
546
int i;
547
548
for (i = clause_FirstAntecedentLitIndex(Clause);
549
i < clause_FirstSuccedentLitIndex(Clause);
550
i++)
551
if (clause_LiteralIsEquality(clause_GetLiteral(Clause, i)))
552
return TRUE;
553
554
return FALSE;
555
}
556
557
558
int clause_ContainsFolAtom(CLAUSE Clause, BOOL *Prop, BOOL *Grd, BOOL *Monadic,
559
BOOL *NonMonadic)
560
/*********************************************************
561
INPUT: A clause.
562
RETURNS: The number of boolean variables changed.
563
If <*Prop> is FALSE and the clause contains a propositional
564
variable, it is changed to TRUE.
565
If <*Grd> is FALSE and the clause contains a non-propositional
566
ground atom, it is changed to TRUE.
567
If <*Monadic> is FALSE and the clause contains a monadic atom,
568
it is changed to TRUE.
569
If <*NonMonadic> is FALSE and the clause contains an at least
570
2-place non-equality atom, it is changed to TRUE.
571
**********************************************************/
572
{
573
int i,Result,Arity;
574
BOOL Ground;
575
576
Result = 0;
577
i = clause_FirstLitIndex();
578
579
while (Result < 4 &&
580
i < clause_Length(Clause) &&
581
(!(*Prop) || !(*Monadic) || !(*NonMonadic))) {
582
Arity = symbol_Arity(term_TopSymbol(clause_GetLiteralAtom(Clause,i)));
583
Ground = term_IsGround(clause_GetLiteralAtom(Clause,i));
584
if (!(*Prop) && Arity == 0) {
585
Result++;
586
*Prop = TRUE;
587
}
588
if (!(*Grd) && Arity > 0 && Ground &&
589
!fol_IsEquality(clause_GetLiteralAtom(Clause,i))) {
590
Result++;
591
*Grd = TRUE;
592
}
593
if (!(*Monadic) && Arity == 1 && !Ground) {
594
Result++;
595
*Monadic = TRUE;
596
}
597
if (!(*NonMonadic) && Arity > 1 && !Ground &&
598
!fol_IsEquality(clause_GetLiteralAtom(Clause,i))) {
599
Result++;
600
*NonMonadic = TRUE;
601
}
602
i++;
603
}
604
return Result;
605
}
606
607
608
BOOL clause_ContainsVariables(CLAUSE Clause)
609
/*********************************************************
610
INPUT: A clause.
611
RETURNS: TRUE, if the clause contains at least one variable
612
**********************************************************/
613
{
614
int i;
615
TERM Term;
616
617
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) {
618
Term = clause_GetLiteralAtom(Clause,i);
619
if (term_NumberOfVarOccs(Term)>0)
620
return TRUE;
621
}
622
623
return FALSE;
624
}
625
626
627
void clause_ContainsSortRestriction(CLAUSE Clause, BOOL *Sortres, BOOL *USortres)
628
/*********************************************************
629
INPUT: A clause.
630
RETURNS: TRUE, if the clause contains a negative monadic atom with
631
a variable argument
632
**********************************************************/
633
{
634
int i;
635
TERM Term;
636
637
for (i = clause_FirstLitIndex();
638
i <= clause_LastAntecedentLitIndex(Clause) && (!*Sortres || !*USortres);
639
i++) {
640
Term = clause_GetLiteralAtom(Clause,i);
641
if (symbol_IsBaseSort(term_TopSymbol(Term))) {
642
*USortres = TRUE;
643
if (symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))))
644
*Sortres = TRUE;
645
}
646
}
647
}
648
649
BOOL clause_ContainsFunctions(CLAUSE Clause)
650
/*********************************************************
651
INPUT: A clause.
652
RETURNS: TRUE, if the clause contains at least one function symbol
653
**********************************************************/
654
{
655
int i;
656
TERM Term;
657
658
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) {
659
Term = clause_GetLiteralAtom(Clause,i);
660
if (term_ContainsFunctions(Term))
661
return TRUE;
662
}
663
664
return FALSE;
665
}
666
667
BOOL clause_ContainsSymbol(CLAUSE Clause, SYMBOL Symbol)
668
/*********************************************************
669
INPUT: A clause and a symbol.
670
RETURNS: TRUE, if the clause contains the symbol
671
**********************************************************/
672
{
673
int i;
674
675
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++)
676
if (term_ContainsSymbol(clause_GetLiteralAtom(Clause,i), Symbol))
677
return TRUE;
678
return FALSE;
679
}
680
681
NAT clause_NumberOfSymbolOccurrences(CLAUSE Clause, SYMBOL Symbol)
682
/*********************************************************
683
INPUT: A clause and a symbol.
684
RETURNS: the number of occurrences of <Symbol> in <Clause>
685
**********************************************************/
686
{
687
int i;
688
NAT Result;
689
690
Result = 0;
691
692
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++)
693
Result += term_NumberOfSymbolOccurrences(clause_GetLiteralAtom(Clause,i), Symbol);
694
695
return Result;
696
}
697
698
BOOL clause_ImpliesFiniteDomain(CLAUSE Clause)
699
/*********************************************************
700
INPUT: A clause.
701
RETURNS: TRUE, if the clause consists of a positive disjunction
702
of equations, where each equation is of the form "x=t" for
703
some variable "x" and ground term "t"
704
**********************************************************/
705
{
706
int i;
707
TERM Term;
708
709
if (clause_FirstLitIndex() != clause_FirstSuccedentLitIndex(Clause))
710
return FALSE;
711
712
for (i = clause_FirstLitIndex(); i < clause_Length(Clause); i++) {
713
Term = clause_GetLiteralTerm(Clause,i);
714
if (!symbol_Equal(term_TopSymbol(Term),fol_Equality()) ||
715
(!symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))) &&
716
!symbol_IsVariable(term_TopSymbol(term_SecondArgument(Term)))) ||
717
(symbol_IsVariable(term_TopSymbol(term_FirstArgument(Term))) &&
718
!term_IsGround(term_SecondArgument(Term))) ||
719
(symbol_IsVariable(term_TopSymbol(term_SecondArgument(Term))) &&
720
!term_IsGround(term_FirstArgument(Term))))
721
return FALSE;
722
}
723
724
return TRUE;
725
}
726
727
BOOL clause_ImpliesNonTrivialDomain(CLAUSE Clause)
728
/*********************************************************
729
INPUT: A clause.
730
RETURNS: TRUE, if the clause consists of a negative equation
731
with two syntactically different arguments
732
**********************************************************/
733
{
734
if (clause_Length(Clause) == 1 &&
735
!clause_HasEmptyAntecedent(Clause) &&
736
clause_LiteralIsEquality(clause_FirstAntecedentLit(Clause)) &&
737
!term_Equal(term_FirstArgument(clause_LiteralAtom(clause_FirstAntecedentLit(Clause))),
738
term_SecondArgument(clause_LiteralAtom(clause_FirstAntecedentLit(Clause)))))
739
return TRUE;
740
741
return FALSE;
742
}
743
744
LIST clause_FiniteMonadicPredicates(LIST Clauses)
745
/*********************************************************
746
INPUT: A list of clauses.
747
RETURNS: A list of all predicate symbols that are guaranteed
748
to have a finite extension in any minimal Herbrand model.
749
These predicates must only positively occur
750
in unit clauses and must have a ground term argument.
751
**********************************************************/
752
{
753
LIST Result, NonFinite, Scan;
754
CLAUSE Clause;
755
int i, n;
756
SYMBOL Pred;
757
758
Result = list_Nil();
759
NonFinite = list_Nil();
760
761
for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) {
762
Clause = (CLAUSE)list_Car(Scan);
763
n = clause_Length(Clause);
764
for (i=clause_FirstSuccedentLitIndex(Clause);i<n;i++) {
765
Pred = term_TopSymbol(clause_GetLiteralAtom(Clause,i));
766
if (symbol_Arity(Pred) == 1 &&
767
!list_PointerMember(NonFinite, (POINTER)Pred)) {
768
if (term_NumberOfVarOccs(clause_GetLiteralAtom(Clause,i)) > 0 ||
769
n > 1) {
770
NonFinite = list_Cons((POINTER)Pred, NonFinite);
771
Result = list_PointerDeleteElement(Result, (POINTER)Pred);
772
}
773
else {
774
if (!list_PointerMember(Result, (POINTER)Pred))
775
Result = list_Cons((POINTER)Pred, Result);
776
}
777
}
778
}
779
}
780
list_Delete(NonFinite);
781
782
Result = list_PointerDeleteElement(Result, (POINTER)fol_Equality());
783
784
return Result;
785
}
786
787
NAT clause_NumberOfVarOccs(CLAUSE Clause)
788
/**************************************************************
789
INPUT: A Clause.
790
RETURNS: The number of variable occurrences in the clause.
791
***************************************************************/
792
{
793
int i,n;
794
NAT Result;
795
796
Result = 0;
797
n = clause_Length(Clause);
798
799
for (i = clause_FirstLitIndex(); i < n; i++)
800
Result += term_NumberOfVarOccs(clause_GetLiteralTerm(Clause,i));
801
802
return Result;
803
}
804
805
806
NAT clause_ComputeWeight(CLAUSE Clause, FLAGSTORE Flags)
807
/**************************************************************
808
INPUT: A clause and a flag store.
809
RETURNS: The Weight of the literals in the clause,
810
up to now the number of variable symbols plus
811
twice the number of signature symbols.
812
EFFECT: The weight of the literals is updated, but not the
813
weight of the clause!
814
***************************************************************/
815
{
816
int i, n;
817
NAT Weight;
818
LITERAL Lit;
819
820
Weight = 0;
821
n = clause_Length(Clause);
822
823
for (i = clause_FirstLitIndex(); i < n; i++) {
824
Lit = clause_GetLiteral(Clause, i);
825
clause_UpdateLiteralWeight(Lit, Flags);
826
Weight += clause_LiteralWeight(Lit);
827
}
828
return Weight;
829
}
830
831
832
NAT clause_ComputeTermDepth(CLAUSE Clause)
833
/**************************************************************
834
INPUT: A Clause.
835
RETURNS: Maximal depth of a literal in <Clause>.
836
***************************************************************/
837
{
838
int i,n;
839
NAT Depth,Help;
840
841
#ifdef CHECK
842
if (!clause_IsUnorderedClause(Clause)) {
843
misc_StartErrorReport();
844
misc_ErrorReport("\n In clause_ComputeTermDepth:");
845
misc_ErrorReport("\n Illegal input. Input not a clause.");
846
misc_FinishErrorReport();
847
}
848
#endif
849
850
Depth = 0;
851
n = clause_Length(Clause);
852
853
for (i = clause_FirstLitIndex();i < n;i++) {
854
Help = term_Depth(clause_GetLiteralAtom(Clause,i));
855
if (Help > Depth)
856
Depth = Help;
857
}
858
return Depth;
859
}
860
861
NAT clause_MaxTermDepthClauseList(LIST Clauses)
862
/**************************************************************
863
INPUT: A list of clauses.
864
RETURNS: Maximal depth of a clause in <Clauses>.
865
***************************************************************/
866
{
867
NAT Depth,Help;
868
869
Depth = 0;
870
871
while (!list_Empty(Clauses)) {
872
Help = clause_ComputeTermDepth(list_Car(Clauses));
873
if (Help > Depth)
874
Depth = Help;
875
Clauses = list_Cdr(Clauses);
876
}
877
878
return Depth;
879
}
880
881
882
NAT clause_ComputeSize(CLAUSE Clause)
883
/**************************************************************
884
INPUT: A Clause.
885
RETURNS: The Size of the literals in the clause,
886
up to now the number of symbols.
887
***************************************************************/
888
{
889
int i,n;
890
NAT Size;
891
892
#ifdef CHECK
893
if (!clause_IsUnorderedClause(Clause)) {
894
misc_StartErrorReport();
895
misc_ErrorReport("\n In clause_ComputeSize:");
896
misc_ErrorReport("\n Illegal input. Input not a clause.");
897
misc_FinishErrorReport();
898
}
899
#endif
900
901
Size = 0;
902
n = clause_Length(Clause);
903
904
for (i = clause_FirstLitIndex();i < n;i++)
905
Size += term_ComputeSize(clause_GetLiteralTerm(Clause,i));
906
907
return Size;
908
}
909
910
911
BOOL clause_WeightCorrect(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence)
912
/*********************************************************
913
INPUT: A clause, a flag store and a precedence.
914
RETURNS: TRUE iff the weight fields of the clause and its
915
literals are correct.
916
**********************************************************/
917
{
918
int i, n;
919
NAT Weight, Help;
920
LITERAL Lit;
921
922
#ifdef CHECK
923
if (!clause_IsClause(Clause, Flags, Precedence)) {
924
misc_StartErrorReport();
925
misc_ErrorReport("\n In clause_WeightCorrect:");
926
misc_ErrorReport("\n Illegal input. Input not a clause.");
927
misc_FinishErrorReport();
928
}
929
#endif
930
931
Weight = 0;
932
n = clause_Length(Clause);
933
934
for (i = clause_FirstLitIndex(); i < n; i++) {
935
Lit = clause_GetLiteral(Clause, i);
936
Help = clause_LiteralComputeWeight(Lit, Flags);
937
if (Help != clause_LiteralWeight(Lit))
938
return FALSE;
939
Weight += Help;
940
}
941
942
return (clause_Weight(Clause) == Weight);
943
}
944
945
946
LIST clause_InsertWeighed(CLAUSE Clause, LIST UsList, FLAGSTORE Flags,
947
PRECEDENCE Precedence)
948
/*********************************************************
949
INPUT: A clause, a list to insert the clause into,
950
a flag store and a precedence.
951
RETURNS: The list where the clause is inserted wrt its
952
weight (Weight(Car(list)) <= Weight(Car(Cdr(list)))).
953
MEMORY: A new listnode is allocated.
954
**********************************************************/
955
{
956
LIST Scan;
957
NAT Weight;
958
959
#ifdef CHECK
960
if (!clause_IsClause(Clause, Flags, Precedence)) {
961
misc_StartErrorReport();
962
misc_ErrorReport("\n In clause_InsertWeighted:");
963
misc_ErrorReport("\n Illegal input. Input not a clause.");
964
misc_FinishErrorReport();
965
}
966
#endif
967
968
Weight = clause_Weight(Clause);
969
970
Scan = UsList;
971
972
if (list_Empty(Scan) ||
973
(clause_Weight(list_Car(Scan)) > Weight)) {
974
return list_Cons(Clause, Scan);
975
976
} else {
977
while (!list_Empty(list_Cdr(Scan)) &&
978
(clause_Weight(list_Car(list_Cdr(Scan))) <= Weight)) {
979
Scan = list_Cdr(Scan);
980
}
981
list_Rplacd(Scan, list_Cons(Clause, list_Cdr(Scan)));
982
return UsList;
983
}
984
}
985
986
987
LIST clause_ListSortWeighed(LIST Clauses)
988
/*********************************************************
989
INPUT: A list of clauses.
990
RETURNS: The clause list sorted with respect to the weight
991
of clauses, minimal weight first.
992
EFFECT: The original list is destructively changed!
993
This function doesn't sort stable!
994
The function uses bucket sort for clauses with weight
995
smaller than clause_MAXWEIGHT, and the usual list sort
996
function for clauses with weight >= clause_MAXWEIGHT.
997
This implies the function uses time O(n-c + c*log c),
998
where n is the length of the list and c is the number
999
of clauses with weight >= clause_MAXWEIGHT.
1000
For c=0 you get time O(n), for c=n you get time (n*log n).
1001
**********************************************************/
1002
{
1003
int weight;
1004
LIST Scan;
1005
1006
for (Scan=Clauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
1007
weight = clause_Weight(list_Car(Scan));
1008
if (weight < clause_MAXWEIGHT)
1009
clause_SORT[weight] = list_Cons(list_Car(Scan),clause_SORT[weight]);
1010
else
1011
clause_SORT[clause_MAXWEIGHT] = list_Cons(list_Car(Scan),clause_SORT[clause_MAXWEIGHT]);
1012
}
1013
Scan = list_NumberSort(clause_SORT[clause_MAXWEIGHT],
1014
(NAT (*)(POINTER)) clause_Weight);
1015
clause_SORT[clause_MAXWEIGHT] = list_Nil();
1016
for (weight = clause_MAXWEIGHT-1; weight >= 0; weight--) {
1017
Scan = list_Nconc(clause_SORT[weight],Scan);
1018
clause_SORT[weight] = list_Nil();
1019
}
1020
list_Delete(Clauses);
1021
return Scan;
1022
}
1023
1024
1025
LITERAL clause_LiteralCopy(LITERAL Literal)
1026
/*********************************************************
1027
INPUT: A literal.
1028
RETURNS: An unshared copy of the literal, where the owning
1029
clause-slot is set to NULL.
1030
MEMORY: Memory for a new LITERAL_NODE and all its TERMs
1031
subterms is allocated.
1032
**********************************************************/
1033
{
1034
1035
LITERAL Result;
1036
1037
#ifdef CHECK
1038
if (!clause_LiteralIsLiteral(Literal)) {
1039
misc_StartErrorReport();
1040
misc_ErrorReport("\n In clause_LiteralCopy:");
1041
misc_ErrorReport("\n Illegal input. Input not a literal.");
1042
misc_FinishErrorReport();
1043
}
1044
#endif
1045
1046
Result = (LITERAL)memory_Malloc(sizeof(LITERAL_NODE));
1047
1048
Result->atomWithSign = term_Copy(clause_LiteralSignedAtom(Literal));
1049
Result->oriented = clause_LiteralIsOrientedEquality(Literal);
1050
1051
Result->maxLit = Literal->maxLit;
1052
Result->weight = Literal->weight;
1053
Result->owningClause = (POINTER)NULL;
1054
1055
return Result;
1056
}
1057
1058
void clause_SetSplitDataFromList(CLAUSE Result, LIST List)
1059
{
1060
CLAUSE TempClause;
1061
LIST Scan;
1062
NAT l;
1063
Scan = List;
1064
l = Result->splitfield_length;
1065
while (!list_Empty(Scan)) {
1066
TempClause = (CLAUSE) list_Top(Scan);
1067
if (clause_GetFlag(TempClause, CONCLAUSE))
1068
clause_SetFlag(Result, CONCLAUSE);
1069
clause_SetSplitLevel(Result,
1070
clause_SplitLevel(TempClause) > clause_SplitLevel(Result)
1071
? clause_SplitLevel(TempClause)
1072
: clause_SplitLevel(Result));
1073
if (l < TempClause->splitfield_length)
1074
l = TempClause->splitfield_length;
1075
Scan = list_Cdr(Scan);
1076
}
1077
if (l > Result->splitfield_length) {
1078
if (Result->splitfield != NULL)
1079
memory_Free(Result->splitfield,
1080
sizeof(SPLITFIELDENTRY) * Result->splitfield_length);
1081
Result->splitfield = memory_Malloc(sizeof(SPLITFIELDENTRY) * l);
1082
Result->splitfield_length = l;
1083
}
1084
1085
for (l=0; l < Result->splitfield_length; l++)
1086
Result->splitfield[l] = 0;
1087
1088
while (!list_Empty(List)) {
1089
TempClause= (CLAUSE) list_Top(List);
1090
List = list_Cdr(List);
1091
for (l=0; l < TempClause->splitfield_length; l++)
1092
Result->splitfield[l] = Result->splitfield[l] | TempClause->splitfield[l];
1093
}
1094
}
1095
1096
1097
void clause_SetSplitDataFromParents(CLAUSE Result,
1098
CLAUSE Mother,
1099
CLAUSE Father)
1100
{
1101
NAT i;
1102
if (clause_GetFlag(Father, CONCLAUSE) || clause_GetFlag(Mother, CONCLAUSE))
1103
clause_SetFlag(Result, CONCLAUSE);
1104
if ((clause_SplitLevel(Father) == 0) && (clause_SplitLevel(Mother) == 0))
1105
return;
1106
clause_SetSplitLevel(Result, clause_SplitLevel(Mother) > clause_SplitLevel(Father)
1107
? clause_SplitLevel(Mother)
1108
: clause_SplitLevel(Father));
1109
1110
if (Mother->splitfield_length > Father->splitfield_length) {
1111
if (Result->splitfield != NULL)
1112
memory_Free(Result->splitfield,
1113
sizeof(SPLITFIELDENTRY) * Result->splitfield_length);
1114
Result->splitfield = memory_Malloc(sizeof(SPLITFIELDENTRY) *
1115
Mother->splitfield_length);
1116
Result->splitfield_length = Mother->splitfield_length;
1117
for (i=0; i < Father->splitfield_length; i++)
1118
Result->splitfield[i] =
1119
Mother->splitfield[i] | Father->splitfield[i];
1120
for (i=Father->splitfield_length; i < Mother->splitfield_length; i++)
1121
Result->splitfield[i] = Mother->splitfield[i];
1122
}
1123
else {
1124
if (Result->splitfield != NULL)
1125
memory_Free(Result->splitfield,
1126
sizeof(SPLITFIELDENTRY) * Result->splitfield_length);
1127
Result->splitfield = memory_Malloc(sizeof(SPLITFIELDENTRY) *
1128
Father->splitfield_length);
1129
Result->splitfield_length = Father->splitfield_length;
1130
for (i=0; i < Mother->splitfield_length; i++)
1131
Result->splitfield[i] =
1132
Mother->splitfield[i] | Father->splitfield[i];
1133
for (i=Mother->splitfield_length; i < Father->splitfield_length; i++)
1134
Result->splitfield[i] = Father->splitfield[i];
1135
}
1136
}
1137
1138
void clause_SetSplitDataFromFather(CLAUSE Result,
1139
CLAUSE Father)
1140
{
1141
if (clause_GetFlag(Father, CONCLAUSE))
1142
clause_SetFlag(Result, CONCLAUSE);
1143
clause_SetSplitLevel(Result, clause_SplitLevel(Father));
1144
clause_SetSplitField(Result, Father->splitfield, Father->splitfield_length);
1145
}
1146
1147
void clause_UpdateSplitField(CLAUSE C1, CLAUSE C2)
1148
/*********************************************************
1149
INPUT: Two clauses C1 and C2.
1150
RETURNS: None.
1151
EFFECT: Add the split data of <C2> to <C1>.
1152
**********************************************************/
1153
{
1154
unsigned i;
1155
if (C1->splitfield_length < C2->splitfield_length)
1156
clause_ExpandSplitField(C1, C2->splitfield_length);
1157
for (i=0; i < C2->splitfield_length; i++)
1158
C1->splitfield[i] = C1->splitfield[i] | C2->splitfield[i];
1159
}
1160
1161
BOOL clause_LiteralIsSort(LITERAL L)
1162
{
1163
SYMBOL S;
1164
S = clause_LiteralPredicate(L);
1165
return (symbol_IsPredicate(S) &&
1166
(symbol_Arity(S) == 1));
1167
}
1168
1169
TERM clause_LiteralAtom(LITERAL L)
1170
{
1171
if (clause_LiteralIsNegative(L))
1172
return term_FirstArgument(clause_LiteralSignedAtom(L));
1173
else
1174
return clause_LiteralSignedAtom(L);
1175
}
1176
1177
1178
CLAUSE clause_Copy(CLAUSE Clause)
1179
/*********************************************************
1180
INPUT: A Clause.
1181
RETURNS: An unshared copy of the Clause.
1182
MEMORY: Memory for a new CLAUSE_NODE, LITERAL_NODE and
1183
all its TERMs subterms is allocated.
1184
**********************************************************/
1185
{
1186
1187
CLAUSE Result;
1188
int i,c,a,s,l;
1189
1190
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
1191
1192
Result->clausenumber = clause_Number(Clause);
1193
Result->maxVar = clause_MaxVar(Clause);
1194
Result->flags = Clause->flags;
1195
clause_InitSplitData(Result);
1196
Result->validlevel = clause_SplitLevel(Clause);
1197
clause_SetSplitField(Result, Clause->splitfield, Clause->splitfield_length);
1198
Result->depth = clause_Depth(Clause);
1199
Result->weight = Clause->weight;
1200
Result->splitpotential = Clause->splitpotential;
1201
Result->parentCls = list_Copy(clause_ParentClauses(Clause));
1202
Result->parentLits = list_Copy(clause_ParentLiterals(Clause));
1203
Result->origin = clause_Origin(Clause);
1204
1205
Result->c = (c = clause_NumOfConsLits(Clause));
1206
Result->a = (a = clause_NumOfAnteLits(Clause));
1207
Result->s = (s = clause_NumOfSuccLits(Clause));
1208
1209
l = c + a + s;
1210
if (l != 0)
1211
Result->literals = (LITERAL *)memory_Malloc(l * sizeof(LITERAL));
1212
1213
for (i = 0; i < l; i++) {
1214
clause_SetLiteral(Result, i,
1215
clause_LiteralCopy(clause_GetLiteral(Clause, i)));
1216
clause_LiteralSetOwningClause((Result->literals[i]), Result);
1217
}
1218
1219
return Result;
1220
}
1221
1222
1223
SYMBOL clause_LiteralMaxVar(LITERAL Literal)
1224
/*********************************************************
1225
INPUT: A literal.
1226
RETURNS: The maximal symbol of the literals variables,
1227
if the literal is ground, symbol_GetInitialStandardVarCounter().
1228
**********************************************************/
1229
{
1230
1231
TERM Term;
1232
int Bottom;
1233
SYMBOL MaxSym,Help;
1234
1235
#ifdef CHECK
1236
if (!clause_LiteralIsLiteral(Literal)) {
1237
misc_StartErrorReport();
1238
misc_ErrorReport("\n In clause_LiteralMaxVar:");
1239
misc_ErrorReport("\n Illegal input. Input not a literal.");
1240
misc_FinishErrorReport();
1241
}
1242
#endif
1243
1244
Bottom = stack_Bottom();
1245
MaxSym = symbol_GetInitialStandardVarCounter();
1246
Term = clause_LiteralAtom(Literal);
1247
1248
do {
1249
if (term_IsComplex(Term))
1250
stack_Push(term_ArgumentList(Term));
1251
else
1252
if (term_IsVariable(Term))
1253
MaxSym = ((MaxSym < (Help = term_TopSymbol(Term))) ?
1254
Help : MaxSym);
1255
while (!stack_Empty(Bottom) && list_Empty(stack_Top()))
1256
stack_Pop();
1257
if (!stack_Empty(Bottom)) {
1258
Term = (TERM) list_Car(stack_Top());
1259
stack_RplacTop(list_Cdr(stack_Top()));
1260
}
1261
} while (!stack_Empty(Bottom));
1262
1263
return MaxSym;
1264
}
1265
1266
1267
SYMBOL clause_AtomMaxVar(TERM Term)
1268
/*********************************************************
1269
INPUT: A term.
1270
RETURNS: The maximal symbol of the lcontained variables,
1271
if <Term> is ground, symbol_GetInitialStandardVarCounter().
1272
**********************************************************/
1273
{
1274
int Bottom;
1275
SYMBOL VarSym,Help;
1276
1277
Bottom = stack_Bottom();
1278
VarSym = symbol_GetInitialStandardVarCounter();
1279
1280
do {
1281
if (term_IsComplex(Term))
1282
stack_Push(term_ArgumentList(Term));
1283
else
1284
if (term_IsVariable(Term))
1285
VarSym = ((VarSym < (Help = term_TopSymbol(Term))) ?
1286
Help : VarSym);
1287
while (!stack_Empty(Bottom) && list_Empty(stack_Top()))
1288
stack_Pop();
1289
if (!stack_Empty(Bottom)) {
1290
Term = (TERM)list_Car(stack_Top());
1291
stack_RplacTop(list_Cdr(stack_Top()));
1292
}
1293
} while (!stack_Empty(Bottom));
1294
1295
return VarSym;
1296
}
1297
1298
void clause_SetMaxLitFlagsAux(CLAUSE Clause, FLAGSTORE FlagStore,
1299
PRECEDENCE Precedence, BOOL VarIsConst)
1300
/**********************************************************
1301
INPUT: A clause, a flag store and a precedence.
1302
A boolean flag.
1303
RETURNS: Nothing.
1304
EFFECT: Sets the maxLit-flag for maximal literals.
1305
if <VarIsConst> is set then variables are
1306
interpreted as skolem constants.
1307
***********************************************************/
1308
{
1309
int i,j,n,fa;
1310
LITERAL ActLit,CompareLit;
1311
BOOL Result, Twin;
1312
ord_RESULT HelpRes;
1313
1314
n = clause_Length(Clause);
1315
fa = clause_FirstAntecedentLitIndex(Clause);
1316
1317
clause_RemoveFlag(Clause,CLAUSESELECT);
1318
for (i = clause_FirstLitIndex(); i < n; i++)
1319
clause_LiteralFlagReset(clause_GetLiteral(Clause, i));
1320
if (term_StampOverflow(clause_STAMPID))
1321
for (i = clause_FirstLitIndex(); i < n; i++)
1322
term_ResetTermStamp(clause_LiteralSignedAtom(clause_GetLiteral(Clause, i)));
1323
term_StartStamp();
1324
1325
/*printf("\n Start: "); clause_Print(Clause);*/
1326
1327
for (i = fa; i < n; i++) {
1328
ActLit = clause_GetLiteral(Clause, i);
1329
if (!term_HasTermStamp(clause_LiteralSignedAtom(ActLit))) {
1330
Result = TRUE;
1331
Twin = FALSE;
1332
for (j = fa; j < n && Result; j++)
1333
if (i != j) {
1334
CompareLit = clause_GetLiteral(Clause, j);
1335
HelpRes = ord_LiteralCompareAux(clause_LiteralSignedAtom(ActLit),
1336
clause_LiteralIsOrientedEquality(ActLit),
1337
clause_LiteralSignedAtom(CompareLit),
1338
clause_LiteralIsOrientedEquality(CompareLit),
1339
FALSE, VarIsConst, FlagStore, Precedence);
1340
1341
/*printf("\n\tWe compare: ");
1342
fol_PrintDFG(clause_LiteralAtom(ActLit));
1343
putchar(' ');
1344
fol_PrintDFG(clause_LiteralAtom(CompareLit));
1345
printf(" Result: "); ord_Print(HelpRes);*/
1346
1347
if (ord_IsEqual(HelpRes))
1348
Twin = TRUE;
1349
if (ord_IsSmallerThan(HelpRes))
1350
Result = FALSE;
1351
if (ord_IsGreaterThan(HelpRes))
1352
term_SetTermStamp(clause_LiteralSignedAtom(CompareLit));
1353
}
1354
if (Result) {
1355
clause_LiteralSetFlag(ActLit, MAXIMAL);
1356
if (!Twin)
1357
clause_LiteralSetFlag(ActLit, STRICTMAXIMAL);
1358
}
1359
}
1360
}
1361
term_StopStamp();
1362
/*printf("\n End: "); clause_Print(Clause);*/
1363
}
1364
1365
1366
void clause_SetMaxLitFlagsSkolem(CLAUSE Clause, FLAGSTORE FlagStore,
1367
PRECEDENCE Precedence)
1368
/**********************************************************
1369
INPUT: A clause, a flag store and a precedence.
1370
RETURNS: Nothing.
1371
EFFECT: Sets the maxLit-flag for maximal literals.
1372
variables are interpreted as skolem constants
1373
***********************************************************/
1374
{
1375
clause_SetMaxLitFlagsAux(Clause, FlagStore, Precedence, TRUE);
1376
}
1377
1378
void clause_SetMaxLitFlags(CLAUSE Clause, FLAGSTORE FlagStore,
1379
PRECEDENCE Precedence)
1380
/**********************************************************
1381
INPUT: A clause, a flag store and a precedence.
1382
RETURNS: Nothing.
1383
EFFECT: Sets the maxLit-flag for maximal literals.
1384
***********************************************************/
1385
{
1386
clause_SetMaxLitFlagsAux(Clause, FlagStore, Precedence, FALSE);
1387
}
1388
1389
1390
void clause_SetNativeMaxLitFlags(CLAUSE Clause, FLAGSTORE FlagStore,
1391
PRECEDENCE Precedence)
1392
/**********************************************************
1393
INPUT: A clause, a flag store and a precedence.
1394
RETURNS: Nothing.
1395
EFFECT: Sets the maxLit-flag for maximal literals,
1396
keeping the sel flag on literals in input clauses.
1397
***********************************************************/
1398
{
1399
int i,j,n,fa;
1400
LITERAL ActLit,CompareLit;
1401
BOOL Result, Twin;
1402
ord_RESULT HelpRes;
1403
1404
n = clause_Length(Clause);
1405
fa = clause_FirstAntecedentLitIndex(Clause);
1406
1407
/* Reset literal flags first. */
1408
if (clause_GetFlag(Clause, CLAUSESELECT))
1409
/* If selected literals need to be kept,
1410
only reset maxlit and strictmaxlit flags. */
1411
for (i = clause_FirstLitIndex(); i < n; i++)
1412
clause_LiteralFlagResetAndKeepSelFlag(clause_GetLiteral(Clause, i));
1413
else {
1414
/* Otherwise, reset the literal flag. */
1415
for (i = clause_FirstLitIndex(); i < n; i++)
1416
clause_LiteralFlagReset(clause_GetLiteral(Clause, i));
1417
}
1418
if (term_StampOverflow(clause_STAMPID))
1419
for (i = clause_FirstLitIndex(); i < n; i++)
1420
term_ResetTermStamp(clause_LiteralSignedAtom(clause_GetLiteral(Clause, i)));
1421
term_StartStamp();
1422
1423
/*printf("\n Start: "); clause_Print(Clause);*/
1424
1425
for (i = fa; i < n; i++) {
1426
ActLit = clause_GetLiteral(Clause, i);
1427
if (!term_HasTermStamp(clause_LiteralSignedAtom(ActLit))) {
1428
Result = TRUE;
1429
Twin = FALSE;
1430
for (j = fa; j < n && Result; j++)
1431
if (i != j) {
1432
CompareLit = clause_GetLiteral(Clause, j);
1433
HelpRes = ord_LiteralCompare(clause_LiteralSignedAtom(ActLit),
1434
clause_LiteralIsOrientedEquality(ActLit),
1435
clause_LiteralSignedAtom(CompareLit),
1436
clause_LiteralIsOrientedEquality(CompareLit),
1437
FALSE, FlagStore, Precedence);
1438
1439
/*printf("\n\tWe compare: ");
1440
fol_PrintDFG(clause_LiteralAtom(ActLit));
1441
putchar(' ');
1442
fol_PrintDFG(clause_LiteralAtom(CompareLit));
1443
printf(" Result: "); ord_Print(HelpRes);*/
1444
1445
if (ord_IsEqual(HelpRes))
1446
Twin = TRUE;
1447
if (ord_IsSmallerThan(HelpRes))
1448
Result = FALSE;
1449
if (ord_IsGreaterThan(HelpRes))
1450
term_SetTermStamp(clause_LiteralSignedAtom(CompareLit));
1451
}
1452
if (Result) {
1453
clause_LiteralSetFlag(ActLit, MAXIMAL);
1454
if (!Twin)
1455
clause_LiteralSetFlag(ActLit, STRICTMAXIMAL);
1456
}
1457
}
1458
}
1459
term_StopStamp();
1460
/*printf("\n End: "); clause_Print(Clause);*/
1461
}
1462
1463
SYMBOL clause_SearchMaxVar(CLAUSE Clause)
1464
/**********************************************************
1465
INPUT: A clause.
1466
RETURNS: The maximal symbol of the clauses variables.
1467
If the clause is ground, symbol_GetInitialStandardVarCounter().
1468
***********************************************************/
1469
{
1470
int i, n;
1471
SYMBOL Help, MaxSym;
1472
1473
n = clause_Length(Clause);
1474
1475
MaxSym = symbol_GetInitialStandardVarCounter();
1476
1477
for (i = 0; i < n; i++) {
1478
Help = clause_LiteralMaxVar(clause_GetLiteral(Clause, i));
1479
if (Help > MaxSym)
1480
MaxSym = Help;
1481
}
1482
return MaxSym;
1483
}
1484
1485
1486
void clause_RenameVarsBiggerThan(CLAUSE Clause, SYMBOL MinVar)
1487
/**********************************************************
1488
INPUT: A clause and a variable symbol.
1489
RETURNS: The clause with variables renamed in a way, that
1490
all vars are (excl.) bigger than MinVar.
1491
***********************************************************/
1492
{
1493
int i,n;
1494
1495
#ifdef CHECK
1496
if (!clause_IsUnorderedClause(Clause)) {
1497
misc_StartErrorReport();
1498
misc_ErrorReport("\n In clause_RenameVarsBiggerThan:");
1499
misc_ErrorReport("\n Illegal input.");
1500
misc_FinishErrorReport();
1501
}
1502
#endif
1503
1504
if (MinVar != symbol_GetInitialStandardVarCounter()) {
1505
n = clause_Length(Clause);
1506
1507
term_StartMaxRenaming(MinVar);
1508
1509
for (i = clause_FirstLitIndex(); i < n; i++)
1510
term_Rename(clause_GetLiteralTerm(Clause, i));
1511
}
1512
}
1513
1514
void clause_Normalize(CLAUSE Clause)
1515
/**********************************************************
1516
INPUT: A clause.
1517
RETURNS: The term with normalized Variables, DESTRUCTIVE
1518
on the variable subterms' topsymbols.
1519
***********************************************************/
1520
{
1521
int i,n;
1522
1523
n = clause_Length(Clause);
1524
1525
term_StartMinRenaming();
1526
1527
for (i = clause_FirstLitIndex(); i < n; i++)
1528
term_Rename(clause_GetLiteralTerm(Clause, i));
1529
}
1530
1531
1532
void clause_SubstApply(SUBST Subst, CLAUSE Clause)
1533
/**********************************************************
1534
INPUT: A clause.
1535
RETURNS: Nothing.
1536
EFFECTS: Applies the substitution to the clause.
1537
***********************************************************/
1538
{
1539
int i,n;
1540
1541
#ifdef CHECK
1542
if (!clause_IsUnorderedClause(Clause)) {
1543
misc_StartErrorReport();
1544
misc_ErrorReport("\n In clause_SubstApply:");
1545
misc_ErrorReport("\n Illegal input.");
1546
misc_FinishErrorReport();
1547
}
1548
#endif
1549
1550
n = clause_Length(Clause);
1551
1552
for (i=clause_FirstLitIndex(); i<n; i++)
1553
clause_LiteralSetAtom(clause_GetLiteral(Clause, i),
1554
subst_Apply(Subst,clause_GetLiteralAtom(Clause,i)));
1555
}
1556
1557
1558
void clause_ReplaceVariable(CLAUSE Clause, SYMBOL Var, TERM Term)
1559
/**********************************************************
1560
INPUT: A clause, a variable symbol, and a term.
1561
RETURNS: Nothing.
1562
EFFECTS: All occurences of the variable <Var> in <Clause>
1563
are replaced by copies if <Term>.
1564
CAUTION: The maximum variable of the clause is not updated!
1565
***********************************************************/
1566
{
1567
int i, li;
1568
1569
#ifdef CHECK
1570
if (!symbol_IsVariable(Var)) {
1571
misc_StartErrorReport();
1572
misc_ErrorReport("\n In clause_ReplaceVariable: symbol is not a variable");
1573
misc_FinishErrorReport();
1574
}
1575
#endif
1576
1577
li = clause_LastLitIndex(Clause);
1578
for (i = clause_FirstLitIndex(); i <= li; i++)
1579
term_ReplaceVariable(clause_GetLiteralAtom(Clause,i), Var, Term);
1580
}
1581
1582
1583
void clause_UpdateMaxVar(CLAUSE Clause)
1584
/**********************************************************
1585
INPUT: A clause.
1586
RETURNS: Nothing.
1587
EFFECTS: Actualizes the MaxVar slot wrt the actual literals.
1588
***********************************************************/
1589
{
1590
clause_SetMaxVar(Clause, clause_SearchMaxVar(Clause));
1591
}
1592
1593
void clause_OrientEqualitiesAux(CLAUSE Clause, FLAGSTORE FlagStore,
1594
PRECEDENCE Precedence, BOOL VarIsConst)
1595
/**********************************************************
1596
INPUT: An unshared clause, a flag store and a precedence,
1597
a boolean flag
1598
RETURNS: Nothing.
1599
EFFECTS: Reorders the arguments of equality literals
1600
wrt. the ordering. Thus first arguments aren't smaller
1601
after the application. If <VarIsConst> is set
1602
variables are treated as skolem constants
1603
***********************************************************/
1604
{
1605
int i,length;
1606
LITERAL EqLit;
1607
ord_RESULT HelpRes;
1608
1609
/*printf("\n Clause: ");clause_Print(Clause);*/
1610
1611
length = clause_Length(Clause);
1612
1613
for (i = clause_FirstLitIndex(); i < length; i++) {
1614
EqLit = clause_GetLiteral(Clause, i);
1615
1616
if (clause_LiteralIsEquality(EqLit)) {
1617
HelpRes = ord_CompareAux(term_FirstArgument(clause_LiteralAtom(EqLit)),
1618
term_SecondArgument(clause_LiteralAtom(EqLit)),
1619
FlagStore, Precedence, VarIsConst);
1620
1621
/*printf("\n\tWe compare: ");
1622
fol_PrintDFG(term_FirstArgument(clause_LiteralAtom(EqLit)));
1623
putchar(' ');
1624
fol_PrintDFG(term_SecondArgument(clause_LiteralAtom(EqLit)));
1625
printf("\nResult: "); ord_Print(HelpRes);*/
1626
1627
switch(HelpRes) {
1628
1629
case ord_SMALLER_THAN:
1630
/* printf("\nSwapping: ");
1631
term_Print(clause_LiteralAtom(EqLit)); DBG */
1632
term_EqualitySwap(clause_LiteralAtom(EqLit));
1633
clause_LiteralSetOrientedEquality(EqLit);
1634
/* Swapped = TRUE; */
1635
break;
1636
case ord_GREATER_THAN:
1637
clause_LiteralSetOrientedEquality(EqLit);
1638
break;
1639
default:
1640
clause_LiteralSetNoOrientedEquality(EqLit);
1641
break;
1642
}
1643
}
1644
else
1645
clause_LiteralSetNoOrientedEquality(EqLit);
1646
}
1647
}
1648
1649
void clause_OrientEqualitiesSkolem(CLAUSE Clause, FLAGSTORE FlagStore,
1650
PRECEDENCE Precedence)
1651
/**********************************************************
1652
INPUT: A clause, a Flagstore and a precedence
1653
RETURNS: Nothing.
1654
EFFECTS: Reorders the arguments of equalities.
1655
Variables are interpreted as skolem constants
1656
***********************************************************/
1657
{
1658
clause_OrientEqualitiesAux(Clause, FlagStore, Precedence, TRUE);
1659
}
1660
1661
void clause_OrientEqualities(CLAUSE Clause, FLAGSTORE FlagStore,
1662
PRECEDENCE Precedence)
1663
/**********************************************************
1664
INPUT: A Clause, a Flagstore and a precedence
1665
RETURNS: Nothing.
1666
EFFECTS: Reorders the arguments of equality literals
1667
wrt. the ordering. Thus first arguments aren't smaller
1668
after the application. If <VarIsConst> is set
1669
variables are treated as skolem constants
1670
***********************************************************/
1671
{
1672
clause_OrientEqualitiesAux(Clause, FlagStore, Precedence, FALSE);
1673
}
1674
1675
1676
void clause_InsertFlatIntoIndex(CLAUSE Clause, st_INDEX Index)
1677
/**********************************************************
1678
INPUT: An unshared clause and an index.
1679
EFFECT: The atoms of <Clause> are inserted into the index.
1680
A link from the atom to its literal via the supertermlist
1681
is established.
1682
***********************************************************/
1683
{
1684
int i,n;
1685
LITERAL Lit;
1686
TERM Atom ;
1687
1688
n = clause_Length(Clause);
1689
1690
for (i=clause_FirstLitIndex();i<n;i++) {
1691
Lit = clause_GetLiteral(Clause,i);
1692
Atom = clause_LiteralAtom(Lit);
1693
term_RplacSupertermList(Atom, list_List(Lit));
1694
st_EntryCreate(Index, Atom, Atom, cont_LeftContext());
1695
}
1696
}
1697
1698
void clause_DeleteFlatFromIndex(CLAUSE Clause, st_INDEX Index)
1699
/**********************************************************
1700
INPUT: An unshared clause and an index.
1701
EFFECT: The clause is deleted from the index and deleted itself.
1702
***********************************************************/
1703
{
1704
int i,n;
1705
LITERAL Lit;
1706
TERM Atom ;
1707
1708
n = clause_Length(Clause);
1709
1710
for (i=clause_FirstLitIndex();i<n;i++) {
1711
Lit = clause_GetLiteral(Clause,i);
1712
Atom = clause_LiteralAtom(Lit);
1713
list_Delete(term_SupertermList(Atom));
1714
term_RplacSupertermList(Atom, list_Nil());
1715
st_EntryDelete(Index, Atom, Atom, cont_LeftContext());
1716
}
1717
clause_Delete(Clause);
1718
}
1719
1720
1721
void clause_DeleteClauseListFlatFromIndex(LIST Clauses, st_INDEX Index)
1722
/**********************************************************
1723
INPUT: An list of unshared clause and an index.
1724
EFFECT: The clauses are deleted from the index and deleted itself.
1725
The list is deleted.
1726
***********************************************************/
1727
{
1728
LIST Scan;
1729
1730
for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan))
1731
clause_DeleteFlatFromIndex(list_Car(Scan), Index);
1732
1733
list_Delete(Clauses);
1734
}
1735
1736
1737
/******************************************************************/
1738
/* Some special functions used by hyper inference/reduction rules */
1739
/******************************************************************/
1740
1741
static void clause_VarToSizeMap(SUBST Subst, NAT* Map, NAT MaxIndex)
1742
/**************************************************************
1743
INPUT: A substitution, an array <Map> of size <MaxIndex>+1.
1744
RETURNS: Nothing.
1745
EFFECT: The index i within the array corresponds to the index
1746
of a variable x_i. For each variable x_i, 0<=i<=MaxIndex
1747
the size of its substitution term is calculated
1748
and written to Map[i].
1749
***************************************************************/
1750
{
1751
NAT *Scan;
1752
1753
#ifdef CHECK
1754
if (subst_Empty(Subst) || Map == NULL) {
1755
misc_StartErrorReport();
1756
misc_ErrorReport("\n In clause_VarToSizeMap: Illegal input.");
1757
misc_FinishErrorReport();
1758
}
1759
#endif
1760
1761
/* Initialization */
1762
for (Scan = Map + MaxIndex; Scan >= Map; Scan--)
1763
*Scan = 1;
1764
/* Compute the size of substitution terms */
1765
for ( ; !subst_Empty(Subst); Subst = subst_Next(Subst))
1766
Map[subst_Dom(Subst)] = term_ComputeSize(subst_Cod(Subst));
1767
}
1768
1769
1770
static NAT clause_ComputeTermSize(TERM Term, NAT* VarMap)
1771
/**************************************************************
1772
INPUT: A term and a an array of NATs.
1773
RETURNS: The number of symbols in the term.
1774
EFFECT: This function calculates the number of symbols in <Term>
1775
with respect to some substitution s.
1776
A naive way to do this is to apply the substitution
1777
to a copy of the term, and to count the number of symbols
1778
in the copied term.
1779
We use a more sophisticated algorithm, that first stores
1780
the size of every variable's substitution term in <VarMap>.
1781
We then 'scan' the term and for a variable occurrence x_i
1782
we simply add the corresponding value VarMap[i] to the result.
1783
This way we avoid copying the term and the substitution terms,
1784
which is especially useful if we reuse the VarMap several times.
1785
***************************************************************/
1786
{
1787
NAT Stack, Size;
1788
1789
#ifdef CHECK
1790
if (!term_IsTerm(Term)) {
1791
misc_StartErrorReport();
1792
misc_ErrorReport("\n In clause_ComputeTermSize: Illegal input.");
1793
misc_FinishErrorReport();
1794
}
1795
#endif
1796
1797
Size = 0;
1798
Stack = stack_Bottom();
1799
do {
1800
if (VarMap!=NULL && symbol_IsVariable(term_TopSymbol(Term)))
1801
Size += VarMap[symbol_VarIndex(term_TopSymbol(Term))];
1802
else {
1803
Size++;
1804
if (term_IsComplex(Term))
1805
stack_Push(term_ArgumentList(Term));
1806
}
1807
while (!stack_Empty(Stack) && list_Empty(stack_Top()))
1808
stack_Pop();
1809
1810
if (!stack_Empty(Stack)) {
1811
Term = list_Car(stack_Top());
1812
stack_RplacTop(list_Cdr(stack_Top()));
1813
}
1814
} while (!stack_Empty(Stack));
1815
1816
return Size;
1817
}
1818
1819
1820
LIST clause_MoveBestLiteralToFront(LIST Literals, SUBST Subst, SYMBOL MaxVar,
1821
BOOL (*Better)(LITERAL, NAT, LITERAL, NAT))
1822
/**************************************************************
1823
INPUT: A list of literals, a substitution, the maximum variable
1824
from the domain of the substitution, and a comparison
1825
function. The function <Better> will be called with two
1826
literals L1 and L2 and two number S1 and S2, where Si is
1827
the size of the atom of Li with respect to variable bindings
1828
in <Subst>.
1829
RETURNS: The same list.
1830
EFFECT: This function moves the first literal L to the front of the
1831
list, so that no other literal L' is better than L with respect
1832
to the function <Better>.
1833
The function exchanges only the literals, the order of list
1834
items within the list is not changed.
1835
***************************************************************/
1836
{
1837
NAT *Map, MapSize, BestSize, Size;
1838
LIST Best, Scan;
1839
1840
#ifdef CHECK
1841
if (!list_IsSetOfPointers(Literals)) {
1842
misc_StartErrorReport();
1843
misc_ErrorReport("\n In clause_MoveBestLiteralToFront: List contains duplicates");
1844
misc_FinishErrorReport();
1845
}
1846
#endif
1847
1848
if (list_Empty(Literals) || list_Empty(list_Cdr(Literals)))
1849
/* < 2 list items, so nothing to do */
1850
return Literals;
1851
1852
Map = NULL;
1853
MapSize = 0;
1854
1855
if (!subst_Empty(Subst)) {
1856
MapSize = symbol_VarIndex(MaxVar) + 1;
1857
Map = memory_Malloc(sizeof(NAT)*MapSize);
1858
clause_VarToSizeMap(Subst, Map, MapSize-1);
1859
}
1860
Best = Literals; /* Remember list item, not literal itself */
1861
BestSize = clause_ComputeTermSize(clause_LiteralAtom(list_Car(Best)), Map);
1862
for (Scan = list_Cdr(Literals); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
1863
Size = clause_ComputeTermSize(clause_LiteralAtom(list_Car(Scan)), Map);
1864
if (Better(list_Car(Scan), Size, list_Car(Best), BestSize)) {
1865
/* Actual literal is better than the best encountered so far */
1866
BestSize = Size;
1867
Best = Scan;
1868
}
1869
}
1870
if (Best != Literals) {
1871
/* Move best literal to the front. We just exchange the literals. */
1872
LITERAL h = list_Car(Literals);
1873
list_Rplaca(Literals, list_Car(Best));
1874
list_Rplaca(Best, h);
1875
}
1876
/* cleanup */
1877
if (Map != NULL)
1878
memory_Free(Map, sizeof(NAT)*MapSize);
1879
1880
return Literals;
1881
}
1882
1883
1884
/**************************************************************/
1885
/* Literal Output Functions */
1886
/**************************************************************/
1887
1888
void clause_LiteralPrint(LITERAL Literal)
1889
/**************************************************************
1890
INPUT: A Literal.
1891
RETURNS: Nothing.
1892
***************************************************************/
1893
{
1894
#ifdef CHECK
1895
if (!clause_LiteralIsLiteral(Literal)) {
1896
misc_StartErrorReport();
1897
misc_ErrorReport("\n In clause_LiteralPrint:");
1898
misc_ErrorReport("\n Illegal input. Input not a literal.");
1899
misc_FinishErrorReport();
1900
}
1901
#endif
1902
1903
term_PrintPrefix(clause_LiteralSignedAtom(Literal));
1904
}
1905
1906
1907
void clause_LiteralListPrint(LIST LitList)
1908
/**************************************************************
1909
INPUT: A list of literals.
1910
RETURNS: Nothing.
1911
SUMMARY: Prints the literals to stdout.
1912
***************************************************************/
1913
{
1914
while (!(list_Empty(LitList))) {
1915
clause_LiteralPrint(list_First(LitList));
1916
LitList = list_Cdr(LitList);
1917
1918
if (!list_Empty(LitList))
1919
putchar(' ');
1920
}
1921
}
1922
1923
1924
void clause_LiteralPrintUnsigned(LITERAL Literal)
1925
/**************************************************************
1926
INPUT: A Literal.
1927
RETURNS: Nothing.
1928
SUMMARY:
1929
***************************************************************/
1930
{
1931
#ifdef CHECK
1932
if (!clause_LiteralIsLiteral(Literal)) {
1933
misc_StartErrorReport();
1934
misc_ErrorReport("\n In clause_LiteralPrintUnsigned:");
1935
misc_ErrorReport("\n Illegal input. Input not a literal.");
1936
misc_FinishErrorReport();
1937
}
1938
#endif
1939
1940
term_PrintPrefix(clause_LiteralAtom(Literal));
1941
fflush(stdout);
1942
}
1943
1944
1945
void clause_LiteralPrintSigned(LITERAL Literal)
1946
/**************************************************************
1947
INPUT: A Literal.
1948
RETURNS: Nothing.
1949
SUMMARY:
1950
***************************************************************/
1951
{
1952
#ifdef CHECK
1953
if (!clause_LiteralIsLiteral(Literal)) {
1954
misc_StartErrorReport();
1955
misc_ErrorReport("\n In clause_LiteralPrintSigned:");
1956
misc_ErrorReport("\n Illegal input. Input not a literal.");
1957
misc_FinishErrorReport();
1958
}
1959
#endif
1960
1961
term_PrintPrefix(clause_LiteralSignedAtom(Literal));
1962
fflush(stdout);
1963
}
1964
1965
1966
void clause_LiteralFPrint(FILE* File, LITERAL Lit)
1967
/**************************************************************
1968
INPUT: A file and a literal.
1969
RETURNS: Nothing.
1970
************************************************************/
1971
{
1972
term_FPrintPrefix(File, clause_LiteralSignedAtom(Lit));
1973
}
1974
1975
void clause_LiteralFPrintUnsigned(FILE* File, LITERAL Lit)
1976
/**************************************************************
1977
INPUT: A file and a literal.
1978
RETURNS: Nothing.
1979
************************************************************/
1980
{
1981
term_FPrintPrefix(File, clause_LiteralAtom(Lit));
1982
}
1983
1984
LIST clause_GetLiteralSubSetList(CLAUSE Clause, int StartIndex, int EndIndex,
1985
FLAGSTORE FlagStore, PRECEDENCE Precedence)
1986
/**************************************************************
1987
INPUT: A clause, a start literal index, an end index, a
1988
flag store and a precedence.
1989
RETURNS: The list of literals between the start and the end
1990
index.
1991
It is a list of pointers, not a list of indices.
1992
**************************************************************/
1993
{
1994
1995
LIST Result;
1996
int i;
1997
1998
#ifdef CHECK
1999
if (!clause_IsClause(Clause, FlagStore, Precedence)) {
2000
misc_StartErrorReport();
2001
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
2002
misc_ErrorReport("\n Illegal input.");
2003
misc_FinishErrorReport();
2004
}
2005
if ((StartIndex < clause_FirstLitIndex())
2006
|| (EndIndex > clause_LastLitIndex(Clause))) {
2007
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
2008
misc_ErrorReport("\n Illegal input.");
2009
misc_ErrorReport("\n Index out of range.");
2010
misc_FinishErrorReport();
2011
}
2012
#endif
2013
2014
Result = list_Nil();
2015
2016
for (i=StartIndex;
2017
i<=EndIndex;
2018
i++) {
2019
Result = list_Cons(clause_GetLiteral(Clause, i), Result);
2020
}
2021
2022
return Result;
2023
}
2024
2025
2026
void clause_ReplaceLiteralSubSet(CLAUSE Clause, int StartIndex,
2027
int EndIndex, LIST Replacement,
2028
FLAGSTORE FlagStore, PRECEDENCE Precedence)
2029
/**************************************************************
2030
INPUT: A clause, a start literal index, an end literal
2031
index, a flag store and a precedence.
2032
RETURNS: None.
2033
EFFECT: Replaces the subset of literals in <Clause> with
2034
indices between (and including) <StartIndex> and
2035
<EndIndex> with literals from the <Replacement>
2036
list.
2037
**************************************************************/
2038
{
2039
2040
int i;
2041
LIST Scan;
2042
2043
#ifdef CHECK
2044
if (!clause_IsClause(Clause, FlagStore, Precedence)) {
2045
misc_StartErrorReport();
2046
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
2047
misc_ErrorReport("\n Illegal input.");
2048
misc_FinishErrorReport();
2049
}
2050
if ((StartIndex < clause_FirstLitIndex())
2051
|| (EndIndex > clause_LastLitIndex(Clause))) {
2052
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
2053
misc_ErrorReport("\n Illegal input.");
2054
misc_ErrorReport("\n Index out of range.");
2055
misc_FinishErrorReport();
2056
}
2057
if (list_Length(Replacement) != (EndIndex - StartIndex + 1)) {
2058
misc_StartErrorReport();
2059
misc_ErrorReport("\n In clause_ReplaceLiteralSubSet:");
2060
misc_ErrorReport("\n Illegal input. Replacement list size");
2061
misc_ErrorReport("\n and set size don't match");
2062
misc_FinishErrorReport();
2063
}
2064
#endif
2065
2066
for (i = StartIndex, Scan = Replacement;
2067
i <= EndIndex;
2068
i++, Scan = list_Cdr(Scan)) {
2069
clause_SetLiteral(Clause, i, list_Car(Scan));
2070
}
2071
}
2072
2073
static __inline__ BOOL clause_LiteralsCompare(LITERAL Left, LITERAL Right)
2074
/**************************************************************
2075
INPUT: Two literals.
2076
RETURNS: TRUE if Left <= Right, FALSE otherwise.
2077
EFFECT: Compares literals by comparing their terms' arities.
2078
***************************************************************/
2079
{
2080
#ifdef CHECK
2081
if (!(clause_LiteralIsLiteral(Left) && clause_LiteralIsLiteral(Right))) {
2082
misc_StartErrorReport();
2083
misc_ErrorReport("\n In clause_LiteralsCompare:");
2084
misc_ErrorReport("\n Illegal input.");
2085
misc_FinishErrorReport();
2086
}
2087
#endif
2088
2089
return term_CompareAbstractLEQ(clause_LiteralSignedAtom(Left),
2090
clause_LiteralSignedAtom(Right));
2091
}
2092
2093
static __inline__ void clause_FixLiteralSubsetOrder(CLAUSE Clause,
2094
int StartIndex,
2095
int EndIndex,
2096
FLAGSTORE FlagStore,
2097
PRECEDENCE Precedence)
2098
/**************************************************************
2099
INPUT: A clause, a start index, an end index a flag store
2100
and a precedence.
2101
RETURNS: None.
2102
EFFECT: Sorts literals with indices between (and including)
2103
<StartIndex> and <EndIndex> with respect to an abstract
2104
list representation of terms that identifies function
2105
symbols with their arity.
2106
***************************************************************/
2107
{
2108
2109
LIST literals;
2110
2111
#ifdef CHECK
2112
if ((StartIndex < clause_FirstLitIndex())
2113
|| (EndIndex > clause_LastLitIndex(Clause))) {
2114
misc_ErrorReport("\n In clause_FixLiteralSubSetOrder:");
2115
misc_ErrorReport("\n Illegal input.");
2116
misc_ErrorReport("\n Index out of range.");
2117
misc_FinishErrorReport();
2118
}
2119
#endif
2120
2121
/* Get the literals */
2122
literals = clause_GetLiteralSubSetList(Clause, StartIndex, EndIndex, FlagStore, Precedence);
2123
2124
/* Sort them */
2125
literals = list_Sort(literals, (BOOL (*) (POINTER, POINTER)) clause_LiteralsCompare);
2126
2127
/* Replace clause literals in subset with sorted literals */
2128
clause_ReplaceLiteralSubSet(Clause, StartIndex, EndIndex, literals, FlagStore, Precedence);
2129
2130
list_Delete(literals);
2131
}
2132
2133
void clause_FixLiteralOrder(CLAUSE Clause, FLAGSTORE FlagStore, PRECEDENCE Precedence)
2134
/**************************************************************
2135
INPUT: A clause, a flag store, and a precedence.
2136
RETURNS: None.
2137
EFFECT: Fixes literal order in a <Clause>. Different literal
2138
types are ordered separately.
2139
***************************************************************/
2140
{
2141
#ifdef CHECK
2142
if (!clause_IsClause(Clause, FlagStore, Precedence)) {
2143
misc_StartErrorReport();
2144
misc_ErrorReport("\n In clause_FixLiteralOrder:");
2145
misc_ErrorReport("\n Illegal input.");
2146
misc_FinishErrorReport();
2147
}
2148
#endif
2149
2150
/* Fix antecedent literal order */
2151
clause_FixLiteralSubsetOrder(Clause,
2152
clause_FirstAntecedentLitIndex(Clause),
2153
clause_LastAntecedentLitIndex(Clause),
2154
FlagStore, Precedence);
2155
2156
/* Fix succedent literal order */
2157
clause_FixLiteralSubsetOrder(Clause,
2158
clause_FirstSuccedentLitIndex(Clause),
2159
clause_LastSuccedentLitIndex(Clause),
2160
FlagStore, Precedence);
2161
2162
/* Fix constraint literal order */
2163
clause_FixLiteralSubsetOrder(Clause,
2164
clause_FirstConstraintLitIndex(Clause),
2165
clause_LastConstraintLitIndex(Clause),
2166
FlagStore, Precedence);
2167
2168
/* Normalize clause, to get variable names right. */
2169
clause_Normalize(Clause);
2170
}
2171
2172
static int clause_CompareByWeight(CLAUSE Left, CLAUSE Right)
2173
/**************************************************************
2174
INPUT: Two clauses.
2175
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2176
EFFECT: Compares two clauses by their weight.
2177
***************************************************************/
2178
{
2179
NAT lweight, rweight;
2180
int result;
2181
2182
lweight = clause_Weight(Left);
2183
rweight = clause_Weight(Right);
2184
2185
if (lweight < rweight) {
2186
result = -1;
2187
}
2188
else if (lweight > rweight) {
2189
result = 1;
2190
}
2191
else {
2192
result = 0;
2193
}
2194
2195
return result;
2196
}
2197
2198
static int clause_CompareByClausePartSize(CLAUSE Left, CLAUSE Right)
2199
/**************************************************************
2200
INPUT: Two clauses.
2201
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2202
EFFECT: Compares two clauses by the number of literals in
2203
the antecedent, succedent and constraint.
2204
***************************************************************/
2205
{
2206
int lsize, rsize;
2207
2208
lsize = clause_NumOfAnteLits(Left);
2209
rsize = clause_NumOfAnteLits(Right);
2210
if (lsize < rsize)
2211
return -1;
2212
else if (lsize > rsize)
2213
return 1;
2214
2215
lsize = clause_NumOfSuccLits(Left);
2216
rsize = clause_NumOfSuccLits(Right);
2217
2218
if (lsize < rsize)
2219
return -1;
2220
else if (lsize > rsize)
2221
return 1;
2222
2223
lsize = clause_NumOfConsLits(Left);
2224
rsize = clause_NumOfConsLits(Right);
2225
2226
if (lsize < rsize)
2227
return -1;
2228
else if (lsize > rsize)
2229
return 1;
2230
2231
return 0;
2232
}
2233
2234
void clause_CountSymbols(CLAUSE Clause)
2235
/**************************************************************
2236
INPUT: A clause.
2237
RETURNS: None.
2238
EFFECT: Counts the non-variable symbols in the clause, and
2239
increases their counts accordingly.
2240
***************************************************************/
2241
{
2242
int i;
2243
2244
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
2245
LITERAL l;
2246
TERM t;
2247
2248
l = clause_GetLiteral(Clause, i);
2249
if (clause_LiteralIsPredicate(l)) {
2250
SYMBOL S;
2251
2252
S = clause_LiteralPredicate(l);
2253
symbol_SetCount(S, symbol_GetCount(S) + 1);
2254
}
2255
2256
t = clause_GetLiteralAtom(Clause, i);
2257
2258
term_CountSymbols(t);
2259
}
2260
}
2261
2262
2263
LIST clause_ListOfPredicates(CLAUSE Clause)
2264
/**************************************************************
2265
INPUT: A clause.
2266
RETURNS: A list of symbols.
2267
EFFECT: Creates a list of predicates occurring in the clause.
2268
A predicate occurs several times in the list, if
2269
it does so in the clause.
2270
***************************************************************/
2271
{
2272
LIST preds;
2273
int i;
2274
2275
preds = list_Nil();
2276
2277
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
2278
LITERAL l;
2279
2280
l = clause_GetLiteral(Clause, i);
2281
if (clause_LiteralIsPredicate(l)) {
2282
preds = list_Cons((POINTER) clause_LiteralPredicate(l), preds);
2283
}
2284
}
2285
2286
return preds;
2287
}
2288
2289
LIST clause_ListOfConstants(CLAUSE Clause)
2290
/**************************************************************
2291
INPUT: A clause.
2292
RETURNS: A list of symbols.
2293
EFFECT: Creates a list of constants occurring in the clause.
2294
A constant occurs several times in the list, if
2295
it does so in the clause.
2296
***************************************************************/
2297
{
2298
LIST consts;
2299
int i;
2300
2301
consts = list_Nil();
2302
2303
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
2304
TERM t;
2305
2306
t = clause_GetLiteralAtom(Clause, i);
2307
2308
consts = list_Nconc(term_ListOfConstants(t), consts);
2309
}
2310
2311
return consts;
2312
}
2313
2314
LIST clause_ListOfVariables(CLAUSE Clause)
2315
/**************************************************************
2316
INPUT: A clause.
2317
RETURNS: A list of variables.
2318
EFFECT: Creates a list of variables occurring in the clause.
2319
A variable occurs several times in the list, if
2320
it does so in the clause.
2321
***************************************************************/
2322
{
2323
LIST vars;
2324
int i;
2325
2326
vars = list_Nil();
2327
2328
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
2329
TERM t;
2330
2331
t = clause_GetLiteralAtom(Clause, i);
2332
2333
vars = list_Nconc(term_ListOfVariables(t), vars);
2334
}
2335
2336
return vars;
2337
}
2338
2339
LIST clause_ListOfFunctions(CLAUSE Clause)
2340
/**************************************************************
2341
INPUT: A clause.
2342
RETURNS: A list of symbols.
2343
EFFECT: Creates a list of functions occurring in the clause.
2344
A function occurs several times in the list, if
2345
it does so in the clause.
2346
***************************************************************/
2347
{
2348
LIST funs;
2349
int i;
2350
2351
funs = list_Nil();
2352
2353
for (i=clause_FirstLitIndex(); i<=clause_LastLitIndex(Clause); i++) {
2354
TERM t;
2355
2356
t = clause_GetLiteralAtom(Clause, i);
2357
2358
funs = list_Nconc(term_ListOfFunctions(t), funs);
2359
}
2360
2361
return funs;
2362
}
2363
2364
static int clause_CompareByPredicateDistribution(CLAUSE Left, CLAUSE Right)
2365
/**************************************************************
2366
INPUT: Two clauses.
2367
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2368
EFFECT: Compares two clauses by the frequency of predicates.
2369
***************************************************************/
2370
{
2371
LIST lpreds, rpreds;
2372
int result;
2373
2374
lpreds = clause_ListOfPredicates(Left);
2375
rpreds = clause_ListOfPredicates(Right);
2376
2377
result = list_CompareMultisetsByElementDistribution(lpreds, rpreds);
2378
2379
list_Delete(lpreds);
2380
list_Delete(rpreds);
2381
2382
return result;
2383
}
2384
2385
static int clause_CompareByConstantDistribution(CLAUSE Left, CLAUSE Right)
2386
/**************************************************************
2387
INPUT: Two clauses.
2388
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2389
EFFECT: Compares two clauses by the frequency of constants.
2390
***************************************************************/
2391
{
2392
LIST lconsts, rconsts;
2393
int result;
2394
2395
lconsts = clause_ListOfConstants(Left);
2396
rconsts = clause_ListOfConstants(Right);
2397
2398
result = list_CompareMultisetsByElementDistribution(lconsts, rconsts);
2399
2400
list_Delete(lconsts);
2401
list_Delete(rconsts);
2402
2403
return result;
2404
}
2405
2406
static int clause_CompareByVariableDistribution(CLAUSE Left, CLAUSE Right)
2407
/**************************************************************
2408
INPUT: Two clauses.
2409
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2410
EFFECT: Compares two clauses by the frequency of variables.
2411
***************************************************************/
2412
{
2413
LIST lvars, rvars;
2414
int result;
2415
2416
lvars = clause_ListOfVariables(Left);
2417
rvars = clause_ListOfVariables(Right);
2418
2419
result = list_CompareMultisetsByElementDistribution(lvars, rvars);
2420
2421
list_Delete(lvars);
2422
list_Delete(rvars);
2423
2424
return result;
2425
}
2426
2427
static int clause_CompareByFunctionDistribution(CLAUSE Left, CLAUSE Right)
2428
/**************************************************************
2429
INPUT: Two clauses.
2430
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2431
EFFECT: Compares two clauses by the frequency of functions.
2432
***************************************************************/
2433
{
2434
LIST lfuns, rfuns;
2435
int result;
2436
2437
lfuns = clause_ListOfFunctions(Left);
2438
rfuns = clause_ListOfFunctions(Right);
2439
2440
result = list_CompareMultisetsByElementDistribution(lfuns, rfuns);
2441
2442
list_Delete(lfuns);
2443
list_Delete(rfuns);
2444
2445
return result;
2446
}
2447
2448
static int clause_CompareByDepth(CLAUSE Left, CLAUSE Right)
2449
/**************************************************************
2450
INPUT: Two clauses.
2451
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2452
EFFECT: Compares two clauses by their depth.
2453
***************************************************************/
2454
{
2455
if (clause_Depth(Left) < clause_Depth(Right))
2456
return -1;
2457
else if (clause_Depth(Left) > clause_Depth(Right))
2458
return 1;
2459
2460
return 0;
2461
}
2462
2463
static int clause_CompareByMaxVar(CLAUSE Left, CLAUSE Right)
2464
/**************************************************************
2465
INPUT: Two clauses.
2466
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2467
EFFECT: Compares two clauses by their maximal variable.
2468
***************************************************************/
2469
{
2470
if (clause_MaxVar(Left) < clause_MaxVar(Right))
2471
return -1;
2472
else if (clause_MaxVar(Left) > clause_MaxVar(Right))
2473
return 1;
2474
2475
return 0;
2476
}
2477
2478
static int clause_CompareByLiterals(CLAUSE Left, CLAUSE Right)
2479
/**************************************************************
2480
INPUT: Two clauses.
2481
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2482
EFFECT: Compares two clauses by comparing their literals
2483
from left to right.
2484
***************************************************************/
2485
{
2486
int firstlitleft, lastlitleft;
2487
int firstlitright, lastlitright;
2488
int i, j;
2489
int result;
2490
2491
result = 0;
2492
2493
/* Compare sorted literals from right to left */
2494
2495
firstlitleft = clause_FirstLitIndex();
2496
lastlitleft = clause_LastLitIndex(Left);
2497
firstlitright = clause_FirstLitIndex();
2498
lastlitright = clause_LastLitIndex(Right);
2499
2500
for (i = lastlitleft, j = lastlitright;
2501
i >= firstlitleft && j >= firstlitright;
2502
--i, --j) {
2503
TERM lterm, rterm;
2504
2505
lterm = clause_GetLiteralTerm(Left, i);
2506
rterm = clause_GetLiteralTerm(Right, j);
2507
2508
result = term_CompareAbstract(lterm, rterm);
2509
2510
if (result != 0)
2511
break;
2512
}
2513
2514
if (result == 0) {
2515
/* All literals compared equal, so check if someone has
2516
uncompared literals left over.
2517
*/
2518
if ( i > j) {
2519
/* Left clause has uncompared literals left over. */
2520
result = 1;
2521
}
2522
else if (i < j) {
2523
/* Right clause has uncompared literals left over. */
2524
result = -1;
2525
}
2526
}
2527
2528
return result;
2529
}
2530
2531
static int clause_CompareBySymbolOccurences(CLAUSE Left, CLAUSE Right)
2532
/**************************************************************
2533
INPUT: Two clauses.
2534
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2535
EFFECT: Compares two clauses by comparing the occurrences of
2536
symbols in their respective literals from left to
2537
right. If a symbol occurs less frequently than
2538
its positional equivalent in the other clause,
2539
then the first clause is smaller.
2540
***************************************************************/
2541
{
2542
int firstlitleft, lastlitleft;
2543
int firstlitright, lastlitright;
2544
int i, j;
2545
int result;
2546
2547
result = 0;
2548
2549
/* Compare sorted literals from right to left */
2550
2551
firstlitleft = clause_FirstLitIndex();
2552
lastlitleft = clause_LastLitIndex(Left);
2553
firstlitright = clause_FirstLitIndex();
2554
lastlitright = clause_LastLitIndex(Right);
2555
2556
for (i = lastlitleft, j = lastlitright;
2557
i >= firstlitleft && j >= firstlitright;
2558
--i, --j) {
2559
TERM lterm, rterm;
2560
LITERAL llit, rlit;
2561
2562
llit = clause_GetLiteral(Left, i);
2563
rlit = clause_GetLiteral(Right, j);
2564
2565
if (clause_LiteralIsPredicate(llit)) {
2566
if (clause_LiteralIsPredicate(rlit)) {
2567
if (symbol_GetCount(clause_LiteralPredicate(llit))
2568
< symbol_GetCount(clause_LiteralPredicate(rlit))) {
2569
return -1;
2570
}
2571
else if (symbol_GetCount(clause_LiteralPredicate(llit))
2572
> symbol_GetCount(clause_LiteralPredicate(rlit))) {
2573
return 1;
2574
}
2575
}
2576
}
2577
2578
lterm = clause_GetLiteralTerm(Left, i);
2579
rterm = clause_GetLiteralTerm(Right, j);
2580
2581
result = term_CompareBySymbolOccurences(lterm, rterm);
2582
2583
if (result != 0)
2584
break;
2585
}
2586
2587
return result;
2588
}
2589
2590
int clause_CompareAbstract(CLAUSE Left, CLAUSE Right)
2591
/**************************************************************
2592
INPUT: Two clauses.
2593
RETURNS: 1 if left > right, -1 if left < right, 0 otherwise.
2594
EFFECT: Compares two clauses by their weight. If the weight
2595
is equal, it compares the clauses by the arity of
2596
their literals from right to left.
2597
CAUTION: Expects clause literal order to be fixed.
2598
***************************************************************/
2599
{
2600
2601
typedef int (*CLAUSE_COMPARE_FUNCTION) (CLAUSE, CLAUSE);
2602
2603
static const CLAUSE_COMPARE_FUNCTION clause_compare_functions [] = {
2604
clause_CompareByWeight,
2605
clause_CompareByDepth,
2606
clause_CompareByMaxVar,
2607
clause_CompareByClausePartSize,
2608
clause_CompareByLiterals,
2609
clause_CompareBySymbolOccurences,
2610
clause_CompareByPredicateDistribution,
2611
clause_CompareByConstantDistribution,
2612
clause_CompareByFunctionDistribution,
2613
clause_CompareByVariableDistribution,
2614
};
2615
2616
int result;
2617
int i;
2618
int functions;
2619
2620
result = 0;
2621
functions = sizeof(clause_compare_functions)/sizeof(CLAUSE_COMPARE_FUNCTION);
2622
2623
for (i = 0; i < functions; i++) {
2624
result = clause_compare_functions[i](Left, Right);
2625
2626
if ( result != 0) {
2627
return result;
2628
}
2629
}
2630
2631
return 0;
2632
}
2633
2634
2635
/**************************************************************/
2636
/* Clause functions */
2637
/**************************************************************/
2638
2639
void clause_Init(void)
2640
/**************************************************************
2641
INPUT: None.
2642
RETURNS: Nothing.
2643
SUMMARY: Initializes the clause counter and other variables
2644
from this module.
2645
***************************************************************/
2646
{
2647
int i;
2648
clause_SetCounter(1);
2649
clause_STAMPID = term_GetStampID();
2650
for (i = 0; i <= clause_MAXWEIGHT; i++)
2651
clause_SORT[i] = list_Nil();
2652
}
2653
2654
2655
CLAUSE clause_CreateBody(int ClauseLength)
2656
/**************************************************************
2657
INPUT: The number of literals as integer.
2658
RETURNS: A new generated clause node for 'ClauseLength'
2659
MEMORY: Allocates a CLAUSE_NODE and the needed array for LITERALs.
2660
*************************************************************/
2661
{
2662
CLAUSE Result;
2663
2664
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
2665
2666
Result->clausenumber = clause_IncreaseCounter();
2667
Result->maxVar = symbol_GetInitialStandardVarCounter();
2668
Result->flags = 0;
2669
Result->depth = 0;
2670
Result->splitpotential = 0.0;
2671
clause_InitSplitData(Result);
2672
Result->weight = clause_WEIGHTUNDEFINED;
2673
Result->parentCls = list_Nil();
2674
Result->parentLits = list_Nil();
2675
2676
Result->c = 0;
2677
Result->a = 0;
2678
Result->s = 0;
2679
2680
if (ClauseLength != 0)
2681
Result->literals =
2682
(LITERAL *)memory_Malloc((ClauseLength) * sizeof(LITERAL));
2683
2684
clause_SetFromInput(Result);
2685
2686
return Result;
2687
}
2688
2689
2690
2691
CLAUSE clause_CreateAux(LIST Constraint, LIST Antecedent, LIST Succedent,
2692
FLAGSTORE Flags, PRECEDENCE Precedence, BOOL VarIsConst)
2693
/**************************************************************
2694
INPUT: Three lists of pointers to atoms, a flag store,
2695
a precedence and a flag
2696
RETURNS: The new generated clause.
2697
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
2698
uses the terms from the lists, additionally allocates
2699
termnodes for the fol_Not() in Const. and Ante.
2700
CAUTION: If <VarIsConst> is TRUE then variables are interpreted
2701
as constants
2702
*************************************************************/
2703
{
2704
CLAUSE Result;
2705
int i, c, a, s;
2706
2707
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
2708
2709
Result->clausenumber = clause_IncreaseCounter();
2710
Result->flags = 0;
2711
Result->depth = 0;
2712
Result->weight = clause_WEIGHTUNDEFINED;
2713
Result->splitpotential = 0.0;
2714
clause_InitSplitData(Result);
2715
Result->parentCls = list_Nil();
2716
Result->parentLits = list_Nil();
2717
2718
Result->c = (c = list_Length(Constraint));
2719
Result->a = (a = list_Length(Antecedent));
2720
Result->s = (s = list_Length(Succedent));
2721
2722
if (!clause_IsEmptyClause(Result))
2723
Result->literals =
2724
(LITERAL *) memory_Malloc((c+a+s) * sizeof(LITERAL));
2725
2726
for (i = 0; i < c; i++) {
2727
Result->literals[i] =
2728
clause_LiteralCreate(term_Create(fol_Not(),
2729
list_List((TERM)list_Car(Constraint))),Result);
2730
Constraint = list_Cdr(Constraint);
2731
}
2732
2733
a += c;
2734
for ( ; i < a; i++) {
2735
Result->literals[i] =
2736
clause_LiteralCreate(term_Create(fol_Not(),
2737
list_List((TERM)list_Car(Antecedent))), Result);
2738
Antecedent = list_Cdr(Antecedent);
2739
}
2740
2741
s += a;
2742
for ( ; i < s; i++) {
2743
Result->literals[i] =
2744
clause_LiteralCreate((TERM) list_Car(Succedent), Result);
2745
Succedent = list_Cdr(Succedent);
2746
}
2747
2748
if(VarIsConst)
2749
clause_OrientAndReInitSkolem(Result, Flags, Precedence);
2750
else
2751
clause_OrientAndReInit(Result, Flags, Precedence);
2752
2753
clause_SetFromInput(Result);
2754
2755
return Result;
2756
}
2757
2758
2759
CLAUSE clause_Create(LIST Constraint, LIST Antecedent, LIST Succedent,
2760
FLAGSTORE Flags, PRECEDENCE Precedence)
2761
/**************************************************************
2762
INPUT: Three lists of pointers to atoms, a flag store and
2763
a precedence.
2764
RETURNS: The new generated clause.
2765
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
2766
uses the terms from the lists, additionally allocates
2767
termnodes for the fol_Not() in Const. and Ante.
2768
*************************************************************/
2769
{
2770
return clause_CreateAux(Constraint, Antecedent, Succedent,
2771
Flags, Precedence, FALSE);
2772
}
2773
2774
2775
CLAUSE clause_CreateSkolem(LIST Constraint, LIST Antecedent, LIST Succedent,
2776
FLAGSTORE Flags, PRECEDENCE Precedence)
2777
/**************************************************************
2778
INPUT: Three lists of pointers to atoms, a flag store and
2779
a precedence.
2780
RETURNS: The new generated clause.
2781
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
2782
uses the terms from the lists, additionally allocates
2783
termnodes for the fol_Not() in Const. and Ante.
2784
CAUTION: Variables are interpreted to as constants
2785
*************************************************************/
2786
{
2787
return clause_CreateAux(Constraint, Antecedent, Succedent,
2788
Flags, Precedence, TRUE);
2789
}
2790
2791
2792
CLAUSE clause_CreateCrude(LIST Constraint, LIST Antecedent, LIST Succedent,
2793
BOOL Con)
2794
/**************************************************************
2795
INPUT: Three lists of pointers to literals (!) and a Flag indicating
2796
whether the clause comes from the conjecture part of of problem.
2797
It is assumed that Constraint and Antecedent literals are negative,
2798
whereas Succedent literals are positive.
2799
RETURNS: The new generated clause, where a clause_OrientAndReInit has still
2800
to be performed, i.e., variables are not normalized, maximal literal
2801
flags not set, equations not oriented, the weight is not set.
2802
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
2803
uses the terms from the lists, additionally allocates
2804
termnodes for the fol_Not() in Const. and Ante.
2805
****************************************************************/
2806
{
2807
CLAUSE Result;
2808
int i,c,a,s;
2809
2810
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
2811
2812
Result->clausenumber = clause_IncreaseCounter();
2813
Result->flags = 0;
2814
if (Con)
2815
clause_SetFlag(Result, CONCLAUSE);
2816
2817
Result->depth = 0;
2818
Result->weight = clause_WEIGHTUNDEFINED;
2819
Result->splitpotential = 0.0;
2820
clause_InitSplitData(Result);
2821
Result->parentCls = list_Nil();
2822
Result->parentLits = list_Nil();
2823
2824
Result->c = (c = list_Length(Constraint));
2825
Result->a = (a = list_Length(Antecedent));
2826
Result->s = (s = list_Length(Succedent));
2827
2828
if (!clause_IsEmptyClause(Result))
2829
Result->literals = (LITERAL *)memory_Malloc((c+a+s) * sizeof(LITERAL));
2830
2831
for (i = 0; i < c; i++) {
2832
Result->literals[i] =
2833
clause_LiteralCreate(list_Car(Constraint),Result);
2834
Constraint = list_Cdr(Constraint);
2835
}
2836
2837
a += c;
2838
for ( ; i < a; i++) {
2839
Result->literals[i] =
2840
clause_LiteralCreate(list_Car(Antecedent), Result);
2841
Antecedent = list_Cdr(Antecedent);
2842
}
2843
2844
s += a;
2845
for ( ; i < s; i++) {
2846
Result->literals[i] = clause_LiteralCreate(list_Car(Succedent), Result);
2847
Succedent = list_Cdr(Succedent);
2848
}
2849
2850
clause_SetFromInput(Result);
2851
2852
return Result;
2853
}
2854
2855
2856
CLAUSE clause_CreateUnnormalized(LIST Constraint, LIST Antecedent,
2857
LIST Succedent)
2858
/**************************************************************
2859
INPUT: Three lists of pointers to atoms.
2860
RETURNS: The new generated clause.
2861
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
2862
uses the terms from the lists, additionally allocates
2863
termnodes for the fol_Not() in Const. and Ante.
2864
CAUTION: The weight of the clause is not set correctly and
2865
equations are not oriented!
2866
****************************************************************/
2867
{
2868
CLAUSE Result;
2869
int i,c,a,s;
2870
2871
Result = (CLAUSE)memory_Malloc(sizeof(CLAUSE_NODE));
2872
2873
Result->clausenumber = clause_IncreaseCounter();
2874
Result->flags = 0;
2875
Result->depth = 0;
2876
Result->weight = clause_WEIGHTUNDEFINED;
2877
Result->splitpotential = 0.0;
2878
clause_InitSplitData(Result);
2879
Result->parentCls = list_Nil();
2880
Result->parentLits = list_Nil();
2881
2882
Result->c = (c = list_Length(Constraint));
2883
Result->a = (a = list_Length(Antecedent));
2884
Result->s = (s = list_Length(Succedent));
2885
2886
if (!clause_IsEmptyClause(Result)) {
2887
Result->literals = (LITERAL *)memory_Malloc((c+a+s) * sizeof(LITERAL));
2888
2889
for (i = 0; i < c; i++) {
2890
Result->literals[i] =
2891
clause_LiteralCreate(term_Create(fol_Not(),
2892
list_List(list_Car(Constraint))),
2893
Result);
2894
Constraint = list_Cdr(Constraint);
2895
}
2896
2897
a += c;
2898
for ( ; i < a; i++) {
2899
Result->literals[i] =
2900
clause_LiteralCreate(term_Create(fol_Not(),
2901
list_List(list_Car(Antecedent))),
2902
Result);
2903
Antecedent = list_Cdr(Antecedent);
2904
}
2905
2906
s += a;
2907
for ( ; i < s; i++) {
2908
Result->literals[i] =
2909
clause_LiteralCreate((TERM)list_Car(Succedent), Result);
2910
Succedent = list_Cdr(Succedent);
2911
}
2912
clause_UpdateMaxVar(Result);
2913
}
2914
2915
return Result;
2916
}
2917
2918
CLAUSE clause_CreateFromLiteralLists(LIST Constraint, LIST Antecedent,
2919
LIST Succedent, BOOL Conclause,
2920
TERM selected)
2921
/**************************************************************
2922
INPUT: Three lists of literals, a boolean flag indicating
2923
whether the clause is a conjecture clause, and a
2924
selected term.
2925
RETURNS: The new generated clause.
2926
EFFECT: The result clause will be normalized and the maximal
2927
variable will be set. If the flag is set, the clause
2928
will be set as a conjecture clause. If the selected
2929
term is not NULL, its corresponding literal will be
2930
selected.
2931
This function is intended for the parser for creating
2932
clauses at a time when the ordering and weight flags
2933
aren't determined finally.
2934
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
2935
uses the terms from the lists.
2936
****************************************************************/
2937
{
2938
CLAUSE Result;
2939
2940
Result = clause_CreateUnnormalized(Constraint, Antecedent, Succedent);
2941
2942
if(Conclause)
2943
clause_SetFlag(Result, CONCLAUSE);
2944
2945
if (selected != (TERM) NULL) {
2946
int i;
2947
for (i = clause_FirstAntecedentLitIndex(Result);
2948
i <= clause_LastAntecedentLitIndex(Result);
2949
++i) {
2950
TERM negated;
2951
negated = clause_GetLiteralAtom(Result, i);
2952
if (negated == selected) {
2953
clause_LiteralSetFlag(clause_GetLiteral(Result, i),
2954
LITSELECT);
2955
clause_SetFlag(Result, CLAUSESELECT);
2956
break;
2957
}
2958
}
2959
}
2960
2961
clause_Normalize(Result);
2962
clause_UpdateMaxVar(Result);
2963
clause_SetFromInput(Result);
2964
2965
return Result;
2966
}
2967
2968
CLAUSE clause_CreateFromLiterals(LIST LitList, BOOL Sorts, BOOL Conclause,
2969
BOOL Ordering, FLAGSTORE Flags,
2970
PRECEDENCE Precedence)
2971
/**************************************************************
2972
INPUT: A list of literals, three boolean flags indicating whether
2973
sort constraint literals should be generated, whether the
2974
clause is a conjecture clause, whether the ordering information
2975
should be established, a flag store and a precedence.
2976
RETURNS: The new generated clause.
2977
EFFECT: The result clause will be normalized and the maximal
2978
variable will be set. If <Ordering> is FALSE no additional
2979
initializations will be done. This mode is intended for
2980
the parser for creating clauses at a time when the ordering
2981
and weight flags aren't determined finally.
2982
Only if <Ordering> is TRUE the equations will be oriented,
2983
the maximal literals will be marked and the clause weight
2984
will be set correctly.
2985
MEMORY: Allocates a CLAUSE_NODE and the needed LITERAL_NODEs,
2986
uses the terms from the lists.
2987
****************************************************************/
2988
{
2989
CLAUSE Result;
2990
LIST Antecedent,Succedent,Constraint;
2991
TERM Atom;
2992
2993
Antecedent = list_Nil();
2994
Succedent = list_Nil();
2995
Constraint = list_Nil();
2996
2997
while (!list_Empty(LitList)) {
2998
if (term_TopSymbol(list_Car(LitList)) == fol_Not()) {
2999
Atom = term_FirstArgument(list_Car(LitList));
3000
if (Sorts && symbol_IsBaseSort(term_TopSymbol(Atom)) && term_IsVariable(term_FirstArgument(Atom)))
3001
Constraint = list_Cons(list_Car(LitList),Constraint);
3002
else
3003
Antecedent = list_Cons(list_Car(LitList),Antecedent);
3004
}
3005
else
3006
Succedent = list_Cons(list_Car(LitList),Succedent);
3007
LitList = list_Cdr(LitList);
3008
}
3009
3010
Constraint = list_NReverse(Constraint);
3011
Antecedent = list_NReverse(Antecedent);
3012
Succedent = list_NReverse(Succedent);
3013
Result = clause_CreateCrude(Constraint, Antecedent, Succedent, Conclause);
3014
3015
list_Delete(Constraint);
3016
list_Delete(Antecedent);
3017
list_Delete(Succedent);
3018
3019
if (Ordering)
3020
clause_OrientAndReInit(Result, Flags, Precedence);
3021
else {
3022
clause_Normalize(Result);
3023
clause_UpdateMaxVar(Result);
3024
}
3025
3026
return Result;
3027
}
3028
3029
void clause_SetSortConstraint(CLAUSE Clause, BOOL Strong, FLAGSTORE Flags,
3030
PRECEDENCE Precedence)
3031
/**************************************************************
3032
INPUT: A clause, a flag indicating whether also negative
3033
monadic literals with a real term argument should be
3034
put in the sort constraint, a flag store and a precedence.
3035
RETURNS: Nothing.
3036
EFFECT: Negative monadic literals are put in the sort constraint.
3037
****************************************************************/
3038
{
3039
LITERAL ActLit,Help;
3040
TERM ActAtom;
3041
int i,k,NewConLits;
3042
3043
3044
#ifdef CHECK
3045
if (!clause_IsUnorderedClause(Clause)) {
3046
misc_StartErrorReport();
3047
misc_ErrorReport("\n In clause_SetSortConstraint:");
3048
misc_ErrorReport("\n Illegal input.");
3049
misc_FinishErrorReport();
3050
}
3051
#endif
3052
3053
i = clause_LastConstraintLitIndex(Clause);
3054
NewConLits = 0;
3055
3056
for (k=clause_FirstAntecedentLitIndex(Clause);k<=clause_LastAntecedentLitIndex(Clause);k++) {
3057
ActLit = clause_GetLiteral(Clause,k);
3058
ActAtom = clause_LiteralAtom(ActLit);
3059
if (symbol_IsBaseSort(term_TopSymbol(ActAtom)) &&
3060
(Strong || term_IsVariable(term_FirstArgument(ActAtom)))) {
3061
if (++i != k) {
3062
Help = clause_GetLiteral(Clause,i);
3063
clause_SetLiteral(Clause,i,ActLit);
3064
clause_SetLiteral(Clause,k,Help);
3065
}
3066
NewConLits++;
3067
}
3068
}
3069
3070
clause_SetNumOfConsLits(Clause, clause_NumOfConsLits(Clause) + NewConLits);
3071
clause_SetNumOfAnteLits(Clause, clause_NumOfAnteLits(Clause) - NewConLits);
3072
clause_ReInit(Clause, Flags, Precedence);
3073
3074
#ifdef CHECK
3075
if (!clause_IsUnorderedClause(Clause)) {
3076
misc_StartErrorReport();
3077
misc_ErrorReport("\n In clause_SetSortConstraint:");
3078
misc_ErrorReport("\n Illegal computations.");
3079
misc_FinishErrorReport();
3080
}
3081
#endif
3082
3083
}
3084
3085
3086
3087
void clause_Delete(CLAUSE Clause)
3088
/**************************************************************
3089
INPUT: A Clause.
3090
RETURNS: Nothing.
3091
MEMORY: Frees the memory of the clause.
3092
***************************************************************/
3093
{
3094
int i, n;
3095
3096
#ifdef CHECK
3097
if (!clause_IsUnorderedClause(Clause)) { /* Clause may be a byproduct of some hyper rule */
3098
misc_StartErrorReport();
3099
misc_ErrorReport("\n In clause_Delete:");
3100
misc_ErrorReport("\n Illegal input.");
3101
misc_FinishErrorReport();
3102
}
3103
#endif
3104
3105
n = clause_Length(Clause);
3106
3107
for (i = 0; i < n; i++)
3108
clause_LiteralDelete(clause_GetLiteral(Clause,i));
3109
3110
clause_FreeLitArray(Clause);
3111
3112
list_Delete(clause_ParentClauses(Clause));
3113
list_Delete(clause_ParentLiterals(Clause));
3114
#ifdef CHECK
3115
if ((Clause->splitfield != NULL) && (Clause->splitfield_length == 0))
3116
{
3117
misc_StartErrorReport();
3118
misc_ErrorReport("\n In clause_Delete:");
3119
misc_ErrorReport("\n Illegal splitfield_length.");
3120
misc_FinishErrorReport();
3121
}
3122
if ((Clause->splitfield == NULL) && (Clause->splitfield_length != 0))
3123
{
3124
misc_StartErrorReport();
3125
misc_ErrorReport("\n In clause_Delete:");
3126
misc_ErrorReport("\n Illegal splitfield.");
3127
misc_FinishErrorReport();
3128
}
3129
#endif
3130
if (Clause->splitfield != NULL) {
3131
3132
memory_Free(Clause->splitfield,
3133
sizeof(SPLITFIELDENTRY) * Clause->splitfield_length);
3134
}
3135
clause_Free(Clause);
3136
}
3137
3138
3139
/**************************************************************/
3140
/* Functions to use the sharing for clauses. */
3141
/**************************************************************/
3142
3143
void clause_InsertIntoSharing(CLAUSE Clause, SHARED_INDEX ShIndex,
3144
FLAGSTORE Flags, PRECEDENCE Precedence)
3145
/**************************************************************
3146
INPUT: A Clause, an index, a flag store and a precedence.
3147
RETURNS: Nothing.
3148
SUMMARY: Inserts the unsigned atoms of 'Clause' into the sharing index.
3149
***************************************************************/
3150
{
3151
int i, litnum;
3152
3153
#ifdef CHECK
3154
if (!clause_IsClause(Clause, Flags, Precedence)) {
3155
misc_StartErrorReport();
3156
misc_ErrorReport("\n In clause_Delete:");
3157
misc_ErrorReport("\n Illegal input.");
3158
misc_FinishErrorReport();
3159
}
3160
clause_Check(Clause, Flags, Precedence);
3161
#endif
3162
3163
litnum = clause_Length(Clause);
3164
3165
for (i = 0; i < litnum; i++) {
3166
clause_LiteralInsertIntoSharing(clause_GetLiteral(Clause,i), ShIndex);
3167
}
3168
}
3169
3170
3171
void clause_DeleteFromSharing(CLAUSE Clause, SHARED_INDEX ShIndex,
3172
FLAGSTORE Flags, PRECEDENCE Precedence)
3173
/**************************************************************
3174
INPUT: A Clause, an Index, a flag store and a precedence.
3175
RETURNS: Nothing.
3176
SUMMARY: Deletes 'Clause' and all its literals from the sharing,
3177
frees the memory of 'Clause'.
3178
***************************************************************/
3179
{
3180
int i, length;
3181
3182
#ifdef CHECK
3183
if (!clause_IsClause(Clause, Flags, Precedence)) {
3184
misc_StartErrorReport();
3185
misc_ErrorReport("\n In clause_DeleteFromSharing:");
3186
misc_ErrorReport("\n Illegal input.");
3187
misc_FinishErrorReport();
3188
}
3189
#endif
3190
3191
length = clause_Length(Clause);
3192
3193
for (i = 0; i < length; i++)
3194
clause_LiteralDeleteFromSharing(clause_GetLiteral(Clause,i),ShIndex);
3195
3196
clause_FreeLitArray(Clause);
3197
3198
list_Delete(clause_ParentClauses(Clause));
3199
list_Delete(clause_ParentLiterals(Clause));
3200
#ifdef CHECK
3201
if ((Clause->splitfield != NULL) && (Clause->splitfield_length == 0))
3202
{
3203
misc_StartErrorReport();
3204
misc_ErrorReport("\n In clause_DeleteFromSharing:");
3205
misc_ErrorReport("\n Illegal splitfield_length.");
3206
misc_FinishErrorReport();
3207
}
3208
if ((Clause->splitfield == NULL) && (Clause->splitfield_length != 0))
3209
{
3210
misc_StartErrorReport();
3211
misc_ErrorReport("\n In clause_DeleteFromSharing:");
3212
misc_ErrorReport("\n Illegal splitfield.");
3213
misc_FinishErrorReport();
3214
}
3215
#endif
3216
if (Clause->splitfield != NULL) {
3217
memory_Free(Clause->splitfield,
3218
sizeof(SPLITFIELDENTRY) * Clause->splitfield_length);
3219
}
3220
clause_Free(Clause);
3221
}
3222
3223
3224
void clause_MakeUnshared(CLAUSE Clause, SHARED_INDEX ShIndex)
3225
/**************************************************************
3226
INPUT: A Clause and an Index.
3227
RETURNS: Nothing.
3228
SUMMARY: Deletes the clauses literals from the sharing and
3229
replaces them by unshared copies.
3230
***************************************************************/
3231
{
3232
LITERAL ActLit;
3233
TERM SharedAtom, AtomCopy;
3234
int i,LastAnte,length;
3235
3236
#ifdef CHECK
3237
if (!clause_IsUnorderedClause(Clause)) {
3238
misc_StartErrorReport();
3239
misc_ErrorReport("\n In clause_MakeUnshared:");
3240
misc_ErrorReport("\n Illegal input.");
3241
misc_FinishErrorReport();
3242
}
3243
#endif
3244
3245
LastAnte = clause_LastAntecedentLitIndex(Clause);
3246
length = clause_Length(Clause);
3247
3248
for (i = clause_FirstLitIndex(); i <= LastAnte; i++) {
3249
ActLit = clause_GetLiteral(Clause, i);
3250
SharedAtom = clause_LiteralAtom(ActLit);
3251
AtomCopy = term_Copy(SharedAtom);
3252
sharing_Delete(ActLit, SharedAtom, ShIndex);
3253
clause_LiteralSetNegAtom(ActLit, AtomCopy);
3254
}
3255
3256
for ( ; i < length; i++) {
3257
ActLit = clause_GetLiteral(Clause, i);
3258
SharedAtom = clause_LiteralSignedAtom(ActLit);
3259
AtomCopy = term_Copy(SharedAtom);
3260
sharing_Delete(ActLit, SharedAtom, ShIndex);
3261
clause_LiteralSetPosAtom(ActLit, AtomCopy);
3262
}
3263
}
3264
3265
void clause_MoveSharedClause(CLAUSE Clause, SHARED_INDEX Source,
3266
SHARED_INDEX Destination, FLAGSTORE Flags,
3267
PRECEDENCE Precedence)
3268
/**************************************************************
3269
INPUT: A Clause, two indexes, a flag store, and a precedence.
3270
RETURNS: Nothing.
3271
EFFECT: Deletes <Clause> from <Source> and inserts it into
3272
<Destination>.
3273
***************************************************************/
3274
{
3275
LITERAL Lit;
3276
TERM Atom,Copy;
3277
int i,length;
3278
3279
#ifdef CHECK
3280
if (!clause_IsClause(Clause, Flags, Precedence)) {
3281
misc_StartErrorReport();
3282
misc_ErrorReport("\n In clause_MoveSharedClause:");
3283
misc_ErrorReport("\n Illegal input.");
3284
misc_FinishErrorReport();
3285
}
3286
#endif
3287
3288
length = clause_Length(Clause);
3289
3290
for (i = clause_FirstLitIndex(); i < length; i++) {
3291
Lit = clause_GetLiteral(Clause, i);
3292
Atom = clause_LiteralAtom(Lit);
3293
Copy = term_Copy(Atom); /* sharing_Insert works destructively on <Copy>'s superterms */
3294
clause_LiteralSetAtom(Lit, sharing_Insert(Lit, Copy, Destination));
3295
sharing_Delete(Lit, Atom, Source);
3296
term_Delete(Copy);
3297
}
3298
}
3299
3300
3301
void clause_DeleteSharedLiteral(CLAUSE Clause, int Indice, SHARED_INDEX ShIndex,
3302
FLAGSTORE Flags, PRECEDENCE Precedence)
3303
/**************************************************************
3304
INPUT: A Clause, a literals indice, an Index, a flag store
3305
and a precedence.
3306
RETURNS: Nothing.
3307
SUMMARY: Deletes the shared literal from the clause.
3308
MEMORY: Various.
3309
***************************************************************/
3310
{
3311
3312
#ifdef CHECK
3313
if (!clause_IsClause(Clause, Flags, Precedence)) {
3314
misc_StartErrorReport();
3315
misc_ErrorReport("\n In clause_DeleteSharedLiteral:");
3316
misc_ErrorReport("\n Illegal input.");
3317
misc_FinishErrorReport();
3318
}
3319
#endif
3320
3321
clause_MakeUnshared(Clause, ShIndex);
3322
clause_DeleteLiteral(Clause, Indice, Flags, Precedence);
3323
clause_InsertIntoSharing(Clause, ShIndex, Flags, Precedence);
3324
}
3325
3326
3327
void clause_DeleteClauseList(LIST ClauseList)
3328
/**************************************************************
3329
INPUT: A list of unshared clauses.
3330
RETURNS: Nothing.
3331
SUMMARY: Deletes all clauses in the list and the list.
3332
MEMORY: Frees the lists and the clauses' memory.
3333
***************************************************************/
3334
{
3335
LIST Scan;
3336
3337
for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan))
3338
if (clause_Exists(list_Car(Scan)))
3339
clause_Delete(list_Car(Scan));
3340
3341
list_Delete(ClauseList);
3342
}
3343
3344
3345
void clause_DeleteSharedClauseList(LIST ClauseList, SHARED_INDEX ShIndex,
3346
FLAGSTORE Flags, PRECEDENCE Precedence)
3347
/**************************************************************
3348
INPUT: A list of clauses, an index, a flag store and
3349
a precedence.
3350
RETURNS: Nothing.
3351
SUMMARY: Deletes all clauses in the list from the sharing.
3352
MEMORY: Frees the lists and the clauses' memory.
3353
***************************************************************/
3354
{
3355
LIST Scan;
3356
3357
for (Scan = ClauseList; !list_Empty(Scan); Scan = list_Cdr(Scan))
3358
clause_DeleteFromSharing(list_Car(Scan), ShIndex, Flags, Precedence);
3359
3360
list_Delete(ClauseList);
3361
}
3362
3363
3364
void clause_DeleteAllIndexedClauses(SHARED_INDEX ShIndex, FLAGSTORE Flags,
3365
PRECEDENCE Precedence)
3366
/**************************************************************
3367
INPUT: An Index, a flag store and a precedence.
3368
RETURNS: Nothing.
3369
SUMMARY: Deletes all clauses' terms from the sharing, frees their
3370
memory.
3371
MEMORY: Frees the memory of all clauses with terms in the index.
3372
***************************************************************/
3373
{
3374
LIST TermList,DelList,Scan;
3375
TERM NewVar;
3376
SYMBOL NewVarSymbol;
3377
3378
NewVar = term_CreateStandardVariable();
3379
NewVarSymbol = term_TopSymbol(NewVar);
3380
3381
TermList = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), NewVar);
3382
/* This should yield a list of all terms in the index
3383
and thus the sharing. */
3384
3385
while (!list_Empty(TermList)) {
3386
3387
DelList = sharing_GetDataList(list_Car(TermList), ShIndex);
3388
3389
for (Scan = DelList;
3390
!list_Empty(Scan);
3391
Scan = list_Cdr(Scan))
3392
list_Rplaca(Scan, clause_LiteralOwningClause(list_Car(Scan)));
3393
3394
DelList = list_PointerDeleteDuplicates(DelList);
3395
3396
for (Scan = DelList;
3397
!list_Empty(Scan);
3398
Scan = list_Cdr(Scan))
3399
clause_DeleteFromSharing(list_Car(Scan), ShIndex, Flags, Precedence);
3400
3401
list_Delete(TermList);
3402
3403
TermList = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), NewVar);
3404
3405
list_Delete(DelList);
3406
}
3407
term_Delete(NewVar);
3408
symbol_Delete(NewVarSymbol);
3409
}
3410
3411
3412
void clause_PrintAllIndexedClauses(SHARED_INDEX ShIndex)
3413
/**************************************************************
3414
INPUT: An Index.
3415
RETURNS: Nothing.
3416
SUMMARY: Prints all indexed clauses to stdout.
3417
***************************************************************/
3418
{
3419
LIST TermList,ClList,PrintList,Scan;
3420
TERM NewVar;
3421
SYMBOL NewVarSymbol;
3422
3423
NewVar = term_CreateStandardVariable();
3424
NewVarSymbol = term_TopSymbol(NewVar);
3425
3426
TermList = st_GetInstance(cont_LeftContext(), sharing_Index(ShIndex), NewVar);
3427
/* This should yield a list of all terms in the index
3428
and thus the sharing. */
3429
3430
PrintList = list_Nil();
3431
3432
while (!list_Empty(TermList)) {
3433
3434
ClList = sharing_GetDataList(list_Car(TermList), ShIndex);
3435
3436
for (Scan = ClList;
3437
!list_Empty(Scan);
3438
Scan = list_Cdr(Scan))
3439
list_Rplaca(Scan, clause_LiteralOwningClause(list_Car(Scan)));
3440
3441
PrintList = list_NPointerUnion(ClList, PrintList);
3442
3443
Scan = TermList;
3444
TermList = list_Cdr(TermList);
3445
list_Free(Scan);
3446
}
3447
clause_ListPrint(PrintList);
3448
3449
list_Delete(PrintList);
3450
3451
term_Delete(NewVar);
3452
symbol_Delete(NewVarSymbol);
3453
}
3454
3455
3456
LIST clause_AllIndexedClauses(SHARED_INDEX ShIndex)
3457
/**************************************************************
3458
INPUT: An index
3459
RETURNS: A list of all the clauses in the index
3460
MEMORY: Memory is allocated for the list nodes
3461
***************************************************************/
3462
{
3463
LIST clauselist, scan;
3464
clauselist = sharing_GetAllSuperTerms(ShIndex);
3465
for (scan = clauselist; scan != list_Nil(); scan = list_Cdr(scan))
3466
list_Rplaca(scan, clause_LiteralOwningClause(list_Car(scan)));
3467
clauselist = list_PointerDeleteDuplicates(clauselist);
3468
return clauselist;
3469
}
3470
3471
3472
/**************************************************************/
3473
/* Clause Access Functions */
3474
/**************************************************************/
3475
3476
void clause_DeleteLiteralNN(CLAUSE Clause, int Indice)
3477
/**************************************************************
3478
INPUT: An unshared clause, and a literal index.
3479
RETURNS: Nothing.
3480
EFFECT: The literal is position <Indice> is deleted from <Clause>.
3481
The clause isn't reinitialized afterwards.
3482
MEMORY: The memory of the literal with the 'Indice' and
3483
memory of its atom is freed.
3484
***************************************************************/
3485
{
3486
int i, lc, la, length, shift;
3487
LITERAL *Literals;
3488
3489
#ifdef CHECK
3490
if (!clause_IsUnorderedClause(Clause) || (clause_Length(Clause) <= Indice) ||
3491
Indice < 0) {
3492
misc_StartErrorReport();
3493
misc_ErrorReport("\n In clause_DeleteLiteral:");
3494
misc_ErrorReport("\n Illegal input.");
3495
misc_FinishErrorReport();
3496
}
3497
#endif
3498
3499
lc = clause_LastConstraintLitIndex(Clause);
3500
la = clause_LastAntecedentLitIndex(Clause);
3501
length = clause_Length(Clause);
3502
3503
/* Create a new literal array */
3504
if (length > 1)
3505
Literals = (LITERAL*) memory_Malloc(sizeof(LITERAL) * (length-1));
3506
else
3507
Literals = (LITERAL*) NULL;
3508
3509
/* Copy literals to the new array */
3510
shift = 0;
3511
length--; /* The loop iterates over the new array */
3512
for (i = 0; i < length; i++) {
3513
if (i == Indice)
3514
shift = 1;
3515
Literals[i] = Clause->literals[i+shift];
3516
}
3517
3518
/* Free literal and old array and set new one */
3519
clause_LiteralDelete(clause_GetLiteral(Clause, Indice));
3520
clause_FreeLitArray(Clause);
3521
Clause->literals = Literals;
3522
3523
/* Update clause */
3524
if (Indice <= lc)
3525
clause_SetNumOfConsLits(Clause, clause_NumOfConsLits(Clause) - 1);
3526
else if (Indice <= la)
3527
clause_SetNumOfAnteLits(Clause, clause_NumOfAnteLits(Clause) - 1);
3528
else
3529
clause_SetNumOfSuccLits(Clause, clause_NumOfSuccLits(Clause) - 1);
3530
/* Mark the weight as undefined */
3531
Clause->weight = clause_WEIGHTUNDEFINED;
3532
}
3533
3534
3535
void clause_DeleteLiteral(CLAUSE Clause, int Indice, FLAGSTORE Flags,
3536
PRECEDENCE Precedence)
3537
/**************************************************************
3538
INPUT: An unshared clause, a literals index, a flag store,
3539
and a precedence.
3540
RETURNS: Nothing.
3541
EFFECT: The literal at position <Indice> is deleted from <Clause>.
3542
In contrast to the function clause_DeleteLiteralNN
3543
the clause is reinitialized afterwards.
3544
MEMORY: The memory of the literal with the 'Indice' and memory
3545
of its atom is freed.
3546
***************************************************************/
3547
{
3548
clause_DeleteLiteralNN(Clause, Indice);
3549
clause_ReInit(Clause, Flags, Precedence);
3550
}
3551
3552
3553
void clause_DeleteLiterals(CLAUSE Clause, LIST Indices, FLAGSTORE Flags,
3554
PRECEDENCE Precedence)
3555
/**************************************************************
3556
INPUT: An unshared clause, a list of literal indices a
3557
flag store and a precedence.
3558
RETURNS: Nothing.
3559
EFFECT: The literals given by <Indices> are deleted.
3560
The clause is reinitialized afterwards.
3561
MEMORY: The memory of the literals with the 'Indice' and
3562
memory of its atom is freed.
3563
***************************************************************/
3564
{
3565
LITERAL *NewLits;
3566
int i, j, nc, na, ns, lc, la, olength, nlength;
3567
3568
#ifdef CHECK
3569
LIST Scan;
3570
if (!list_IsSetOfPointers(Indices)) {
3571
misc_StartErrorReport();
3572
misc_ErrorReport("\n In clause_DeleteLiterals:");
3573
misc_ErrorReport(" list contains duplicate indices.");
3574
misc_FinishErrorReport();
3575
}
3576
/* check the literal indices */
3577
for (Scan = Indices; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
3578
i = (int) list_Car(Scan);
3579
if (i < 0 || i > clause_LastLitIndex(Clause)) {
3580
misc_StartErrorReport();
3581
misc_ErrorReport("\n In clause_DeleteLiterals:");
3582
misc_ErrorReport(" literal index %d is out ", i);
3583
misc_ErrorReport(" of bounds");
3584
misc_FinishErrorReport();
3585
}
3586
}
3587
#endif
3588
3589
nc = 0;
3590
na = 0;
3591
ns = 0;
3592
lc = clause_LastConstraintLitIndex(Clause);
3593
la = clause_LastAntecedentLitIndex(Clause);
3594
3595
olength = clause_Length(Clause);
3596
nlength = olength - list_Length(Indices);
3597
3598
if (nlength != 0)
3599
NewLits = (LITERAL*) memory_Malloc(sizeof(LITERAL) * nlength);
3600
else
3601
NewLits = (LITERAL*) NULL;
3602
3603
for (i=clause_FirstLitIndex(), j=clause_FirstLitIndex(); i < olength; i++)
3604
3605
if (list_PointerMember(Indices, (POINTER) i))
3606
clause_LiteralDelete(clause_GetLiteral(Clause,i));
3607
else {
3608
3609
NewLits[j++] = clause_GetLiteral(Clause,i);
3610
3611
if (i <= lc)
3612
nc++;
3613
else if (i <= la)
3614
na++;
3615
else
3616
ns++;
3617
}
3618
clause_FreeLitArray(Clause);
3619
Clause->literals = NewLits;
3620
3621
clause_SetNumOfConsLits(Clause, nc);
3622
clause_SetNumOfAnteLits(Clause, na);
3623
clause_SetNumOfSuccLits(Clause, ns);
3624
3625
clause_ReInit(Clause, Flags, Precedence);
3626
}
3627
3628
3629
/**************************************************************/
3630
/* Clause Comparisons */
3631
/**************************************************************/
3632
3633
BOOL clause_IsHornClause(CLAUSE Clause)
3634
/**************************************************************
3635
INPUT: A clause.
3636
RETURNS: The boolean value TRUE if 'Clause' is a hornclause
3637
FALSE else.
3638
***************************************************************/
3639
{
3640
#ifdef CHECK
3641
if (!clause_IsUnorderedClause(Clause)) {
3642
misc_StartErrorReport();
3643
misc_ErrorReport("\n In clause_IsHornClause:");
3644
misc_ErrorReport("\n Illegal input.");
3645
misc_FinishErrorReport();
3646
}
3647
#endif
3648
return (clause_NumOfSuccLits(Clause) <= 1);
3649
}
3650
3651
3652
BOOL clause_HasTermSortConstraintLits(CLAUSE Clause)
3653
/**************************************************************
3654
INPUT: A clause,
3655
RETURNS: TRUE iff there is at least one sort constraint atom having
3656
a term as its argument
3657
***************************************************************/
3658
{
3659
int i,n;
3660
3661
#ifdef CHECK
3662
if (!clause_IsUnorderedClause(Clause)) {
3663
misc_StartErrorReport();
3664
misc_ErrorReport("\n In clause_HasTermSortConstraintLits:");
3665
misc_ErrorReport("\n Illegal input.");
3666
misc_FinishErrorReport();
3667
}
3668
#endif
3669
3670
n = clause_LastConstraintLitIndex(Clause);
3671
3672
for (i = clause_FirstConstraintLitIndex(Clause); i <= n; i++)
3673
if (!term_AllArgsAreVar(clause_GetLiteralAtom(Clause,i)))
3674
return TRUE;
3675
3676
return FALSE;
3677
}
3678
3679
BOOL clause_HasOnlySpecDomArgs(CLAUSE Clause)
3680
/**************************************************************
3681
INPUT: A clause.
3682
RETURNS: TRUE iff all non sort constraint literals are of the
3683
form x=a, x=y, a=b.
3684
***************************************************************/
3685
{
3686
int i,n;
3687
3688
#ifdef CHECK
3689
if (!clause_IsUnorderedClause(Clause)) {
3690
misc_StartErrorReport();
3691
misc_ErrorReport("\n In clause_HasOnlySpecDomArgs:");
3692
misc_ErrorReport("\n Illegal input.");
3693
misc_FinishErrorReport();
3694
}
3695
#endif
3696
3697
n = clause_Length(Clause);
3698
3699
for (i = clause_FirstAntecedentLitIndex(Clause); i < n; i++)
3700
if (!fol_IsEquality(clause_GetLiteralAtom(Clause,i)) ||
3701
!(term_IsVariable(term_FirstArgument(clause_GetLiteralAtom(Clause,i))) ||
3702
term_IsConstant(term_FirstArgument(clause_GetLiteralAtom(Clause,i)))) ||
3703
!(term_IsVariable(term_SecondArgument(clause_GetLiteralAtom(Clause,i))) ||
3704
term_IsConstant(term_SecondArgument(clause_GetLiteralAtom(Clause,i)))))
3705
return FALSE;
3706
3707
return TRUE;
3708
}
3709
3710
BOOL clause_HasSolvedConstraint(CLAUSE Clause)
3711
/**************************************************************
3712
INPUT: A clause.
3713
RETURNS: The boolean value TRUE if 'Clause' has a solved
3714
constraint, i.e. only variables as sort arguments,
3715
or only equality literals with variable and constant
3716
arguments, e.g., x=a, x=y
3717
FALSE else.
3718
***************************************************************/
3719
{
3720
int i,c;
3721
LIST CVars, LitVars;
3722
3723
#ifdef CHECK
3724
if (!clause_IsUnorderedClause(Clause)) {
3725
misc_StartErrorReport();
3726
misc_ErrorReport("\n In clause_HasSolvedConstraint:");
3727
misc_ErrorReport("\n Illegal input.");
3728
misc_FinishErrorReport();
3729
}
3730
#endif
3731
3732
CVars = list_Nil();
3733
c = clause_NumOfConsLits(Clause);
3734
3735
if (c == 0)
3736
return TRUE;
3737
3738
if (clause_HasTermSortConstraintLits(Clause) || clause_HasOnlySpecDomArgs(Clause))
3739
return FALSE;
3740
3741
for (i = 0; i < c; i++)
3742
CVars = list_NPointerUnion(term_VariableSymbols(clause_GetLiteralAtom(Clause, i)), CVars);
3743
3744
if (i == c) {
3745
c = clause_Length(Clause);
3746
LitVars = list_Nil();
3747
3748
for ( ; i < c; i++)
3749
LitVars = list_NPointerUnion(LitVars, term_VariableSymbols(clause_GetLiteralAtom(Clause, i)));
3750
3751
if (list_Empty(CVars = list_NPointerDifference(CVars, LitVars))) {
3752
list_Delete(LitVars);
3753
return TRUE;
3754
}
3755
list_Delete(LitVars);
3756
}
3757
3758
list_Delete(CVars);
3759
3760
return FALSE;
3761
}
3762
3763
3764
BOOL clause_HasSelectedLiteral(CLAUSE Clause, FLAGSTORE Flags,
3765
PRECEDENCE Precedence)
3766
/**************************************************************
3767
INPUT: A Clause, a flag store and a precedence.
3768
RETURNS: The boolean value TRUE iff <Clause> has a selected literal
3769
***************************************************************/
3770
{
3771
int i,negs;
3772
3773
#ifdef CHECK
3774
if (!clause_IsClause(Clause, Flags, Precedence)) {
3775
misc_StartErrorReport();
3776
misc_ErrorReport("\n In clause_HasSelectedLiteral:");
3777
misc_ErrorReport("\n Illegal input.");
3778
misc_FinishErrorReport();
3779
}
3780
#endif
3781
3782
negs = clause_LastAntecedentLitIndex(Clause);
3783
3784
for (i=clause_FirstAntecedentLitIndex(Clause); i <= negs; i++)
3785
if (clause_LiteralGetFlag(clause_GetLiteral(Clause,i), LITSELECT))
3786
return TRUE;
3787
3788
return FALSE;
3789
}
3790
3791
3792
BOOL clause_IsDeclarationClause(CLAUSE Clause)
3793
/**************************************************************
3794
INPUT: A clause.
3795
RETURNS: The boolean value TRUE, if 'Clause' has only variables
3796
as arguments in constraint literals.
3797
***************************************************************/
3798
{
3799
int i,length;
3800
LITERAL Lit;
3801
3802
#ifdef CHECK
3803
if (!clause_IsUnorderedClause(Clause)) {
3804
misc_StartErrorReport();
3805
misc_ErrorReport("\n In clause_IsDeclarationClause:");
3806
misc_ErrorReport("\n Illegal input.");
3807
misc_FinishErrorReport();
3808
}
3809
#endif
3810
3811
if (!clause_HasSolvedConstraint(Clause))
3812
return FALSE;
3813
3814
length = clause_Length(Clause);
3815
3816
for (i=clause_FirstSuccedentLitIndex(Clause);i<length;i++) {
3817
Lit = clause_GetLiteral(Clause,i);
3818
if (clause_LiteralIsMaximal(Lit) &&
3819
symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(Lit))))
3820
return TRUE;
3821
}
3822
3823
return FALSE;
3824
}
3825
3826
3827
BOOL clause_IsSortTheoryClause(CLAUSE Clause, FLAGSTORE Flags,
3828
PRECEDENCE Precedence)
3829
/**************************************************************
3830
INPUT: A Clause, a flag store and a precedence.
3831
RETURNS: The boolean value TRUE, if 'Clause' has only variables
3832
as arguments in constraint literals, no antecedent literals
3833
and exactly one monadic succedent literal.
3834
***************************************************************/
3835
{
3836
LITERAL Lit;
3837
3838
#ifdef CHECK
3839
if (!clause_IsClause(Clause, Flags, Precedence)) {
3840
misc_StartErrorReport();
3841
misc_ErrorReport("\n In clause_IsSortTheoryClause:");
3842
misc_ErrorReport("\n Illegal input. Input not a clause.");
3843
misc_FinishErrorReport();
3844
}
3845
#endif
3846
3847
if (clause_NumOfAnteLits(Clause) > 0 ||
3848
clause_NumOfSuccLits(Clause) > 1 ||
3849
!clause_HasSolvedConstraint(Clause))
3850
return FALSE;
3851
3852
Lit = clause_GetLiteral(Clause,clause_FirstSuccedentLitIndex(Clause));
3853
if (symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(Lit))))
3854
return TRUE;
3855
3856
return FALSE;
3857
}
3858
3859
BOOL clause_IsPotentialSortTheoryClause(CLAUSE Clause, FLAGSTORE Flags,
3860
PRECEDENCE Precedence)
3861
/**************************************************************
3862
INPUT: A Clause, a flag store and a precedence.
3863
RETURNS: The boolean value TRUE, if 'Clause' has monadic literals
3864
only variables as arguments in antecedent/constraint literals,
3865
no other antecedent literals and exactly one monadic succedent
3866
literal.
3867
***************************************************************/
3868
{
3869
LITERAL Lit;
3870
int i;
3871
3872
#ifdef CHECK
3873
if (!clause_IsClause(Clause, Flags, Precedence)) {
3874
misc_StartErrorReport();
3875
misc_ErrorReport("\n In clause_IsPotentialSortTheoryClause:");
3876
misc_ErrorReport("\n Illegal input. Input not a clause.");
3877
misc_FinishErrorReport();
3878
}
3879
#endif
3880
3881
if (clause_NumOfSuccLits(Clause) != 1)
3882
return FALSE;
3883
3884
for (i=clause_FirstLitIndex();i<clause_FirstSuccedentLitIndex(Clause);i++) {
3885
Lit = clause_GetLiteral(Clause,i);
3886
if (!symbol_IsBaseSort(term_TopSymbol(clause_LiteralAtom(Lit))) ||
3887
!term_IsVariable(term_FirstArgument(clause_LiteralAtom(Lit))))
3888
return FALSE;
3889
}
3890
3891
Lit = clause_GetLiteral(Clause,clause_FirstSuccedentLitIndex(Clause));
3892
if (symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(Lit))))
3893
return TRUE;
3894
3895
return FALSE;
3896
}
3897
3898
3899
BOOL clause_HasOnlyVarsInConstraint(CLAUSE Clause, FLAGSTORE Flags,
3900
PRECEDENCE Precedence)
3901
/**************************************************************
3902
INPUT: A Clause, a flag store and a precedence.
3903
RETURNS: The boolean value TRUE, if 'Clause' has only variables
3904
as arguments in constraint literals.
3905
***************************************************************/
3906
{
3907
int i,nc;
3908
3909
#ifdef CHECK
3910
if (!clause_IsClause(Clause, Flags, Precedence)) {
3911
misc_StartErrorReport();
3912
misc_ErrorReport("\n In clause_HasOnlyVarsInConstraint:");
3913
misc_ErrorReport("\n Illegal input. Input not a clause.");
3914
misc_FinishErrorReport();
3915
}
3916
#endif
3917
3918
nc = clause_NumOfConsLits(Clause);
3919
3920
for (i = 0; i < nc && term_AllArgsAreVar(clause_GetLiteralAtom(Clause,i)); i++)
3921
/* empty */;
3922
3923
return (i == nc);
3924
}
3925
3926
3927
BOOL clause_HasSortInSuccedent(CLAUSE Clause, FLAGSTORE Flags,
3928
PRECEDENCE Precedence)
3929
/**************************************************************
3930
INPUT: A Clause, a flag store and a precedence.
3931
RETURNS: The boolean value TRUE, if 'Clause' has a maximal succedent
3932
sort literal; FALSE, else.
3933
***************************************************************/
3934
{
3935
LITERAL Lit;
3936
int i,l;
3937
BOOL result = FALSE;
3938
3939
#ifdef CHECK
3940
if (!clause_IsClause(Clause, Flags, Precedence)) {
3941
misc_StartErrorReport();
3942
misc_ErrorReport("\n In clause_HasSortInSuccedent:");
3943
misc_ErrorReport("\n Illegal input. Input not a clause.");
3944
misc_FinishErrorReport();
3945
}
3946
#endif
3947
3948
l = clause_Length(Clause);
3949
3950
for (i = clause_FirstSuccedentLitIndex(Clause); i < l && !result ; i++) {
3951
Lit = clause_GetLiteral(Clause, i);
3952
result = (symbol_Arity(term_TopSymbol(clause_LiteralAtom(Lit))) == 1);
3953
}
3954
return result;
3955
}
3956
3957
3958
BOOL clause_LitsHaveCommonVar(LITERAL Lit1, LITERAL Lit2)
3959
/**************************************************************
3960
INPUT: Two literals.
3961
RETURNS: The boolean value TRUE, if 'Lit1' and 'Lit2' have
3962
common variables, FALSE, else.
3963
***************************************************************/
3964
{
3965
LIST Vars1, Vars2;
3966
BOOL Result;
3967
3968
Vars1 = term_VariableSymbols(clause_LiteralAtom(Lit1));
3969
Vars2 = term_VariableSymbols(clause_LiteralAtom(Lit2));
3970
Result = list_HasIntersection(Vars1, Vars2);
3971
list_Delete(Vars1);
3972
list_Delete(Vars2);
3973
3974
return Result;
3975
}
3976
3977
BOOL clause_VarsOfClauseAreInTerm(CLAUSE Clause, TERM Term)
3978
/**********************************************************
3979
* INPUT: A clause and a term
3980
* OUTPUT: TRUE, if vars(<Clause>) is a subset of vars(<Term>)
3981
* else FALSE
3982
* EFFECT: modifies ord_VARCOUNT
3983
**********************************************************/
3984
{
3985
SYMBOL MaxVarClause, MaxVarTerm;
3986
LITERAL Lit;
3987
TERM Atom;
3988
int i, n;
3989
3990
MaxVarClause = clause_MaxVar(Clause);
3991
MaxVarTerm = term_MaxVar(Term);
3992
3993
if(MaxVarClause > MaxVarTerm)
3994
return FALSE;
3995
3996
n = clause_Length(Clause);
3997
3998
for (i = 0; i <= MaxVarTerm; i++) {
3999
ord_VARCOUNT[i][0] = 0;
4000
ord_VARCOUNT[i][1] = 0;
4001
}
4002
4003
for(i = clause_FirstLitIndex(); i < n; i++) {
4004
Lit = clause_GetLiteral(Clause, i);
4005
Atom = clause_LiteralAtom(Lit);
4006
4007
ord_CompareCountVars(Atom, 0);
4008
}
4009
4010
ord_CompareCountVars(Term, 1);
4011
4012
for (i = 0; i <= MaxVarTerm; i++) {
4013
if(ord_VARCOUNT[i][1] == 0 && ord_VARCOUNT[i][0] != 0)
4014
return FALSE;
4015
}
4016
4017
return TRUE;
4018
}
4019
4020
4021
BOOL clause_LiteralIsStrictMaximalLiteralSkolem(CLAUSE Clause, int i,
4022
FLAGSTORE Flags, PRECEDENCE Precedence)
4023
/**********************************************************
4024
* INPUT: A clause and a literal
4025
* OUTPUT: TRUE, if Literal <i> of <Clause> is strictly maximal in <Clause>.
4026
* Consider variables to be (skolem) constants.
4027
* EFFECT: modifies ord_VARCOUNT
4028
* NOTE: We only need to compare STRICTLY MAXIMAL Literals
4029
* of <Clause> with <Lit>
4030
**********************************************************/
4031
{
4032
int ri, last;
4033
4034
last = clause_LastLitIndex(Clause);
4035
for (ri = clause_FirstLitIndex(); ri <= last; ri++) {
4036
if(ri != i &&
4037
clause_LiteralGetFlag(clause_GetLiteral(Clause, ri),STRICTMAXIMAL) &&
4038
ord_LiteralCompareAux(clause_GetLiteralTerm(Clause, i),
4039
clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i)),
4040
clause_GetLiteralTerm(Clause, ri),
4041
clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause, ri)),
4042
TRUE, TRUE, Flags, Precedence) != ord_GREATER_THAN )
4043
return FALSE;
4044
}
4045
return TRUE;
4046
4047
4048
}
4049
/**************************************************************/
4050
/* Clause Input and Output Functions */
4051
/**************************************************************/
4052
4053
void clause_Print(CLAUSE Clause)
4054
/**************************************************************
4055
INPUT: A Clause.
4056
RETURNS: Nothing.
4057
SUMMARY: The clause is printed to stdout.
4058
***************************************************************/
4059
{
4060
RULE Origin;
4061
LITERAL Lit;
4062
int i,c,a,s;
4063
4064
#ifdef CHECK
4065
if (!clause_IsUnorderedClause(Clause)) {
4066
misc_StartErrorReport();
4067
misc_ErrorReport("\n In clause_Print:");
4068
misc_ErrorReport("\n Illegal input. Input not a clause.");
4069
misc_FinishErrorReport();
4070
}
4071
#endif
4072
4073
if (!clause_Exists(Clause))
4074
fputs("(CLAUSE)NULL", stdout);
4075
else {
4076
printf("%d",clause_Number(Clause));
4077
4078
Origin = clause_Origin(Clause);
4079
printf("[%d:", clause_SplitLevel(Clause));
4080
4081
#ifdef CHECK
4082
if (Clause->splitfield_length <= 1)
4083
fputs("0.", stdout);
4084
else
4085
for (i=Clause->splitfield_length-1; i > 0; i--)
4086
printf("%lu.", Clause->splitfield[i]);
4087
if (Clause->splitfield_length == 0)
4088
putchar('1');
4089
else
4090
printf("%lu", (Clause->splitfield[0] | 1));
4091
printf(":%c%c:%c:%d:%d:%.1f:", clause_GetFlag(Clause, CONCLAUSE) ? 'C' : 'A',
4092
clause_GetFlag(Clause, WORKEDOFF) ? 'W' : 'U',
4093
clause_GetFlag(Clause, NOPARAINTO) ? 'N' : 'P',
4094
clause_Weight(Clause), clause_Depth(Clause), clause_SplitPotential(Clause));
4095
#endif
4096
4097
clause_PrintOrigin(Clause);
4098
4099
if (Origin == INPUT) {
4100
;
4101
} else {
4102
putchar(':');
4103
clause_PrintParentClauses(Clause);
4104
}
4105
putchar(']');
4106
4107
c = clause_NumOfConsLits(Clause);
4108
a = clause_NumOfAnteLits(Clause);
4109
s = clause_NumOfSuccLits(Clause);
4110
4111
for (i = 0; i < c; i++) {
4112
putchar(' ');
4113
Lit = clause_GetLiteral(Clause, i);
4114
clause_LiteralPrintUnsigned(Lit);
4115
}
4116
fputs(" || ", stdout);
4117
4118
a += c;
4119
for ( ; i < a; i++) {
4120
4121
Lit = clause_GetLiteral(Clause, i);
4122
clause_LiteralPrintUnsigned(Lit);
4123
if (clause_LiteralIsMaximal(Lit)) {
4124
putchar('*');
4125
if (clause_LiteralIsOrientedEquality(Lit))
4126
putchar('*');
4127
}
4128
if (clause_LiteralGetFlag(Lit,LITSELECT))
4129
putchar('+');
4130
if (i+1 < a)
4131
putchar(' ');
4132
}
4133
fputs(" -> ",stdout);
4134
4135
s += a;
4136
for ( ; i < s; i++) {
4137
4138
Lit = clause_GetLiteral(Clause, i);
4139
clause_LiteralPrintUnsigned(Lit);
4140
if (clause_LiteralIsMaximal(Lit)) {
4141
putchar('*');
4142
if (clause_LiteralIsOrientedEquality(Lit))
4143
putchar('*');
4144
}
4145
#ifdef CHECK
4146
if (clause_LiteralGetFlag(Lit,LITSELECT)) {
4147
misc_StartErrorReport();
4148
misc_ErrorReport("\n In clause_Print: Clause has selected positive literal.\n");
4149
misc_FinishErrorReport();
4150
}
4151
#endif
4152
if (i+1 < s)
4153
putchar(' ');
4154
}
4155
putchar('.');
4156
}
4157
}
4158
4159
void clause_PrintSpecial(CLAUSE Clause)
4160
/**************************************************************
4161
INPUT: A Clause, where parents are the pointers to clauses
4162
as used in the tableau module
4163
RETURNS: Nothing.
4164
SUMMARY: The clause is printed to stdout. For DEBUGGING!
4165
***************************************************************/
4166
{
4167
RULE Origin;
4168
LITERAL Lit;
4169
int i,j,c,a,s;
4170
4171
#ifdef CHECK
4172
if (!clause_IsUnorderedClause(Clause)) {
4173
misc_StartErrorReport();
4174
misc_ErrorReport("\n In clause_PrintSpecial:");
4175
misc_ErrorReport("\n Illegal input. Input not a clause.");
4176
misc_FinishErrorReport();
4177
}
4178
#endif
4179
4180
if (!clause_Exists(Clause))
4181
fputs("(CLAUSE)NULL", stdout);
4182
else {
4183
printf("%d",clause_Number(Clause));
4184
4185
Origin = clause_Origin(Clause);
4186
printf("[%d:", clause_SplitLevel(Clause));
4187
4188
fputs("0", stdout);
4189
for (i = Clause->splitfield_length-1; i >= 0; i--)
4190
if (Clause->splitfield[i] != 0) {
4191
for (j = 0; j<=sizeof(SPLITFIELDENTRY)*CHAR_BIT-1; j++)
4192
if (Clause->splitfield[i] & ((SPLITFIELDENTRY)1 << j))
4193
printf(",%u", i*sizeof(SPLITFIELDENTRY)*CHAR_BIT+j);
4194
}
4195
4196
4197
printf(":%c%c:%c:%d:%d:%.1f:", clause_GetFlag(Clause, CONCLAUSE) ? 'C' : 'A',
4198
clause_GetFlag(Clause, WORKEDOFF) ? 'W' : 'U',
4199
clause_GetFlag(Clause, NOPARAINTO) ? 'N' : 'P',
4200
clause_Weight(Clause), clause_Depth(Clause), clause_SplitPotential(Clause));
4201
4202
clause_PrintOrigin(Clause);
4203
4204
if (Origin == INPUT) {
4205
;
4206
} else {
4207
putchar(':');
4208
clause_PrintParentClausesSpecial(Clause);
4209
}
4210
putchar(']');
4211
4212
c = clause_NumOfConsLits(Clause);
4213
a = clause_NumOfAnteLits(Clause);
4214
s = clause_NumOfSuccLits(Clause);
4215
4216
for (i = 0; i < c; i++) {
4217
putchar(' ');
4218
Lit = clause_GetLiteral(Clause, i);
4219
clause_LiteralPrintUnsigned(Lit);
4220
}
4221
fputs(" || ", stdout);
4222
4223
a += c;
4224
for ( ; i < a; i++) {
4225
4226
Lit = clause_GetLiteral(Clause, i);
4227
clause_LiteralPrintUnsigned(Lit);
4228
if (clause_LiteralIsMaximal(Lit)) {
4229
putchar('*');
4230
if (clause_LiteralIsOrientedEquality(Lit))
4231
putchar('*');
4232
}
4233
if (clause_LiteralGetFlag(Lit,LITSELECT))
4234
putchar('+');
4235
if (i+1 < a)
4236
putchar(' ');
4237
}
4238
fputs(" -> ",stdout);
4239
4240
s += a;
4241
for ( ; i < s; i++) {
4242
4243
Lit = clause_GetLiteral(Clause, i);
4244
clause_LiteralPrintUnsigned(Lit);
4245
if (clause_LiteralIsMaximal(Lit)) {
4246
putchar('*');
4247
if (clause_LiteralIsOrientedEquality(Lit))
4248
putchar('*');
4249
}
4250
#ifdef CHECK
4251
if (clause_LiteralGetFlag(Lit,LITSELECT)) {
4252
misc_StartErrorReport();
4253
misc_ErrorReport("\n In clause_Print: Clause has selected positive literal.\n");
4254
misc_FinishErrorReport();
4255
}
4256
#endif
4257
if (i+1 < s)
4258
putchar(' ');
4259
}
4260
putchar('.');
4261
}
4262
}
4263
4264
void clause_PrintSplitfield(CLAUSE Clause, NAT MaxLevel)
4265
{
4266
int i,j;
4267
unsigned field;
4268
short first = 1;
4269
4270
for(i=1; i<=MaxLevel; i++) {
4271
j = clause_ComputeSplitFieldAddress(i, &field);
4272
if((Clause->splitfield[field] & ((SPLITFIELDENTRY)1 << j)) != 0) {
4273
if(first==1) {
4274
printf("%d", i);
4275
first=0;
4276
} else {
4277
printf(".%d", i);
4278
}
4279
}
4280
}
4281
}
4282
4283
void clause_PrintSplitfieldOnly(SPLITFIELD SF, int SF_length)
4284
{
4285
int i,j;
4286
NAT k;
4287
short first = 1;
4288
4289
for(i=0; i<SF_length; i++) {
4290
for(j=0; j<sizeof(SPLITFIELDENTRY) * CHAR_BIT; j++) {
4291
if((SF[i] & ((SPLITFIELDENTRY)1 << j)) != 0) {
4292
k = (i * sizeof(SPLITFIELDENTRY) * CHAR_BIT)+j;
4293
if(first==1) {
4294
printf("%u", k);
4295
first=0;
4296
} else {
4297
printf(".%u", k);
4298
}
4299
}
4300
}
4301
}
4302
}
4303
4304
void clause_PrintMaxLitsOnly(CLAUSE Clause, FLAGSTORE Flags,
4305
PRECEDENCE Precedence)
4306
/**************************************************************
4307
INPUT: A Clause, a flag store and a precedence.
4308
RETURNS: Nothing.
4309
SUMMARY:
4310
***************************************************************/
4311
{
4312
int i,c,a,s;
4313
4314
#ifdef CHECK
4315
if (!clause_IsClause(Clause, Flags, Precedence)) {
4316
misc_StartErrorReport();
4317
misc_ErrorReport("\n In clause_PrinMaxLitsOnly:");
4318
misc_ErrorReport("\n Illegal input. Input not a clause.");
4319
misc_FinishErrorReport();
4320
}
4321
#endif
4322
4323
c = clause_NumOfConsLits(Clause);
4324
a = clause_NumOfAnteLits(Clause);
4325
s = clause_NumOfSuccLits(Clause);
4326
4327
for (i = 0; i < c; i++) {
4328
if (clause_LiteralIsMaximal(clause_GetLiteral(Clause, i)))
4329
clause_LiteralPrint(clause_GetLiteral(Clause, i));
4330
if (clause_LiteralGetFlag(clause_GetLiteral(Clause, i),STRICTMAXIMAL)) {
4331
clause_LiteralPrint(clause_GetLiteral(Clause, i));
4332
fputs("(strictly)", stdout);
4333
}
4334
}
4335
fputs(" || ", stdout);
4336
4337
a += c;
4338
for ( ; i < a; i++) {
4339
if (clause_LiteralIsMaximal(clause_GetLiteral(Clause, i)))
4340
clause_LiteralPrint(clause_GetLiteral(Clause, i));
4341
if (clause_LiteralGetFlag(clause_GetLiteral(Clause, i),STRICTMAXIMAL)) {
4342
clause_LiteralPrint(clause_GetLiteral(Clause, i));
4343
fputs("(strictly)", stdout);
4344
}
4345
}
4346
fputs(" -> ", stdout);
4347
4348
s += a;
4349
for ( ; i < s; i++) {
4350
if (clause_LiteralIsMaximal(clause_GetLiteral(Clause, i)))
4351
clause_LiteralPrint(clause_GetLiteral(Clause, i));
4352
if (clause_LiteralGetFlag(clause_GetLiteral(Clause, i),STRICTMAXIMAL)) {
4353
clause_LiteralPrint(clause_GetLiteral(Clause, i));
4354
fputs("(strictly)", stdout);
4355
}
4356
}
4357
puts("."); /* with newline */
4358
}
4359
4360
4361
void clause_FPrint(FILE* File, CLAUSE Clause)
4362
/**************************************************************
4363
INPUT: A file and a clause.
4364
RETURNS: Nothing.
4365
SUMMARY: Prints any clause to the file 'File'.
4366
CAUTION: Uses the term_Output functions.
4367
***************************************************************/
4368
{
4369
int i, c, a, s;
4370
4371
c = clause_NumOfConsLits(Clause);
4372
a = clause_NumOfAnteLits(Clause);
4373
s = clause_NumOfSuccLits(Clause);
4374
4375
for (i = 0; i < c; i++)
4376
term_FPrint(File, clause_GetLiteralAtom(Clause, i));
4377
4378
fputs(" || ", stdout);
4379
4380
a += c;
4381
for ( ; i < a; i++)
4382
term_FPrint(File, clause_GetLiteralAtom(Clause, i));
4383
4384
fputs(" -> ", stdout);
4385
4386
s += a;
4387
for ( ; i < s; i++)
4388
term_FPrint(File, clause_GetLiteralAtom(Clause, i));
4389
4390
putc('.', File);
4391
}
4392
4393
4394
void clause_ListPrint(LIST ClauseList)
4395
/**************************************************************
4396
INPUT: A list of clauses.
4397
RETURNS: Nothing.
4398
SUMMARY: Prints the clauses to stdout.
4399
CAUTION: Uses the clause_Print function.
4400
***************************************************************/
4401
{
4402
while (!(list_Empty(ClauseList))) {
4403
clause_Print(list_First(ClauseList));
4404
ClauseList = list_Cdr(ClauseList);
4405
if (!list_Empty(ClauseList))
4406
putchar('\n');
4407
}
4408
}
4409
4410
4411
void clause_PrintParentClauses(CLAUSE Clause)
4412
/**************************************************************
4413
INPUT: A Clause.
4414
RETURNS: Nothing.
4415
SUMMARY: Prints the clauses parentclauses and -literals to stdout.
4416
***************************************************************/
4417
{
4418
LIST Scan1,Scan2;
4419
4420
if (!list_Empty(clause_ParentClauses(Clause))) {
4421
4422
Scan1 = clause_ParentClauses(Clause);
4423
Scan2 = clause_ParentLiterals(Clause);
4424
printf("%d.%d", (int)list_Car(Scan1), (int)list_Car(Scan2));
4425
4426
for (Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2);
4427
!list_Empty(Scan1);
4428
Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2))
4429
printf(",%d.%d", (int)list_Car(Scan1), (int)list_Car(Scan2));
4430
}
4431
}
4432
4433
void clause_PrintParentClausesSpecial(CLAUSE Clause)
4434
/**************************************************************
4435
INPUT: A Clause where parents are clause pointers.
4436
RETURNS: Nothing.
4437
SUMMARY: Prints the clauses parentclauses and -literals to stdout.
4438
***************************************************************/
4439
{
4440
LIST Scan1,Scan2;
4441
4442
if (!list_Empty(clause_ParentClauses(Clause))) {
4443
4444
Scan1 = clause_ParentClauses(Clause);
4445
Scan2 = clause_ParentLiterals(Clause);
4446
printf("%d.%d", clause_Number((CLAUSE)list_Car(Scan1)), (int)list_Car(Scan2));
4447
4448
for (Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2);
4449
!list_Empty(Scan1);
4450
Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2))
4451
printf(",%d.%d", clause_Number((CLAUSE)list_Car(Scan1)), (int)list_Car(Scan2));
4452
}
4453
}
4454
4455
4456
RULE clause_GetOriginFromString(const char* RuleName)
4457
/**************************************************************
4458
INPUT: A string containing the abbreviated name of a rule.
4459
RETURNS: The RULE corresponding to the <RuleName>.
4460
***************************************************************/
4461
{
4462
if (string_Equal(RuleName, "App")) return CLAUSE_DELETION;
4463
else if (string_Equal(RuleName, "EmS")) return EMPTY_SORT;
4464
else if (string_Equal(RuleName, "SoR")) return SORT_RESOLUTION;
4465
else if (string_Equal(RuleName, "EqR")) return EQUALITY_RESOLUTION;
4466
else if (string_Equal(RuleName, "EqF")) return EQUALITY_FACTORING;
4467
else if (string_Equal(RuleName, "MPm")) return MERGING_PARAMODULATION;
4468
else if (string_Equal(RuleName, "SpR")) return SUPERPOSITION_RIGHT;
4469
else if (string_Equal(RuleName, "SPm")) return PARAMODULATION;
4470
else if (string_Equal(RuleName, "OPm")) return ORDERED_PARAMODULATION;
4471
else if (string_Equal(RuleName, "SpL")) return SUPERPOSITION_LEFT;
4472
else if (string_Equal(RuleName, "Res")) return GENERAL_RESOLUTION;
4473
else if (string_Equal(RuleName, "SHy")) return SIMPLE_HYPER;
4474
else if (string_Equal(RuleName, "OHy")) return ORDERED_HYPER;
4475
else if (string_Equal(RuleName, "URR")) return UR_RESOLUTION;
4476
else if (string_Equal(RuleName, "Fac")) return GENERAL_FACTORING;
4477
else if (string_Equal(RuleName, "Spt")) return SPLITTING;
4478
else if (string_Equal(RuleName, "Inp")) return INPUT;
4479
else if (string_Equal(RuleName, "Rew")) return REWRITING;
4480
else if (string_Equal(RuleName, "CRw")) return CONTEXTUAL_REWRITING;
4481
else if (string_Equal(RuleName, "Con")) return CONDENSING;
4482
else if (string_Equal(RuleName, "AED")) return ASSIGNMENT_EQUATION_DELETION;
4483
else if (string_Equal(RuleName, "Obv")) return OBVIOUS_REDUCTIONS;
4484
else if (string_Equal(RuleName, "SSi")) return SORT_SIMPLIFICATION;
4485
else if (string_Equal(RuleName, "MRR")) return MATCHING_REPLACEMENT_RESOLUTION;
4486
else if (string_Equal(RuleName, "UnC")) return UNIT_CONFLICT;
4487
else if (string_Equal(RuleName, "Def")) return DEFAPPLICATION;
4488
else if (string_Equal(RuleName, "Ter")) return TERMINATOR;
4489
else {
4490
misc_StartErrorReport();
4491
misc_ErrorReport("\nIn clause_GetOriginFromString: Unknown clause origin '%s'.", RuleName);
4492
misc_FinishErrorReport();
4493
return CLAUSE_DELETION; /* Just for the compiler, code is not reachable */
4494
}
4495
}
4496
4497
void clause_FPrintOrigin(FILE* File, CLAUSE Clause)
4498
/**************************************************************
4499
INPUT: A Clause.
4500
RETURNS: Nothing.
4501
SUMMARY: Prints the clause's origin to the file.
4502
***************************************************************/
4503
{
4504
RULE Result;
4505
4506
Result = clause_Origin(Clause);
4507
4508
switch(Result) {
4509
case CLAUSE_DELETION: fputs("App", File); break;
4510
case EMPTY_SORT: fputs("EmS", File); break;
4511
case SORT_RESOLUTION: fputs("SoR", File); break;
4512
case EQUALITY_RESOLUTION: fputs("EqR", File); break;
4513
case EQUALITY_FACTORING: fputs("EqF", File); break;
4514
case MERGING_PARAMODULATION: fputs("MPm", File); break;
4515
case SUPERPOSITION_RIGHT: fputs("SpR", File); break;
4516
case PARAMODULATION: fputs("SPm", File); break;
4517
case ORDERED_PARAMODULATION: fputs("OPm", File); break;
4518
case SUPERPOSITION_LEFT: fputs("SpL", File); break;
4519
case GENERAL_RESOLUTION: fputs("Res", File); break;
4520
case SIMPLE_HYPER: fputs("SHy", File); break;
4521
case ORDERED_HYPER: fputs("OHy", File); break;
4522
case UR_RESOLUTION: fputs("URR", File); break;
4523
case GENERAL_FACTORING: fputs("Fac", File); break;
4524
case SPLITTING: fputs("Spt", File); break;
4525
case INPUT: fputs("Inp", File); break;
4526
case REWRITING: fputs("Rew", File); break;
4527
case CONTEXTUAL_REWRITING: fputs("CRw", File); break;
4528
case CONDENSING: fputs("Con", File); break;
4529
case ASSIGNMENT_EQUATION_DELETION: fputs("AED", File); break;
4530
case OBVIOUS_REDUCTIONS: fputs("Obv", File); break;
4531
case SORT_SIMPLIFICATION: fputs("SSi", File); break;
4532
case MATCHING_REPLACEMENT_RESOLUTION: fputs("MRR", File); break;
4533
case UNIT_CONFLICT: fputs("UnC", File); break;
4534
case DEFAPPLICATION: fputs("Def", File); break;
4535
case TERMINATOR: fputs("Ter", File); break;
4536
case TEMPORARY: fputs("Temporary", File); break;
4537
default:
4538
misc_StartErrorReport();
4539
misc_ErrorReport("\n In clause_FPrintOrigin: Clause has no origin.");
4540
misc_FinishErrorReport();
4541
}
4542
}
4543
4544
4545
void clause_PrintOrigin(CLAUSE Clause)
4546
/**************************************************************
4547
INPUT: A Clause.
4548
RETURNS: Nothing.
4549
SUMMARY: Prints the clauses origin to stdout.
4550
***************************************************************/
4551
{
4552
clause_FPrintOrigin(stdout, Clause);
4553
}
4554
4555
4556
void clause_PrintVerbose(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence)
4557
/**************************************************************
4558
INPUT: A Clause, a flag store and a precedence.
4559
RETURNS: Nothing.
4560
SUMMARY: Prints almost all the information kept in the
4561
clause structure.
4562
***************************************************************/
4563
{
4564
int c,a,s;
4565
4566
#ifdef CHECK
4567
if (!clause_IsClause(Clause, Flags, Precedence)) {
4568
misc_StartErrorReport();
4569
misc_ErrorReport("\n In clause_PrintVerbose:");
4570
misc_ErrorReport("\n Illegal input. Input not a clause.");
4571
misc_FinishErrorReport();
4572
}
4573
#endif
4574
4575
c = clause_NumOfConsLits(Clause);
4576
a = clause_NumOfAnteLits(Clause);
4577
s = clause_NumOfSuccLits(Clause);
4578
4579
printf(" c = %d a = %d s = %d", c,a,s);
4580
printf(" Weight : %d", clause_Weight(Clause));
4581
printf(" Depth : %d", clause_Depth(Clause));
4582
printf(" %s %s ",
4583
(clause_GetFlag(Clause,WORKEDOFF) ? "WorkedOff" : "Usable"),
4584
(clause_GetFlag(Clause,CLAUSESELECT) ? "Selected" : "NotSelected"));
4585
4586
clause_Print(Clause);
4587
}
4588
4589
4590
CLAUSE clause_GetNumberedCl(int number, LIST ClList)
4591
/**************************************************************
4592
INPUT:
4593
RETURNS:
4594
CAUTION:
4595
***************************************************************/
4596
{
4597
while (!list_Empty(ClList) &&
4598
clause_Number((CLAUSE)list_Car(ClList)) != number)
4599
ClList = list_Cdr(ClList);
4600
4601
if (list_Empty(ClList))
4602
return NULL;
4603
else
4604
return list_Car(ClList);
4605
}
4606
4607
static __inline__ BOOL clause_NumberLower(CLAUSE A, CLAUSE B)
4608
{
4609
return (BOOL) (clause_Number(A) < clause_Number(B));
4610
}
4611
4612
LIST clause_NumberSort(LIST List)
4613
/**************************************************************
4614
INPUT: A list of clauses.
4615
RETURNS: The same list where the elements are sorted wrt their number.
4616
CAUTION: Destructive.
4617
***************************************************************/
4618
{
4619
return list_Sort(List, (BOOL (*) (POINTER, POINTER)) clause_NumberLower);
4620
}
4621
4622
4623
LIST clause_NumberDelete(LIST List, int Number)
4624
/**************************************************************
4625
INPUT: A list of clauses and an integer.
4626
RETURNS: The same list where the clauses with <Number> are deleted.
4627
CAUTION: Destructive.
4628
***************************************************************/
4629
{
4630
LIST Scan1,Scan2;
4631
4632
for (Scan1 = List; !list_Empty(Scan1); )
4633
if (clause_Number(list_Car(Scan1))==Number) {
4634
4635
Scan2 = Scan1;
4636
Scan1 = list_Cdr(Scan1);
4637
List = list_PointerDeleteOneElement(List, list_Car(Scan2));
4638
} else
4639
Scan1 = list_Cdr(Scan1);
4640
4641
return List;
4642
}
4643
4644
4645
static NAT clause_NumberOfMaxLits(CLAUSE Clause)
4646
/**************************************************************
4647
INPUT: A clause.
4648
RETURNS: The number of maximal literals in a clause.
4649
***************************************************************/
4650
{
4651
NAT Result,i,n;
4652
4653
Result = 0;
4654
n = clause_Length(Clause);
4655
4656
for (i = clause_FirstAntecedentLitIndex(Clause); i < n; i++)
4657
if (clause_LiteralIsMaximal(clause_GetLiteral(Clause,i)))
4658
Result++;
4659
4660
return Result;
4661
}
4662
4663
/* Unused ! */
4664
NAT clause_NumberOfMaxAntecedentLits(CLAUSE Clause)
4665
/**************************************************************
4666
INPUT: A clause.
4667
RETURNS: The number of maximal antecedent literals in a clause.
4668
***************************************************************/
4669
{
4670
NAT Result,i,n;
4671
4672
Result = 0;
4673
n = clause_LastAntecedentLitIndex(Clause);
4674
4675
for (i = clause_FirstAntecedentLitIndex(Clause); i <= n; i++)
4676
if (clause_LiteralIsMaximal(clause_GetLiteral(Clause,i)))
4677
Result++;
4678
4679
return Result;
4680
}
4681
4682
4683
void clause_SelectLiteral(CLAUSE Clause, FLAGSTORE Flags)
4684
/**************************************************************
4685
INPUT: A clause and a flag store.
4686
RETURNS: Nothing.
4687
EFFECT: If the clause contains more than 2 maximal literals,
4688
at least one antecedent literal, the literal with
4689
the highest weight is selected or if selected predicates
4690
are set, the first (from left to right) literal with
4691
selected predicate
4692
Or the user has determined literals to be selected that
4693
will then be chosen if they occur in the antecedent.
4694
***************************************************************/
4695
{
4696
if (clause_HasSolvedConstraint(Clause) &&
4697
!clause_GetFlag(Clause,CLAUSESELECT) &&
4698
clause_NumOfAnteLits(Clause) > 0 &&
4699
flag_GetFlagIntValue(Flags, flag_SELECT) != flag_SELECTOFF &&
4700
(flag_GetFlagIntValue(Flags, flag_SELECT) != flag_SELECTIFSEVERALMAXIMAL || clause_NumberOfMaxLits(Clause) > 1)) {
4701
NAT i,n;
4702
LITERAL Lit;
4703
4704
Lit = (LITERAL)NULL;
4705
n = clause_LastAntecedentLitIndex(Clause);
4706
i = clause_FirstAntecedentLitIndex(Clause);
4707
4708
if (flag_GetFlagIntValue(Flags, flag_SELECT) == flag_SELECTFROMLIST) {
4709
for ( ; i <= n; i++)
4710
if (symbol_HasProperty(term_TopSymbol(clause_LiteralAtom(clause_GetLiteral(Clause,i))), SELECTED)) {
4711
Lit = clause_GetLiteral(Clause,i);
4712
i = n + 1;
4713
}
4714
}
4715
else {
4716
4717
Lit = clause_GetLiteral(Clause,i);
4718
i++;
4719
4720
if (symbol_HasProperty(term_TopSymbol(clause_LiteralAtom(Lit)), SELECTED))
4721
i = n + 1;
4722
4723
for ( ; i <= n; i++)
4724
if (symbol_HasProperty(term_TopSymbol(clause_LiteralAtom(clause_GetLiteral(Clause,i))), SELECTED)) {
4725
Lit = clause_GetLiteral(Clause,i);
4726
i = n + 1;
4727
}
4728
else
4729
if (clause_LiteralWeight(Lit)
4730
< clause_LiteralWeight(clause_GetLiteral(Clause,i)))
4731
Lit = clause_GetLiteral(Clause,i);
4732
}
4733
4734
if (Lit != (LITERAL)NULL) {
4735
clause_LiteralSetFlag(Lit,LITSELECT);
4736
clause_SetFlag(Clause,CLAUSESELECT);
4737
}
4738
}
4739
}
4740
4741
4742
void clause_SetSpecialFlags(CLAUSE Clause, BOOL SortDecreasing, FLAGSTORE Flags,
4743
PRECEDENCE Precedence)
4744
/**************************************************************
4745
INPUT: A clause, a flag indicating whether all equations are
4746
sort decreasing, a flag store and a precedence.
4747
RETURNS: void.
4748
EFFECT: If the clause is a sort theory clause and its declaration
4749
top symbol is a set declaration sort, i.e., it occurred in a
4750
declaration right from the beginning, the paramodulation/superposition
4751
steps into the clause are forbidden by setting the
4752
NOPARAINTO clause flag
4753
***************************************************************/
4754
{
4755
if (SortDecreasing &&
4756
clause_IsSortTheoryClause(Clause, Flags, Precedence) &&
4757
symbol_HasProperty(term_TopSymbol(clause_GetLiteralTerm(Clause,clause_FirstSuccedentLitIndex(Clause))),
4758
DECLSORT))
4759
clause_SetFlag(Clause,NOPARAINTO);
4760
}
4761
4762
4763
BOOL clause_ContainsPotPredDef(CLAUSE Clause, FLAGSTORE Flags,
4764
PRECEDENCE Precedence, NAT* Index, LIST* Pair)
4765
/**************************************************************
4766
INPUT: A clause, a flag store, a precedence and a pointer to an index.
4767
RETURNS: TRUE iff a succedent literal of the clause is a predicate
4768
having only variables as arguments, the predicate occurs only
4769
once in the clause and no other variables but the predicates'
4770
occur.
4771
In that case Index is set to the index of the predicate and
4772
Pair contains two lists : the literals for which positive
4773
occurrences must be found and a list of literals for which negative
4774
occurrences must be found for a complete definition.
4775
***************************************************************/
4776
{
4777
NAT i;
4778
4779
#ifdef CHECK
4780
if (!clause_IsClause(Clause, Flags, Precedence)) {
4781
misc_StartErrorReport();
4782
misc_ErrorReport("\n In clause_ContainsPotPredDef:");
4783
misc_ErrorReport("\n Illegal input. Input not a clause.");
4784
misc_FinishErrorReport();
4785
}
4786
#endif
4787
4788
/* Iterate over all succedent literals */
4789
for (i=clause_FirstSuccedentLitIndex(Clause); i < clause_Length(Clause); i++) {
4790
LITERAL lit;
4791
TERM atom;
4792
LIST pair;
4793
4794
lit = clause_GetLiteral(Clause, i);
4795
atom = clause_LiteralSignedAtom(lit);
4796
if (symbol_IsPredicate(term_TopSymbol(atom))) {
4797
LIST l;
4798
BOOL ok;
4799
ok = TRUE;
4800
pair = list_PairCreate(list_Nil(), list_Nil());
4801
4802
/* Make sure all arguments of predicate are variables */
4803
for (l=term_ArgumentList(atom); !list_Empty(l); l=list_Cdr(l)) {
4804
if (!term_IsStandardVariable((TERM) list_Car(l))) {
4805
ok = FALSE;
4806
break;
4807
}
4808
}
4809
if (ok) {
4810
/* Make sure predicate occurs only once in clause */
4811
NAT j, count;
4812
count = 0;
4813
for (j=0; (j < clause_Length(Clause)) && (count < 2); j++) {
4814
TERM t;
4815
t = clause_GetLiteralAtom(Clause, j);
4816
if (symbol_Equal(term_TopSymbol(t), term_TopSymbol(atom)))
4817
count++;
4818
}
4819
if (count > 1)
4820
ok = FALSE;
4821
}
4822
if (ok) {
4823
/* Build lists of positive and negative literals */
4824
/* At the same time check if other variables than those among
4825
the predicates arguments are found */
4826
NAT j;
4827
LIST predvars, vars;
4828
predvars = fol_FreeVariables(atom);
4829
4830
/* Build list of literals for which positive occurrences are required */
4831
for (j=0; (j < clause_FirstSuccedentLitIndex(Clause)) && ok; j++) {
4832
list_Rplaca(pair, list_Cons(clause_GetLiteralAtom(Clause, j), list_PairFirst(pair)));
4833
vars = fol_FreeVariables(clause_GetLiteralTerm(Clause, j));
4834
for (l = vars; !list_Empty(l); l = list_Cdr(l)) {
4835
if (!term_ListContainsTerm(predvars, list_Car(l))) {
4836
ok = FALSE;
4837
break;
4838
}
4839
}
4840
list_Delete(vars);
4841
}
4842
4843
/* Build list of literals for which negative occurrences are required */
4844
for (j = clause_FirstSuccedentLitIndex(Clause);
4845
(j < clause_Length(Clause)) && ok; j++) {
4846
if (j != i) {
4847
list_Rplacd(pair, list_Cons(clause_GetLiteralAtom(Clause, j), list_PairSecond(pair)));
4848
vars = fol_FreeVariables(clause_GetLiteralAtom(Clause, j));
4849
for (l=vars; !list_Empty(l); l=list_Cdr(l)) {
4850
if (!term_ListContainsTerm(predvars, list_Car(l))) {
4851
ok = FALSE;
4852
break;
4853
}
4854
}
4855
list_Delete(vars);
4856
}
4857
}
4858
list_Delete(predvars);
4859
}
4860
4861
if (ok) {
4862
*Index = i;
4863
*Pair = pair;
4864
return TRUE;
4865
}
4866
else {
4867
list_Delete(list_PairFirst(pair));
4868
list_Delete(list_PairSecond(pair));
4869
list_PairFree(pair);
4870
}
4871
}
4872
}
4873
return FALSE;
4874
}
4875
4876
BOOL clause_IsPartOfDefinition(CLAUSE Clause, TERM Predicate, int *Index,
4877
LIST Pair)
4878
/**************************************************************
4879
INPUT: A clause, a term, a pointer to an int and a pair of term lists.
4880
RETURNS: TRUE iff the predicate occurs among the negative literals of
4881
the clause and the other negative and positive literals are found
4882
in the pairs' lists.
4883
In that case they are removed from the lists.
4884
Index is set to the index of the defined predicate in Clause.
4885
***************************************************************/
4886
{
4887
NAT predindex, i;
4888
BOOL ok;
4889
4890
ok = TRUE;
4891
4892
/* Check whether Predicate is among antecedent or constraint literals */
4893
for (predindex=clause_FirstLitIndex();
4894
predindex < clause_FirstSuccedentLitIndex(Clause);
4895
predindex++)
4896
if (term_Equal(Predicate, clause_GetLiteralAtom(Clause, predindex)))
4897
break;
4898
if (predindex == clause_FirstSuccedentLitIndex(Clause))
4899
return FALSE;
4900
*Index = predindex;
4901
4902
/* Check if other negative literals are required for definition */
4903
for (i=clause_FirstLitIndex();
4904
(i < clause_FirstSuccedentLitIndex(Clause)) && ok; i++) {
4905
if (i != predindex)
4906
if (!term_ListContainsTerm((LIST) list_PairSecond(Pair),
4907
clause_GetLiteralAtom(Clause, i)))
4908
ok = FALSE;
4909
}
4910
4911
/* Check if positive literals are required for definition */
4912
for (i=clause_FirstSuccedentLitIndex(Clause);
4913
(i < clause_Length(Clause)) && ok; i++)
4914
if (!term_ListContainsTerm((LIST) list_PairFirst(Pair),
4915
clause_GetLiteralAtom(Clause, i)))
4916
ok = FALSE;
4917
4918
if (!ok)
4919
return FALSE;
4920
else {
4921
/* Complement for definition found, remove literals from pair lists */
4922
for (i=0; i < clause_FirstSuccedentLitIndex(Clause); i++)
4923
if (i != predindex)
4924
list_Rplacd(Pair,
4925
list_DeleteElement((LIST) list_PairSecond(Pair),
4926
clause_GetLiteralAtom(Clause, i),
4927
(BOOL (*)(POINTER, POINTER)) term_Equal));
4928
for (i=clause_FirstSuccedentLitIndex(Clause); i < clause_Length(Clause); i++)
4929
list_Rplaca(Pair,
4930
list_DeleteElement((LIST) list_PairFirst(Pair),
4931
clause_GetLiteralAtom(Clause, i),
4932
(BOOL (*)(POINTER, POINTER)) term_Equal));
4933
return TRUE;
4934
}
4935
}
4936
4937
void clause_FPrintRule(FILE* File, CLAUSE Clause)
4938
/**************************************************************
4939
INPUT: A file and a clause.
4940
RETURNS: Nothing.
4941
SUMMARY: Prints any term of the clause to file in rule format.
4942
CAUTION: Uses the term_Output functions.
4943
***************************************************************/
4944
{
4945
int i,n;
4946
TERM Literal;
4947
LIST scan,antecedent,succedent,constraints;
4948
4949
n = clause_Length(Clause);
4950
4951
constraints = list_Nil();
4952
antecedent = list_Nil();
4953
succedent = list_Nil();
4954
4955
for (i = 0; i < n; i++) {
4956
Literal = clause_GetLiteralTerm(Clause,i);
4957
if (symbol_Equal(term_TopSymbol(Literal),fol_Not())) {
4958
if (symbol_Arity(term_TopSymbol(fol_Atom(Literal))) == 1 &&
4959
symbol_IsVariable(term_TopSymbol(term_FirstArgument(fol_Atom(Literal)))))
4960
constraints = list_Cons(Literal,constraints);
4961
else
4962
antecedent = list_Cons(Literal,antecedent);
4963
}
4964
else
4965
succedent = list_Cons(Literal,succedent);
4966
}
4967
4968
for (scan = constraints; !list_Empty(scan); scan = list_Cdr(scan)) {
4969
term_FPrint(File, fol_Atom(list_Car(scan)));
4970
putc(' ', File);
4971
}
4972
fputs("||", File);
4973
for (scan = antecedent; !list_Empty(scan); scan = list_Cdr(scan)) {
4974
putc(' ', File);
4975
term_FPrint(File,fol_Atom(list_Car(scan)));
4976
if (list_Empty(list_Cdr(scan)))
4977
putc(' ', File);
4978
}
4979
fputs("->", File);
4980
for (scan = succedent; !list_Empty(scan); scan = list_Cdr(scan)) {
4981
putc(' ', File);
4982
term_FPrint(File,list_Car(scan));
4983
}
4984
fputs(".\n", File);
4985
4986
list_Delete(antecedent);
4987
list_Delete(succedent);
4988
list_Delete(constraints);
4989
}
4990
4991
4992
void clause_FPrintOtter(FILE* File, CLAUSE clause)
4993
/**************************************************************
4994
INPUT: A file and a clause.
4995
RETURNS: Nothing.
4996
SUMMARY: Prints any clause to File.
4997
CAUTION: Uses the other clause_Output functions.
4998
***************************************************************/
4999
{
5000
int n,j;
5001
LITERAL Lit;
5002
TERM Atom;
5003
5004
n = clause_Length(clause);
5005
5006
if (n == 0)
5007
fputs(" $F ", File);
5008
else {
5009
for (j = 0; j < n; j++) {
5010
Lit = clause_GetLiteral(clause,j);
5011
Atom = clause_LiteralAtom(Lit);
5012
if (clause_LiteralIsNegative(Lit))
5013
putc('-', File);
5014
if (fol_IsEquality(Atom)) {
5015
if (clause_LiteralIsNegative(Lit))
5016
putc('(', File);
5017
term_FPrintOtterPrefix(File,term_FirstArgument(Atom));
5018
fputs(" = ", File);
5019
term_FPrintOtterPrefix(File,term_SecondArgument(Atom));
5020
if (clause_LiteralIsNegative(Lit))
5021
putc(')', File);
5022
}
5023
else
5024
term_FPrintOtterPrefix(File,Atom);
5025
if (j <= (n-2))
5026
fputs(" | ", File);
5027
}
5028
}
5029
5030
fputs(".\n", File);
5031
}
5032
5033
5034
void clause_FPrintCnfDFG(FILE* File, BOOL OnlyProductive, LIST Axioms,
5035
LIST Conjectures, FLAGSTORE Flags,
5036
PRECEDENCE Precedence)
5037
/**************************************************************
5038
INPUT: A file, a list of axiom clauses and a list of conjecture clauses.
5039
A flag indicating whether only potentially productive clauses should
5040
be printed.
5041
A flag store.
5042
A precedence.
5043
RETURNS: Nothing.
5044
SUMMARY: Prints a the respective clause lists to <File> dependent
5045
on <OnlyProductive>.
5046
***************************************************************/
5047
{
5048
LIST scan;
5049
CLAUSE Clause;
5050
5051
if (Axioms) {
5052
fputs("list_of_clauses(axioms, cnf).\n", File);
5053
for (scan=Axioms;!list_Empty(scan);scan=list_Cdr(scan)) {
5054
Clause = (CLAUSE)list_Car(scan);
5055
if (!OnlyProductive ||
5056
(clause_HasSolvedConstraint(Clause) &&
5057
!clause_HasSelectedLiteral(Clause, Flags, Precedence)))
5058
clause_FPrintDFG(File,Clause,FALSE);
5059
}
5060
fputs("end_of_list.\n\n", File);
5061
}
5062
5063
if (Conjectures) {
5064
fputs("list_of_clauses(conjectures, cnf).\n", File);
5065
for (scan=Conjectures;!list_Empty(scan);scan=list_Cdr(scan)) {
5066
Clause = (CLAUSE)list_Car(scan);
5067
if (!OnlyProductive ||
5068
(clause_HasSolvedConstraint(Clause) &&
5069
!clause_HasSelectedLiteral(Clause, Flags, Precedence)))
5070
clause_FPrintDFG(File,Clause,FALSE);
5071
}
5072
fputs("end_of_list.\n\n", File);
5073
}
5074
}
5075
5076
void clause_FPrintCnfDFGProof(FILE* File, BOOL OnlyProductive, LIST Axioms,
5077
LIST Conjectures, FLAGSTORE Flags,
5078
PRECEDENCE Precedence)
5079
/**************************************************************
5080
INPUT: A file, a list of axiom clauses and a list of conjecture clauses.
5081
A flag indicating whether only potentially productive clauses should
5082
be printed.
5083
A flag store.
5084
A precedence.
5085
RETURNS: Nothing.
5086
SUMMARY: Prints a the respective clause lists to <File> dependent
5087
on <OnlyProductive>.
5088
***************************************************************/
5089
{
5090
LIST scan;
5091
CLAUSE Clause;
5092
5093
if (Axioms) {
5094
fputs("list_of_clauses(axioms, cnf).\n", File);
5095
for (scan=Axioms;!list_Empty(scan);scan=list_Cdr(scan)) {
5096
Clause = (CLAUSE)list_Car(scan);
5097
if (!OnlyProductive ||
5098
(clause_HasSolvedConstraint(Clause) &&
5099
!clause_HasSelectedLiteral(Clause, Flags, Precedence)))
5100
clause_FPrintDFGProof(File,Clause,FALSE);
5101
}
5102
fputs("end_of_list.\n\n", File);
5103
}
5104
5105
if (Conjectures) {
5106
fputs("list_of_clauses(conjectures, cnf).\n", File);
5107
for (scan=Conjectures;!list_Empty(scan);scan=list_Cdr(scan)) {
5108
Clause = (CLAUSE)list_Car(scan);
5109
if (!OnlyProductive ||
5110
(clause_HasSolvedConstraint(Clause) &&
5111
!clause_HasSelectedLiteral(Clause, Flags, Precedence)))
5112
clause_FPrintDFGProof(File,Clause,FALSE);
5113
}
5114
fputs("end_of_list.\n\n", File);
5115
}
5116
}
5117
5118
5119
static void clause_FPrintDescription(FILE* File, const char* Name,
5120
const char* Author, const char* Status,
5121
const char* Description)
5122
{
5123
fputs("list_of_descriptions.\n", File);
5124
fprintf(File, "name(%s).\n", Name);
5125
fprintf(File, "author(%s).\n", Author);
5126
fprintf(File, "status(%s).\n", Status);
5127
fprintf(File, "description(%s).\n", Description);
5128
fputs("end_of_list.\n", File);
5129
}
5130
5131
static void clause_FPrintClauseFomulaRelationForClauses(FILE* File, LIST Clauses,
5132
HASH ClauseToTermLabelList)
5133
/**************************************************************
5134
INPUT: A file, a list of axioms, a list of conjectures,
5135
and a relationship between clauses and formala names.
5136
RETURNS: Nothing.
5137
SUMMARY: Prints relationship between clauses and formula names
5138
to <File>.
5139
***************************************************************/
5140
{
5141
LIST Scan, ValueList;
5142
5143
for (Scan=Clauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
5144
ValueList = hsh_Get(ClauseToTermLabelList, list_Car(Scan));
5145
if (!list_Empty(ValueList)) {
5146
fprintf(File, "(%d,", clause_Number(list_Car(Scan)));
5147
fputs(list_Car(ValueList), File);
5148
ValueList = list_Cdr(ValueList);
5149
while (!list_Empty(ValueList)) {
5150
fputs(",", File);
5151
fputs(list_Car(ValueList), File);
5152
ValueList = list_Cdr(ValueList);
5153
}
5154
fputs(")", File);
5155
if (!list_Empty(list_Cdr(Scan)))
5156
fputs(",\n ", File);
5157
}
5158
}
5159
}
5160
5161
static void clause_FPrintClauseFormulaRelation(FILE* File, LIST Axioms,
5162
LIST Conjectures, HASH ClauseToTermLabelList)
5163
/**************************************************************
5164
INPUT: A file, a list of axioms, a list of conjectures,
5165
and a relationship between clauses and formala names.
5166
RETURNS: Nothing.
5167
SUMMARY: Prints relationship between clauses and formula names
5168
to <File>.
5169
***************************************************************/
5170
{
5171
fputs("set_ClauseFormulaRelation(", File);
5172
clause_FPrintClauseFomulaRelationForClauses(File, Axioms, ClauseToTermLabelList);
5173
clause_FPrintClauseFomulaRelationForClauses(File, Conjectures, ClauseToTermLabelList);
5174
fputs(").\n\n\n", File);
5175
}
5176
5177
static void clause_FPrintSelectedSymbols(FILE* File)
5178
/**************************************************************
5179
INPUT: A file.
5180
RETURNS: Nothing.
5181
SUMMARY: Prints selected symbols to <File>.
5182
***************************************************************/
5183
{
5184
LIST Scan, SelectedSymbols;
5185
5186
SelectedSymbols = symbol_GetAllSymbolsWithProperty(SELECTED);
5187
5188
/* Print the selected symbols. */
5189
if (!list_Empty(SelectedSymbols)) {
5190
fputs("set_selection(", File);
5191
5192
for (Scan = SelectedSymbols; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
5193
SYMBOL Symbol;
5194
5195
Symbol = (SYMBOL)list_Car(Scan);
5196
fputs(symbol_Name(Symbol), File);
5197
5198
/* If there are more selected symbols following, add a ',' after the symbol. */
5199
if (!list_Empty(list_Cdr(Scan)))
5200
putc(',', File);
5201
}
5202
fputs(").\n\n\n", File);
5203
5204
list_Free(SelectedSymbols);
5205
}
5206
}
5207
5208
static void clause_FPrintSettings(FILE* File, LIST Axioms,
5209
LIST Conjectures, FLAGSTORE Flags,
5210
PRECEDENCE Precedence, HASH ClauseToTermLabelList)
5211
/**************************************************************
5212
INPUT: A file, a list of axioms, a list of conjectures,
5213
a flag store, a precedence, a relationship
5214
between clauses and formula names.
5215
RETURNS: Nothing.
5216
SUMMARY: Prints SPASS settings to <File>.
5217
***************************************************************/
5218
{
5219
fputs("list_of_settings(SPASS).\n{*\n", File);
5220
if (ClauseToTermLabelList != (HASH)NULL)
5221
clause_FPrintClauseFormulaRelation(File, Axioms, Conjectures, ClauseToTermLabelList);
5222
5223
/* Print just the necessary flags. */
5224
if (Flags != NULL) {
5225
flag_FPrintFlag(File, Flags, flag_ORD);
5226
flag_FPrintFlag(File, Flags, flag_SELECT);
5227
fputs("\nset_flag(RInput,0).",File);
5228
fputs("\n\n", File);
5229
5230
/* Print the selected symbols. */
5231
if(flag_GetFlagIntValue(Flags, flag_SELECT) != flag_SELECTOFF)
5232
clause_FPrintSelectedSymbols(File);
5233
}
5234
5235
if(Precedence != NULL)
5236
symbol_FPrintPrecedence(File, Precedence);
5237
5238
fputs("*}\nend_of_list.\n\n", File);
5239
}
5240
5241
static void clause_FPrintClauses(FILE* File, BOOL OnlyProductive,
5242
BOOL PrintConjectures, LIST Clauses,
5243
FLAGSTORE Flags, PRECEDENCE Precedence)
5244
/**************************************************************
5245
INPUT: A file, a flag indicating whether only potentially
5246
productive clauses should be printed, a flag
5247
indicating whether only conjectures or only axioms
5248
should be printed, a list of clauses, an optional
5249
flag store and an optional precedence.
5250
RETURNS: Nothing.
5251
SUMMARY: Prints (productive) axiom or conjecture clauses to
5252
<File>.
5253
***************************************************************/
5254
{
5255
LIST Scan;
5256
5257
for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) {
5258
CLAUSE Clause;
5259
5260
Clause = (CLAUSE) list_Car(Scan);
5261
5262
if (!OnlyProductive ||
5263
(clause_HasSolvedConstraint(Clause) &&
5264
!clause_HasSelectedLiteral(Clause, Flags, Precedence)))
5265
if (PrintConjectures == clause_GetFlag(Clause,CONCLAUSE))
5266
clause_FPrintDFG(File,Clause,FALSE);
5267
}
5268
}
5269
5270
void clause_FPrintCnfDFGProblem(FILE* File, BOOL OnlyProductive,
5271
const char* Name, const char* Author,
5272
const char* Status, const char* Description,
5273
LIST Clauses, LIST Conjectures,
5274
FLAGSTORE Flags, PRECEDENCE Precedence,
5275
HASH ClauseToTermLabelList,
5276
BOOL IsModel, BOOL PrintSettings)
5277
/**************************************************************
5278
INPUT: A file, a flag indicating whether only potentially
5279
productive clauses should be printed, the problem's
5280
name, author, status and description to be included
5281
in the description block given as strings, a list
5282
of clauses, an optional additional list of
5283
conjectures, an optional flag store, an optional
5284
precedence, an optional relationship between
5285
clauses and formula names, whether the problem
5286
is a model, and whether the settings should be printed.
5287
RETURNS: Nothing.
5288
SUMMARY: Prints a complete DFG problem clause file to <File>.
5289
***************************************************************/
5290
{
5291
fputs("begin_problem(Unknown).\n\n", File);
5292
clause_FPrintDescription(File, Name, Author, Status, Description);
5293
putc('\n', File);
5294
5295
fputs("list_of_symbols.\n", File);
5296
symbol_FPrintDFGSignature(File);
5297
fputs("end_of_list.\n\n", File);
5298
5299
/* Since Clauses can hold both axioms and conjectures, it's
5300
* printed in both cases, once just the axioms, the other time
5301
* just the conjectures, except when we're printing a model.
5302
* If we are printing a model, the conjectures are printed
5303
* along with the axioms, to keep prior behaviour.
5304
*/
5305
fputs("list_of_clauses(axioms, cnf).\n", File);
5306
clause_FPrintClauses(File, OnlyProductive, FALSE,
5307
Clauses, Flags, Precedence);
5308
if(IsModel)
5309
clause_FPrintClauses(File, OnlyProductive, TRUE,
5310
Clauses, Flags, Precedence);
5311
fputs("end_of_list.\n\n", File);
5312
5313
fputs("list_of_clauses(conjectures, cnf).\n", File);
5314
if(!IsModel)
5315
clause_FPrintClauses(File, OnlyProductive, TRUE,
5316
Clauses, Flags, Precedence);
5317
clause_FPrintClauses(File, OnlyProductive, TRUE,
5318
Conjectures, Flags, Precedence);
5319
fputs("end_of_list.\n\n", File);
5320
5321
if(PrintSettings)
5322
clause_FPrintSettings(File, Clauses, Conjectures, Flags,
5323
Precedence, ClauseToTermLabelList);
5324
5325
fputs("\nend_problem.\n\n", File);
5326
}
5327
5328
void clause_FPrintCnfFormulasDFGProblem(FILE* File, BOOL OnlyProductive,
5329
const char* Name, const char* Author,
5330
const char* Status,
5331
const char* Description, LIST Axioms,
5332
LIST Conjectures, FLAGSTORE Flags,
5333
PRECEDENCE Precedence)
5334
/**************************************************************
5335
INPUT: A file, a list of axiom clauses and a list of conjecture clauses.
5336
A flag indicating whether only potentially productive clauses should
5337
be printed.
5338
A bunch of strings that are printed to the description.
5339
A flag store.
5340
A precedence.
5341
RETURNS: Nothing.
5342
SUMMARY: Prints the respective clause lists as a complete DFG formulae output
5343
to <File>.
5344
***************************************************************/
5345
{
5346
LIST scan;
5347
CLAUSE Clause;
5348
5349
fputs("begin_problem(Unknown).\n\n", File);
5350
clause_FPrintDescription(File, Name, Author, Status, Description);
5351
fputs("\nlist_of_symbols.\n", File);
5352
symbol_FPrintDFGSignature(File);
5353
fputs("end_of_list.\n\n", File);
5354
5355
if (Axioms) {
5356
fputs("list_of_formulae(axioms).\n", File);
5357
for (scan=Axioms; !list_Empty(scan); scan=list_Cdr(scan)) {
5358
Clause = (CLAUSE)list_Car(scan);
5359
if (!OnlyProductive ||
5360
(clause_HasSolvedConstraint(Clause) &&
5361
!clause_HasSelectedLiteral(Clause, Flags, Precedence)))
5362
clause_FPrintFormulaDFG(File,Clause,FALSE);
5363
}
5364
fputs("end_of_list.\n\n", File);
5365
}
5366
5367
if (Conjectures) {
5368
fputs("list_of_formulae(conjectures).\n", File);
5369
for (scan=Conjectures; !list_Empty(scan); scan=list_Cdr(scan)) {
5370
Clause = (CLAUSE)list_Car(scan);
5371
if (!OnlyProductive ||
5372
(clause_HasSolvedConstraint(Clause) &&
5373
!clause_HasSelectedLiteral(Clause, Flags, Precedence)))
5374
clause_FPrintFormulaDFG(File,Clause,FALSE);
5375
}
5376
fputs("end_of_list.\n\n", File);
5377
}
5378
5379
fputs("list_of_settings(SPASS).\n{*\n", File);
5380
fol_FPrintPrecedence(File, Precedence);
5381
fputs("\n*}\nend_of_list.\n\nend_problem.\n\n", File);
5382
}
5383
5384
void clause_FPrintCnfOtter(FILE* File, LIST Clauses, FLAGSTORE Flags)
5385
/**************************************************************
5386
INPUT: A file, a list of clauses and a flag store.
5387
RETURNS: Nothing.
5388
SUMMARY: Prints the clauses to <File> in a format readable by Otter.
5389
***************************************************************/
5390
{
5391
LIST scan;
5392
int i;
5393
BOOL Equality;
5394
CLAUSE Clause;
5395
5396
Equality = FALSE;
5397
5398
for (scan=Clauses;!list_Empty(scan) && !Equality; scan=list_Cdr(scan)) {
5399
Clause = (CLAUSE)list_Car(scan);
5400
for (i=clause_FirstAntecedentLitIndex(Clause);i<clause_Length(Clause);i++)
5401
if (fol_IsEquality(clause_GetLiteralAtom(Clause,i))) {
5402
Equality = TRUE;
5403
i = clause_Length(Clause);
5404
}
5405
}
5406
5407
fol_FPrintOtterOptions(File, Equality,
5408
flag_GetFlagIntValue(Flags, flag_TDFG2OTTEROPTIONS));
5409
5410
if (Clauses) {
5411
fputs("list(usable).\n", File);
5412
if (Equality)
5413
fputs("x=x.\n", File);
5414
for (scan=Clauses;!list_Empty(scan);scan=list_Cdr(scan))
5415
clause_FPrintOtter(File,list_Car(scan));
5416
fputs("end_of_list.\n\n", File);
5417
}
5418
}
5419
5420
5421
void clause_FPrintCnfDFGDerivables(FILE* File, LIST Clauses, BOOL Type)
5422
/**************************************************************
5423
INPUT: A file, a list of clauses and a bool flag Type.
5424
RETURNS: Nothing.
5425
SUMMARY: If <Type> is true then all axiom clauses in <Clauses> are
5426
written to <File>. Otherwise all conjecture clauses in
5427
<Clauses> are written to <File>.
5428
***************************************************************/
5429
{
5430
CLAUSE Clause;
5431
5432
while (Clauses) {
5433
Clause = (CLAUSE)list_Car(Clauses);
5434
if ((Type && !clause_GetFlag(Clause,CONCLAUSE)) ||
5435
(!Type && clause_GetFlag(Clause,CONCLAUSE)))
5436
clause_FPrintDFG(File,Clause,FALSE);
5437
Clauses = list_Cdr(Clauses);
5438
}
5439
}
5440
5441
5442
void clause_FPrintDFGStep(FILE* File, CLAUSE Clause, BOOL Justif)
5443
/**************************************************************
5444
INPUT: A file, a clause and a boolean value.
5445
RETURNS: Nothing.
5446
SUMMARY: Prints any clause together with a label (the clause number)
5447
to File. If <Justif> is TRUE also the labels of the parent
5448
clauses are printed.
5449
CAUTION: Uses the other clause_Output functions.
5450
***************************************************************/
5451
{
5452
int n,j;
5453
LITERAL Lit;
5454
TERM Atom;
5455
LIST Variables,Iter;
5456
5457
n = clause_Length(Clause);
5458
5459
fputs(" step(", File);
5460
fprintf(File, "%d,", clause_Number(Clause));
5461
5462
Variables = list_Nil();
5463
5464
for (j = 0; j < n; j++)
5465
Variables =
5466
list_NPointerUnion(Variables,
5467
term_VariableSymbols(clause_GetLiteralAtom(Clause,j)));
5468
5469
if (!list_Empty(Variables)) {
5470
symbol_FPrint(File, fol_All());
5471
fputs("([", File);
5472
for (Iter = Variables; !list_Empty(Iter); Iter = list_Cdr(Iter)) {
5473
symbol_FPrint(File, (SYMBOL) list_Car(Iter));
5474
if (!list_Empty(list_Cdr(Iter)))
5475
putc(',', File);
5476
}
5477
fputs("],", File);
5478
}
5479
5480
symbol_FPrint(File, fol_Or());
5481
putc('(', File);
5482
5483
for (j = 0; j < n; j++) {
5484
Lit = clause_GetLiteral(Clause,j);
5485
Atom = clause_LiteralSignedAtom(Lit);
5486
term_FPrintPrefix(File,Atom);
5487
if (j+1 < n)
5488
putc(',', File);
5489
}
5490
if (n==0)
5491
symbol_FPrint(File,fol_False());
5492
5493
if (!list_Empty(Variables)) {
5494
list_Delete(Variables);
5495
putc(')', File);
5496
}
5497
fputs("),", File);
5498
clause_FPrintOrigin(File, Clause);
5499
5500
fputs(",[", File);
5501
for (Iter = clause_ParentClauses(Clause);
5502
!list_Empty(Iter);
5503
Iter = list_Cdr(Iter)) {
5504
fprintf(File, "%d", (int)list_Car(Iter));
5505
if (!list_Empty(list_Cdr(Iter)))
5506
putc(',', File);
5507
}
5508
putc(']', File);
5509
fprintf(File, ",[splitlevel:%d]", clause_SplitLevel(Clause));
5510
5511
fputs(").\n", File);
5512
}
5513
5514
void clause_FPrintDFGProof(FILE* File, CLAUSE Clause, BOOL Justif)
5515
/**************************************************************
5516
INPUT: A file, a clause and a boolean value.
5517
RETURNS: Nothing.
5518
SUMMARY: Prints any clause together with a label (the clause number)
5519
to File. If Justif is TRUE also the labels of the parent
5520
clauses are printed.
5521
CAUTION: Uses the other clause_Output functions.
5522
***************************************************************/
5523
{
5524
int n,j;
5525
LITERAL Lit;
5526
TERM Atom;
5527
LIST Variables,Iter;
5528
5529
n = clause_Length(Clause);
5530
5531
fputs(" clause(", File);
5532
Variables = list_Nil();
5533
5534
for (j = 0; j < n; j++)
5535
Variables =
5536
list_NPointerUnion(Variables,
5537
term_VariableSymbols(clause_GetLiteralAtom(Clause,j)));
5538
5539
if (!list_Empty(Variables)) {
5540
symbol_FPrint(File, fol_All());
5541
fputs("([", File);
5542
for (Iter = Variables; !list_Empty(Iter); Iter = list_Cdr(Iter)) {
5543
symbol_FPrint(File, (SYMBOL) list_Car(Iter));
5544
if (!list_Empty(list_Cdr(Iter)))
5545
putc(',', File);
5546
}
5547
fputs("],", File);
5548
}
5549
5550
symbol_FPrint(File, fol_Or());
5551
putc('(', File);
5552
5553
for (j = 0; j < n; j++) {
5554
Lit = clause_GetLiteral(Clause,j);
5555
Atom = clause_LiteralSignedAtom(Lit);
5556
term_FPrintPrefix(File,Atom);
5557
if (j+1 < n)
5558
putc(',', File);
5559
}
5560
if (n==0)
5561
symbol_FPrint(File,fol_False());
5562
5563
if (!list_Empty(Variables)) {
5564
list_Delete(Variables);
5565
putc(')', File);
5566
}
5567
fprintf(File, "),%d", clause_Number(Clause));
5568
5569
if (Justif) {
5570
putc(',', File);
5571
clause_FPrintOrigin(File, Clause);
5572
fputs(",[", File);
5573
for (Iter = clause_ParentClauses(Clause);
5574
!list_Empty(Iter);
5575
Iter = list_Cdr(Iter)) {
5576
fprintf(File, "%d", (int)list_Car(Iter));
5577
if (!list_Empty(list_Cdr(Iter)))
5578
putc(',', File);
5579
}
5580
putc(']', File);
5581
fprintf(File, ",%d", clause_SplitLevel(Clause));
5582
}
5583
5584
fputs(").\n", File);
5585
}
5586
5587
void clause_FPrintDFG(FILE* File, CLAUSE Clause, BOOL Justif)
5588
/**************************************************************
5589
INPUT: A file, a clause and a boolean value.
5590
RETURNS: Nothing.
5591
SUMMARY: Prints any clause together with a label (the clause number)
5592
to File. If Justif is TRUE also the labels of the parent
5593
clauses are printed.
5594
CAUTION: Uses the other clause_Output functions.
5595
***************************************************************/
5596
{
5597
int n,j,c,a,s;
5598
LITERAL Lit;
5599
LIST Iter;
5600
5601
fputs(" clause(", File);
5602
5603
n = clause_Length(Clause);
5604
if (n==0)
5605
symbol_FPrint(File,fol_False());
5606
else {
5607
c = clause_NumOfConsLits(Clause);
5608
a = clause_NumOfAnteLits(Clause);
5609
s = clause_NumOfSuccLits(Clause);
5610
5611
for (j = 0; j < c; j++) {
5612
putchar(' ');
5613
Lit = clause_GetLiteral(Clause, j);
5614
clause_LiteralFPrintUnsigned(File, Lit);
5615
if (j+1 < c)
5616
putc(' ', File);
5617
}
5618
fputs(" || ", File);
5619
5620
a += c;
5621
for ( ; j < a; j++) {
5622
Lit = clause_GetLiteral(Clause, j);
5623
clause_LiteralFPrintUnsigned(File, Lit);
5624
if (clause_LiteralGetFlag(Lit,LITSELECT))
5625
putc('+', File);
5626
if (j+1 < a)
5627
putc(' ', File);
5628
}
5629
fputs(" -> ",File);
5630
5631
s += a;
5632
for ( ; j < s; j++) {
5633
Lit = clause_GetLiteral(Clause, j);
5634
clause_LiteralFPrintUnsigned(File, Lit);
5635
#ifdef CHECK
5636
if (clause_LiteralGetFlag(Lit,LITSELECT)) {
5637
misc_StartErrorReport();
5638
misc_ErrorReport("\n In clause_FPrintDFG: Clause has selected positive literal.\n");
5639
misc_FinishErrorReport();
5640
}
5641
#endif
5642
if (j+1 < s)
5643
putc(' ', File);
5644
}
5645
}
5646
5647
fprintf(File, ",%d", clause_Number(Clause));
5648
5649
if (Justif) {
5650
putc(',', File);
5651
clause_FPrintOrigin(File, Clause);
5652
fputs(",[", File);
5653
for (Iter = clause_ParentClauses(Clause);
5654
!list_Empty(Iter);
5655
Iter = list_Cdr(Iter)) {
5656
fprintf(File, "%d", (int)list_Car(Iter));
5657
if (!list_Empty(list_Cdr(Iter)))
5658
putc(',', File);
5659
}
5660
putc(']', File);
5661
fprintf(File, ",%d", clause_SplitLevel(Clause));
5662
}
5663
5664
fputs(").\n", File);
5665
}
5666
5667
void clause_FPrintFormulaDFG(FILE* File, CLAUSE Clause, BOOL Justif)
5668
/**************************************************************
5669
INPUT: A file, a clause and a boolean value.
5670
RETURNS: Nothing.
5671
SUMMARY: Prints any clause together with a label (the clause number)
5672
as DFG Formula to File. If Justif is TRUE also the labels of the
5673
parent clauses are printed.
5674
CAUTION: Uses the other clause_Output functions.
5675
***************************************************************/
5676
{
5677
int n,j;
5678
LITERAL Lit;
5679
TERM Atom;
5680
LIST Variables,Iter;
5681
5682
n = clause_Length(Clause);
5683
5684
fputs(" formula(", File);
5685
Variables = list_Nil();
5686
5687
for (j = 0; j < n; j++)
5688
Variables =
5689
list_NPointerUnion(Variables,
5690
term_VariableSymbols(clause_GetLiteralAtom(Clause,j)));
5691
5692
if (!list_Empty(Variables)) {
5693
symbol_FPrint(File, fol_All());
5694
fputs("([", File);
5695
for (Iter = Variables; !list_Empty(Iter); Iter = list_Cdr(Iter)) {
5696
symbol_FPrint(File, (SYMBOL) list_Car(Iter));
5697
if (!list_Empty(list_Cdr(Iter)))
5698
putc(',', File);
5699
}
5700
fputs("],", File);
5701
}
5702
5703
if (n>1) {
5704
symbol_FPrint(File, fol_Or());
5705
putc('(', File);
5706
}
5707
5708
for (j = 0; j < n; j++) {
5709
Lit = clause_GetLiteral(Clause,j);
5710
Atom = clause_LiteralSignedAtom(Lit);
5711
term_FPrintPrefix(File,Atom);
5712
if (j+1 < n)
5713
putc(',', File);
5714
}
5715
if (n==0)
5716
symbol_FPrint(File,fol_False());
5717
5718
if (!list_Empty(Variables)) {
5719
list_Delete(Variables);
5720
putc(')', File);
5721
}
5722
5723
if (n>1)
5724
fprintf(File, "),%d", clause_Number(Clause));
5725
else
5726
fprintf(File, ",%d", clause_Number(Clause));
5727
5728
if (Justif) {
5729
putc(',', File);
5730
clause_FPrintOrigin(File, Clause);
5731
fputs(",[", File);
5732
for (Iter = clause_ParentClauses(Clause);
5733
!list_Empty(Iter);
5734
Iter = list_Cdr(Iter)) {
5735
fprintf(File, "%d", (int)list_Car(Iter));
5736
if (!list_Empty(list_Cdr(Iter)))
5737
putc(',', File);
5738
}
5739
putc(']', File);
5740
fprintf(File, ",%d", clause_SplitLevel(Clause));
5741
}
5742
5743
fputs(").\n", File);
5744
}
5745
5746
5747
void clause_CheckAux(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence, BOOL VarIsConst)
5748
/**************************************************************
5749
INPUT: A clause, a flag store and a precedence and a flag.
5750
RETURNS: Nothing.
5751
EFFECT: Checks whether the clause is in a proper state. If
5752
not, a core is dumped.
5753
CAUTION: If <VarIsConst> is set to TRUE variables of
5754
<Clause> are interpreted as constants
5755
***************************************************************/
5756
{
5757
CLAUSE Copy;
5758
if (!clause_Exists(Clause))
5759
return;
5760
5761
if (!clause_IsClauseAux(Clause, Flags, Precedence, VarIsConst)) {
5762
misc_StartErrorReport();
5763
misc_ErrorReport("\n In clause_Check: Clause not consistent !\n");
5764
misc_FinishErrorReport();
5765
}
5766
5767
Copy = clause_Copy(Clause);
5768
5769
if(VarIsConst)
5770
clause_OrientAndReInitSkolem(Copy, Flags, Precedence);
5771
else
5772
clause_OrientAndReInit(Copy, Flags, Precedence);
5773
5774
if ((clause_Weight(Clause) != clause_Weight(Copy)) ||
5775
(clause_MaxVar(Clause) != clause_MaxVar(Copy))) {
5776
misc_StartErrorReport();
5777
misc_ErrorReport("\n In clause_Check: Weight or maximal variable not properly set.\n");
5778
misc_FinishErrorReport();
5779
}
5780
clause_Delete(Copy);
5781
}
5782
5783
void clause_Check(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence)
5784
/**************************************************************
5785
INPUT: A clause, a flag store and a precedence.
5786
RETURNS: Nothing.
5787
EFFECT: Checks whether the clause is in a proper state. If
5788
not, a core is dumped.
5789
***************************************************************/
5790
{
5791
clause_CheckAux(Clause, Flags, Precedence, FALSE);
5792
}
5793
5794
5795
void clause_CheckSkolem(CLAUSE Clause, FLAGSTORE Flags, PRECEDENCE Precedence)
5796
/**************************************************************
5797
INPUT: A clause, a flag store and a precedence.
5798
RETURNS: Nothing.
5799
EFFECT: Checks whether the clause is in a proper state. If
5800
not, a core is dumped.
5801
***************************************************************/
5802
{
5803
clause_CheckAux(Clause, Flags, Precedence, TRUE);
5804
}
5805
5806
/* The following are output procedures for clauses with parent pointers */
5807
5808
5809
void clause_PParentsFPrintParentClauses(FILE* File, CLAUSE Clause, BOOL ParentPts)
5810
/**************************************************************
5811
INPUT: A file, a clause and a boolean flag indicating whether
5812
the clause's parents are given by numbers or pointers.
5813
RETURNS: Nothing.
5814
SUMMARY: Prints the clauses parent clauses and -literals to the file.
5815
If <ParentPts> is TRUE the parent clauses are defined
5816
by pointers, else by numbers.
5817
***************************************************************/
5818
{
5819
LIST Scan1,Scan2;
5820
int length;
5821
int ParentNum;
5822
5823
if (!list_Empty(clause_ParentClauses(Clause))) {
5824
5825
Scan1 = clause_ParentClauses(Clause);
5826
Scan2 = clause_ParentLiterals(Clause);
5827
5828
if (ParentPts)
5829
ParentNum = clause_Number(list_Car(Scan1));
5830
else
5831
ParentNum = (int)list_Car(Scan1);
5832
5833
fprintf(File, "%d.%d", ParentNum, (int)list_Car(Scan2));
5834
5835
if (!list_Empty(list_Cdr(Scan1))) {
5836
5837
length = list_Length(Scan1) - 2;
5838
putc(',', File);
5839
Scan1 = list_Cdr(Scan1);
5840
Scan2 = list_Cdr(Scan2);
5841
5842
if (ParentPts)
5843
ParentNum = clause_Number(list_Car(Scan1));
5844
else
5845
ParentNum = (int)list_Car(Scan1);
5846
5847
fprintf(File, "%d.%d", ParentNum, (int)list_Car(Scan2));
5848
5849
for (Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2);
5850
!list_Empty(Scan1);
5851
Scan1 = list_Cdr(Scan1), Scan2 = list_Cdr(Scan2)) {
5852
5853
length -= 2;
5854
5855
if (ParentPts)
5856
ParentNum = clause_Number(list_Car(Scan1));
5857
else
5858
ParentNum = (int)list_Car(Scan1);
5859
5860
fprintf(File, ",%d.%d", ParentNum, (int)list_Car(Scan2));
5861
}
5862
}
5863
}
5864
}
5865
5866
void clause_PParentsLiteralFPrintUnsigned(FILE* File, LITERAL Literal)
5867
/**************************************************************
5868
INPUT: A Literal.
5869
RETURNS: Nothing.
5870
SUMMARY:
5871
***************************************************************/
5872
{
5873
#ifdef CHECK
5874
if (!clause_LiteralIsLiteral(Literal)) {
5875
misc_StartErrorReport();
5876
misc_ErrorReport("\n In clause_PParentsLiteralFPrintUnsigned:");
5877
misc_ErrorReport("\n Illegal input. Input not a literal.");
5878
misc_FinishErrorReport();
5879
}
5880
#endif
5881
5882
term_FPrintPrefix(File, clause_LiteralAtom(Literal));
5883
fflush(stdout);
5884
}
5885
5886
void clause_PParentsFPrintGen(FILE* File, CLAUSE Clause, BOOL ParentPts)
5887
/**************************************************************
5888
INPUT: A file, a clause, a boolean flag.
5889
RETURNS: Nothing.
5890
EFFECTS: Prints the clause to file in SPASS format. If <ParentPts>
5891
is TRUE, the parents of <Clause> are interpreted as pointers.
5892
***************************************************************/
5893
{
5894
LITERAL Lit;
5895
int i,c,a,s;
5896
5897
if (!clause_Exists(Clause))
5898
fputs("(CLAUSE)NULL", File);
5899
else {
5900
fprintf(File, "%d",clause_Number(Clause));
5901
5902
fprintf(File, "[%d:", clause_SplitLevel(Clause));
5903
5904
#ifdef CHECK
5905
if (Clause->splitfield_length <= 1)
5906
fputs("0.", File);
5907
else
5908
for (i=Clause->splitfield_length-1; i > 0; i--)
5909
fprintf(File, "%lu.", Clause->splitfield[i]);
5910
if (Clause->splitfield_length == 0)
5911
putc('1', File);
5912
else
5913
fprintf(File, "%lu", (Clause->splitfield[0] | 1));
5914
fprintf(File,":%c%c:%c:%d:%d:", clause_GetFlag(Clause, CONCLAUSE) ? 'C' : 'A',
5915
clause_GetFlag(Clause, WORKEDOFF) ? 'W' : 'U',
5916
clause_GetFlag(Clause, NOPARAINTO) ? 'N' : 'P',
5917
clause_Weight(Clause), clause_Depth(Clause));
5918
#endif
5919
5920
clause_FPrintOrigin(File, Clause);
5921
5922
if (!list_Empty(clause_ParentClauses(Clause))) {
5923
putc(':', File);
5924
clause_PParentsFPrintParentClauses(File, Clause, ParentPts);
5925
}
5926
putc(']', File);
5927
5928
c = clause_NumOfConsLits(Clause);
5929
a = clause_NumOfAnteLits(Clause);
5930
s = clause_NumOfSuccLits(Clause);
5931
5932
for (i = 0; i < c; i++) {
5933
Lit = clause_GetLiteral(Clause, i);
5934
clause_PParentsLiteralFPrintUnsigned(File, Lit);
5935
if (i+1 < c)
5936
putc(' ', File);
5937
}
5938
fputs(" || ", File);
5939
5940
a += c;
5941
for ( ; i < a; i++) {
5942
5943
Lit = clause_GetLiteral(Clause, i);
5944
clause_PParentsLiteralFPrintUnsigned(File, Lit);
5945
if (clause_LiteralIsMaximal(Lit)) {
5946
putc('*', File);
5947
if (clause_LiteralIsOrientedEquality(Lit))
5948
putc('*', File);
5949
}
5950
if (clause_LiteralGetFlag(Lit,LITSELECT))
5951
putc('+', File);
5952
if (i+1 < a)
5953
putc(' ', File);
5954
}
5955
fputs(" -> ",File);
5956
5957
s += a;
5958
for ( ; i < s; i++) {
5959
5960
Lit = clause_GetLiteral(Clause, i);
5961
clause_PParentsLiteralFPrintUnsigned(File, Lit);
5962
if (clause_LiteralIsMaximal(Lit)) {
5963
putc('*', File);
5964
if (clause_LiteralIsOrientedEquality(Lit))
5965
putc('*', File);
5966
}
5967
#ifdef CHECK
5968
if (clause_LiteralGetFlag(Lit, LITSELECT)) {
5969
misc_StartErrorReport();
5970
misc_ErrorReport("\n In clause_PParentsFPrintGen: Clause has selected positive literal.\n");
5971
misc_FinishErrorReport();
5972
}
5973
#endif
5974
if (i+1 < s)
5975
putc(' ', File);
5976
}
5977
putc('.', File);
5978
}
5979
}
5980
5981
void clause_PParentsFPrint(FILE* File, CLAUSE Clause)
5982
/**************************************************************
5983
INPUT: A file handle and a clause.
5984
RETURNS: Nothing.
5985
EFFECTS: Prints out the clause to file in SPASS output format
5986
***************************************************************/
5987
{
5988
clause_PParentsFPrintGen(File, Clause, TRUE);
5989
}
5990
5991
void clause_PParentsListFPrint(FILE* File, LIST L)
5992
/**************************************************************
5993
INPUT: A file handle, a list of clauses with parent pointers
5994
RETURNS: Nothing.
5995
EFFECTS: Print the list to <file>.
5996
***************************************************************/
5997
{
5998
while (!list_Empty(L)) {
5999
clause_PParentsFPrint(File, list_Car(L));
6000
putc('\n', File);
6001
L = list_Cdr(L);
6002
}
6003
}
6004
6005
6006
void clause_PParentsPrint(CLAUSE Clause)
6007
/**************************************************************
6008
INPUT: A clause with parent pointers
6009
RETURNS: Nothing.
6010
EFFECTS: The clause is printed to stdout.
6011
***************************************************************/
6012
{
6013
clause_PParentsFPrint(stdout, Clause);
6014
}
6015
6016
void clause_PParentsListPrint(LIST L)
6017
/**************************************************************
6018
INPUT: A file handle, a list of clauses with parent pointers
6019
RETURNS: Nothing.
6020
EFFECTS: Print the clause list to stdout.
6021
***************************************************************/
6022
{
6023
clause_PParentsListFPrint(stdout, L);
6024
}
Loggerhead is a web-based interface for Breezy
Version: 2.0.1