From d0a8c9b331022dce224c230c6b6d7edd416d5866 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 9 Feb 2021 00:37:10 -0300 Subject: [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 +- src/theory/quantifiers/quantifiers_rewriter.cpp | 132 ++++++++++++++---------- src/theory/quantifiers/quantifiers_rewriter.h | 19 ++-- 3 files changed, 89 insertions(+), 65 deletions(-) (limited to 'src') 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 */ - - -- cgit v1.2.3