Standardize equality engine notifications in sets (#5098)

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 66f35f24fcabcd1bd0677c41602484c7144857d5..971a12dc235fedfffe7a5d6bc5207c30bf8e5e05 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -38,7 +38,7 @@ TheorySets::TheorySets(context::Context* c,
       d_state(c, u, valuation, d_skCache),
       d_im(*this, d_state, pnm),
       d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)),
-      d_notify(*d_internal.get())
+      d_notify(*d_internal.get(), d_im)
 {
   // use the official theory state and inference manager objects
   d_theoryState = &d_state;
@@ -201,37 +201,6 @@ bool TheorySets::isEntailed( Node n, bool pol ) {
 
 /**************************** eq::NotifyClass *****************************/
 
-bool TheorySets::NotifyClass::eqNotifyTriggerPredicate(TNode predicate,
-                                                       bool value)
-{
-  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = "
-                   << predicate << " value = " << value << std::endl;
-  if (value)
-  {
-    return d_theory.propagate(predicate);
-  }
-  return d_theory.propagate(predicate.notNode());
-}
-
-bool TheorySets::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag,
-                                                          TNode t1,
-                                                          TNode t2,
-                                                          bool value)
-{
-  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
-                   << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value
-                   << std::endl;
-  d_theory.propagate(value ? t1.eqNode(t2) : t1.eqNode(t2).negate());
-  return true;
-}
-
-void TheorySets::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
-{
-  Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge "
-                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
-  d_theory.conflict(t1, t2);
-}
-
 void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
 {
   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:"

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index fce57ca6c224c5f19b22f2149354f5a9255e5ec2..4d0c74516acfeaa716f65dfb57b74d9ab5ae2a9e 100644 (file)
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -25,6 +25,7 @@
 #include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"
 #include "theory/theory.h"
+#include "theory/theory_eq_notify.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -82,16 +83,13 @@ class TheorySets : public Theory
 
  private:
   /** Functions to handle callbacks from equality engine */
-  class NotifyClass : public eq::EqualityEngineNotify
+  class NotifyClass : public TheoryEqNotifyClass
   {
    public:
-    NotifyClass(TheorySetsPrivate& theory) : d_theory(theory) {}
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
-    bool eqNotifyTriggerTermEquality(TheoryId tag,
-                                     TNode t1,
-                                     TNode t2,
-                                     bool value) override;
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    NotifyClass(TheorySetsPrivate& theory, TheoryInferenceManager& im)
+        : TheoryEqNotifyClass(im), d_theory(theory)
+    {
+    }
     void eqNotifyNewClass(TNode t) override;
     void eqNotifyMerge(TNode t1, TNode t2) override;
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index c928718982763f819d3e14be69732eaa84a5ca1c..8779ac48931f74e24697918f42852542658b0933 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -111,7 +111,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
             // singleton equal to emptyset, conflict
             Trace("sets-prop")
                 << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
-            conflict(s1, s2);
+            d_im.conflictEqConstantMerge(s1, s2);
             return;
           }
         }
@@ -829,7 +829,7 @@ void TheorySetsPrivate::postCheck(Theory::Effort level)
         if (!d_state.isInConflict() && !d_im.hasSentLemma()
             && d_full_check_incomplete)
         {
-          d_external.d_out->setIncomplete();
+          d_im.setIncomplete();
         }
       }
     }
@@ -1234,44 +1234,8 @@ Node mkAnd(const std::vector<TNode>& conjunctions)
   return conjunction;
 } /* mkAnd() */
 
-bool TheorySetsPrivate::propagate(TNode literal)
-{
-  Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
-
-  // If already in conflict, no more propagation
-  if (d_state.isInConflict())
-  {
-    Debug("sets-prop") << "TheoryUF::propagate(" << literal
-                       << "): already in conflict" << std::endl;
-    return false;
-  }
-
-  // Propagate out
-  bool ok = d_external.d_out->propagate(literal);
-  if (!ok)
-  {
-    d_state.notifyInConflict();
-  }
-
-  return ok;
-} /* TheorySetsPrivate::propagate(TNode) */
-
-OutputChannel* TheorySetsPrivate::getOutputChannel()
-{
-  return d_external.d_out;
-}
-
 Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
 
-void TheorySetsPrivate::conflict(TNode a, TNode b)
-{
-  Node conf = explain(a.eqNode(b));
-  d_im.conflict(conf);
-  Debug("sets") << "[sets] conflict: " << a << " iff " << b << ", explanation "
-                << conf << std::endl;
-  Trace("sets-lemma") << "Equality Conflict : " << conf << std::endl;
-}
-
 Node TheorySetsPrivate::explain(TNode literal)
 {
   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl;

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index d58967c5f78e4643b65ad731a69fd983044aa724..b2d3723cd3c97bf8103b0d74b7b15f10a0e57968 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -213,17 +213,8 @@ class TheorySetsPrivate {
 
   void presolve();
 
-  /** get default output channel */
-  OutputChannel* getOutputChannel();
   /** get the valuation */
   Valuation& getValuation();
-
-  /** Proagate out to output channel */
-  bool propagate(TNode);
-
-  /** generate and send out conflict node */
-  void conflict(TNode, TNode);
-
  private:
   TheorySets& d_external;
   /** The state of the sets solver at full effort */