1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King, Dejan Jovanovic |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Base for theory interface. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/theory.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
#include <sstream> |
20 |
|
#include <string> |
21 |
|
#include <vector> |
22 |
|
|
23 |
|
#include "base/check.h" |
24 |
|
#include "expr/node_algorithm.h" |
25 |
|
#include "options/arith_options.h" |
26 |
|
#include "options/bv_options.h" |
27 |
|
#include "options/smt_options.h" |
28 |
|
#include "options/theory_options.h" |
29 |
|
#include "smt/smt_statistics_registry.h" |
30 |
|
#include "theory/ee_setup_info.h" |
31 |
|
#include "theory/ext_theory.h" |
32 |
|
#include "theory/output_channel.h" |
33 |
|
#include "theory/quantifiers_engine.h" |
34 |
|
#include "theory/substitutions.h" |
35 |
|
#include "theory/theory_inference_manager.h" |
36 |
|
#include "theory/theory_model.h" |
37 |
|
#include "theory/theory_rewriter.h" |
38 |
|
#include "theory/theory_state.h" |
39 |
|
#include "theory/trust_substitutions.h" |
40 |
|
|
41 |
|
using namespace std; |
42 |
|
|
43 |
|
namespace cvc5 { |
44 |
|
namespace theory { |
45 |
|
|
46 |
|
/** Default value for the uninterpreted sorts is the UF theory */ |
47 |
|
TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; |
48 |
|
|
49 |
|
std::ostream& operator<<(std::ostream& os, Theory::Effort level){ |
50 |
|
switch(level){ |
51 |
|
case Theory::EFFORT_STANDARD: |
52 |
|
os << "EFFORT_STANDARD"; break; |
53 |
|
case Theory::EFFORT_FULL: |
54 |
|
os << "EFFORT_FULL"; break; |
55 |
|
case Theory::EFFORT_LAST_CALL: |
56 |
|
os << "EFFORT_LAST_CALL"; break; |
57 |
|
default: |
58 |
|
Unreachable(); |
59 |
|
} |
60 |
|
return os; |
61 |
|
}/* ostream& operator<<(ostream&, Theory::Effort) */ |
62 |
|
|
63 |
127936 |
Theory::Theory(TheoryId id, |
64 |
|
context::Context* satContext, |
65 |
|
context::UserContext* userContext, |
66 |
|
OutputChannel& out, |
67 |
|
Valuation valuation, |
68 |
|
const LogicInfo& logicInfo, |
69 |
|
ProofNodeManager* pnm, |
70 |
127936 |
std::string name) |
71 |
|
: d_id(id), |
72 |
|
d_satContext(satContext), |
73 |
|
d_userContext(userContext), |
74 |
|
d_logicInfo(logicInfo), |
75 |
|
d_facts(satContext), |
76 |
|
d_factsHead(satContext, 0), |
77 |
|
d_sharedTermsIndex(satContext, 0), |
78 |
|
d_careGraph(nullptr), |
79 |
|
d_instanceName(name), |
80 |
255872 |
d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) |
81 |
255872 |
+ name + "checkTime")), |
82 |
127936 |
d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( |
83 |
255872 |
getStatsPrefix(id) + name + "computeCareGraphTime")), |
84 |
|
d_sharedTerms(satContext), |
85 |
|
d_out(&out), |
86 |
|
d_valuation(valuation), |
87 |
|
d_equalityEngine(nullptr), |
88 |
|
d_allocEqualityEngine(nullptr), |
89 |
|
d_theoryState(nullptr), |
90 |
|
d_inferManager(nullptr), |
91 |
|
d_quantEngine(nullptr), |
92 |
511744 |
d_pnm(pnm) |
93 |
|
{ |
94 |
127936 |
} |
95 |
|
|
96 |
127936 |
Theory::~Theory() { |
97 |
127936 |
} |
98 |
|
|
99 |
19676 |
bool Theory::needsEqualityEngine(EeSetupInfo& esi) |
100 |
|
{ |
101 |
|
// by default, this theory does not use an (official) equality engine |
102 |
19676 |
return false; |
103 |
|
} |
104 |
|
|
105 |
127894 |
void Theory::setEqualityEngine(eq::EqualityEngine* ee) |
106 |
|
{ |
107 |
|
// set the equality engine pointer |
108 |
127894 |
d_equalityEngine = ee; |
109 |
127894 |
if (d_theoryState != nullptr) |
110 |
|
{ |
111 |
108218 |
d_theoryState->setEqualityEngine(ee); |
112 |
|
} |
113 |
127894 |
if (d_inferManager != nullptr) |
114 |
|
{ |
115 |
108218 |
d_inferManager->setEqualityEngine(ee); |
116 |
|
} |
117 |
127894 |
} |
118 |
|
|
119 |
127894 |
void Theory::setQuantifiersEngine(QuantifiersEngine* qe) |
120 |
|
{ |
121 |
|
// quantifiers engine may be null if not in quantified logic |
122 |
127894 |
d_quantEngine = qe; |
123 |
127894 |
} |
124 |
|
|
125 |
127894 |
void Theory::setDecisionManager(DecisionManager* dm) |
126 |
|
{ |
127 |
127894 |
Assert(dm != nullptr); |
128 |
127894 |
if (d_inferManager != nullptr) |
129 |
|
{ |
130 |
108218 |
d_inferManager->setDecisionManager(dm); |
131 |
|
} |
132 |
127894 |
} |
133 |
|
|
134 |
|
void Theory::finishInitStandalone() |
135 |
|
{ |
136 |
|
EeSetupInfo esi; |
137 |
|
if (needsEqualityEngine(esi)) |
138 |
|
{ |
139 |
|
// always associated with the same SAT context as the theory (d_satContext) |
140 |
|
d_allocEqualityEngine.reset(new eq::EqualityEngine( |
141 |
|
*esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers)); |
142 |
|
// use it as the official equality engine |
143 |
|
setEqualityEngine(d_allocEqualityEngine.get()); |
144 |
|
} |
145 |
|
finishInit(); |
146 |
|
} |
147 |
|
|
148 |
174927481 |
TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) |
149 |
|
{ |
150 |
174927481 |
TheoryId tid = THEORY_BUILTIN; |
151 |
174927481 |
switch(mode) { |
152 |
122035911 |
case options::TheoryOfMode::THEORY_OF_TYPE_BASED: |
153 |
|
// Constants, variables, 0-ary constructors |
154 |
122035911 |
if (node.isVar()) |
155 |
|
{ |
156 |
4679114 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
157 |
|
{ |
158 |
230504 |
tid = THEORY_UF; |
159 |
|
} |
160 |
|
else |
161 |
|
{ |
162 |
4448610 |
tid = Theory::theoryOf(node.getType()); |
163 |
|
} |
164 |
|
} |
165 |
117356797 |
else if (node.getKind() == kind::EQUAL) |
166 |
|
{ |
167 |
|
// Equality is owned by the theory that owns the domain |
168 |
7224912 |
tid = Theory::theoryOf(node[0].getType()); |
169 |
|
} |
170 |
|
else |
171 |
|
{ |
172 |
|
// Regular nodes are owned by the kind. Notice that constants are a |
173 |
|
// special case here, where the theory of the kind of a constant |
174 |
|
// always coincides with the type of that constant. |
175 |
110131885 |
tid = kindToTheoryId(node.getKind()); |
176 |
|
} |
177 |
122035911 |
break; |
178 |
52891570 |
case options::TheoryOfMode::THEORY_OF_TERM_BASED: |
179 |
|
// Variables |
180 |
52891570 |
if (node.isVar()) |
181 |
|
{ |
182 |
5047596 |
if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) |
183 |
|
{ |
184 |
|
// We treat the variables as uninterpreted |
185 |
5035870 |
tid = s_uninterpretedSortOwner; |
186 |
|
} |
187 |
|
else |
188 |
|
{ |
189 |
11726 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
190 |
|
{ |
191 |
|
// Boolean vars go to UF |
192 |
7265 |
tid = THEORY_UF; |
193 |
|
} |
194 |
|
else |
195 |
|
{ |
196 |
|
// Except for the Boolean ones |
197 |
4461 |
tid = THEORY_BOOL; |
198 |
|
} |
199 |
|
} |
200 |
|
} |
201 |
47843974 |
else if (node.getKind() == kind::EQUAL) |
202 |
|
{ // Equality |
203 |
|
// If one of them is an ITE, it's irelevant, since they will get |
204 |
|
// replaced out anyhow |
205 |
4483562 |
if (node[0].getKind() == kind::ITE) |
206 |
|
{ |
207 |
5056 |
tid = Theory::theoryOf(node[0].getType()); |
208 |
|
} |
209 |
4478506 |
else if (node[1].getKind() == kind::ITE) |
210 |
|
{ |
211 |
10593 |
tid = Theory::theoryOf(node[1].getType()); |
212 |
|
} |
213 |
|
else |
214 |
|
{ |
215 |
8935826 |
TNode l = node[0]; |
216 |
8935826 |
TNode r = node[1]; |
217 |
8935826 |
TypeNode ltype = l.getType(); |
218 |
8935826 |
TypeNode rtype = r.getType(); |
219 |
|
// If the types are different, we must assign based on type due |
220 |
|
// to handling subtypes (limited to arithmetic). Also, if we are |
221 |
|
// a Boolean equality, we must assign THEORY_BOOL. |
222 |
4467913 |
if (ltype != rtype || ltype.isBoolean()) |
223 |
|
{ |
224 |
59095 |
tid = Theory::theoryOf(ltype); |
225 |
|
} |
226 |
|
else |
227 |
|
{ |
228 |
|
// If both sides belong to the same theory the choice is easy |
229 |
4408818 |
TheoryId T1 = Theory::theoryOf(l); |
230 |
4408818 |
TheoryId T2 = Theory::theoryOf(r); |
231 |
4408818 |
if (T1 == T2) |
232 |
|
{ |
233 |
2552326 |
tid = T1; |
234 |
|
} |
235 |
|
else |
236 |
|
{ |
237 |
1856492 |
TheoryId T3 = Theory::theoryOf(ltype); |
238 |
|
// This is a case of |
239 |
|
// * x*y = f(z) -> UF |
240 |
|
// * x = c -> UF |
241 |
|
// * f(x) = read(a, y) -> either UF or ARRAY |
242 |
|
// at least one of the theories has to be parametric, i.e. theory |
243 |
|
// of the type is different from the theory of the term |
244 |
1856492 |
if (T1 == T3) |
245 |
|
{ |
246 |
47982 |
tid = T2; |
247 |
|
} |
248 |
1808510 |
else if (T2 == T3) |
249 |
|
{ |
250 |
1761067 |
tid = T1; |
251 |
|
} |
252 |
|
else |
253 |
|
{ |
254 |
|
// If both are parametric, we take the smaller one (arbitrary) |
255 |
47443 |
tid = T1 < T2 ? T1 : T2; |
256 |
|
} |
257 |
|
} |
258 |
|
} |
259 |
|
} |
260 |
|
} |
261 |
|
else |
262 |
|
{ |
263 |
|
// Regular nodes are owned by the kind, which includes constants as a |
264 |
|
// special case. |
265 |
43360412 |
tid = kindToTheoryId(node.getKind()); |
266 |
|
} |
267 |
52891570 |
break; |
268 |
|
default: |
269 |
|
Unreachable(); |
270 |
|
} |
271 |
174927481 |
Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl; |
272 |
174927481 |
return tid; |
273 |
|
} |
274 |
|
|
275 |
904222 |
void Theory::notifySharedTerm(TNode n) |
276 |
|
{ |
277 |
|
// do nothing |
278 |
904222 |
} |
279 |
|
|
280 |
2418117 |
void Theory::notifyInConflict() |
281 |
|
{ |
282 |
2418117 |
if (d_inferManager != nullptr) |
283 |
|
{ |
284 |
2046099 |
d_inferManager->notifyInConflict(); |
285 |
|
} |
286 |
2418117 |
} |
287 |
|
|
288 |
6542 |
void Theory::computeCareGraph() { |
289 |
6542 |
Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl; |
290 |
7070 |
for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { |
291 |
1056 |
TNode a = d_sharedTerms[i]; |
292 |
1056 |
TypeNode aType = a.getType(); |
293 |
5094 |
for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) { |
294 |
8676 |
TNode b = d_sharedTerms[j]; |
295 |
4566 |
if (b.getType() != aType) { |
296 |
|
// We don't care about the terms of different types |
297 |
456 |
continue; |
298 |
|
} |
299 |
4110 |
switch (d_valuation.getEqualityStatus(a, b)) { |
300 |
3304 |
case EQUALITY_TRUE_AND_PROPAGATED: |
301 |
|
case EQUALITY_FALSE_AND_PROPAGATED: |
302 |
|
// If we know about it, we should have propagated it, so we can skip |
303 |
3304 |
break; |
304 |
806 |
default: |
305 |
|
// Let's split on it |
306 |
806 |
addCarePair(a, b); |
307 |
806 |
break; |
308 |
|
} |
309 |
|
} |
310 |
|
} |
311 |
6542 |
} |
312 |
|
|
313 |
|
void Theory::printFacts(std::ostream& os) const { |
314 |
|
unsigned i, n = d_facts.size(); |
315 |
|
for(i = 0; i < n; i++){ |
316 |
|
const Assertion& a_i = d_facts[i]; |
317 |
|
Node assertion = a_i; |
318 |
|
os << d_id << '[' << i << ']' << " " << assertion << endl; |
319 |
|
} |
320 |
|
} |
321 |
|
|
322 |
|
void Theory::debugPrintFacts() const{ |
323 |
|
DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl; |
324 |
|
printFacts(DebugChannel.getStream()); |
325 |
|
} |
326 |
|
|
327 |
17888 |
bool Theory::isLegalElimination(TNode x, TNode val) |
328 |
|
{ |
329 |
17888 |
Assert(x.isVar()); |
330 |
35776 |
if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE |
331 |
17888 |
|| val.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
332 |
|
{ |
333 |
|
return false; |
334 |
|
} |
335 |
17888 |
if (expr::hasSubterm(val, x)) |
336 |
|
{ |
337 |
4755 |
return false; |
338 |
|
} |
339 |
13133 |
if (!val.getType().isSubtypeOf(x.getType())) |
340 |
|
{ |
341 |
|
return false; |
342 |
|
} |
343 |
13133 |
if (!options::produceModels() && !d_logicInfo.isQuantified()) |
344 |
|
{ |
345 |
|
// Don't care about the model and logic is not quantified, we can eliminate. |
346 |
2949 |
return true; |
347 |
|
} |
348 |
|
// If models are enabled, then it depends on whether the term contains any |
349 |
|
// unevaluable operators like FORALL, SINE, etc. Having such operators makes |
350 |
|
// model construction contain non-constant values for variables, which is |
351 |
|
// not ideal from a user perspective. |
352 |
|
// We also insist on this check since the term to eliminate should never |
353 |
|
// contain quantifiers, or else variable shadowing issues may arise. |
354 |
|
// there should be a model object |
355 |
10184 |
TheoryModel* tm = d_valuation.getModel(); |
356 |
10184 |
Assert(tm != nullptr); |
357 |
10184 |
return tm->isLegalElimination(x, val); |
358 |
|
} |
359 |
|
|
360 |
14565 |
std::unordered_set<TNode> Theory::currentlySharedTerms() const |
361 |
|
{ |
362 |
14565 |
std::unordered_set<TNode> currentlyShared; |
363 |
271723 |
for (shared_terms_iterator i = shared_terms_begin(), |
364 |
14565 |
i_end = shared_terms_end(); i != i_end; ++i) { |
365 |
257158 |
currentlyShared.insert (*i); |
366 |
|
} |
367 |
14565 |
return currentlyShared; |
368 |
|
} |
369 |
|
|
370 |
102806 |
bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) |
371 |
|
{ |
372 |
|
// if we are using an equality engine, assert it to the model |
373 |
102806 |
if (d_equalityEngine != nullptr && !termSet.empty()) |
374 |
|
{ |
375 |
56868 |
Trace("model-builder") << "Assert Equality engine for " << d_id |
376 |
28434 |
<< std::endl; |
377 |
28434 |
if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) |
378 |
|
{ |
379 |
|
return false; |
380 |
|
} |
381 |
|
} |
382 |
102806 |
Trace("model-builder") << "Collect Model values for " << d_id << std::endl; |
383 |
|
// now, collect theory-specific value assigments |
384 |
102806 |
return collectModelValues(m, termSet); |
385 |
|
} |
386 |
|
|
387 |
99558 |
void Theory::computeRelevantTerms(std::set<Node>& termSet) |
388 |
|
{ |
389 |
|
// by default, there are no additional relevant terms |
390 |
99558 |
} |
391 |
|
|
392 |
37965 |
bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) |
393 |
|
{ |
394 |
37965 |
return true; |
395 |
|
} |
396 |
|
|
397 |
46415 |
Theory::PPAssertStatus Theory::ppAssert(TrustNode tin, |
398 |
|
TrustSubstitutionMap& outSubstitutions) |
399 |
|
{ |
400 |
92830 |
TNode in = tin.getNode(); |
401 |
46415 |
if (in.getKind() == kind::EQUAL) |
402 |
|
{ |
403 |
|
// (and (= x t) phi) can be replaced by phi[x/t] if |
404 |
|
// 1) x is a variable |
405 |
|
// 2) x is not in the term t |
406 |
|
// 3) x : T and t : S, then S <: T |
407 |
78020 |
if (in[0].isVar() && isLegalElimination(in[0], in[1]) |
408 |
73393 |
&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
409 |
|
{ |
410 |
10375 |
outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); |
411 |
10375 |
return PP_ASSERT_STATUS_SOLVED; |
412 |
|
} |
413 |
32140 |
if (in[1].isVar() && isLegalElimination(in[1], in[0]) |
414 |
32140 |
&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
415 |
|
{ |
416 |
247 |
outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); |
417 |
247 |
return PP_ASSERT_STATUS_SOLVED; |
418 |
|
} |
419 |
10384 |
if (in[0].isConst() && in[1].isConst()) |
420 |
|
{ |
421 |
|
if (in[0] != in[1]) |
422 |
|
{ |
423 |
|
return PP_ASSERT_STATUS_CONFLICT; |
424 |
|
} |
425 |
|
} |
426 |
|
} |
427 |
74347 |
else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL |
428 |
73928 |
&& in[0][0].getType().isBoolean()) |
429 |
|
{ |
430 |
44 |
TNode eq = in[0]; |
431 |
40 |
if (eq[0].isVar()) |
432 |
|
{ |
433 |
72 |
Node res = eq[0].eqNode(eq[1].notNode()); |
434 |
72 |
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
435 |
36 |
return ppAssert(tn, outSubstitutions); |
436 |
|
} |
437 |
4 |
else if (eq[1].isVar()) |
438 |
|
{ |
439 |
|
Node res = eq[1].eqNode(eq[0].notNode()); |
440 |
|
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
441 |
|
return ppAssert(tn, outSubstitutions); |
442 |
|
} |
443 |
|
} |
444 |
|
|
445 |
35757 |
return PP_ASSERT_STATUS_UNSOLVED; |
446 |
|
} |
447 |
|
|
448 |
|
std::pair<bool, Node> Theory::entailmentCheck(TNode lit) |
449 |
|
{ |
450 |
|
return make_pair(false, Node::null()); |
451 |
|
} |
452 |
|
|
453 |
41952 |
void Theory::addCarePair(TNode t1, TNode t2) { |
454 |
41952 |
if (d_careGraph) { |
455 |
41952 |
d_careGraph->insert(CarePair(t1, t2, d_id)); |
456 |
|
} |
457 |
41952 |
} |
458 |
|
|
459 |
68261 |
void Theory::getCareGraph(CareGraph* careGraph) { |
460 |
68261 |
Assert(careGraph != NULL); |
461 |
|
|
462 |
68261 |
Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; |
463 |
136522 |
TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); |
464 |
68261 |
d_careGraph = careGraph; |
465 |
68261 |
computeCareGraph(); |
466 |
68261 |
d_careGraph = NULL; |
467 |
68261 |
} |
468 |
|
|
469 |
|
bool Theory::proofsEnabled() const |
470 |
|
{ |
471 |
|
return d_pnm != nullptr; |
472 |
|
} |
473 |
|
|
474 |
20245 |
EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) |
475 |
|
{ |
476 |
|
// if not using an equality engine, then by default we don't know the status |
477 |
20245 |
if (d_equalityEngine == nullptr) |
478 |
|
{ |
479 |
5768 |
return EQUALITY_UNKNOWN; |
480 |
|
} |
481 |
14477 |
Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl; |
482 |
14477 |
Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); |
483 |
|
|
484 |
|
// Check for equality (simplest) |
485 |
14477 |
if (d_equalityEngine->areEqual(a, b)) |
486 |
|
{ |
487 |
|
// The terms are implied to be equal |
488 |
7296 |
return EQUALITY_TRUE; |
489 |
|
} |
490 |
|
|
491 |
|
// Check for disequality |
492 |
7181 |
if (d_equalityEngine->areDisequal(a, b, false)) |
493 |
|
{ |
494 |
|
// The terms are implied to be dis-equal |
495 |
2649 |
return EQUALITY_FALSE; |
496 |
|
} |
497 |
|
|
498 |
|
// All other terms are unknown, which is conservative. A theory may override |
499 |
|
// this method if it knows more information. |
500 |
4532 |
return EQUALITY_UNKNOWN; |
501 |
|
} |
502 |
|
|
503 |
13847623 |
void Theory::check(Effort level) |
504 |
|
{ |
505 |
|
// see if we are already done (as an optimization) |
506 |
13847623 |
if (done() && level < EFFORT_FULL) |
507 |
|
{ |
508 |
18044198 |
return; |
509 |
|
} |
510 |
4825524 |
Assert(d_theoryState!=nullptr); |
511 |
|
// standard calls for resource, stats |
512 |
4825524 |
d_out->spendResource(Resource::TheoryCheckStep); |
513 |
9651048 |
TimerStat::CodeTimer checkTimer(d_checkTime); |
514 |
9651048 |
Trace("theory-check") << "Theory::preCheck " << level << " " << d_id |
515 |
4825524 |
<< std::endl; |
516 |
|
// pre-check at level |
517 |
4825524 |
if (preCheck(level)) |
518 |
|
{ |
519 |
|
// check aborted for a theory-specific reason |
520 |
|
return; |
521 |
|
} |
522 |
4825524 |
Assert(d_theoryState != nullptr); |
523 |
4825524 |
Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl; |
524 |
|
// process the pending fact queue |
525 |
33880586 |
while (!done() && !d_theoryState->isInConflict()) |
526 |
|
{ |
527 |
|
// Get the next assertion from the fact queue |
528 |
21367255 |
Assertion assertion = get(); |
529 |
21367255 |
TNode fact = assertion.d_assertion; |
530 |
29055068 |
Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id |
531 |
14527534 |
<< std::endl; |
532 |
14527534 |
bool polarity = fact.getKind() != kind::NOT; |
533 |
21367255 |
TNode atom = polarity ? fact : fact[0]; |
534 |
|
// call the pre-notify method |
535 |
14527534 |
if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false)) |
536 |
|
{ |
537 |
|
// handled in theory-specific way that doesn't involve equality engine |
538 |
7687813 |
continue; |
539 |
|
} |
540 |
13679442 |
Trace("theory-check") << "Theory::assert " << fact << " " << d_id |
541 |
6839721 |
<< std::endl; |
542 |
|
// Theories that don't have an equality engine should always return true |
543 |
|
// for preNotifyFact |
544 |
6839721 |
Assert(d_equalityEngine != nullptr); |
545 |
|
// assert to the equality engine |
546 |
6839721 |
if (atom.getKind() == kind::EQUAL) |
547 |
|
{ |
548 |
5357951 |
d_equalityEngine->assertEquality(atom, polarity, fact); |
549 |
|
} |
550 |
|
else |
551 |
|
{ |
552 |
1481773 |
d_equalityEngine->assertPredicate(atom, polarity, fact); |
553 |
|
} |
554 |
13679436 |
Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id |
555 |
6839718 |
<< std::endl; |
556 |
|
// notify the theory of the new fact, which is not internal |
557 |
6839718 |
notifyFact(atom, polarity, fact, false); |
558 |
|
} |
559 |
4825521 |
Trace("theory-check") << "Theory::postCheck " << d_id << std::endl; |
560 |
|
// post-check at level |
561 |
4825521 |
postCheck(level); |
562 |
4825520 |
Trace("theory-check") << "Theory::finish check " << d_id << std::endl; |
563 |
|
} |
564 |
|
|
565 |
1790693 |
bool Theory::preCheck(Effort level) { return false; } |
566 |
|
|
567 |
2 |
void Theory::postCheck(Effort level) {} |
568 |
|
|
569 |
4927900 |
bool Theory::preNotifyFact( |
570 |
|
TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) |
571 |
|
{ |
572 |
4927900 |
return false; |
573 |
|
} |
574 |
|
|
575 |
8384 |
void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal) |
576 |
|
{ |
577 |
8384 |
} |
578 |
|
|
579 |
22124 |
void Theory::preRegisterTerm(TNode node) {} |
580 |
|
|
581 |
1646650 |
void Theory::addSharedTerm(TNode n) |
582 |
|
{ |
583 |
3293300 |
Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" |
584 |
1646650 |
<< std::endl; |
585 |
3293300 |
Debug("theory::assertions") |
586 |
1646650 |
<< "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; |
587 |
1646650 |
d_sharedTerms.push_back(n); |
588 |
|
// now call theory-specific method notifySharedTerm |
589 |
1646650 |
notifySharedTerm(n); |
590 |
|
// if we have an equality engine, add the trigger term |
591 |
1646650 |
if (d_equalityEngine != nullptr) |
592 |
|
{ |
593 |
1641053 |
d_equalityEngine->addTriggerTerm(n, d_id); |
594 |
|
} |
595 |
1646650 |
} |
596 |
|
|
597 |
392873 |
eq::EqualityEngine* Theory::getEqualityEngine() |
598 |
|
{ |
599 |
|
// get the assigned equality engine, which is a pointer stored in this class |
600 |
392873 |
return d_equalityEngine; |
601 |
|
} |
602 |
|
|
603 |
350 |
bool Theory::usesCentralEqualityEngine() const |
604 |
|
{ |
605 |
350 |
return usesCentralEqualityEngine(d_id); |
606 |
|
} |
607 |
|
|
608 |
25306625 |
bool Theory::usesCentralEqualityEngine(TheoryId id) |
609 |
|
{ |
610 |
25306625 |
if (id == THEORY_BUILTIN) |
611 |
|
{ |
612 |
9611959 |
return true; |
613 |
|
} |
614 |
15694666 |
if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) |
615 |
|
{ |
616 |
15650852 |
return false; |
617 |
|
} |
618 |
43814 |
if (id == THEORY_ARITH) |
619 |
|
{ |
620 |
|
// conditional on whether we are using the equality solver |
621 |
70 |
return options::arithEqSolver(); |
622 |
|
} |
623 |
43744 |
if (id == THEORY_BV) |
624 |
|
{ |
625 |
|
// the internal bitblast BV solver doesnt use an equality engine |
626 |
80 |
return options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL; |
627 |
|
} |
628 |
41226 |
return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS |
629 |
23232 |
|| id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS |
630 |
66320 |
|| id == THEORY_SEP || id == THEORY_ARRAYS; |
631 |
|
} |
632 |
|
|
633 |
29135746 |
bool Theory::expUsingCentralEqualityEngine(TheoryId id) |
634 |
|
{ |
635 |
29135746 |
return id != THEORY_ARITH && usesCentralEqualityEngine(id); |
636 |
|
} |
637 |
|
|
638 |
|
} // namespace theory |
639 |
29280 |
} // namespace cvc5 |