diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 54 |
1 files changed, 47 insertions, 7 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 24a6b78b0..672cce959 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1134,12 +1134,23 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s return body; } -Node QuantifiersRewriter::computePrenexAgg( Node n ){ +Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ if( containsQuantifiers( n ) ){ - if( n.getKind()==NOT ){ - return computePrenexAgg( n[0] ).negate(); + if( topLevel && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = computePrenexAgg( n[i], true ); + if( n.getKind()==NOT ){ + nc = nc.negate(); + } + children.push_back( nc ); + } + return NodeManager::currentNM()->mkNode( AND, children ); + }else if( n.getKind()==NOT ){ + return computePrenexAgg( n[0], false ).negate(); }else if( n.getKind()==FORALL ){ - Node nn = computePrenexAgg( n[1] ); + /* + Node nn = computePrenexAgg( n[1], false ); if( nn!=n[1] ){ if( n.getNumChildren()==2 ){ return NodeManager::currentNM()->mkNode( FORALL, n[0], nn ); @@ -1147,12 +1158,37 @@ Node QuantifiersRewriter::computePrenexAgg( Node n ){ return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] ); } } + */ + std::vector< Node > children; + if( n[1].getKind()==OR ){ + for( unsigned i=0; i<n[1].getNumChildren(); i++ ){ + children.push_back( computePrenexAgg( n[1][i], false ) ); + } + }else{ + children.push_back( computePrenexAgg( n[1], false ) ); + } + std::vector< Node > args; + for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ + args.push_back( n[0][i] ); + } + 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]; + } + } + Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + return mkForall( args, nb, true ); }else{ std::vector< Node > args; std::vector< Node > nargs; Node nn = computePrenex( n, args, nargs, true ); if( n!=nn ){ - Node nnn = computePrenexAgg( nn ); + Node nnn = computePrenexAgg( nn, false ); //merge prenex if( nnn.getKind()==FORALL ){ for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){ @@ -1770,6 +1806,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return n; } + Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { Node prev = n; if( n.getKind() == kind::REWRITE_RULE ){ @@ -1787,8 +1824,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } //pull all quantifiers globally if( options::prenexQuantAgg() ){ - n = quantifiers::QuantifiersRewriter::computePrenexAgg( n ); - Assert( isPrenexNormalForm( n ) ); + Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; + n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true ); + n = Rewriter::rewrite( n ); + Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; + //Assert( isPrenexNormalForm( n ) ); } if( n!=prev ){ Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; |