1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
/********************* */
/*! \file shared_solver.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The shared solver base class
**/
#include "theory/shared_solver.h"
#include "expr/node_visitor.h"
#include "theory/ee_setup_info.h"
#include "theory/logic_info.h"
#include "theory/theory_engine.h"
namespace cvc5 {
namespace theory {
// Always creates shared terms database. In all cases, shared terms
// database is used as a way of tracking which calls to Theory::addSharedTerm
// we need to make in preNotifySharedFact.
// In distributed equality engine management, shared terms database also
// maintains an equality engine. In central equality engine management,
// it does not.
SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm)
: d_te(te),
d_logicInfo(te.getLogicInfo()),
d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm),
d_preRegistrationVisitor(&te, d_te.getSatContext()),
d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext())
{
}
bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi)
{
return false;
}
void SharedSolver::preRegister(TNode atom)
{
Trace("theory") << "SharedSolver::preRegister atom " << atom << std::endl;
// This method uses two different implementations for preregistering terms,
// which depends on whether sharing is enabled.
// If sharing is disabled, we use PreRegisterVisitor, which keeps a global
// SAT-context dependent cache of terms visited.
// If sharing is disabled, we use SharedTermsVisitor which does *not* keep a
// global cache. This is because shared terms must be associated with the
// given atom, and thus it must traverse the set of subterms in each atom.
// See term_registration_visitor.h for more details.
if (d_logicInfo.isSharingEnabled())
{
// register it with the shared terms database if sharing is enabled
preRegisterSharedInternal(atom);
// Collect the shared terms in atom, as well as calling preregister on the
// appropriate theories in atom.
// This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly
// multiple times.
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom);
}
else
{
// just use the normal preregister visitor, which calls
// Theory::preRegisterTerm possibly multiple times.
NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, atom);
}
Trace("theory") << "SharedSolver::preRegister atom finished" << std::endl;
}
void SharedSolver::preNotifySharedFact(TNode atom)
{
if (d_sharedTerms.hasSharedTerms(atom))
{
// Always notify the theories of the shared terms, which is independent of
// the architecture currently.
SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
for (; it != it_end; ++it)
{
TNode term = *it;
TheoryIdSet theories = d_sharedTerms.getTheoriesToNotify(atom, term);
for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id)
{
if (TheoryIdSetUtil::setContains(id, theories))
{
Theory* t = d_te.theoryOf(id);
// call the add shared term method
t->addSharedTerm(term);
}
}
d_sharedTerms.markNotified(term, theories);
}
}
}
EqualityStatus SharedSolver::getEqualityStatus(TNode a, TNode b)
{
return EQUALITY_UNKNOWN;
}
void SharedSolver::sendLemma(TrustNode trn, TheoryId atomsTo)
{
d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
}
bool SharedSolver::propagateSharedEquality(theory::TheoryId theory,
TNode a,
TNode b,
bool value)
{
// Propagate equality between shared terms to the one who asked for it
Node equality = a.eqNode(b);
if (value)
{
d_te.assertToTheory(equality, equality, theory, THEORY_BUILTIN);
}
else
{
d_te.assertToTheory(
equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN);
}
return true;
}
bool SharedSolver::isShared(TNode t) const { return d_sharedTerms.isShared(t); }
} // namespace theory
} // namespace cvc5
|
