From d0a8c9b331022dce224c230c6b6d7edd416d5866 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 9 Feb 2021 00:37:10 -0300 Subject: [PATCH] [quantifiers] Fix prenex computation (#5879) Previously our prenex computation could generate quantifiers of the form forall x y y. F, which would lead to an assertion failure in getFreeVariablesScope, as it assumes that no shadowing occurs. This commit makes the prenex computation take a set rather than a vector, thus avoiding duplications of prenexed variables. It also changes mkForall to take a constant vector, since it does not modify the given vector. Fixes #5693 --- src/expr/node_algorithm.cpp | 3 +- .../quantifiers/quantifiers_rewriter.cpp | 132 ++++++++++-------- src/theory/quantifiers/quantifiers_rewriter.h | 19 ++- test/regress/CMakeLists.txt | 2 + .../quantifiers/issue5693-prenex.smt2 | 7 + ...prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 | 19 +++ 6 files changed, 117 insertions(+), 65 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue5693-prenex.smt2 create mode 100644 test/regress/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 2439e28b6..34ebfcd59 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -375,7 +375,8 @@ bool getFreeVariablesScope(TNode n, for (const TNode& cn : cur[0]) { // should not shadow - Assert(scope.find(cn) == scope.end()); + Assert(scope.find(cn) == scope.end()) + << "Shadowed variable " << cn << " in " << cur << "\n"; scope.insert(cn); } // must make recursive call to use separate cache diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6ca2e5b22..2126bf1f0 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1237,12 +1237,13 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } -Node QuantifiersRewriter::computePrenex(Node q, - Node body, - std::vector& args, - std::vector& nargs, - bool pol, - bool prenexAgg) +Node QuantifiersRewriter::computePrenex( + Node q, + Node body, + std::unordered_set& args, + std::unordered_set& nargs, + bool pol, + bool prenexAgg) { NodeManager* nm = NodeManager::currentNM(); Kind k = body.getKind(); @@ -1271,10 +1272,13 @@ Node QuantifiersRewriter::computePrenex(Node q, } subs.push_back(vv); } - if( pol ){ - args.insert( args.end(), subs.begin(), subs.end() ); - }else{ - nargs.insert( nargs.end(), subs.begin(), subs.end() ); + if (pol) + { + args.insert(subs.begin(), subs.end()); + } + else + { + nargs.insert(subs.begin(), subs.end()); } Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); @@ -1368,45 +1372,43 @@ Node QuantifiersRewriter::computePrenexAgg(Node n, } else { - std::vector args; - std::vector nargs; + std::unordered_set argsSet; + std::unordered_set nargsSet; Node q; - Node nn = computePrenex(q, n, args, nargs, true, true); + Node nn = computePrenex(q, n, argsSet, nargsSet, true, true); + Assert(n != nn || argsSet.empty()); + Assert(n != nn || nargsSet.empty()); if (n != nn) { Node nnn = computePrenexAgg(nn, visited); // merge prenex if (nnn.getKind() == FORALL) { - args.insert(args.end(), nnn[0].begin(), nnn[0].end()); + argsSet.insert(nnn[0].begin(), nnn[0].end()); nnn = nnn[1]; // pos polarity variables are inner - if (!args.empty()) + if (!argsSet.empty()) { - nnn = mkForall(args, nnn, true); + nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); } - args.clear(); + argsSet.clear(); } else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) { - nargs.insert(nargs.end(), nnn[0][0].begin(), nnn[0][0].end()); + nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end()); nnn = nnn[0][1].negate(); } - if (!nargs.empty()) + if (!nargsSet.empty()) { - nnn = mkForall(nargs, nnn.negate(), true).negate(); + nnn = mkForall({nargsSet.begin(), nargsSet.end()}, nnn.negate(), true) + .negate(); } - if (!args.empty()) + if (!argsSet.empty()) { - nnn = mkForall(args, nnn, true); + nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); } ret = nnn; } - else - { - Assert(args.empty()); - Assert(nargs.empty()); - } } visited[n] = ret; return ret; @@ -1516,43 +1518,58 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA } } -Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){ - if( args.empty() ){ +Node QuantifiersRewriter::mkForAll(const std::vector& args, + Node body, + QAttributes& qa) +{ + if (args.empty()) + { return body; - }else{ - std::vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); - children.push_back( body ); - if( !qa.d_ipl.isNull() ){ - children.push_back( qa.d_ipl ); - } - return NodeManager::currentNM()->mkNode( kind::FORALL, children ); } + NodeManager* nm = NodeManager::currentNM(); + std::vector children; + children.push_back(nm->mkNode(kind::BOUND_VAR_LIST, args)); + children.push_back(body); + if (!qa.d_ipl.isNull()) + { + children.push_back(qa.d_ipl); + } + return nm->mkNode(kind::FORALL, children); } -Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, bool marked ) { +Node QuantifiersRewriter::mkForall(const std::vector& args, + Node body, + bool marked) +{ std::vector< Node > iplc; return mkForall( args, body, iplc, marked ); } -Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked ) { - if( args.empty() ){ +Node QuantifiersRewriter::mkForall(const std::vector& args, + Node body, + std::vector& iplc, + bool marked) +{ + if (args.empty()) + { return body; - }else{ - std::vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); - children.push_back( body ); - if( marked ){ - Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); - QuantIdNumAttribute ida; - avar.setAttribute(ida,0); - iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); - } - if( !iplc.empty() ){ - children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) ); - } - return NodeManager::currentNM()->mkNode( FORALL, children ); } + NodeManager* nm = NodeManager::currentNM(); + std::vector children; + children.push_back(nm->mkNode(kind::BOUND_VAR_LIST, args)); + children.push_back(body); + if (marked) + { + Node avar = nm->mkSkolem("id", nm->booleanType()); + QuantIdNumAttribute ida; + avar.setAttribute(ida, 0); + iplc.push_back(nm->mkNode(kind::INST_ATTRIBUTE, avar)); + } + if (!iplc.empty()) + { + children.push_back(nm->mkNode(kind::INST_PATTERN_LIST, iplc)); + } + return nm->mkNode(kind::FORALL, children); } //computes miniscoping, also eliminates variables that do not occur free in body @@ -1865,9 +1882,10 @@ Node QuantifiersRewriter::computeOperation(Node f, } else { - std::vector< Node > nargs; - n = computePrenex(f, n, args, nargs, true, false); - Assert(nargs.empty()); + std::unordered_set argsSet, nargsSet; + n = computePrenex(f, n, argsSet, nargsSet, true, false); + Assert(nargsSet.empty()); + args.insert(args.end(), argsSet.begin(), argsSet.end()); } } else if (computeOption == COMPUTE_VAR_ELIMINATION) diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 1ceab7fc0..93f2c5dba 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -248,8 +248,8 @@ class QuantifiersRewriter : public TheoryRewriter */ static Node computePrenex(Node q, Node body, - std::vector& args, - std::vector& nargs, + std::unordered_set& args, + std::unordered_set& nargs, bool pol, bool prenexAgg); /** @@ -289,9 +289,16 @@ public: * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE. */ static TrustNode preprocess(Node n, bool isInst = false); - static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); - static Node mkForall( std::vector< Node >& args, Node body, bool marked = false ); - static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false ); + static Node mkForAll(const std::vector& args, + Node body, + QAttributes& qa); + static Node mkForall(const std::vector& args, + Node body, + bool marked = false); + static Node mkForall(const std::vector& args, + Node body, + std::vector& iplc, + bool marked = false); }; /* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ @@ -299,5 +306,3 @@ public: }/* CVC4 namespace */ #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ - - diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ddf810b0c..1e4f42ffd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -847,6 +847,7 @@ set(regress_0_tests regress0/quantifiers/issue4437-unc-quant.smt2 regress0/quantifiers/issue4576.smt2 regress0/quantifiers/issue5645-dt-cm-spurious.smt2 + regress0/quantifiers/issue5693-prenex.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macros-int-real.smt2 regress0/quantifiers/macros-real-arg.smt2 @@ -1784,6 +1785,7 @@ set(regress_1_tests regress1/quantifiers/nra-interleave-inst.smt2 regress1/quantifiers/opisavailable-12.smt2 regress1/quantifiers/parametric-lists.smt2 + regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 regress1/quantifiers/psyco-001-bv.smt2 regress1/quantifiers/psyco-107-bv.smt2 regress1/quantifiers/psyco-196.smt2 diff --git a/test/regress/regress0/quantifiers/issue5693-prenex.smt2 b/test/regress/regress0/quantifiers/issue5693-prenex.smt2 new file mode 100644 index 000000000..15ee0e7cf --- /dev/null +++ b/test/regress/regress0/quantifiers/issue5693-prenex.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --full-saturate-quant -i --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL) +(set-option :pre-skolem-quant true) +(declare-fun v7 () Bool) +(assert (forall ((q49 Bool) (q55 Bool)) (xor v7 (exists ((q49 Bool)) (xor v7 q49 q49)) v7 (= q55 q49)))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 b/test/regress/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 new file mode 100644 index 000000000..f0a4560d1 --- /dev/null +++ b/test/regress/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 @@ -0,0 +1,19 @@ +(set-info :smt-lib-version 2.6) +(set-logic LRA) +(set-info :source | + Scholl, Christoph; Disch, Stefan; Pigorsch, Florian and Kupferschmid, + Stefan; Using an SMT Solver and Craig Interpolation to Detect and Remove + Redundant Linear Constraints in Representations of Non-Convex Polyhedra. + Proceedings of 6th International Workshop on Satisfiability Modulo + Theories, Princeton, USA, July 2008. + +|) +(set-info :category "random") +(set-info :status unsat) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(assert (forall ((?x1 Real)) (exists ((?x2 Real)) (forall ((?x3 Real)) (exists ((?x4 Real)) (or (and (and (and (>= (+ (+ (* (- 54) ?x1) (* 62 ?x3)) (* (- 53) ?x4)) 79) (not (= (+ (+ (* (- 49) ?x1) (* 25 ?x2)) (* 51 ?x3)) 12))) (or (< (+ (+ (* 5 ?x1) (* 20 ?x2)) (* (- 1) ?x3)) 0) (not (= (+ (+ (* 58 ?x1) (* 61 ?x2)) (* 74 ?x3)) (- 18))))) (or (and (>= (+ (+ (* 48 ?x1) (* (- 47) ?x2)) (* 1 ?x4)) 61) (>= (+ (+ (* (- 19) ?x1) (* (- 80) ?x2)) (* (- 66) ?x3)) 25)) (and (<= (+ (+ (* (- 63) ?x2) (* (- 98) ?x3)) (* (- 4) ?x4)) (- 28)) (not (= (+ (+ (+ (* 10 ?x1) (* 47 ?x2)) (* 77 ?x3)) (* 73 ?x4)) 72))))) (and (or (or (= (+ (+ (* 40 ?x1) (* 16 ?x3)) (* 33 ?x4)) 0) (not (= (+ (+ (* 94 ?x2) (* (- 32) ?x3)) (* (- 19) ?x4)) (- 6)))) (or (not (= (+ (+ (+ (* (- 8) ?x1) (* (- 45) ?x2)) (* 34 ?x3)) (* 11 ?x4)) 57)) (> (+ (* (- 7) ?x2) (* (- 17) ?x3)) 0))) (and (< (+ (+ (+ (* 51 ?x1) (* 5 ?x2)) (* (- 86) ?x3)) (* (- 33) ?x4)) (- 32)) (and (>= (+ (* 50 ?x1) (* (- 46) ?x4)) 37) (not (= (+ (* (- 95) ?x2) (* (- 96) ?x4)) (- 24)))))))))))) +(check-sat) +(exit) -- 2.30.2