1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Shared solver in the distributed architecture.
16 #include "theory/shared_solver_distributed.h"
18 #include "theory/theory_engine.h"
23 SharedSolverDistributed::SharedSolverDistributed(Env
& env
, TheoryEngine
& te
)
24 : SharedSolver(env
, te
)
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::assertShared(TNode n
, bool polarity
, TNode reason
)
90 d_sharedTerms
.assertShared(n
, polarity
, reason
);