From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 17 Feb 2022 19:45:10 +0000 (-0600)
Subject: Remove some irrelevant node kinds from the model (#8110)
X-Git-Tag: cvc5-1.0.0~419
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2acec47dc1bf0fcb2cd3b163993132bc5a630cd5;p=cvc5.git

Remove some irrelevant node kinds from the model (#8110)

There are several kinds of nodes that are currently sent to the model that don't need to be. Furthermore, we require not sending some of these due to the new invariants in #8095.
---

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 3ee4fa012..7c1c58e5d 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -104,8 +104,14 @@ void TheorySep::finishInit()
 {
   Assert(d_equalityEngine != nullptr);
   // The kinds we are treating as function application in congruence
-  d_equalityEngine->addFunctionKind(kind::SEP_PTO);
+  d_equalityEngine->addFunctionKind(SEP_PTO);
   // we could but don't do congruence on SEP_STAR here.
+
+  // separation logic predicates are not relevant for model building
+  d_valuation.setIrrelevantKind(SEP_STAR);
+  d_valuation.setIrrelevantKind(SEP_WAND);
+  d_valuation.setIrrelevantKind(SEP_LABEL);
+  d_valuation.setIrrelevantKind(SEP_PTO);
 }
 
 void TheorySep::preRegisterTerm(TNode n)
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index c3d0b9bbe..dbc52f387 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -93,6 +93,9 @@ void TheorySets::finishInit()
 
   // finish initialization internally
   d_internal->finishInit();
+
+  // memberships are not relevant for model building
+  d_valuation.setIrrelevantKind(SET_MEMBER);
 }
 
 void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }