diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 46 |
1 files changed, 28 insertions, 18 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index dcf58e692..8f055473d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -83,10 +83,10 @@ bool QuantifiersRewriter::isCube( Node n ){ } } -int QuantifiersRewriter::getPurifyId( Node n ){ +int QuantifiersRewriter::getPurifyId( Node n, std::vector< Node >& args ){ if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ return 1; - }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL ){ + }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::containsTerms( n, args ) ){ return 0; }else{ return -1; @@ -196,7 +196,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; - Trace("quantifiers-rewrite-debug") << "Attributes : " << std::endl; if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){ RewriteStatus status = REWRITE_DONE; Node ret = in; @@ -769,7 +768,7 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) { +bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) { if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ return false; }else{ @@ -777,7 +776,7 @@ bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::v std::map< Node, std::vector< int > >::iterator it = var_parent.find( v ); if( it!=var_parent.end() ){ Assert( !it->second.empty() ); - int id = getPurifyId( s ); + int id = getPurifyId( s, args ); return it->second.size()==1 && it->second[0]==id; } } @@ -791,7 +790,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto for( unsigned i=0; i<2; i++ ){ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] ); if( ita!=args.end() ){ - if( isVariableElim( lit[i], lit[1-i], var_parent ) ){ + if( isVariableElim( lit[i], lit[1-i], args, var_parent ) ){ + Trace("var-elim-quant") << "Variable eliminate based on equality : " << lit[i] << " -> " << lit[1-i] << std::endl; vars.push_back( lit[i] ); subs.push_back( lit[1-i] ); args.erase( ita ); @@ -809,7 +809,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto Node veq_c; Node val; int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); - if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){ + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, args, var_parent ) ){ + Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl; vars.push_back( itm->first ); subs.push_back( val ); args.erase( ita ); @@ -873,7 +874,7 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node > } } if( !vars.empty() ){ - Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl; + Trace("var-elim-quant-debug") << "VE " << vars.size() << "/" << args.size() << std::endl; //remake with eliminated nodes body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); body = Rewriter::rewrite( body ); @@ -1688,12 +1689,24 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, return it->second; }else{ Node ret = body; - if( body.getNumChildren()>0 && body.getKind()!=FORALL ){ + if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::containsTerms( ret, args ) ){ std::vector< Node > children; bool childrenChanged = false; - int id = getPurifyId( body ); + int id = getPurifyId( body, args ); for( unsigned i=0; i<body.getNumChildren(); i++ ){ - Node bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id ); + Node bi; + if( body.getKind()==EQUAL && i==1 ){ + int cid = getPurifyId( children[0], args ); + bi = computePurify2( body[i], args, visited, var_to_term, var_parent, cid ); + if( children[0].getKind()==BOUND_VARIABLE ){ + cid = getPurifyId( bi, args ); + if( cid!=0 && std::find( var_parent[children[0]].begin(), var_parent[children[0]].end(), cid )==var_parent[children[0]].end() ){ + var_parent[children[0]].push_back( id ); + } + } + }else{ + bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id ); + } childrenChanged = childrenChanged || bi!=body[i]; children.push_back( bi ); if( id!=0 && bi.getKind()==BOUND_VARIABLE ){ @@ -1709,13 +1722,10 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); } if( parentId!=0 && parentId!=id ){ - //must purify if this has a bound variable - if( TermDb::containsTerms( ret, args ) ){ - Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() ); - var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) ); - ret = v; - args.push_back( v ); - } + Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() ); + var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) ); + ret = v; + args.push_back( v ); } } visited[body] = ret; |