diff options
| -rw-r--r-- | src/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/theory/shared_solver.cpp | 116 | ||||
| -rw-r--r-- | src/theory/shared_solver.h | 133 | ||||
| -rw-r--r-- | src/theory/shared_solver_distributed.cpp | 95 | ||||
| -rw-r--r-- | src/theory/shared_solver_distributed.h | 64 | ||||
| -rw-r--r-- | src/theory/shared_terms_database.cpp | 12 | ||||
| -rw-r--r-- | src/theory/shared_terms_database.h | 11 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 2 |
8 files changed, 437 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e6cb97894..5695e271e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -732,6 +732,10 @@ libcvc4_add_sources( theory/sets/theory_sets_type_enumerator.cpp theory/sets/theory_sets_type_enumerator.h theory/sets/theory_sets_type_rules.h + theory/shared_solver.cpp + theory/shared_solver.h + theory/shared_solver_distributed.cpp + theory/shared_solver_distributed.h theory/shared_terms_database.cpp theory/shared_terms_database.h theory/smt_engine_subsolver.cpp diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp new file mode 100644 index 000000000..794d3ca7c --- /dev/null +++ b/src/theory/shared_solver.cpp @@ -0,0 +1,116 @@ +/********************* */ +/*! \file shared_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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/theory_engine.h" + +namespace CVC4 { +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) + : d_te(te), + d_logicInfo(te.getLogicInfo()), + d_sharedTerms(&d_te, d_te.getSatContext()), + d_sharedTermsVisitor(d_sharedTerms) +{ +} + +bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi) +{ + return false; +} + +void SharedSolver::preRegisterShared(TNode t, bool multipleTheories) +{ + // register it with the equality engine manager if sharing is enabled + if (d_logicInfo.isSharingEnabled()) + { + preRegisterSharedInternal(t); + } + // if multiple theories are present in t + if (multipleTheories) + { + // Collect the shared terms if there are multiple theories + // This calls Theory::addSharedTerm, possibly multiple times + NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, t); + } +} + +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 CVC4 diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h new file mode 100644 index 000000000..d3604faca --- /dev/null +++ b/src/theory/shared_solver.h @@ -0,0 +1,133 @@ +/********************* */ +/*! \file shared_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Base class for shared solver + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__SHARED_SOLVER__H +#define CVC4__THEORY__SHARED_SOLVER__H + +#include "expr/node.h" +#include "theory/ee_setup_info.h" +#include "theory/logic_info.h" +#include "theory/shared_terms_database.h" +#include "theory/term_registration_visitor.h" +#include "theory/valuation.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace theory { + +/** + * A base class for shared solver. The shared solver is the component of theory + * engine that behaves like a theory solver, and whose purpose is to ensure the + * main theory combination method can be performed in CombinationEngine. + * Its role is to: + * (1) Notify the individual theories of shared terms via addSharedTerms, + * (2) Be the official interface for equality statuses, + * (3) Propagate equalities to TheoryEngine when necessary and explain them. + */ +class SharedSolver +{ + public: + SharedSolver(TheoryEngine& te); + virtual ~SharedSolver() {} + //------------------------------------- initialization + /** + * Returns true if we need an equality engine, this has the same contract + * as Theory::needsEqualityEngine. + */ + virtual bool needsEqualityEngine(theory::EeSetupInfo& esi); + /** + * Set the equality engine. This should be called by equality engine manager + * during EqEngineManager::initializeTheories. + */ + virtual void setEqualityEngine(eq::EqualityEngine* ee) = 0; + //------------------------------------- end initialization + /** + * Called when the given term t is pre-registered in TheoryEngine. + * + * This adds t as an equality to propagate in the shared terms database + * if it is an equality, or adds its shared terms if it involves multiple + * theories. + * + * @param t The term to preregister + * @param multipleTheories Whether multiple theories are present in t. + */ + void preRegisterShared(TNode t, bool multipleTheories); + /** + * Pre-notify assertion fact with the given atom. This is called when any + * fact is asserted in TheoryEngine, just before it is dispatched to the + * appropriate theory. + * + * This calls Theory::notifySharedTerm for the shared terms of the atom. + */ + void preNotifySharedFact(TNode atom); + /** + * Get the equality status of a and b. + * + * This method is used by theories via Valuation mostly for determining their + * care graph. + */ + virtual EqualityStatus getEqualityStatus(TNode a, TNode b); + /** + * Explain literal, which returns a conjunction of literals that entail + * the given one. + */ + virtual TrustNode explain(TNode literal, TheoryId id) = 0; + /** + * Assert equality to the shared terms database. + * + * This method is called by TheoryEngine when a fact has been marked to + * send to THEORY_BUILTIN, meaning that shared terms database should + * maintain this fact. This is the case when either an equality is + * asserted from the SAT solver or a theory propagates an equality between + * shared terms. + */ + virtual void assertSharedEquality(TNode equality, + bool polarity, + TNode reason) = 0; + /** Is term t a shared term? */ + virtual bool isShared(TNode t) const; + + /** + * Method called by equalityEngine when a becomes (dis-)equal to b and a and b + * are shared with the theory. Returns false if there is a direct conflict + * (via rewrite for example). + */ + bool propagateSharedEquality(theory::TheoryId theory, + TNode a, + TNode b, + bool value); + /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */ + void sendLemma(TrustNode trn, TheoryId atomsTo); + + protected: + /** Solver-specific pre-register shared */ + virtual void preRegisterSharedInternal(TNode t) = 0; + /** Reference to the theory engine */ + TheoryEngine& d_te; + /** Logic info of theory engine (cached) */ + const LogicInfo& d_logicInfo; + /** The database of shared terms.*/ + SharedTermsDatabase d_sharedTerms; + /** Visitor for collecting shared terms */ + SharedTermsVisitor d_sharedTermsVisitor; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__SHARED_SOLVER__H */ diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp new file mode 100644 index 000000000..873c81db1 --- /dev/null +++ b/src/theory/shared_solver_distributed.cpp @@ -0,0 +1,95 @@ +/********************* */ +/*! \file shared_solver_distributed.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Shared solver in the distributed architecture + **/ + +#include "theory/shared_solver_distributed.h" + +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace theory { + +SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te) + : SharedSolver(te) +{ +} + +bool SharedSolverDistributed::needsEqualityEngine(theory::EeSetupInfo& esi) +{ + return d_sharedTerms.needsEqualityEngine(esi); +} + +void SharedSolverDistributed::setEqualityEngine(eq::EqualityEngine* ee) +{ + d_sharedTerms.setEqualityEngine(ee); +} + +void SharedSolverDistributed::preRegisterSharedInternal(TNode t) +{ + if (t.getKind() == kind::EQUAL) + { + // When sharing is enabled, we propagate from the shared terms manager also + d_sharedTerms.addEqualityToPropagate(t); + } +} + +EqualityStatus SharedSolverDistributed::getEqualityStatus(TNode a, TNode b) +{ + // if we're using a shared terms database, ask its status if a and b are + // shared. + if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) + { + if (d_sharedTerms.areEqual(a, b)) + { + return EQUALITY_TRUE_AND_PROPAGATED; + } + else if (d_sharedTerms.areDisequal(a, b)) + { + return EQUALITY_FALSE_AND_PROPAGATED; + } + } + // otherwise, ask the theory + return d_te.theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); +} + +TrustNode SharedSolverDistributed::explain(TNode literal, TheoryId id) +{ + TrustNode texp; + if (id == THEORY_BUILTIN) + { + // explanation using the shared terms database + Node exp = d_sharedTerms.explain(literal); + texp = TrustNode::mkTrustPropExp(literal, exp, nullptr); + Trace("shared-solver") + << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " + << texp.getNode() << std::endl; + } + else + { + // By default, we ask the individual theory for the explanation. + texp = d_te.theoryOf(id)->explain(literal); + Trace("shared-solver") << "\tTerm was propagated by owner theory: " << id + << ". Explanation: " << texp.getNode() << std::endl; + } + return texp; +} + +void SharedSolverDistributed::assertSharedEquality(TNode equality, + bool polarity, + TNode reason) +{ + d_sharedTerms.assertEquality(equality, polarity, reason); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h new file mode 100644 index 000000000..45c7eafb3 --- /dev/null +++ b/src/theory/shared_solver_distributed.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file shared_solver_distributed.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Shared solver in the distributed architecture. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H +#define CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H + +#include "expr/node.h" +#include "theory/shared_solver.h" + +namespace CVC4 { +namespace theory { + +/** + * The shared solver in the distributed architecture. This class uses the + * SharedTermsDatabase for implementing the core methods of a shared solver. + */ +class SharedSolverDistributed : public SharedSolver +{ + public: + SharedSolverDistributed(TheoryEngine& te); + virtual ~SharedSolverDistributed() {} + //------------------------------------- initialization + /** + * Returns true if we need an equality engine, this has the same contract + * as Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(theory::EeSetupInfo& esi) override; + /** Set equality engine in the shared terms database */ + void setEqualityEngine(eq::EqualityEngine* ee) override; + //------------------------------------- end initialization + /** Assert equality to the shared terms database. */ + void assertSharedEquality(TNode equality, + bool polarity, + TNode reason) override; + /** + * Get equality status based on the equality engine of shared terms database + */ + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + /** Explain literal that was propagated by a theory or using shared terms + * database */ + TrustNode explain(TNode literal, TheoryId id) override; + + protected: + /** If t is an equality, add it as one that may be propagated */ + void preRegisterSharedInternal(TNode t) override; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__SHARED_SOLVER_DISTRIBUTED__H */ diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index b01cef377..034401b9a 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -44,6 +44,18 @@ SharedTermsDatabase::~SharedTermsDatabase() smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms); } +void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee) +{ + // TODO (project #39): dynamic allocation of equality engine here +} + +bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi) +{ + esi.d_notify = &d_EENotify; + esi.d_name = "SharedTermsDatabase"; + return true; +} + void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { d_registeredEqualities.insert(equality); d_equalityEngine.addTriggerPredicate(equality); diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index ca4f6c183..1a50224e1 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -21,6 +21,7 @@ #include "context/cdhashset.h" #include "expr/node.h" +#include "theory/ee_setup_info.h" #include "theory/theory_id.h" #include "theory/uf/equality_engine.h" #include "util/statistics_registry.h" @@ -158,6 +159,16 @@ public: SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context); ~SharedTermsDatabase(); + //-------------------------------------------- initialization + /** Called to set the equality engine. */ + void setEqualityEngine(theory::eq::EqualityEngine* ee); + /** + * Returns true if we need an equality engine, this has the same contract + * as Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(theory::EeSetupInfo& esi); + //-------------------------------------------- end initialization + /** * Asserts the equality to the shared terms database, */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a6258b7d6..fda32206b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -87,6 +87,7 @@ struct NodeTheoryPairHashFunction { namespace theory { class TheoryModel; class CombinationEngine; +class SharedSolver; class DecisionManager; class RelevanceManager; @@ -113,6 +114,7 @@ class TheoryEngine { friend class theory::CombinationEngine; friend class theory::EngineOutputChannel; friend class theory::CombinationEngine; + friend class theory::SharedSolver; /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; |