1
2 /*
3 * File Selector.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 Selector.cpp
21 * Implements class Selector.
22 */
23
24 #include "Lib/DHMap.hpp"
25 #include "Lib/DHSet.hpp"
26 #include "Lib/Environment.hpp"
27 #include "Lib/Exception.hpp"
28 #include "Lib/Stack.hpp"
29 #include "Lib/TimeCounter.hpp"
30
31 #include "Kernel/Clause.hpp"
32 #include "Kernel/Inference.hpp"
33
34 #include "Shell/Options.hpp"
35 #include "Shell/Statistics.hpp"
36
37 #include "Selector.hpp"
38
39 namespace Shell
40 {
41 namespace LTB
42 {
43
44 using namespace Lib;
45 using namespace Kernel;
46
47 class SignatureMap
48 {
49 public:
SignatureMap(Storage * storage)50 SignatureMap(Storage* storage)
51 : _storage(storage)
52 {
53 }
54 private:
55 Storage* _storage;
56
57 DHMap<unsigned,unsigned> _predLoc2Glob;
58 DHMap<unsigned,unsigned> _funLoc2Glob;
59 DHMap<unsigned,unsigned> _predGlob2Loc;
60 DHMap<unsigned,unsigned> _funGlob2Loc;
61 };
62
63 /**
64 * Class for obtaining global SymIds from units.
65 *
66 * Global SymIds correspond to the signature used in the theory stored
67 * in the @b Storage object passed to the constructor.
68 */
69 class TranslatingSymbolCollector
70 {
71 public:
TranslatingSymbolCollector(Storage * storage)72 TranslatingSymbolCollector(Storage* storage)
73 : _storage(storage)
74 {
75 }
76
77 void collectSymIds(Unit* u);
78
79 SymIdIterator getSymIds();
80
81 private:
82 DHSet<SymId> _collected;
83
84 SineSymbolExtractor _sSymExtr;
85 Storage* _storage;
86 };
87
88
collectSymIds(Unit * u)89 void TranslatingSymbolCollector::collectSymIds(Unit* u)
90 {
91 CALL("TranslatingSymbolCollector::collectSymIds");
92
93 SymIdIterator locSymIds=_sSymExtr.extractSymIds(u);
94 while(locSymIds.hasNext()) {
95 SymId s=locSymIds.next();
96 _collected.insert(s);
97 }
98 }
99
100 /**
101 * Return collected global SymIds
102 *
103 * Local SymIds that don't have a global counterpart are discarded.
104 */
getSymIds()105 SymIdIterator TranslatingSymbolCollector::getSymIds()
106 {
107 CALL("TranslatingSymbolExtractor::extractSymIds");
108
109 // static Stack<SymId> unknownSymIds;
110 // unknownSymIds.reset();
111 //
112 // while(locSymIds.hasNext()) {
113 // SymId s=locSymIds.next();
114 // SymId gs;
115 // if(_dict.find(s, gs)) {
116 // List<SymId>::push(gs, res);
117 // }
118 // else {
119 // unknownSymIds.push(s);
120 // }
121 // }
122
123 Stack<pair<bool, unsigned> > queries;
124 SymIdIterator sit=_collected.iterator();
125 while(sit.hasNext()) {
126 SymId s=sit.next();
127 bool pred;
128 unsigned functor;
129 _sSymExtr.decodeSymId(s, pred, functor);
130 queries.push(make_pair(pred, functor));
131 }
132
133
134 int globPreds;
135 int globFuns;
136 _storage->getSignatureSize(globPreds, globFuns);
137
138 VirtualIterator<pair<bool, unsigned> > results=_storage->getGlobalSymbols(queries);
139 List<SymId>* res=0;
140
141 while(results.hasNext()) {
142 pair<bool, unsigned> s=results.next();
143 SymId sid;
144 if(s.first) {
145 sid=s.second;
146 }
147 else {
148 sid=globPreds+s.second;
149 }
150 List<SymId>::push(sid, res);
151 }
152
153 return pvi( List<SymId>::DestructiveIterator(res) );
154 }
155
156
selectForProblem(UnitList * & units)157 void Selector::selectForProblem(UnitList*& units)
158 {
159 CALL("Selector::selectForProblem");
160
161 TimeCounter tc(TC_SINE_SELECTION);
162
163 if(_storage.getEmptyClausePossession()) {
164 Clause* cl=Clause::fromIterator(VirtualIterator<Literal*>::getEmpty(), Unit::AXIOM, new Inference0(Inference::EXTERNAL_THEORY_AXIOM));
165 units->destroy();
166 units=0;
167 UnitList::push(cl, units);
168 return;
169 }
170
171 TranslatingSymbolCollector tsc(&_storage);
172 UnitList::Iterator uit(units);
173 while(uit.hasNext()) {
174 tsc.collectSymIds(uit.next());
175 }
176
177 unsigned itolerance=static_cast<unsigned>(100*env.options->sineTolerance());
178
179 DHSet<SymId> selectedSymbols;
180 Stack<SymId> newlySelected;
181
182 newlySelected.loadFromIterator(tsc.getSymIds());
183 selectedSymbols.loadFromIterator(Stack<SymId>::Iterator(newlySelected));
184
185 unsigned depthLimit=env.options->sineDepth();
186 unsigned depth=1;
187 for(;;) {
188 if(depthLimit && depth==depthLimit) {
189 break;
190 }
191
192 SymIdIterator sit=_storage.getDRelatedSymbols(newlySelected, itolerance);
193 newlySelected.reset();
194 while(sit.hasNext()) {
195 SymId s=sit.next();
196 if(selectedSymbols.insert(s)) {
197 newlySelected.push(s);
198 }
199 }
200 if(newlySelected.isEmpty()) {
201 break;
202 }
203 depth++;
204 }
205
206 env.statistics->sineIterations=depth;
207
208 DHSet<unsigned> selectedFormulas;
209 selectedFormulas.loadFromIterator(_storage.getNumbersOfUnitsWithoutSymbols());
210 selectedFormulas.loadFromIterator(_storage.getDRelatedUnitNumbers(selectedSymbols.iterator(), itolerance));
211
212 UnitList* selected=_storage.getClausesByUnitNumbers(selectedFormulas.iterator());
213
214 units=UnitList::concat(units, selected);
215 }
216
217
218 }
219 }
220
221