diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-10 10:06:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-10 16:06:27 +0000 |
commit | cdcdd49a79ba03966cbb29c4f380f426c95a7d3a (patch) | |
tree | de8cf667daead76fa107e8513c2a7915435d2473 /src/theory/term_registration_visitor.cpp | |
parent | 2ff196ccba2ce611fe7320ef775955c291d34dab (diff) |
Fix term registration and non-theory-preprocessed terms in substitutions (#6080)
This fixes two issues for preprocessing:
(1) The term preregistration visitor was calling preRegister on terms multiple times in a SAT context, which the linear arithmetic solver is sensitive to.
(2) It was possible for non-preprocessed terms to appear in assertions if they were on the RHS of substitutions learned by non-clausal simplification, and substituted into assertions post-theory-preprocessing.
To fix (1), the SharedTermsVisitor is update to track which theories has preregistered each term, as is done in the PreRegisterVisitor. To fix (2), we no longer apply-subst after theory preprocessing.
These two fixes are required to fix #6071.
Note: we should performance test this on SMT-LIB.
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 37 |
1 files changed, 27 insertions, 10 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 3a3003ba9..253f21d98 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -113,8 +113,9 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TheoryIdSet visitedTheories = d_visited[current]; // call the preregistration on current, parent or type theories and update - // visitedTheories. - preRegister(d_engine, visitedTheories, current, parent); + // visitedTheories. The set of preregistering theories coincides with + // visitedTheories here. + preRegister(d_engine, visitedTheories, current, parent, visitedTheories); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent @@ -129,17 +130,20 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { void PreRegisterVisitor::preRegister(TheoryEngine* te, TheoryIdSet& visitedTheories, TNode current, - TNode parent) + TNode parent, + TheoryIdSet preregTheories) { // Preregister with the current theory, if necessary TheoryId currentTheoryId = Theory::theoryOf(current); - preRegisterWithTheory(te, visitedTheories, currentTheoryId, current, parent); + preRegisterWithTheory( + te, visitedTheories, currentTheoryId, current, parent, preregTheories); if (current != parent) { // preregister with parent theory, if necessary TheoryId parentTheoryId = Theory::theoryOf(parent); - preRegisterWithTheory(te, visitedTheories, parentTheoryId, current, parent); + preRegisterWithTheory( + te, visitedTheories, parentTheoryId, current, parent, preregTheories); // Note that if enclosed by different theories it's shared, for example, // in read(a, f(a)), f(a) should be shared with integers. @@ -148,7 +152,8 @@ void PreRegisterVisitor::preRegister(TheoryEngine* te, { // preregister with the type's theory, if necessary TheoryId typeTheoryId = Theory::theoryOf(type); - preRegisterWithTheory(te, visitedTheories, typeTheoryId, current, parent); + preRegisterWithTheory( + te, visitedTheories, typeTheoryId, current, parent, preregTheories); } } } @@ -156,11 +161,18 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te, TheoryIdSet& visitedTheories, TheoryId id, TNode current, - TNode parent) + TNode parent, + TheoryIdSet preregTheories) { if (TheoryIdSetUtil::setContains(id, visitedTheories)) { - // already registered + // already visited + return; + } + visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories); + if (TheoryIdSetUtil::setContains(id, preregTheories)) + { + // already pregregistered return; } if (Configuration::isAssertionBuild()) @@ -192,7 +204,6 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te, } } // call the theory's preRegisterTerm method - visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories); Theory* th = te->theoryOf(id); th->preRegisterTerm(current); } @@ -242,13 +253,19 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { Debug("register::internal") << toString() << std::endl; } TheoryIdSet visitedTheories = d_visited[current]; + TheoryIdSet preregTheories = d_preregistered[current]; // preregister the term with the current, parent or type theories, as needed - PreRegisterVisitor::preRegister(d_engine, visitedTheories, current, parent); + PreRegisterVisitor::preRegister( + d_engine, visitedTheories, current, parent, preregTheories); // Record the new theories that we visited d_visited[current] = visitedTheories; + // add visited theories to those who have preregistered + d_preregistered[current] = + TheoryIdSetUtil::setUnion(preregTheories, visitedTheories); + // If there is more than two theories and a new one has been added notify the shared terms database TheoryId currentTheoryId = Theory::theoryOf(current); if (TheoryIdSetUtil::setDifference( |