« back to all changes in this revision
Viewing changes to SPASS/top.c
- browse files at revision 4
- compare with another revision
- 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/top.c
1
/**************************************************************/
2
/* ********************************************************** */
3
/* * * */
4
/* * TOP MODULE OF SPASS * */
5
/* * * */
6
/* * $Module: TOP * */
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
/* * * */
23
/* $Revision: 1.21 $ * */
24
/* $State: Exp $ * */
25
/* $Date: 2010-02-22 14:10:00 $ * */
26
/* $Author: weidenb $ * */
27
/* * * */
28
/* * Contact: * */
29
/* * Christoph Weidenbach * */
30
/* * MPI fuer Informatik * */
31
/* * Stuhlsatzenhausweg 85 * */
32
/* * 66123 Saarbruecken * */
33
/* * Email: spass@mpi-inf.mpg.de * */
34
/* * Germany * */
35
/* * * */
36
/* ********************************************************** */
37
/**************************************************************/
38
39
40
/* $RCSfile: top.c,v $ */
41
42
/*** MAIN LOOP *************************************************/
43
44
45
/**************************************************************/
46
/* Includes */
47
/**************************************************************/
48
49
#include "dfg.h"
50
#include "description.h"
51
#include "defs.h"
52
#include "ia.h"
53
#include "rules-inf.h"
54
#include "rules-sort.h"
55
#include "rules-split.h"
56
#include "terminator.h"
57
#include "rules-red.h"
58
#include "analyze.h"
59
#include "clock.h"
60
#include "strings.h"
61
#include "cmdline.h"
62
#include "context.h"
63
#include "cnf.h"
64
#include "search.h"
65
#include "hasharray.h"
66
#include "closure.h"
67
#include "eml.h"
68
#include "tptp.h"
69
#include <errno.h>
70
#include <stdlib.h>
71
72
73
/**************************************************************/
74
/* Types and Variables */
75
/**************************************************************/
76
77
static const char *top_InputFile;
78
static char *top_DiscoveredFile = (char*)NULL;
79
static int top_NoAlarm = 0; /* prevent race between handler and poll: 0 no result, 1 poll printed, -1 SIGNAL printed */
80
BOOL top_RemoveInputFile;
81
82
83
typedef enum {top_PROOF, top_COMPLETION, top_RESOURCE} top_SEARCHRESULT;
84
85
86
/**************************************************************/
87
/* Catch Signals Section */
88
/**************************************************************/
89
90
#ifdef SPASS_SIGNALS
91
#include <signal.h>
92
93
static PROOFSEARCH *top_PROOFSEARCH;
94
95
static void top_SigHandler(int Signal)
96
/**************************************************************
97
INPUT:
98
RETURNS:
99
EFFECT:
100
***************************************************************/
101
{
102
if (Signal == SIGSEGV || Signal == SIGBUS) {
103
puts("\n\n\tSPASS is going to crash. This is probably caused by a");
104
puts("\tbug in SPASS. Please send a copy of the input file(s) together");
105
puts("\twith the used options to spass@mpi-inf.mpg.de, and someone will");
106
puts("\ttry to fix the problem.\n");
107
abort();
108
}
109
110
if (Signal == SIGINT || Signal == SIGTERM || (Signal == SIGALRM && top_NoAlarm == 0)) {
111
top_NoAlarm = -1;
112
clock_StopPassedTime(clock_OVERALL);
113
printf("\nSPASS %s ", vrs_VERSION);
114
puts("\nSPASS beiseite: Ran out of time. SPASS was killed.");
115
printf("Problem: %s ",
116
(top_DiscoveredFile != (char*)NULL ? top_DiscoveredFile : "Read from stdin."));
117
printf("\nSPASS derived %d clauses, backtracked %d clauses, performed %d splits, "
118
"and kept %d clauses.",
119
(*top_PROOFSEARCH == (PROOFSEARCH)NULL ? 0 : prfs_DerivedClauses(*top_PROOFSEARCH)),
120
(*top_PROOFSEARCH == (PROOFSEARCH)NULL ? 0 : prfs_BacktrackedClauses(*top_PROOFSEARCH)),
121
(*top_PROOFSEARCH == (PROOFSEARCH)NULL ? 0 : prfs_SplitCounter(*top_PROOFSEARCH)),
122
(*top_PROOFSEARCH == (PROOFSEARCH)NULL ? 0 : prfs_KeptClauses(*top_PROOFSEARCH)));
123
printf("\nSPASS allocated %lu KBytes.", memory_DemandedBytes()/1024);
124
fputs("\nSPASS spent\t", stdout);
125
clock_PrintTime(clock_OVERALL);
126
fputs(" on the problem.\n\t\t", stdout);
127
clock_PrintTime(clock_INPUT);
128
fputs(" for the input.\n\t\t", stdout);
129
clock_PrintTime(clock_CNF);
130
fputs(" for the FLOTTER CNF translation.\n\t\t", stdout);
131
clock_PrintTime(clock_INFERENCE);
132
fputs(" for inferences.\n\t\t", stdout);
133
clock_PrintTime(clock_BACKTRACK);
134
fputs(" for the backtracking.\n\t\t", stdout);
135
clock_PrintTime(clock_REDUCTION);
136
puts(" for the reduction.");
137
}
138
139
if (top_RemoveInputFile) /* Only files in current directory might get removed, not with respect to environment variables */
140
remove(top_InputFile);
141
142
exit(EXIT_FAILURE);
143
}
144
145
#endif
146
147
148
/**************************************************************/
149
/* Clause Selection Functions */
150
/**************************************************************/
151
152
static CLAUSE top_SelectClauseDepth(LIST List, FLAGSTORE Flags)
153
/**************************************************************
154
INPUT: A list of clauses and a flag store.
155
RETURNS: A clause selected from the list.
156
EFFECT: This function selects a clause from the list according
157
to the following criteria:
158
1. minimal depth
159
2. minimal weight
160
3a. maximal number of variable occurrences, if the flag
161
'PrefVar' is TRUE
162
3b. minimal number of variable occurrences, if 'PrefVar'
163
is FALSE
164
***************************************************************/
165
{
166
CLAUSE Result;
167
NAT Vars,NewVars,Weight,Depth,NewDepth;
168
169
Result = (CLAUSE)list_Car(List);
170
Depth = clause_Depth(Result);
171
Weight = clause_Weight(Result);
172
Vars = clause_NumberOfVarOccs(Result);
173
List = list_Cdr(List);
174
175
while (!list_Empty(List)) {
176
NewDepth = clause_Depth(list_Car(List));
177
if (NewDepth <= Depth) {
178
if (NewDepth < Depth || clause_Weight(list_Car(List)) < Weight) {
179
Depth = NewDepth;
180
Result = (CLAUSE)list_Car(List);
181
Weight = clause_Weight(Result);
182
Vars = clause_NumberOfVarOccs(list_Car(List));
183
}
184
else
185
if (clause_Weight(list_Car(List)) == Weight) {
186
NewVars = clause_NumberOfVarOccs(list_Car(List));
187
if (flag_GetFlagIntValue(Flags, flag_PREFVAR)) {
188
if (Vars < NewVars) {
189
Depth = NewDepth;
190
Result = (CLAUSE)list_Car(List);
191
Weight = clause_Weight(Result);
192
Vars = NewVars;
193
}
194
}
195
else
196
if (Vars > NewVars) {
197
Depth = NewDepth;
198
Result = (CLAUSE)list_Car(List);
199
Weight = clause_Weight(Result);
200
Vars = NewVars;
201
}
202
}
203
}
204
List = list_Cdr(List);
205
}
206
207
return Result;
208
}
209
210
211
static CLAUSE top_SelectMinimalWeightClause(LIST List, FLAGSTORE Flags)
212
/**************************************************************
213
INPUT: A list of clauses and a flag store.
214
RETURNS: A clause selected from the list.
215
EFFECT: This function selects a clause with minimal weight.
216
If more than one clause has minimal weight and the flag
217
'PrefVar' is TRUE, a clause with maximal number of variable
218
occurrences is selected. If 'PrefVar' is FALSE, a clause with
219
minimal number of variable occurrences is selected.
220
If two clauses are equal with respect to the two criteria
221
the clause with the smaller list position is selected.
222
CAUTION: THE LIST HAS TO BY SORTED BY WEIGHT IN ASCENDING ORDER!
223
***************************************************************/
224
{
225
CLAUSE Result;
226
NAT Vars, NewVars, Weight;
227
228
#ifdef CHECK
229
/* Check invariant: List has to be sorted by weight (ascending) */
230
LIST Scan;
231
Weight = clause_Weight(list_Car(List));
232
for (Scan = list_Cdr(List); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
233
NAT NewWeight;
234
NewWeight = clause_Weight(list_Car(Scan));
235
if (NewWeight < Weight) {
236
misc_StartErrorReport();
237
misc_ErrorReport("\n In top_SelectMinimalConWeightClause: clause list ");
238
misc_ErrorReport("isn't sorted by weight");
239
misc_FinishErrorReport();
240
}
241
Weight = NewWeight;
242
}
243
#endif
244
245
Result = (CLAUSE)list_Car(List);
246
Weight = clause_Weight(Result);
247
Vars = clause_NumberOfVarOccs(Result);
248
List = list_Cdr(List);
249
250
while (!list_Empty(List)) {
251
if (clause_Weight(list_Car(List)) == Weight) {
252
NewVars = clause_NumberOfVarOccs(list_Car(List));
253
if (flag_GetFlagIntValue(Flags, flag_PREFVAR)) {
254
if (Vars < NewVars) {
255
Result = (CLAUSE)list_Car(List);
256
Weight = clause_Weight(Result);
257
Vars = NewVars;
258
}
259
}
260
else
261
if (Vars > NewVars) {
262
Result = (CLAUSE)list_Car(List);
263
Weight = clause_Weight(Result);
264
Vars = NewVars;
265
}
266
}
267
else
268
return Result;
269
List = list_Cdr(List);
270
}
271
return Result;
272
}
273
274
275
static CLAUSE top_SelectMinimalConWeightClause(LIST List, FLAGSTORE Flags)
276
/**************************************************************
277
INPUT: A non-empty list of clauses and a flag store.
278
RETURNS: A clause selected from the list.
279
EFFECT: This function selects a clause from the list in a
280
similar way as the function top_SelectMinimalWeightClause.
281
The only difference is that conjecture clauses are
282
preferred over axiom clauses, because their weight
283
is divided by a factor given by the flag 'PrefCon'.
284
***************************************************************/
285
{
286
CLAUSE Result;
287
NAT NewWeight,Weight, NewVars, Vars, Factor;
288
289
Result = (CLAUSE)list_Car(List);
290
Factor = flag_GetFlagIntValue(Flags, flag_PREFCON);
291
Weight = clause_Weight(Result);
292
if (clause_GetFlag(Result, CONCLAUSE))
293
Weight = Weight / Factor;
294
Vars = clause_NumberOfVarOccs(list_Car(List));
295
List = list_Cdr(List);
296
297
while (!list_Empty(List)) {
298
NewWeight = clause_Weight(list_Car(List));
299
if (clause_GetFlag(list_Car(List),CONCLAUSE))
300
NewWeight = NewWeight / Factor;
301
if (NewWeight < Weight) {
302
Weight = NewWeight;
303
Result = list_Car(List);
304
Vars = clause_NumberOfVarOccs(list_Car(List));
305
}
306
else {
307
if (NewWeight == Weight) {
308
NewVars = clause_NumberOfVarOccs(list_Car(List));
309
if (flag_GetFlagIntValue(Flags, flag_PREFVAR)) {
310
if (Vars < NewVars) {
311
Result = (CLAUSE)list_Car(List);
312
Weight = NewWeight;
313
Vars = NewVars;
314
}
315
}
316
else
317
if (Vars > NewVars) {
318
Result = (CLAUSE)list_Car(List);
319
Weight = NewWeight;
320
Vars = NewVars;
321
}
322
}
323
}
324
325
List = list_Cdr(List);
326
}
327
return Result;
328
}
329
330
331
/*static CLAUSE top_SelectClauseDepth(LIST List)*/
332
/**************************************************************
333
INPUT: A list of clauses.
334
RETURNS: A clause selected from the list.
335
EFFECT:
336
***************************************************************/
337
/*{
338
CLAUSE Result;
339
int Min, Depth;
340
341
Result = (CLAUSE)list_Car(List);
342
Depth = clause_Depth(Result);
343
Min = Depth * clause_Weight(Result);
344
List = list_Cdr(List);
345
346
if (Depth == 0)
347
return Result;
348
349
while (!list_Empty(List)) {
350
Depth = clause_Depth(list_Car(List));
351
if (Min > Depth * clause_Weight(list_Car(List))) {
352
Result = list_Car(List);
353
if (Depth == 0)
354
return Result;
355
Min = clause_Depth(Result) * clause_Weight(Result);
356
}
357
List = list_Cdr(List);
358
}
359
360
return Result;
361
}*/
362
363
364
static LIST top_GetLiteralsForSplitting(CLAUSE Clause, BOOL SuccedentOnly)
365
/**************************************************************
366
INPUT: A clause and a flag whether only succedent literals should be
367
considered
368
RETURNS: A list of literal sets where every single
369
set doesn't share any variables with other literal sets..
370
If SuccedentOnly is TRUE, only succedent lits are considered.
371
The literal sets contain the full splits.
372
Returns list_Nil() if the clause has only one component.
373
***************************************************************/
374
{
375
LIST* Variables; /* An array, mapping literal index to list of variables */
376
LIST* Cluster; /* potential variable sharing clusters of considered literals */
377
int i, j, EndIndex;
378
LIST Result,Scan1, Scan2;
379
BOOL NeedTest;
380
381
Result = list_Nil();
382
EndIndex = (SuccedentOnly ? clause_FirstSuccedentLitIndex(Clause) : clause_FirstLitIndex());
383
384
/* Special case: clause is ground, so return all literals */
385
if (clause_IsGround(Clause)) {
386
for (i = clause_LastLitIndex(Clause); i >= EndIndex; i--)
387
Result = list_Cons(list_List(clause_GetLiteral(Clause,i)), Result);
388
return Result;
389
}
390
391
392
Variables = memory_Malloc(sizeof(LIST) * clause_Length(Clause));
393
Cluster = memory_Malloc(sizeof(LIST) * clause_Length(Clause)); /* not necessarily all needed */
394
/* Initialize the arrays */
395
for (i = clause_FirstLitIndex(); i <= clause_LastLitIndex(Clause); i++) {
396
Variables[i] = term_VariableSymbols(clause_GetLiteralAtom(Clause, i));
397
Cluster[i] = list_List((POINTER)i);
398
}
399
400
for (i = EndIndex; i <= clause_LastLitIndex(Clause); i++) {
401
if (!list_Empty(Cluster[i])) { /* not already clustered */
402
NeedTest = TRUE;
403
while (NeedTest) {
404
NeedTest = FALSE;
405
/* We don't know yet whether the literal shares variables */
406
for (j = clause_FirstLitIndex(); j <= clause_LastLitIndex(Clause); j++) {
407
if (i != j && list_HasIntersection(Variables[i], Variables[j])) {
408
Variables[i] = list_Nconc(Variables[j],Variables[i]);
409
Variables[j] = list_Nil();
410
Cluster[i] = list_Nconc(Cluster[i], Cluster[j]);
411
Cluster[j] = list_Nil();
412
NeedTest = TRUE;
413
}
414
}
415
}
416
}
417
}
418
419
420
/* Compute Results */
421
for (i = clause_FirstLitIndex(); i <= clause_LastLitIndex(Clause); i++) {
422
list_Delete(Variables[i]);
423
if (i < EndIndex)
424
list_Delete(Cluster[i]);
425
else
426
if (!list_Empty(Cluster[i]))
427
Result = list_Cons(Cluster[i], Result);
428
}
429
430
memory_Free(Variables, sizeof(LIST) * clause_Length(Clause));
431
memory_Free(Cluster, sizeof(LIST) * clause_Length(Clause));
432
433
if (list_Length(Result) == 1) {
434
list_Delete(list_Car(Result));
435
list_Delete(Result);
436
Result = list_Nil();
437
}
438
439
440
for (Scan1=Result;!list_Empty(Scan1);Scan1=list_Cdr(Scan1))
441
for (Scan2=list_Car(Scan1);!list_Empty(Scan2);Scan2=list_Cdr(Scan2))
442
list_Rplaca(Scan2,clause_GetLiteral(Clause,(int)list_Car(Scan2)));
443
444
445
/* printf("\nSplits: "); clause_Print(Clause); printf("\n"); */
446
/* for(Scan2=Result;!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) { */
447
/* printf("[ "); */
448
/* for(Scan1=list_Car(Scan2);!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) { */
449
/* clause_LiteralPrint(list_Car(Scan1)); printf(" "); */
450
/* } */
451
/* printf("] "); */
452
/* } */
453
454
return Result;
455
}
456
457
#ifdef CHECK
458
static BOOL top_ClauseIsSplittable(CLAUSE Clause, BOOL SuccedentOnly)
459
{
460
LIST Lits;
461
BOOL Result;
462
463
Lits = top_GetLiteralsForSplitting(Clause, SuccedentOnly);
464
Result = (Lits != list_Nil());
465
while (!list_Empty(Lits)) {
466
list_Delete(list_Car(Lits));
467
Lits = list_Pop(Lits);
468
}
469
return Result;
470
}
471
#endif
472
473
static float top_ComputeSplitPotential(PROOFSEARCH Search, CLAUSE Clause)
474
/**************************************************************
475
INPUT: A proofsearch object <Search> and a clause.
476
RETURNS: If the clause is a split clause, the average number of instances
477
of all split literals from <Clause>
478
****************************************************************/
479
{
480
LIST SplitLitSets,Literals;
481
float NrOfInstances;
482
LITERAL Literal;
483
TERM Atom;
484
int i;
485
486
SplitLitSets = list_Nil();
487
NrOfInstances = 0.0;
488
i = 0;
489
490
if (clause_HasSolvedConstraint(Clause) &&
491
clause_Length(Clause) > 1 &&
492
(!clause_IsHornClause(Clause) ||
493
(!ana_PUREPROPOSITIONAL &&
494
clause_GetFlag(Clause, CONCLAUSE) && /* Split non-Horn clauses or input conjecture clauses */
495
clause_Depth(Clause) == 0))) {
496
/* Get a list of splittable literal indices */
497
SplitLitSets = top_GetLiteralsForSplitting(Clause, !clause_IsHornClause(Clause));
498
}
499
if (!list_Empty(SplitLitSets)) {
500
for ( ; !list_Empty(SplitLitSets); SplitLitSets = list_Pop(SplitLitSets)) {
501
Literals = list_Car(SplitLitSets);
502
while (!list_Empty(Literals)) {
503
i++;
504
Literal = list_Car(Literals);
505
Atom = clause_LiteralAtom(Literal);
506
NrOfInstances += prfs_GetNumberOfInstances(Search, Literal, TRUE);
507
Literals = list_Cdr(Literals);
508
}
509
list_Delete(list_Car(SplitLitSets));
510
}
511
NrOfInstances = NrOfInstances / i; /* Average Hits */
512
}
513
return NrOfInstances;
514
}
515
516
517
static LIST top_GetBestSplitLiterals(PROOFSEARCH Search, CLAUSE Clause, BOOL Usables)
518
/**************************************************************
519
INPUT: A proofsearch object <Search>, a <Clause>
520
and a bool <Usables> telling whether the Usable set schould also be
521
considered for computing the best split
522
RETURNS: The literal list out of the SplitLitSets
523
from <Clause>, such that the positive
524
split literals together with this literal have the maximal number of instances
525
in clauses from <Search> where <Usables> determins whether the
526
usable clauses are considered too as instance candidates
527
****************************************************************/
528
{
529
LITERAL Literal;
530
LIST Literals, SplitLitSets, ActLiterals;
531
int j;
532
float SetAverage, MaxSetAverage;
533
TERM Atom;
534
535
MaxSetAverage = 0.0;
536
ActLiterals = list_Nil();
537
538
SplitLitSets = top_GetLiteralsForSplitting(Clause, !clause_IsHornClause(Clause));
539
540
if (!list_Empty(SplitLitSets)) {
541
for ( ; !list_Empty(SplitLitSets); SplitLitSets = list_Pop(SplitLitSets)) {
542
Literals = list_Car(SplitLitSets);
543
SetAverage = 0.0;
544
j = 0;
545
while (!list_Empty(Literals)) {
546
j++;
547
Literal = list_Car(Literals);
548
Atom = clause_LiteralAtom(Literal);
549
SetAverage += prfs_GetNumberOfInstances(Search, Literal, Usables);
550
Literals = list_Cdr(Literals);
551
}
552
SetAverage = SetAverage / j;
553
if (ActLiterals == list_Nil() || SetAverage > MaxSetAverage) {
554
MaxSetAverage = SetAverage;
555
list_Delete(ActLiterals);
556
ActLiterals = list_Car(SplitLitSets);
557
}
558
else
559
list_Delete(list_Car(SplitLitSets));
560
}
561
}
562
563
return ActLiterals;
564
}
565
566
567
568
static LIST top_GetSplitLiterals(PROOFSEARCH Search, CLAUSE Clause, BOOL Usables)
569
/**************************************************************
570
INPUT: A proofsearch object, a clause and a boolean flag.
571
RETURNS: The index of the positive literal from <Clause>
572
with the greatest number of instances (maybe 0) within
573
the WorkedOff/Usable sets of the proof search object.
574
The literal mustn't share any variables with other literals.
575
If the clause doesn't have a suitable literal, a negative
576
number is returned.
577
EFFECT: If <Usables> is FALSE, only the number of instances
578
within the WorkedOff set is considered, otherwise
579
the number of instances within both clause sets is considered.
580
***************************************************************/
581
{
582
float MaxInstances;
583
LIST Result;
584
585
MaxInstances = 0.0;
586
Result = list_Nil();
587
588
MaxInstances = top_ComputeSplitPotential(Search, Clause);
589
590
if (MaxInstances > 0.0 &&
591
(ana_PUREPROPOSITIONAL || MaxInstances >= flag_GetFlagIntValue(prfs_Store(Search), flag_SPLITMININST)))
592
Result = top_GetBestSplitLiterals(Search, Clause, Usables);
593
594
return Result;
595
}
596
597
598
599
static CLAUSE top_GetPowerfulSplitClause(PROOFSEARCH Search, BOOL Usables, LIST* Literals, int MinInstances)
600
/**************************************************************
601
INPUT: A proofsearch object, a boolean flag, a pointer to a literal
602
list which is used as return value and a minimum number
603
of instances a potential split cause must match
604
RETURNS: A clause from the usable set that was selected as given clause.
605
Iff no suitable clause was found NULL is returned and <*LitIndex>
606
is set to -1.
607
Iff a suitable clause was found, this clause is returned and
608
<*LitIndex> is set to the index of the "optimal" literal, that
609
is a literal that can be split off as unit witha high reduction
610
potential
611
EFFECT: This function selects a clause from the "usable" set and
612
a literal that are "optimal" for the application of the splitting
613
rule with respect to the following criteria:
614
1) the literal must occur in the succedent of the non-horn clause,
615
2) the literal mustn't share any variables with other literals,
616
3) the clause must have a solved constraint,
617
4) the atom must have the maximum number of instances
618
a) within the set of "workedoff" clauses, iff <Usables>=FALSE
619
b) within the set of "usable" and "workedoff" clauses,
620
iff "Usables"=TRUE
621
5) the atom must have at least one instance in another clause.
622
6) if the split heuristic is flag_SPLITHEURISTICALWAYS the function
623
always selects a non-Horn clause to be split if available
624
7) if the split heutistic is flag_SPLITHEURISTICGROUND then
625
ground input conjecture clauses are split as well (even if
626
the clause is Horn)
627
***************************************************************/
628
{
629
LIST Scan;
630
CLAUSE Clause, OptimalClause;
631
632
633
OptimalClause = NULL;
634
635
for (Scan = prfs_UsableClauses(Search); !list_Empty(Scan);
636
Scan = list_Cdr(Scan)) {
637
Clause = list_Car(Scan);
638
if (clause_SplitPotential(Clause) > 0.0)
639
if (OptimalClause == NULL || clause_SplitPotential(OptimalClause) < clause_SplitPotential(Clause))
640
OptimalClause = Clause;
641
}
642
643
if (OptimalClause != (CLAUSE)NULL) {
644
if (clause_SplitPotential(OptimalClause) > MinInstances)
645
*Literals = top_GetBestSplitLiterals(Search, OptimalClause, Usables);
646
else
647
OptimalClause = (CLAUSE)NULL;
648
}
649
650
return OptimalClause;
651
}
652
653
654
static LIST top_FullReductionSelectGivenComputeDerivables(PROOFSEARCH Search,
655
CLAUSE *SplitClause,
656
int *Counter, int *MinInstances)
657
/**************************************************************
658
INPUT: A proof search object, a pointer to a clause resulting from a
659
previous splitting step, and a pointer to an integer counter and
660
a pointer the minimum number of instances for a successful split application
661
RETURNS: A list of derived clauses.
662
EFFECT: In this function a clause is selected from the set of
663
"usable" clauses. After a clause was selected as "given clause",
664
inferences between the given clause and the "worked off" clauses
665
are made. The selection works as follows:
666
1) If <*SplitClause> is not NULL, the split clause
667
is selected as "given clause". <*SplitClause> should result
668
from splitting
669
2) If <*SplitClause> is NULL, we try to find a clause that is
670
"optimal" for splitting. This is done by selecting a literal
671
<L> in a clause, such that <L> is variable-disjoint from
672
the rest of the clause, and the atom of <L> has the maximum
673
number of instances within the set of "usable" and "workoff"
674
clauses.
675
3) If the previous steps failed, a clause is selected by weight
676
or by depth, depending on the parameters "WDRatio", "PrefVar"
677
and "PrefCon". Then splitting is tried on the selected clause.
678
If the clause is a non-horn clause, we try to find a positive
679
literal <L> and a set of negative literals <N>, such that <N>
680
and <L> are variable disjoint from the rest of the clause.
681
***************************************************************/
682
{
683
CLAUSE GivenClause, TerminatorClause;
684
LIST Derivables, SplitLits;
685
FLAGSTORE Flags;
686
PRECEDENCE Precedence;
687
688
GivenClause = NULL;
689
Derivables = list_Nil();
690
Flags = prfs_Store(Search);
691
Precedence = prfs_Precedence(Search);
692
SplitLits = list_Nil();
693
694
/* 1) If the last given clause was split or if backtracking was applied, */
695
/* then choose the clause resulting from the splitting step as */
696
/* given clause. */
697
/* ATTENTION: Since the <SplitClause> might have been reduced since */
698
/* the time the variable was set, we have to check whether */
699
/* <SplitClause> is still element of the set of usable clauses. */
700
if (*SplitClause != NULL &&
701
list_PointerMember(prfs_UsableClauses(Search), *SplitClause))
702
GivenClause = *SplitClause;
703
704
*SplitClause = NULL;
705
706
if (GivenClause == NULL) {
707
if (prfs_SplitsAvailable(Search, Flags)) {
708
/* 2) Try to find an "optimal" splitting clause, that doesn't share */
709
/* variables with any other literal. */
710
GivenClause = top_GetPowerfulSplitClause(Search, TRUE, &SplitLits, *MinInstances);
711
#ifdef CHECK
712
if (GivenClause != (CLAUSE)NULL && !top_ClauseIsSplittable(GivenClause, FALSE)) {
713
misc_StartErrorReport();
714
misc_ErrorReport("\n In top_FullReductionSelectGivenComputeDerivables: powerful split clause ");
715
misc_ErrorReport("is not splittable.");
716
misc_FinishErrorReport();
717
}
718
#endif
719
}
720
if (GivenClause != NULL) {
721
/* Found "optimal" split clause, so apply splitting */
722
(*MinInstances)++;
723
*SplitClause = prfs_DoSplitting(Search, GivenClause, SplitLits);
724
list_Delete(SplitLits);
725
} else {
726
/* 3) Splitting wasn't applied, so use the other strategies */
727
*MinInstances = flag_GetFlagIntValue(Flags, flag_SPLITMININST);
728
if ((*Counter) % flag_GetFlagIntValue(Flags, flag_WDRATIO) == 0)
729
GivenClause = top_SelectClauseDepth(prfs_UsableClauses(Search), Flags);
730
else {
731
if (flag_GetFlagIntValue(Flags, flag_PREFCON) != flag_PREFCONUNCHANGED)
732
GivenClause = top_SelectMinimalConWeightClause(prfs_UsableClauses(Search),
733
Flags);
734
else
735
GivenClause = top_SelectMinimalWeightClause(prfs_UsableClauses(Search),
736
Flags);
737
}
738
(*Counter)++; /* EK: hier lassen, oder eine Klammerebene nach aussen? */
739
}
740
}
741
742
if (*SplitClause == NULL && prfs_SplitsAvailable(Search,Flags)) {
743
/* Try to find the "optimal" literal for splitting the clause. */
744
/* This makes sense for a clause that is the right part of a */
745
/* splitting step. */
746
SplitLits = top_GetSplitLiterals(Search, GivenClause, FALSE);
747
if (!list_Empty(SplitLits)) {
748
#ifdef CHECK
749
if (!top_ClauseIsSplittable(GivenClause, FALSE)) {
750
misc_StartErrorReport();
751
misc_ErrorReport("\n In top_FullReductionSelectGivenComputeDerivables: powerful split clause ");
752
misc_ErrorReport("is not splittable.");
753
misc_FinishErrorReport();
754
}
755
#endif
756
*SplitClause = prfs_DoSplitting(Search, GivenClause, SplitLits);
757
list_Delete(SplitLits);
758
} else {
759
/* Optimal splitting wasn't possible, so try the old-style splitting. */
760
/* Here a split is done if a positive literal doesn't share variables */
761
/* with another POSITIVE literal. */
762
*SplitClause = (CLAUSE)NULL; /* only split optimal clauses prfs_PerformSplitting(Search, GivenClause);*/
763
}
764
}
765
766
prfs_ExtractUsable(Search, GivenClause);
767
clause_SelectLiteral(GivenClause, Flags);
768
769
if (flag_GetFlagIntValue(Flags, flag_PGIVEN)) {
770
fputs("\n\tGiven clause: ", stdout);
771
clause_Print(GivenClause);
772
fflush(stdout);
773
}
774
775
if (*SplitClause != NULL) {
776
/*printf("\n Split: "); clause_Print(*SplitClause); printf(" from\n");
777
clause_Print(GivenClause);printf("\n");*/
778
Derivables = list_List(*SplitClause);
779
}
780
else {
781
/* No splitting was applied */
782
if (flag_GetFlagIntValue(Flags, flag_RTER) != flag_RTEROFF) {
783
clock_StartCounter(clock_REDUCTION);
784
TerminatorClause = red_Terminator(GivenClause,
785
flag_GetFlagIntValue(Flags, flag_RTER),
786
prfs_WorkedOffSharingIndex(Search),
787
prfs_UsableSharingIndex(Search), Flags,
788
Precedence);
789
clock_StopAddPassedTime(clock_REDUCTION);
790
791
if (TerminatorClause != NULL) {
792
/* An empty clause was derived by the "terminator" rule */
793
Derivables = list_List(TerminatorClause);
794
prfs_InsertUsableClause(Search, GivenClause);
795
}
796
}
797
if (list_Empty(Derivables)) {
798
/* No splitting was applied, no empty clause was found by terminator */
799
/*clause_SetSpecialFlags(GivenClause,ana_SortDecreasing());*/
800
prfs_InsertWorkedOffClause(Search, GivenClause);
801
clock_StartCounter(clock_INFERENCE);
802
Derivables = inf_DerivableClauses(Search, GivenClause);
803
clock_StopAddPassedTime(clock_INFERENCE);
804
}
805
}
806
807
prfs_IncDerivedClauses(Search, list_Length(Derivables));
808
809
return Derivables;
810
}
811
812
813
static LIST top_LazyReductionSelectGivenComputeDerivables(PROOFSEARCH Search,
814
CLAUSE *SplitClause,
815
int *Counter, int *MinInstances)
816
/**************************************************************
817
INPUT: A proof search object, a pointer to a clause resulting from a
818
previous splitting step, and a pointer to an integer counter
819
and a pointer to the minimum number of instances for successful split clause selection.
820
RETURNS: A list of derived clauses.
821
EFFECT: In this function a clause is selected from the set of
822
"usable" clauses. After a clause was selected as "given clause",
823
inferences between the given clause and the "worked off" clauses
824
are made. Take a look at the description of the function
825
top_FullReduction... for more details.
826
This function is more complicated than the other function,
827
since clauses in the set of usable clauses may be reducible.
828
Because of this fact, the selection of the given clause
829
has to be done in a loop. After picking a "candidate" clause
830
the clause is inter-reduced with the "worked off" set.
831
If the candidate still exists after the reduction it is
832
selected as given clause, else another usable clause is picked
833
as candidate.
834
***************************************************************/
835
{
836
CLAUSE GivenClause, TerminatorClause;
837
LIST Derivables;
838
FLAGSTORE Flags;
839
PRECEDENCE Precedence;
840
LIST SplitLits;
841
842
GivenClause = (CLAUSE)NULL;
843
TerminatorClause = (CLAUSE)NULL;
844
Derivables = list_Nil();
845
Flags = prfs_Store(Search);
846
Precedence = prfs_Precedence(Search);
847
SplitLits = list_Nil();
848
849
while (GivenClause == (CLAUSE)NULL &&
850
!list_Empty(prfs_UsableClauses(Search))) {
851
/* The selected clause may be redundant */
852
853
if (*SplitClause != NULL &&
854
list_PointerMember(prfs_UsableClauses(Search), *SplitClause))
855
GivenClause = *SplitClause;
856
857
*SplitClause = NULL;
858
859
/* Try selecting a clause that is optimal for splitting */
860
if (GivenClause == NULL) {
861
if (prfs_SplitsAvailable(Search,Flags)) {
862
GivenClause = top_GetPowerfulSplitClause(Search, TRUE, &SplitLits, *MinInstances);
863
list_Delete(SplitLits); /* GivenClause has to be reduced first */
864
}
865
866
if (GivenClause == NULL) {
867
/* No optimal clause for splitting found */
868
*MinInstances = flag_GetFlagIntValue(Flags, flag_SPLITMININST);
869
if ((*Counter) % flag_GetFlagIntValue(Flags, flag_WDRATIO) == 0)
870
GivenClause = top_SelectClauseDepth(prfs_UsableClauses(Search), Flags);
871
else {
872
if (flag_GetFlagIntValue(Flags, flag_PREFCON) != flag_PREFCONUNCHANGED)
873
GivenClause = top_SelectMinimalConWeightClause(prfs_UsableClauses(Search),
874
Flags);
875
else
876
GivenClause = top_SelectMinimalWeightClause(prfs_UsableClauses(Search),
877
Flags);
878
}
879
(*Counter)++;
880
}
881
else
882
(*MinInstances)++;
883
}
884
prfs_ExtractUsable(Search, GivenClause);
885
886
/* Reduce the selected clause */
887
clock_StartCounter(clock_REDUCTION);
888
GivenClause = red_CompleteReductionOnDerivedClause(Search, GivenClause,
889
red_WORKEDOFF);
890
clock_StopAddPassedTime(clock_REDUCTION);
891
}
892
893
if (GivenClause == (CLAUSE)NULL)
894
/* Set of usable clauses is empty */
895
return list_Nil();
896
897
898
if (clause_IsEmptyClause(GivenClause)) {
899
Derivables = list_List(GivenClause);
900
return Derivables;
901
}
902
else {
903
/* Reduce Workedoff clauses with selected clause */
904
clock_StartCounter(clock_REDUCTION);
905
Derivables = red_BackReduction(Search, GivenClause, red_WORKEDOFF);
906
clock_StopAddPassedTime(clock_REDUCTION);
907
}
908
909
clause_SelectLiteral(GivenClause, Flags);
910
/* Print selected clause */
911
if (flag_GetFlagIntValue(Flags, flag_PGIVEN)) {
912
fputs("\n\tGiven clause: ", stdout);
913
clause_Print(GivenClause);
914
fflush(stdout);
915
}
916
917
/* Try splitting */
918
if (prfs_SplitsAvailable(Search,Flags)) {
919
/* First try "optimal" splitting on the selected clause */
920
SplitLits = top_GetSplitLiterals(Search, GivenClause, FALSE);
921
922
if (!list_Empty(SplitLits)) {
923
*SplitClause = prfs_DoSplitting(Search, GivenClause, SplitLits);
924
list_Delete(SplitLits);
925
} else {
926
/* Try the old splitting that allows negative literals */
927
/* sharing variables with the selected positive literal. */
928
*SplitClause = prfs_PerformSplitting(Search, GivenClause);
929
}
930
}
931
932
if (*SplitClause != NULL) {
933
Derivables = list_Cons(*SplitClause, Derivables);
934
} else {
935
/* Try terminator reduction only for a clause that wasn't splitted. */
936
if (flag_GetFlagIntValue(Flags, flag_RTER) != flag_RTEROFF) {
937
TerminatorClause = red_Terminator(GivenClause,
938
flag_GetFlagIntValue(Flags, flag_RTER),
939
prfs_WorkedOffSharingIndex(Search),
940
prfs_UsableSharingIndex(Search),
941
Flags, Precedence);
942
if (TerminatorClause != NULL) {
943
Derivables = list_Cons(TerminatorClause, Derivables);
944
prfs_InsertUsableClause(Search, GivenClause);
945
}
946
}
947
if (TerminatorClause == (CLAUSE)NULL) {
948
/* clause_SetSpecialFlags(GivenClause,ana_SortDecreasing());*/
949
prfs_InsertWorkedOffClause(Search, GivenClause);
950
clock_StartCounter(clock_INFERENCE);
951
Derivables = list_Nconc(Derivables,
952
inf_DerivableClauses(Search, GivenClause));
953
clock_StopAddPassedTime(clock_INFERENCE);
954
}
955
}
956
957
prfs_IncDerivedClauses(Search, list_Length(Derivables));
958
959
return Derivables;
960
}
961
962
963
static PROOFSEARCH top_ProofSearch(PROOFSEARCH Search, LIST ProblemClauses,
964
FLAGSTORE InputFlags, LIST UserPrecedence,
965
int *BoundApplied, BOOL NativeClauseInput)
966
/**************************************************************
967
INPUT: A proof search object, a list of clauses, a flag store
968
containing the flags from the command line and from
969
the input file, a list containing the precedence as
970
specified by the user, a pointer to an integer, and a
971
boolean indicating if the input clauses need to be
972
treated specially.
973
RETURNS: The same proof search object
974
EFFECTS:
975
***************************************************************/
976
{
977
LIST Scan,EmptyClauses,Derivables;
978
LIST UsedEmptyClauses;
979
CLAUSE SplitClause,HighestLevelEmptyClause;
980
FLAGSTORE Flags;
981
PRECEDENCE Precedence;
982
int Counter, ActBound, BoundMode, BoundLoops, MinInstances;
983
984
HighestLevelEmptyClause = (CLAUSE)NULL;
985
UsedEmptyClauses = list_Nil();
986
EmptyClauses = list_Nil();
987
Derivables = list_Nil();
988
Flags = prfs_Store(Search);
989
Precedence = prfs_Precedence(Search);
990
Counter = 1;
991
992
clock_InitCounter(clock_REDUCTION);
993
clock_InitCounter(clock_BACKTRACK);
994
clock_InitCounter(clock_INFERENCE);
995
996
/* Important ! Recomputes Weight ! */
997
ana_AnalyzeProblem(Search, ProblemClauses);
998
if (flag_GetFlagIntValue(Flags, flag_AUTO)) {
999
prfs_InstallFiniteMonadicPredicates(Search, ProblemClauses, ana_FinMonPredList());
1000
ana_AutoConfiguration(ProblemClauses, Flags, Precedence);
1001
/* File and input flags have higher precedence */
1002
flag_TransferSetFlags(InputFlags, Flags);
1003
}
1004
1005
MinInstances = flag_GetFlagIntValue(Flags, flag_SPLITMININST);
1006
1007
/* Rearrange automatically determined precedence according to user's specification. */
1008
symbol_RearrangePrecedence(Precedence, UserPrecedence);
1009
1010
if (NativeClauseInput) {
1011
CLAUSE Clause;
1012
for (Scan = ProblemClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
1013
Clause = (CLAUSE)list_Car(Scan);
1014
clause_OrientEqualities(Clause, Flags, Precedence);
1015
clause_Normalize(Clause);
1016
clause_SetNativeMaxLitFlags(Clause, Flags, Precedence);
1017
clause_UpdateWeight(Clause, Flags);
1018
clause_UpdateMaxVar(Clause);
1019
}
1020
}
1021
else
1022
for (Scan = ProblemClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
1023
clause_OrientAndReInit(list_Car(Scan), Flags, Precedence);
1024
1025
/* Must be called after ana_AnalyzeProblem and Reorientation */
1026
ana_AnalyzeSortStructure(ProblemClauses, Flags, Precedence);
1027
1028
if (flag_GetFlagIntValue(Flags, flag_AUTO)) {
1029
ana_ExploitSortAnalysis(Flags);
1030
/* File and input flags have higher precedence */
1031
flag_TransferSetFlags(InputFlags, Flags);
1032
}
1033
1034
ActBound = flag_GetFlagIntValue(Flags, flag_BOUNDSTART);
1035
BoundMode = flag_GetFlagIntValue(Flags, flag_BOUNDMODE);
1036
BoundLoops = flag_GetFlagIntValue(Flags, flag_BOUNDLOOPS);
1037
*BoundApplied = -1;
1038
1039
if (flag_GetFlagIntValue(Flags, flag_PPROBLEM)) {
1040
puts("");
1041
puts("--------------------------SPASS-START-----------------------------");
1042
puts("Input Problem:");
1043
clause_ListPrint(ProblemClauses);
1044
ana_Print(Flags, Precedence);
1045
}
1046
1047
if (!NativeClauseInput && flag_GetFlagIntValue(Flags, flag_SORTS) != flag_SORTSOFF) {
1048
BOOL Strong;
1049
Strong = (flag_GetFlagIntValue(Flags, flag_SORTS) == flag_SORTSMONADICALL);
1050
for (Scan = ProblemClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
1051
clause_SetSortConstraint((CLAUSE)list_Car(Scan),Strong,Flags, Precedence);
1052
}
1053
1054
if (flag_GetFlagIntValue(Flags, flag_RINPUT)) {
1055
clock_StartCounter(clock_REDUCTION);
1056
EmptyClauses = red_ReduceInput(Search, ProblemClauses);
1057
clock_StopAddPassedTime(clock_REDUCTION);
1058
if (list_Empty(EmptyClauses) && flag_GetFlagIntValue(Flags, flag_SATINPUT))
1059
EmptyClauses = red_SatInput(Search);
1060
}
1061
else {
1062
for (Scan=ProblemClauses; !list_Empty(Scan); Scan=list_Cdr(Scan))
1063
if (red_ExplicitTautology(list_Car(Scan),Flags,Precedence))
1064
clause_Delete(list_Car(Scan));
1065
else
1066
prfs_InsertUsableClause(Search, list_Car(Scan));
1067
}
1068
Derivables = list_Nil();
1069
1070
if (ana_SortRestrictions() ||
1071
(ana_UnsolvedSortRestrictions() &&
1072
flag_GetFlagIntValue(Flags,flag_SORTS) == flag_SORTSMONADICALL)) {
1073
if (flag_GetFlagIntValue(Flags, flag_RSST))
1074
prfs_SetStaticSortTheory(Search,sort_ApproxStaticSortTheory(prfs_UsableClauses(Search),Flags,Precedence));
1075
prfs_SetDynamicSortTheory(Search,sort_TheoryCreate());
1076
}
1077
1078
/* Fix literal order in clauses in the usable set.
1079
Since they are shared, we have to extract them from
1080
the sharing before fixing them. Afterwards, we have to
1081
insert them in the sharing again.
1082
*/
1083
for (Scan = prfs_UsableClauses(Search);
1084
!list_Empty(Scan);
1085
Scan = list_Cdr(Scan)) {
1086
CLAUSE clause;
1087
clause = list_Car(Scan);
1088
clause_MakeUnshared(clause,prfs_UsableSharingIndex(Search));
1089
clause_FixLiteralOrder(clause, Flags, Precedence);
1090
clause_InsertIntoSharing(clause, prfs_UsableSharingIndex(Search),
1091
prfs_Store(Search), prfs_Precedence(Search));
1092
}
1093
1094
/* Calculate the frequency counts and split potential for the symbols in the usable set. */
1095
for (Scan = prfs_UsableClauses(Search);
1096
!list_Empty(Scan);
1097
Scan = list_Cdr(Scan)) {
1098
CLAUSE Clause;
1099
Clause = list_Car(Scan);
1100
if (flag_GetFlagIntValue(Flags, flag_SPLITS) != flag_OFF)
1101
clause_SetSplitPotential(Clause, top_ComputeSplitPotential(Search, Clause));
1102
clause_CountSymbols(Clause);
1103
}
1104
1105
/* Sort usable set. */
1106
prfs_SetUsableClauses(Search,
1107
list_Sort(prfs_UsableClauses(Search),
1108
(BOOL (*) (void *, void *)) clause_CompareAbstractLEQ));
1109
1110
if (flag_GetFlagIntValue(Flags, flag_SOS)) {
1111
Derivables = list_Copy(prfs_UsableClauses(Search));
1112
for (Scan=Derivables;!list_Empty(Scan);Scan=list_Cdr(Scan))
1113
if (!clause_GetFlag(list_Car(Scan), CONCLAUSE))
1114
prfs_MoveUsableWorkedOff(Search,list_Car(Scan));
1115
list_Delete(Derivables);
1116
}
1117
1118
if (flag_GetFlagIntValue(Flags, flag_PPROBLEM)) {
1119
puts("\nProcessed Problem:");
1120
puts("\nWorked Off Clauses:");
1121
clause_ListPrint(prfs_WorkedOffClauses(Search));
1122
puts("\nUsable Clauses:");
1123
clause_ListPrint(prfs_UsableClauses(Search));
1124
}
1125
1126
while ((list_Empty(EmptyClauses) || !prfs_SplitStackEmpty(Search)) &&
1127
prfs_Loops(Search) != 0 &&
1128
((*BoundApplied != -1) || !list_Empty(prfs_UsableClauses(Search))) &&
1129
(flag_GetFlagIntValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED ||
1130
flag_GetFlagIntValue(Flags,flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) {
1131
1132
Derivables = list_Nil();
1133
SplitClause = (CLAUSE)NULL;
1134
*BoundApplied = -1;
1135
1136
while ((list_Empty(EmptyClauses) || !prfs_SplitStackEmpty(Search)) &&
1137
prfs_Loops(Search) != 0 &&
1138
(!list_Empty(prfs_UsableClauses(Search)) || !list_Empty(EmptyClauses)) &&
1139
(flag_GetFlagIntValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED ||
1140
flag_GetFlagIntValue(Flags,flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) {
1141
1142
if (!list_Empty(EmptyClauses)) {
1143
/* Backtracking */
1144
clock_StartCounter(clock_BACKTRACK);
1145
Derivables = split_Backtrack(Search, HighestLevelEmptyClause,
1146
&SplitClause);
1147
clock_StopAddPassedTime(clock_BACKTRACK);
1148
prfs_IncBacktrackedClauses(Search, list_Length(Derivables));
1149
1150
if (prfs_SplitStackEmpty(Search)) {
1151
EmptyClauses = list_PointerDeleteElement(EmptyClauses, HighestLevelEmptyClause);
1152
list_DeleteWithElement(EmptyClauses, (void (*)(POINTER))clause_Delete); /* make sure the right clause is used for doc proof */
1153
Derivables = list_Cons(HighestLevelEmptyClause, Derivables);
1154
}
1155
else {
1156
for ( ; !list_Empty(EmptyClauses); EmptyClauses = list_Pop(EmptyClauses))
1157
if (list_Car(EmptyClauses) != HighestLevelEmptyClause)
1158
clause_Delete(list_Car(EmptyClauses));
1159
prfs_InsertDocProofClause(Search, HighestLevelEmptyClause);
1160
/* Keep HighestLevelEmptyClause for finding the terms required */
1161
/* for the proof. */
1162
if (flag_GetFlagIntValue(Flags, flag_DOCPROOF))
1163
UsedEmptyClauses = list_Cons(HighestLevelEmptyClause, UsedEmptyClauses);
1164
if (flag_GetFlagIntValue(Flags, flag_DOCSPLIT)) {
1165
printf("\n\t Split Backtracking level %d:",prfs_ValidLevel(Search));
1166
if (flag_GetFlagIntValue(Flags, flag_DOCSPLIT) == 2) {
1167
LIST Scon;
1168
printf("\n\t Backtracked clauses:");
1169
for(Scon=Derivables;!list_Empty(Scon);Scon=list_Cdr(Scon)) {
1170
fputs("\n\tBclause: ", stdout);
1171
clause_Print((CLAUSE)list_Car(Scon));
1172
fflush(stdout);
1173
}
1174
printf("\n\t End Backtracked clauses:");
1175
}
1176
}
1177
}
1178
EmptyClauses = list_Nil();
1179
HighestLevelEmptyClause = (CLAUSE)NULL;
1180
}
1181
else { /* no empty clause found */
1182
1183
#ifdef CHECK
1184
if (!prfs_Check(Search)) {
1185
misc_StartErrorReport();
1186
misc_ErrorReport("\n In top_ProofSearch: Illegal state of search in SPASS.\n");
1187
misc_FinishErrorReport();
1188
}
1189
if (!ana_Equations())
1190
red_CheckSplitSubsumptionCondition(Search);
1191
#endif
1192
1193
if (flag_GetFlagIntValue(Flags, flag_FULLRED))
1194
Derivables = top_FullReductionSelectGivenComputeDerivables(Search, &SplitClause, &Counter, &MinInstances);
1195
else
1196
Derivables = top_LazyReductionSelectGivenComputeDerivables(Search, &SplitClause, &Counter, &MinInstances);
1197
}
1198
1199
/* Print the derived clauses, if required */
1200
if (flag_GetFlagIntValue(Flags, flag_PDER))
1201
for (Scan=Derivables; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
1202
fputs("\nDerived: ", stdout);
1203
clause_Print(list_Car(Scan));
1204
}
1205
1206
/* Partition the derived clauses into empty and non-empty clauses */
1207
Derivables = split_ExtractEmptyClauses(Derivables, &EmptyClauses);
1208
1209
/* Apply reduction rules */
1210
clock_StartCounter(clock_REDUCTION);
1211
if (flag_GetFlagIntValue(Flags, flag_FULLRED)) {
1212
EmptyClauses =
1213
list_Nconc(EmptyClauses,
1214
red_CompleteReductionOnDerivedClauses(Search, Derivables,
1215
red_ALL, ActBound,
1216
BoundMode,
1217
BoundApplied));
1218
} else {
1219
EmptyClauses =
1220
list_Nconc(EmptyClauses,
1221
red_CompleteReductionOnDerivedClauses(Search, Derivables,
1222
red_WORKEDOFF,
1223
ActBound, BoundMode,
1224
BoundApplied));
1225
}
1226
clock_StopAddPassedTime(clock_REDUCTION);
1227
1228
1229
if (!list_Empty(EmptyClauses)) {
1230
HighestLevelEmptyClause = split_SmallestSplitLevelClause(EmptyClauses);
1231
if (flag_GetFlagIntValue(Flags, flag_PEMPTYCLAUSE)) {
1232
fputs("\nEmptyClause: ", stdout);
1233
clause_Print(HighestLevelEmptyClause);
1234
}
1235
}
1236
prfs_DecLoops(Search);
1237
}
1238
1239
if (ActBound != flag_BOUNDSTARTUNLIMITED &&
1240
BoundMode != flag_BOUNDMODEUNLIMITED) {
1241
BoundLoops--;
1242
if (BoundLoops == flag_BOUNDLOOPSMIN)
1243
ActBound = flag_BOUNDSTARTUNLIMITED;
1244
else
1245
ActBound = *BoundApplied;
1246
if (*BoundApplied != -1) {
1247
prfs_SwapIndexes(Search);
1248
if (flag_GetFlagIntValue(Flags,flag_PBINC))
1249
printf("\n\n\t ---- New Clause %s Bound: %2d ----\n",
1250
(BoundMode==flag_BOUNDMODERESTRICTEDBYDEPTH) ? "Term Depth" : "Weight",ActBound);
1251
}
1252
}
1253
}
1254
prfs_SetEmptyClauses(Search, EmptyClauses);
1255
prfs_SetUsedEmptyClauses(Search, UsedEmptyClauses);
1256
1257
return Search;
1258
}
1259
1260
1261
static void top_Flotter(int argc, const char* argv[], LIST InputClauses, HASH ClauseToTermLabelList, DFGDESCRIPTION Description)
1262
/**************************************************************
1263
INPUT:
1264
RETURNS: Nothing.
1265
EFFECT:
1266
***************************************************************/
1267
{
1268
FILE *Output;
1269
char *description;
1270
const char *creator = "\n\tCNF generated by FLOTTER " vrs_VERSION " *}";
1271
int size;
1272
int creator_size;
1273
1274
if (cmdlne_GetOutputFile() == (char*)NULL)
1275
Output = stdout;
1276
else
1277
Output = misc_OpenFile(cmdlne_GetOutputFile(),"w");
1278
1279
creator_size = (int)strlen(creator);
1280
size = (int)strlen(desc_Description(Description)) + creator_size;
1281
description = (char*)memory_Malloc(sizeof(char)*size);
1282
strncpy(description,desc_Description(Description),size-creator_size-3);
1283
strcpy(description+size-creator_size-3, creator);
1284
1285
1286
clause_FPrintCnfDFGProblem(Output, FALSE, desc_Name(Description), desc_Author(Description),
1287
desc_StatusString(Description), description, InputClauses,
1288
NULL, NULL, NULL, ClauseToTermLabelList, FALSE, TRUE);
1289
1290
fputs("\nFLOTTER needed\t", stdout);
1291
clock_PrintTime(clock_INPUT);
1292
puts(" for the input.");
1293
fputs("\t\t", stdout);
1294
clock_PrintTime(clock_CNF);
1295
fputs(" for the CNF translation.", stdout);
1296
1297
1298
if (Output != stdout)
1299
misc_CloseFile(Output,cmdlne_GetOutputFile());
1300
memory_Free(description, sizeof(char)*size);
1301
}
1302
1303
static BOOL top_CalledFlotter(FLAGSTORE Flags, const char* Call)
1304
{
1305
int length;
1306
BOOL result;
1307
length = strlen(Call);
1308
result = string_Equal((Call + (length > 7 ? length - 7 : 0)), "FLOTTER");
1309
if (result)
1310
flag_SetFlagIntValue(Flags, flag_FLOTTER, flag_FLOTTERON);
1311
return result;
1312
}
1313
1314
static void top_EstablishClAxRelation(LIST ClAxRelation, LIST InputClauses, LIST* Labellist, HASH ClauseToTermLabellist, BOOL DocProof)
1315
/**************************************************************
1316
INPUT: A list of relations between clause numbers and formula labels (strings) <ClAxRelation>
1317
a list of input clauses
1318
the list of used formula labels
1319
a hash array relating clauses to formula labels (strings)
1320
the doc proof flag
1321
RETURNS: Nothing.
1322
EFFECT: If <DocProof> and the <ClAxRelation> is not empty, then the
1323
list representation of the clause to formula label relation is established
1324
in the hash array <ClauseToTermLabellist> and the labels are collected in <Labellist>
1325
1326
the <ClAxRelation> is eventually deleted
1327
***************************************************************/
1328
{
1329
LIST Scan1, Scan2;
1330
CLAUSE Clause;
1331
1332
if (!list_Empty(ClAxRelation)) {
1333
if (DocProof) {
1334
for (Scan1=ClAxRelation; !list_Empty(Scan1);Scan1=list_Cdr(Scan1)) {
1335
for (Scan2=InputClauses;
1336
!list_Empty(Scan2) &&
1337
clause_Number((CLAUSE)list_Car(Scan2)) != (int)list_Car(list_Car(Scan1));
1338
Scan2=list_Cdr(Scan2));
1339
if (list_Empty(Scan2)) {
1340
misc_StartUserErrorReport();
1341
misc_UserErrorReport("\n For clause %d a formula relation was defined but the clause was not found in the input file!\n",
1342
(int)list_Car(list_Car(Scan1)));
1343
misc_FinishUserErrorReport();
1344
}
1345
Clause = (CLAUSE)list_Car(Scan2);
1346
for (Scan2=list_Cdr(list_Car(Scan1)); !list_Empty(Scan2); Scan2=list_Cdr(Scan2))
1347
*Labellist = list_Cons(list_Car(Scan2), *Labellist);
1348
hsh_PutList(ClauseToTermLabellist, Clause, list_Cdr(list_Car(Scan1)));
1349
list_Free(list_Car(Scan1));
1350
}
1351
*Labellist = list_PointerDeleteDuplicates(*Labellist);
1352
for (Scan1=InputClauses; !list_Empty(Scan1);Scan1=list_Cdr(Scan1))
1353
if (hsh_Get(ClauseToTermLabellist, list_Car(Scan1)) == NULL) {
1354
misc_StartUserErrorReport();
1355
misc_UserErrorReport("\n The formula relation for clause %d is missing!\n",
1356
clause_Number((CLAUSE)list_Car(Scan1)));
1357
misc_FinishUserErrorReport();
1358
}
1359
}
1360
else {
1361
for (Scan1=ClAxRelation;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) {
1362
for (Scan2=list_Cdr(list_Car(Scan1));!list_Empty(Scan2);Scan2=list_Cdr(Scan2))
1363
string_StringFree((char *)list_Car(Scan2));
1364
list_Delete(list_Car(Scan1));
1365
}
1366
}
1367
list_Delete(ClAxRelation);
1368
}
1369
}
1370
1371
1372
1373
/**************************************************************/
1374
/* Main Function */
1375
/**************************************************************/
1376
1377
int main(int argc, const char* argv[])
1378
{
1379
LIST InputClauses,Scan,Axioms,Conjectures, Sorts, QueryClauses,
1380
LabelClauses, QueryPair, ProblemClauses, Labellist, Sortlabellist,
1381
Symblist, UserPrecedence, UserSelection, ClAxRelation;
1382
PROOFSEARCH Search, FlotterSearch;
1383
/* <InputFlags> are the flags from the problem file and the command line. */
1384
FLAGSTORE InputFlags, Flags;
1385
/* <InputPrecedence> is the precedence after reading the problem file. */
1386
PRECEDENCE InputPrecedence, Precedence;
1387
FILE* InputStream;
1388
HASH TermLabelToClauselist, ClauseToTermLabellist;
1389
top_SEARCHRESULT Result;
1390
BOOL NativeClauseInput;
1391
DFGDESCRIPTION Description; /*Problem description store*/
1392
1393
Search = (PROOFSEARCH)NULL;
1394
NativeClauseInput = FALSE;
1395
1396
#ifdef SPASS_SIGNALS
1397
top_PROOFSEARCH = &Search;
1398
signal(SIGINT, top_SigHandler);
1399
signal(SIGTERM, top_SigHandler);
1400
signal(SIGSEGV, top_SigHandler);
1401
signal(SIGBUS, top_SigHandler);
1402
signal(SIGALRM, top_SigHandler);
1403
#endif
1404
1405
clock_Init();
1406
clock_StartCounter(clock_OVERALL);
1407
memory_Init(memory__UNLIMITED);
1408
#ifdef CHECK
1409
atexit(memory_FreeAllMem);
1410
#endif
1411
symbol_Init(TRUE);
1412
stack_Init();
1413
hash_Init();
1414
sort_Init();
1415
term_Init();
1416
1417
InputPrecedence = symbol_CreatePrecedence();
1418
fol_Init(TRUE, InputPrecedence);
1419
eml_Init(InputPrecedence);
1420
cont_Init();
1421
unify_Init();
1422
flag_Init(flag_SPASS);
1423
subs_Init();
1424
clause_Init();
1425
red_Init();
1426
ren_Init();
1427
dp_Init();
1428
cmdlne_Init();
1429
ana_Init();
1430
cc_Init();
1431
tptp_Init();
1432
1433
/* Build proof search object to store definitions in */
1434
Search = prfs_Create();
1435
InputFlags = flag_CreateStore();
1436
1437
if(!cmdlne_Read(argc, argv)) {
1438
return EXIT_FAILURE;
1439
}
1440
1441
/* Check whether flag_STDIN is set in the command line */
1442
flag_InitStoreByDefaults(InputFlags);
1443
if (!cmdlne_SetFlags(InputFlags))
1444
return EXIT_FAILURE;
1445
1446
if (cmdlne_GetInputFile() == (char*) NULL &&
1447
!flag_GetFlagIntValue(InputFlags,flag_STDIN)) {
1448
/* No input file, no stdin input */
1449
printf("\n\t %s %s",argv[0],vrs_VERSION);
1450
if (top_CalledFlotter(InputFlags, argv[0]) ||
1451
flag_GetFlagIntValue(InputFlags, flag_FLOTTER))
1452
puts("\n\t Usage: FLOTTER [options] [<input-file>] [<output-file>]\n");
1453
else
1454
puts("\n\t Usage: SPASS [options] [<input-file>] \n");
1455
puts("Possible options:\n");
1456
cmdlne_PrintSPASSNames();
1457
1458
return EXIT_FAILURE;
1459
}
1460
FlotterSearch = NULL;
1461
1462
Description = desc_Create();
1463
Axioms = Conjectures = Sorts = Labellist = Sortlabellist = UserPrecedence = UserSelection = ClAxRelation = list_Nil();
1464
1465
cmdlne_SetFlags(InputFlags); /* Needed for TPTP flag triggering TPTP parser */
1466
1467
if (flag_GetFlagIntValue(InputFlags, flag_STDIN)) {
1468
top_InputFile = (char*)NULL;
1469
top_RemoveInputFile = FALSE;
1470
InputStream = stdin;
1471
} else {
1472
top_InputFile = cmdlne_GetInputFile();
1473
top_RemoveInputFile = (flag_GetFlagIntValue(InputFlags, flag_GLOBALRIF) == flag_ON);
1474
if (flag_GetFlagIntValue(InputFlags,flag_TPTP) == flag_ON)
1475
InputStream = tptp_OpenFile(top_InputFile,&top_DiscoveredFile);
1476
else
1477
InputStream = dfg_OpenFile(top_InputFile,&top_DiscoveredFile);
1478
}
1479
1480
clock_StartCounter(clock_INPUT);
1481
if (flag_GetFlagIntValue(InputFlags,flag_TPTP) == flag_ON) { /* TPTP parsing */
1482
flag_CleanStore(InputFlags); /* Mark all flags as unset */
1483
InputClauses = tptp_TPTPParser(InputStream, InputFlags, InputPrecedence, Description, &Axioms,
1484
&Conjectures, &Sorts, &UserPrecedence, &UserSelection,
1485
&ClAxRelation, &NativeClauseInput);
1486
}
1487
else { /* DFG parsing */
1488
flag_CleanStore(InputFlags); /* Mark all flags as unset */
1489
/* Now add flags from file to InputFlags and set precedence */
1490
InputClauses = dfg_DFGParser(InputStream, InputFlags, InputPrecedence, Description, &Axioms,
1491
&Conjectures, &Sorts, &UserPrecedence, &UserSelection,
1492
&ClAxRelation, &NativeClauseInput);
1493
}
1494
1495
for(Scan=UserSelection;!list_Empty(Scan);Scan=list_Cdr(Scan))
1496
symbol_AddProperty((SYMBOL)list_Car(Scan), SELECTED);
1497
1498
/* Add/overwrite with command line flags */
1499
cmdlne_SetFlags(InputFlags);
1500
1501
Flags = prfs_Store(Search);
1502
Precedence = prfs_Precedence(Search);
1503
/* The Flags were initialized with the default flag values. */
1504
/* This values are now overwritten by command line flags and flags */
1505
/* from the input file. */
1506
flag_TransferSetFlags(InputFlags, Flags);
1507
/* From now on the input flags are not changed! */
1508
1509
#ifdef SPASS_SIGNALS
1510
if (flag_GetFlagIntValue(Flags,flag_TIMELIMIT) != flag_TIMELIMITUNLIMITED)
1511
alarm(flag_GetFlagIntValue(Flags,flag_TIMELIMIT)+1); /* No race with main loop polling */
1512
#endif
1513
1514
/* Transfer input precedence to search object */
1515
symbol_TransferPrecedence(InputPrecedence, Precedence);
1516
1517
1518
/* Complain about missing input clauses/formulae when in */
1519
/* non-interactive mode */
1520
if (!flag_GetFlagIntValue(Flags, flag_INTERACTIVE) && list_Empty(Axioms) &&
1521
list_Empty(Conjectures) && list_Empty(InputClauses)) {
1522
misc_StartUserErrorReport();
1523
misc_UserErrorReport("\n No formulae and clauses found in input file!\n");
1524
misc_FinishUserErrorReport();
1525
}
1526
1527
cnf_Init(Flags); /* Depends on Strong Skolemization Flag */
1528
1529
/* DocProof is required for interactive mode */
1530
if (flag_GetFlagIntValue(Flags, flag_INTERACTIVE)) {
1531
flag_SetFlagIntValue(Flags, flag_DOCPROOF, flag_DOCPROOFON);
1532
}
1533
1534
if (flag_GetFlagIntValue(Flags, flag_DOCPROOF))
1535
prfs_AddDocProofSharingIndex(Search);
1536
1537
/* Create necessary hasharrays */
1538
if (flag_GetFlagIntValue(Flags, flag_DOCPROOF) ||
1539
top_CalledFlotter(Flags, argv[0]) || flag_GetFlagIntValue(Flags, flag_FLOTTER)) {
1540
TermLabelToClauselist = hsh_Create();
1541
ClauseToTermLabellist = hsh_Create();
1542
}
1543
else {
1544
TermLabelToClauselist = NULL;
1545
ClauseToTermLabellist = NULL;
1546
}
1547
1548
/* Establish clause to term (formula) labels in case of doc proof */
1549
top_EstablishClAxRelation(ClAxRelation,InputClauses, &Labellist, ClauseToTermLabellist,flag_GetFlagIntValue(Flags, flag_DOCPROOF));
1550
1551
/* Build conjecture formula and negate it: Conjectures are taken disjunctively!!*/
1552
for (Scan = Conjectures; !list_Empty(Scan); Scan = list_Cdr(Scan))
1553
list_Rplacd(list_Car(Scan), (LIST)term_Create(fol_Not(),
1554
list_List(list_PairSecond(list_Car(Scan)))));
1555
1556
clock_StopPassedTime(clock_INPUT);
1557
1558
if (top_DiscoveredFile) {
1559
misc_CloseFile(InputStream,top_DiscoveredFile);
1560
if (flag_GetFlagIntValue(Flags, flag_GLOBALRIF) == flag_ON)
1561
remove(top_InputFile);
1562
}
1563
1564
clock_StartCounter(clock_CNF);
1565
1566
if (list_Empty(InputClauses)) {
1567
NAT Termcount;
1568
1569
Termcount = 0;
1570
1571
/* Create labels for formulae without them */
1572
for (Scan = Axioms; !list_Empty(Scan); Scan = list_Cdr(Scan), Termcount++) {
1573
if (list_PairFirst(list_Car(Scan)) == NULL) {
1574
char L[100];
1575
char* Label;
1576
sprintf(L, "axiom%d", Termcount);
1577
Label = string_StringCopy(L);
1578
list_Rplaca(list_Car(Scan), Label);
1579
if (flag_GetFlagIntValue(Flags, flag_DOCPROOF) &&
1580
flag_GetFlagIntValue(Flags, flag_PLABELS)) {
1581
printf("\nAdded label %s for axiom \n", Label);
1582
fol_PrettyPrintDFG((TERM) list_PairSecond(list_Car(Scan)));
1583
}
1584
}
1585
}
1586
Termcount = 0;
1587
for (Scan = Sorts; !list_Empty(Scan); Scan = list_Cdr(Scan), Termcount++) {
1588
char L[100];
1589
char* Label;
1590
sprintf(L, "declaration%d", Termcount);
1591
Label = string_StringCopy(L);
1592
list_Rplaca(list_Car(Scan), Label);
1593
if (flag_GetFlagIntValue(Flags, flag_DOCPROOF) &&
1594
flag_GetFlagIntValue(Flags, flag_PLABELS)) {
1595
printf("\nAdded label %s for declaration \n", Label);
1596
fol_PrettyPrintDFG((TERM) list_PairSecond(list_Car(Scan)));
1597
}
1598
Sortlabellist = list_Cons(Label, Sortlabellist);
1599
}
1600
Axioms = list_Nconc(Axioms, Sorts);
1601
1602
if (flag_GetFlagIntValue(Flags, flag_EML)) {
1603
clock_StartCounter(clock_TRANSL);
1604
1605
/* Reduce EML special formulae to first-order logic */
1606
if (flag_GetFlagIntValue(Flags, flag_EML) ) {
1607
eml_TranslateToFolMain(&Axioms, &Conjectures,
1608
flag_GetFlagIntValue(Flags, flag_INTERACTIVE), Flags, Precedence);
1609
}
1610
1611
clock_StopPassedTime(clock_TRANSL);
1612
}
1613
1614
if (flag_GetFlagIntValue(Flags, flag_APPLYDEFS) != flag_APPLYDEFSOFF) {
1615
def_ExtractDefsFromTermlist(Search, Axioms, Conjectures);
1616
Conjectures = def_ApplyDefinitionToTermList(prfs_Definitions(Search),
1617
Conjectures, Flags,
1618
Precedence);
1619
}
1620
1621
/* We must keep the list of symbols because they can't be freed in cnf_Flotter */
1622
Symblist = list_Nil();
1623
1624
/* Axioms is list of pairs, conjectures is list of terms */
1625
/* A ProofSearch object is only returned and the symbols kept in Symblist
1626
if flag_INTERACTIVE is set */
1627
FlotterSearch = cnf_Flotter(Axioms,Conjectures,&InputClauses, &Labellist,
1628
TermLabelToClauselist, ClauseToTermLabellist,
1629
Flags, Precedence, &Symblist);
1630
1631
InputClauses = clause_ListSortWeighed(InputClauses);
1632
clause_SetCounter(1);
1633
for (Scan = InputClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) {
1634
clause_NewNumber(list_Car(Scan));
1635
}
1636
}
1637
else {
1638
dfg_DeleteFormulaPairList(Axioms);
1639
dfg_DeleteFormulaPairList(Sorts);
1640
dfg_DeleteFormulaPairList(Conjectures);
1641
if (flag_GetFlagIntValue(Flags, flag_APPLYDEFS) != flag_APPLYDEFSOFF) {
1642
/* Extract list of definitions */
1643
def_ExtractDefsFromClauselist(Search, InputClauses);
1644
def_FlattenDefinitionsDestructive(Search);
1645
for (Scan=prfs_Definitions(Search); !list_Empty(Scan); Scan=list_Cdr(Scan))
1646
InputClauses = def_ApplyDefToClauselist(Search, (DEF) list_Car(Scan),
1647
InputClauses, TRUE);
1648
}
1649
}
1650
1651
clock_StopPassedTime(clock_CNF);
1652
1653
if (top_CalledFlotter(Flags, argv[0]) || flag_GetFlagIntValue(Flags, flag_FLOTTER)) {
1654
if ( flag_GetFlagIntValue(Flags, flag_SORTS) != flag_SORTSOFF) { /* Now native clause output, so lets print sorts already */
1655
for (Scan = InputClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
1656
clause_SetSortConstraint((CLAUSE)list_Car(Scan), FALSE, Flags, Precedence);
1657
}
1658
top_Flotter(argc,argv,InputClauses, ClauseToTermLabellist,Description);
1659
flag_SetFlagIntValue(Flags, flag_TIMELIMIT, 0); /* Exit No Output */
1660
flag_SetFlagIntValue(Flags, flag_INTERACTIVE, flag_INTERACTIVEOFF);
1661
flag_SetFlagIntValue(Flags, flag_PPROBLEM, flag_PPROBLEMOFF);
1662
}
1663
1664
memory_Restrict(flag_GetFlagIntValue(Flags, flag_MEMORY));
1665
symbol_SeparateVariableSymbolNames();
1666
1667
do {
1668
LIST deflist;
1669
int BoundApplied;
1670
ProblemClauses = list_Nil();
1671
LabelClauses = list_Nil();
1672
Result = top_RESOURCE;
1673
1674
if (flag_GetFlagIntValue(Flags, flag_INTERACTIVE)) {
1675
QueryPair = ia_GetNextRequest(InputStream, Flags);
1676
/* A pair (<formula,labellist>) */
1677
/* Get list of clauses derivable from formulae with labels in labellist */
1678
if (list_Empty(QueryPair)) {
1679
break;
1680
}
1681
for (Scan=list_PairSecond(QueryPair);!list_Empty(Scan);Scan=list_Cdr(Scan)) {
1682
LIST l;
1683
l = hsh_GetWithCompareFunc(TermLabelToClauselist, list_Car(Scan),
1684
(BOOL (*)(POINTER, POINTER)) cnf_LabelEqual,
1685
(unsigned long (*)(POINTER)) hsh_StringHashKey);
1686
1687
l = list_PointerDeleteDuplicates(list_Copy(l));
1688
LabelClauses = list_Nconc(l, LabelClauses);
1689
}
1690
/* Get list of clauses derivable from sorts */
1691
for (Scan=Sortlabellist; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
1692
LIST l;
1693
l = hsh_GetWithCompareFunc(TermLabelToClauselist, list_Car(Scan),
1694
(BOOL (*)(POINTER, POINTER)) cnf_LabelEqual,
1695
(unsigned long (*)(POINTER)) hsh_StringHashKey);
1696
1697
l = list_PointerDeleteDuplicates(list_Copy(l));
1698
LabelClauses = list_Nconc(l, LabelClauses);
1699
}
1700
1701
/* For labelclauses copies are introduced */
1702
/* So an update to the clause to term mapping is necessary */
1703
for (Scan=LabelClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) {
1704
CLAUSE C;
1705
LIST l;
1706
C = (CLAUSE) list_Car(Scan);
1707
l = list_Copy(hsh_Get(ClauseToTermLabellist, C));
1708
l = cnf_DeleteDuplicateLabelsFromList(l);
1709
list_Rplaca(Scan, clause_Copy(C));
1710
hsh_PutList(ClauseToTermLabellist, list_Car(Scan), l);
1711
}
1712
QueryClauses = cnf_QueryFlotter(FlotterSearch, list_PairFirst(QueryPair),
1713
&Symblist);
1714
ProblemClauses = list_Nconc(QueryClauses, LabelClauses);
1715
1716
for (Scan=list_PairSecond(QueryPair); !list_Empty(Scan); Scan= list_Cdr(Scan))
1717
string_StringFree(list_Car(Scan)); /* Free the label strings */
1718
list_Delete(list_PairSecond(QueryPair));
1719
list_PairFree(QueryPair);
1720
clock_InitCounter(clock_OVERALL);
1721
clock_StartCounter(clock_OVERALL);
1722
}
1723
else {
1724
ProblemClauses = InputClauses;
1725
InputClauses = list_Nil();
1726
}
1727
1728
prfs_SetLoops(Search,flag_GetFlagIntValue(Flags, flag_LOOPS));
1729
prfs_SetBacktrackedClauses(Search, 0);
1730
BoundApplied = -1;
1731
if (flag_GetFlagIntValue(Flags, flag_LOOPS) != 0 && flag_GetFlagIntValue(Flags, flag_TIMELIMIT) != 0)
1732
Search = top_ProofSearch(Search, ProblemClauses, InputFlags, UserPrecedence, &BoundApplied, NativeClauseInput);
1733
1734
if ((flag_GetFlagIntValue(Flags, flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED ||
1735
flag_GetFlagIntValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL)) &&
1736
prfs_Loops(Search) != 0 &&
1737
(BoundApplied == -1 || !list_Empty(prfs_EmptyClauses(Search)))) {
1738
if (list_Empty(prfs_EmptyClauses(Search)))
1739
Result = top_COMPLETION;
1740
else
1741
Result = top_PROOF;
1742
}
1743
1744
if (flag_GetFlagIntValue(Flags, flag_TIMELIMIT) != 0 && top_NoAlarm == 0) {
1745
/* Stop SPASS immediately */
1746
top_NoAlarm = 1; /* No race with SIGALRM handler */
1747
printf("\nSPASS %s ", vrs_VERSION);
1748
fputs("\nSPASS beiseite: ", stdout);
1749
switch (Result) {
1750
case top_RESOURCE:
1751
if (prfs_Loops(Search) != 0)
1752
fputs("Ran out of time.", stdout);
1753
else
1754
fputs("Maximal number of loops exceeded.", stdout);
1755
break;
1756
case top_PROOF:
1757
fputs("Proof found.", stdout);
1758
break;
1759
default: /* Completion */
1760
fputs("Completion found.", stdout);
1761
}
1762
printf("\nProblem: %s ",
1763
(top_DiscoveredFile != (char*)NULL ? top_DiscoveredFile : "Read from stdin."));
1764
if (flag_GetFlagIntValue(Flags, flag_PSTATISTIC)) {
1765
clock_StopPassedTime(clock_OVERALL);
1766
printf("\nSPASS derived %d clauses,", prfs_DerivedClauses(Search));
1767
printf(" backtracked %d clauses,", prfs_BacktrackedClauses(Search));
1768
printf(" performed %d splits", prfs_SplitCounter(Search));
1769
printf(" and kept %d clauses.", prfs_KeptClauses(Search));
1770
printf("\nSPASS allocated %lu KBytes.", memory_DemandedBytes()/1024);
1771
fputs("\nSPASS spent\t", stdout);
1772
clock_PrintTime(clock_OVERALL);
1773
fputs(" on the problem.\n\t\t", stdout);
1774
clock_PrintTime(clock_INPUT);
1775
fputs(" for the input.\n\t\t", stdout);
1776
clock_PrintTime(clock_CNF);
1777
fputs(" for the FLOTTER CNF translation", stdout);
1778
if(flag_GetFlagIntValue(Flags, flag_EML)) {
1779
fputs(", of which", stdout);
1780
fputs("\n\t\t", stdout); clock_PrintTime(clock_TRANSL);
1781
fprintf(stdout, " for the translation from %s to FOL", flag_Name(flag_EML));
1782
}
1783
printf(".");
1784
printf("\n\t\t"); clock_PrintTime(clock_INFERENCE);
1785
fputs(" for inferences.\n\t\t", stdout);
1786
clock_PrintTime(clock_BACKTRACK);
1787
fputs(" for the backtracking.\n\t\t", stdout);
1788
clock_PrintTime(clock_REDUCTION);
1789
puts(" for the reduction.");
1790
}
1791
if (Result != top_PROOF &&
1792
flag_GetFlagIntValue(Flags, flag_FPMODEL) != flag_FPMODELOFF) {
1793
FILE *Output;
1794
char name[100];
1795
const char * creator = "{*SPASS " vrs_VERSION " *}";
1796
BOOL PrintPotProductive;
1797
1798
strcpy(name, (top_InputFile != (char*)NULL ? top_InputFile : "SPASS"));
1799
if (Result == top_COMPLETION)
1800
strcat(name, ".model");
1801
else
1802
strcat(name, ".clauses");
1803
Output = misc_OpenFile(name,"w");
1804
PrintPotProductive = (flag_GetFlagIntValue(Flags, flag_FPMODEL) ==
1805
flag_FPMODELPOTENTIALLYPRODUCTIVECLAUSES);
1806
if (Result == top_COMPLETION)
1807
clause_FPrintCnfDFGProblem(Output, PrintPotProductive,
1808
"{*Completion_by_SPASS*}",
1809
creator, "satisfiable",
1810
desc_Description(Description),
1811
prfs_WorkedOffClauses(Search),
1812
list_Nil(), Flags, Precedence, NULL, TRUE, TRUE);
1813
else
1814
clause_FPrintCnfDFGProblem(Output, PrintPotProductive,
1815
"{*Clauses_generated_by_SPASS*}",
1816
creator, "unknown",
1817
desc_Description(Description),
1818
prfs_WorkedOffClauses(Search),
1819
prfs_UsableClauses(Search), Flags,
1820
Precedence, NULL, FALSE, TRUE);
1821
misc_CloseFile(Output, name);
1822
if (Result == top_COMPLETION)
1823
printf("\nCompletion printed to: %s\n", name);
1824
else
1825
printf("\nClauses printed to: %s\n", name);
1826
}
1827
1828
if (flag_GetFlagIntValue(Flags, flag_DOCPROOF) && Result != top_RESOURCE) {
1829
if (Result == top_COMPLETION) {
1830
puts("\n\n The saturated set of worked-off clauses is :");
1831
clause_ListPrint(prfs_WorkedOffClauses(Search));
1832
}
1833
else {
1834
LIST UsedClauses, UsedTerms;
1835
UsedClauses = dp_PrintProof(Search, prfs_EmptyClauses(Search),
1836
top_DiscoveredFile ? top_DiscoveredFile : "SPASS");
1837
/* Find terms required for proof */
1838
UsedTerms = list_Nil();
1839
1840
for (Scan = UsedClauses; !list_Empty(Scan); Scan = list_Cdr(Scan))
1841
if (clause_IsFromInput((CLAUSE) list_Car(Scan))) {
1842
LIST L;
1843
L = hsh_Get(ClauseToTermLabellist, list_Car(Scan));
1844
L = list_Copy(L);
1845
L = cnf_DeleteDuplicateLabelsFromList(L);
1846
UsedTerms = list_Nconc(UsedTerms, L);
1847
}
1848
list_Delete(UsedClauses);
1849
UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms);
1850
fputs("\nFormulae used in the proof :", stdout);
1851
for (Scan = UsedTerms; !list_Empty(Scan); Scan = list_Cdr(Scan))
1852
if (!(strncmp((char*) list_Car(Scan), "_SORT_", 6) == 0))
1853
printf(" %s", (char*) list_Car(Scan));
1854
putchar('\n');
1855
list_Delete(UsedTerms);
1856
}
1857
}
1858
}
1859
1860
/* Delete mapping for the clause copies of the labelclauses */
1861
for (Scan = LabelClauses; !list_Empty(Scan); Scan=list_Cdr(Scan))
1862
hsh_DelItem(ClauseToTermLabellist, list_Car(Scan));
1863
1864
list_Delete(ProblemClauses);
1865
1866
fflush(stdout);
1867
1868
/* Keep definitions */
1869
deflist = prfs_Definitions(Search);
1870
prfs_SetDefinitions(Search, list_Nil());
1871
prfs_Clean(Search);
1872
prfs_SetDefinitions(Search, deflist);
1873
1874
symbol_TransferPrecedence(InputPrecedence, Precedence);
1875
if (flag_GetFlagIntValue(Flags, flag_PPROBLEM))
1876
fputs("\n--------------------------SPASS-STOP------------------------------", stdout);
1877
} while (flag_GetFlagIntValue(Flags, flag_INTERACTIVE) &&
1878
(flag_GetFlagIntValue(Flags, flag_TIMELIMIT) != 0));
1879
1880
for (Scan = InputClauses; !list_Empty(Scan); Scan=list_Cdr(Scan))
1881
clause_OrientAndReInit(list_Car(Scan), Flags, Precedence);
1882
1883
/* Cleanup Flotter data structures */
1884
if (flag_GetFlagIntValue(Flags, flag_INTERACTIVE)) {
1885
if (flag_GetFlagIntValue(Flags, flag_DOCPROOF))
1886
list_Delete(Symblist);
1887
else
1888
symbol_DeleteSymbolList(Symblist);
1889
/* symbol_ResetSkolemIndex(); */
1890
if (FlotterSearch != NULL)
1891
prfs_Delete(FlotterSearch);
1892
}
1893
if (flag_GetFlagIntValue(Flags, flag_PFLAGS)) {
1894
putchar('\n');
1895
flag_Print(Flags);
1896
}
1897
if (TermLabelToClauselist != (HASH)NULL) {
1898
hsh_Delete(TermLabelToClauselist);
1899
hsh_Delete(ClauseToTermLabellist);
1900
}
1901
for (Scan = Labellist; !list_Empty(Scan); Scan = list_Cdr(Scan))
1902
string_StringFree(list_Car(Scan));
1903
list_Delete(Labellist);
1904
list_Delete(Sortlabellist);
1905
list_Delete(UserPrecedence);
1906
list_Delete(UserSelection);
1907
1908
cnf_Free(Flags);
1909
eml_Free();
1910
1911
if (top_DiscoveredFile)
1912
string_StringFree(top_DiscoveredFile);
1913
1914
prfs_Delete(Search);
1915
clause_DeleteClauseList(InputClauses);
1916
flag_DeleteStore(InputFlags);
1917
symbol_DeletePrecedence(InputPrecedence);
1918
desc_Delete(Description);
1919
1920
tptp_Free();
1921
cc_Free();
1922
ana_Free();
1923
sort_Free();
1924
subs_Free();
1925
unify_Free();
1926
cont_Free();
1927
fol_Free();
1928
symbol_FreeAllSymbols();
1929
red_Free();
1930
cmdlne_Free();
1931
#ifdef CHECK
1932
memory_Print();
1933
memory_PrintLeaks();
1934
#endif
1935
putchar('\n');
1936
return 0;
1937
}
Loggerhead is a web-based interface for Breezy
Version: 2.0.1