Remove spurious pto singleton inference (#8925)

This removes a spurious lemma schema that is already covered by SEP_POS_REDUCTION.

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index d828d6e5ddf3fb73d0387097caef309c47627136..dbc013cb772598c369ba07d0d99611f895d65189 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -324,7 +324,6 @@ const char* toString(InferenceId i)
     case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO";
     case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF";
     case InferenceId::SEP_EMP: return "SEP_EMP";
-    case InferenceId::SEP_POS_PTO_SINGLETON: return "SEP_POS_PTO_SINGLETON";
     case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION";
     case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION";
     case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index ee3cb6004e37f88f7973ca990de011834df1e5c6..eb5867fa1ba2baef2011632930f8c2f05c0c4806 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -462,8 +462,6 @@ enum class InferenceId
   SEP_LABEL_DEF,
   // lemma for sep.emp
   SEP_EMP,
-  // lemma for positive labelled PTO
-  SEP_POS_PTO_SINGLETON,
   // positive reduction for sep constraint
   SEP_POS_REDUCTION,
   // negative reduction for sep constraint

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 75484ceb020488c4b4cb9d497e741670299c8124..d86bea6b46400137712649b49271054eaf595969 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -293,19 +293,6 @@ bool TheorySep::preNotifyFact(
   }
   if (!slbl.isNull() && satom.getKind() == SEP_PTO)
   {
-    if (polarity)
-    {
-      NodeManager* nm = NodeManager::currentNM();
-      // (SEP_LABEL (sep.pto x y) L) => L = (set.singleton x)
-      Node s = nm->mkNode(SET_SINGLETON, satom[0]);
-      Node eq = slbl.eqNode(s);
-      TrustNode trn =
-          d_im.mkLemmaExp(eq, PfRule::THEORY_INFERENCE, {fact}, {fact}, {eq});
-      d_im.addPendingLemma(trn.getNode(),
-                           InferenceId::SEP_POS_PTO_SINGLETON,
-                           LemmaProperty::NONE,
-                           trn.getGenerator());
-    }
     return false;
   }
   // assert to equality if non-spatial or a labelled pto