From c94d59516c62b481c7984830cf26753af16100a8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 7 Dec 2020 14:43:34 -0600 Subject: [PATCH] Fix issue with free variables introduced by quantifier rewriter (#5602) This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted. This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression. --- src/options/quantifiers_options.toml | 8 -- src/smt/set_defaults.cpp | 13 --- .../quantifiers/cegqi/ceg_instantiator.cpp | 7 +- .../quantifiers/quantifiers_rewriter.cpp | 98 +------------------ src/theory/quantifiers/quantifiers_rewriter.h | 3 +- test/regress/CMakeLists.txt | 1 + .../regress0/quantifiers/ufnia-fv-delta.smt2 | 5 + 7 files changed, 16 insertions(+), 119 deletions(-) create mode 100644 test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d29052042..57bf69162 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -177,14 +177,6 @@ header = "options/quantifiers_options.h" read_only = true help = "eliminate tautological disjuncts of quantified formulas" -[[option]] - name = "elimExtArithQuant" - category = "regular" - long = "elim-ext-arith-quant" - type = "bool" - default = "true" - help = "eliminate extended arithmetic symbols in quantified formulas" - [[option]] name = "extRewriteQuant" category = "regular" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 7e6bed464..ca5a2773b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -239,14 +239,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::fmfBound.set(true); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } - // Do not eliminate extended arithmetic symbols from quantified formulas, - // since some strategies, e.g. --re-elim-agg, introduce them. - if (!options::elimExtArithQuant.wasSetByUser()) - { - options::elimExtArithQuant.set(false); - Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp" - << std::endl; - } // Note we allow E-matching by default to support combinations of sequences // and quantifiers. } @@ -935,11 +927,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT); } - // do not eliminate extended arithmetic symbols from quantified formulas - if (!options::elimExtArithQuant.wasSetByUser()) - { - options::elimExtArithQuant.set(false); - } if (!options::eMatching.wasSetByUser()) { options::eMatching.set(options::fmfInstEngine()); diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index aa847d8ea..0a5deb480 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -250,9 +250,10 @@ bool CegInstantiator::isEligible( Node n ) { CegHandledStatus CegInstantiator::isCbqiKind(Kind k) { if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ - || k == EQUAL - || k == MULT - || k == NONLINEAR_MULT) + || k == EQUAL || k == MULT || k == NONLINEAR_MULT || k == DIVISION + || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL + || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == TO_INTEGER + || k == IS_INTEGER) { return CEG_HANDLED; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6d7275fac..20d807793 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -401,11 +401,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; if (!fbody.isNull()) { - Node r = computeProcessTerms2(fbody, - cache, - new_vars, - new_conds, - false); + Node r = computeProcessTerms2(fbody, cache, new_vars, new_conds); Assert(new_vars.size() == h.getNumChildren()); return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r)); } @@ -413,18 +409,13 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to // forall xy. false. } - return computeProcessTerms2(body, - cache, - new_vars, - new_conds, - options::elimExtArithQuant()); + return computeProcessTerms2(body, cache, new_vars, new_conds); } Node QuantifiersRewriter::computeProcessTerms2(Node body, std::map& cache, std::vector& new_vars, - std::vector& new_conds, - bool elimExtArith) + std::vector& new_conds) { NodeManager* nm = NodeManager::currentNM(); Trace("quantifiers-rewrite-term-debug2") @@ -438,8 +429,7 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body, for (size_t i = 0; i < body.getNumChildren(); i++) { // do the recursive call on children - Node nn = - computeProcessTerms2(body[i], cache, new_vars, new_conds, elimExtArith); + Node nn = computeProcessTerms2(body[i], cache, new_vars, new_conds); children.push_back(nn); changed = changed || nn != body[i]; } @@ -515,82 +505,6 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body, ret = nm->mkNode(ITE, iconds[i], elements[i], ret); } } - else if (elimExtArith) - { - if (ret.getKind() == INTS_DIVISION_TOTAL - || ret.getKind() == INTS_MODULUS_TOTAL) - { - Node num = ret[0]; - Node den = ret[1]; - if (den.isConst()) - { - const Rational& rat = den.getConst(); - Assert(!num.isConst()); - if (rat != 0) - { - Node intVar = nm->mkBoundVar(nm->integerType()); - new_vars.push_back(intVar); - Node cond; - if (rat > 0) - { - cond = nm->mkNode( - AND, - nm->mkNode(LEQ, nm->mkNode(MULT, den, intVar), num), - nm->mkNode( - LT, - num, - nm->mkNode( - MULT, - den, - nm->mkNode(PLUS, intVar, nm->mkConst(Rational(1)))))); - } - else - { - cond = nm->mkNode( - AND, - nm->mkNode(LEQ, nm->mkNode(MULT, den, intVar), num), - nm->mkNode( - LT, - num, - nm->mkNode( - MULT, - den, - nm->mkNode(PLUS, intVar, nm->mkConst(Rational(-1)))))); - } - new_conds.push_back(cond.negate()); - if (ret.getKind() == INTS_DIVISION_TOTAL) - { - ret = intVar; - } - else - { - ret = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar)); - } - } - } - } - else if (ret.getKind() == TO_INTEGER || ret.getKind() == IS_INTEGER) - { - Node intVar = nm->mkBoundVar(nm->integerType()); - new_vars.push_back(intVar); - new_conds.push_back( - nm->mkNode( - AND, - nm->mkNode(LT, - nm->mkNode(MINUS, ret[0], nm->mkConst(Rational(1))), - intVar), - nm->mkNode(LEQ, intVar, ret[0])) - .negate()); - if (ret.getKind() == TO_INTEGER) - { - ret = intVar; - } - else - { - ret = ret[0].eqNode(intVar); - } - } - } cache[body] = ret; return ret; } @@ -1865,9 +1779,7 @@ bool QuantifiersRewriter::doOperation(Node q, } else if (computeOption == COMPUTE_PROCESS_TERMS) { - return is_std - && (options::elimExtArithQuant() - || options::iteLiftQuant() != options::IteLiftQuantMode::NONE); + return is_std && options::iteLiftQuant() != options::IteLiftQuantMode::NONE; } else if (computeOption == COMPUTE_COND_SPLIT) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 550f5b1dc..78586fc87 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -155,8 +155,7 @@ class QuantifiersRewriter : public TheoryRewriter static Node computeProcessTerms2(Node body, std::map& cache, std::vector& new_vars, - std::vector& new_conds, - bool elimExtArith); + std::vector& new_conds); static void computeDtTesterIteSplit( Node n, std::map& pcons, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5298a2ca9..d0e28f9e5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -820,6 +820,7 @@ set(regress_0_tests regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/sygus-inst-nia-psyco-060.smt2 regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 + regress0/quantifiers/ufnia-fv-delta.smt2 regress0/rec-fun-const-parse-bug.smt2 regress0/rels/addr_book_0.cvc regress0/rels/atom_univ2.cvc diff --git a/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 b/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 new file mode 100644 index 000000000..dfb87a1b9 --- /dev/null +++ b/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat +(set-logic UFNIA) +(assert (exists ((k Int)) (not (=> (forall ((a Int) (b Int)) (! (= k (ite (= 0 (mod a 2)) 1 0)) :pattern (b))) false)))) +(check-sat) -- 2.30.2