diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index cc5a31aa8..79c300401 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -231,6 +231,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; RewriteStatus status = REWRITE_DONE; Node ret = in; + int rew_op = -1; //get the body if( in.getKind()==EXISTS ){ std::vector< Node > children; @@ -251,6 +252,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { if( doOperation( in, op, qa ) ){ ret = computeOperation( in, op, qa ); if( ret!=in ){ + rew_op = op; status = REWRITE_AGAIN_FULL; break; } @@ -260,7 +262,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { } //print if changed if( in!=ret ){ - Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; + Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl; Trace("quantifiers-rewrite") << " to " << std::endl; Trace("quantifiers-rewrite") << ret << std::endl; } @@ -1537,8 +1539,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg return mkForAll( args, body, qa ); } -bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){ - bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef(); +bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){ + bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST; + bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger; if( computeOption==COMPUTE_ELIM_SYMBOLS ){ return true; }else if( computeOption==COMPUTE_MINISCOPING ){ @@ -1551,15 +1554,15 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ - return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std; + return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger; }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); + return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std; //}else if( computeOption==COMPUTE_CNF ){ // return options::cnfQuant(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ - return options::purifyQuant(); + return options::purifyQuant() && is_std; }else{ return false; } @@ -1617,7 +1620,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut std::vector< Node > children; children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); children.push_back( n ); - if( !qa.d_ipl.isNull() ){ + if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){ children.push_back( qa.d_ipl ); } return NodeManager::currentNM()->mkNode(kind::FORALL, children ); |