1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* The shared solver base class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/shared_solver.h" |
17 |
|
|
18 |
|
#include "expr/node_visitor.h" |
19 |
|
#include "theory/ee_setup_info.h" |
20 |
|
#include "theory/logic_info.h" |
21 |
|
#include "theory/theory_engine.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
|
26 |
|
// Always creates shared terms database. In all cases, shared terms |
27 |
|
// database is used as a way of tracking which calls to Theory::addSharedTerm |
28 |
|
// we need to make in preNotifySharedFact. |
29 |
|
// In distributed equality engine management, shared terms database also |
30 |
|
// maintains an equality engine. In central equality engine management, |
31 |
|
// it does not. |
32 |
9460 |
SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm) |
33 |
|
: d_te(te), |
34 |
9460 |
d_logicInfo(te.getLogicInfo()), |
35 |
28380 |
d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm), |
36 |
9460 |
d_preRegistrationVisitor(&te, d_te.getSatContext()), |
37 |
56760 |
d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext()) |
38 |
|
{ |
39 |
9460 |
} |
40 |
|
|
41 |
|
bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi) |
42 |
|
{ |
43 |
|
return false; |
44 |
|
} |
45 |
|
|
46 |
893253 |
void SharedSolver::preRegister(TNode atom) |
47 |
|
{ |
48 |
893253 |
Trace("theory") << "SharedSolver::preRegister atom " << atom << std::endl; |
49 |
|
// This method uses two different implementations for preregistering terms, |
50 |
|
// which depends on whether sharing is enabled. |
51 |
|
// If sharing is disabled, we use PreRegisterVisitor, which keeps a global |
52 |
|
// SAT-context dependent cache of terms visited. |
53 |
|
// If sharing is disabled, we use SharedTermsVisitor which does *not* keep a |
54 |
|
// global cache. This is because shared terms must be associated with the |
55 |
|
// given atom, and thus it must traverse the set of subterms in each atom. |
56 |
|
// See term_registration_visitor.h for more details. |
57 |
893253 |
if (d_logicInfo.isSharingEnabled()) |
58 |
|
{ |
59 |
|
// register it with the shared terms database if sharing is enabled |
60 |
757307 |
preRegisterSharedInternal(atom); |
61 |
|
// Collect the shared terms in atom, as well as calling preregister on the |
62 |
|
// appropriate theories in atom. |
63 |
|
// This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly |
64 |
|
// multiple times. |
65 |
757310 |
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom); |
66 |
|
} |
67 |
|
else |
68 |
|
{ |
69 |
|
// just use the normal preregister visitor, which calls |
70 |
|
// Theory::preRegisterTerm possibly multiple times. |
71 |
135947 |
NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom); |
72 |
|
} |
73 |
893249 |
Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl; |
74 |
893249 |
} |
75 |
|
|
76 |
6630106 |
void SharedSolver::preNotifySharedFact(TNode atom) |
77 |
|
{ |
78 |
6630106 |
if (d_sharedTerms.hasSharedTerms(atom)) |
79 |
|
{ |
80 |
|
// Always notify the theories of the shared terms, which is independent of |
81 |
|
// the architecture currently. |
82 |
4119610 |
SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); |
83 |
4119610 |
SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); |
84 |
27475148 |
for (; it != it_end; ++it) |
85 |
|
{ |
86 |
23355538 |
TNode term = *it; |
87 |
11677769 |
TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term); |
88 |
163488766 |
for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) |
89 |
|
{ |
90 |
151810997 |
if (TheoryIdSetUtil::setContains(id, theories)) |
91 |
|
{ |
92 |
1693044 |
Theory* t = d_te.theoryOf(id); |
93 |
|
// call the add shared term method |
94 |
1693044 |
t->addSharedTerm(term); |
95 |
|
} |
96 |
|
} |
97 |
11677769 |
d_sharedTerms.markNotified(term, theories); |
98 |
|
} |
99 |
|
} |
100 |
6630106 |
} |
101 |
|
|
102 |
|
EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b) |
103 |
|
{ |
104 |
|
return EQUALITY_UNKNOWN; |
105 |
|
} |
106 |
|
|
107 |
|
void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo) |
108 |
|
{ |
109 |
|
d_te.lemma(trn, LemmaProperty::NONE, atomsTo); |
110 |
|
} |
111 |
|
|
112 |
|
bool SharedSolver::propagateSharedEquality(theory::TheoryId theory, |
113 |
|
TNode a, |
114 |
|
TNode b, |
115 |
|
bool value) |
116 |
|
{ |
117 |
|
// Propagate equality between shared terms to the one who asked for it |
118 |
|
Node equality = a.eqNode(b); |
119 |
|
if (value) |
120 |
|
{ |
121 |
|
d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN); |
122 |
|
} |
123 |
|
else |
124 |
|
{ |
125 |
|
d_te.assertToTheory( |
126 |
|
equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN); |
127 |
|
} |
128 |
|
return true; |
129 |
|
} |
130 |
|
|
131 |
4654 |
bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); } |
132 |
|
|
133 |
|
} // namespace theory |
134 |
28194 |
} // namespace cvc5 |