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