diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 36 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 |
2 files changed, 18 insertions, 20 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 672cce959..3bf7749a4 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, std::vector< Node >& nargs, bool pol ){ +Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){ if( body.getKind()==FORALL ){ - if( ( pol || options::prenexQuantAgg() ) && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ + if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers @@ -1095,16 +1095,16 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s return newBody; } //must remove structure - }else if( options::prenexQuantAgg() && body.getKind()==kind::ITE && body.getType().isBoolean() ){ + }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] ) ); - return computePrenex( nn, args, nargs, pol ); - }else if( options::prenexQuantAgg() && body.getKind()==kind::IFF ){ + return computePrenex( nn, args, nargs, pol, prenexAgg ); + }else if( prenexAgg && 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 ); + return computePrenex( nn, args, nargs, pol, prenexAgg ); }else if( body.getType().isBoolean() ){ Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; @@ -1114,7 +1114,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); if( newHasPol ){ - Node n = computePrenex( body[i], args, nargs, newPol ); + Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg ); newChildren.push_back( n ); if( n!=body[i] ){ childrenChanged = true; @@ -1136,7 +1136,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ if( containsQuantifiers( n ) ){ - if( topLevel && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ + if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( 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 ); @@ -1160,7 +1160,7 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ } */ std::vector< Node > children; - if( n[1].getKind()==OR ){ + if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){ for( unsigned i=0; i<n[1].getNumChildren(); i++ ){ children.push_back( computePrenexAgg( n[1][i], false ) ); } @@ -1186,7 +1186,7 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ }else{ std::vector< Node > args; std::vector< Node > nargs; - Node nn = computePrenex( n, args, nargs, true ); + Node nn = computePrenex( n, args, nargs, true, true ); if( n!=nn ){ Node nnn = computePrenexAgg( nn, false ); //merge prenex @@ -1533,7 +1533,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q }else if( computeOption==COMPUTE_COND_SPLIT ){ return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger; }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; + return options::prenexQuant()!=PRENEX_QUANT_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() ) && is_std; }else{ @@ -1552,9 +1552,9 @@ 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( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ if( !qa.d_qid_num.isNull() ){ + //already processed this, return self return f; } } @@ -1572,14 +1572,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut }else if( computeOption==COMPUTE_COND_SPLIT ){ n = computeCondSplit( n, qa ); }else if( computeOption==COMPUTE_PRENEX ){ - if( options::prenexQuantAgg() ){ - //Node pf = computePrenexAgg( f ); - //Assert( isPrenexNormalForm( pf ) ); - //will do it at preprocess time + if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ + //will rewrite at preprocess time return f; }else{ std::vector< Node > nargs; - n = computePrenex( n, args, nargs, true ); + n = computePrenex( n, args, nargs, true, false ); Assert( nargs.empty() ); } }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ @@ -1823,7 +1821,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } } //pull all quantifiers globally - if( options::prenexQuantAgg() ){ + if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){ Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true ); n = Rewriter::rewrite( n ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2423caaee..90a22f4b7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -59,7 +59,7 @@ public: //cache is dependent upon currCond, icache is not, new_conds are negated conditions static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); static Node computeCondSplit( Node body, QAttributes& qa ); - static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ); + static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); static Node computePrenexAgg( Node n, bool topLevel ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); |