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 |
9926 |
SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm) |
34 |
|
: d_te(te), |
35 |
9926 |
d_logicInfo(te.getLogicInfo()), |
36 |
29778 |
d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm), |
37 |
9926 |
d_preRegistrationVisitor(&te, d_te.getSatContext()), |
38 |
9926 |
d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext()), |
39 |
69482 |
d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager()) |
40 |
|
{ |
41 |
9926 |
} |
42 |
|
|
43 |
|
bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi) |
44 |
|
{ |
45 |
|
return false; |
46 |
|
} |
47 |
|
|
48 |
1077096 |
void SharedSolver::preRegister(TNode atom) |
49 |
|
{ |
50 |
1077096 |
Trace("theory") << "SharedSolver::preRegister atom " << atom << std::endl; |
51 |
|
// This method uses two different implementations for preregistering terms, |
52 |
|
// which depends on whether sharing is enabled. |
53 |
|
// If sharing is disabled, we use PreRegisterVisitor, which keeps a global |
54 |
|
// SAT-context dependent cache of terms visited. |
55 |
|
// If sharing is disabled, we use SharedTermsVisitor which does *not* keep a |
56 |
|
// global cache. This is because shared terms must be associated with the |
57 |
|
// given atom, and thus it must traverse the set of subterms in each atom. |
58 |
|
// See term_registration_visitor.h for more details. |
59 |
1077096 |
if (d_logicInfo.isSharingEnabled()) |
60 |
|
{ |
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 |
871684 |
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom); |
66 |
|
// Register it with the shared terms database if sharing is enabled. |
67 |
|
// Notice that this must come *after* the above call, since we must ensure |
68 |
|
// that all subterms of atom have already been added to the central |
69 |
|
// equality engine before atom is added. This avoids spurious notifications |
70 |
|
// from the equality engine. |
71 |
871678 |
preRegisterSharedInternal(atom); |
72 |
|
} |
73 |
|
else |
74 |
|
{ |
75 |
|
// just use the normal preregister visitor, which calls |
76 |
|
// Theory::preRegisterTerm possibly multiple times. |
77 |
205416 |
NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom); |
78 |
|
} |
79 |
1077092 |
Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl; |
80 |
1077092 |
} |
81 |
|
|
82 |
7878596 |
void SharedSolver::preNotifySharedFact(TNode atom) |
83 |
|
{ |
84 |
7878596 |
if (d_sharedTerms.hasSharedTerms(atom)) |
85 |
|
{ |
86 |
|
// Always notify the theories of the shared terms, which is independent of |
87 |
|
// the architecture currently. |
88 |
5162574 |
SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); |
89 |
5162574 |
SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); |
90 |
31714814 |
for (; it != it_end; ++it) |
91 |
|
{ |
92 |
26552240 |
TNode term = *it; |
93 |
13276120 |
TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term); |
94 |
185865680 |
for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) |
95 |
|
{ |
96 |
172589560 |
if (TheoryIdSetUtil::setContains(id, theories)) |
97 |
|
{ |
98 |
1895708 |
Theory* t = d_te.theoryOf(id); |
99 |
|
// call the add shared term method |
100 |
1895708 |
t->addSharedTerm(term); |
101 |
|
} |
102 |
|
} |
103 |
13276120 |
d_sharedTerms.markNotified(term, theories); |
104 |
|
} |
105 |
|
} |
106 |
7878596 |
} |
107 |
|
|
108 |
|
EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b) |
109 |
|
{ |
110 |
|
return EQUALITY_UNKNOWN; |
111 |
|
} |
112 |
|
|
113 |
14928 |
bool SharedSolver::propagateLit(TNode predicate, bool value) |
114 |
|
{ |
115 |
14928 |
if (value) |
116 |
|
{ |
117 |
13553 |
return d_im->propagateLit(predicate); |
118 |
|
} |
119 |
1375 |
return d_im->propagateLit(predicate.notNode()); |
120 |
|
} |
121 |
|
|
122 |
4757 |
bool SharedSolver::propagateSharedEquality(theory::TheoryId theory, |
123 |
|
TNode a, |
124 |
|
TNode b, |
125 |
|
bool value) |
126 |
|
{ |
127 |
|
// Propagate equality between shared terms to the one who asked for it |
128 |
9514 |
Node equality = a.eqNode(b); |
129 |
4757 |
if (value) |
130 |
|
{ |
131 |
4458 |
d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN); |
132 |
|
} |
133 |
|
else |
134 |
|
{ |
135 |
1196 |
d_te.assertToTheory( |
136 |
1196 |
equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN); |
137 |
|
} |
138 |
9514 |
return true; |
139 |
|
} |
140 |
|
|
141 |
4619 |
bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); } |
142 |
|
|
143 |
39314 |
void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo, InferenceId id) |
144 |
|
{ |
145 |
|
// Do we need to check atoms |
146 |
39314 |
if (atomsTo != theory::THEORY_LAST) |
147 |
|
{ |
148 |
39314 |
d_te.ensureLemmaAtoms(trn.getNode(), atomsTo); |
149 |
|
} |
150 |
39314 |
d_im->trustedLemma(trn, id); |
151 |
39314 |
} |
152 |
|
|
153 |
28 |
void SharedSolver::sendConflict(TrustNode trn, InferenceId id) |
154 |
|
{ |
155 |
28 |
d_im->trustedConflict(trn, id); |
156 |
28 |
} |
157 |
|
|
158 |
|
} // namespace theory |
159 |
29502 |
} // namespace cvc5 |