Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The shared solver base class.
11 : : */
12 : :
13 : : #include "theory/shared_solver.h"
14 : :
15 : : #include "expr/node_visitor.h"
16 : : #include "theory/ee_setup_info.h"
17 : : #include "theory/logic_info.h"
18 : : #include "theory/theory_engine.h"
19 : : #include "theory/theory_inference_manager.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : :
24 : : // Always creates shared terms database. In all cases, shared terms
25 : : // database is used as a way of tracking which calls to Theory::addSharedTerm
26 : : // we need to make in preNotifySharedFact.
27 : : // In distributed equality engine management, shared terms database also
28 : : // maintains an equality engine. In central equality engine management,
29 : : // it does not.
30 : 28664 : SharedSolver::SharedSolver(Env& env, TheoryEngine& te)
31 : : : EnvObj(env),
32 : 28664 : d_te(te),
33 : 57328 : d_logicInfo(logicInfo()),
34 : 28664 : d_sharedTerms(env, &d_te),
35 : 28664 : d_preRegistrationVisitor(env, &te),
36 : 28664 : d_sharedTermsVisitor(env, &te, d_sharedTerms),
37 : 57328 : d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager())
38 : : {
39 : 28664 : }
40 : :
41 : 0 : bool SharedSolver::needsEqualityEngine(CVC5_UNUSED theory::EeSetupInfo& esi)
42 : : {
43 : 0 : return false;
44 : : }
45 : :
46 : 2144309 : void SharedSolver::preRegister(TNode atom)
47 : : {
48 [ + - ]: 2144309 : 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 [ + + ]: 2144309 : if (d_logicInfo.isSharingEnabled())
58 : : {
59 : : // Collect the shared terms in atom, as well as calling preregister on the
60 : : // appropriate theories in atom.
61 : : // This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly
62 : : // multiple times.
63 : 1827871 : NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom);
64 : : // Register it with the shared terms database if sharing is enabled.
65 : : // Notice that this must come *after* the above call, since we must ensure
66 : : // that all subterms of atom have already been added to the central
67 : : // equality engine before atom is added. This avoids spurious notifications
68 : : // from the equality engine.
69 : 1827843 : preRegisterSharedInternal(atom);
70 : : }
71 : : else
72 : : {
73 : : // just use the normal preregister visitor, which calls
74 : : // Theory::preRegisterTerm possibly multiple times.
75 : 316454 : NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom);
76 : : }
77 [ + - ]: 2144293 : Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl;
78 : 2144293 : }
79 : :
80 : 16362810 : void SharedSolver::preNotifySharedFact(TNode atom)
81 : : {
82 [ + + ]: 16362810 : if (d_sharedTerms.hasSharedTerms(atom))
83 : : {
84 : : // Always notify the theories of the shared terms, which is independent of
85 : : // the architecture currently.
86 : 10666136 : SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
87 : 10666136 : SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
88 [ + + ]: 40871282 : for (; it != it_end; ++it)
89 : : {
90 : 30205147 : TNode term = *it;
91 : 30205147 : TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term);
92 [ + + ]: 453077203 : for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id)
93 : : {
94 [ + + ]: 422872057 : if (TheoryIdSetUtil::setContains(id, theories))
95 : : {
96 : 3849433 : Theory* t = d_te.theoryOf(id);
97 : : // call the add shared term method
98 : 3849434 : t->addSharedTerm(term);
99 : : }
100 : : }
101 : 30205146 : d_sharedTerms.markNotified(term, theories);
102 : 30205147 : }
103 : : }
104 : 16362809 : }
105 : :
106 : 0 : EqualityStatus SharedSolver::getEqualityStatus(CVC5_UNUSED TNode a,
107 : : CVC5_UNUSED TNode b)
108 : : {
109 : 0 : return EQUALITY_UNKNOWN;
110 : : }
111 : :
112 : 15541 : bool SharedSolver::propagateLit(TNode predicate, bool value)
113 : : {
114 [ + + ]: 15541 : if (value)
115 : : {
116 : 11116 : return d_im->propagateLit(predicate);
117 : : }
118 : 4425 : return d_im->propagateLit(predicate.notNode());
119 : : }
120 : :
121 : 6526 : 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 : : // As an optimization, we ensure the equality is oriented based on the
128 : : // same order used by the rewriter for equality.
129 [ - + ]: 6526 : Node equality = a > b ? b.eqNode(a) : a.eqNode(b);
130 [ + + ]: 6526 : if (value)
131 : : {
132 : 5010 : d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN);
133 : : }
134 : : else
135 : : {
136 : : // Use negatedEquality to ensure deterministic node ID assignments
137 : 1516 : Node negatedEquality = equality.notNode();
138 : 1516 : d_te.assertToTheory(
139 : : negatedEquality, negatedEquality, theory, THEORY_BUILTIN);
140 : 1516 : }
141 : 6526 : return true;
142 : 6526 : }
143 : :
144 : 12464 : bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); }
145 : :
146 : 80423 : void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo, InferenceId id)
147 : : {
148 : : // Do we need to check atoms
149 [ + - ]: 80423 : if (atomsTo != theory::THEORY_LAST)
150 : : {
151 : 80423 : d_te.ensureLemmaAtoms(trn.getNode(), atomsTo);
152 : : }
153 : 80423 : d_im->trustedLemma(trn, id);
154 : 80423 : }
155 : :
156 : 20 : void SharedSolver::sendConflict(TrustNode trn, InferenceId id)
157 : : {
158 : 20 : d_im->trustedConflict(trn, id);
159 : 20 : }
160 : :
161 : : } // namespace theory
162 : : } // namespace cvc5::internal
|
