From 906aa7a59ffde0db0b7a3d81c37ea472eedb691e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Jun 2022 13:29:52 -0500 Subject: [PATCH] Remove spurious pto singleton inference (#8925) This removes a spurious lemma schema that is already covered by SEP_POS_REDUCTION. --- src/theory/inference_id.cpp | 1 - src/theory/inference_id.h | 2 -- src/theory/sep/theory_sep.cpp | 13 ------------- 3 files changed, 16 deletions(-) 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 -- 2.30.2