From 996f6f9e2ecf76e39c236f9c410c109807c7073d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Sep 2020 21:19:15 -0500 Subject: [PATCH] Standard equality engine notify class for Theory (#5042) This makes a standard equality engine notify class that forwards the 3 mandatory callbacks to the provided inference manager (the other 3 callbacks may be specific to the theory). It updates TheoryUF to use this class, other theories will be updated to this style as more inference manager are added. Notice that we could also forward the other 3 callbacks in this class to Theory, making eqNotifyNewClass, eqNotifyMerge, and eqNotifyDisequal virtual methods in Theory, which can be done on a future PR if needed. --- src/CMakeLists.txt | 1 + src/theory/theory_eq_notify.h | 82 +++++++++++++++++++++++++++++++++++ src/theory/uf/theory_uf.cpp | 33 +------------- src/theory/uf/theory_uf.h | 60 ++++++------------------- 4 files changed, 99 insertions(+), 77 deletions(-) create mode 100644 src/theory/theory_eq_notify.h 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 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 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 */ -- 2.30.2