Branch data Line data Source code
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-2024 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::internal {
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 : 49172 : SharedSolver::SharedSolver(Env& env, TheoryEngine& te)
34 : : : EnvObj(env),
35 : : d_te(te),
36 : 98344 : d_logicInfo(logicInfo()),
37 : 49172 : d_sharedTerms(env, &d_te),
38 : : d_preRegistrationVisitor(env, &te),
39 : 49172 : d_sharedTermsVisitor(env, &te, d_sharedTerms),
40 : 49172 : d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager())
41 : : {
42 : 49172 : }
43 : :
44 : 0 : bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi)
45 : : {
46 : 0 : return false;
47 : : }
48 : :
49 : 2147970 : void SharedSolver::preRegister(TNode atom)
50 : : {
51 [ + - ]: 2147970 : 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 [ + + ]: 2147970 : 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 : 1775040 : 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 : 1775010 : preRegisterSharedInternal(atom);
73 : : }
74 : : else
75 : : {
76 : : // just use the normal preregister visitor, which calls
77 : : // Theory::preRegisterTerm possibly multiple times.
78 : 372943 : NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom);
79 : : }
80 [ + - ]: 2147950 : Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl;
81 : 2147950 : }
82 : :
83 : 15515200 : void SharedSolver::preNotifySharedFact(TNode atom)
84 : : {
85 [ + + ]: 15515200 : if (d_sharedTerms.hasSharedTerms(atom))
86 : : {
87 : : // Always notify the theories of the shared terms, which is independent of
88 : : // the architecture currently.
89 : 8943620 : SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
90 : 8943620 : SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
91 [ + + ]: 31698900 : for (; it != it_end; ++it)
92 : : {
93 : 22755300 : TNode term = *it;
94 : 22755300 : TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term);
95 [ + + ]: 341329000 : for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id)
96 : : {
97 [ + + ]: 318574000 : if (TheoryIdSetUtil::setContains(id, theories))
98 : : {
99 : 3506930 : Theory* t = d_te.theoryOf(id);
100 : : // call the add shared term method
101 : 3506930 : t->addSharedTerm(term);
102 : : }
103 : : }
104 : 22755300 : d_sharedTerms.markNotified(term, theories);
105 : : }
106 : : }
107 : 15515200 : }
108 : :
109 : 0 : EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b)
110 : : {
111 : 0 : return EQUALITY_UNKNOWN;
112 : : }
113 : :
114 : 6922 : bool SharedSolver::propagateLit(TNode predicate, bool value)
115 : : {
116 [ + + ]: 6922 : if (value)
117 : : {
118 : 4779 : return d_im->propagateLit(predicate);
119 : : }
120 : 2143 : return d_im->propagateLit(predicate.notNode());
121 : : }
122 : :
123 : 2254 : 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 : : // As an optimization, we ensure the equality is oriented based on the
130 : : // same order used by the rewriter for equality.
131 [ - + ]: 2254 : Node equality = a>b ? b.eqNode(a) : a.eqNode(b);
132 [ + + ]: 2254 : if (value)
133 : : {
134 : 1743 : d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN);
135 : : }
136 : : else
137 : : {
138 : 1022 : d_te.assertToTheory(
139 : 1533 : equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
140 : : }
141 : 4508 : return true;
142 : : }
143 : :
144 : 10558 : bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); }
145 : :
146 : 93207 : void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo, InferenceId id)
147 : : {
148 : : // Do we need to check atoms
149 [ + - ]: 93207 : if (atomsTo != theory::THEORY_LAST)
150 : : {
151 : 93207 : d_te.ensureLemmaAtoms(trn.getNode(), atomsTo);
152 : : }
153 : 93207 : d_im->trustedLemma(trn, id);
154 : 93207 : }
155 : :
156 : 21 : void SharedSolver::sendConflict(TrustNode trn, InferenceId id)
157 : : {
158 : 21 : d_im->trustedConflict(trn, id);
159 : 21 : }
160 : :
161 : : } // namespace theory
162 : : } // namespace cvc5::internal
|
