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 3ee4fa0120c313edc2374c85142ef124dc018434..7c1c58e5d5fcaa71a97d60f8e90de31e6dbf094f 100644 (file)
--- 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 c3d0b9bbe6540204214705188203143d2e3fccec..dbc52f3870da5bfeb273b7af8f4dac9fc6153fb0 100644 (file)
--- 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); }