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 |
128144 |
Theory::Theory(TheoryId id, |
63 |
|
Env& env, |
64 |
|
OutputChannel& out, |
65 |
|
Valuation valuation, |
66 |
128144 |
std::string name) |
67 |
|
: d_id(id), |
68 |
|
d_env(env), |
69 |
128144 |
d_facts(d_env.getContext()), |
70 |
128144 |
d_factsHead(d_env.getContext(), 0), |
71 |
128144 |
d_sharedTermsIndex(d_env.getContext(), 0), |
72 |
|
d_careGraph(nullptr), |
73 |
|
d_instanceName(name), |
74 |
256288 |
d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) |
75 |
256288 |
+ name + "checkTime")), |
76 |
128144 |
d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( |
77 |
256288 |
getStatsPrefix(id) + name + "computeCareGraphTime")), |
78 |
128144 |
d_sharedTerms(d_env.getContext()), |
79 |
|
d_out(&out), |
80 |
|
d_valuation(valuation), |
81 |
|
d_equalityEngine(nullptr), |
82 |
|
d_allocEqualityEngine(nullptr), |
83 |
|
d_theoryState(nullptr), |
84 |
|
d_inferManager(nullptr), |
85 |
|
d_quantEngine(nullptr), |
86 |
128144 |
d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() |
87 |
1153296 |
: nullptr) |
88 |
|
{ |
89 |
128144 |
} |
90 |
|
|
91 |
128144 |
Theory::~Theory() { |
92 |
128144 |
} |
93 |
|
|
94 |
19708 |
bool Theory::needsEqualityEngine(EeSetupInfo& esi) |
95 |
|
{ |
96 |
|
// by default, this theory does not use an (official) equality engine |
97 |
19708 |
return false; |
98 |
|
} |
99 |
|
|
100 |
128102 |
void Theory::setEqualityEngine(eq::EqualityEngine* ee) |
101 |
|
{ |
102 |
|
// set the equality engine pointer |
103 |
128102 |
d_equalityEngine = ee; |
104 |
128102 |
if (d_theoryState != nullptr) |
105 |
|
{ |
106 |
118248 |
d_theoryState->setEqualityEngine(ee); |
107 |
|
} |
108 |
128102 |
if (d_inferManager != nullptr) |
109 |
|
{ |
110 |
118248 |
d_inferManager->setEqualityEngine(ee); |
111 |
|
} |
112 |
128102 |
} |
113 |
|
|
114 |
128102 |
void Theory::setQuantifiersEngine(QuantifiersEngine* qe) |
115 |
|
{ |
116 |
|
// quantifiers engine may be null if not in quantified logic |
117 |
128102 |
d_quantEngine = qe; |
118 |
128102 |
} |
119 |
|
|
120 |
128102 |
void Theory::setDecisionManager(DecisionManager* dm) |
121 |
|
{ |
122 |
128102 |
Assert(dm != nullptr); |
123 |
128102 |
if (d_inferManager != nullptr) |
124 |
|
{ |
125 |
118248 |
d_inferManager->setDecisionManager(dm); |
126 |
|
} |
127 |
128102 |
} |
128 |
|
|
129 |
|
void Theory::finishInitStandalone() |
130 |
|
{ |
131 |
|
EeSetupInfo esi; |
132 |
|
if (needsEqualityEngine(esi)) |
133 |
|
{ |
134 |
|
// always associated with the same SAT context as the theory |
135 |
|
d_allocEqualityEngine.reset( |
136 |
|
new eq::EqualityEngine(*esi.d_notify, |
137 |
|
getSatContext(), |
138 |
|
esi.d_name, |
139 |
|
esi.d_constantsAreTriggers)); |
140 |
|
// use it as the official equality engine |
141 |
|
setEqualityEngine(d_allocEqualityEngine.get()); |
142 |
|
} |
143 |
|
finishInit(); |
144 |
|
} |
145 |
|
|
146 |
168709275 |
TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) |
147 |
|
{ |
148 |
168709275 |
TheoryId tid = THEORY_BUILTIN; |
149 |
168709275 |
switch(mode) { |
150 |
115649538 |
case options::TheoryOfMode::THEORY_OF_TYPE_BASED: |
151 |
|
// Constants, variables, 0-ary constructors |
152 |
115649538 |
if (node.isVar()) |
153 |
|
{ |
154 |
4632666 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
155 |
|
{ |
156 |
228090 |
tid = THEORY_UF; |
157 |
|
} |
158 |
|
else |
159 |
|
{ |
160 |
4404576 |
tid = Theory::theoryOf(node.getType()); |
161 |
|
} |
162 |
|
} |
163 |
111016872 |
else if (node.getKind() == kind::EQUAL) |
164 |
|
{ |
165 |
|
// Equality is owned by the theory that owns the domain |
166 |
7293213 |
tid = Theory::theoryOf(node[0].getType()); |
167 |
|
} |
168 |
|
else |
169 |
|
{ |
170 |
|
// Regular nodes are owned by the kind. Notice that constants are a |
171 |
|
// special case here, where the theory of the kind of a constant |
172 |
|
// always coincides with the type of that constant. |
173 |
103723659 |
tid = kindToTheoryId(node.getKind()); |
174 |
|
} |
175 |
115649538 |
break; |
176 |
53059737 |
case options::TheoryOfMode::THEORY_OF_TERM_BASED: |
177 |
|
// Variables |
178 |
53059737 |
if (node.isVar()) |
179 |
|
{ |
180 |
5062904 |
if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) |
181 |
|
{ |
182 |
|
// We treat the variables as uninterpreted |
183 |
5051717 |
tid = s_uninterpretedSortOwner; |
184 |
|
} |
185 |
|
else |
186 |
|
{ |
187 |
11187 |
if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
188 |
|
{ |
189 |
|
// Boolean vars go to UF |
190 |
6724 |
tid = THEORY_UF; |
191 |
|
} |
192 |
|
else |
193 |
|
{ |
194 |
|
// Except for the Boolean ones |
195 |
4463 |
tid = THEORY_BOOL; |
196 |
|
} |
197 |
|
} |
198 |
|
} |
199 |
47996833 |
else if (node.getKind() == kind::EQUAL) |
200 |
|
{ // Equality |
201 |
|
// If one of them is an ITE, it's irelevant, since they will get |
202 |
|
// replaced out anyhow |
203 |
4494029 |
if (node[0].getKind() == kind::ITE) |
204 |
|
{ |
205 |
5053 |
tid = Theory::theoryOf(node[0].getType()); |
206 |
|
} |
207 |
4488976 |
else if (node[1].getKind() == kind::ITE) |
208 |
|
{ |
209 |
10607 |
tid = Theory::theoryOf(node[1].getType()); |
210 |
|
} |
211 |
|
else |
212 |
|
{ |
213 |
8956738 |
TNode l = node[0]; |
214 |
8956738 |
TNode r = node[1]; |
215 |
8956738 |
TypeNode ltype = l.getType(); |
216 |
8956738 |
TypeNode rtype = r.getType(); |
217 |
|
// If the types are different, we must assign based on type due |
218 |
|
// to handling subtypes (limited to arithmetic). Also, if we are |
219 |
|
// a Boolean equality, we must assign THEORY_BOOL. |
220 |
4478369 |
if (ltype != rtype || ltype.isBoolean()) |
221 |
|
{ |
222 |
59067 |
tid = Theory::theoryOf(ltype); |
223 |
|
} |
224 |
|
else |
225 |
|
{ |
226 |
|
// If both sides belong to the same theory the choice is easy |
227 |
4419302 |
TheoryId T1 = Theory::theoryOf(l); |
228 |
4419302 |
TheoryId T2 = Theory::theoryOf(r); |
229 |
4419302 |
if (T1 == T2) |
230 |
|
{ |
231 |
2562609 |
tid = T1; |
232 |
|
} |
233 |
|
else |
234 |
|
{ |
235 |
1856693 |
TheoryId T3 = Theory::theoryOf(ltype); |
236 |
|
// This is a case of |
237 |
|
// * x*y = f(z) -> UF |
238 |
|
// * x = c -> UF |
239 |
|
// * f(x) = read(a, y) -> either UF or ARRAY |
240 |
|
// at least one of the theories has to be parametric, i.e. theory |
241 |
|
// of the type is different from the theory of the term |
242 |
1856693 |
if (T1 == T3) |
243 |
|
{ |
244 |
47982 |
tid = T2; |
245 |
|
} |
246 |
1808711 |
else if (T2 == T3) |
247 |
|
{ |
248 |
1761268 |
tid = T1; |
249 |
|
} |
250 |
|
else |
251 |
|
{ |
252 |
|
// If both are parametric, we take the smaller one (arbitrary) |
253 |
47443 |
tid = T1 < T2 ? T1 : T2; |
254 |
|
} |
255 |
|
} |
256 |
|
} |
257 |
|
} |
258 |
|
} |
259 |
|
else |
260 |
|
{ |
261 |
|
// Regular nodes are owned by the kind, which includes constants as a |
262 |
|
// special case. |
263 |
43502804 |
tid = kindToTheoryId(node.getKind()); |
264 |
|
} |
265 |
53059737 |
break; |
266 |
|
default: |
267 |
|
Unreachable(); |
268 |
|
} |
269 |
168709275 |
Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl; |
270 |
168709275 |
return tid; |
271 |
|
} |
272 |
|
|
273 |
893965 |
void Theory::notifySharedTerm(TNode n) |
274 |
|
{ |
275 |
|
// do nothing |
276 |
893965 |
} |
277 |
|
|
278 |
2439320 |
void Theory::notifyInConflict() |
279 |
|
{ |
280 |
2439320 |
if (d_inferManager != nullptr) |
281 |
|
{ |
282 |
2251680 |
d_inferManager->notifyInConflict(); |
283 |
|
} |
284 |
2439320 |
} |
285 |
|
|
286 |
6539 |
void Theory::computeCareGraph() { |
287 |
6539 |
Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl; |
288 |
7067 |
for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { |
289 |
1056 |
TNode a = d_sharedTerms[i]; |
290 |
1056 |
TypeNode aType = a.getType(); |
291 |
5094 |
for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) { |
292 |
8676 |
TNode b = d_sharedTerms[j]; |
293 |
4566 |
if (b.getType() != aType) { |
294 |
|
// We don't care about the terms of different types |
295 |
456 |
continue; |
296 |
|
} |
297 |
4110 |
switch (d_valuation.getEqualityStatus(a, b)) { |
298 |
3304 |
case EQUALITY_TRUE_AND_PROPAGATED: |
299 |
|
case EQUALITY_FALSE_AND_PROPAGATED: |
300 |
|
// If we know about it, we should have propagated it, so we can skip |
301 |
3304 |
break; |
302 |
806 |
default: |
303 |
|
// Let's split on it |
304 |
806 |
addCarePair(a, b); |
305 |
806 |
break; |
306 |
|
} |
307 |
|
} |
308 |
|
} |
309 |
6539 |
} |
310 |
|
|
311 |
|
void Theory::printFacts(std::ostream& os) const { |
312 |
|
unsigned i, n = d_facts.size(); |
313 |
|
for(i = 0; i < n; i++){ |
314 |
|
const Assertion& a_i = d_facts[i]; |
315 |
|
Node assertion = a_i; |
316 |
|
os << d_id << '[' << i << ']' << " " << assertion << endl; |
317 |
|
} |
318 |
|
} |
319 |
|
|
320 |
|
void Theory::debugPrintFacts() const{ |
321 |
|
DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl; |
322 |
|
printFacts(DebugChannel.getStream()); |
323 |
|
} |
324 |
|
|
325 |
17891 |
bool Theory::isLegalElimination(TNode x, TNode val) |
326 |
|
{ |
327 |
17891 |
Assert(x.isVar()); |
328 |
35782 |
if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE |
329 |
17891 |
|| val.getKind() == kind::BOOLEAN_TERM_VARIABLE) |
330 |
|
{ |
331 |
|
return false; |
332 |
|
} |
333 |
17891 |
if (expr::hasSubterm(val, x)) |
334 |
|
{ |
335 |
4757 |
return false; |
336 |
|
} |
337 |
13134 |
if (!val.getType().isSubtypeOf(x.getType())) |
338 |
|
{ |
339 |
|
return false; |
340 |
|
} |
341 |
13134 |
if (!options::produceModels() && !getLogicInfo().isQuantified()) |
342 |
|
{ |
343 |
|
// Don't care about the model and logic is not quantified, we can eliminate. |
344 |
2949 |
return true; |
345 |
|
} |
346 |
|
// If models are enabled, then it depends on whether the term contains any |
347 |
|
// unevaluable operators like FORALL, SINE, etc. Having such operators makes |
348 |
|
// model construction contain non-constant values for variables, which is |
349 |
|
// not ideal from a user perspective. |
350 |
|
// We also insist on this check since the term to eliminate should never |
351 |
|
// contain quantifiers, or else variable shadowing issues may arise. |
352 |
|
// there should be a model object |
353 |
10185 |
TheoryModel* tm = d_valuation.getModel(); |
354 |
10185 |
Assert(tm != nullptr); |
355 |
10185 |
return tm->isLegalElimination(x, val); |
356 |
|
} |
357 |
|
|
358 |
14537 |
std::unordered_set<TNode> Theory::currentlySharedTerms() const |
359 |
|
{ |
360 |
14537 |
std::unordered_set<TNode> currentlyShared; |
361 |
271569 |
for (shared_terms_iterator i = shared_terms_begin(), |
362 |
14537 |
i_end = shared_terms_end(); i != i_end; ++i) { |
363 |
257032 |
currentlyShared.insert (*i); |
364 |
|
} |
365 |
14537 |
return currentlyShared; |
366 |
|
} |
367 |
|
|
368 |
69636 |
bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) |
369 |
|
{ |
370 |
|
// if we are using an equality engine, assert it to the model |
371 |
69636 |
if (d_equalityEngine != nullptr && !termSet.empty()) |
372 |
|
{ |
373 |
56746 |
Trace("model-builder") << "Assert Equality engine for " << d_id |
374 |
28373 |
<< std::endl; |
375 |
28373 |
if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) |
376 |
|
{ |
377 |
|
return false; |
378 |
|
} |
379 |
|
} |
380 |
69636 |
Trace("model-builder") << "Collect Model values for " << d_id << std::endl; |
381 |
|
// now, collect theory-specific value assigments |
382 |
69636 |
return collectModelValues(m, termSet); |
383 |
|
} |
384 |
|
|
385 |
66415 |
void Theory::computeRelevantTerms(std::set<Node>& termSet) |
386 |
|
{ |
387 |
|
// by default, there are no additional relevant terms |
388 |
66415 |
} |
389 |
|
|
390 |
89328 |
void Theory::collectAssertedTerms(std::set<Node>& termSet, |
391 |
|
bool includeShared) const |
392 |
|
{ |
393 |
|
// Collect all terms appearing in assertions |
394 |
89328 |
context::CDList<Assertion>::const_iterator assert_it = facts_begin(), |
395 |
89328 |
assert_it_end = facts_end(); |
396 |
4495822 |
for (; assert_it != assert_it_end; ++assert_it) |
397 |
|
{ |
398 |
2203247 |
collectTerms(*assert_it, termSet); |
399 |
|
} |
400 |
|
|
401 |
89328 |
if (includeShared) |
402 |
|
{ |
403 |
|
// Add terms that are shared terms |
404 |
89328 |
context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), |
405 |
89328 |
shared_it_end = shared_terms_end(); |
406 |
1341646 |
for (; shared_it != shared_it_end; ++shared_it) |
407 |
|
{ |
408 |
626159 |
collectTerms(*shared_it, termSet); |
409 |
|
} |
410 |
|
} |
411 |
89328 |
} |
412 |
|
|
413 |
2829406 |
void Theory::collectTerms(TNode n, std::set<Node>& termSet) const |
414 |
|
{ |
415 |
|
const std::set<Kind>& irrKinds = |
416 |
2829406 |
d_theoryState->getModel()->getIrrelevantKinds(); |
417 |
5658812 |
std::vector<TNode> visit; |
418 |
5658812 |
TNode cur; |
419 |
2829406 |
visit.push_back(n); |
420 |
7163484 |
do |
421 |
|
{ |
422 |
9992890 |
cur = visit.back(); |
423 |
9992890 |
visit.pop_back(); |
424 |
9992890 |
if (termSet.find(cur) != termSet.end()) |
425 |
|
{ |
426 |
|
// already visited |
427 |
4881122 |
continue; |
428 |
|
} |
429 |
5111768 |
Kind k = cur.getKind(); |
430 |
|
// only add to term set if a relevant kind |
431 |
5111768 |
if (irrKinds.find(k) == irrKinds.end()) |
432 |
|
{ |
433 |
2446381 |
termSet.insert(cur); |
434 |
|
} |
435 |
|
// traverse owned terms, don't go under quantifiers |
436 |
14166169 |
if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == d_id) |
437 |
14994422 |
&& !cur.isClosure()) |
438 |
|
{ |
439 |
4741381 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
440 |
|
} |
441 |
9992890 |
} while (!visit.empty()); |
442 |
2829406 |
} |
443 |
|
|
444 |
4930 |
bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) |
445 |
|
{ |
446 |
4930 |
return true; |
447 |
|
} |
448 |
|
|
449 |
46431 |
Theory::PPAssertStatus Theory::ppAssert(TrustNode tin, |
450 |
|
TrustSubstitutionMap& outSubstitutions) |
451 |
|
{ |
452 |
92862 |
TNode in = tin.getNode(); |
453 |
46431 |
if (in.getKind() == kind::EQUAL) |
454 |
|
{ |
455 |
|
// (and (= x t) phi) can be replaced by phi[x/t] if |
456 |
|
// 1) x is a variable |
457 |
|
// 2) x is not in the term t |
458 |
|
// 3) x : T and t : S, then S <: T |
459 |
78056 |
if (in[0].isVar() && isLegalElimination(in[0], in[1]) |
460 |
73427 |
&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
461 |
|
{ |
462 |
10376 |
outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); |
463 |
10376 |
return PP_ASSERT_STATUS_SOLVED; |
464 |
|
} |
465 |
32170 |
if (in[1].isVar() && isLegalElimination(in[1], in[0]) |
466 |
32170 |
&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE) |
467 |
|
{ |
468 |
247 |
outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); |
469 |
247 |
return PP_ASSERT_STATUS_SOLVED; |
470 |
|
} |
471 |
10394 |
if (in[0].isConst() && in[1].isConst()) |
472 |
|
{ |
473 |
|
if (in[0] != in[1]) |
474 |
|
{ |
475 |
|
return PP_ASSERT_STATUS_CONFLICT; |
476 |
|
} |
477 |
|
} |
478 |
|
} |
479 |
74360 |
else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL |
480 |
73939 |
&& in[0][0].getType().isBoolean()) |
481 |
|
{ |
482 |
45 |
TNode eq = in[0]; |
483 |
41 |
if (eq[0].isVar()) |
484 |
|
{ |
485 |
74 |
Node res = eq[0].eqNode(eq[1].notNode()); |
486 |
74 |
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
487 |
37 |
return ppAssert(tn, outSubstitutions); |
488 |
|
} |
489 |
4 |
else if (eq[1].isVar()) |
490 |
|
{ |
491 |
|
Node res = eq[1].eqNode(eq[0].notNode()); |
492 |
|
TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr); |
493 |
|
return ppAssert(tn, outSubstitutions); |
494 |
|
} |
495 |
|
} |
496 |
|
|
497 |
35771 |
return PP_ASSERT_STATUS_UNSOLVED; |
498 |
|
} |
499 |
|
|
500 |
|
std::pair<bool, Node> Theory::entailmentCheck(TNode lit) |
501 |
|
{ |
502 |
|
return make_pair(false, Node::null()); |
503 |
|
} |
504 |
|
|
505 |
41697 |
void Theory::addCarePair(TNode t1, TNode t2) { |
506 |
41697 |
if (d_careGraph) { |
507 |
41697 |
d_careGraph->insert(CarePair(t1, t2, d_id)); |
508 |
|
} |
509 |
41697 |
} |
510 |
|
|
511 |
68124 |
void Theory::getCareGraph(CareGraph* careGraph) { |
512 |
68124 |
Assert(careGraph != NULL); |
513 |
|
|
514 |
68124 |
Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; |
515 |
136248 |
TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); |
516 |
68124 |
d_careGraph = careGraph; |
517 |
68124 |
computeCareGraph(); |
518 |
68124 |
d_careGraph = NULL; |
519 |
68124 |
} |
520 |
|
|
521 |
|
bool Theory::proofsEnabled() const |
522 |
|
{ |
523 |
|
return d_env.getProofNodeManager() != nullptr; |
524 |
|
} |
525 |
|
|
526 |
20137 |
EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) |
527 |
|
{ |
528 |
|
// if not using an equality engine, then by default we don't know the status |
529 |
20137 |
if (d_equalityEngine == nullptr) |
530 |
|
{ |
531 |
5768 |
return EQUALITY_UNKNOWN; |
532 |
|
} |
533 |
14369 |
Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl; |
534 |
14369 |
Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); |
535 |
|
|
536 |
|
// Check for equality (simplest) |
537 |
14369 |
if (d_equalityEngine->areEqual(a, b)) |
538 |
|
{ |
539 |
|
// The terms are implied to be equal |
540 |
7261 |
return EQUALITY_TRUE; |
541 |
|
} |
542 |
|
|
543 |
|
// Check for disequality |
544 |
7108 |
if (d_equalityEngine->areDisequal(a, b, false)) |
545 |
|
{ |
546 |
|
// The terms are implied to be dis-equal |
547 |
2572 |
return EQUALITY_FALSE; |
548 |
|
} |
549 |
|
|
550 |
|
// All other terms are unknown, which is conservative. A theory may override |
551 |
|
// this method if it knows more information. |
552 |
4536 |
return EQUALITY_UNKNOWN; |
553 |
|
} |
554 |
|
|
555 |
14182761 |
void Theory::check(Effort level) |
556 |
|
{ |
557 |
|
// see if we are already done (as an optimization) |
558 |
14182761 |
if (done() && level < EFFORT_FULL) |
559 |
|
{ |
560 |
18619020 |
return; |
561 |
|
} |
562 |
4873251 |
Assert(d_theoryState!=nullptr); |
563 |
|
// standard calls for resource, stats |
564 |
4873251 |
d_out->spendResource(Resource::TheoryCheckStep); |
565 |
9746502 |
TimerStat::CodeTimer checkTimer(d_checkTime); |
566 |
9746502 |
Trace("theory-check") << "Theory::preCheck " << level << " " << d_id |
567 |
4873251 |
<< std::endl; |
568 |
|
// pre-check at level |
569 |
4873251 |
if (preCheck(level)) |
570 |
|
{ |
571 |
|
// check aborted for a theory-specific reason |
572 |
|
return; |
573 |
|
} |
574 |
4873251 |
Assert(d_theoryState != nullptr); |
575 |
4873251 |
Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl; |
576 |
|
// process the pending fact queue |
577 |
33080287 |
while (!done() && !d_theoryState->isInConflict()) |
578 |
|
{ |
579 |
|
// Get the next assertion from the fact queue |
580 |
22449445 |
Assertion assertion = get(); |
581 |
22449445 |
TNode fact = assertion.d_assertion; |
582 |
28207042 |
Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id |
583 |
14103521 |
<< std::endl; |
584 |
14103521 |
bool polarity = fact.getKind() != kind::NOT; |
585 |
22449445 |
TNode atom = polarity ? fact : fact[0]; |
586 |
|
// call the pre-notify method |
587 |
14103521 |
if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false)) |
588 |
|
{ |
589 |
|
// handled in theory-specific way that doesn't involve equality engine |
590 |
5757597 |
continue; |
591 |
|
} |
592 |
16691848 |
Trace("theory-check") << "Theory::assert " << fact << " " << d_id |
593 |
8345924 |
<< std::endl; |
594 |
|
// Theories that don't have an equality engine should always return true |
595 |
|
// for preNotifyFact |
596 |
8345924 |
Assert(d_equalityEngine != nullptr); |
597 |
|
// assert to the equality engine |
598 |
8345924 |
if (atom.getKind() == kind::EQUAL) |
599 |
|
{ |
600 |
6006354 |
d_equalityEngine->assertEquality(atom, polarity, fact); |
601 |
|
} |
602 |
|
else |
603 |
|
{ |
604 |
2339573 |
d_equalityEngine->assertPredicate(atom, polarity, fact); |
605 |
|
} |
606 |
16691842 |
Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id |
607 |
8345921 |
<< std::endl; |
608 |
|
// notify the theory of the new fact, which is not internal |
609 |
8345921 |
notifyFact(atom, polarity, fact, false); |
610 |
|
} |
611 |
4873248 |
Trace("theory-check") << "Theory::postCheck " << d_id << std::endl; |
612 |
|
// post-check at level |
613 |
4873248 |
postCheck(level); |
614 |
4873247 |
Trace("theory-check") << "Theory::finish check " << d_id << std::endl; |
615 |
|
} |
616 |
|
|
617 |
1843143 |
bool Theory::preCheck(Effort level) { return false; } |
618 |
|
|
619 |
2 |
void Theory::postCheck(Effort level) {} |
620 |
|
|
621 |
4902327 |
bool Theory::preNotifyFact( |
622 |
|
TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) |
623 |
|
{ |
624 |
4902327 |
return false; |
625 |
|
} |
626 |
|
|
627 |
6814 |
void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal) |
628 |
|
{ |
629 |
6814 |
} |
630 |
|
|
631 |
22132 |
void Theory::preRegisterTerm(TNode node) {} |
632 |
|
|
633 |
1647106 |
void Theory::addSharedTerm(TNode n) |
634 |
|
{ |
635 |
3294212 |
Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" |
636 |
1647106 |
<< std::endl; |
637 |
3294212 |
Debug("theory::assertions") |
638 |
1647106 |
<< "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; |
639 |
1647106 |
d_sharedTerms.push_back(n); |
640 |
|
// now call theory-specific method notifySharedTerm |
641 |
1647106 |
notifySharedTerm(n); |
642 |
|
// if we have an equality engine, add the trigger term |
643 |
1647106 |
if (d_equalityEngine != nullptr) |
644 |
|
{ |
645 |
1641607 |
d_equalityEngine->addTriggerTerm(n, d_id); |
646 |
|
} |
647 |
1647106 |
} |
648 |
|
|
649 |
372693 |
eq::EqualityEngine* Theory::getEqualityEngine() |
650 |
|
{ |
651 |
|
// get the assigned equality engine, which is a pointer stored in this class |
652 |
372693 |
return d_equalityEngine; |
653 |
|
} |
654 |
|
|
655 |
350 |
bool Theory::usesCentralEqualityEngine() const |
656 |
|
{ |
657 |
350 |
return usesCentralEqualityEngine(d_id); |
658 |
|
} |
659 |
|
|
660 |
25955400 |
bool Theory::usesCentralEqualityEngine(TheoryId id) |
661 |
|
{ |
662 |
25955400 |
if (id == THEORY_BUILTIN) |
663 |
|
{ |
664 |
9935210 |
return true; |
665 |
|
} |
666 |
16020190 |
if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) |
667 |
|
{ |
668 |
16002480 |
return false; |
669 |
|
} |
670 |
17710 |
if (id == THEORY_ARITH) |
671 |
|
{ |
672 |
|
// conditional on whether we are using the equality solver |
673 |
70 |
return options::arithEqSolver(); |
674 |
|
} |
675 |
16662 |
return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS |
676 |
10048 |
|| id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS |
677 |
27112 |
|| id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV; |
678 |
|
} |
679 |
|
|
680 |
29890581 |
bool Theory::expUsingCentralEqualityEngine(TheoryId id) |
681 |
|
{ |
682 |
29890581 |
return id != THEORY_ARITH && usesCentralEqualityEngine(id); |
683 |
|
} |
684 |
|
|
685 |
|
} // namespace theory |
686 |
29349 |
} // namespace cvc5 |