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 |
|
#include "theory/theory_inference_manager.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
|
27 |
|
// Always creates shared terms database. In all cases, shared terms |
28 |
|
// database is used as a way of tracking which calls to Theory::addSharedTerm |
29 |
|
// we need to make in preNotifySharedFact. |
30 |
|
// In distributed equality engine management, shared terms database also |
31 |
|
// maintains an equality engine. In central equality engine management, |
32 |
|
// it does not. |
33 |
15273 |
SharedSolver::SharedSolver(Env& env, TheoryEngine& te) |
34 |
|
: EnvObj(env), |
35 |
|
d_te(te), |
36 |
15273 |
d_logicInfo(logicInfo()), |
37 |
15273 |
d_sharedTerms(env, &d_te), |
38 |
|
d_preRegistrationVisitor(env, &te), |
39 |
|
d_sharedTermsVisitor(env, &te, d_sharedTerms), |
40 |
45819 |
d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager()) |
41 |
|
{ |
42 |
15273 |
} |
43 |
|
|
44 |
|
bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi) |
45 |
|
{ |
46 |
|
return false; |
47 |
|
} |
48 |
|
|
49 |
1218861 |
void SharedSolver::preRegister(TNode atom) |
50 |
|
{ |
51 |
1218861 |
Trace("theory") << "SharedSolver::preRegister atom " << atom << std::endl; |
52 |
|
// This method uses two different implementations for preregistering terms, |
53 |
|
// which depends on whether sharing is enabled. |
54 |
|
// If sharing is disabled, we use PreRegisterVisitor, which keeps a global |
55 |
|
// SAT-context dependent cache of terms visited. |
56 |
|
// If sharing is disabled, we use SharedTermsVisitor which does *not* keep a |
57 |
|
// global cache. This is because shared terms must be associated with the |
58 |
|
// given atom, and thus it must traverse the set of subterms in each atom. |
59 |
|
// See term_registration_visitor.h for more details. |
60 |
1218861 |
if (d_logicInfo.isSharingEnabled()) |
61 |
|
{ |
62 |
|
// Collect the shared terms in atom, as well as calling preregister on the |
63 |
|
// appropriate theories in atom. |
64 |
|
// This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly |
65 |
|
// multiple times. |
66 |
1006908 |
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom); |
67 |
|
// Register it with the shared terms database if sharing is enabled. |
68 |
|
// Notice that this must come *after* the above call, since we must ensure |
69 |
|
// that all subterms of atom have already been added to the central |
70 |
|
// equality engine before atom is added. This avoids spurious notifications |
71 |
|
// from the equality engine. |
72 |
1006902 |
preRegisterSharedInternal(atom); |
73 |
|
} |
74 |
|
else |
75 |
|
{ |
76 |
|
// just use the normal preregister visitor, which calls |
77 |
|
// Theory::preRegisterTerm possibly multiple times. |
78 |
211957 |
NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom); |
79 |
|
} |
80 |
1218857 |
Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl; |
81 |
1218857 |
} |
82 |
|
|
83 |
11637586 |
void SharedSolver::preNotifySharedFact(TNode atom) |
84 |
|
{ |
85 |
11637586 |
if (d_sharedTerms.hasSharedTerms(atom)) |
86 |
|
{ |
87 |
|
// Always notify the theories of the shared terms, which is independent of |
88 |
|
// the architecture currently. |
89 |
8215500 |
SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); |
90 |
8215500 |
SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); |
91 |
49432580 |
for (; it != it_end; ++it) |
92 |
|
{ |
93 |
41217080 |
TNode term = *it; |
94 |
20608540 |
TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term); |
95 |
288519560 |
for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) |
96 |
|
{ |
97 |
267911020 |
if (TheoryIdSetUtil::setContains(id, theories)) |
98 |
|
{ |
99 |
2570273 |
Theory* t = d_te.theoryOf(id); |
100 |
|
// call the add shared term method |
101 |
2570273 |
t->addSharedTerm(term); |
102 |
|
} |
103 |
|
} |
104 |
20608540 |
d_sharedTerms.markNotified(term, theories); |
105 |
|
} |
106 |
|
} |
107 |
11637586 |
} |
108 |
|
|
109 |
|
EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b) |
110 |
|
{ |
111 |
|
return EQUALITY_UNKNOWN; |
112 |
|
} |
113 |
|
|
114 |
22356 |
bool SharedSolver::propagateLit(TNode predicate, bool value) |
115 |
|
{ |
116 |
22356 |
if (value) |
117 |
|
{ |
118 |
20309 |
return d_im->propagateLit(predicate); |
119 |
|
} |
120 |
2047 |
return d_im->propagateLit(predicate.notNode()); |
121 |
|
} |
122 |
|
|
123 |
7105 |
bool SharedSolver::propagateSharedEquality(theory::TheoryId theory, |
124 |
|
TNode a, |
125 |
|
TNode b, |
126 |
|
bool value) |
127 |
|
{ |
128 |
|
// Propagate equality between shared terms to the one who asked for it |
129 |
14210 |
Node equality = a.eqNode(b); |
130 |
7105 |
if (value) |
131 |
|
{ |
132 |
6686 |
d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN); |
133 |
|
} |
134 |
|
else |
135 |
|
{ |
136 |
1676 |
d_te.assertToTheory( |
137 |
1676 |
equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN); |
138 |
|
} |
139 |
14210 |
return true; |
140 |
|
} |
141 |
|
|
142 |
4527 |
bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); } |
143 |
|
|
144 |
39922 |
void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo, InferenceId id) |
145 |
|
{ |
146 |
|
// Do we need to check atoms |
147 |
39922 |
if (atomsTo != theory::THEORY_LAST) |
148 |
|
{ |
149 |
39922 |
d_te.ensureLemmaAtoms(trn.getNode(), atomsTo); |
150 |
|
} |
151 |
39922 |
d_im->trustedLemma(trn, id); |
152 |
39922 |
} |
153 |
|
|
154 |
34 |
void SharedSolver::sendConflict(TrustNode trn, InferenceId id) |
155 |
|
{ |
156 |
34 |
d_im->trustedConflict(trn, id); |
157 |
34 |
} |
158 |
|
|
159 |
|
} // namespace theory |
160 |
31137 |
} // namespace cvc5 |