1
2 /*
3 * File InferenceStore.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 InferenceStore.cpp
21 * Implements class InferenceStore.
22 */
23
24 #include "Lib/Allocator.hpp"
25 #include "Lib/DHSet.hpp"
26 #include "Lib/Environment.hpp"
27 #include "Lib/Int.hpp"
28 #include "Lib/ScopedPtr.hpp"
29 #include "Lib/SharedSet.hpp"
30 #include "Lib/Stack.hpp"
31 #include "Lib/StringUtils.hpp"
32 #include "Lib/ScopedPtr.hpp"
33 #include "Lib/Sort.hpp"
34
35 #include "Shell/LaTeX.hpp"
36 #include "Shell/Options.hpp"
37 #include "Shell/Statistics.hpp"
38 #include "Shell/UIHelper.hpp"
39
40 #include "Parse/TPTP.hpp"
41
42 #include "Saturation/Splitter.hpp"
43
44 #include "Signature.hpp"
45 #include "Clause.hpp"
46 #include "Formula.hpp"
47 #include "FormulaUnit.hpp"
48 #include "FormulaVarIterator.hpp"
49 #include "Inference.hpp"
50 #include "Term.hpp"
51 #include "TermIterators.hpp"
52 #include "SortHelper.hpp"
53
54 #include "InferenceStore.hpp"
55
56 //TODO: when we delete clause, we should also delete all its records from the inference store
57
58 namespace Kernel
59 {
60
61 using namespace std;
62 using namespace Lib;
63 using namespace Shell;
64
increasePremiseRefCounters()65 void InferenceStore::FullInference::increasePremiseRefCounters()
66 {
67 CALL("InferenceStore::FullInference::increasePremiseRefCounters");
68
69 for(unsigned i=0;i<premCnt;i++) {
70 if (premises[i]->isClause()) {
71 premises[i]->incRefCnt();
72 }
73 }
74 }
75
76
77
InferenceStore()78 InferenceStore::InferenceStore()
79 {
80 }
81
getUnitIdStr(Unit * cs)82 vstring InferenceStore::getUnitIdStr(Unit* cs)
83 {
84 CALL("InferenceStore::getUnitIdStr");
85
86 if (!cs->isClause()) {
87 return Int::toString(cs->number());
88 }
89 return Int::toString(cs->number());
90 }
91
92 /**
93 * Records informations needed for outputting proofs of general splitting
94 */
recordSplittingNameLiteral(Unit * us,Literal * lit)95 void InferenceStore::recordSplittingNameLiteral(Unit* us, Literal* lit)
96 {
97 CALL("InferenceStore::recordSplittingNameLiteral");
98
99 //each clause is result of a splitting only once
100 ALWAYS(_splittingNameLiterals.insert(us, lit));
101 }
102
103
104 /**
105 * Record the introduction of a new symbol
106 */
recordIntroducedSymbol(Unit * u,bool func,unsigned number)107 void InferenceStore::recordIntroducedSymbol(Unit* u, bool func, unsigned number)
108 {
109 CALL("InferenceStore::recordIntroducedSymbol");
110
111 SymbolStack* pStack;
112 _introducedSymbols.getValuePtr(u->number(),pStack);
113 pStack->push(SymbolId(func,number));
114 }
115
116 /**
117 * Record the introduction of a split name
118 */
recordIntroducedSplitName(Unit * u,vstring name)119 void InferenceStore::recordIntroducedSplitName(Unit* u, vstring name)
120 {
121 CALL("InferenceStore::recordIntroducedSplitName");
122 ALWAYS(_introducedSplitNames.insert(u->number(),name));
123 }
124
125 /**
126 * Get the parents of unit represented by us and fill in the rule used to generate this unit
127 *
128 * This will first check if the unit was generated by a special inference that was
129 * recorded in the InferenceStore and if not, use the inference stored in the unit itself
130 */
getParents(Unit * us,InferenceRule & rule)131 UnitIterator InferenceStore::getParents(Unit* us, InferenceRule& rule)
132 {
133 CALL("InferenceStore::getParents/2");
134 ASS_NEQ(us,0);
135
136 // The unit itself stores the inference
137 UnitList* res = 0;
138 Inference& inf = us->inference();
139
140 // opportunity to shrink the premise list
141 // (currently applies if this was a SAT-based inference
142 // and the solver didn't provide a proper proof nor a core)
143 inf.minimizePremises();
144
145 Inference::Iterator iit = inf.iterator();
146 while(inf.hasNext(iit)) {
147 Unit* premUnit = inf.next(iit);
148 UnitList::push(premUnit, res);
149 }
150 rule = inf.rule();
151 res = UnitList::reverse(res); //we want items in the same order
152 return pvi(UnitList::DestructiveIterator(res));
153 }
154
155 /**
156 * Get parents where we do not care about the generating rule
157 */
getParents(Unit * us)158 UnitIterator InferenceStore::getParents(Unit* us)
159 {
160 CALL("InferenceStore::getParents/1");
161
162 InferenceRule aux;
163 return getParents(us, aux);
164 }
165
166 /**
167 * Return @b inner quantified over variables in @b vars
168 *
169 * It is caller's responsibility to ensure that variables in @b vars are unique.
170 */
171 template<typename VarContainer>
getQuantifiedStr(const VarContainer & vars,vstring inner,DHMap<unsigned,unsigned> & t_map,bool innerParentheses=true)172 vstring getQuantifiedStr(const VarContainer& vars, vstring inner, DHMap<unsigned,unsigned>& t_map, bool innerParentheses=true){
173 CALL("getQuantifiedStr(VarContainer, vstring, map)");
174
175 VirtualIterator<unsigned> vit=pvi( getContentIterator(vars) );
176 vstring varStr;
177 bool first=true;
178 while(vit.hasNext()) {
179 unsigned var =vit.next();
180 if (!first) {
181 varStr+=",";
182 }
183 vstring ty="";
184 unsigned t;
185 if(t_map.find(var,t) && t!=Sorts::SRT_DEFAULT){
186 //TODO should assert that we are in tff mode here
187 ty=":" + env.sorts->sortName(t);
188 }
189 varStr+=vstring("X")+Int::toString(var)+ty;
190 first=false;
191 }
192
193 if (first) {
194 //we didn't quantify any variable
195 return inner;
196 }
197
198 if (innerParentheses) {
199 return "( ! ["+varStr+"] : ("+inner+") )";
200 }
201 else {
202 return "( ! ["+varStr+"] : "+inner+" )";
203 }
204 }
205
206 /**
207 * Return @b inner quentified over variables in @b vars
208 *
209 * It is caller's responsibility to ensure that variables in @b vars are unique.
210 */
211 template<typename VarContainer>
getQuantifiedStr(const VarContainer & vars,vstring inner,bool innerParentheses=true)212 vstring getQuantifiedStr(const VarContainer& vars, vstring inner, bool innerParentheses=true)
213 {
214 CALL("getQuantifiedStr(VarContainer, vstring)");
215 static DHMap<unsigned,unsigned> d;
216 return getQuantifiedStr(vars,inner,d,innerParentheses);
217 }
218
219 /**
220 * Return vstring containing quantified unit @b u.
221 */
getQuantifiedStr(Unit * u,List<unsigned> * nonQuantified=0)222 vstring getQuantifiedStr(Unit* u, List<unsigned>* nonQuantified=0)
223 {
224 CALL("getQuantifiedStr(Unit*...)");
225
226 Set<unsigned> vars;
227 vstring res;
228 DHMap<unsigned,unsigned> t_map;
229 SortHelper::collectVariableSorts(u,t_map);
230 if (u->isClause()) {
231 Clause* cl=static_cast<Clause*>(u);
232 unsigned clen=cl->length();
233 for(unsigned i=0;i<clen;i++) {
234 TermVarIterator vit( (*cl)[i] );
235 while(vit.hasNext()) {
236 unsigned var=vit.next();
237 if (List<unsigned>::member(var, nonQuantified)) {
238 continue;
239 }
240 vars.insert(var);
241 }
242 }
243 res=cl->literalsOnlyToString();
244 } else {
245 Formula* formula=static_cast<FormulaUnit*>(u)->formula();
246 FormulaVarIterator fvit( formula );
247 while(fvit.hasNext()) {
248 unsigned var=fvit.next();
249 if (List<unsigned>::member(var, nonQuantified)) {
250 continue;
251 }
252 vars.insert(var);
253 }
254 res=formula->toString();
255 }
256
257 return getQuantifiedStr(vars, res, t_map);
258 }
259
260 struct UnitNumberComparator
261 {
compareKernel::UnitNumberComparator262 static Comparison compare(Unit* u1, Unit* u2)
263 {
264 return Int::compare(u1->number(), u2->number());
265 }
266 };
267
268 struct InferenceStore::ProofPrinter
269 {
270 CLASS_NAME(InferenceStore::ProofPrinter);
271 USE_ALLOCATOR(InferenceStore::ProofPrinter);
272
ProofPrinterKernel::InferenceStore::ProofPrinter273 ProofPrinter(ostream& out, InferenceStore* is)
274 : _is(is), out(out)
275 {
276 CALL("InferenceStore::ProofPrinter::ProofPrinter");
277
278 outputAxiomNames=env.options->outputAxiomNames();
279 delayPrinting=true;
280 proofExtra=env.options->proofExtra()!=Options::ProofExtra::OFF;
281 }
282
scheduleForPrintingKernel::InferenceStore::ProofPrinter283 void scheduleForPrinting(Unit* us)
284 {
285 CALL("InferenceStore::ProofPrinter::scheduleForPrinting");
286
287 outKernel.push(us);
288 handledKernel.insert(us);
289 }
290
~ProofPrinterKernel::InferenceStore::ProofPrinter291 virtual ~ProofPrinter() {}
292
printKernel::InferenceStore::ProofPrinter293 virtual void print()
294 {
295 CALL("InferenceStore::ProofPrinter::print");
296
297 while(outKernel.isNonEmpty()) {
298 Unit* cs=outKernel.pop();
299 handleStep(cs);
300 }
301 if(delayPrinting) printDelayed();
302 }
303
304 protected:
305
hideProofStepKernel::InferenceStore::ProofPrinter306 virtual bool hideProofStep(InferenceRule rule)
307 {
308 return false;
309 }
310
requestProofStepKernel::InferenceStore::ProofPrinter311 void requestProofStep(Unit* prem)
312 {
313 if (!handledKernel.contains(prem)) {
314 handledKernel.insert(prem);
315 outKernel.push(prem);
316 }
317 }
318
printStepKernel::InferenceStore::ProofPrinter319 virtual void printStep(Unit* cs)
320 {
321 CALL("InferenceStore::ProofPrinter::printStep");
322
323 InferenceRule rule;
324 UnitIterator parents=_is->getParents(cs, rule);
325
326 cs->inference().updateStatistics(); // in particular, update inductionDepth (which could have decreased, since we might have fewer parents after miniminization)
327
328 if((rule == InferenceRule::INDUCTION_AXIOM) || (rule == InferenceRule::GEN_INDUCTION_AXIOM)){
329 env.statistics->inductionInProof++;
330 if (rule == InferenceRule::GEN_INDUCTION_AXIOM) {
331 env.statistics->generalizedInductionInProof++;
332 }
333 }
334
335 if (cs->isClause()) {
336 Clause* cl=cs->asClause();
337 out << cl->toString() << vstring("\n");
338 }
339 else {
340 out << _is->getUnitIdStr(cs) << ". ";
341 FormulaUnit* fu=static_cast<FormulaUnit*>(cs);
342 if (env.colorUsed && fu->inheritedColor() != COLOR_INVALID) {
343 out << " IC" << fu->inheritedColor() << " ";
344 }
345 out << fu->formula()->toString() << ' ';
346
347 out <<"["<<Kernel::ruleName(rule);
348
349 if (outputAxiomNames && rule==InferenceRule::INPUT) {
350 ASS(!parents.hasNext()); //input clauses don't have parents
351 vstring name;
352 if (Parse::TPTP::findAxiomName(cs, name)) {
353 out << " " << name;
354 }
355 }
356
357 bool first=true;
358 while(parents.hasNext()) {
359 Unit* prem=parents.next();
360 out << (first ? ' ' : ',');
361 out << _is->getUnitIdStr(prem);
362 first=false;
363 }
364
365 // print Extra
366 vstring extra;
367 if (env.proofExtra && env.proofExtra->find(cs,extra) && extra != "") {
368 out << ", " << extra;
369 }
370 out << "]" << endl;
371 }
372 }
373
handleStepKernel::InferenceStore::ProofPrinter374 void handleStep(Unit* cs)
375 {
376 CALL("InferenceStore::ProofPrinter::handleStep");
377 InferenceRule rule;
378 UnitIterator parents=_is->getParents(cs, rule);
379
380 while(parents.hasNext()) {
381 Unit* prem=parents.next();
382 ASS(prem!=cs);
383 requestProofStep(prem);
384 }
385
386 if (!hideProofStep(rule)) {
387 if(delayPrinting) delayed.push(cs);
388 else printStep(cs);
389 }
390 }
391
printDelayedKernel::InferenceStore::ProofPrinter392 void printDelayed()
393 {
394 CALL("InferenceStore::ProofPrinter::printDelayed");
395
396 // Sort
397 sort<UnitNumberComparator>(delayed.begin(),delayed.end());
398
399 // Print
400 for(unsigned i=0;i<delayed.size();i++){
401 printStep(delayed[i]);
402 }
403
404 }
405
406
407
408 Stack<Unit*> outKernel;
409 Set<Unit*> handledKernel; // use UnitSpec to provide its own hash and equals
410 Stack<Unit*> delayed;
411
412 InferenceStore* _is;
413 ostream& out;
414
415 bool outputAxiomNames;
416 bool delayPrinting;
417 bool proofExtra;
418 };
419
420 struct InferenceStore::ProofPropertyPrinter
421 : public InferenceStore::ProofPrinter
422 {
423 CLASS_NAME(InferenceStore::ProofPropertyPrinter);
424 USE_ALLOCATOR(InferenceStore::ProofPropertyPrinter);
425
ProofPropertyPrinterKernel::InferenceStore::ProofPropertyPrinter426 ProofPropertyPrinter(ostream& out, InferenceStore* is) : ProofPrinter(out,is)
427 {
428 CALL("InferenceStore::ProofPropertyPrinter::ProofPropertyPrinter");
429
430 max_theory_clause_depth = 0;
431 for(unsigned i=0;i<11;i++){ buckets.push(0); }
432 last_one = false;
433 }
434
printKernel::InferenceStore::ProofPropertyPrinter435 void print()
436 {
437 ProofPrinter::print();
438 for(unsigned i=0;i<11;i++){ out << buckets[i] << " ";}
439 out << endl;
440 if(last_one){ out << "yes" << endl; }
441 else{ out << "no" << endl; }
442 }
443
444 protected:
445
printStepKernel::InferenceStore::ProofPropertyPrinter446 void printStep(Unit* us)
447 {
448 static unsigned lastP = Unit::getLastParsingNumber();
449 static float chunk = lastP / 10.0;
450 if(us->number() <= lastP){
451 if(us->number() == lastP){
452 last_one = true;
453 }
454 unsigned bucket = (unsigned)(us->number() / chunk);
455 buckets[bucket]++;
456 }
457
458 // TODO we could make clauses track this information, but I am not sure that that's worth it
459 if(us->isClause() && us->isPureTheoryDescendant()){
460 //cout << "HERE with " << us->toString() << endl;
461 Inference* inf = &us->inference();
462 while(inf->rule() == InferenceRule::EVALUATION){
463 Inference::Iterator piit = inf->iterator();
464 inf = &inf->next(piit)->inference();
465 }
466 Stack<Inference*> current;
467 current.push(inf);
468 unsigned level = 0;
469 while(!current.isEmpty()){
470 //cout << current.size() << endl;
471 Stack<Inference*> next;
472 Stack<Inference*>::Iterator it(current);
473 while(it.hasNext()){
474 Inference* inf = it.next();
475 Inference::Iterator iit=inf->iterator();
476 while(inf->hasNext(iit)) {
477 Unit* premUnit=inf->next(iit);
478 Inference* premInf = &premUnit->inference();
479 while(premInf->rule() == InferenceRule::EVALUATION){
480 Inference::Iterator piit = premInf->iterator();
481 premUnit = premInf->next(piit);
482 premInf = &premUnit->inference();
483 }
484
485 //for(unsigned i=0;i<level;i++){ cout << ">";}; cout << premUnit->toString() << endl;
486 next.push(premInf);
487 }
488 }
489 level++;
490 current = next;
491 }
492 level--;
493 //cout << "level is " << level << endl;
494
495 if(level > max_theory_clause_depth){
496 max_theory_clause_depth=level;
497 }
498 }
499 }
500
501 unsigned max_theory_clause_depth;
502 bool last_one;
503 Stack<unsigned> buckets;
504
505 };
506
507
508 struct InferenceStore::TPTPProofPrinter
509 : public InferenceStore::ProofPrinter
510 {
511 CLASS_NAME(InferenceStore::TPTPProofPrinter);
512 USE_ALLOCATOR(InferenceStore::TPTPProofPrinter);
513
TPTPProofPrinterKernel::InferenceStore::TPTPProofPrinter514 TPTPProofPrinter(ostream& out, InferenceStore* is)
515 : ProofPrinter(out, is) {
516 splitPrefix = Saturation::Splitter::splPrefix;
517 // Don't delay printing in TPTP proof mode
518 delayPrinting = false;
519 }
520
printKernel::InferenceStore::TPTPProofPrinter521 void print()
522 {
523 UIHelper::outputSortDeclarations(env.out());
524 UIHelper::outputSymbolDeclarations(env.out());
525 ProofPrinter::print();
526 }
527
528 protected:
529 vstring splitPrefix;
530
getRoleKernel::InferenceStore::TPTPProofPrinter531 vstring getRole(InferenceRule rule, UnitInputType origin)
532 {
533 switch(rule) {
534 case InferenceRule::INPUT:
535 if (origin==UnitInputType::CONJECTURE) {
536 return "conjecture";
537 }
538 else {
539 return "axiom";
540 }
541 case InferenceRule::NEGATED_CONJECTURE:
542 return "negated_conjecture";
543 default:
544 return "plain";
545 }
546 }
547
tptpRuleNameKernel::InferenceStore::TPTPProofPrinter548 vstring tptpRuleName(InferenceRule rule)
549 {
550 return StringUtils::replaceChar(ruleName(rule), ' ', '_');
551 }
552
unitIdToTptpKernel::InferenceStore::TPTPProofPrinter553 vstring unitIdToTptp(vstring unitId)
554 {
555 return "f"+unitId;
556 }
557
tptpUnitIdKernel::InferenceStore::TPTPProofPrinter558 vstring tptpUnitId(Unit* us)
559 {
560 return unitIdToTptp(_is->getUnitIdStr(us));
561 }
562
tptpDefIdKernel::InferenceStore::TPTPProofPrinter563 vstring tptpDefId(Unit* us)
564 {
565 return unitIdToTptp(Int::toString(us->number())+"_D");
566 }
567
splitsToStringKernel::InferenceStore::TPTPProofPrinter568 vstring splitsToString(SplitSet* splits)
569 {
570 CALL("InferenceStore::TPTPProofPrinter::splitsToString");
571 ASS_G(splits->size(),0);
572
573 if (splits->size()==1) {
574 return Saturation::Splitter::getFormulaStringFromName(splits->sval(),true /*negated*/);
575 }
576 SplitSet::Iterator sit(*splits);
577 vstring res("(");
578 while(sit.hasNext()) {
579 res+= Saturation::Splitter::getFormulaStringFromName(sit.next(),true /*negated*/);
580 if (sit.hasNext()) {
581 res+=" | ";
582 }
583 }
584 res+=")";
585 return res;
586 }
587
quoteAxiomNameKernel::InferenceStore::TPTPProofPrinter588 vstring quoteAxiomName(vstring n)
589 {
590 CALL("InferenceStore::TPTPProofPrinter::quoteAxiomName");
591
592 static vstring allowedFirst("0123456789abcdefghijklmnopqrstuvwxyz");
593 const char* allowed="_ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789abcdefghijklmnopqrstuvwxyz";
594
595 if (n.size()==0 || allowedFirst.find(n[0])==vstring::npos ||
596 n.find_first_not_of(allowed)!=vstring::npos) {
597 n='\''+n+'\'';
598 }
599 return n;
600 }
601
getFofStringKernel::InferenceStore::TPTPProofPrinter602 vstring getFofString(vstring id, vstring formula, vstring inference, InferenceRule rule, UnitInputType origin=UnitInputType::AXIOM)
603 {
604 CALL("InferenceStore::TPTPProofPrinter::getFofString");
605
606 vstring kind = "fof";
607 if(env.statistics->hasTypes){ kind="tff"; }
608
609 return kind+"("+id+","+getRole(rule,origin)+",("+"\n"
610 +" "+formula+"),\n"
611 +" "+inference+").";
612 }
613
getFormulaStringKernel::InferenceStore::TPTPProofPrinter614 vstring getFormulaString(Unit* us)
615 {
616 CALL("InferenceStore::TPTPProofPrinter::getFormulaString");
617
618 vstring formulaStr;
619 if (us->isClause()) {
620 Clause* cl=us->asClause();
621 formulaStr=getQuantifiedStr(cl);
622 if (cl->splits() && !cl->splits()->isEmpty()) {
623 formulaStr+=" | "+splitsToString(cl->splits());
624 }
625 }
626 else {
627 FormulaUnit* fu=static_cast<FormulaUnit*>(us);
628 formulaStr=getQuantifiedStr(fu);
629 }
630 return formulaStr;
631 }
632
hasNewSymbolsKernel::InferenceStore::TPTPProofPrinter633 bool hasNewSymbols(Unit* u) {
634 CALL("InferenceStore::TPTPProofPrinter::hasNewSymbols");
635 bool res = _is->_introducedSymbols.find(u->number());
636 ASS(!res || _is->_introducedSymbols.get(u->number()).isNonEmpty());
637 if(!res){
638 res = _is->_introducedSplitNames.find(u->number());
639 }
640 return res;
641 }
getNewSymbolsKernel::InferenceStore::TPTPProofPrinter642 vstring getNewSymbols(vstring origin, vstring symStr) {
643 CALL("InferenceStore::TPTPProofPrinter::getNewSymbols(vstring,vstring)");
644 return "new_symbols(" + origin + ",[" +symStr + "])";
645 }
646 /** It is an iterator over SymbolId */
647 template<class It>
getNewSymbolsKernel::InferenceStore::TPTPProofPrinter648 vstring getNewSymbols(vstring origin, It symIt) {
649 CALL("InferenceStore::TPTPProofPrinter::getNewSymbols(vstring,It)");
650
651 vostringstream symsStr;
652 while(symIt.hasNext()) {
653 SymbolId sym = symIt.next();
654 if (sym.first) {
655 symsStr << env.signature->functionName(sym.second);
656 }
657 else {
658 symsStr << env.signature->predicateName(sym.second);
659 }
660 if (symIt.hasNext()) {
661 symsStr << ',';
662 }
663 }
664 return getNewSymbols(origin, symsStr.str());
665 }
getNewSymbolsKernel::InferenceStore::TPTPProofPrinter666 vstring getNewSymbols(vstring origin, Unit* u) {
667 CALL("InferenceStore::TPTPProofPrinter::getNewSymbols(vstring,Unit*)");
668 ASS(hasNewSymbols(u));
669
670 if(_is->_introducedSplitNames.find(u->number())){
671 return getNewSymbols(origin,_is->_introducedSplitNames.get(u->number()));
672 }
673
674 SymbolStack& syms = _is->_introducedSymbols.get(u->number());
675 return getNewSymbols(origin, SymbolStack::ConstIterator(syms));
676 }
677
printStepKernel::InferenceStore::TPTPProofPrinter678 void printStep(Unit* us)
679 {
680 CALL("InferenceStore::TPTPProofPrinter::printStep");
681
682 InferenceRule rule;
683 UnitIterator parents=_is->getParents(us, rule);
684
685 switch(rule) {
686 //case Inference::AVATAR_COMPONENT:
687 // printSplittingComponentIntroduction(us);
688 // return;
689 case InferenceRule::GENERAL_SPLITTING_COMPONENT:
690 printGeneralSplittingComponent(us);
691 return;
692 case InferenceRule::GENERAL_SPLITTING:
693 printSplitting(us);
694 return;
695 default: ;
696 }
697
698
699 //get vstring representing the formula
700
701 vstring formulaStr=getFormulaString(us);
702
703 //get inference vstring
704
705 vstring inferenceStr;
706 if (rule==InferenceRule::INPUT) {
707 vstring fileName;
708 if (env.options->inputFile()=="") {
709 fileName="unknown";
710 }
711 else {
712 fileName="'"+env.options->inputFile()+"'";
713 }
714 vstring axiomName;
715 if (!outputAxiomNames || !Parse::TPTP::findAxiomName(us, axiomName)) {
716 axiomName="unknown";
717 }
718 inferenceStr="file("+fileName+","+quoteAxiomName(axiomName)+")";
719 }
720 else if (!parents.hasNext()) {
721 vstring newSymbolInfo;
722 if (hasNewSymbols(us)) {
723 newSymbolInfo = getNewSymbols("naming",us);
724 }
725 inferenceStr="introduced("+tptpRuleName(rule)+",["+newSymbolInfo+"])";
726 }
727 else {
728 ASS(parents.hasNext());
729 vstring statusStr;
730 if (rule==InferenceRule::SKOLEMIZE) {
731 statusStr="status(esa),"+getNewSymbols("skolem",us);
732 }
733
734 inferenceStr="inference("+tptpRuleName(rule);
735
736 inferenceStr+=",["+statusStr+"],[";
737 bool first=true;
738 while(parents.hasNext()) {
739 Unit* prem=parents.next();
740 if (!first) {
741 inferenceStr+=',';
742 }
743 inferenceStr+=tptpUnitId(prem);
744 first=false;
745 }
746 inferenceStr+="])";
747 }
748
749 out<<getFofString(tptpUnitId(us), formulaStr, inferenceStr, rule, us->inputType())<<endl;
750 }
751
printSplittingKernel::InferenceStore::TPTPProofPrinter752 void printSplitting(Unit* us)
753 {
754 CALL("InferenceStore::TPTPProofPrinter::printSplitting");
755 ASS(us->isClause());
756
757 InferenceRule rule;
758 UnitIterator parents=_is->getParents(us, rule);
759 ASS(rule==InferenceRule::GENERAL_SPLITTING);
760
761 vstring inferenceStr="inference("+tptpRuleName(rule)+",[],[";
762
763 //here we rely on the fact that the base premise is always put as the first premise in
764 //GeneralSplitting::apply
765
766 ALWAYS(parents.hasNext());
767 Unit* base=parents.next();
768 inferenceStr+=tptpUnitId(base);
769
770 ASS(parents.hasNext()); //we always split off at least one component
771 while(parents.hasNext()) {
772 Unit* comp=parents.next();
773 ASS(_is->_splittingNameLiterals.find(comp));
774 inferenceStr+=","+tptpDefId(comp);
775 }
776 inferenceStr+="])";
777
778 out<<getFofString(tptpUnitId(us), getFormulaString(us), inferenceStr, rule)<<endl;
779 }
780
printGeneralSplittingComponentKernel::InferenceStore::TPTPProofPrinter781 void printGeneralSplittingComponent(Unit* us)
782 {
783 CALL("InferenceStore::TPTPProofPrinter::printGeneralSplittingComponent");
784 ASS(us->isClause());
785
786 InferenceRule rule;
787 UnitIterator parents=_is->getParents(us, rule);
788 ASS(!parents.hasNext());
789
790 Literal* nameLit=_is->_splittingNameLiterals.get(us); //the name literal must always be stored
791
792 vstring defId=tptpDefId(us);
793
794 out<<getFofString(tptpUnitId(us), getFormulaString(us),
795 "inference("+tptpRuleName(InferenceRule::CLAUSIFY)+",[],["+defId+"])", InferenceRule::CLAUSIFY)<<endl;
796
797
798 List<unsigned>* nameVars=0;
799 VariableIterator vit(nameLit);
800 while(vit.hasNext()) {
801 unsigned var=vit.next().var();
802 ASS(!List<unsigned>::member(var, nameVars)); //each variable appears only once in the naming literal
803 List<unsigned>::push(var,nameVars);
804 }
805
806 vstring compStr;
807 List<unsigned>* compOnlyVars=0;
808 Clause::Iterator lits(*us->asClause());
809 bool first=true;
810 bool multiple=false;
811 while(lits.hasNext()) {
812 Literal* lit=lits.next();
813 if (lit==nameLit) {
814 continue;
815 }
816 if (first) {
817 first=false;
818 }
819 else {
820 multiple=true;
821 compStr+=" | ";
822 }
823 compStr+=lit->toString();
824
825 VariableIterator lvit(lit);
826 while(lvit.hasNext()) {
827 unsigned var=lvit.next().var();
828 if (!List<unsigned>::member(var, nameVars) && !List<unsigned>::member(var, compOnlyVars)) {
829 List<unsigned>::push(var,compOnlyVars);
830 }
831 }
832 }
833 ASS(!first);
834
835 compStr=getQuantifiedStr(compOnlyVars, compStr, multiple);
836 List<unsigned>::destroy(compOnlyVars);
837
838 vstring defStr=compStr+" <=> "+Literal::complementaryLiteral(nameLit)->toString();
839 defStr=getQuantifiedStr(nameVars, defStr);
840 List<unsigned>::destroy(nameVars);
841
842 SymbolId nameSymbol = SymbolId(false,nameLit->functor());
843 vostringstream originStm;
844 originStm << "introduced(" << tptpRuleName(rule)
845 << ",[" << getNewSymbols("naming",getSingletonIterator(nameSymbol))
846 << "])";
847
848 out<<getFofString(defId, defStr, originStm.str(), rule)<<endl;
849 }
850
printSplittingComponentIntroductionKernel::InferenceStore::TPTPProofPrinter851 void printSplittingComponentIntroduction(Unit* us)
852 {
853 CALL("InferenceStore::TPTPProofPrinter::printSplittingComponentIntroduction");
854 ASS(us->isClause());
855
856 Clause* cl=us->asClause();
857 ASS(cl->splits());
858 ASS_EQ(cl->splits()->size(),1);
859
860 InferenceRule rule=InferenceRule::AVATAR_COMPONENT;
861
862 vstring defId=tptpDefId(us);
863 vstring splitPred = splitsToString(cl->splits());
864 vstring defStr=getQuantifiedStr(cl)+" <=> ~"+splitPred;
865
866 out<<getFofString(tptpUnitId(us), getFormulaString(us),
867 "inference("+tptpRuleName(InferenceRule::CLAUSIFY)+",[],["+defId+"])", InferenceRule::CLAUSIFY)<<endl;
868
869 vstringstream originStm;
870 originStm << "introduced(" << tptpRuleName(rule)
871 << ",[" << getNewSymbols("naming",splitPred)
872 << "])";
873
874 out<<getFofString(defId, defStr, originStm.str(), rule)<<endl;
875 }
876
877 };
878
879 struct InferenceStore::ProofCheckPrinter
880 : public InferenceStore::ProofPrinter
881 {
882 CLASS_NAME(InferenceStore::ProofCheckPrinter);
883 USE_ALLOCATOR(InferenceStore::ProofCheckPrinter);
884
ProofCheckPrinterKernel::InferenceStore::ProofCheckPrinter885 ProofCheckPrinter(ostream& out, InferenceStore* is)
886 : ProofPrinter(out, is) {}
887
888 protected:
printStepKernel::InferenceStore::ProofCheckPrinter889 void printStep(Unit* cs)
890 {
891 CALL("InferenceStore::ProofCheckPrinter::printStep");
892 InferenceRule rule;
893 UnitIterator parents=_is->getParents(cs, rule);
894
895 UIHelper::outputSortDeclarations(out);
896 UIHelper::outputSymbolDeclarations(out);
897
898 vstring kind = "fof";
899 if(env.statistics->hasTypes){ kind="tff"; }
900
901 out << kind
902 << "(r"<<_is->getUnitIdStr(cs)
903 << ",conjecture, "
904 << getQuantifiedStr(cs)
905 << " ). %"<<ruleName(rule)<<"\n";
906
907 while(parents.hasNext()) {
908 Unit* prem=parents.next();
909 out << kind
910 << "(pr"<<_is->getUnitIdStr(prem)
911 << ",axiom, "
912 << getQuantifiedStr(prem);
913 out << " ).\n";
914 }
915 out << "%#\n";
916 }
917
918
hideProofStepKernel::InferenceStore::ProofCheckPrinter919 bool hideProofStep(InferenceRule rule)
920 {
921 switch(rule) {
922 case InferenceRule::INPUT:
923 case InferenceRule::INEQUALITY_SPLITTING_NAME_INTRODUCTION:
924 case InferenceRule::INEQUALITY_SPLITTING:
925 case InferenceRule::SKOLEMIZE:
926 case InferenceRule::EQUALITY_PROXY_REPLACEMENT:
927 case InferenceRule::EQUALITY_PROXY_AXIOM1:
928 case InferenceRule::EQUALITY_PROXY_AXIOM2:
929 case InferenceRule::NEGATED_CONJECTURE:
930 case InferenceRule::RECTIFY:
931 case InferenceRule::FLATTEN:
932 case InferenceRule::ENNF:
933 case InferenceRule::NNF:
934 case InferenceRule::CLAUSIFY:
935 case InferenceRule::AVATAR_DEFINITION:
936 case InferenceRule::AVATAR_COMPONENT:
937 case InferenceRule::AVATAR_REFUTATION:
938 case InferenceRule::AVATAR_SPLIT_CLAUSE:
939 case InferenceRule::AVATAR_CONTRADICTION_CLAUSE:
940 case InferenceRule::FOOL_LET_ELIMINATION:
941 case InferenceRule::FOOL_ITE_ELIMINATION:
942 case InferenceRule::FOOL_ELIMINATION:
943 case InferenceRule::BOOLEAN_TERM_ENCODING:
944 case InferenceRule::CHOICE_AXIOM:
945 case InferenceRule::PREDICATE_DEFINITION:
946 return true;
947 default:
948 return false;
949 }
950 }
951
printKernel::InferenceStore::ProofCheckPrinter952 void print()
953 {
954 ProofPrinter::print();
955 out << "%#\n";
956 }
957 };
958
createProofPrinter(ostream & out)959 InferenceStore::ProofPrinter* InferenceStore::createProofPrinter(ostream& out)
960 {
961 CALL("InferenceStore::createProofPrinter");
962
963 switch(env.options->proof()) {
964 case Options::Proof::ON:
965 return new ProofPrinter(out, this);
966 case Options::Proof::PROOFCHECK:
967 return new ProofCheckPrinter(out, this);
968 case Options::Proof::TPTP:
969 return new TPTPProofPrinter(out, this);
970 case Options::Proof::PROPERTY:
971 return new ProofPropertyPrinter(out,this);
972 case Options::Proof::OFF:
973 return 0;
974 }
975 ASSERTION_VIOLATION;
976 return 0;
977 }
978
979 /**
980 * Output a proof of refutation to out
981 *
982 *
983 */
outputProof(ostream & out,Unit * refutation)984 void InferenceStore::outputProof(ostream& out, Unit* refutation)
985 {
986 CALL("InferenceStore::outputProof(ostream&,Unit*)");
987
988 ProofPrinter* p = createProofPrinter(out);
989 if (!p) {
990 return;
991 }
992 ScopedPtr<ProofPrinter> pp(p);
993 pp->scheduleForPrinting(refutation);
994 pp->print();
995 }
996
997 /**
998 * Output a proof of units to out
999 *
1000 */
outputProof(ostream & out,UnitList * units)1001 void InferenceStore::outputProof(ostream& out, UnitList* units)
1002 {
1003 CALL("InferenceStore::outputProof(ostream&,UnitList*)");
1004
1005 ProofPrinter* p = createProofPrinter(out);
1006 if (!p) {
1007 return;
1008 }
1009 ScopedPtr<ProofPrinter> pp(p);
1010 UnitList::Iterator uit(units);
1011 while(uit.hasNext()) {
1012 Unit* u = uit.next();
1013 pp->scheduleForPrinting(u);
1014 }
1015 pp->print();
1016 }
1017
instance()1018 InferenceStore* InferenceStore::instance()
1019 {
1020 static ScopedPtr<InferenceStore> inst(new InferenceStore());
1021
1022 return inst.ptr();
1023 }
1024
1025 }
1026