diff options
-rw-r--r-- | src/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/theory/theory_eq_notify.h | 82 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 33 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 60 |
4 files changed, 99 insertions, 77 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9753f86a7..1e00de104 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -805,6 +805,7 @@ libcvc4_add_sources( theory/theory_engine_proof_generator.h theory/theory_id.cpp theory/theory_id.h + theory/theory_eq_notify.h theory/theory_inference.cpp theory/theory_inference.h theory/theory_inference_manager.cpp diff --git a/src/theory/theory_eq_notify.h b/src/theory/theory_eq_notify.h new file mode 100644 index 000000000..3df5d32cb --- /dev/null +++ b/src/theory/theory_eq_notify.h @@ -0,0 +1,82 @@ +/********************* */ +/*! \file theory_eq_notify.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 The theory equality notify utility. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__THEORY_EQ_NOTIFY_H +#define CVC4__THEORY__THEORY_EQ_NOTIFY_H + +#include "expr/node.h" +#include "theory/theory_inference_manager.h" +#include "theory/uf/equality_engine_notify.h" + +namespace CVC4 { +namespace theory { + +/** + * The default class for equality engine callbacks for a theory. This forwards + * calls for trigger predicates, trigger term equalities and conflicts due to + * constant merges to the provided theory inference manager. + */ +class TheoryEqNotifyClass : public eq::EqualityEngineNotify +{ + public: + TheoryEqNotifyClass(TheoryInferenceManager& im) : d_im(im) {} + ~TheoryEqNotifyClass() {} + + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { + if (value) + { + return d_im.propagateLit(predicate); + } + return d_im.propagateLit(predicate.notNode()); + } + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { + if (value) + { + return d_im.propagateLit(t1.eqNode(t2)); + } + return d_im.propagateLit(t1.eqNode(t2).notNode()); + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { + d_im.conflictEqConstantMerge(t1, t2); + } + void eqNotifyNewClass(TNode t) override + { + // do nothing + } + void eqNotifyMerge(TNode t1, TNode t2) override + { + // do nothing + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override + { + // do nothing + } + + protected: + /** Reference to the theory inference manager */ + TheoryInferenceManager& d_im; +}; + +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 18ab70d46..4a9f52918 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -46,15 +46,13 @@ TheoryUF::TheoryUF(context::Context* c, ProofNodeManager* pnm, std::string instanceName) : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName), - d_notify(*this), - /* The strong theory solver can be notified by EqualityEngine::init(), - * so make sure it's initialized first. */ d_thss(nullptr), d_ho(nullptr), d_functionsTerms(c), d_symb(u, instanceName), d_state(c, u, valuation), - d_im(*this, d_state, pnm) + d_im(*this, d_state, pnm), + d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -268,25 +266,6 @@ void TheoryUF::preRegisterTerm(TNode node) } } -bool TheoryUF::propagateLit(TNode literal) -{ - Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal << ")" - << std::endl; - // If already in conflict, no more propagation - if (d_state.isInConflict()) - { - Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal - << "): already in conflict" << std::endl; - return false; - } - // Propagate out - bool ok = d_out->propagate(literal); - if (!ok) { - d_state.notifyInConflict(); - } - return ok; -}/* TheoryUF::propagate(TNode) */ - void TheoryUF::explain(TNode literal, Node& exp) { Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl; @@ -648,14 +627,6 @@ void TheoryUF::computeCareGraph() { << std::endl; }/* TheoryUF::computeCareGraph() */ -void TheoryUF::conflict(TNode a, TNode b) -{ - // call the inference manager, which will construct the conflict (possibly - // with proofs from the underlying proof equality engine), and notify the - // state object. - d_im.conflictEqConstantMerge(a, b); -} - void TheoryUF::eqNotifyNewClass(TNode t) { if (d_thss != NULL) { d_thss->newEqClass(t); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 86c1b62c8..25825e17d 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/node_trie.h" #include "theory/theory.h" +#include "theory/theory_eq_notify.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_checker.h" #include "theory/uf/proof_equality_engine.h" @@ -38,44 +39,19 @@ class CardinalityExtension; class HoExtension; class TheoryUF : public Theory { - -public: - - class NotifyClass : public eq::EqualityEngineNotify { - TheoryUF& d_uf; - public: - NotifyClass(TheoryUF& uf): d_uf(uf) {} - - bool eqNotifyTriggerPredicate(TNode predicate, bool value) override - { - Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; - if (value) { - return d_uf.propagateLit(predicate); - } - return d_uf.propagateLit(predicate.notNode()); - } - - bool eqNotifyTriggerTermEquality(TheoryId tag, - TNode t1, - TNode t2, - bool value) override - { - Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; - if (value) { - return d_uf.propagateLit(t1.eqNode(t2)); - } - return d_uf.propagateLit(t1.eqNode(t2).notNode()); - } - - void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + public: + class NotifyClass : public TheoryEqNotifyClass + { + public: + NotifyClass(TheoryInferenceManager& im, TheoryUF& uf) + : TheoryEqNotifyClass(im), d_uf(uf) { - Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; - d_uf.conflict(t1, t2); } void eqNotifyNewClass(TNode t) override { - Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" + << std::endl; d_uf.eqNotifyNewClass(t); } @@ -92,13 +68,12 @@ public: d_uf.eqNotifyDisequal(t1, t2, reason); } + private: + /** Reference to the parent theory */ + TheoryUF& d_uf; };/* class TheoryUF::NotifyClass */ private: - - /** The notify class */ - NotifyClass d_notify; - /** The associated cardinality extension (or nullptr if it does not exist) */ std::unique_ptr<CardinalityExtension> d_thss; /** the higher-order solver extension (or nullptr if it does not exist) */ @@ -107,21 +82,12 @@ private: /** node for true */ Node d_true; - /** - * Should be called to propagate the literal. We use a node here - * since some of the propagated literals are not kept anywhere. - */ - bool propagateLit(TNode literal); - /** All the function terms that the theory has seen */ context::CDList<TNode> d_functionsTerms; /** Symmetry analyzer */ SymmetryBreaker d_symb; - /** Conflict when merging two constants */ - void conflict(TNode a, TNode b); - /** called when a new equivalance class is created */ void eqNotifyNewClass(TNode t); @@ -206,6 +172,8 @@ private: TheoryState d_state; /** A (default) inference manager */ TheoryInferenceManager d_im; + /** The notify class */ + NotifyClass d_notify; };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |