1
2 /*
3 * File TheoryFinder.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file TheoryFinder.cpp
21 * Implements class TheoryFinder for finding theories in the input problems.
22 *
23 * @since 09/06/2004 Manchester
24 * @since 09/07/2008 Linz, changed to new datastructures
25 * @since 28/07/2008 flight Linz airport and train Manchester-London, reimplemented completely
26 * and simplified
27 */
28
29 // #include "CodeGenerator.hpp"
30
31 #include "Debug/Tracer.hpp"
32
33 #include "Kernel/Clause.hpp"
34 #include "Kernel/Formula.hpp"
35 #include "Kernel/FormulaUnit.hpp"
36 #include "Kernel/Term.hpp"
37
38 #include "Property.hpp"
39 #include "TheoryFinder.hpp"
40
41 // Set this to 1 to make Vampire output all matching steps
42 #define TRACE_FINDER 0
43 // Set this to 1 to make Vampire output found matches
44 #define SHOW_FOUND 0
45
46 using namespace Lib;
47 using namespace Shell;
48 using namespace Kernel;
49
50 /**
51 * Build a new theory finder.
52 * @since 09/06/2004 Manchester
53 */
TheoryFinder(const UnitList * units,Property * property)54 TheoryFinder::TheoryFinder (const UnitList* units,Property* property)
55 : _units(units),
56 _property(property)
57 {
58 CALL("TheoryFinder::TheoryFinder");
59 } // TheoryFinder::TheoryFinder
60
61 /**
62 * @since 09/06/2004 Manchester
63 */
~TheoryFinder()64 TheoryFinder::~TheoryFinder ()
65 {
66 CALL("TheoryFinder::~TheoryFinder");
67 } // TheoryFinder::TheoryFinder
68
69 /**
70 * @since 09/06/2004 Manchester
71 * @since 18/06/2004 Manchester, added proof-search for theories
72 */
search()73 int TheoryFinder::search()
74 {
75 CALL("TheoryFinder::search");
76
77 int found = 0;
78 UnitList::Iterator uit(_units);
79 while (uit.hasNext()) {
80 if (matchAll(uit.next())) {
81 found++;
82 }
83 }
84
85 return found;
86 } // TheoryFinder::search
87
88
89 /**
90 * Match against all known axioms.
91 *
92 * @since 09/06/2004 Manchester
93 * @since 27/07/2008 Linz Airport, changed to new datastructures
94 */
matchAll(const Unit * unit)95 bool TheoryFinder::matchAll(const Unit* unit)
96 {
97 CALL("TheoryFinder::matchAll(const Unit*)");
98
99 // do not remove this, we need a pointer to an existing unit
100 if (unit->isClause()) {
101 return matchAll(static_cast<const Clause*>(unit));
102 }
103
104 return matchAll(static_cast<const FormulaUnit*>(unit)->formula());
105 } // TheoryFinder::matchAll
106
107 /**
108 * Match clause against all known axioms.
109 *
110 * @since 09/06/2004 Manchester
111 * @since 27/07/2008 Linz Airport, changed to new datastructures
112 */
matchAll(const Clause * clause)113 bool TheoryFinder::matchAll(const Clause* clause)
114 {
115 CALL("TheoryFinder::matchAll(const Clause*)");
116
117 switch (clause->length()) {
118 case 1:
119 return matchAll((*clause)[0]);
120 case 2:
121 return matchSubset(clause);
122 return false;
123 case 3:
124 return matchFLD2(clause) ||
125 matchCondensedDetachment1(clause) ||
126 matchCondensedDetachment2(clause) ||
127 matchExtensionality(clause);
128 case 4:
129 return matchFLD1(clause);
130 default:
131 return false;
132 }
133 } // TheoryFinder::matchAll(const Clause* clause)
134
135 /**
136 * Match formula against all known axioms.
137 *
138 * @since 09/06/2004 Manchester
139 * @since 27/07/2008 Linz Airport, changed to new datastructures
140 */
matchAll(const Formula * formula)141 bool TheoryFinder::matchAll(const Formula* formula)
142 {
143 CALL("TheoryFinder::matchAll (const Formula*...)");
144
145 while (formula->connective() == FORALL) {
146 formula = formula->qarg();
147 }
148
149 if (formula->connective() == LITERAL) {
150 return matchAll(formula->literal());
151 }
152
153 return matchExtensionality(formula) ||
154 matchSubset(formula) ||
155 matchListConstructors(formula);
156 } // TheoryFinder::matchAll(const Formula*)
157
158 /**
159 * Class for representing information stored about backtrack points
160 * @since 31/07/2008 Manchester
161 */
162 class TheoryFinder::Backtrack
163 {
164 public:
165 /** code pointer */
166 unsigned cp;
167 /** object on which the instruction should be executed */
168 const void* obj;
169 /** position in the object stack */
170 unsigned objPos;
171 }; // TheoryFinder::Backtrack
172
matchCode(const void * obj,const unsigned char * code,uint64_t prop)173 bool TheoryFinder::matchCode(const void* obj,
174 const unsigned char* code,
175 uint64_t prop)
176 {
177 CALL("TheoryFinder::matchCode/3");
178
179 bool found = matchCode(obj, code);
180 if (found && prop) {
181 _property->addProp(prop);
182 }
183 return found;
184 }
185
186 /**
187 * Match the code against an object (a Formula,FormulaList,Literal,TermList or Term).
188 *
189 * @return true if succeeds
190 * @since 24/06/2004 Dresden
191 * @since 28/07/2008 train Manchester-London
192 * @Since 30/01/2014 Refactored pure matching code to be static and public.
193 * Previous method updating the Property field calls this method.
194 */
matchCode(const void * obj,const unsigned char * code)195 bool TheoryFinder::matchCode(const void* obj,
196 const unsigned char* code)
197 {
198 CALL("TheoryFinder::matchCode/2");
199
200 Backtrack backtrack[20];
201 unsigned backtrackPos = 0;
202
203 // stack of objects to be inspected later
204 const void* objects[100];
205 int objectPos = 1;
206 objects[0] = obj;
207
208 // variable numbers
209 unsigned vars[10];
210 // function symbol numbers
211 unsigned funs[10];
212 // predicate symbol numbers
213 unsigned preds[10];
214 unsigned cp = 0; // code pointer
215
216 // the clause, if any
217 const Clause* clause;
218 // the length of this clause
219 int clength;
220 // literal numbers to be matched by LIT i commands
221 int literals[4];
222
223 match:
224 switch (code[cp]) {
225 case END:
226 #if TRACE_FINDER
227 cout << "Matched\n";
228 #endif
229 return true;
230
231 case NEWVAR: {
232 ASS(objectPos > 0);
233 obj = objects[--objectPos];
234 const TermList* ts = reinterpret_cast<const TermList*>(obj);
235 #if TRACE_FINDER
236 cout << "M: NEWVAR " << (int)code[cp+1] << ": " << ts->toString() << "\n";
237 #endif
238 if (! ts->isVar()) {
239 goto backtrack;
240 }
241 vars[code[cp+1]] = ts->var();
242 if (! ts->next()->isEmpty()) {
243 objects[objectPos++] = ts->next();
244 }
245 cp += 2;
246 goto match;
247 }
248
249 case NEWFUN:
250 case NEWFUN1: {
251 ASS(objectPos > 0);
252 obj = objects[--objectPos];
253 const TermList* ts = reinterpret_cast<const TermList*>(obj);
254 int funNumber = code[cp+1];
255 #if TRACE_FINDER
256 cout << "M: NEWFUN" << (code[cp] == NEWFUN1 ? "1" : "") << ' ' << funNumber
257 << '/' << (int)code[cp+2] << ": " << ts->toString() << "\n";
258 #endif
259 if (ts->isVar()) {
260 goto backtrack;
261 }
262 const Term* t = ts->term();
263 if (t->arity() != code[cp+2]) {
264 goto backtrack;
265 }
266 // check that the function is new
267 for (int k = funNumber - 1; k >= 0; k--) {
268 if (funs[k] == t->functor()) {
269 goto backtrack;
270 }
271 }
272 funs[funNumber] = t->functor();
273 if (code[cp] == NEWFUN && ! ts->next()->isEmpty()) {
274 objects[objectPos++] = ts->next();
275 }
276 ts = t->args();
277 if (! ts->isEmpty()) {
278 objects[objectPos++] = ts;
279 }
280 cp += 3;
281 goto match;
282 }
283
284 case NEWPRED: {
285 ASS(objectPos > 0);
286 obj = objects[--objectPos];
287 const Literal* lit = reinterpret_cast<const Literal*>(obj);
288 int predNumber = code[cp+1];
289 #if TRACE_FINDER
290 cout << "M: NEWPRED " << predNumber << '/' << (int)code[cp+2] << ": " << lit->toString() << "\n";
291 #endif
292 if (lit->arity() != code[cp+2]) {
293 goto backtrack;
294 }
295 // check that the predicate is new
296 for (int k = predNumber - 1; k >= 0; k--) {
297 if (preds[k] == lit->functor()) {
298 goto backtrack;
299 }
300 }
301 preds[predNumber] = lit->functor();
302 const TermList* ts = lit->args();
303 if (! ts->isEmpty()) {
304 objects[objectPos++] = ts;
305 }
306 cp += 3;
307 goto match;
308 }
309
310 case OLDFUN:
311 case OLDFUN1: {
312 ASS(objectPos > 0);
313 obj = objects[--objectPos];
314 const TermList* ts = reinterpret_cast<const TermList*>(obj);
315 #if TRACE_FINDER
316 cout << "M: OLDFUN" << (code[cp] == OLDFUN1 ? "1" : "") << " " << (int)code[cp+1]
317 << '/' << (int)code[cp+2] << ": " << ts->toString() << "\n";
318 #endif
319 if (ts->isVar()) {
320 goto backtrack;
321 }
322 const Term* t = ts->term();
323 if (funs[code[cp+1]] != t->functor()) {
324 goto backtrack;
325 }
326 if (code[cp] == OLDFUN && ! ts->next()->isEmpty()) {
327 objects[objectPos++] = ts->next();
328 }
329 ts = t->args();
330 if (! ts->isEmpty()) {
331 objects[objectPos++] = ts;
332 }
333 cp += 2;
334 goto match;
335 }
336
337 case OLDPRED: {
338 #if TRACE_FINDER
339 cout << "M: OLDPRED " << (int)code[cp+1] << "\n";
340 #endif
341 ASS(objectPos > 0);
342 obj = objects[--objectPos];
343 const Literal* lit = reinterpret_cast<const Literal*>(obj);
344
345 if (preds[code[cp+1]] != lit->functor()) {
346 goto backtrack;
347 }
348 const TermList* ts = lit->args();
349 if (! ts->isEmpty()) {
350 objects[objectPos++] = ts;
351 }
352 cp += 2;
353 goto match;
354 }
355
356 case OLDVAR:
357 case OLDVAR1: {
358 ASS(objectPos > 0);
359 obj = objects[--objectPos];
360 const TermList* ts = reinterpret_cast<const TermList*>(obj);
361 #if TRACE_FINDER
362 cout << "M: OLDVAR" << (code[cp] == OLDVAR1 ? "1" : "")
363 << ' ' << (int)code[cp+1] << ": " << ts->toString() << "\n";
364 #endif
365 if (! ts->isVar()) {
366 goto backtrack;
367 }
368 if (vars[code[cp+1]] != ts->var()) {
369 goto backtrack;
370 }
371 if (code[cp] == OLDVAR && ! ts->next()->isEmpty()) {
372 objects[objectPos++] = ts->next();
373 }
374 cp += 2;
375 goto match;
376 }
377
378 case EQL: {
379 ASS(objectPos > 0);
380 obj = objects[--objectPos];
381 const Literal* lit = reinterpret_cast<const Literal*>(obj);
382 #if TRACE_FINDER
383 cout << "M: EQL: " << lit->toString() << "\n";
384 #endif
385 if (! lit->isEquality()) {
386 goto backtrack;
387 }
388
389 Backtrack& back = backtrack[backtrackPos++];
390 back.cp = cp;
391 back.obj = obj;
392 back.objPos = objectPos;
393
394 const TermList* ts = lit->args();
395 objects[objectPos++] = ts->next();
396 objects[objectPos++] = ts;
397
398 cp++;
399 goto match;
400 }
401
402 case CLS: {
403 ASS(objectPos > 0);
404 obj = objects[--objectPos];
405 clause = reinterpret_cast<const Clause*>(obj);
406 #if TRACE_FINDER
407 cout << "M: CLS: " << clause->toString() << endl;
408 #endif
409 clength = clause->length();
410 cp++;
411 goto match;
412 }
413
414 case PLIT:
415 case NLIT: {
416 #if TRACE_FINDER
417 cout << "M: LIT " << (int)code[cp+1] << "\n";
418 #endif
419 unsigned l = code[cp+1];
420 // bit field of choices for this literal
421 unsigned choice = (1u << clength) - 1;
422 for (int i = l-1;i >= 0;i--) {
423 // remove from the choice literals already used
424 choice -= 1u << literals[i];
425 }
426 int c = 0;
427 // find the next available literal whose polarity matches
428 while (c < clength) {
429 // remove from the choice literals already used
430 if (choice & (1 << c)) {
431 if ((*clause)[c]->isPositive()) {
432 if (code[cp] == PLIT) {
433 break;
434 }
435 }
436 else if (code[cp] == NLIT) {
437 break;
438 }
439 }
440 c++;
441 }
442
443 if (c == clength) { // no candidate found
444 goto backtrack;
445 }
446
447 // create a backtrack point
448 Backtrack& back = backtrack[backtrackPos++];
449 back.cp = cp;
450 back.objPos = objectPos;
451
452 literals[l] = c;
453 objects[objectPos++] = (*clause)[c];
454
455 cp += 2;
456 goto match;
457 }
458
459 case CIFF:
460 case NBCIFF: {
461 ASS(objectPos > 0);
462 obj = objects[--objectPos];
463 const Formula* f = reinterpret_cast<const Formula*>(obj);
464 #if TRACE_FINDER
465 cout << "M: IFF: " << f->toString() << "\n";
466 #endif
467 if (f->connective() != IFF) {
468 goto backtrack;
469 }
470
471 if (code[cp] == CIFF) {
472 Backtrack& back = backtrack[backtrackPos++];
473 back.cp = cp;
474 back.obj = obj;
475 back.objPos = objectPos;
476 }
477
478 objects[objectPos++] = f->right();
479 objects[objectPos++] = f->left();
480
481 cp++;
482 goto match;
483 }
484
485 // FUTURE WORK: COR is not commutative, currently we add code for both permutations
486 // it should be changed
487 case COR: {
488 ASS(objectPos > 0);
489 obj = objects[--objectPos];
490 const Formula* f = reinterpret_cast<const Formula*>(obj);
491 #if TRACE_FINDER
492 cout << "M: OR " << (int)code[cp+1] << ": " << f->toString() << "\n";
493 #endif
494 if (f->connective() != OR) {
495 goto backtrack;
496 }
497
498 // TEMPORARY, we can only handle disjunctions of length 2
499 ASS(code[cp+1] == 2);
500
501 const FormulaList* args = f->args();
502 if (FormulaList::length(args) != code[cp+1]) {
503 goto backtrack;
504 }
505
506 // Backtrack& back = backtrack[backtrackPos++];
507 // back.cp = cp;
508 // back.obj = obj;
509 // back.objPos = objectPos;
510
511 FormulaList::Iterator as(args);
512 while (as.hasNext()) {
513 objects[objectPos++] = as.next();
514 }
515
516 cp += 2;
517 goto match;
518 }
519
520 case CIMP: {
521 ASS(objectPos > 0);
522 obj = objects[--objectPos];
523 const Formula* f = reinterpret_cast<const Formula*>(obj);
524 #if TRACE_FINDER
525 cout << "M: IMP: " << f->toString() << "\n";
526 #endif
527 if (f->connective() != IMP) {
528 goto backtrack;
529 }
530
531 objects[objectPos++] = f->right();
532 objects[objectPos++] = f->left();
533
534 cp++;
535 goto match;
536 }
537
538 case CFORALL: {
539 ASS(objectPos > 0);
540 obj = objects[--objectPos];
541 const Formula* f = reinterpret_cast<const Formula*>(obj);
542 #if TRACE_FINDER
543 cout << "M: FORALL " << (int)code[cp+1] << ": " << f->toString() << "\n";
544 #endif
545 if (f->connective() != FORALL) {
546 goto backtrack;
547 }
548 if (Formula::VarList::length(f->vars()) != code[cp+1]) {
549 goto backtrack;
550 }
551 cp += 2;
552 List<int>::Iterator vs(f->vars());
553 while (vs.hasNext()) {
554 vars[code[cp++]] = vs.next();
555 }
556 objects[objectPos++] = f->qarg();
557
558 goto match;
559 }
560
561 case POS: {
562 ASS(objectPos > 0);
563
564 obj = objects[--objectPos];
565 const Formula* f = reinterpret_cast<const Formula*>(obj);
566 #if TRACE_FINDER
567 cout << "M: POS: " << f->toString() << "\n";
568 #endif
569 if (f->connective() != LITERAL) {
570 goto backtrack;
571 }
572 const Literal* lit = f->literal();
573 if (! lit->isPositive()) {
574 goto backtrack;
575 }
576 objects[objectPos++] = lit;
577
578 cp++;
579 goto match;
580 }
581
582 #if VDEBUG
583 case CAND:
584 case CNOT:
585 case CXOR:
586 case CEXISTS:
587 case NEG:
588 case TERM:
589 case FORM:
590 default:
591 ASSERTION_VIOLATION;
592 #endif
593 }
594
595 backtrack:
596 if (backtrackPos == 0) {
597 #if TRACE_FINDER
598 cout << "M: fail\n";
599 #endif
600 return false;
601 }
602 // retrieving information for backtracking
603 Backtrack& back = backtrack[--backtrackPos];
604 cp = back.cp;
605 obj = back.obj;
606
607 ASS_GE(objectPos,(int)back.objPos); // if we already went below the stored objPos, if the restored code succeeds, we will continue into undefined territory
608 // Actually, this might still be to weak; we should insist the whole objects stack up back.objPos is identical to the one when Backtrack back was created.
609 // Example of the problem: Matching
610 /* {CIFF, // <=>
611 * CFORALL,1,0,CIFF, // (Ax0)<=>
612 * POS,NEWPRED,0,2,OLDVAR,0,NEWVAR,1, // member(x0,x1)
613 * POS,OLDPRED,0,OLDVAR,0,NEWVAR,2, // member(x0,x2)
614 * POS,EQL,OLDVAR1,1,OLDVAR1,2,END}; // x1=x2
615 * against
616 * set_equal(X,Y) <=> ! [Z] : ( element(Z,X) <=> element(Z,Y) ).
617 *
618 * After
619 * ! [Z] : ( element(Z,X) <=> element(Z,Y) )
620 * succeeds
621 * set_equal(X,Y)
622 * fails (because set_equal is not "=").
623 *
624 * Backtracking to the other polarity of ( element(Z,X) <=> element(Z,Y) )
625 * is at this point evil, since the objects stack no longer contains
626 * set_equal(X,Y) as a LITARAL formula at objectPos==0
627 *
628 * In this case fixed by using non-backtrackable CIFF for the inner <=>
629 **/
630
631 objectPos = back.objPos;
632
633 switch (code[cp]) {
634 case EQL: {
635 const Literal* lit = reinterpret_cast<const Literal*>(obj);
636 #if TRACE_FINDER
637 cout << "B: EQL: " << lit->toString() << "\n";
638 #endif
639 const TermList* ts = lit->args();
640 objects[objectPos++] = ts;
641 objects[objectPos++] = ts->next();
642
643 cp++;
644 goto match;
645 }
646
647 case CIFF: {
648 const Formula* f = reinterpret_cast<const Formula*>(obj);
649 #if TRACE_FINDER
650 cout << "B: IFF: " << f->toString() << "\n";
651 #endif
652 objects[objectPos++] = f->left();
653 objects[objectPos++] = f->right();
654
655 cp++;
656 goto match;
657 }
658
659 case PLIT:
660 case NLIT: {
661 #if TRACE_FINDER
662 cout << "B: LIT\n";
663 #endif
664 unsigned l = code[cp+1];
665 // bit field of choices for this literal
666 unsigned choice = (1u << clength) - 1;
667 for (int i = l-1;i >= 0;i--) {
668 // remove from the choice literals already used
669 choice -= 1u << literals[i];
670 }
671 int c = literals[l]+1;
672 // find the next available literal whose polarity matches
673 while (c < clength) {
674 // remove from the choice literals already used
675 if (choice & (1 << c)) {
676 if ((*clause)[c]->isPositive()) {
677 if (code[cp] == PLIT) {
678 break;
679 }
680 }
681 else if (code[cp] == NLIT) {
682 break;
683 }
684 }
685 c++;
686 }
687
688 if (c == clength) { // no candidate found
689 goto backtrack;
690 }
691
692 // create a backtrack point
693 Backtrack& back = backtrack[backtrackPos++];
694 back.cp = cp;
695 back.objPos = objectPos;
696
697 literals[l] = c;
698 objects[objectPos++] = (*clause)[c];
699
700 cp += 2;
701 goto match;
702 }
703
704 #if VDEBUG
705 default:
706 ASSERTION_VIOLATION;
707 #endif
708 }
709 } // TheoryFinder::MatcherState::match
710
711 /**
712 * Match atom against commutativity x+y=y+x.
713 *
714 * @since 10/06/2004 Manchester
715 */
matchC(const Literal * lit)716 bool TheoryFinder::matchC(const Literal* lit)
717 {
718 CALL("TheoryFinder::matchC");
719
720 #if TRACE_FINDER
721 cout << lit->toString() << "\n";
722 #endif
723 static const unsigned char code[] =
724 {EQL, // // =
725 NEWFUN1,0,2,NEWVAR,0,NEWVAR,1, // +(x0,x1)
726 OLDFUN1,0,OLDVAR,1,OLDVAR,0,
727 END}; // +(x1,x0)
728
729 if (matchCode(lit,code,0)) {
730 #if SHOW_FOUND
731 cout << "C: " << lit->toString() << "\n";
732 #endif
733 return true;
734 }
735 return false;
736 } // TheoryFinder::matchC(const Literal* lit)
737
738
739 /**
740 * Match atom against associativity (x+y)+z=x+(y+z).
741 *
742 * @since 16/06/2005 Manchester
743 */
matchA(const Literal * lit)744 bool TheoryFinder::matchA(const Literal* lit)
745 {
746 CALL("TheoryFinder::matchA");
747 static const unsigned char code[] =
748 {EQL, // // =
749 NEWFUN1,0,2,OLDFUN,0,
750 NEWVAR,0,NEWVAR,1,NEWVAR,2, // +(+(x0,x1),x2)
751 OLDFUN1,0,OLDVAR,0,OLDFUN,0,
752 OLDVAR,1,OLDVAR,2, // +(x0,+(x1,x2))
753 END};
754
755 if (matchCode(lit,code,0)) {
756 #if SHOW_FOUND
757 cout << "A: " << lit->toString() << "\n";
758 #endif
759 return true;
760 }
761 return false;
762 } // TheoryFinder::matchA(const Literal* lit)
763
764 /**
765 * Match clause against part of extensionality axiom
766 * member(f(X,Y),X) \/ member(f(X,Y),Y) \/ X=Y
767 *
768 * @since 25/06/2004 Dresden
769 */
matchExtensionality(const Clause * c)770 bool TheoryFinder::matchExtensionality (const Clause* c)
771 {
772 CALL("TheoryFinder::matchExtensionality (const Clause&...)");
773
774 static const unsigned char code[] =
775 {CLS,
776 NLIT,0,
777 NEWPRED,0,2, // ~member(f(X,Y),X),
778 NEWFUN,0,2,NEWVAR,0,NEWVAR,1,OLDVAR,0,
779 NLIT,1,
780 OLDPRED,0, // ~member(f(X,Y),Y),
781 OLDFUN,0,OLDVAR,0,OLDVAR,1,OLDVAR,1,
782 PLIT,2,
783 EQL,OLDVAR,0,OLDVAR,1,END}; // X=Y
784
785 if (matchCode(c,code,Property::PR_HAS_EXTENSIONALITY)) {
786 #if SHOW_FOUND
787 cout << "Extensionality: " << c->toString() << "\n";
788 #endif
789 return true;
790 }
791 return false;
792 } // TheoryFinder::matchExtensionality
793
794 /**
795 * Match clause against the condensed detachment axiom
796 * ~theorem(X) \/ ~theorem(imply(X,Y)) \/ theorem(Y).
797 *
798 * @since 21/06/2005 Manchester
799 */
matchCondensedDetachment1(const Clause * c)800 bool TheoryFinder::matchCondensedDetachment1(const Clause* c)
801 {
802 CALL("TheoryFinder::CondensedDetachment1(const LiteralList&...)");
803
804 static const unsigned char code[] =
805 {CLS,
806 PLIT,0,
807 NEWPRED,0,1,NEWVAR,0, // theorem(x0)
808 NLIT,1,
809 OLDPRED,0,NEWVAR,1, // ~theorem(x1)
810 NLIT,2,
811 OLDPRED,0,NEWFUN,0,2,OLDVAR,1,OLDVAR,0,END}; // ~theorem(imply(x1,x0))
812
813 if (matchCode(c,code,Property::PR_HAS_CONDENSED_DETACHMENT1)) {
814 #if SHOW_FOUND
815 cout << "Condensed detachment 1: " << c->toString() << "\n";
816 #endif
817 return true;
818 }
819 return false;
820 } // TheoryFinder::matchCondensedDetachment1
821
822 /**
823 * Match clause against the condensed detachment axiom
824 * ~theorem(X) \/ ~theorem(or(not(X),Y)) \/ theorem(Y).
825 *
826 * @since 21/06/2005 Manchester
827 */
matchCondensedDetachment2(const Clause * c)828 bool TheoryFinder::matchCondensedDetachment2(const Clause* c)
829 {
830 CALL("TheoryFinder::CondensedDetachment2(const Clause&...)");
831
832 static const unsigned char code[] =
833 {CLS,
834 PLIT,0,
835 NEWPRED,0,1,NEWVAR,0, // theorem(x0)
836 NLIT,1,
837 OLDPRED,0,NEWVAR,1, // ~theorem(x1)
838 NLIT,2,
839 OLDPRED,0,NEWFUN,0,2,NEWFUN,1,1,OLDVAR,1,OLDVAR,0,END}; // ~theorem(or(not(x1),x0))
840
841 if (matchCode(c,code,Property::PR_HAS_CONDENSED_DETACHMENT2)) {
842 #if SHOW_FOUND
843 cout << "Condensed detachment 2: " << c->toString() << "\n";
844 #endif
845 return true;
846 }
847 return false;
848 } // TheoryFinder::matchmatchCondensedDetachment2
849
850 /**
851 * Match clause against the axiom
852 * equalish(add(multiply(X,Z),multiply(Y,Z)),multiply(add(X,Y),Z)) \/
853 * ~defined(X) \/ ~defined(Y) \/ ~defined(Z).
854 *
855 * @since 21/06/2005 Manchester
856 */
matchFLD1(const Clause * c)857 bool TheoryFinder::matchFLD1(const Clause* c)
858 {
859 CALL("TheoryFinder::matchFLD1(const Clause&...)");
860
861 static const unsigned char code[] =
862 {CLS,
863 PLIT,0,
864 NEWPRED,0,2,NEWFUN,0,2,NEWFUN,1,2,NEWVAR,0,NEWVAR,1, // equalish(add(multiply(x0,x1),
865 OLDFUN,1,NEWVAR,2,OLDVAR,1, // multiply(x2,x1)),
866 OLDFUN,1,OLDFUN,0,OLDVAR,0,OLDVAR,2,OLDVAR,1, // multiply(add(x0,x2),x1))
867 NLIT,1,
868 NEWPRED,1,1,OLDVAR,0, // ~defined(x0)
869 NLIT,2,
870 OLDPRED,1,OLDVAR,2, // ~defined(x2)
871 NLIT,3,
872 OLDPRED,1,OLDVAR,1,END}; // ~defined(x1)
873
874 if (matchCode(c,code,Property::PR_HAS_FLD1)) {
875 #if SHOW_FOUND
876 cout << "FLD1: " << c->toString() << "\n";
877 #endif
878 return true;
879 }
880 return false;
881 } // TheoryFinder::matchFLD1
882
883 /**
884 * Match clause against the axiom
885 * product(multiplicative_inverse(X),X,multiplicative_identity) \/
886 * sum(additive_identity,X,additive_identity) \/
887 * ~defined(X).
888 *
889 * @since 21/06/2005 Manchester
890 */
matchFLD2(const Clause * c)891 bool TheoryFinder::matchFLD2(const Clause* c)
892 {
893 CALL("TheoryFinder::matchFLD2(const Clause&...)");
894
895 static const unsigned char code[] =
896 {CLS,
897 PLIT,0,
898 NEWPRED,0,3,NEWFUN,0,1,NEWVAR,0,OLDVAR,0,NEWFUN,0,0, // product(inv(x0),x0,1)
899 PLIT,1,
900 NEWPRED,1,3,NEWFUN,2,0,OLDVAR,0,OLDFUN,2, // sum(0,x0,0)
901 NLIT,2,
902 NEWPRED,2,1,OLDVAR,0,END}; // ~defined(x0)
903
904 if (matchCode(c,code,Property::PR_HAS_FLD2)) {
905 #if SHOW_FOUND
906 cout << "FLD2: " << c->toString() << "\n";
907 #endif
908 return true;
909 }
910 return false;
911 } // TheoryFinder::matchFLD2
912
913 /**
914 * Match clause against part of the subset axiom
915 * member(f(X,Y),X) \/ subset(X,Y), where f is disregarded.
916 *
917 * @since 24/06/2004 Dresden
918 * @since 19/06/2005 Manchester, simplified using matchCode(...)
919 */
matchSubset(const Clause * c)920 bool TheoryFinder::matchSubset (const Clause* c)
921 {
922 CALL("TheoryFinder::matchSubset(const Clause* c)");
923
924 static const unsigned char code[] =
925 {CLS,
926 PLIT,0,
927 NEWPRED,0,2, // member(f(X,Y),X),
928 NEWFUN,0,2,NEWVAR,0,NEWVAR,1,OLDVAR,0,
929 PLIT,1,
930 NEWPRED,1,2,OLDVAR,0,OLDVAR,1,END}; // subset(X,Y)
931
932 if (matchCode(c,code,Property::PR_HAS_SUBSET)) {
933 #if SHOW_FOUND
934 cout << "Subset: " << c->toString() << "\n";
935 #endif
936 return true;
937 }
938 return false;
939 } // TheoryFinder::matchSubset
940
941 /**
942 * Match formula against part the subset axiom
943 * subset(x,y) <=> (Az)(member(z,x) => member(z,y)).
944 *
945 * @since 25/06/2004 Dresden
946 * @since 19/06/2005 Manchester, simplified using matchCode(...)
947 */
matchSubset(const Formula * f)948 bool TheoryFinder::matchSubset (const Formula* f)
949 {
950 CALL("TheoryFinder::matchSubset(const Formula* f)");
951
952 static const unsigned char code[] =
953 {CIFF, // <=>
954 POS,NEWPRED,0,2,NEWVAR,0,NEWVAR,1, // subset(x,y)
955 CFORALL,1,2,CIMP, // (Az) =>
956 POS,NEWPRED,1,2,OLDVAR,2,OLDVAR,0,// member(z,x)
957 POS,OLDPRED,1,OLDVAR,2,OLDVAR,1,END}; // member(z,y)
958
959 if (matchCode(f,code,Property::PR_HAS_SUBSET)) {
960 #if SHOW_FOUND
961 cout << "Subset: " << f->toString() << "\n";
962 #endif
963 return true;
964 }
965 return false;
966 } // TheoryFinder::matchSubset
967
968 // tff(l1,axiom,(! [K: $int,L: list] : head(cons(K,L)) = K )).
969 // tff(l2,axiom,(! [K: $int,L: list] : tail(cons(K,L)) = L )).
970 // %----Constructors
971 // tff(l3,axiom,(
972 // ! [L: list] :
973 // ( L = nil
974 // | L = cons(head(L),tail(L)) ) )).
975 // tff(l4,axiom,(
976 // ! [K: $int,L: list] : cons(K,L) != nil )).
977
978 /**
979 * Match formula against part the list constructors axiom
980 * L = nil v L = cons(head(L),tail(L))
981 * @since 16/06/2015 Manchester
982 * @author Andrei Voronkov
983 */
matchListConstructors(const Formula * f)984 bool TheoryFinder::matchListConstructors (const Formula* f)
985 {
986 CALL("TheoryFinder::matchListConstructors");
987 #if TRACE_FINDER
988 cout << "M: [match list constructors axiom]\n";
989 #endif
990
991 static const unsigned char code1[] =
992 {COR,2, // \/
993 POS,EQL,NEWVAR,0, // =(L,
994 NEWFUN1,0,2, // cons
995 NEWFUN,1,1,OLDVAR,0, // head(L)
996 NEWFUN,2,1,OLDVAR,0, // tail(L)
997 POS,EQL,OLDVAR1,0,NEWFUN1,3,0,END}; // =(L,nil)
998 static const unsigned char code2[] =
999 {COR,2, // \/
1000 POS,EQL,NEWVAR,0,NEWFUN1,0,0, // =(L,nil)
1001 POS,EQL,OLDVAR1,0, // =(L,
1002 NEWFUN1,1,2, // cons
1003 NEWFUN,2,1,OLDVAR,0, // head(L)
1004 NEWFUN,3,1,OLDVAR,0, // tail(L)
1005 END};
1006 if (matchCode(f,code1,Property::PR_LIST_AXIOMS) ||
1007 matchCode(f,code2,Property::PR_LIST_AXIOMS)) {
1008 #if SHOW_FOUND
1009 cout << "List constructors: " << f->toString() << "\n";
1010 #endif
1011 return true;
1012 }
1013 return false;
1014 } // TheoryFinder::matchListConstructors
1015
1016 /**
1017 * Match formula against the extensionality axiom
1018 * (Az)(member(z,x) <=> member(z,y)) => x=y,
1019 * or the same but with <=> instead of =>.
1020 *
1021 * @since 25/06/2004 Dresden
1022 * @since 19/06/2005 Manchester, simplified using matchCode(...)
1023 */
matchExtensionality(const Formula * f)1024 bool TheoryFinder::matchExtensionality (const Formula* f)
1025 {
1026 CALL("TheoryFinder::matchExtensionality (const Formula&...)");
1027
1028 static const unsigned char code1[] =
1029 {CIFF, // <=>
1030 CFORALL,1,0,NBCIFF, // (Ax0)<=>
1031 POS,NEWPRED,0,2,OLDVAR,0,NEWVAR,1, // member(x0,x1)
1032 POS,OLDPRED,0,OLDVAR,0,NEWVAR,2, // member(x0,x2)
1033 POS,EQL,OLDVAR1,1,OLDVAR1,2,END}; // x1=x2
1034 static const unsigned char code2[] =
1035 {CIMP, // =>
1036 CFORALL,1,0,NBCIFF, // (Ax0)<=>
1037 POS,NEWPRED,0,2,OLDVAR,0,NEWVAR,1, // member(x0,x1)
1038 POS,OLDPRED,0,OLDVAR,0,NEWVAR,2, // member(x0,x2)
1039 POS,EQL,OLDVAR1,1,OLDVAR1,2,END}; // x1=x2
1040
1041 // NBCIFF explained: As the LHS and the RHS of the inner <=> are variants, it does not make sense to backtrack over them; EQL is commutative to check the two versions!
1042
1043 if (matchCode(f,code1,Property::PR_HAS_EXTENSIONALITY) ||
1044 matchCode(f,code2,Property::PR_HAS_EXTENSIONALITY)) {
1045 #if SHOW_FOUND
1046 cout << "Extensionality: " << f->toString() << "\n";
1047 #endif
1048 return true;
1049 }
1050 return false;
1051 } // TheoryFinder::matchExtensionality
1052
1053
1054 /**
1055 * Match atom against the left inverse axiom i(x)*x=1
1056 *
1057 * @since 16/06/2005 Manchester
1058 */
matchLeftInverse(const Literal * lit)1059 bool TheoryFinder::matchLeftInverse(const Literal* lit)
1060 {
1061 CALL("TheoryFinder::matchLeftInverse");
1062
1063 static const unsigned char code[] =
1064 {EQL, // // =
1065 NEWFUN1,0,2,NEWFUN,1,1,NEWVAR,0,OLDVAR,0, // *(i(x0),x0)
1066 NEWFUN1,2,0, // 1
1067 END};
1068
1069 if (matchCode(lit,code,0)) {
1070 #if SHOW_FOUND
1071 cout << "Left inverse: " << lit->toString() << "\n";
1072 #endif
1073 return true;
1074 }
1075 return false;
1076 } // TheoryFinder::matchLeftInverse(const Literal* lit)
1077
1078 /**
1079 * Match atom against the right inverse axiom x*i(x)=1
1080 *
1081 * @since 16/06/2005 Manchester
1082 */
matchRightInverse(const Literal * lit)1083 bool TheoryFinder::matchRightInverse(const Literal* lit)
1084 {
1085 CALL("TheoryFinder::matchRightInverse");
1086
1087 static const unsigned char code[] =
1088 {EQL, // // =
1089 NEWFUN1,0,2,NEWVAR,0,NEWFUN,1,1,OLDVAR,0,// *(x0,i(x0))
1090 NEWFUN1,2,0, // 1
1091 END};
1092
1093 if (matchCode(lit,code,0)) {
1094 #if SHOW_FOUND
1095 cout << "Right inverse: " << lit->toString() << "\n";
1096 #endif
1097 return true;
1098 }
1099 return false;
1100 } // TheoryFinder::matchRightInverse(const Literal* lit)
1101
1102 /**
1103 * Match atom against the left identity axiom 1*x=x
1104 *
1105 * @since 16/06/2005 Manchester
1106 */
matchLeftIdentity(const Literal * lit)1107 bool TheoryFinder::matchLeftIdentity(const Literal* lit)
1108 {
1109 CALL("TheoryFinder::matchLeftIdentity");
1110
1111 static const unsigned char code[] =
1112 {EQL, // // =
1113 NEWFUN1,0,2,NEWFUN,1,0,NEWVAR,0, // *(1,x)
1114 OLDVAR1,0, // x
1115 END};
1116
1117 if (matchCode(lit,code,0)) {
1118 #if SHOW_FOUND
1119 cout << "Left identity: " << lit->toString() << "\n";
1120 #endif
1121 return true;
1122 }
1123 return false;
1124 } // TheoryFinder::matchLeftIdentity(const Literal* lit)
1125
1126 /**
1127 * Match atom against the idempotence axiom x*x=x
1128 *
1129 * @since 16/06/2005 Manchester
1130 */
matchIdempotence(const Literal * lit)1131 bool TheoryFinder::matchIdempotence(const Literal* lit)
1132 {
1133 CALL("TheoryFinder::matchIdempotence");
1134
1135 static const unsigned char code[] =
1136 {EQL,NEWFUN1,0,2,NEWVAR,0,OLDVAR,0,
1137 OLDVAR1,0,END}; // =(*(x0,x0),x0)
1138
1139 if (matchCode(lit,code,0)) {
1140 #if SHOW_FOUND
1141 cout << "Idempotence: " << lit->toString() << "\n";
1142 #endif
1143 return true;
1144 }
1145 return false;
1146 } // TheoryFinder::matchIdempotence(const Literal* lit)
1147
1148 /**
1149 * Match atom against the right identity axiom x*1=x
1150 *
1151 * @since 16/06/2005 Manchester
1152 */
matchRightIdentity(const Literal * lit)1153 bool TheoryFinder::matchRightIdentity(const Literal* lit)
1154 {
1155 CALL("TheoryFinder::matchRightIdentity");
1156
1157 static const unsigned char code[] =
1158 {EQL, // // =
1159 NEWFUN1,0,2,NEWVAR,0,NEWFUN,1,0, // *(x,1)
1160 OLDVAR1,0,END}; // x
1161
1162 if (matchCode(lit,code,0)) {
1163 #if SHOW_FOUND
1164 cout << "Right identity: " << lit->toString() << "\n";
1165 #endif
1166 return true;
1167 }
1168 return false;
1169 } // TheoryFinder::matchRightIdentity(const Literal* lit)
1170
1171 /**
1172 * Match atom against the associator axiom
1173 * A(x,y,z) = A(x,y,z) = +(*(*(x,y),z),-(*(x,*(y,z)))).
1174 *
1175 * @since 17/06/2005 Manchester
1176 */
matchAssociator(const Literal * lit)1177 bool TheoryFinder::matchAssociator(const Literal* lit)
1178 {
1179 CALL("TheoryFinder::matchAssociator");
1180
1181 static const unsigned char code[] =
1182 {EQL, // // =
1183 NEWFUN1,0,3,NEWVAR,0,NEWVAR,1,NEWVAR,2, // A(x0,x1,x2)
1184 NEWFUN1,1,2,NEWFUN,2,2,OLDFUN,2,OLDVAR,0,OLDVAR,1,OLDVAR,2, // +(*(*(x0,x1),x2),
1185 NEWFUN,3,1,OLDFUN,2,OLDVAR,0,OLDFUN,2,OLDVAR,1,OLDVAR,2, // -(*(x0,*(x1,x2))))
1186 END};
1187
1188 if (matchCode(lit,code,0)) {
1189 #if SHOW_FOUND
1190 cout << "Associator: " << lit->toString() << "\n";
1191 #endif
1192 return true;
1193 }
1194 return false;
1195 } // TheoryFinder::matchAssociator
1196
1197 /**
1198 * Match atom against the commutator axiom C(x,y) = +(*(y,x),-(*(x,y))).
1199 *
1200 * @since 17/06/2005 Manchester
1201 */
matchCommutator(const Literal * lit)1202 bool TheoryFinder::matchCommutator(const Literal* lit)
1203 {
1204 CALL("TheoryFinder::matchCommutator");
1205
1206 static const unsigned char code[] =
1207 {EQL, // =
1208 NEWFUN1,0,3,NEWVAR,0,NEWVAR,1, // C(x0,x1)
1209 NEWFUN1,1,2,NEWFUN,2,2,OLDVAR,1,OLDVAR,0, // +(*(x1,x0),
1210 NEWFUN,3,1,OLDFUN,2,OLDVAR,0,OLDVAR,1, // -(*(x0,x1)))
1211 END};
1212
1213 if (matchCode(lit,code,0)) {
1214 #if SHOW_FOUND
1215 cout << "Commutator: " << lit->toString() << "\n";
1216 #endif
1217 return true;
1218 }
1219 return false;
1220 } // TheoryFinder::matchCommutator
1221
1222 /**
1223 * Match atom against the left distributivity axiom.
1224 *
1225 * @since 17/06/2005 Manchester
1226 */
matchLeftDistributivity(const Literal * lit)1227 bool TheoryFinder::matchLeftDistributivity(const Literal* lit)
1228 {
1229 CALL("TheoryFinder::matchLeftDistributivity");
1230
1231 static const unsigned char code[] =
1232 {EQL, // // =
1233 NEWFUN1,0,2,NEWFUN,1,2,NEWVAR,0,
1234 NEWVAR,1,NEWVAR,2, // *(+(x0,x1),x2)
1235 OLDFUN1,1,OLDFUN,0,OLDVAR,0,OLDVAR,2,
1236 OLDFUN,0,OLDVAR,1,OLDVAR,2,END}; // +(*(x0,x2),*(x1,x2))
1237
1238 if (matchCode(lit,code,0)) {
1239 #if SHOW_FOUND
1240 cout << "Left distributivity: " << lit->toString() << "\n";
1241 #endif
1242 return true;
1243 }
1244 return false;
1245 } // TheoryFinder::matchLeftDistributivity(const Literal* lit)
1246
1247 /**
1248 * Match atom against the right distributivity axiom.
1249 *
1250 * @since 17/06/2005 Manchester
1251 */
matchRightDistributivity(const Literal * lit)1252 bool TheoryFinder::matchRightDistributivity (const Literal* lit)
1253 {
1254 CALL("TheoryFinder::matchRightDistributivity");
1255
1256 static const unsigned char code[] =
1257 {EQL, // // =
1258 NEWFUN1,0,2,NEWVAR,0,NEWFUN,1,2,
1259 NEWVAR,1,NEWVAR,2, // *(x0,+(x1,x2))
1260 OLDFUN1,1,OLDFUN,0,OLDVAR,0,OLDVAR,1,
1261 OLDFUN,0,OLDVAR,0,OLDVAR,2,END}; // +(*(x0,x1),*(x0,x2))
1262
1263 if (matchCode(lit,code,0)) {
1264 #if SHOW_FOUND
1265 cout << "Right distributivity: " << lit->toString() << "\n";
1266 #endif
1267 return true;
1268 }
1269 return false;
1270 } // TheoryFinder::matchRightDistributivity(const Literal* lit)
1271
1272 /**
1273 * Match atom against any of the four versions of the Robbins Algebra axiom.
1274 *
1275 * @since 17/06/2005 Manchester
1276 */
matchRobbins(const Literal * lit)1277 bool TheoryFinder::matchRobbins(const Literal* lit)
1278 {
1279 CALL("TheoryFinder::matchRobbins");
1280
1281 static const unsigned char code1[] =
1282 {EQL, // // =
1283 NEWFUN1,0,1,NEWFUN,1,2,OLDFUN,0,OLDFUN,1,NEWVAR,0,NEWVAR,1,// n(+(n(+(x0,x1)),
1284 OLDFUN,0,OLDFUN,1,OLDVAR,0,OLDFUN,0,OLDVAR,1, // n(+(x0,n(x1)))))
1285 OLDVAR1,0,END}; // x0
1286 static const unsigned char code2[] =
1287 {EQL, // // =
1288 NEWFUN1,0,1,NEWFUN,1,2,OLDFUN,0,OLDFUN,1,NEWVAR,0,NEWVAR,1,// n(+(n(+(x0,x1)),
1289 OLDFUN,0,OLDFUN,1,OLDFUN,0,OLDVAR,0,OLDVAR,1, // n(+(n(x0),x1))))
1290 OLDVAR1,1,END}; // x1
1291 static const unsigned char code3[] =
1292 {EQL, // // =
1293 NEWFUN1,0,1,NEWFUN,1,2,OLDFUN,0,OLDFUN,1,NEWVAR,0,OLDFUN,0,NEWVAR,1,// n(+(n(+(x0,n(x1))),
1294 OLDFUN,0,OLDFUN,1,OLDVAR,0,OLDVAR,1, // n(+(x0,x1))))
1295 OLDVAR1,0,END}; // x0
1296 static const unsigned char code4[] =
1297 {EQL, // // =
1298 NEWFUN,0,1,NEWFUN,1,2,OLDFUN,0,OLDFUN,1,OLDFUN,0,NEWVAR,0,NEWVAR,1,// n(+(n(+(n(x0),x1)),
1299 OLDFUN,0,OLDFUN,1,OLDVAR,0,OLDVAR,1, // n(+(x0,x1))))
1300 OLDVAR,1,END}; // x1
1301
1302 if (matchCode(lit,code1,0) ||
1303 matchCode(lit,code2,0) ||
1304 matchCode(lit,code3,0) ||
1305 matchCode(lit,code4,0)) {
1306 #if SHOW_FOUND
1307 cout << "Robbins: " << lit->toString() << "\n";
1308 #endif
1309 return true;
1310 }
1311 return false;
1312 } // TheoryFinder::matchRobbins(const Literal* lit)
1313
1314 /**
1315 * Match atom against any of the two versions of the alternative
1316 * associativity axiom: *(*(x,x),y) = *(x,*(x,y)) or
1317 * *(*(x,y),y) = *(x,*(y,y)).
1318 *
1319 * @since 17/06/2005 Manchester
1320 */
matchAlternative(const Literal * lit)1321 bool TheoryFinder::matchAlternative(const Literal* lit)
1322 {
1323 CALL("TheoryFinder::matchAlternative");
1324
1325 static const unsigned char code1[] =
1326 {EQL, // // =
1327 NEWFUN1,0,2,OLDFUN,0,NEWVAR,0,OLDVAR,0,NEWVAR,1, // *(*(x0,x0),x1)
1328 OLDFUN1,0,OLDVAR,0,OLDFUN,0,OLDVAR,0,OLDVAR,1,END}; // *(x0,*(x0,x1))
1329 static const unsigned char code2[] =
1330 {EQL, // // =
1331 NEWFUN1,0,2,OLDFUN,0,NEWVAR,0,NEWVAR,1,OLDVAR,1, // *(*(x0,x1),x1)
1332 OLDFUN1,0,OLDVAR,0,OLDFUN,0,OLDVAR,1,OLDVAR,1,END}; // *(x0,*(x1,x1))
1333
1334 if (matchCode(lit,code1,0) ||
1335 matchCode(lit,code2,0)) {
1336 #if SHOW_FOUND
1337 cout << "Alternative: " << lit->toString() << "\n";
1338 #endif
1339 return true;
1340 }
1341 return false;
1342 } // TheoryFinder::matchAlternative(const Literal* lit)
1343
1344 /**
1345 * Match atom against the right absorption axiom *(x,+(x,y)) = x.
1346 *
1347 * @since 17/06/2005 Manchester
1348 */
matchAbsorption(const Literal * lit)1349 bool TheoryFinder::matchAbsorption(const Literal* lit)
1350 {
1351 CALL("TheoryFinder::matchAbsorption");
1352
1353 static const unsigned char code[] =
1354 {EQL, // =
1355 NEWFUN1,0,2,NEWVAR,0,NEWFUN,1,2,OLDVAR,0,NEWVAR,1, // *(x0,+(x0,x1))
1356 OLDVAR1,0,END}; // x0
1357
1358 if (matchCode(lit,code,0)) {
1359 #if SHOW_FOUND
1360 cout << "Absorption: " << lit->toString() << "\n";
1361 #endif
1362 return true;
1363 }
1364 return false;
1365 } // TheoryFinder::matchAbsorption(const Literal* lit)
1366
1367 /**
1368 * Match atom against the S-combinator axiom
1369 * _(_(_(S,x),y),z) = _(_(x,z),_(y,z)).
1370 *
1371 * @since 18/06/2005 Manchester
1372 */
matchCombinatorS(const Literal * lit)1373 bool TheoryFinder::matchCombinatorS(const Literal* lit)
1374 {
1375 CALL("TheoryFinder::matchCombinatorS");
1376
1377 static const unsigned char code[] =
1378 {EQL, // =
1379 NEWFUN1,0,2,OLDFUN,0,OLDFUN,0,NEWFUN,1,0,
1380 NEWVAR,0,NEWVAR,1,NEWVAR,2, // _(_(_(S,x0),x1),x2)
1381 OLDFUN1,0,OLDFUN,0,OLDVAR,0,OLDVAR,2,
1382 OLDFUN,0,OLDVAR,1,OLDVAR,2,END}; // _(_(x0,x2),_(x1,x2))
1383
1384 if (matchCode(lit,code,Property::PR_COMBINATOR)) {
1385 #if SHOW_FOUND
1386 cout << "S: " << lit->toString() << "\n";
1387 #endif
1388 return true;
1389 }
1390 return false;
1391 } // TheoryFinder::matchCombinatorS
1392
1393 /**
1394 * Match atom against the B-combinator axiom
1395 * ._(_(_(B,x),y),z) = _(x,_(y,z)).
1396 *
1397 * @since 18/06/2005 Manchester
1398 */
matchCombinatorB(const Literal * lit)1399 bool TheoryFinder::matchCombinatorB(const Literal* lit)
1400 {
1401 CALL("TheoryFinder::matchCombinatorB");
1402
1403 static const unsigned char code[] =
1404 {EQL, // =
1405 NEWFUN1,0,2,OLDFUN,0,OLDFUN,0,NEWFUN,1,0,
1406 NEWVAR,0,NEWVAR,1,NEWVAR,2, // _(_(_(B,x0),x1),x2)
1407 OLDFUN1,0,OLDVAR,0,OLDFUN,0,OLDVAR,1,OLDVAR,2,END}; // _(x0,_(x1,x2))
1408
1409 if (matchCode(lit,code,Property::PR_COMBINATOR_B)) {
1410 #if SHOW_FOUND
1411 cout << "B: " << lit->toString() << "\n";
1412 #endif
1413 return true;
1414 }
1415 return false;
1416 } // TheoryFinder::matchCombinatorB
1417
1418 /**
1419 * Match atom against the T-combinator axiom
1420 * _(_(T,x),y) = _(y,x).
1421 *
1422 * @since 18/06/2005 Manchester
1423 */
matchCombinatorT(const Literal * lit)1424 bool TheoryFinder::matchCombinatorT(const Literal* lit)
1425 {
1426 CALL("TheoryFinder::matchCombinatorT");
1427
1428 static const unsigned char code[] =
1429 {EQL, // =
1430 NEWFUN1,0,2,OLDFUN,0,NEWFUN,1,0,NEWVAR,0,NEWVAR,1, // _(_(T,x0),x1)
1431 OLDFUN1,0,OLDVAR,1,OLDVAR,0,END}; // _(x1,x0)
1432
1433 if (matchCode(lit,code,Property::PR_COMBINATOR)) {
1434 #if SHOW_FOUND
1435 cout << "T: " << lit->toString() << "\n";
1436 #endif
1437 return true;
1438 }
1439 return false;
1440 } // TheoryFinder::matchCombinatorT
1441
1442 /**
1443 * Match atom against the O-combinator axiom
1444 * _(_(O,x),y) = _(y,_(x,y)).
1445 *
1446 * @since 18/06/2005 Manchester
1447 */
matchCombinatorO(const Literal * lit)1448 bool TheoryFinder::matchCombinatorO(const Literal* lit)
1449 {
1450 CALL("TheoryFinder::matchCombinatorO");
1451
1452 static const unsigned char code[] =
1453 {EQL, // =
1454 NEWFUN1,0,2,OLDFUN,0,NEWFUN,1,0,NEWVAR,0,NEWVAR,1, // _(_(O,x0),x1)
1455 OLDFUN1,0,OLDVAR,1,OLDFUN,0,OLDVAR,0,OLDVAR,1,END}; // _(x1,_(x0,x1))
1456
1457 if (matchCode(lit,code,Property::PR_COMBINATOR)) {
1458 #if SHOW_FOUND
1459 cout << "O: " << lit->toString() << "\n";
1460 #endif
1461 return true;
1462 }
1463 return false;
1464 } // TheoryFinder::matchCombinatorO
1465
1466 /**
1467 * Match atom against the Q-combinator axiom
1468 * _(_(_(Q,x),y),z) = _(y,_(x,z)).
1469 *
1470 * @since 18/06/2005 Manchester
1471 */
matchCombinatorQ(const Literal * lit)1472 bool TheoryFinder::matchCombinatorQ(const Literal* lit)
1473 {
1474 CALL("TheoryFinder::matchCombinatorQ");
1475
1476 static const unsigned char code[] =
1477 {EQL, // =
1478 NEWFUN1,0,2,OLDFUN,0,OLDFUN,0,NEWFUN,1,0,
1479 NEWVAR,0,NEWVAR,1,NEWVAR,2, // _(_(_(Q,x0),x1),x2)
1480 OLDFUN1,0,OLDVAR,1,OLDFUN,0,OLDVAR,0,OLDVAR,2,END}; // _(x1,_(x0,x2))
1481
1482 if (matchCode(lit,code,Property::PR_COMBINATOR)) {
1483 #if SHOW_FOUND
1484 cout << "Q: " << lit->toString() << "\n";
1485 #endif
1486 return true;
1487 }
1488 return false;
1489 } // TheoryFinder::matchCombinatorQ
1490
1491 /**
1492 * Match atom against all known unit axioms.
1493 *
1494 * @since 17/06/2005 Manchester
1495 */
matchAll(const Literal * lit)1496 bool TheoryFinder::matchAll (const Literal* lit)
1497 {
1498 CALL("TheoryFinder::matchAll(const Literal*)");
1499
1500 if (! lit->isPositive()) {
1501 return false;
1502 }
1503
1504 return matchC(lit) ||
1505 matchA(lit) ||
1506 matchIdempotence(lit) ||
1507 matchLeftInverse(lit) ||
1508 matchLeftIdentity(lit) ||
1509 matchRightInverse(lit) ||
1510 matchRightIdentity(lit) ||
1511 matchLeftDistributivity(lit) ||
1512 matchRightDistributivity(lit) ||
1513 matchAssociator(lit) ||
1514 matchCommutator(lit) ||
1515 matchAlternative(lit) ||
1516 matchAbsorption(lit) ||
1517 matchRobbins(lit) ||
1518 matchCombinatorS(lit) ||
1519 matchCombinatorB(lit) ||
1520 matchCombinatorT(lit) ||
1521 matchCombinatorO(lit) ||
1522 matchCombinatorQ(lit);
1523 } // TheoryFinder::matchAll(const Literal*)
1524
1525 // /**
1526 // * Analyse the clause obtained by refuting _metaTheory.
1527 // * @since 18/06/2005 Manchester
1528 // */
1529 // void TheoryFinder::analyse (const Clause& clause)
1530 // {
1531 // CALL("TheoryFinder::analyse");
1532
1533 // const Term& answer = clause.literals().head().atom().args().head();
1534 // const vstring theory(answer.functor().name());
1535 // if (theory == "group") {
1536 // _property->addProp(Property::PR_GROUP);
1537 // }
1538 // else if (theory == "ring") {
1539 // _property->addProp(Property::PR_RING);
1540 // }
1541 // else if (theory == "robbins_algebra") {
1542 // _property->addProp(Property::PR_ROBBINS_ALGEBRA);
1543 // }
1544 // else if (theory == "non_associative_ring") {
1545 // _property->addProp(Property::PR_NA_RING);
1546 // }
1547 // else if (theory == "boolean_algebra") {
1548 // _property->addProp(Property::PR_BOOLEAN_ALGEBRA);
1549 // }
1550 // else if (theory == "lattice") {
1551 // _property->addProp(Property::PR_LATTICE);
1552 // }
1553 // else if (theory == "lattice_ordered_group") {
1554 // _property->addProp(Property::PR_LO_GROUP);
1555 // }
1556 // #if DEBUG_THEORY_FINDER
1557 // cout << "THEORY FOUND: " << theory << "\n";
1558 // #endif
1559 // } // TheoryFinder::analyse
1560
1561 /**
1562 * Returns true iff @c c matches the pattern of a known extensionality clause.
1563 * At the moment this includes the standard and subset-based formulations of the
1564 * set extensionality axiom, as well as the array extensionality axiom.
1565 *
1566 * All patterns must have exactly one equality among variables.
1567 *
1568 * f(X,Y) ∉ X v f(X,Y) ∉ Y v X=Y
1569 * X ⊊ Y v Y ⊊ X v X=Y
1570 * X[sk(X,Y)] ≠ Y[sk(X,Y)] v X=Y
1571 */
matchKnownExtensionality(const Clause * c)1572 bool TheoryFinder::matchKnownExtensionality(const Clause* c) {
1573 static const unsigned char setCode[] =
1574 {CLS,
1575 NLIT,0,
1576 NEWPRED,0,2, // ~member(f(X,Y),X),
1577 NEWFUN,0,2,NEWVAR,0,NEWVAR,1,OLDVAR,0,
1578 NLIT,1,
1579 OLDPRED,0, // ~member(f(X,Y),Y),
1580 OLDFUN,0,OLDVAR,0,OLDVAR,1,OLDVAR,1,
1581 PLIT,2,
1582 EQL,OLDVAR1,0,OLDVAR1,1,END}; // X=Y
1583 static const unsigned char arrayCode[] =
1584 {CLS,
1585 NLIT,0,
1586 EQL,
1587 NEWFUN1,0,2,NEWVAR,0,NEWFUN,1,2,OLDVAR,0,NEWVAR,1, // sel(X,sk(X,Y) != sel(Y,sk(X,Y)),
1588 OLDFUN1,0 ,OLDVAR,1,OLDFUN,1 ,OLDVAR,0,OLDVAR,1,
1589 PLIT,1,
1590 EQL,OLDVAR1,0,OLDVAR1,1,END}; // X=Y
1591 static const unsigned char subsetCode[] =
1592 {CLS,
1593 NLIT,0,
1594 NEWPRED,0,2,NEWVAR,0,NEWVAR,1, // ~subseteq(X,Y),
1595 NLIT,1,
1596 OLDPRED,0, OLDVAR,1,OLDVAR,0, // ~subseteq(Y,X),
1597 PLIT,2,
1598 EQL,OLDVAR1,0,OLDVAR1,1,END}; // X=Y
1599
1600 switch (c->length()) {
1601 case 2:
1602 return matchCode(c, arrayCode);
1603 case 3:
1604 return (matchCode(c, setCode) || matchCode(c, subsetCode));
1605 default:
1606 return false;
1607 }
1608 } // matchKnownExtensionality
1609
1610