From 2acec47dc1bf0fcb2cd3b163993132bc5a630cd5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Feb 2022 13:45:10 -0600 Subject: [PATCH] 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. --- src/theory/sep/theory_sep.cpp | 8 +++++++- src/theory/sets/theory_sets.cpp | 3 +++ 2 files changed, 10 insertions(+), 1 deletion(-) 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); } -- 2.30.2