1 /********************* */
2 /*! \file shared_solver_distributed.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Shared solver in the distributed architecture
15 #include "theory/shared_solver_distributed.h"
17 #include "theory/theory_engine.h"
22 SharedSolverDistributed::SharedSolverDistributed(TheoryEngine
& te
,
23 ProofNodeManager
* pnm
)
24 : SharedSolver(te
, pnm
)
28 bool SharedSolverDistributed::needsEqualityEngine(theory::EeSetupInfo
& esi
)
30 return d_sharedTerms
.needsEqualityEngine(esi
);
33 void SharedSolverDistributed::setEqualityEngine(eq::EqualityEngine
* ee
)
35 d_sharedTerms
.setEqualityEngine(ee
);
38 void SharedSolverDistributed::preRegisterSharedInternal(TNode t
)
40 if (t
.getKind() == kind::EQUAL
)
42 // When sharing is enabled, we propagate from the shared terms manager also
43 d_sharedTerms
.addEqualityToPropagate(t
);
47 EqualityStatus
SharedSolverDistributed::getEqualityStatus(TNode a
, TNode b
)
49 // if we're using a shared terms database, ask its status if a and b are
51 if (d_sharedTerms
.isShared(a
) && d_sharedTerms
.isShared(b
))
53 if (d_sharedTerms
.areEqual(a
, b
))
55 return EQUALITY_TRUE_AND_PROPAGATED
;
57 else if (d_sharedTerms
.areDisequal(a
, b
))
59 return EQUALITY_FALSE_AND_PROPAGATED
;
62 // otherwise, ask the theory
63 return d_te
.theoryOf(Theory::theoryOf(a
.getType()))->getEqualityStatus(a
, b
);
66 TrustNode
SharedSolverDistributed::explain(TNode literal
, TheoryId id
)
69 if (id
== THEORY_BUILTIN
)
71 // explanation using the shared terms database
72 texp
= d_sharedTerms
.explain(literal
);
73 Trace("shared-solver")
74 << "\tTerm was propagated by THEORY_BUILTIN. Explanation: "
75 << texp
.getNode() << std::endl
;
79 // By default, we ask the individual theory for the explanation.
80 // It is possible that a centralized approach could preempt this.
81 texp
= d_te
.theoryOf(id
)->explain(literal
);
82 Trace("shared-solver") << "\tTerm was propagated by owner theory: " << id
83 << ". Explanation: " << texp
.getNode() << std::endl
;
88 void SharedSolverDistributed::assertSharedEquality(TNode equality
,
92 d_sharedTerms
.assertEquality(equality
, polarity
, reason
);