diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 13:03:31 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 13:03:45 -0500 |
commit | 9aaa7ca741199f73e70149f8309cd7cd9a12e69f (patch) | |
tree | 1dec877f28b4733f9a866620c1e671b4e522faf9 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 532a228bc718bde32afb3b96ca2cd3abcbd40f48 (diff) |
Option for prenex normal form
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 133 |
1 files changed, 123 insertions, 10 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index b0718699e..24a6b78b0 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1074,9 +1074,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } -Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){ +Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ){ if( body.getKind()==FORALL ){ - if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ + if( ( pol || options::prenexQuantAgg() ) && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers @@ -1085,14 +1085,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b terms.push_back( body[0][i] ); subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); } - args.insert( args.end(), subs.begin(), subs.end() ); + if( pol ){ + args.insert( args.end(), subs.begin(), subs.end() ); + }else{ + nargs.insert( nargs.end(), subs.begin(), subs.end() ); + } Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); return newBody; - }else{ - return body; } - }else{ + //must remove structure + }else if( options::prenexQuantAgg() && 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] ) ); + return computePrenex( nn, args, nargs, pol ); + }else if( options::prenexQuantAgg() && body.getKind()==kind::IFF ){ + 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() ) ); + return computePrenex( nn, args, nargs, pol ); + }else if( body.getType().isBoolean() ){ Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; std::vector< Node > newChildren; @@ -1101,7 +1114,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); if( newHasPol ){ - Node n = computePrenex( body[i], args, newPol ); + Node n = computePrenex( body[i], args, nargs, newPol ); newChildren.push_back( n ); if( n!=body[i] ){ childrenChanged = true; @@ -1116,10 +1129,61 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b }else{ return NodeManager::currentNM()->mkNode( body.getKind(), newChildren ); } + } + } + return body; +} + +Node QuantifiersRewriter::computePrenexAgg( Node n ){ + if( containsQuantifiers( n ) ){ + if( n.getKind()==NOT ){ + return computePrenexAgg( n[0] ).negate(); + }else if( n.getKind()==FORALL ){ + Node nn = computePrenexAgg( n[1] ); + 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] ); + } + } }else{ - return body; + std::vector< Node > args; + std::vector< Node > nargs; + Node nn = computePrenex( n, args, nargs, true ); + if( n!=nn ){ + Node nnn = computePrenexAgg( nn ); + //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 ); + } + return nnn; + }else{ + Assert( args.empty() ); + Assert( nargs.empty() ); + } } } + return n; } Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { @@ -1237,6 +1301,26 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri return NodeManager::currentNM()->mkNode( kind::FORALL, children ); } } +Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, 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 ); + std::vector< Node > iplc; + 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 ); + } +} //computes miniscoping, also eliminates variables that do not occur free in body Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){ @@ -1423,7 +1507,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q //general method for computing various rewrites Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){ - Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl; + Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl; std::vector< Node > args; for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ args.push_back( f[0][i] ); @@ -1432,6 +1516,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut if( computeOption==COMPUTE_ELIM_SYMBOLS ){ n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ + if( options::prenexQuantAgg() ){ + //if( isPrenexNormalForm( n ) ){ + if( !qa.d_qid_num.isNull() ){ + return f; + } + } //return directly return computeMiniscoping( args, n, qa ); }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ @@ -1446,7 +1536,16 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut }else if( computeOption==COMPUTE_COND_SPLIT ){ n = computeCondSplit( n, qa ); }else if( computeOption==COMPUTE_PRENEX ){ - n = computePrenex( n, args, true ); + if( options::prenexQuantAgg() ){ + //Node pf = computePrenexAgg( f ); + //Assert( isPrenexNormalForm( pf ) ); + //will do it at preprocess time + return f; + }else{ + std::vector< Node > nargs; + n = computePrenex( n, args, nargs, true ); + Assert( nargs.empty() ); + } }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ n = computeVarElimination( n, args, qa ); } @@ -1592,6 +1691,15 @@ bool QuantifiersRewriter::containsQuantifiers( Node n ){ return cq; } } +bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { + if( n.getKind()==FORALL ){ + return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] ); + }else if( n.getKind()==NOT ){ + return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] ); + }else{ + return !containsQuantifiers( n ); + } +} Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){ Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; @@ -1677,6 +1785,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } } } + //pull all quantifiers globally + if( options::prenexQuantAgg() ){ + n = quantifiers::QuantifiersRewriter::computePrenexAgg( n ); + Assert( isPrenexNormalForm( n ) ); + } if( n!=prev ){ Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; Trace("quantifiers-preprocess") << "..returned " << n << std::endl; |