summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/theory_eq_notify.h82
-rw-r--r--src/theory/uf/theory_uf.cpp33
-rw-r--r--src/theory/uf/theory_uf.h60
3 files changed, 98 insertions, 77 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback