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 |
9838 |
SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm) |
33 |
|
: d_te(te), |
34 |
9838 |
d_logicInfo(te.getLogicInfo()), |
35 |
29514 |
d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm), |
36 |
9838 |
d_preRegistrationVisitor(&te, d_te.getSatContext()), |
37 |
9838 |
d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext()), |
38 |
68866 |
d_out(te.theoryOf(THEORY_BUILTIN)->getOutputChannel()) |
39 |
|
{ |
40 |
9838 |
} |
41 |
|
|
42 |
|
bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi) |
43 |
|
{ |
44 |
|
return false; |
45 |
|
} |
46 |
|
|
47 |
1065278 |
void SharedSolver::preRegister(TNode atom) |
48 |
|
{ |
49 |
1065278 |
Trace("theory") << "SharedSolver::preRegister atom " << atom << std::endl; |
50 |
|
// This method uses two different implementations for preregistering terms, |
51 |
|
// which depends on whether sharing is enabled. |
52 |
|
// If sharing is disabled, we use PreRegisterVisitor, which keeps a global |
53 |
|
// SAT-context dependent cache of terms visited. |
54 |
|
// If sharing is disabled, we use SharedTermsVisitor which does *not* keep a |
55 |
|
// global cache. This is because shared terms must be associated with the |
56 |
|
// given atom, and thus it must traverse the set of subterms in each atom. |
57 |
|
// See term_registration_visitor.h for more details. |
58 |
1065278 |
if (d_logicInfo.isSharingEnabled()) |
59 |
|
{ |
60 |
|
// Collect the shared terms in atom, as well as calling preregister on the |
61 |
|
// appropriate theories in atom. |
62 |
|
// This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly |
63 |
|
// multiple times. |
64 |
832186 |
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom); |
65 |
|
// Register it with the shared terms database if sharing is enabled. |
66 |
|
// Notice that this must come *after* the above call, since we must ensure |
67 |
|
// that all subterms of atom have already been added to the central |
68 |
|
// equality engine before atom is added. This avoids spurious notifications |
69 |
|
// from the equality engine. |
70 |
832180 |
preRegisterSharedInternal(atom); |
71 |
|
} |
72 |
|
else |
73 |
|
{ |
74 |
|
// just use the normal preregister visitor, which calls |
75 |
|
// Theory::preRegisterTerm possibly multiple times. |
76 |
233096 |
NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom); |
77 |
|
} |
78 |
1065274 |
Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl; |
79 |
1065274 |
} |
80 |
|
|
81 |
6975203 |
void SharedSolver::preNotifySharedFact(TNode atom) |
82 |
|
{ |
83 |
6975203 |
if (d_sharedTerms.hasSharedTerms(atom)) |
84 |
|
{ |
85 |
|
// Always notify the theories of the shared terms, which is independent of |
86 |
|
// the architecture currently. |
87 |
4413855 |
SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); |
88 |
4413855 |
SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); |
89 |
27824613 |
for (; it != it_end; ++it) |
90 |
|
{ |
91 |
23410758 |
TNode term = *it; |
92 |
11705379 |
TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term); |
93 |
163875306 |
for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) |
94 |
|
{ |
95 |
152169927 |
if (TheoryIdSetUtil::setContains(id, theories)) |
96 |
|
{ |
97 |
1646650 |
Theory* t = d_te.theoryOf(id); |
98 |
|
// call the add shared term method |
99 |
1646650 |
t->addSharedTerm(term); |
100 |
|
} |
101 |
|
} |
102 |
11705379 |
d_sharedTerms.markNotified(term, theories); |
103 |
|
} |
104 |
|
} |
105 |
6975203 |
} |
106 |
|
|
107 |
|
EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b) |
108 |
|
{ |
109 |
|
return EQUALITY_UNKNOWN; |
110 |
|
} |
111 |
|
|
112 |
38798 |
bool SharedSolver::propagateLit(TNode predicate, bool value) |
113 |
|
{ |
114 |
38798 |
if (value) |
115 |
|
{ |
116 |
35249 |
return d_out.propagate(predicate); |
117 |
|
} |
118 |
3549 |
return d_out.propagate(predicate.notNode()); |
119 |
|
} |
120 |
|
|
121 |
11963 |
bool SharedSolver::propagateSharedEquality(theory::TheoryId theory, |
122 |
|
TNode a, |
123 |
|
TNode b, |
124 |
|
bool value) |
125 |
|
{ |
126 |
|
// Propagate equality between shared terms to the one who asked for it |
127 |
23926 |
Node equality = a.eqNode(b); |
128 |
11963 |
if (value) |
129 |
|
{ |
130 |
11258 |
d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN); |
131 |
|
} |
132 |
|
else |
133 |
|
{ |
134 |
2820 |
d_te.assertToTheory( |
135 |
2820 |
equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN); |
136 |
|
} |
137 |
23926 |
return true; |
138 |
|
} |
139 |
|
|
140 |
4488 |
bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); } |
141 |
|
|
142 |
30166 |
void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo, InferenceId id) |
143 |
|
{ |
144 |
30166 |
Trace("im") << "(lemma " << id << " " << trn.getProven() << ")" << std::endl; |
145 |
30166 |
d_te.lemma(trn, LemmaProperty::NONE, atomsTo); |
146 |
30166 |
} |
147 |
|
|
148 |
36 |
void SharedSolver::sendConflict(TrustNode trn) { d_out.trustedConflict(trn); } |
149 |
|
|
150 |
|
} // namespace theory |
151 |
29280 |
} // namespace cvc5 |