« back to all changes in this revision
Viewing changes to SPASS/defs.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/defs.c
1
/**************************************************************/
2
/* ********************************************************** */
3
/* * * */
4
/* * DEFINITIONS * */
5
/* * * */
6
/* * $Module: DEFS * */
7
/* * * */
8
/* * Copyright (C) 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.3 $ * */
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: defs.c,v $ */
40
41
#include "cnf.h"
42
#include "defs.h"
43
#include "foldfg.h"
44
45
static void def_DeleteFromClauses(DEF);
46
static void def_DeleteFromTerm(DEF);
47
48
DEF def_CreateFromClauses(TERM ExpTerm, TERM PredTerm, LIST Clauses, LIST Lits,
49
BOOL Con)
50
/**********************************************************
51
INPUT: Two terms, a list of clausenumbers, a list of literal indices and
52
a boolean saying whether all clauses derived by expanding the
53
predicate should be conclauses.
54
RETURNS: A definition consisting of the 2 terms as expansion term and
55
predicate term and the list of parent clause numbers and a list
56
of the indices of the defined predicate in the parent clauses.
57
ToProve and label are set to NULL.
58
********************************************************/
59
{
60
DEF result;
61
62
#ifdef CHECK
63
if (!term_IsTerm(ExpTerm) || !term_IsTerm(PredTerm)) {
64
misc_StartErrorReport();
65
misc_ErrorReport("\n In def_CreateFromClause: Illegal input.");
66
misc_FinishErrorReport();
67
}
68
if (list_Empty(Clauses)) {
69
misc_StartErrorReport();
70
misc_ErrorReport("\n In def_CreateFromClause: No parent clause given.");
71
misc_FinishErrorReport();
72
}
73
#endif
74
75
result = (DEF) memory_Malloc(sizeof(DEF_NODE));
76
result->expansion = ExpTerm;
77
result->predicate = PredTerm;
78
result->toprove = (TERM) NULL;
79
result->parentclauses = list_PairCreate(Clauses, Lits);
80
result->label = (const char*) NULL;
81
result->conjecture = Con;
82
83
return result;
84
}
85
86
DEF def_CreateFromTerm(TERM ExpTerm, TERM PredTerm, TERM ToProve, const char* Label)
87
/**********************************************************
88
INPUT: 3 terms and a term label.
89
RETURNS: A definition consisting of the 3 terms as expansion term,
90
predicate term and term to prove before applying the
91
definition and the label of the parent term.
92
The list of clausenumbers is set to NULL.
93
********************************************************/
94
{
95
DEF result;
96
97
#ifdef CHECK
98
if (!term_IsTerm(ExpTerm) || !term_IsTerm(PredTerm)) {
99
misc_StartErrorReport();
100
misc_ErrorReport("\n In def_CreateFromTerm: Illegal input.");
101
misc_FinishErrorReport();
102
}
103
if (Label == NULL) {
104
misc_StartErrorReport();
105
misc_ErrorReport("\n In def_CreateFromTerm: No parent clause given.");
106
misc_FinishErrorReport();
107
}
108
#endif
109
110
result = (DEF) memory_Malloc(sizeof(DEF_NODE));
111
result->expansion = ExpTerm;
112
result->predicate = PredTerm;
113
result->toprove = ToProve;
114
result->parentclauses = list_PairCreate(list_Nil(), list_Nil());
115
result->label = Label;
116
result->conjecture = FALSE;
117
118
return result;
119
}
120
121
static void def_DeleteFromClauses(DEF D)
122
/**********************************************************
123
INPUT: A definition derived from clauses.
124
EFFECT: The definition is deleted, INCLUDING THE TERMS AND
125
THE LIST OF CLAUSE NUMBERS.
126
********************************************************/
127
{
128
#ifdef CHECK
129
if (!term_IsTerm(def_Expansion(D)) || !term_IsTerm(def_Predicate(D))) {
130
misc_StartErrorReport();
131
misc_ErrorReport("\n In def_DeleteFormClauses: Illegal input.");
132
misc_FinishErrorReport();
133
}
134
#endif
135
136
/* ToProve and Label are NULL */
137
term_Delete(def_Expansion(D));
138
term_Delete(def_Predicate(D));
139
list_Delete(def_ClauseNumberList(D));
140
list_Delete(def_ClauseLitsList(D));
141
list_PairFree(D->parentclauses);
142
143
memory_Free(D, sizeof(DEF_NODE));
144
}
145
146
static void def_DeleteFromTerm(DEF D)
147
/**********************************************************
148
INPUT: A definition derived from a term.
149
EFFECT: The definition is deleted, INCLUDING THE TERMS.
150
THE LABEL IS NOT FREED.
151
********************************************************/
152
{
153
#ifdef CHECK
154
if (!term_IsTerm(def_Expansion(D)) || !term_IsTerm(def_Predicate(D))) {
155
misc_StartErrorReport();
156
misc_ErrorReport("\n In def_DeleteFromTerm: Illegal input.");
157
misc_FinishErrorReport();
158
}
159
#endif
160
161
/* List of clausenumbers is NULL */
162
term_Delete(def_Expansion(D));
163
term_Delete(def_Predicate(D));
164
if (def_ToProve(D) != (TERM) NULL)
165
term_Delete(def_ToProve(D));
166
list_PairFree(D->parentclauses);
167
memory_Free(D, sizeof(DEF_NODE));
168
}
169
170
void def_Delete(DEF D)
171
/**********************************************************
172
INPUT: A definition derived from a term.
173
EFFECT: The definition is deleted.
174
CAUTION: All elements of the definition except of the label are freed.
175
********************************************************/
176
{
177
if (!list_Empty(def_ClauseNumberList(D)))
178
def_DeleteFromClauses(D);
179
else
180
def_DeleteFromTerm(D);
181
}
182
183
int def_PredicateOccurrences(TERM Term, SYMBOL P)
184
/****************************************************
185
INPUT: A term and a predicate symbol.
186
RETURNS: The number of occurrences of the predicate symbol in Term
187
**************************************************/
188
{
189
/* Quantifiers */
190
if (fol_IsQuantifier(term_TopSymbol(Term)))
191
return def_PredicateOccurrences(term_SecondArgument(Term), P);
192
193
/* Junctors and NOT */
194
if (fol_IsJunctor(term_TopSymbol(Term)) ||
195
symbol_Equal(term_TopSymbol(Term),fol_Not())){
196
LIST scan;
197
int count;
198
count = 0;
199
for (scan=term_ArgumentList(Term); !list_Empty(scan); scan=list_Cdr(scan)) {
200
count += def_PredicateOccurrences((TERM) list_Car(scan), P);
201
/* Only the cases count==1 and count>1 are important */
202
if (count > 1)
203
return count;
204
}
205
return count;
206
}
207
208
if (symbol_Equal(term_TopSymbol(Term), P))
209
return 1;
210
return 0;
211
}
212
213
LIST def_ExtractDefsFromTerm(TERM Term, const char* Label)
214
/**************************************************************
215
INPUT: A term and its label.
216
RETURNS: A list of definitions found in the term.
217
NOTE: The Term is not changed, the definitions contain copies.
218
***************************************************************/
219
{
220
TERM andterm;
221
BOOL found;
222
int pol;
223
LIST univars, termlist, defslist, scan;
224
225
/* First check if there is a top level and() so that the Term may
226
contain several definitions */
227
228
andterm = Term;
229
found = FALSE;
230
pol = 1;
231
univars = list_Nil();
232
233
/* Traverse top down universal quantifiers */
234
while (!found) {
235
if ((symbol_Equal(term_TopSymbol(andterm), fol_All()) && (pol == 1))
236
|| (symbol_Equal(term_TopSymbol(andterm), fol_Exist()) && (pol == -1))) {
237
univars = list_Nconc(univars, list_Copy(fol_QuantifierVariables(andterm)));
238
andterm = term_SecondArgument(andterm);
239
}
240
else {
241
if (symbol_Equal(term_TopSymbol(andterm), fol_Not())) {
242
pol = -pol;
243
andterm = term_FirstArgument(andterm);
244
}
245
else
246
found = TRUE;
247
}
248
}
249
250
termlist = list_Nil();
251
/* Check if conjunction was found */
252
if ((symbol_Equal(term_TopSymbol(andterm), fol_And()) && (pol == 1))
253
|| (symbol_Equal(term_TopSymbol(andterm), fol_Or()) && (pol == -1))) {
254
LIST l;
255
/* Flatten nested and/or */
256
/* Make copy of relevant subterm */
257
andterm = cnf_Flatten(term_Copy(andterm), term_TopSymbol(andterm));
258
for (l=term_ArgumentList(andterm); !list_Empty(l); l=list_Cdr(l)) {
259
TERM newterm;
260
newterm = fol_CreateQuantifierAddFather(fol_All(), term_CopyTermList(univars),
261
list_List(list_Car(l)));
262
termlist = list_Cons(newterm, termlist);
263
}
264
/* Arguments are used in new terms */
265
list_Delete(term_ArgumentList(andterm));
266
term_Free(andterm);
267
}
268
else
269
termlist = list_List(term_Copy(Term));
270
271
list_Delete(univars);
272
273
/* Now we have a list of terms that may contain definitions */
274
defslist = list_Nil();
275
for (scan=termlist; !list_Empty(scan); scan=list_Cdr(scan)) {
276
TERM cand;
277
TERM foundpred, toprove;
278
279
/* Candidate from list */
280
cand = (TERM) list_Car(scan);
281
term_AddFatherLinks(cand);
282
283
if (cnf_ContainsDefinition(cand, &foundpred)) {
284
DEF def;
285
#ifdef CHECK
286
if (!fol_CheckFormula(cand)) {
287
misc_StartErrorReport();
288
misc_ErrorReport("\n In def_ExtractDefsFromTerm: Illegal term cand");
289
misc_FinishErrorReport();
290
}
291
#endif
292
cand = cnf_DefConvert(cand, foundpred, &toprove);
293
#ifdef CHECK
294
if (!fol_CheckFormula(cand)) {
295
misc_StartErrorReport();
296
misc_ErrorReport("\n In def_ExtractDefsFromTerm: Illegal term cand");
297
misc_FinishErrorReport();
298
}
299
#endif
300
def = def_CreateFromTerm(term_Copy(term_SecondArgument(term_Superterm(foundpred))),
301
term_Copy(foundpred), toprove, Label);
302
303
if (def_PredicateOccurrences(cand, term_TopSymbol(foundpred)) > 1)
304
def_RemoveAttribute(def, PREDOCCURONCE);
305
else
306
def_AddAttribute(def, PREDOCCURONCE);
307
if (symbol_Equal(term_TopSymbol(foundpred), fol_Equality()))
308
def_AddAttribute(def, ISEQUALITY);
309
else
310
def_RemoveAttribute(def, ISEQUALITY);
311
312
defslist = list_Cons(def, defslist);
313
}
314
term_Delete(cand);
315
}
316
317
list_Delete(termlist);
318
return defslist;
319
}
320
321
void def_ExtractDefsFromClauselist(PROOFSEARCH Search, LIST Clauselist)
322
/**************************************************************
323
INPUT: A proofsearch object and a list of clauses
324
RETURNS: Nothing.
325
EFFECT: The definitions found in the clauselist object are stored in
326
the proofsearch object.
327
NOTE: The clause list is not changed.
328
The old list of definitions in the proofsearch object is
329
overwritten.
330
***************************************************************/
331
{
332
LIST scan, defslist;
333
FLAGSTORE FlagStore;
334
PRECEDENCE Precedence;
335
336
defslist = list_Nil();
337
FlagStore = prfs_Store(Search);
338
Precedence = prfs_Precedence(Search);
339
340
for (scan=Clauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
341
CLAUSE Clause;
342
NAT literal_index;
343
LIST pair;
344
345
Clause = (CLAUSE) list_Car(scan);
346
/* Check if clause contains a predicate that may be part of a definition */
347
if (clause_ContainsPotPredDef(Clause, FlagStore, Precedence, &literal_index, &pair)) {
348
LIST l, compl, compllits;
349
BOOL done;
350
351
compl = compllits = list_Nil();
352
done = FALSE;
353
354
/* Search for complement clauses */
355
for (l=Clauselist; !list_Empty(l) && !done; l=list_Cdr(l)) {
356
int predindex;
357
if (clause_IsPartOfDefinition((CLAUSE) list_Car(l),
358
clause_GetLiteralTerm(Clause, literal_index),
359
&predindex, pair)) {
360
compl = list_Cons(list_Car(l), compl);
361
compllits = list_Cons((POINTER) predindex, compllits);
362
363
if (list_Empty(list_PairFirst(pair)) &&
364
list_Empty(list_PairSecond(pair)))
365
done = TRUE;
366
}
367
}
368
369
/* All complements found ? */
370
if (done) {
371
LIST l2, clausenumbers, args;
372
DEF def;
373
NAT i;
374
TERM defterm, predterm;
375
BOOL con;
376
377
clausenumbers = list_Nil();
378
con = clause_GetFlag(Clause, CONCLAUSE);
379
380
for (l2=compl; !list_Empty(l2); l2=list_Cdr(l2)) {
381
clausenumbers = list_Cons((POINTER) clause_Number((CLAUSE) list_Car(l2)),
382
clausenumbers);
383
if (clause_GetFlag((CLAUSE) list_Car(l2), CONCLAUSE))
384
con = TRUE;
385
}
386
clausenumbers = list_Cons((POINTER) clause_Number(Clause),
387
clausenumbers);
388
compllits = list_Cons((POINTER) literal_index, compllits);
389
390
/* Build definition term */
391
predterm = term_Copy(clause_GetLiteralTerm(Clause, literal_index));
392
args = list_Nil();
393
for (i = 0; i < clause_Length(Clause); i++)
394
if (i != literal_index)
395
args = list_Cons(term_Copy(clause_GetLiteralTerm(Clause, i)), args);
396
defterm = term_CreateAddFather(fol_Or(), args);
397
/* The expansion is negative here, so it must be inverted */
398
defterm = term_Create(fol_Not(), list_List(defterm));
399
defterm = cnf_NegationNormalFormula(defterm);
400
def = def_CreateFromClauses(defterm, predterm, clausenumbers, compllits, con);
401
defslist = list_Cons(def, defslist);
402
if (flag_GetFlagIntValue(FlagStore, flag_PAPPLYDEFS)) {
403
fputs("\nNew definition found :", stdout);
404
def_Print(def);
405
}
406
}
407
else {
408
list_Delete(compllits);
409
list_Delete(list_PairSecond(pair));
410
list_Delete(list_PairFirst(pair));
411
}
412
list_Delete(compl);
413
list_PairFree(pair);
414
}
415
}
416
417
if (flag_GetFlagIntValue(FlagStore, flag_PAPPLYDEFS)) {
418
if (!list_Empty(defslist)) {
419
fputs("\nFound definitions :\n", stdout);
420
for (scan = defslist; !list_Empty(scan); scan = list_Cdr(scan)) {
421
def_Print((DEF) list_Car(scan));
422
fputs("\n---\n", stdout);
423
}
424
}
425
}
426
427
for (scan=defslist; !list_Empty(scan); scan=list_Cdr(scan))
428
symbol_AddProperty(term_TopSymbol(def_Predicate((DEF) list_Car(scan))), ISDEF);
429
430
prfs_SetDefinitions(Search, list_Nconc(prfs_Definitions(Search), defslist));
431
}
432
433
TERM def_ApplyDefToTermOnce(DEF Def, TERM Term, FLAGSTORE FlagStore,
434
PRECEDENCE Precedence, BOOL* Complete)
435
/**************************************************************
436
INPUT: A DEF structure, a term and a boolean that is set
437
to TRUE if no occurrences of the defined predicate
438
remain in the term. A flag store and a precedence.
439
RETURNS: A term where all occurrences of the definitions
440
predicate are expanded if possible.
441
NOTE: The Term is not changed.
442
***************************************************************/
443
{
444
TERM newtarget, oldtarget, targetpredicate, totoplevel, toprove;
445
LIST targettermvars, varsfortoplevel;
446
BOOL applicable;
447
448
oldtarget = Term;
449
*Complete = TRUE;
450
451
while (TRUE) {
452
newtarget = term_Copy(oldtarget);
453
term_AddFatherLinks(newtarget);
454
targettermvars = varsfortoplevel = list_Nil();
455
456
if (cnf_ContainsPredicate(newtarget, term_TopSymbol(def_Predicate(Def)),
457
&targetpredicate, &totoplevel, &targettermvars,
458
&varsfortoplevel)) {
459
*Complete = FALSE;
460
applicable = FALSE;
461
/* Check if definition is not always applicable */
462
if (term_Equal(def_ToProve(Def), term_Null())) {
463
applicable = TRUE;
464
newtarget = cnf_ApplyDefinitionOnce(def_Predicate(Def), term_Copy(def_Expansion(Def)),
465
newtarget, targetpredicate, FlagStore);
466
if (oldtarget != Term)
467
term_Delete(oldtarget);
468
oldtarget = newtarget;
469
list_Delete(targettermvars);
470
list_Delete(varsfortoplevel);
471
}
472
else {
473
toprove = term_Copy(def_ToProve(Def));
474
newtarget = cnf_DefTargetConvert(newtarget, totoplevel, toprove,
475
term_ArgumentList(def_Predicate(Def)),
476
term_ArgumentList(targetpredicate),
477
targettermvars, varsfortoplevel,
478
FlagStore, Precedence,
479
&applicable);
480
list_Delete(targettermvars);
481
list_Delete(varsfortoplevel);
482
if (applicable) {
483
newtarget = cnf_ApplyDefinitionOnce(def_Predicate(Def), term_Copy(def_Expansion(Def)),
484
newtarget, targetpredicate, FlagStore);
485
if (oldtarget != Term)
486
term_Delete(oldtarget);
487
oldtarget = newtarget;
488
}
489
else {
490
/* Predicate still exists but cannot be expanded */
491
term_Delete(newtarget);
492
if (oldtarget == Term)
493
return NULL;
494
else {
495
oldtarget = cnf_ObviousSimplifications(oldtarget);
496
return oldtarget;
497
}
498
}
499
}
500
}
501
else {
502
*Complete = TRUE;
503
/* Predicate does no longer exist */
504
term_Delete(newtarget);
505
/* No expansion possible */
506
if (oldtarget == Term)
507
return NULL;
508
else {
509
oldtarget = cnf_ObviousSimplifications(oldtarget);
510
return oldtarget;
511
}
512
}
513
}
514
return NULL; /* Unreachable */
515
}
516
517
TERM def_ApplyDefToTermExhaustive(PROOFSEARCH Search, TERM Term)
518
/**************************************************************
519
INPUT: A proofsearch object and a term.
520
RETURNS: An expanded term.
521
NOTE: All occurences of defined predicates are expanded in the term,
522
until no further changes are possible.
523
CAUTION: If cyclic definitions exist, this will crash.
524
***************************************************************/
525
{
526
TERM oldterm, newterm;
527
BOOL done, complete;
528
FLAGSTORE FlagStore;
529
PRECEDENCE Precedence;
530
531
done = FALSE;
532
oldterm = Term;
533
FlagStore = prfs_Store(Search);
534
Precedence = prfs_Precedence(Search);
535
536
while (!done) {
537
LIST l;
538
done = TRUE;
539
/* Apply all definitions to term until no more changes occur */
540
for (l=prfs_Definitions(Search); !list_Empty(l); l=list_Cdr(l)) {
541
newterm = def_ApplyDefToTermOnce((DEF) list_Car(l), oldterm,
542
FlagStore, Precedence, &complete);
543
if (newterm != NULL) {
544
if (oldterm != Term)
545
term_Delete(oldterm);
546
oldterm = newterm;
547
done = FALSE;
548
}
549
}
550
}
551
if (oldterm == Term)
552
return NULL;
553
else
554
return oldterm;
555
}
556
557
LIST def_ApplyDefToClauseOnce(DEF Def, CLAUSE Clause,
558
FLAGSTORE FlagStore, PRECEDENCE Precedence)
559
/**************************************************************
560
INPUT: A DEF structure, a clause, a flag store and a
561
precedence.
562
RETURNS: A list of new clauses.
563
NOTE: The clause is not changed.
564
All occurences of the defined predicate are expanded
565
in the clause and in the derived clauses.
566
***************************************************************/
567
{
568
LIST result, l;
569
570
result = list_List(Clause);
571
572
for (l = result; !list_Empty(l); l = list_Cdr(l)) {
573
if (clause_ContainsSymbol((CLAUSE) list_Car(l),
574
term_TopSymbol(def_Predicate(Def)))) {
575
result = list_Nconc(result,
576
cnf_ApplyDefinitionToClause((CLAUSE) list_Car(l),
577
def_Predicate(Def),
578
def_Expansion(Def),
579
FlagStore, Precedence));
580
/* Remove temporary clause */
581
if ((CLAUSE) list_Car(l) != Clause)
582
clause_Delete((CLAUSE) list_Car(l));
583
list_Rplaca(l, NULL);
584
}
585
}
586
result = list_PointerDeleteElement(result, NULL);
587
588
/* Make sure the original clause is no longer in the list */
589
if (!list_Empty(result))
590
if (list_First(result) == Clause)
591
result = list_Pop(result);
592
593
for (l = result; !list_Empty(l); l=list_Cdr(l)) {
594
CLAUSE c;
595
c = (CLAUSE) list_Car(l);
596
if (def_Conjecture(Def))
597
clause_SetFlag((CLAUSE) list_Car(l), CONCLAUSE);
598
clause_SetFromDefApplication(c);
599
clause_SetParentClauses(c, list_Cons((POINTER) clause_Number(Clause),
600
list_Copy(def_ClauseNumberList(Def))));
601
/* Parent literal is not available, as the predicate may occur several
602
times in the target clause */
603
clause_SetParentLiterals(c, list_Cons((POINTER) 0,
604
list_Copy(def_ClauseLitsList(Def))));
605
}
606
return result;
607
}
608
609
LIST def_ApplyDefToClauseExhaustive(PROOFSEARCH Search, CLAUSE Clause)
610
/**************************************************************
611
INPUT: A proofsearch object and a clause.
612
RETURNS: A list of derived clauses.
613
NOTE: All occurences of defined predicates are expanded in the clause.
614
until no further changes are possible.
615
CAUTION: If cyclic definitions exist, this will crash.
616
***************************************************************/
617
{
618
LIST newclauses, scan, result;
619
CLAUSE orig;
620
FLAGSTORE FlagStore;
621
PRECEDENCE Precedence;
622
623
orig = clause_Copy(Clause);
624
newclauses = list_List(orig);
625
result = list_Nil();
626
FlagStore = prfs_Store(Search);
627
Precedence = prfs_Precedence(Search);
628
629
while (!list_Empty(newclauses)) {
630
/* Check all clauses */
631
LIST l, nextlist;
632
633
/* List of clauses derived from newclauses by expanding predicates */
634
nextlist = list_Nil();
635
636
for (l=newclauses; !list_Empty(l); l=list_Cdr(l)) {
637
LIST clauses;
638
CLAUSE c;
639
640
c = (CLAUSE) list_Car(l);
641
642
/* Apply all definitions to the clause */
643
644
/* List of clauses derived from one clause in newclauses by */
645
/* expanding all possible predicates */
646
clauses = list_Nil();
647
648
for (scan=prfs_Definitions(Search); !list_Empty(scan); scan=list_Cdr(scan))
649
clauses = list_Nconc(clauses, def_ApplyDefToClauseOnce((DEF) list_Car(scan), c, FlagStore, Precedence));
650
651
/* If expansions were made delete old clause */
652
if (!list_Empty(clauses)) {
653
/* DOCPROOF ? */
654
if (c != Clause) {
655
if (flag_GetFlagIntValue(FlagStore, flag_DOCPROOF)) {
656
prfs_InsertDocProofClause(Search, c);
657
}
658
else
659
clause_Delete(c);
660
}
661
nextlist = list_Nconc(nextlist, clauses);
662
}
663
else {
664
/* No more expansions possible for this clause */
665
/* If it is not the original clause, add it to the result list */
666
if (c != Clause)
667
result = list_Cons(c, result);
668
}
669
}
670
list_Delete(newclauses);
671
newclauses = nextlist;
672
}
673
674
return result;
675
}
676
677
678
void def_Print(DEF D)
679
/**************************************************************
680
INPUT: A DEF structure.
681
RETURNS: None.
682
EFFECT: Prints the definition to stdout.
683
***************************************************************/
684
{
685
LIST scan, scan2;
686
fputs("\n\nAtom: ", stdout);
687
fol_PrettyPrint(def_Predicate(D));
688
fputs("\nExpansion: \n", stdout);
689
fol_PrettyPrint(def_Expansion(D));
690
if (!list_Empty(def_ClauseNumberList(D))) {
691
fputs("\nParent clauses: ", stdout);
692
for (scan = def_ClauseNumberList(D), scan2 = def_ClauseLitsList(D);
693
!list_Empty(scan); scan = list_Cdr(scan), scan2 = list_Cdr(scan2))
694
printf("%d.%d ", (NAT) list_Car(scan), (NAT) list_Car(scan2));
695
if (D->conjecture)
696
fputs("\nDerived from conjecture clauses.", stdout);
697
else
698
fputs("\nNot derived from conjecture clauses.", stdout);
699
}
700
else {
701
fputs("\nLabel: ", stdout);
702
fputs(def_Label(D), stdout);
703
puts("\nGuard:");
704
if (def_ToProve(D) != NULL)
705
fol_PrettyPrint(def_ToProve(D));
706
else
707
fputs("Nothing.", stdout);
708
}
709
710
fputs("\nAttributes: ", stdout);
711
if (def_HasAttribute(D, ISEQUALITY) || def_HasAttribute(D, PREDOCCURONCE)) {
712
if (def_HasAttribute(D, ISEQUALITY))
713
fputs(" Equality ", stdout);
714
if (def_HasAttribute(D, PREDOCCURONCE))
715
fputs(" No Multiple Occurrences ", stdout);
716
}
717
else {
718
fputs(" None ", stdout);
719
}
720
}
721
722
LIST def_ApplyDefToClauselist(PROOFSEARCH Search, DEF Def,
723
LIST Clauselist, BOOL Destructive)
724
/**************************************************************
725
INPUT: A proofsearch object, a DEF structure, a list of unshared clauses
726
and a boolean saying whether the parent clause of an expansion
727
should be deleted.
728
RETURNS: None.
729
EFFECT: For each occurrence of the defined predicate in a clause in the list,
730
a new clause with expanded predicate is added to the list.
731
***************************************************************/
732
{
733
LIST l, newclauses, allnew;
734
FLAGSTORE FlagStore;
735
PRECEDENCE Precedence;
736
737
allnew = list_Nil();
738
FlagStore = prfs_Store(Search);
739
Precedence = prfs_Precedence(Search);
740
741
for (l = Clauselist; !list_Empty(l); l = list_Cdr(l)) {
742
newclauses = def_ApplyDefToClauseOnce(Def, (CLAUSE) list_Car(l),
743
FlagStore, Precedence);
744
/* Expansions were possible, delete the original clause */
745
if (Destructive && !list_Empty(newclauses)) {
746
if (flag_GetFlagIntValue(FlagStore, flag_DOCPROOF))
747
prfs_InsertDocProofClause(Search, (CLAUSE) list_Car(l));
748
else
749
clause_Delete((CLAUSE) list_Car(l));
750
list_Rplaca(l, NULL);
751
}
752
allnew = list_Nconc(allnew, newclauses);
753
}
754
if (Destructive)
755
Clauselist = list_PointerDeleteElement(Clauselist, NULL);
756
757
758
if (flag_GetFlagIntValue(FlagStore, flag_PAPPLYDEFS)) {
759
if (!list_Empty(allnew)) {
760
fputs("\nNew clauses after applying definitions : \n", stdout);
761
clause_ListPrint(allnew);
762
}
763
}
764
765
Clauselist = list_Nconc(Clauselist, allnew);
766
return Clauselist;
767
}
768
769
LIST def_ApplyDefToTermlist(DEF Def, LIST Termlist,
770
FLAGSTORE FlagStore, PRECEDENCE Precedence,
771
BOOL* Complete, BOOL Destructive)
772
/**************************************************************
773
INPUT: A DEF structure and a list of pairs (label, term),
774
a flag store, a precedence and a pointer to a
775
boolean.
776
If Destructive is TRUE the father of an expanded
777
term is deleted.
778
RETURNS: The changed list of terms.
779
EFFECT: For each occurrence of the defined predicate in a
780
term in the list, a new term with expanded predicate
781
is added to the list.
782
If every occurrence of the predicate could be
783
expanded, Complete is set to TRUE.
784
***************************************************************/
785
{
786
LIST l, newterms;
787
788
newterms = list_Nil();
789
790
*Complete = TRUE;
791
for (l=Termlist; !list_Empty(l); l=list_Cdr(l)) {
792
TERM newterm;
793
TERM oldterm;
794
BOOL complete;
795
oldterm = list_PairSecond(list_Car(l));
796
newterm = def_ApplyDefToTermOnce(Def, oldterm, FlagStore,
797
Precedence, &complete);
798
if (!complete)
799
*Complete = FALSE;
800
/* destructive part of function */
801
if (newterm != NULL) {
802
newterms = list_Cons(list_PairCreate(NULL, newterm),newterms);
803
if (Destructive) {
804
/* Delete oldterm from Termlist */
805
term_Delete(list_PairSecond(list_Car(l)));
806
if (list_PairFirst(list_Car(l)) != NULL)
807
string_StringFree(list_PairFirst(list_Car(l)));
808
809
list_PairFree(list_Car(l));
810
list_Rplaca(l, NULL);
811
}
812
}
813
}
814
Termlist = list_PointerDeleteElement(Termlist, NULL);
815
816
if (flag_GetFlagIntValue(FlagStore, flag_PAPPLYDEFS)) {
817
if (!list_Empty(newterms)) {
818
fputs("\n\nNew terms after applying definitions : \n", stdout);
819
for (l=newterms; !list_Empty(l); l=list_Cdr(l)) {
820
fputs("\n", stdout);
821
fol_PrettyPrint(list_PairSecond(list_Car(l)));
822
}
823
}
824
}
825
826
Termlist = list_Nconc(Termlist, newterms);
827
return Termlist;
828
}
829
830
void def_ExtractDefsFromTermlist(PROOFSEARCH Search, LIST Axioms, LIST Conj)
831
/**************************************************************
832
INPUT: A proofsearch object and 2 lists of pairs label/term.
833
RETURNS: None.
834
EFFECT: Add all found definitions to the proofsearch object.
835
The old list of definitions in the proofsearch object is
836
overwritten.
837
***************************************************************/
838
{
839
LIST l, deflist;
840
FLAGSTORE FlagStore;
841
842
deflist = list_Nil();
843
FlagStore = prfs_Store(Search);
844
845
for (l=Axioms; !list_Empty(l); l=list_Cdr(l)) {
846
fol_NormalizeVars(list_PairSecond(list_Car(l))); /* Is needed for proper variable match ! */
847
deflist = list_Nconc(deflist,
848
def_ExtractDefsFromTerm(list_PairSecond(list_Car(l)),
849
list_PairFirst(list_Car(l))));
850
}
851
for (l=Conj; !list_Empty(l); l=list_Cdr(l)) {
852
fol_NormalizeVars(list_PairSecond(list_Car(l))); /* Is needed for proper variable match ! */
853
deflist = list_Nconc(deflist,
854
def_ExtractDefsFromTerm(list_PairSecond(list_Car(l)),
855
list_PairFirst(list_Car(l))));
856
}
857
for (l=deflist; !list_Empty(l); l=list_Cdr(l))
858
symbol_AddProperty(term_TopSymbol(def_Predicate(list_Car(l))), ISDEF);
859
860
prfs_SetDefinitions(Search, list_Nconc(prfs_Definitions(Search), deflist));
861
862
if (flag_GetFlagIntValue(FlagStore, flag_PAPPLYDEFS)) {
863
if (!list_Empty(deflist)) {
864
fputs("\nFound definitions :\n", stdout);
865
for (l = prfs_Definitions(Search); !list_Empty(l); l = list_Cdr(l)) {
866
def_Print(list_Car(l));
867
fputs("\n---\n", stdout);
868
}
869
}
870
}
871
}
872
873
LIST def_FlattenWithOneDefinition(PROOFSEARCH Search, DEF Def)
874
/**************************************************************
875
INPUT: A proofsearch object and one definition.
876
RETURNS: The list of new definitions.
877
EFFECT: For every occurrence of the defined predicate among the other
878
definitions an expansion is attempted.
879
A new definition is only created if the result of the expansion is
880
again a definition.
881
The proofsearch object is not changed.
882
***************************************************************/
883
{
884
LIST newdefinitions;
885
FLAGSTORE FlagStore;
886
PRECEDENCE Precedence;
887
888
newdefinitions = list_Nil();
889
FlagStore = prfs_Store(Search);
890
Precedence = prfs_Precedence(Search);
891
892
if (def_ToProve(Def) == NULL) {
893
LIST definitions, l;
894
895
definitions = prfs_Definitions(Search);
896
897
for (l = definitions; !list_Empty(l); l=list_Cdr(l)) {
898
DEF d;
899
900
d = (DEF) list_Car(l);
901
if (d != Def) {
902
/* Expansion possible */
903
if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) {
904
/* Resulting term is still a definition */
905
if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) {
906
TERM newexpansion;
907
BOOL complete;
908
DEF newdef;
909
newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d),
910
FlagStore, Precedence,
911
&complete);
912
913
newdef = def_CreateFromTerm(newexpansion,
914
term_Copy(def_Predicate(d)),
915
term_Copy(def_ToProve(d)), def_Label(d));
916
newdefinitions = list_Cons(newdef, newdefinitions);
917
}
918
}
919
}
920
921
}
922
}
923
return newdefinitions;
924
}
925
926
927
void def_FlattenWithOneDefinitionDestructive(PROOFSEARCH Search, DEF Def)
928
/**************************************************************
929
INPUT: A proofsearch object and one definition.
930
RETURNS: None.
931
EFFECT: If the definition is always applicable, every occurrence of the
932
defined predicate among the other definitions is expanded in place.
933
If the resulting term is no longer a definition, it is deleted from
934
the proofsearch object.
935
Def is deleted.
936
CAUTION: This function changes the list entries in the list of definitions
937
in the proofsearch object, so do not call it from a loop over
938
all definitions.
939
***************************************************************/
940
{
941
FLAGSTORE FlagStore;
942
PRECEDENCE Precedence;
943
944
FlagStore = prfs_Store(Search);
945
Precedence = prfs_Precedence(Search);
946
947
if (def_ToProve(Def) == NULL) {
948
LIST definitions, l;
949
950
definitions = prfs_Definitions(Search);
951
for (l = definitions; !list_Empty(l); l = list_Cdr(l)) {
952
DEF d;
953
954
d = (DEF) list_Car(l);
955
if (d != Def) {
956
/* Expansion possible */
957
if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) {
958
/* Resulting term is still a definition */
959
if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) {
960
TERM newexpansion;
961
BOOL complete;
962
963
newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d), FlagStore, Precedence, &complete);
964
term_Delete(def_Expansion(d));
965
def_RplacExp(d, newexpansion);
966
}
967
else {
968
symbol_RemoveProperty(term_TopSymbol(def_Predicate(d)), ISDEF);
969
def_Delete(d);
970
list_Rplaca(l, NULL);
971
}
972
}
973
}
974
else {
975
/* Remove given definition */
976
list_Rplaca(l, NULL);
977
}
978
}
979
symbol_RemoveProperty(term_TopSymbol(def_Predicate(Def)), ISDEF);
980
def_Delete(Def);
981
definitions = list_PointerDeleteElement(definitions, NULL);
982
prfs_SetDefinitions(Search, definitions);
983
}
984
}
985
986
void def_FlattenWithOneDefinitionSemiDestructive(PROOFSEARCH Search, DEF Def)
987
/**************************************************************
988
INPUT: A proofsearch object and one definition.
989
RETURNS: Nothing.
990
EFFECT: If the definition can be applied to another definition
991
in the search object, that definition is destructively changed.
992
If the resulting term is no longer a definition, it is deleted to
993
prevent cycles.
994
The applied definition Def is NOT deleted.
995
CAUTION: After calling this function some entries of the definitions list
996
in the proofsearch object may be NULL.
997
***************************************************************/
998
{
999
FLAGSTORE FlagStore;
1000
PRECEDENCE Precedence;
1001
1002
FlagStore = prfs_Store(Search);
1003
Precedence = prfs_Precedence(Search);
1004
1005
if (def_ToProve(Def) == NULL) {
1006
LIST definitions, l;
1007
1008
definitions = prfs_Definitions(Search);
1009
for (l = definitions; !list_Empty(l); l=list_Cdr(l)) {
1010
DEF d;
1011
1012
d = (DEF) list_Car(l);
1013
if (d != Def) {
1014
/* Expansion possible */
1015
if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) {
1016
/* Resulting term is still a definition */
1017
if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) {
1018
TERM newexpansion;
1019
BOOL complete;
1020
1021
newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d),
1022
FlagStore, Precedence,
1023
&complete);
1024
term_Delete(def_Expansion(d));
1025
def_RplacExp(d, newexpansion);
1026
}
1027
else {
1028
symbol_RemoveProperty(term_TopSymbol(def_Predicate(d)), ISDEF);
1029
def_Delete(d);
1030
list_Rplaca(l, NULL);
1031
}
1032
}
1033
}
1034
}
1035
}
1036
}
1037
1038
void def_FlattenDefinitionsDestructive(PROOFSEARCH Search)
1039
/**************************************************************
1040
INPUT: A proofsearch object.
1041
RETURNS: None.
1042
EFFECT: For every definition that is always applicable try to
1043
expand the predicate in other
1044
definitions if possible.
1045
***************************************************************/
1046
{
1047
LIST l;
1048
1049
for (l = prfs_Definitions(Search); !list_Empty(l); l=list_Cdr(l)) {
1050
DEF d;
1051
1052
d = (DEF) list_Car(l);
1053
fol_PrettyPrintDFG(def_Predicate(d));
1054
if (d != NULL)
1055
def_FlattenWithOneDefinitionSemiDestructive(Search, d);
1056
}
1057
prfs_SetDefinitions(Search, list_PointerDeleteElement(prfs_Definitions(Search), NULL));
1058
}
1059
1060
LIST def_GetTermsForProof(TERM Term, TERM SubTerm, int Polarity)
1061
/**************************************************************
1062
INPUT: Two formulas, <Term> and <SubTerm> which must be subformula
1063
of <Term>,an int which is the polarity of <SubTerm> in its
1064
superterm and a list of variables <Variables>.
1065
RETURN: A list of formulas that are used to prove the guard of Atom.
1066
COMMENT: Helpfunction of def_FindProofFor Guard.
1067
CAUTION: Father links must be set. Free variables may exist in terms of
1068
return list.
1069
Terms are copied.
1070
***************************************************************/
1071
{
1072
TERM SuperTerm, AddToList;
1073
SYMBOL Top;
1074
LIST Scan1, NewList;
1075
1076
term_AddFatherLinks(Term);
1077
1078
#ifdef CHECK
1079
if (!fol_CheckFormula(Term)) {
1080
misc_StartErrorReport();
1081
misc_ErrorReport("\n In def_GetTermsForProof: Illegal input Term.");
1082
misc_FinishErrorReport();
1083
}
1084
#endif
1085
1086
if (Term == SubTerm)
1087
return list_Nil();
1088
1089
SuperTerm = term_Superterm(SubTerm);
1090
Top = term_TopSymbol(SuperTerm);
1091
NewList = list_Nil();
1092
AddToList = term_Null();
1093
1094
if (symbol_Equal(Top, fol_Not()))
1095
return def_GetTermsForProof(Term, SuperTerm, -1*Polarity);
1096
1097
if (symbol_Equal(Top, fol_Or()) && Polarity == 1) {
1098
/* Get and store AddToList */
1099
for (Scan1 = term_ArgumentList(SuperTerm); !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) {
1100
if (!term_HasPointerSubterm(list_Car(Scan1), SubTerm))
1101
NewList = list_Cons(term_Create(fol_Not(),list_List(term_Copy(list_Car(Scan1)))), NewList);
1102
/* NewList's elements have the form not(term) */
1103
}
1104
if (list_Length(NewList) == 1) {
1105
AddToList = list_Car(NewList);
1106
list_Delete(NewList);
1107
}
1108
else {
1109
AddToList = term_Create(fol_And(), NewList);
1110
}
1111
return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
1112
}
1113
if (symbol_Equal(Top, fol_And()) && Polarity == -1) {
1114
/* Get and store AddToList */
1115
if (list_Length(term_ArgumentList(SuperTerm)) == 2) {
1116
if (!term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm)) {
1117
AddToList = term_Copy(term_FirstArgument(SuperTerm));
1118
}
1119
else {
1120
AddToList = term_Copy(term_SecondArgument(SuperTerm));
1121
}
1122
}
1123
else if (list_Length(term_ArgumentList(SuperTerm)) > 2) {
1124
for (Scan1 = term_ArgumentList(SuperTerm); !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) {
1125
if (!term_HasPointerSubterm(list_Car(Scan1), SubTerm))
1126
NewList = list_Cons(term_Copy(list_Car(Scan1)), NewList);
1127
}
1128
AddToList = term_Create(fol_And(), NewList);
1129
}
1130
else { /* Only one argument */
1131
AddToList = term_Copy(term_FirstArgument(SuperTerm));
1132
}
1133
return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
1134
}
1135
if (symbol_Equal(Top, fol_Implies())) {
1136
if (term_HasPointerSubterm(term_SecondArgument(SuperTerm), SubTerm) && Polarity == 1) {
1137
AddToList = term_Copy(term_FirstArgument(SuperTerm));
1138
return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
1139
}
1140
if (term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm) && Polarity == -1) {
1141
AddToList = term_Copy(term_SecondArgument(SuperTerm));
1142
AddToList = term_Create(fol_Not(), list_List(AddToList));
1143
return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, -1*Polarity));
1144
}
1145
}
1146
if (symbol_Equal(Top, fol_Implied())) { /* symmetric to fol_Implies */
1147
if (term_HasPointerSubterm(term_SecondArgument(SuperTerm), SubTerm) && Polarity == -1) {
1148
AddToList = term_Copy(term_FirstArgument(SuperTerm));
1149
AddToList = term_Create(fol_Not(), list_List(AddToList));
1150
return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, -1*Polarity));
1151
}
1152
if (term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm) && Polarity == 1) {
1153
AddToList = term_Copy(term_SecondArgument(SuperTerm));
1154
return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
1155
}
1156
}
1157
if (fol_IsQuantifier(Top))
1158
return def_GetTermsForProof(Term, SuperTerm, Polarity);
1159
1160
/* In all other cases, SubTerm is the top level term in which Atom occurs disjunctively */
1161
1162
return list_Nil();
1163
}
1164
1165
BOOL def_FindProofForGuard(TERM Term, TERM Atom, TERM Guard, FLAGSTORE FlagStore, PRECEDENCE Precedence)
1166
/**************************************************************************
1167
INPUT: A formula Term, an atom Atom, a term Guard a flag store and a
1168
precedence.
1169
RETURNS: True iff a proof can be found for Guard in Term.
1170
***************************************************************************/
1171
{
1172
BOOL LocallyTrue;
1173
TERM ToProve, Conjecture;
1174
LIST ArgList, FreeVars;
1175
1176
ArgList = list_Nil();
1177
FreeVars = list_Nil();
1178
ToProve = term_Null();
1179
Conjecture = term_Copy(Term);
1180
1181
#ifdef CHECK
1182
if (!fol_CheckFormula(Term)) {
1183
misc_StartErrorReport();
1184
misc_ErrorReport("\n In def_FindProofForGuard: No correct formula term.");
1185
misc_FinishErrorReport();
1186
}
1187
if (!term_HasPointerSubterm(Term, Atom)) {
1188
misc_StartErrorReport();
1189
misc_ErrorReport("\n In def_FindProofForGuard: Illegal input.");
1190
misc_FinishErrorReport();
1191
}
1192
#endif
1193
1194
ArgList = def_GetTermsForProof(Term, Atom, 1);
1195
1196
if (!list_Empty(ArgList)) {
1197
ToProve = term_Create(fol_And(), ArgList);
1198
FreeVars = list_Nconc(fol_FreeVariables(ToProve), fol_FreeVariables(Guard));
1199
FreeVars = term_DeleteDuplicatesFromList(FreeVars);
1200
term_CopyTermsInList(FreeVars);
1201
1202
ArgList = list_List(term_Copy(Guard));
1203
ArgList = list_Cons(ToProve, ArgList);
1204
ToProve = term_Create(fol_Implies(), ArgList);
1205
ToProve = fol_CreateQuantifier(fol_All(), FreeVars, list_List(ToProve));
1206
1207
/* Now ToProve has the form <forall[]: A implies Guard> */
1208
/* puts("\n*ToProve: "); fol_PrettyPrintDFG(ToProve); */
1209
1210
#ifdef CHECK
1211
if (!fol_CheckFormula(ToProve)) {
1212
misc_StartErrorReport();
1213
misc_ErrorReport("\n In def_FindProofForGuard: No correct formula ToProve.");
1214
misc_FinishErrorReport();
1215
}
1216
#endif
1217
1218
LocallyTrue = cnf_HaveProof(list_Nil(), ToProve, FlagStore, Precedence);
1219
term_Delete(ToProve);
1220
term_Delete(Conjecture);
1221
if (LocallyTrue)
1222
return TRUE;
1223
}
1224
else { /* empty list */
1225
term_DeleteTermList(ArgList);
1226
term_Delete(Conjecture);
1227
}
1228
1229
return FALSE;
1230
}
1231
1232
LIST def_ApplyDefinitionToTermList(LIST Defs, LIST Terms,
1233
FLAGSTORE Flags, PRECEDENCE Precedence)
1234
/**************************************************************************
1235
INPUT: A list of definitions <Defs> and a list of pairs (Label.Formula),
1236
the maximal number <Applics> of expansions, a flag store and a
1237
precedence.
1238
RETURNS: The possibly destructively changed list <Terms>.
1239
EFFECT: In all formulas of Terms any definition of Defs is applied exactly
1240
once if possible.
1241
The terms are changed destructively if the expanded def_predicate
1242
is not an equality.
1243
**************************************************************************/
1244
{
1245
TERM ActTerm; /* Actual term in Terms */
1246
TERM DefPredicate; /* Actual definition predicate out of Defs */
1247
TERM Expansion; /* Expansion term of the definition */
1248
TERM Target; /* Target predicate to be replaced */
1249
LIST TargetList, Scan1, Scan2, Scan3;
1250
BOOL Apply;
1251
int Applics;
1252
1253
Apply = TRUE;
1254
TargetList = list_Nil();
1255
Applics = flag_GetFlagIntValue(Flags, flag_APPLYDEFS);
1256
1257
while (Apply && Applics != 0) {
1258
Apply = FALSE;
1259
1260
for (Scan1=Defs; !list_Empty(Scan1) && Applics != 0; Scan1=list_Cdr(Scan1)) {
1261
DefPredicate = term_Copy(def_Predicate(list_Car(Scan1)));
1262
1263
/* puts("\n----\nDefPred:"); fol_PrettyPrintDFG(DefPredicate);*/
1264
1265
for (Scan2=Terms; !list_Empty(Scan2) && Applics != 0; Scan2=list_Cdr(Scan2)) {
1266
ActTerm = list_PairSecond(list_Car(Scan2));
1267
TargetList = term_FindAllAtoms(ActTerm, term_TopSymbol(DefPredicate));
1268
term_AddFatherLinks(ActTerm);
1269
1270
/* puts("\nActTerm:"); fol_PrettyPrintDFG(ActTerm);*/
1271
1272
for (Scan3=TargetList; !list_Empty(Scan3) && Applics != 0; Scan3=list_Cdr(Scan3)) {
1273
Target = list_Car(Scan3);
1274
cont_StartBinding();
1275
1276
/* puts("\nTarget:"); fol_PrettyPrintDFG(Target);*/
1277
1278
if (unify_Match(cont_LeftContext(), DefPredicate, Target)) {
1279
cont_BackTrack();
1280
Expansion = term_Copy(def_Expansion(list_Car(Scan1)));
1281
fol_NormalizeVarsStartingAt(ActTerm, term_MaxVar(Expansion));
1282
unify_Match(cont_LeftContext(), DefPredicate, Target);
1283
1284
if (fol_ApplyContextToTerm(cont_LeftContext(), Expansion)) { /* Matcher applied on Expansion */
1285
if (!def_HasGuard(list_Car(Scan1))) {
1286
Applics--;
1287
Apply = TRUE;
1288
/* puts("\n*no Guard!");*/
1289
term_RplacTop(Target, term_TopSymbol(Expansion));
1290
term_DeleteTermList(term_ArgumentList(Target));
1291
term_RplacArgumentList(Target, term_ArgumentList(Expansion));
1292
term_RplacArgumentList(Expansion, list_Nil());
1293
term_AddFatherLinks(ActTerm);
1294
#ifdef CHECK
1295
if (!fol_CheckFormula(ActTerm)) {
1296
misc_StartErrorReport();
1297
misc_ErrorReport("\n In def_ApplyDefinitionToTermList:");
1298
misc_ErrorReport(" No correct formula ActTerm.");
1299
misc_FinishErrorReport();
1300
}
1301
#endif
1302
if (flag_GetFlagIntValue(Flags, flag_PAPPLYDEFS)) {
1303
puts("\nApplied definition for");
1304
fol_PrettyPrintDFG(def_Predicate(list_Car(Scan1)));
1305
puts("\nNew formula:");
1306
fol_PrettyPrintDFG(ActTerm);
1307
}
1308
}
1309
else { /* check guard */
1310
TERM Guard;
1311
Guard = term_Copy(def_ToProve(list_Car(Scan1)));
1312
if (fol_ApplyContextToTerm(cont_LeftContext(), Guard)) {
1313
cont_BackTrack();
1314
if (def_FindProofForGuard(ActTerm, Target,Guard,
1315
Flags, Precedence)) {
1316
Applics--;
1317
Apply = TRUE;
1318
term_RplacTop(Target, term_TopSymbol(Expansion));
1319
term_DeleteTermList(term_ArgumentList(Target));
1320
term_RplacArgumentList(Target, term_ArgumentList(Expansion));
1321
term_RplacArgumentList(Expansion, list_Nil());
1322
term_AddFatherLinks(ActTerm);
1323
#ifdef CHECK
1324
if (!fol_CheckFormula(ActTerm)) {
1325
misc_StartErrorReport();
1326
misc_ErrorReport("\n In def_ApplyDefinitionToTermList:");
1327
misc_ErrorReport(" No correct formula ActTerm");
1328
misc_FinishErrorReport();
1329
}
1330
#endif
1331
if (flag_GetFlagIntValue(Flags, flag_PAPPLYDEFS)) {
1332
puts("\nApplied definition for");
1333
fol_PrettyPrintDFG(def_Predicate(list_Car(Scan1)));
1334
puts("\nNew formula:");
1335
fol_PrettyPrintDFG(ActTerm);
1336
}
1337
}
1338
}
1339
term_Delete(Guard);
1340
}
1341
}
1342
term_Delete(Expansion);
1343
}
1344
cont_BackTrack();
1345
}
1346
list_Delete(TargetList);
1347
}
1348
term_Delete(DefPredicate);
1349
}
1350
}
1351
return Terms;
1352
}
Loggerhead is a web-based interface for Breezy
Version: 2.0.1