diff options
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 90 |
1 files changed, 55 insertions, 35 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index ce79d6ca0..9787e8b00 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -2,9 +2,9 @@ /*! \file justification_heuristic.cpp ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Aina Niemetz, Tim King + ** Kshitij Bansal, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -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<n.getNumChildren(); ++i) { - SkolemMap::iterator it2 = d_iteAssertions.find(n[i]); - if(it2 != d_iteAssertions.end()) { + SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]); + if (it2 != d_skolemAssertions.end()) + { l.push_back(make_pair(n[i], (*it2).second)); Assert(n[i].getNumChildren() == 0); } - if(d_visitedComputeITE.find(n[i]) == - d_visitedComputeITE.end()) { - computeITEs(n[i], l); + if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end()) + { + computeSkolems(n[i], l); } } } @@ -470,9 +489,8 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) * If not in theory of booleans, check if this is something to split-on. */ if(isAtom) { - // if node has embedded ites, resolve that first - if(handleEmbeddedITEs(node) == FOUND_SPLITTER) - return FOUND_SPLITTER; + // if node has embedded skolems due to term removal, resolve that first + if (handleEmbeddedSkolems(node) == FOUND_SPLITTER) return FOUND_SPLITTER; if(litVal != SAT_VALUE_UNKNOWN) { Assert(litVal == desiredVal); @@ -700,13 +718,15 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod }// else (...ifVal...) } -JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs(TNode node) +JustificationHeuristic::SearchResult +JustificationHeuristic::handleEmbeddedSkolems(TNode node) { - const IteList l = getITEs(node); - Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl; + const SkolemList l = getSkolems(node); + Trace("decision::jh::skolems") << " skolems size = " << l.size() << std::endl; bool noSplitter = true; - for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) { + for (SkolemList::const_iterator i = l.begin(); i != l.end(); ++i) + { if(d_visited.find((*i).first) == d_visited.end()) { d_visited.insert((*i).first); SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE); |