1
2 /*
3 * File SineUtils.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 SineUtils.cpp
21 * Implements class SineUtils.
22 */
23
24 #include <cmath>
25
26 #include "Lib/Deque.hpp"
27 #include "Lib/DHSet.hpp"
28 #include "Lib/DHMultiset.hpp"
29 #include "Lib/Environment.hpp"
30 #include "Lib/List.hpp"
31 #include "Lib/Metaiterators.hpp"
32 #include "Lib/Set.hpp"
33 #include "Lib/TimeCounter.hpp"
34 #include "Lib/VirtualIterator.hpp"
35
36 #include "Kernel/Clause.hpp"
37 #include "Kernel/FormulaUnit.hpp"
38 #include "Kernel/Problem.hpp"
39 #include "Kernel/Signature.hpp"
40 #include "Kernel/SubformulaIterator.hpp"
41 #include "Kernel/Term.hpp"
42 #include "Kernel/TermIterators.hpp"
43
44 #include "Options.hpp"
45 #include "Statistics.hpp"
46
47 #include "SineUtils.hpp"
48
49 #define SINE_PRINT_SELECTED 0
50
51 namespace Shell
52 {
53
54 using namespace Lib;
55 using namespace Kernel;
56
57 /**
58 * Return @b SymId that is greater than any @b SymId that can come from
59 * the current problem
60 *
61 * The returned value is to be used to determine the size of various
62 * arrays.
63 */
getSymIdBound()64 SineSymbolExtractor::SymId SineSymbolExtractor::getSymIdBound()
65 {
66 return max(env.signature->predicates()*2-1, env.signature->functions()*2);
67 }
68
addSymIds(Term * term,Stack<SymId> & ids)69 void SineSymbolExtractor::addSymIds(Term* term, Stack<SymId>& ids)
70 {
71 CALL("SineSymbolExtractor::addSymIds");
72
73 if (!term->shared()) {
74 if (term->isSpecial()) {
75 Term::SpecialTermData *sd = term->getSpecialData();
76 switch (sd->getType()) {
77 case Term::SF_FORMULA:
78 extractFormulaSymbols(sd->getFormula(), ids);
79 break;
80 case Term::SF_ITE:
81 extractFormulaSymbols(sd->getCondition(), ids);
82 break;
83 case Term::SF_LET:
84 case Term::SF_LET_TUPLE: {
85 TermList binding = sd->getBinding();
86 if (binding.isTerm()) {
87 addSymIds(binding.term(), ids);
88 }
89 break;
90 }
91 case Term::SF_TUPLE: {
92 addSymIds(sd->getTupleTerm(), ids);
93 break;
94 }
95 default:
96 ASSERTION_VIOLATION;
97 }
98 } else {
99 ids.push(term->functor() * 2 + 1);
100 }
101 NonVariableIterator nvi(term);
102 while (nvi.hasNext()) {
103 addSymIds(nvi.next().term(), ids);
104 }
105 } else {
106 ids.push(term->functor() * 2 + 1);
107
108 NonVariableIterator nvi(term);
109 while (nvi.hasNext()) {
110 Term* t = nvi.next().term();
111 ids.push(t->functor() * 2 + 1);
112 }
113 }
114 }
115
116 /**
117 * Add all occurrences of symbol ids of symbols occurring in the the literal to @c ids.
118 * @since 04/05/2013 Manchester, argument polarity removed
119 * @author Andrei Voronkov
120 */
addSymIds(Literal * lit,Stack<SymId> & ids)121 void SineSymbolExtractor::addSymIds(Literal* lit,Stack<SymId>& ids)
122 {
123 CALL("SineSymbolExtractor::addSymIds");
124
125 SymId predId=lit->functor()*2;
126 ids.push(predId);
127
128 if (!lit->shared()) {
129 NonVariableIterator nvi(lit);
130 while (nvi.hasNext()) {
131 addSymIds(nvi.next().term(), ids);
132 }
133 } else {
134 NonVariableIterator nvi(lit);
135 while (nvi.hasNext()) {
136 Term *t = nvi.next().term();
137 SymId funId = t->functor() * 2 + 1;
138 ids.push(funId);
139 }
140 }
141 } // addSymIds
142
decodeSymId(SymId s,bool & pred,unsigned & functor)143 void SineSymbolExtractor::decodeSymId(SymId s, bool& pred, unsigned& functor)
144 {
145 pred = (s%2)==0;
146 functor = s/2;
147 }
148
validSymId(SymId s)149 bool SineSymbolExtractor::validSymId(SymId s)
150 {
151 CALL("SineSymbolExtractor::validSymId");
152
153 bool pred;
154 unsigned functor;
155 decodeSymId(s, pred, functor);
156 if (pred) {
157 if (functor>=static_cast<unsigned>(env.signature->predicates())) {
158 return false;
159 }
160 }
161 else {
162 if (functor>=static_cast<unsigned>(env.signature->functions())) {
163 return false;
164 }
165 }
166 return true;
167 }
168
169 /**
170 * Add all occurrences of symbol ids of symbols occurring in the formula to @c ids.
171 * @since 04/05/2013 Manchester, argument polarity removed, made non-recursive
172 * @author Andrei Voronkov
173 */
extractFormulaSymbols(Formula * f,Stack<SymId> & itms)174 void SineSymbolExtractor::extractFormulaSymbols(Formula* f,Stack<SymId>& itms)
175 {
176 CALL("SineSymbolExtractor::extractFormulaSymbols");
177 Stack<Formula*> fs;
178 fs.push(f);
179 while (!fs.isEmpty()) {
180 Formula* f = fs.pop();
181 switch (f->connective()) {
182 case LITERAL:
183 addSymIds(f->literal(),itms);
184 break;
185 case BOOL_TERM: {
186 TermList ts = f->getBooleanTerm();
187 if (ts.isTerm()) {
188 addSymIds(ts.term(), itms);
189 }
190 break;
191 }
192 case AND:
193 case OR:
194 {
195 FormulaList::Iterator args(f->args());
196 while (args.hasNext()) {
197 fs.push(args.next());
198 }
199 }
200 break;
201 case IMP:
202 case IFF:
203 case XOR:
204 fs.push(f->left());
205 fs.push(f->right());
206 break;
207 case NOT:
208 fs.push(f->uarg());
209 break;
210 case FORALL:
211 case EXISTS:
212 fs.push(f->qarg());
213 break;
214 case TRUE:
215 case FALSE:
216 break;
217 #if VDEBUG
218 default:
219 ASSERTION_VIOLATION;
220 return;
221 #endif
222 }
223 }
224 } // SineSymbolExtractor::extractFormulaSymbols
225
226 /**
227 * Return iterator that yields SymIds of symbols in a unit.
228 * Each SymId is yielded at most once.
229 */
extractSymIds(Unit * u)230 SineSymbolExtractor::SymIdIterator SineSymbolExtractor::extractSymIds(Unit* u)
231 {
232 CALL("SineSymbolExtractor::extractSymIds");
233
234 static Stack<SymId> itms;
235 itms.reset();
236
237 if (u->isClause()) {
238 Clause* cl=static_cast<Clause*>(u);
239 unsigned clen=cl->length();
240 for (unsigned i=0;i<clen;i++) {
241 Literal* lit=(*cl)[i];
242 addSymIds(lit,itms);
243 }
244 } else {
245 FormulaUnit* fu=static_cast<FormulaUnit*>(u);
246 extractFormulaSymbols(fu->formula(),itms);
247 }
248 return pvi( getUniquePersistentIterator(Stack<SymId>::Iterator(itms)) );
249 }
250
initGeneralityFunction(UnitList * units)251 void SineBase::initGeneralityFunction(UnitList* units)
252 {
253 CALL("SineBase::initGeneralityFunction");
254
255 SymId symIdBound=_symExtr.getSymIdBound();
256 _gen.init(symIdBound,0);
257
258 UnitList::Iterator uit(units);
259 while (uit.hasNext()) {
260 Unit* u=uit.next();
261 SymIdIterator sit=_symExtr.extractSymIds(u);
262 while (sit.hasNext()) {
263 SymId sid=sit.next();
264 _gen[sid]++;
265 }
266 }
267 }
268
SineSelector(const Options & opt)269 SineSelector::SineSelector(const Options& opt)
270 : _onIncluded(opt.sineSelection()==Options::SineSelection::INCLUDED),
271 _genThreshold(opt.sineGeneralityThreshold()),
272 _tolerance(opt.sineTolerance()),
273 _depthLimit(opt.sineDepth()),
274 _justForSineLevels(false)
275 {
276 CALL("SineSelector::SineSelector/0");
277
278 init();
279 }
280
SineSelector(bool onIncluded,float tolerance,unsigned depthLimit,unsigned genThreshold,bool justForSineLevels)281 SineSelector::SineSelector(bool onIncluded, float tolerance, unsigned depthLimit, unsigned genThreshold, bool justForSineLevels)
282 : _onIncluded(onIncluded),
283 _genThreshold(genThreshold),
284 _tolerance(tolerance),
285 _depthLimit(depthLimit),
286 _justForSineLevels(justForSineLevels)
287 {
288 CALL("SineSelector::SineSelector/4");
289
290 init();
291 }
292
init()293 void SineSelector::init()
294 {
295 CALL("SineSelector::init");
296 ASS(_tolerance>=1.0f || _tolerance==-1);
297
298 _strict=_tolerance==1.0f;
299 }
300
301 /**
302 * Connect unit @b u with symbols it defines
303 */
updateDefRelation(Unit * u)304 void SineSelector::updateDefRelation(Unit* u)
305 {
306 CALL("SineSelector::updateDefRelation");
307
308 SymIdIterator sit=_symExtr.extractSymIds(u);
309
310 if (!sit.hasNext()) {
311 if(_justForSineLevels){
312 u->inference().setSineLevel(0);
313 //cout << "set level for a non-symboler " << u->toString() << " as " << "(0)" << endl;
314 }
315 _unitsWithoutSymbols.push(u);
316 return;
317 }
318
319 static Stack<SymId> equalGenerality;
320 equalGenerality.reset();
321
322 SymId leastGenSym=sit.next();
323 unsigned leastGenVal=_gen[leastGenSym];
324
325 //it a symbol fits under _genThreshold, add it immediately [into the relation]
326 if (leastGenVal<=_genThreshold) {
327 UnitList::push(u,_def[leastGenSym]);
328 }
329
330 while (sit.hasNext()) {
331 SymId sym=sit.next();
332 unsigned val=_gen[sym];
333 ASS_G(val,0);
334
335 //it a symbol fits under _genThreshold, add it immediately [into the relation]
336 if (val<=_genThreshold) {
337 UnitList::push(u,_def[sym]);
338 }
339
340 if (val<leastGenVal) {
341 leastGenSym=sym;
342 leastGenVal=val;
343 equalGenerality.reset();
344 } else if (val==leastGenVal) {
345 equalGenerality.push(sym);
346 }
347 }
348
349
350 if (_strict) {
351 //only if the least general symbol is over _genThreshold; otherwise it is already added
352 if (leastGenVal>_genThreshold) {
353 UnitList::push(u,_def[leastGenSym]);
354 while (equalGenerality.isNonEmpty()) {
355 UnitList::push(u,_def[equalGenerality.pop()]);
356 }
357 }
358 }
359 else {
360 unsigned generalityLimit=static_cast<int>(leastGenVal*_tolerance);
361 if (_tolerance==-1.0f) {
362 generalityLimit = UINT_MAX;
363 }
364
365 //if the generalityLimit is under _genThreshold, all suitable symbols are already added
366 if (generalityLimit>_genThreshold) {
367 sit=_symExtr.extractSymIds(u);
368 while (sit.hasNext()) {
369 SymId sym=sit.next();
370 unsigned val=_gen[sym];
371 //only if the symbol is over _genThreshold; otherwise it is already added
372 if (val>_genThreshold && val<=generalityLimit) {
373 UnitList::push(u,_def[sym]);
374 }
375 }
376 }
377 }
378
379 }
380
perform(Problem & prb)381 void SineSelector::perform(Problem& prb)
382 {
383 CALL("SineSelector::perform");
384
385 if (perform(prb.units())) {
386 prb.reportIncompleteTransformation();
387 }
388 prb.invalidateByRemoval();
389 }
390
perform(UnitList * & units)391 bool SineSelector::perform(UnitList*& units)
392 {
393 CALL("SineSelector::perform");
394
395 TimeCounter tc(TC_SINE_SELECTION);
396
397 initGeneralityFunction(units);
398
399 SymId symIdBound=_symExtr.getSymIdBound();
400
401 Set<Unit*> selected;
402 Stack<Unit*> selectedStack; //on this stack there are Units in the order they were selected
403 Deque<Unit*> newlySelected;
404
405 //build the D-relation and select the non-axiom formulas
406 _def.init(symIdBound,0);
407 unsigned numberUnitsLeftOut = 0;
408 UnitList::Iterator uit2(units);
409 while (uit2.hasNext()) {
410 numberUnitsLeftOut++;
411 Unit* u=uit2.next();
412 bool performSelection= _onIncluded ? u->included() : ((u->inputType()==UnitInputType::AXIOM)
413 || (env.options->guessTheGoal() != Options::GoalGuess::OFF && u->inputType()==UnitInputType::ASSUMPTION));
414 if (performSelection) { // register the unit for later
415 updateDefRelation(u);
416 }
417 else { // goal units are immediately taken (well, non-axiom, to by more precise. Includes ASSUMPTION, which cl->isGoal() does not take into account)
418 selected.insert(u);
419 selectedStack.push(u);
420 newlySelected.push_back(u);
421
422 if(_justForSineLevels) {
423 u->inference().setSineLevel(0);
424 //cout << "set level for " << u->toString() << " as " << "(0)" << endl;
425 }
426 }
427 }
428
429 unsigned depth=0;
430 newlySelected.push_back(0);
431
432 // cout << "env.maxClausePriority starts as" << env.maxClausePriority << endl;
433
434 //select required axiom formulas
435 while (newlySelected.isNonEmpty()) {
436 Unit* u=newlySelected.pop_front();
437
438 if (!u) {
439 //next selected formulas will be one step further from the original formulas
440 depth++;
441
442 if (_depthLimit && depth==_depthLimit) {
443 break;
444 }
445 ASS(!_depthLimit || depth<_depthLimit);
446 if(_justForSineLevels){
447 if (env.maxSineLevel < std::numeric_limits<decltype(env.maxSineLevel)>::max()) { // saturate at 255 or something
448 env.maxSineLevel++;
449 }
450 }
451 // cout << "Time to inc" << endl;
452
453 if (newlySelected.isNonEmpty()) {
454 //we must push another mark if we're not done yet
455 newlySelected.push_back(0);
456 }
457 continue;
458 }
459
460 SymIdIterator sit=_symExtr.extractSymIds(u);
461 while (sit.hasNext()) {
462 SymId sym=sit.next();
463
464 if (env.predicateSineLevels) {
465 bool pred;
466 unsigned functor;
467 SineSymbolExtractor::decodeSymId(sym,pred,functor);
468 if (pred && !env.predicateSineLevels->find(functor)) {
469 env.predicateSineLevels->insert(functor,env.maxSineLevel);
470 // cout << "set level of predicate " << functor << " i.e. " << env.signature->predicateName(functor) << " to " << env.maxClausePriority << endl;
471 }
472 }
473
474 UnitList::Iterator defUnits(_def[sym]);
475 while (defUnits.hasNext()) {
476 Unit* du=defUnits.next();
477 if (selected.contains(du)) {
478 continue;
479 }
480 selected.insert(du);
481 selectedStack.push(du);
482 newlySelected.push_back(du);
483
484 if(_justForSineLevels){
485 du->inference().setSineLevel(env.maxSineLevel);
486 //cout << "set level for " << du->toString() << " in iteration as " << env.maxClausePriority << endl;
487 }
488 }
489 //all defining units for the symbol sym were selected,
490 //so we can remove them from the relation
491 UnitList::destroy(_def[sym]);
492 _def[sym]=0;
493 }
494 }
495
496 if (_justForSineLevels) {
497 // units we did not touch will by default keep their sineLevel == UINT_MAX
498 return false;
499 }
500
501 env.statistics->sineIterations=depth;
502 env.statistics->selectedBySine=_unitsWithoutSymbols.size() + selectedStack.size();
503
504 numberUnitsLeftOut -= env.statistics->selectedBySine;
505
506 UnitList::destroy(units);
507 units=0;
508 UnitList::pushFromIterator(Stack<Unit*>::Iterator(_unitsWithoutSymbols), units);
509 while (selectedStack.isNonEmpty()) {
510 UnitList::push(selectedStack.pop(), units);
511 }
512
513 #if SINE_PRINT_SELECTED
514 UnitList::Iterator selIt(units);
515 while (selIt.hasNext()) {
516 cout<<'#'<<selIt.next()->toString()<<endl;
517 }
518 #endif
519
520 return (numberUnitsLeftOut > 0);
521 }
522
523 //////////////////////////////////////
524 // SineTheorySelector
525 //////////////////////////////////////
526
SineTheorySelector(const Options & opt)527 SineTheorySelector::SineTheorySelector(const Options& opt)
528 : _genThreshold(opt.sineGeneralityThreshold()), _opt(opt)
529 {
530 CALL("SineTheorySelector::SineTheorySelector");
531 }
532
handlePossibleSignatureChange()533 void SineTheorySelector::handlePossibleSignatureChange()
534 {
535 CALL("SineTheorySelector::handlePossibleSignatureChange");
536
537 size_t symIdBound=_symExtr.getSymIdBound();
538 size_t oldSize=_def.size();
539 ASS_EQ(_gen.size(), oldSize);
540
541 if (symIdBound==oldSize) {
542 return;
543 }
544 ASS_G(symIdBound, oldSize);
545
546 _gen.expand(symIdBound);
547 _def.expand(symIdBound);
548 for (size_t i=oldSize;i<symIdBound;i++) {
549 _gen[i]=0;
550 _def[i]=0;
551 }
552 }
553
554 /**
555 * Connect unit @b u with symbols it defines
556 */
updateDefRelation(Unit * u)557 void SineTheorySelector::updateDefRelation(Unit* u)
558 {
559 CALL("SineTheorySelector::updateDefRelation");
560
561 SymIdIterator sit0=_symExtr.extractSymIds(u);
562
563 if (!sit0.hasNext()) {
564
565 _unitsWithoutSymbols.push(u);
566 return;
567 }
568
569 static Stack<SymId> symIds;
570 symIds.reset();
571 symIds.loadFromIterator(sit0);
572
573 Stack<SymId>::Iterator sit(symIds);
574
575 ALWAYS(sit.hasNext());
576 unsigned leastGenVal=_gen[sit.next()];
577
578 while (sit.hasNext()) {
579 SymId sym=sit.next();
580 unsigned val=_gen[sym];
581 ASS_G(val,0);
582
583 if (val<leastGenVal) {
584 leastGenVal=val;
585 }
586 }
587
588 unsigned generalityLimit=leastGenVal*(maxTolerance/strictTolerance);
589
590 Stack<SymId>::Iterator sit2(symIds);
591 while (sit2.hasNext()) {
592 SymId sym=sit2.next();
593 unsigned val=_gen[sym];
594
595 if (val<=_genThreshold) {
596 //if a symbol fits under _genThreshold, add it into the relation
597 DEntryList::push(DEntry(strictTolerance,u),_def[sym]);
598 }
599 else if (val<=generalityLimit) {
600 unsigned short minTolerance=(val*strictTolerance)/leastGenVal;
601 //only if the symbol is over _genThreshold; otherwise it is already added
602 DEntryList::push(DEntry(minTolerance,u),_def[sym]);
603 }
604 }
605
606 }
607
608 /**
609 * Preprocess the theory axioms in @b units, so that some of them can be later
610 * selected for a particular problem formulas by the @b addSelectedAxioms() function
611 *
612 * If the value of the sineTolerance and sineDepth options changes after the
613 * preprocessing and before the call to the @b addSelectedAxioms function, the
614 * modified values will be used (The preprocessing allows for selection with
615 * tolerance values up to the limit implied by the value of @b maxTolerance.)
616 */
initSelectionStructure(UnitList * units)617 void SineTheorySelector::initSelectionStructure(UnitList* units)
618 {
619 CALL("SineTheorySelector::initSelectionStructure");
620
621 TimeCounter tc(TC_SINE_SELECTION);
622
623 initGeneralityFunction(units);
624
625 SymId symIdBound=_symExtr.getSymIdBound();
626
627 //build the D-relation
628 _def.init(symIdBound,0);
629 UnitList::Iterator uit(units);
630 while (uit.hasNext()) {
631 Unit* u=uit.next();
632 updateDefRelation(u);
633 }
634 }
635
636
perform(UnitList * & units)637 void SineTheorySelector::perform(UnitList*& units)
638 {
639 CALL("SineTheorySelector::perform");
640
641 TimeCounter tc(TC_SINE_SELECTION);
642
643 handlePossibleSignatureChange();
644
645 UnitList::Iterator uit(units);
646 while (uit.hasNext()) {
647 Unit* u=uit.next();
648 SymIdIterator sit=_symExtr.extractSymIds(u);
649 while (sit.hasNext()) {
650 SymId sid=sit.next();
651 _gen[sid]++;
652 }
653 }
654
655 UnitList* res=0;
656 DHSet<SymId> addedSymIds;
657 DHSet<Unit*> selected;
658 Deque<Unit*> newlySelected;
659
660 bool sineOnIncluded=_opt.sineSelection()==Options::SineSelection::INCLUDED;
661
662 //build the D-relation and select the non-axiom formulas
663 UnitList::Iterator uit2(units);
664 while (uit2.hasNext()) {
665 Unit* u=uit2.next();
666 bool performSelection= sineOnIncluded ? u->included() : ((u->inputType()==UnitInputType::AXIOM)
667 || (env.options->guessTheGoal() != Options::GoalGuess::OFF && u->inputType()==UnitInputType::ASSUMPTION));
668
669 if (performSelection) {
670 updateDefRelation(u);
671 }
672 else {
673 selected.insert(u);
674 newlySelected.push_back(u);
675 UnitList::push(u,res);
676 }
677 }
678
679
680 unsigned short intTolerance=static_cast<unsigned short>(ceil(_opt.sineTolerance()*10));
681
682 unsigned depthLimit=_opt.sineDepth();
683 unsigned depth=0;
684 newlySelected.push_back(0);
685
686 //select required axiom formulas
687 while (newlySelected.isNonEmpty()) {
688 Unit* u=newlySelected.pop_front();
689
690 if (!u) {
691 //next selected formulas will be one step further from the original formulas
692 depth++;
693 if (depthLimit && depth==depthLimit) {
694 break;
695 }
696 ASS(!depthLimit || depth<depthLimit);
697
698 if (newlySelected.isNonEmpty()) {
699 //we must push another mark if we're not done yet
700 newlySelected.push_back(0);
701 }
702 continue;
703 }
704
705 SymIdIterator sit=_symExtr.extractSymIds(u);
706 while (sit.hasNext()) {
707 SymId sym=sit.next();
708 if (!addedSymIds.insert(sym)) {
709 //we already added units belonging to this symbol
710 continue;
711 }
712 DEntryList::Iterator defUnits(_def[sym]);
713 while (defUnits.hasNext()) {
714 DEntry de=defUnits.next();
715
716 if (de.minTolerance>intTolerance || !selected.insert(de.unit)) {
717 continue;
718 }
719 UnitList::push(de.unit,res);
720 newlySelected.push_back(de.unit);
721 }
722 }
723 }
724
725 UnitList::pushFromIterator(Stack<Unit*>::Iterator(_unitsWithoutSymbols), res);
726
727 UnitList::destroy(units);
728 // units=res->reverse(); //we want to resemble the original SInE as much as possible
729 units=res;
730
731 env.statistics->sineIterations=depth;
732 env.statistics->selectedBySine=_unitsWithoutSymbols.size() + selected.size();
733
734 #if SINE_PRINT_SELECTED
735 UnitList::Iterator selIt(units);
736 while (selIt.hasNext()) {
737 cout<<'#'<<selIt.next()->toString()<<endl;
738 }
739 #endif
740 }
741
742 }
743