From 60746dc3ac7806475b5b6dab03123df024bf613e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 5 Jun 2020 05:22:18 -0700 Subject: [PATCH] Fix handling of Boolean term variables (#4550) Fixes #4446. This commit fixes two issues related to the handling of Boolean term variables: Removing Boolean subterms and replacing them with a Boolean term variable introduces an equality of the form (= v t) where v is the Boolean term variable and t is the term. It is important that these equalities do not get removed. This commit changes Theory::isLegalElimination() to take this into account. The incorrect model reported in the issue was caused by some of the Boolean term variables not being assigned values by the SAT solver when we decided that the benchmark is satisfiable. Our justification heuristic (correctly) decided that it is enough to satisfy one of the disjuncts in the assertion to satisfy the whole assertion. However, the assignments that we received from the SAT solver restricted us to pick a specific value for one of the Boolean constants: Literal | Value | Expr --------------------------------------------------------- '7 ' 0 c '0 ' 1 true '1 ' 0 false '2 ' 0 (a BOOLEAN_TERM_VARIABLE_274) '5 ' _ b '3 ' 1 (a BOOLEAN_TERM_VARIABLE_277) '4 ' _ BOOLEAN_TERM_VARIABLE_274 '6 ' 0 BOOLEAN_TERM_VARIABLE_277 This meant that we had to pick true for BOOLEAN_TERM_VARIABLE_274 but we picked false since we simply treated it as an unassigned variable. In general, the justification heuristic handles embedded skolems introduced by term removal first and asks the SAT solver to decide on Boolean term variables. However, for some logics, such as QF_AUFLIA, we use the justification heuristic not for decisions but only to decide when to stop, so those decisions were not done. This commit introduces a conservative fix that adds a check after satsifying all the assertions that makes sure that the equalities introduced for Boolean terms are satisfied as well. Due to the eager treatment of Boolean term variables when we use the justification heuristic also for decisions, it is likely that we don't really have the problem in that case but it doesn't hurt to enable the fix. It is also possible that this fix is only required with models but it is definitely safer to just always enable it (there could be tricky corner cases involving the theory combination between UF and Boolean terms). Additionally, this commit changes the ITE-specific naming in the justification heuristic to reflect more accurately that we are in general dealing with skolems introduced by term removals and not only due to ITE removal. --- src/decision/justification_heuristic.cpp | 86 +++++++++++++++--------- src/decision/justification_heuristic.h | 28 ++++---- src/theory/theory.cpp | 5 ++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/uf/issue4446.smt2 | 7 ++ 5 files changed, 80 insertions(+), 47 deletions(-) create mode 100644 test/regress/regress0/uf/issue4446.smt2 diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index ce79d6ca0..a3873c6da 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -40,10 +40,10 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, d_giveup("decision::jh::giveup", 0), d_timestat("decision::jh::time"), d_assertions(uc), - d_iteAssertions(uc), - d_iteCache(uc), + d_skolemAssertions(uc), + d_skolemCache(uc), d_visited(), - d_visitedComputeITE(), + d_visitedComputeSkolems(), d_curDecision(), d_curThreshold(0), d_childCache(uc), @@ -175,10 +175,26 @@ void JustificationHeuristic::addAssertions( << " assertionsEnd = " << assertionsEnd << std::endl; - // Save the 'real' assertions locally - for (size_t i = 0; i < assertionsEnd; i++) + // Save all assertions locally, including the assertions generated by term + // removal. We have to make sure that we assign a value to all the Boolean + // term variables. To illustrate why this is, consider the case where we have + // a single assertion + // + // (or (f a) (f b)) + // + // where `f` is a function `Bool -> Bool`. Given an assignment: + // + // (f a) -> true + // (f b) -> false + // a -> false + // + // UF will not complain and the justification heuristic considers the + // assertion to be satisifed. However, we also have to make sure that we pick + // a value for `b` that is not in conflict with the other assignments (we can + // only choose `b` to be `true` otherwise the model is incorrect). + for (const Node& assertion : assertions) { - d_assertions.push_back(assertions[i]); + d_assertions.push_back(assertion); } // Save mapping between ite skolems and ite assertions @@ -188,7 +204,7 @@ void JustificationHeuristic::addAssertions( << assertions[(i.second)] << std::endl; Assert(i.second >= assertionsEnd && i.second < assertions.size()); - d_iteAssertions[i.first] = assertions[i.second]; + d_skolemAssertions[i.first] = assertions[i.second]; } // Automatic weight computation @@ -363,36 +379,39 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n) }//end of else } -JustificationHeuristic::IteList -JustificationHeuristic::getITEs(TNode n) +JustificationHeuristic::SkolemList JustificationHeuristic::getSkolems(TNode n) { - IteCache::iterator it = d_iteCache.find(n); - if(it != d_iteCache.end()) { + SkolemCache::iterator it = d_skolemCache.find(n); + if (it != d_skolemCache.end()) + { return (*it).second; - } else { - // Compute the list of ITEs - // TODO: optimize by avoiding multiple lookup for d_iteCache[n] - d_visitedComputeITE.clear(); - IteList ilist; - computeITEs(n, ilist); - d_iteCache.insert(n, ilist); + } + else + { + // Compute the list of Skolems + // TODO: optimize by avoiding multiple lookup for d_skolemCache[n] + d_visitedComputeSkolems.clear(); + SkolemList ilist; + computeSkolems(n, ilist); + d_skolemCache.insert(n, ilist); return ilist; } } -void JustificationHeuristic::computeITEs(TNode n, IteList &l) +void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l) { - Trace("decision::jh::ite") << " computeITEs( " << n << ", &l)\n"; - d_visitedComputeITE.insert(n); + Trace("decision::jh::skolems") << " computeSkolems( " << n << ", &l)\n"; + d_visitedComputeSkolems.insert(n); for(unsigned i=0; i