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.
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
--- /dev/null
+/********************* */
+/*! \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
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 );
}
}
-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;
<< 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);
#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"
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);
}
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) */
/** 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);
TheoryState d_state;
/** A (default) inference manager */
TheoryInferenceManager d_im;
+ /** The notify class */
+ NotifyClass d_notify;
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
projects / cvc5.git / commitdiff