From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jun 2022 18:29:52 +0000 (-0500)
Subject: Remove spurious pto singleton inference (#8925)
X-Git-Tag: cvc5-1.0.1~22
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=906aa7a59ffde0db0b7a3d81c37ea472eedb691e;p=cvc5.git

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 d828d6e5d..dbc013cb7 100644
--- 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 ee3cb6004..eb5867fa1 100644
--- 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 75484ceb0..d86bea6b4 100644
--- 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