From: Andrew Reynolds Date: Thu, 9 Dec 2021 22:04:36 +0000 (-0600) Subject: Consider polarity in relevance manager (#7768) X-Git-Tag: cvc5-1.0.0~691 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93e71ff09714d504da93fbdb0448c656f60c0b98;p=cvc5.git Consider polarity in relevance manager (#7768) This ensures we only consider things relevant if their polarity is compatible with current asserted value. As a consequence, this makes our computation of get-difficulty more accurate, as well as making Valuation::isRelevant more precise (e.g. for non-linear). Notice that this fixes a bug in PolarityTermContext as well. --- diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp index 7f8aa9eac..02ec8981b 100644 --- a/src/expr/term_context.cpp +++ b/src/expr/term_context.cpp @@ -131,7 +131,7 @@ uint32_t PolarityTermContext::getValue(bool hasPol, bool pol) void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol) { - hasPol = val == 0; + hasPol = val != 0; pol = val == 2; } diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index 0ce021e08..9acf2dffc 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -17,6 +17,7 @@ #include +#include "expr/term_context_stack.h" #include "options/smt_options.h" #include "smt/env.h" @@ -123,7 +124,7 @@ void RelevanceManager::computeRelevance() for (const Node& node: d_input) { TNode n = node; - int val = justify(n); + int32_t val = justify(n); if (val != 1) { // if we are in full effort check and fail to justify, then we should @@ -165,22 +166,24 @@ bool RelevanceManager::isBooleanConnective(TNode cur) || (k == EQUAL && cur[0].getType().isBoolean()); } -bool RelevanceManager::updateJustifyLastChild(TNode cur, - std::vector& childrenJustify) +bool RelevanceManager::updateJustifyLastChild(const RlvPair& cur, + std::vector& childrenJustify) { // This method is run when we are informed that child index of cur // has justify status lastChildJustify. We return true if we would like to // compute the next child, in this case we push the status of the current // child to childrenJustify. - size_t nchildren = cur.getNumChildren(); - Assert(isBooleanConnective(cur)); + size_t nchildren = cur.first.getNumChildren(); + Assert(isBooleanConnective(cur.first)); size_t index = childrenJustify.size(); Assert(index < nchildren); - Assert(d_jcache.find(cur[index]) != d_jcache.end()); - Kind k = cur.getKind(); + Kind k = cur.first.getKind(); // Lookup the last child's value in the overall cache, we may choose to // add this to childrenJustify if we return true. - int lastChildJustify = d_jcache[cur[index]]; + RlvPair cp(cur.first[index], + d_ptctx.computeValue(cur.first, cur.second, index)); + Assert(d_jcache.find(cp) != d_jcache.end()); + int32_t lastChildJustify = d_jcache[cp]; if (k == NOT) { d_jcache[cur] = -lastChildJustify; @@ -269,30 +272,32 @@ bool RelevanceManager::updateJustifyLastChild(TNode cur, return false; } -int RelevanceManager::justify(TNode n) +int32_t RelevanceManager::justify(TNode n) { // The set of nodes that we have computed currently have no value. Those // that are marked as having no value in d_jcache must be recomputed, since // the values for SAT literals may have changed. - std::unordered_set noJustify; + std::unordered_set noJustify; // the vector of values of children - std::unordered_map> childJustify; - NodeUIntMap::iterator it; - std::unordered_map>::iterator itc; - std::vector visit; - TNode cur; - visit.push_back(n); + std::unordered_map, RlvPairHashFunction> + childJustify; + RlvPairIntMap::iterator it; + std::unordered_map, RlvPairHashFunction>::iterator + itc; + RlvPair cur; + TCtxStack visit(&d_ptctx); + visit.pushInitial(n); do { - cur = visit.back(); + cur = visit.getCurrent(); // should always have Boolean type - Assert(cur.getType().isBoolean()); + Assert(cur.first.getType().isBoolean()); it = d_jcache.find(cur); if (it != d_jcache.end()) { if (it->second != 0 || noJustify.find(cur) != noJustify.end()) { - visit.pop_back(); + visit.pop(); // already computed value continue; } @@ -302,30 +307,37 @@ int RelevanceManager::justify(TNode n) if (itc == childJustify.end()) { // are we not a Boolean connective (including NOT)? - if (isBooleanConnective(cur)) + if (isBooleanConnective(cur.first)) { // initialize its children justify vector as empty childJustify[cur].clear(); // start with the first child - visit.push_back(cur[0]); + visit.pushChild(cur.first, cur.second, 0); } else { - visit.pop_back(); + visit.pop(); // The atom case, lookup the value in the valuation class to // see its current value in the SAT solver, if it has one. int ret = 0; // otherwise we look up the value bool value; - if (d_val.hasSatValue(cur, value)) + if (d_val.hasSatValue(cur.first, value)) { ret = value ? 1 : -1; - d_rset.insert(cur); - if (d_trackRSetExp) + bool hasPol, pol; + PolarityTermContext::getFlags(cur.second, hasPol, pol); + // relevant if weakly matches polarity + if (!hasPol || pol == value) { - d_rsetExp[cur] = n; - Trace("rel-manager-exp") - << "Reason for " << cur << " is " << n << std::endl; + d_rset.insert(cur.first); + if (d_trackRSetExp) + { + d_rsetExp[cur.first] = n; + Trace("rel-manager-exp") + << "Reason for " << cur.first << " is " << n + << ", polarity is " << hasPol << "/" << pol << std::endl; + } } } d_jcache[cur] = ret; @@ -341,13 +353,12 @@ int RelevanceManager::justify(TNode n) // and possibly requests that a new child is computed. if (updateJustifyLastChild(cur, itc->second)) { - Assert(itc->second.size() < cur.getNumChildren()); - TNode nextChild = cur[itc->second.size()]; - visit.push_back(nextChild); + Assert(itc->second.size() < cur.first.getNumChildren()); + visit.pushChild(cur.first, cur.second, itc->second.size()); } else { - visit.pop_back(); + visit.pop(); Assert(d_jcache.find(cur) != d_jcache.end()); if (d_jcache[cur] == 0) { @@ -356,8 +367,9 @@ int RelevanceManager::justify(TNode n) } } } while (!visit.empty()); - Assert(d_jcache.find(n) != d_jcache.end()); - return d_jcache[n]; + RlvPair ci(n, d_ptctx.initialValue()); + Assert(d_jcache.find(ci) != d_jcache.end()); + return d_jcache[ci]; } bool RelevanceManager::isRelevant(Node lit) diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index 9bcf4af42..582a8a938 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -25,6 +25,7 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/node.h" +#include "expr/term_context.h" #include "smt/env_obj.h" #include "theory/difficulty_manager.h" #include "theory/valuation.h" @@ -76,10 +77,13 @@ class TheoryModel; */ class RelevanceManager : protected EnvObj { + using RlvPair = std::pair; + using RlvPairHashFunction = PairHashFunction>; using NodeList = context::CDList; using NodeMap = context::CDHashMap; using NodeSet = context::CDHashSet; - using NodeUIntMap = context::CDHashMap; + using RlvPairIntMap = + context::CDHashMap; public: /** @@ -155,9 +159,9 @@ class RelevanceManager : protected EnvObj * This method returns 1 if we justified n to be true, -1 means * justified n to be false, 0 means n could not be justified. */ - int justify(TNode n); + int32_t justify(TNode n); /** Is the top symbol of cur a Boolean connective? */ - bool isBooleanConnective(TNode cur); + static bool isBooleanConnective(TNode cur); /** * Update justify last child. This method is a helper function for justify, * which is called at the moment that Boolean connective formula cur @@ -170,7 +174,8 @@ class RelevanceManager : protected EnvObj * @return True if we wish to visit the next child. If this is the case, then * the justify value of the current child is added to childrenJustify. */ - bool updateJustifyLastChild(TNode cur, std::vector& childrenJustify); + bool updateJustifyLastChild(const RlvPair& cur, + std::vector& childrenJustify); /** The valuation object, used to query current value of theory literals */ Valuation d_val; /** The input assertions */ @@ -206,12 +211,18 @@ class RelevanceManager : protected EnvObj * reason why that literal is currently relevant. */ NodeMap d_rsetExp; + /** For computing polarity on terms */ + PolarityTermContext d_ptctx; /** * Set of nodes that we have justified (SAT context dependent). This is SAT * context dependent to avoid repeated calls to justify for uses of - * the relevance manager at standard effort. + * the relevance manager at standard effort. Notice that we pair each node + * with its polarity. We take into account the polarity of the node when + * computing relevance, where a node is only relevant if it is asserted + * and either does not have a polarity in the overall formula, or if its + * asserted value matches its polarity. */ - NodeUIntMap d_jcache; + RlvPairIntMap d_jcache; /** Difficulty module */ std::unique_ptr d_dman; }; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3881a142a..a51a81b19 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1684,6 +1684,7 @@ set(regress_1_tests regress1/decision/wishue149-2.smt2 regress1/decision/wishue149-3.smt2 regress1/decision/wishue160.smt2 + regress1/difficulty-polarity.smt2 regress1/errorcrash.smt2 regress1/fp/fp_to_real.smt2 regress1/fp/rti_3_5_bug_report.smt2 diff --git a/test/regress/regress1/difficulty-polarity.smt2 b/test/regress/regress1/difficulty-polarity.smt2 new file mode 100644 index 000000000..ce2388c54 --- /dev/null +++ b/test/regress/regress1/difficulty-polarity.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --produce-difficulty +; SCRUBBER: sed 's/.*//g' +; EXIT: 0 + +(set-logic ALL) +(set-option :finite-model-find true) +(set-option :mbqi none) +(set-option :produce-difficulty true) + +(declare-sort U 0) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(assert (distinct a b c)) +(declare-fun P (U U) Bool) +(declare-fun R (U) Bool) +(declare-fun S (U) Bool) + +(define-fun Q () Bool (forall ((x U) (y U)) (P x y))) + +(assert (or (not Q) (S a))) +(assert (R a)) +(assert (=> (R a) Q)) + +; This example will instantiate the quantified formula 9 times, hence the +; explanation for why it is relevant will be incremented by 9. +; The explanation for why Q is relevant should be (=> (R b) Q) and +; not (or (not Q) (S a)), since the former is the reason it is asserted true. + +(check-sat) +(get-difficulty)