From 982b585a1b766a933055d7328579cdb482504fe4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Aug 2021 16:42:14 -0500 Subject: [PATCH] Generalize inequality elimination in quantifiers rewriter (#7030) This generalizes our inequality elimination technique to handle disequalities as well as inequalities. #6999 is an example where a variable can be eliminated: if a variable x occurs only in an equality with negative required polarity, then the variable and that literal can be eliminated. Fixes #6999. --- .../quantifiers/quantifiers_rewriter.cpp | 111 ++++++++++++------ test/regress/CMakeLists.txt | 1 + .../quantifiers/issue6999-deq-elim.smt2 | 7 ++ 3 files changed, 80 insertions(+), 39 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue6999-deq-elim.smt2 diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0412513b2..646a4e485 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1021,20 +1021,45 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, std::vector& subs, QAttributes& qa) { - // elimination based on inequalities - std::map > > num_bounds; + Trace("var-elim-quant-debug") << "getVarElimIneq " << body << std::endl; + // For each variable v, we compute a set of implied bounds in the body + // of the quantified formula. + // num_bounds[x][-1] stores the entailed lower bounds for x + // num_bounds[x][1] stores the entailed upper bounds for x + // num_bounds[x][0] stores the entailed disequalities for x + // These bounds are stored in a map that maps the literal for the bound to + // its required polarity. For example, for quantified formula + // (forall ((x Int)) (or (= x 0) (>= x a))) + // we have: + // num_bounds[x][0] contains { x -> { (= x 0) -> false } } + // num_bounds[x][-1] contains { x -> { (>= x a) -> false } } + // This method succeeds in eliminating x if its only occurrences are in + // entailed disequalities, and one kind of bound. This is the case for the + // above quantified formula, which can be rewritten to false. The reason + // is that we can always chose a value for x that is arbitrarily large (resp. + // small) to satisfy all disequalities and inequalities for x. + std::map>> num_bounds; + // The set of variables that we know we can not eliminate + std::unordered_set ineligVars; + // compute the entailed literals QuantPhaseReq qpr(body); + // map to track which literals we have already processed, and hence can be + // excluded from the free variables check in the latter half of this method. + std::map processed; for (const std::pair& pr : qpr.d_phase_reqs) { // an inequality that is entailed with a given polarity Node lit = pr.first; - if (lit.getKind() != GEQ) - { - continue; - } bool pol = pr.second; Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit << ", pol = " << pol << "..." << std::endl; + bool canSolve = + lit.getKind() == GEQ + || (lit.getKind() == EQUAL && lit[0].getType().isReal() && !pol); + if (!canSolve) + { + continue; + } // solve the inequality std::map msum; if (!ArithMSum::getMonomialSumLit(lit, msum)) @@ -1042,9 +1067,10 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, // not an inequality, cannot use continue; } + processed[lit] = pol ? -1 : 1; for (const std::pair& m : msum) { - if (!m.first.isNull()) + if (!m.first.isNull() && ineligVars.find(m.first) == ineligVars.end()) { std::vector::iterator ita = std::find(args.begin(), args.end(), m.first); @@ -1057,13 +1083,22 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, ArithMSum::isolate(m.first, msum, veq_c, val, lit.getKind()); if (ires != 0 && veq_c.isNull()) { - bool is_upper = pol != (ires == 1); - Trace("var-elim-ineq-debug") - << lit << " is a " << (is_upper ? "upper" : "lower") - << " bound for " << m.first << std::endl; - Trace("var-elim-ineq-debug") - << " pol/ires = " << pol << " " << ires << std::endl; - num_bounds[m.first][is_upper][lit] = pol; + if (lit.getKind() == GEQ) + { + bool is_upper = pol != (ires == 1); + Trace("var-elim-ineq-debug") + << lit << " is a " << (is_upper ? "upper" : "lower") + << " bound for " << m.first << std::endl; + Trace("var-elim-ineq-debug") + << " pol/ires = " << pol << " " << ires << std::endl; + num_bounds[m.first][is_upper ? 1 : -1][lit] = pol; + } + else + { + Trace("var-elim-ineq-debug") + << lit << " is a disequality for " << m.first << std::endl; + num_bounds[m.first][0][lit] = pol; + } } else { @@ -1071,8 +1106,8 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, << "...ineligible " << m.first << " since it cannot be solved for (" << ires << ", " << veq_c << ")." << std::endl; - num_bounds[m.first][true].clear(); - num_bounds[m.first][false].clear(); + num_bounds.erase(m.first); + ineligVars.insert(m.first); } } else @@ -1086,8 +1121,8 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, Trace("var-elim-ineq-debug") << "...ineligible " << v << " since it is contained in monomial." << std::endl; - num_bounds[v][true].clear(); - num_bounds[v][false].clear(); + num_bounds.erase(v); + ineligVars.insert(v); } } } @@ -1096,16 +1131,16 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, // collect all variables that have only upper/lower bounds std::map elig_vars; - for (const std::pair > >& nb : + for (const std::pair>>& nb : num_bounds) { - if (nb.second.find(true) == nb.second.end()) + if (nb.second.find(1) == nb.second.end()) { Trace("var-elim-ineq-debug") << "Variable " << nb.first << " has only lower bounds." << std::endl; elig_vars[nb.first] = false; } - else if (nb.second.find(false) == nb.second.end()) + else if (nb.second.find(-1) == nb.second.end()) { Trace("var-elim-ineq-debug") << "Variable " << nb.first << " has only upper bounds." << std::endl; @@ -1118,17 +1153,6 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, } std::vector inactive_vars; std::map > visited; - std::map exclude; - for (const std::pair& pr : qpr.d_phase_reqs) - { - if (pr.first.getKind() == GEQ) - { - exclude[pr.first] = pr.second ? -1 : 1; - Trace("var-elim-ineq-debug") - << "...exclude " << pr.first << " at polarity " << exclude[pr.first] - << std::endl; - } - } // traverse the body, invalidate variables if they occur in places other than // the bounds they occur in std::unordered_map> evisited; @@ -1169,8 +1193,8 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, bool hasPol = ecur_pol != 0; if (hasPol) { - std::map::iterator itx = exclude.find(ecur); - if (itx != exclude.end() && itx->second == ecur_pol) + std::map::iterator itx = processed.find(ecur); + if (itx != processed.end() && itx->second == ecur_pol) { // already processed this literal as a bound rec = false; @@ -1192,6 +1216,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, } while (!evisit.empty() && !elig_vars.empty()); bool ret = false; + NodeManager* nm = NodeManager::currentNM(); for (const std::pair& ev : elig_vars) { Node v = ev.first; @@ -1199,12 +1224,18 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, << v << " is eligible for elimination." << std::endl; // do substitution corresponding to infinite projection, all literals // involving unbounded variable go to true/false - for (const std::pair& nb : num_bounds[v][elig_vars[v]]) + // disequalities of eligible variables are also eliminated + std::map>& nbv = num_bounds[v]; + for (size_t i = 0; i < 2; i++) { - Trace("var-elim-ineq-debug") - << " subs : " << nb.first << " -> " << nb.second << std::endl; - bounds.push_back(nb.first); - subs.push_back(NodeManager::currentNM()->mkConst(nb.second)); + size_t nindex = i == 0 ? (elig_vars[v] ? 1 : -1) : 0; + for (const std::pair& nb : nbv[nindex]) + { + Trace("var-elim-ineq-debug") + << " subs : " << nb.first << " -> " << nb.second << std::endl; + bounds.push_back(nb.first); + subs.push_back(nm->mkConst(nb.second)); + } } // eliminate from args std::vector::iterator ita = std::find(args.begin(), args.end(), v); @@ -1221,6 +1252,8 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& { return body; } + Trace("var-elim-quant-debug") + << "computeVarElimination " << body << std::endl; Node prev; while (prev != body && !args.empty()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d68400b66..55649c2f0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -911,6 +911,7 @@ set(regress_0_tests regress0/quantifiers/issue5693-prenex.smt2 regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 regress0/quantifiers/issue6996-trivial-elim.smt2 + regress0/quantifiers/issue6999-deq-elim.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 diff --git a/test/regress/regress0/quantifiers/issue6999-deq-elim.smt2 b/test/regress/regress0/quantifiers/issue6999-deq-elim.smt2 new file mode 100644 index 000000000..6ea8e6a2f --- /dev/null +++ b/test/regress/regress0/quantifiers/issue6999-deq-elim.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-sort T 0) +(declare-fun S (T Int) Int) +(declare-fun R (T Int Int) T) +(assert (forall ((z T) (x Int)) (= x (S (R z 0 0) 0)))) +(check-sat) -- 2.30.2