diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-02 20:57:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-02 20:57:58 -0500 |
commit | bbfb310eba34ae078ee2601c7e5ea2b56dbe1252 (patch) | |
tree | 665707ebb7d940357317594ebf8ca01ff92ba60c /src/theory | |
parent | 6dd4efeea9fa0d9975fcffecd5af03bc081b68e7 (diff) |
Use prenex normal form when using cegqi-nested-qe (#4522)
Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.
This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 228 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 21 |
2 files changed, 121 insertions, 128 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index df86922bc..43c6e73bc 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1342,15 +1342,19 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& } Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){ - if( body.getKind()==FORALL ){ + NodeManager* nm = NodeManager::currentNM(); + Kind k = body.getKind(); + if (k == FORALL) + { if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers //must rename each variable that already exists - for( unsigned i=0; i<body[0].getNumChildren(); i++ ){ - terms.push_back( body[0][i] ); - subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); + for (const Node& v : body[0]) + { + terms.push_back(v); + subs.push_back(nm->mkBoundVar(v.getType())); } if( pol ){ args.insert( args.end(), subs.begin(), subs.end() ); @@ -1362,161 +1366,134 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s return newBody; } //must remove structure - }else if( prenexAgg && body.getKind()==kind::ITE && body.getType().isBoolean() ){ - Node nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), - NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) ); + } + else if (prenexAgg && k == ITE && body.getType().isBoolean()) + { + Node nn = nm->mkNode(AND, + nm->mkNode(OR, body[0].notNode(), body[1]), + nm->mkNode(OR, body[0], body[2])); return computePrenex( nn, args, nargs, pol, prenexAgg ); - }else if( prenexAgg && body.getKind()==kind::EQUAL && body[0].getType().isBoolean() ){ - Node nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), - NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); + } + else if (prenexAgg && k == EQUAL && body[0].getType().isBoolean()) + { + Node nn = nm->mkNode(AND, + nm->mkNode(OR, body[0].notNode(), body[1]), + nm->mkNode(OR, body[0], body[1].notNode())); return computePrenex( nn, args, nargs, pol, prenexAgg ); }else if( body.getType().isBoolean() ){ - Assert(body.getKind() != EXISTS); + Assert(k != EXISTS); bool childrenChanged = false; std::vector< Node > newChildren; - for( unsigned i=0; i<body.getNumChildren(); i++ ){ + for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++) + { bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); - if( newHasPol ){ - Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg ); - newChildren.push_back( n ); - if( n!=body[i] ){ - childrenChanged = true; - } - }else{ + if (!newHasPol) + { newChildren.push_back( body[i] ); + continue; } + Node n = computePrenex(body[i], args, nargs, newPol, prenexAgg); + newChildren.push_back(n); + childrenChanged = n != body[i] || childrenChanged; } if( childrenChanged ){ - if( body.getKind()==NOT && newChildren[0].getKind()==NOT ){ + if (k == NOT && newChildren[0].getKind() == NOT) + { return newChildren[0][0]; - }else{ - return NodeManager::currentNM()->mkNode( body.getKind(), newChildren ); } + return nm->mkNode(k, newChildren); } } return body; } -Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ){ - unsigned tindex = topLevel ? 0 : 1; - std::map< Node, Node >::iterator itv = visited[tindex].find( n ); - if( itv!=visited[tindex].end() ){ +Node QuantifiersRewriter::computePrenexAgg(Node n, + std::map<Node, Node>& visited) +{ + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv!=visited.end() ){ return itv->second; } - if (expr::hasClosure(n)) + if (!expr::hasClosure(n)) + { + // trivial + return n; + } + NodeManager* nm = NodeManager::currentNM(); + Node ret = n; + if (n.getKind() == NOT) + { + ret = computePrenexAgg(n[0], visited).negate(); + } + else if (n.getKind() == FORALL) { - Node ret = n; - if (topLevel - && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - && (n.getKind() == AND || (n.getKind() == NOT && n[0].getKind() == OR))) + std::vector<Node> children; + children.push_back(computePrenexAgg(n[1], visited)); + std::vector<Node> args; + args.insert(args.end(), n[0].begin(), n[0].end()); + // for each child, strip top level quant + for (unsigned i = 0; i < children.size(); i++) { - std::vector< Node > children; - Node nc = n.getKind()==NOT ? n[0] : n; - for( unsigned i=0; i<nc.getNumChildren(); i++ ){ - Node ncc = computePrenexAgg( nc[i], true, visited ); - if( n.getKind()==NOT ){ - ncc = ncc.negate(); - } - children.push_back( ncc ); + if (children[i].getKind() == FORALL) + { + args.insert(args.end(), children[i][0].begin(), children[i][0].end()); + children[i] = children[i][1]; } - ret = NodeManager::currentNM()->mkNode( AND, children ); } - else if (n.getKind() == NOT) + // keep the pattern + std::vector<Node> iplc; + if (n.getNumChildren() == 3) { - ret = computePrenexAgg( n[0], false, visited ).negate(); + iplc.insert(iplc.end(), n[2].begin(), n[2].end()); } - else if (n.getKind() == FORALL) + Node nb = children.size() == 1 ? children[0] : nm->mkNode(OR, children); + ret = mkForall(args, nb, iplc, true); + } + else + { + std::vector<Node> args; + std::vector<Node> nargs; + Node nn = computePrenex(n, args, nargs, true, true); + if (n != nn) { - /* - Node nn = computePrenexAgg( n[1], false ); - if( nn!=n[1] ){ - if( n.getNumChildren()==2 ){ - return NodeManager::currentNM()->mkNode( FORALL, n[0], nn ); - }else{ - return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] ); - } - } - */ - std::vector< Node > children; - if (n[1].getKind() == OR - && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL) + Node nnn = computePrenexAgg(nn, visited); + // merge prenex + if (nnn.getKind() == FORALL) { - for( unsigned i=0; i<n[1].getNumChildren(); i++ ){ - children.push_back( computePrenexAgg( n[1][i], false, visited ) ); + args.insert(args.end(), nnn[0].begin(), nnn[0].end()); + nnn = nnn[1]; + // pos polarity variables are inner + if (!args.empty()) + { + nnn = mkForall(args, nnn, true); } + args.clear(); } - else + else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) { - children.push_back( computePrenexAgg( n[1], false, visited ) ); + nargs.insert(nargs.end(), nnn[0][0].begin(), nnn[0][0].end()); + nnn = nnn[0][1].negate(); } - std::vector< Node > args; - for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ - args.push_back( n[0][i] ); + if (!nargs.empty()) + { + nnn = mkForall(nargs, nnn.negate(), true).negate(); } - std::vector< Node > nargs; - //for each child, strip top level quant - for( unsigned i=0; i<children.size(); i++ ){ - if( children[i].getKind()==FORALL ){ - for( unsigned j=0; j<children[i][0].getNumChildren(); j++ ){ - args.push_back( children[i][0][j] ); - } - children[i] = children[i][1]; - } + if (!args.empty()) + { + nnn = mkForall(args, nnn, true); } - // keep the pattern - std::vector< Node > iplc; - if( n.getNumChildren()==3 ){ - for( unsigned i=0; i<n[2].getNumChildren(); i++ ){ - iplc.push_back( n[2][i] ); - } - } - Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); - ret = mkForall( args, nb, iplc, true ); + ret = nnn; } else { - std::vector< Node > args; - std::vector< Node > nargs; - Node nn = computePrenex( n, args, nargs, true, true ); - if( n!=nn ){ - Node nnn = computePrenexAgg( nn, false, visited ); - //merge prenex - if( nnn.getKind()==FORALL ){ - for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){ - args.push_back( nnn[0][i] ); - } - nnn = nnn[1]; - //pos polarity variables are inner - if( !args.empty() ){ - nnn = mkForall( args, nnn, true ); - } - args.clear(); - }else if( nnn.getKind()==NOT && nnn[0].getKind()==FORALL ){ - for( unsigned i=0; i<nnn[0][0].getNumChildren(); i++ ){ - nargs.push_back( nnn[0][0][i] ); - } - nnn = nnn[0][1].negate(); - } - if( !nargs.empty() ){ - nnn = mkForall( nargs, nnn.negate(), true ).negate(); - } - if( !args.empty() ){ - nnn = mkForall( args, nnn, true ); - } - ret = nnn; - }else{ - Assert(args.empty()); - Assert(nargs.empty()); - } + Assert(args.empty()); + Assert(nargs.empty()); } - visited[tindex][n] = ret; - return ret; } - return n; + visited[n] = ret; + return ret; } Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { @@ -1925,8 +1902,7 @@ Node QuantifiersRewriter::computeOperation(Node f, if( computeOption==COMPUTE_ELIM_SYMBOLS ){ n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ - if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - || options::prenexQuant() == options::PrenexQuantMode::NORMAL) + if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) { if( !qa.d_qid_num.isNull() ){ //already processed this, return self @@ -1957,8 +1933,7 @@ Node QuantifiersRewriter::computeOperation(Node f, } else if (computeOption == COMPUTE_PRENEX) { - if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - || options::prenexQuant() == options::PrenexQuantMode::NORMAL) + if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) { //will rewrite at preprocess time return f; @@ -2091,12 +2066,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } } //pull all quantifiers globally - if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - || options::prenexQuant() == options::PrenexQuantMode::NORMAL) + if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) { Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; - std::map< unsigned, std::map< Node, Node > > visited; - n = computePrenexAgg( n, true, visited ); + std::map<Node, Node> visited; + n = computePrenexAgg(n, visited); n = Rewriter::rewrite( n ); Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; //Assert( isPrenexNormalForm( n ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2a3180e78..c8995ef4e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -234,8 +234,27 @@ class QuantifiersRewriter : public TheoryRewriter static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); + /** + * This function removes top-level quantifiers from subformulas of body + * appearing with overall polarity pol. It adds quantified variables that + * appear in positive polarity positions into args, and those at negative + * polarity positions in nargs. + * + * If prenexAgg is true, we ensure that all top-level quantifiers are + * eliminated from subformulas. This means that we must expand ITE and + * Boolean equalities to ensure that quantifiers are at fixed polarities. + * + * For example, calling this function on: + * (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z)))) + * would return: + * (or (P x z) (not (Q y z))) + * and add {x} to args, and {y} to nargs. + */ static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); - static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ); + /** + * Apply prenexing aggressively. Returns the prenex normal form of n. + */ + static Node computePrenexAgg(Node n, std::map<Node, Node>& visited); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); private: static Node computeOperation(Node f, |