diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 88 |
1 files changed, 49 insertions, 39 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d25e516fe..dabaa2188 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -185,51 +185,55 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ + RewriteStatus status = REWRITE_DONE; + Node ret = in; //get the arguments std::vector< Node > args; for( int i=0; i<(int)in[0].getNumChildren(); i++ ){ args.push_back( in[0][i] ); } - //get the body - Node body = in[1]; - if( in.getKind()==EXISTS ){ - body = body.getKind()==NOT ? body[0] : body.notNode(); - } //get the instantiation pattern list Node ipl; if( in.getNumChildren()==3 ){ ipl = in[2]; } - bool isNested = in.hasAttribute(NestedQuantAttribute()); - //compute miniscoping first - Node n = body;//computeNNF( body ); TODO: compute NNF here (current bad idea since arithmetic rewrites equalities) - if( body!=n ){ - Notice() << "NNF " << body << " -> " << n << std::endl; - } - n = computeMiniscoping( args, n, ipl, isNested ); - if( in.getKind()==kind::EXISTS ){ - n = n.getKind()==NOT ? n[0] : n.notNode(); + //get the body + if( in.getKind()==EXISTS ){ + std::vector< Node > children; + children.push_back( in[0] ); + children.push_back( in[1].negate() ); + if( in.getNumChildren()==3 ){ + children.push_back( in[2] ); + } + ret = NodeManager::currentNM()->mkNode( FORALL, children ); + ret = ret.negate(); + status = REWRITE_AGAIN_FULL; + }else{ + bool isNested = in.hasAttribute(NestedQuantAttribute()); + for( int op=0; op<COMPUTE_LAST; op++ ){ + if( doOperation( in, isNested, op ) ){ + ret = computeOperation( in, op ); + if( ret!=in ){ + status = REWRITE_AGAIN_FULL; + break; + } + } + } } - //compute other rewrite options for each produced quantifier - n = rewriteQuants( n, isNested, true ); //print if changed - if( in!=n ){ + if( in!=ret ){ if( in.hasAttribute(NestedQuantAttribute()) ){ - setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) ); + setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) ); } - Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; - Trace("quantifiers-rewrite") << " to " << std::endl; - Trace("quantifiers-rewrite") << n << std::endl; if( in.hasAttribute(InstConstantAttribute()) ){ InstConstantAttribute ica; - n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) ); + ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) ); } - - // This is required if substitute in computePrenex() is used. - return RewriteResponse(REWRITE_AGAIN_FULL, n ); - }else{ - return RewriteResponse(REWRITE_DONE, n ); + Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; + Trace("quantifiers-rewrite") << " to " << std::endl; + Trace("quantifiers-rewrite") << ret << std::endl; } + return RewriteResponse( status, ret ); } return RewriteResponse(REWRITE_DONE, in); } @@ -542,7 +546,10 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ if( f.getNumChildren()==3 ){ ipl = f[2]; } - if( computeOption==COMPUTE_NNF ){ + if( computeOption==COMPUTE_MINISCOPING ){ + //return directly + return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) ); + }else if( computeOption==COMPUTE_NNF ){ n = computeNNF( n ); }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){ n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX ); @@ -663,25 +670,25 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } return mkForAll( args, body, ipl ); } - -Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested, bool duringRewrite ){ +/* +Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested ){ if( n.getKind()==FORALL ){ - return rewriteQuant( n, isNested, duringRewrite ); + return rewriteQuant( n, isNested ); }else if( isLiteral( n ) ){ return n; }else{ NodeBuilder<> tt(n.getKind()); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - tt << rewriteQuants( n[i], isNested, duringRewrite ); + tt << rewriteQuants( n[i], isNested ); } return tt.constructNode(); } } -Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrite ){ +Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested ){ Node prev = n; for( int op=0; op<COMPUTE_LAST; op++ ){ - if( doOperation( n, isNested, op, duringRewrite ) ){ + if( doOperation( n, isNested, op ) ){ Node prev2 = n; n = computeOperation( n, op ); if( prev2!=n ){ @@ -695,9 +702,10 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit return n; }else{ //rewrite again until fix point is reached - return rewriteQuant( n, isNested, duringRewrite ); + return rewriteQuant( n, isNested ); } } +*/ bool QuantifiersRewriter::doMiniscopingNoFreeVar(){ return options::miniscopeQuantFreeVar(); @@ -715,17 +723,19 @@ bool QuantifiersRewriter::doMiniscopingAnd(){ } } -bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, bool duringRewrite ){ - if( computeOption==COMPUTE_NNF ){ +bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){ + if( computeOption==COMPUTE_MINISCOPING ){ + return true; + }else if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) }else if( computeOption==COMPUTE_PRE_SKOLEM ){ - return false;//options::preSkolemQuant() && !duringRewrite; + return false;//options::preSkolemQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant(); }else if( computeOption==COMPUTE_CNF ){ - return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind(); + return false;//return options::cnfQuant() ; }else{ return false; } |