(new theory) Update TheorySets to the new interface (#4951)

This updates the theory of sets to the new interface (see #4929).

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 0bf2ed2ea6202b5cf19c4d546287a825552b9e5a..cb42f09d51dbcac759413b04e26ae81f02c06d78 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -67,12 +67,12 @@ void TheorySets::finishInit()
   d_valuation.setUnevaluatedKind(WITNESS);
 
   // functions we are doing congruence over
-  d_equalityEngine->addFunctionKind(kind::SINGLETON);
-  d_equalityEngine->addFunctionKind(kind::UNION);
-  d_equalityEngine->addFunctionKind(kind::INTERSECTION);
-  d_equalityEngine->addFunctionKind(kind::SETMINUS);
-  d_equalityEngine->addFunctionKind(kind::MEMBER);
-  d_equalityEngine->addFunctionKind(kind::SUBSET);
+  d_equalityEngine->addFunctionKind(SINGLETON);
+  d_equalityEngine->addFunctionKind(UNION);
+  d_equalityEngine->addFunctionKind(INTERSECTION);
+  d_equalityEngine->addFunctionKind(SETMINUS);
+  d_equalityEngine->addFunctionKind(MEMBER);
+  d_equalityEngine->addFunctionKind(SUBSET);
   // relation operators
   d_equalityEngine->addFunctionKind(PRODUCT);
   d_equalityEngine->addFunctionKind(JOIN);
@@ -88,14 +88,20 @@ void TheorySets::finishInit()
   d_internal->finishInit();
 }
 
-void TheorySets::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); }
+void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
 
-void TheorySets::check(Effort e) {
-  if (done() && e < Theory::EFFORT_FULL) {
-    return;
-  }
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-  d_internal->check(e);
+bool TheorySets::preNotifyFact(
+    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
+{
+  return d_internal->preNotifyFact(atom, polarity, fact);
+}
+
+void TheorySets::notifyFact(TNode atom,
+                            bool polarity,
+                            TNode fact,
+                            bool isInternal)
+{
+  d_internal->notifyFact(atom, polarity, fact);
 }
 
 bool TheorySets::collectModelValues(TheoryModel* m,
@@ -114,15 +120,12 @@ TrustNode TheorySets::explain(TNode node)
   return TrustNode::mkTrustPropExp(node, exp, nullptr);
 }
 
-EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
-  return d_internal->getEqualityStatus(a, b);
-}
-
 Node TheorySets::getModelValue(TNode node) {
   return Node::null();
 }
 
-void TheorySets::preRegisterTerm(TNode node) {
+void TheorySets::preRegisterTerm(TNode node)
+{
   d_internal->preRegisterTerm(node);
 }
 
@@ -158,7 +161,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubsti
   Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
 
   // this is based off of Theory::ppAssert
-  if (in.getKind() == kind::EQUAL)
+  if (in.getKind() == EQUAL)
   {
     if (in[0].isVar() && isLegalElimination(in[0], in[1]))
     {

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index a826a43afe33e98bc612da8cff06c865e8e3106b..7787c0f9b793d0e62eded02a681409c039a3a035 100644 (file)
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -58,13 +58,23 @@ class TheorySets : public Theory
   void finishInit() override;
   //--------------------------------- end initialization
 
-  void notifySharedTerm(TNode) override;
-  void check(Effort) override;
+  //--------------------------------- standard check
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Effort level) override;
+  /** Pre-notify fact, return true if processed. */
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+  /** Notify fact */
+  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+  //--------------------------------- end standard check
+  /** Collect model values in m based on the relevant terms given by termSet */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
   void computeCareGraph() override;
   TrustNode explain(TNode) override;
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   Node getModelValue(TNode) override;
   std::string identify() const override { return "THEORY_SETS"; }
   void preRegisterTerm(TNode node) override;
@@ -72,6 +82,7 @@ class TheorySets : public Theory
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
   void presolve() override;
   bool isEntailed(Node n, bool pol);
+
  private:
   /** Functions to handle callbacks from equality engine */
   class NotifyClass : public eq::EqualityEngineNotify

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 78824636ad780c1eecd2ac11cf131e363f05673e..c432c8039e2f2d80bc3d8bdf028bebd24c5bc08a 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -276,74 +276,21 @@ bool TheorySetsPrivate::assertFact(Node fact, Node exp)
                        << ", exp = " << exp << std::endl;
   bool polarity = fact.getKind() != kind::NOT;
   TNode atom = polarity ? fact : fact[0];
-  if (!d_state.isEntailed(atom, polarity))
+  if (d_state.isEntailed(atom, polarity))
   {
-    if (atom.getKind() == kind::EQUAL)
-    {
-      d_equalityEngine->assertEquality(atom, polarity, exp);
-    }
-    else
-    {
-      d_equalityEngine->assertPredicate(atom, polarity, exp);
-    }
-    if (!d_state.isInConflict())
-    {
-      if (atom.getKind() == kind::MEMBER && polarity)
-      {
-        // check if set has a value, if so, we can propagate
-        Node r = d_equalityEngine->getRepresentative(atom[1]);
-        EqcInfo* e = getOrMakeEqcInfo(r, true);
-        if (e)
-        {
-          Node s = e->d_singleton;
-          if (!s.isNull())
-          {
-            Node pexp = NodeManager::currentNM()->mkNode(
-                kind::AND, atom, atom[1].eqNode(s));
-            d_keep.insert(pexp);
-            if (s.getKind() == kind::SINGLETON)
-            {
-              if (s[0] != atom[0])
-              {
-                Trace("sets-prop")
-                    << "Propagate mem-eq : " << pexp << std::endl;
-                Node eq = s[0].eqNode(atom[0]);
-                d_keep.insert(eq);
-                assertFact(eq, pexp);
-              }
-            }
-            else
-            {
-              Trace("sets-prop")
-                  << "Propagate mem-eq conflict : " << pexp << std::endl;
-              d_im.conflict(pexp);
-            }
-          }
-        }
-        // add to membership list
-        NodeIntMap::iterator mem_i = d_members.find(r);
-        int n_members = 0;
-        if (mem_i != d_members.end())
-        {
-          n_members = (*mem_i).second;
-        }
-        d_members[r] = n_members + 1;
-        if (n_members < (int)d_members_data[r].size())
-        {
-          d_members_data[r][n_members] = atom;
-        }
-        else
-        {
-          d_members_data[r].push_back(atom);
-        }
-      }
-    }
-    return true;
+    return false;
+  }
+  if (atom.getKind() == kind::EQUAL)
+  {
+    d_equalityEngine->assertEquality(atom, polarity, exp);
   }
   else
   {
-    return false;
+    d_equalityEngine->assertPredicate(atom, polarity, exp);
   }
+  // call the notify new fact method
+  notifyFact(atom, polarity, exp);
+  return true;
 }
 
 void TheorySetsPrivate::fullEffortReset()
@@ -950,26 +897,10 @@ void TheorySetsPrivate::checkReduceComprehensions()
   }
 }
 
-/**************************** TheorySetsPrivate *****************************/
-/**************************** TheorySetsPrivate *****************************/
-/**************************** TheorySetsPrivate *****************************/
+//--------------------------------- standard check
 
-void TheorySetsPrivate::check(Theory::Effort level)
+void TheorySetsPrivate::postCheck(Theory::Effort level)
 {
-  Trace("sets-check") << "Sets check effort " << level << std::endl;
-  if (level == Theory::EFFORT_LAST_CALL)
-  {
-    return;
-  }
-  while (!d_external.done() && !d_state.isInConflict())
-  {
-    // Get all the assertions
-    Assertion assertion = d_external.get();
-    TNode fact = assertion.d_assertion;
-    Trace("sets-assert") << "Assert from input " << fact << std::endl;
-    // assert the fact
-    assertFact(fact, fact);
-  }
   Trace("sets-check") << "Sets finished assertions effort " << level
                       << std::endl;
   // invoke full effort check, relations check
@@ -989,18 +920,75 @@ void TheorySetsPrivate::check(Theory::Effort level)
     }
   }
   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
-} /* TheorySetsPrivate::check() */
+}
 
-/************************ Sharing ************************/
-/************************ Sharing ************************/
-/************************ Sharing ************************/
+bool TheorySetsPrivate::preNotifyFact(TNode atom, bool polarity, TNode fact)
+{
+  // use entailment check (is this necessary?)
+  return d_state.isEntailed(atom, polarity);
+}
 
-void TheorySetsPrivate::addSharedTerm(TNode n)
+void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
 {
-  Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")"
-                << std::endl;
-  d_equalityEngine->addTriggerTerm(n, THEORY_SETS);
+  if (d_state.isInConflict())
+  {
+    return;
+  }
+  if (atom.getKind() == kind::MEMBER && polarity)
+  {
+    // check if set has a value, if so, we can propagate
+    Node r = d_equalityEngine->getRepresentative(atom[1]);
+    EqcInfo* e = getOrMakeEqcInfo(r, true);
+    if (e)
+    {
+      Node s = e->d_singleton;
+      if (!s.isNull())
+      {
+        Node pexp = NodeManager::currentNM()->mkNode(
+            kind::AND, atom, atom[1].eqNode(s));
+        d_keep.insert(pexp);
+        if (s.getKind() == kind::SINGLETON)
+        {
+          if (s[0] != atom[0])
+          {
+            Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
+            Node eq = s[0].eqNode(atom[0]);
+            d_keep.insert(eq);
+            // triggers an internal inference
+            assertFact(eq, pexp);
+          }
+        }
+        else
+        {
+          Trace("sets-prop")
+              << "Propagate mem-eq conflict : " << pexp << std::endl;
+          d_im.conflict(pexp);
+        }
+      }
+    }
+    // add to membership list
+    NodeIntMap::iterator mem_i = d_members.find(r);
+    int n_members = 0;
+    if (mem_i != d_members.end())
+    {
+      n_members = (*mem_i).second;
+    }
+    d_members[r] = n_members + 1;
+    if (n_members < (int)d_members_data[r].size())
+    {
+      d_members_data[r][n_members] = atom;
+    }
+    else
+    {
+      d_members_data[r].push_back(atom);
+    }
+  }
 }
+//--------------------------------- end standard check
+
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
 
 void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
                                      TNodeTrie* t2,
@@ -1193,37 +1181,6 @@ bool TheorySetsPrivate::isCareArg(Node n, unsigned a)
   }
 }
 
-EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b)
-{
-  Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
-  if (d_equalityEngine->areEqual(a, b))
-  {
-    // The terms are implied to be equal
-    return EQUALITY_TRUE;
-  }
-  if (d_equalityEngine->areDisequal(a, b, false))
-  {
-    // The terms are implied to be dis-equal
-    return EQUALITY_FALSE;
-  }
-  return EQUALITY_UNKNOWN;
-  /*
-  Node aModelValue = d_external.d_valuation.getModelValue(a);
-  if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
-  Node bModelValue = d_external.d_valuation.getModelValue(b);
-  if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
-  if( aModelValue == bModelValue ) {
-    // The term are true in current model
-    return EQUALITY_TRUE_IN_MODEL;
-  } else {
-    return EQUALITY_FALSE_IN_MODEL;
-  }
-  */
-  // }
-  // //TODO: can we be more precise sometimes?
-  // return EQUALITY_UNKNOWN;
-}
-
 /******************** Model generation ********************/
 /******************** Model generation ********************/
 /******************** Model generation ********************/
@@ -1261,7 +1218,7 @@ std::string traceElements(const Node& set)
 bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
                                            const std::set<Node>& termSet)
 {
-  Trace("sets-model") << "Set collect model info" << std::endl;
+  Trace("sets-model") << "Set collect model values" << std::endl;
 
   NodeManager* nm = NodeManager::currentNM();
   std::map<Node, Node> mvals;

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 387d56de975e35399324bcee419c3a5a2b865045..0df1eabc5003e078cb99bec68e3dccb84cf800f0 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -172,18 +172,23 @@ class TheorySetsPrivate {
    */
   void finishInit();
 
+  //--------------------------------- standard check
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Theory::Effort level);
+  /** Preprocess fact, return true if processed. */
+  bool preNotifyFact(TNode atom, bool polarity, TNode fact);
+  /** Notify new fact */
+  void notifyFact(TNode atom, bool polarity, TNode fact);
+  //--------------------------------- end standard check
+
+  /** Collect model values in m based on the relevant terms given by termSet */
   void addSharedTerm(TNode);
-
-  void check(Theory::Effort);
-
   bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet);
 
   void computeCareGraph();
 
   Node explain(TNode);
 
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-
   void preRegisterTerm(TNode node);
 
   /** expandDefinition