diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 590 |
1 files changed, 318 insertions, 272 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index afe8cd598..5aae4d640 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file quantifiers_rewriter.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of QuantifiersRewriter class **/ @@ -229,52 +229,48 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; - if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){ - 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 instantiation pattern list - Node ipl; + RewriteStatus status = REWRITE_DONE; + Node ret = in; + int rew_op = -1; + //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 ){ - ipl = in[2]; - } - //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; + children.push_back( in[2] ); + } + ret = NodeManager::currentNM()->mkNode( FORALL, children ); + ret = ret.negate(); + status = REWRITE_AGAIN_FULL; + }else if( in.getKind()==FORALL ){ + if( in[1].isConst() ){ + return RewriteResponse( status, in[1] ); }else{ - for( int op=0; op<COMPUTE_LAST; op++ ){ - //TODO : compute isNested (necessary?) - bool isNested = false; - if( doOperation( in, isNested, op ) ){ - ret = computeOperation( in, isNested, op ); - if( ret!=in ){ - status = REWRITE_AGAIN_FULL; - break; + //compute attributes + QAttributes qa; + TermDb::computeQuantAttributes( in, qa ); + if( !qa.isRewriteRule() ){ + for( int op=0; op<COMPUTE_LAST; op++ ){ + if( doOperation( in, op, qa ) ){ + ret = computeOperation( in, op, qa ); + if( ret!=in ){ + rew_op = op; + status = REWRITE_AGAIN_FULL; + break; + } } } } } - //print if changed - if( in!=ret ){ - 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); + //print if changed + if( in!=ret ){ + Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl; + Trace("quantifiers-rewrite") << " to " << std::endl; + Trace("quantifiers-rewrite") << ret << std::endl; + } + return RewriteResponse( status, ret ); } Node QuantifiersRewriter::computeElimSymbols( Node body ) { @@ -315,6 +311,10 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { } childrenChanged = childrenChanged || c!=body[i]; } + //if( body.getKind()==ITE && isLiteral( body[0] ) ){ + // ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), + // NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) ); + //} if( childrenChanged ){ return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children ); }else{ @@ -330,7 +330,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else if( isLiteral( body[0] ) ){ return body; }else{ - std::vector< Node > children; + std::vector< Node > children; Kind k = body[0].getKind(); if( body[0].getKind()==OR || body[0].getKind()==AND ){ @@ -564,12 +564,23 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v } } -Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ){ +void removeEntailedCond( std::map< Node, bool >& currCond, std::vector< Node >& new_cond, std::map< Node, Node >& cache ) { + if( !new_cond.empty() ){ + for( unsigned j=0; j<new_cond.size(); j++ ){ + currCond.erase( new_cond[j] ); + } + new_cond.clear(); + cache.clear(); + } +} + +Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ){ std::map< Node, bool > curr_cond; std::map< Node, Node > cache; std::map< Node, Node > icache; - Node h = TermDb::getFunDefHead( q ); - if( !h.isNull() ){ + if( qa.isFunDef() ){ + Node h = TermDb::getFunDefHead( q ); + Assert( !h.isNull() ); // if it is a function definition, rewrite the body independently Node fbody = TermDb::getFunDefBody( q ); Assert( !body.isNull() ); @@ -591,96 +602,119 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol ret = iti->second; Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl; }else{ - bool firstTimeCD = true; + //only do context dependent processing up to depth 8 + bool doCD = nCurrCond<8; bool changed = false; std::vector< Node > children; - for( size_t i=0; i<body.getNumChildren(); i++ ){ - std::vector< Node > new_cond; + //set entailed conditions based on OR/AND + std::map< int, std::vector< Node > > new_cond_children; + if( doCD && ( body.getKind()==OR || body.getKind()==AND ) ){ + nCurrCond = nCurrCond + 1; bool conflict = false; - //only do context dependent processing up to depth 8 - if( nCurrCond<8 ){ - if( firstTimeCD ){ - firstTimeCD = false; - nCurrCond = nCurrCond + 1; - } - if( Trace.isOn("quantifiers-rewrite-term-debug") ){ - //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ - if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ - Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl; + bool use_pol = body.getKind()==AND; + for( unsigned j=0; j<body.getNumChildren(); j++ ){ + setEntailedCond( body[j], use_pol, currCond, new_cond_children[j], conflict ); + } + if( conflict ){ + Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl; + ret = NodeManager::currentNM()->mkConst( !use_pol ); + } + } + if( ret.isNull() ){ + for( size_t i=0; i<body.getNumChildren(); i++ ){ + + //set/update entailed conditions + std::vector< Node > new_cond; + bool conflict = false; + if( doCD ){ + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl; + } } - } - if( body.getKind()==ITE && i>0 ){ - setEntailedCond( children[0], i==1, currCond, new_cond, conflict ); - //should not conflict (entailment check failed) - Assert( !conflict ); - } - //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){ - // bool use_pol = !pol; - if( body.getKind()==OR || body.getKind()==AND ){ - bool use_pol = body.getKind()==AND; - for( unsigned j=0; j<body.getNumChildren(); j++ ){ - if( j<i ){ - setEntailedCond( children[j], use_pol, currCond, new_cond, conflict ); - }else if( j>i ){ - setEntailedCond( body[j], use_pol, currCond, new_cond, conflict ); + if( body.getKind()==ITE && i>0 ){ + if( i==1 ){ + nCurrCond = nCurrCond + 1; } + setEntailedCond( children[0], i==1, currCond, new_cond, conflict ); + //should not conflict (entailment check failed) + Assert( !conflict ); } - if( conflict ){ - Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl; - ret = NodeManager::currentNM()->mkConst( !use_pol ); + if( body.getKind()==OR || body.getKind()==AND ){ + bool use_pol = body.getKind()==AND; + //remove the current condition + removeEntailedCond( currCond, new_cond_children[i], cache ); + if( i>0 ){ + //add the previous condition + setEntailedCond( children[i-1], use_pol, currCond, new_cond_children[i-1], conflict ); + } + if( conflict ){ + Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl; + ret = NodeManager::currentNM()->mkConst( !use_pol ); + } } - } - if( !new_cond.empty() ){ - cache.clear(); - } - if( Trace.isOn("quantifiers-rewrite-term-debug") ){ - //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ - if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ - Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl; + if( !new_cond.empty() ){ + cache.clear(); + } + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl; + } } } - } - if( !conflict ){ - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); - Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - if( body.getKind()==ITE && i==0 ){ - int res = getEntailedCond( nn, currCond ); - Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl; - if( res==1 ){ - ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - }else if( res==-1 ){ - ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + + //do the recursive call on children + if( !conflict ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); + Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + if( body.getKind()==ITE && i==0 ){ + int res = getEntailedCond( nn, currCond ); + Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl; + if( res==1 ){ + ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + }else if( res==-1 ){ + ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + } } + children.push_back( nn ); + changed = changed || nn!=body[i]; + } + + //clean up entailed conditions + removeEntailedCond( currCond, new_cond, cache ); + + if( !ret.isNull() ){ + break; } - children.push_back( nn ); - changed = changed || nn!=body[i]; } - if( !new_cond.empty() ){ - for( unsigned j=0; j<new_cond.size(); j++ ){ - currCond.erase( new_cond[j] ); + + //make return value + if( ret.isNull() ){ + if( changed ){ + if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), body.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); + }else{ + ret = body; } - cache.clear(); - } - if( !ret.isNull() ){ - break; } } - if( ret.isNull() ){ - if( changed ){ - if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), body.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); - }else{ - ret = body; + + //clean up entailed conditions + if( body.getKind()==OR || body.getKind()==AND ){ + for( unsigned j=0; j<body.getNumChildren(); j++ ){ + removeEntailedCond( currCond, new_cond_children[j], cache ); } } + Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl; cache[body] = ret; } + //do context-independent rewriting iti = icache.find( ret ); if( iti!=icache.end() ){ return iti->second; @@ -710,46 +744,60 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol } } } - }else if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){ - Node num = ret[0]; - Node den = ret[1]; - if(den.isConst()) { - const Rational& rat = den.getConst<Rational>(); - Assert(!num.isConst()); - if(rat != 0) { - Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - new_vars.push_back( intVar ); - Node cond; - if(rat > 0) { - cond = NodeManager::currentNM()->mkNode(kind::AND, - NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num), - NodeManager::currentNM()->mkNode(kind::LT, num, - NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(1)))))); - } else { - cond = NodeManager::currentNM()->mkNode(kind::AND, - NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num), - NodeManager::currentNM()->mkNode(kind::LT, num, - NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(-1)))))); - } - new_conds.push_back( cond.negate() ); - if( ret.getKind()==INTS_DIVISION_TOTAL ){ - ret = intVar; - }else{ - ret = NodeManager::currentNM()->mkNode(kind::MINUS, num, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar)); + /* ITE lifting + if( ret.getKind()==ITE ){ + TypeNode ite_t = ret[1].getType(); + if( !ite_t.isBoolean() ){ + ite_t = TypeNode::leastCommonTypeNode( ite_t, ret[2].getType() ); + Node ite_v = NodeManager::currentNM()->mkBoundVar(ite_t); + new_vars.push_back( ite_v ); + Node cond = NodeManager::currentNM()->mkNode(kind::ITE, ret[0], ite_v.eqNode( ret[1] ), ite_v.eqNode( ret[2] ) ); + new_conds.push_back( cond.negate() ); + ret = ite_v; + } + */ + }else if( options::elimExtArithQuant() ){ + if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){ + Node num = ret[0]; + Node den = ret[1]; + if(den.isConst()) { + const Rational& rat = den.getConst<Rational>(); + Assert(!num.isConst()); + if(rat != 0) { + Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); + new_vars.push_back( intVar ); + Node cond; + if(rat > 0) { + cond = NodeManager::currentNM()->mkNode(kind::AND, + NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num), + NodeManager::currentNM()->mkNode(kind::LT, num, + NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(1)))))); + } else { + cond = NodeManager::currentNM()->mkNode(kind::AND, + NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num), + NodeManager::currentNM()->mkNode(kind::LT, num, + NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(-1)))))); + } + new_conds.push_back( cond.negate() ); + if( ret.getKind()==INTS_DIVISION_TOTAL ){ + ret = intVar; + }else{ + ret = NodeManager::currentNM()->mkNode(kind::MINUS, num, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar)); + } } } - } - }else if( ret.getKind()==TO_INTEGER || ret.getKind()==IS_INTEGER ){ - Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - new_vars.push_back( intVar ); - new_conds.push_back(NodeManager::currentNM()->mkNode(kind::AND, - NodeManager::currentNM()->mkNode(kind::LT, - NodeManager::currentNM()->mkNode(kind::MINUS, ret[0], NodeManager::currentNM()->mkConst(Rational(1))), intVar), - NodeManager::currentNM()->mkNode(kind::LEQ, intVar, ret[0])).negate()); - if( ret.getKind()==TO_INTEGER ){ - ret = intVar; - }else{ - ret = ret[0].eqNode( intVar ); + }else if( ret.getKind()==TO_INTEGER || ret.getKind()==IS_INTEGER ){ + Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); + new_vars.push_back( intVar ); + new_conds.push_back(NodeManager::currentNM()->mkNode(kind::AND, + NodeManager::currentNM()->mkNode(kind::LT, + NodeManager::currentNM()->mkNode(kind::MINUS, ret[0], NodeManager::currentNM()->mkConst(Rational(1))), intVar), + NodeManager::currentNM()->mkNode(kind::LEQ, intVar, ret[0])).negate()); + if( ret.getKind()==TO_INTEGER ){ + ret = intVar; + }else{ + ret = ret[0].eqNode( intVar ); + } } } icache[prev] = ret; @@ -782,7 +830,7 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ return false; } -Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){ +Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){ Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; std::map< Node, Node > pcons; @@ -799,7 +847,8 @@ Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){ } } if( options::condVarSplitQuant() ){ - if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() && !TermDb::isFunDefAnnotation( ipl ) ) ){ + if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){ + Assert( !qa.isFunDef() ); Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl; bool do_split = false; unsigned index_max = body.getKind()==ITE ? 0 : 1; @@ -932,8 +981,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); std::vector< Node > newVars; for( unsigned j=0; j<c.getNumArgs(); j++ ){ - TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() ); - tn = tn[1]; + TypeNode tn = TypeNode::fromType( c[j].getRangeType() ); Node v = NodeManager::currentNM()->mkBoundVar( tn ); newChildren.push_back( v ); newVars.push_back( v ); @@ -957,7 +1005,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto return false; } -Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){ +Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ){ Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; QuantPhaseReq qpr( body ); std::vector< Node > vars; @@ -977,15 +1025,15 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node > //remake with eliminated nodes body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); body = Rewriter::rewrite( body ); - if( !ipl.isNull() ){ - ipl = ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + if( !qa.d_ipl.isNull() ){ + qa.d_ipl = qa.d_ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); } Trace("var-elim-quant") << "Return " << body << std::endl; } return body; } -Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ +Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){ //the parent id's for each variable, if using purifyQuant std::map< Node, std::vector< int > > var_parent; if( options::purifyQuant() ){ @@ -995,7 +1043,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& Node prev; do{ prev = body; - body = computeVarElimination2( body, args, ipl, var_parent ); + body = computeVarElimination2( body, args, qa, var_parent ); }while( prev!=body && !args.empty() ); } return body; @@ -1290,13 +1338,13 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node return f; } -Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ +Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){ std::vector< Node > activeArgs; //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables - if( options::ceGuidedInst() && TermDb::isSygusConjectureAnnotation( ipl ) ){ + if( options::ceGuidedInst() && qa.d_sygus ){ activeArgs.insert( activeArgs.end(), args.begin(), args.end() ); }else{ - computeArgVec2( args, activeArgs, body, ipl ); + computeArgVec2( args, activeArgs, body, qa.d_ipl ); } if( activeArgs.empty() ){ return body; @@ -1304,14 +1352,14 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i std::vector< Node > children; children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) ); children.push_back( body ); - if( !ipl.isNull() ){ - children.push_back( ipl ); + if( !qa.d_ipl.isNull() ){ + children.push_back( qa.d_ipl ); } return NodeManager::currentNM()->mkNode( kind::FORALL, children ); } } -Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){ +Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){ if( body.getKind()==FORALL ){ //combine arguments std::vector< Node > newArgs; @@ -1319,26 +1367,26 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, newArgs.push_back( body[0][i] ); } newArgs.insert( newArgs.end(), args.begin(), args.end() ); - return mkForAll( newArgs, body[ 1 ], ipl ); + return mkForAll( newArgs, body[ 1 ], qa ); }else{ if( body.getKind()==NOT ){ //push not downwards if( body[0].getKind()==NOT ){ - return computeMiniscoping( f, args, body[0][0], ipl ); + return computeMiniscoping( f, args, body[0][0], qa ); }else if( body[0].getKind()==AND ){ if( options::miniscopeQuantFreeVar() ){ NodeBuilder<> t(kind::OR); for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ t << ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() ); } - return computeMiniscoping( f, args, t.constructNode(), ipl ); + return computeMiniscoping( f, args, t.constructNode(), qa ); } }else if( body[0].getKind()==OR ){ if( options::miniscopeQuant() ){ NodeBuilder<> t(kind::AND); for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ Node trm = body[0][i].negate(); - t << computeMiniscoping( f, args, trm, ipl ); + t << computeMiniscoping( f, args, trm, qa ); } return t.constructNode(); } @@ -1348,7 +1396,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, //break apart NodeBuilder<> t(kind::AND); for( unsigned i=0; i<body.getNumChildren(); i++ ){ - t << computeMiniscoping( f, args, body[i], ipl ); + t << computeMiniscoping( f, args, body[i], qa ); } Node retVal = t; return retVal; @@ -1376,7 +1424,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, return body_split; }else if( body_split.getNumChildren()>0 ){ newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - body_split << mkForAll( args, newBody, ipl ); + body_split << mkForAll( args, newBody, qa ); return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split; } } @@ -1385,7 +1433,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, //if( body==f[1] ){ // return f; //}else{ - return mkForAll( args, body, ipl ); + return mkForAll( args, body, qa ); //} } @@ -1491,101 +1539,96 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg return n; } } - return mkForAll( args, body, Node::null() ); + QAttributes qa; + return mkForAll( args, body, qa ); } -bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){ +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 ){ - return true; + return is_std; }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ - return options::aggressiveMiniscopeQuant(); + return options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_NNF ){ - return options::nnfQuant(); + return true; }else if( computeOption==COMPUTE_PROCESS_TERMS ){ return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ - return options::iteDtTesterSplitQuant() || options::condVarSplitQuant(); + 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(); + 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; } } //general method for computing various rewrites -Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOption ){ - if( f.getKind()==FORALL ){ - Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl; - std::vector< Node > args; - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - args.push_back( f[0][i] ); - } - Node n = f[1]; - Node ipl; - if( f.getNumChildren()==3 ){ - ipl = f[2]; - } - if( computeOption==COMPUTE_ELIM_SYMBOLS ){ - n = computeElimSymbols( n ); - }else if( computeOption==COMPUTE_MINISCOPING ){ - //return directly - return computeMiniscoping( f, args, n, ipl ); - }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ - return computeAggressiveMiniscoping( args, n ); - }else if( computeOption==COMPUTE_NNF ){ - n = computeNNF( n ); - }else if( computeOption==COMPUTE_PROCESS_TERMS ){ - std::vector< Node > new_conds; - n = computeProcessTerms( n, args, new_conds, f ); - if( !new_conds.empty() ){ - new_conds.push_back( n ); - n = NodeManager::currentNM()->mkNode( OR, new_conds ); - } - }else if( computeOption==COMPUTE_COND_SPLIT ){ - n = computeCondSplit( n, ipl ); - }else if( computeOption==COMPUTE_PRENEX ){ - n = computePrenex( n, args, true ); - }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - n = computeVarElimination( n, args, ipl ); - //}else if( computeOption==COMPUTE_CNF ){ - //n = computeCNF( n, args, defs, false ); - //ipl = Node::null(); - }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ - std::vector< Node > conj; - computePurifyExpand( n, conj, args, ipl ); - if( !conj.empty() ){ - return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); - }else{ - return f; - } +Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){ + Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl; + std::vector< Node > args; + for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ + args.push_back( f[0][i] ); + } + Node n = f[1]; + if( computeOption==COMPUTE_ELIM_SYMBOLS ){ + n = computeElimSymbols( n ); + }else if( computeOption==COMPUTE_MINISCOPING ){ + //return directly + return computeMiniscoping( f, args, n, qa ); + }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ + return computeAggressiveMiniscoping( args, n ); + }else if( computeOption==COMPUTE_NNF ){ + n = computeNNF( n ); + }else if( computeOption==COMPUTE_PROCESS_TERMS ){ + std::vector< Node > new_conds; + n = computeProcessTerms( n, args, new_conds, f, qa ); + if( !new_conds.empty() ){ + new_conds.push_back( n ); + n = NodeManager::currentNM()->mkNode( OR, new_conds ); } - Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; - if( f[1]==n && args.size()==f[0].getNumChildren() ){ + }else if( computeOption==COMPUTE_COND_SPLIT ){ + n = computeCondSplit( n, qa ); + }else if( computeOption==COMPUTE_PRENEX ){ + n = computePrenex( n, args, true ); + }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ + n = computeVarElimination( n, args, qa ); + //}else if( computeOption==COMPUTE_CNF ){ + //n = computeCNF( n, args, defs, false ); + //ipl = Node::null(); + }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ + std::vector< Node > conj; + computePurifyExpand( n, conj, args, qa ); + if( !conj.empty() ){ + return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + }else{ return f; + } + } + Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; + if( f[1]==n && args.size()==f[0].getNumChildren() ){ + return f; + }else{ + if( args.empty() ){ + return n; }else{ - if( args.empty() ){ - return n; - }else{ - std::vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); - children.push_back( n ); - if( !ipl.isNull() ){ - children.push_back( ipl ); - } - return NodeManager::currentNM()->mkNode(kind::FORALL, children ); + std::vector< Node > children; + children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); + children.push_back( n ); + if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){ + children.push_back( qa.d_ipl ); } + return NodeManager::currentNM()->mkNode(kind::FORALL, children ); } - }else{ - return f; } } @@ -1754,31 +1797,29 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v //check if it contains a quantifier as a subterm //if so, we will write this node if( containsQuantifiers( n ) ){ - if( n.getType().isBoolean() ){ - if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ - if( options::preSkolemQuantAgg() ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); - } - return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); - } - }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) ); + if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){ + if( options::preSkolemQuantAgg() ){ + Node nn; + //must remove structure + if( n.getKind()==kind::ITE ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); + }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); + }else if( n.getKind()==kind::IMPLIES ){ + nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); + return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); } + }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ + vector< Node > children; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); } } } @@ -1786,15 +1827,20 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v } Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { + Node prev = n; if( options::preSkolemQuant() ){ if( !isInst || !options::preSkolemQuantNested() ){ - //apply pre-skolemization to existential quantifiers Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + //apply pre-skolemization to existential quantifiers std::vector< TypeNode > fvTypes; std::vector< TNode > fvs; - n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs ); + n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); } } + if( n!=prev ){ + Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl; + Trace("quantifiers-preprocess") << "..returned " << n << std::endl; + } return n; } @@ -1886,7 +1932,7 @@ Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, s } } -void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, Node ipl ) { +void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ) { if( body.getKind()==OR ){ Trace("quantifiers-rewrite-purify-exp") << "Purify expansion : " << body << std::endl; std::map< int, std::vector< Node > > disj; |