diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
commit | ada1fc44c9b5b8746a2e1e4046032282149768b5 (patch) | |
tree | efb350f7729004fedb4d7d872d5ff7e8d5d1fdc4 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 97470da31e14104f807fb33b2b3423e583e10726 (diff) |
Minor fixes and improvements to purify quant, relational triggers.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 8f055473d..1e2ac21a0 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, std::vector< Node >& args ){ +int QuantifiersRewriter::getPurifyId( Node n ){ if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ return 1; - }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::containsTerms( n, args ) ){ + }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::hasBoundVarAttr( n ) ){ return 0; }else{ return -1; @@ -768,7 +768,7 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) { +bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) { if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ return false; }else{ @@ -776,7 +776,7 @@ bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& a 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, args ); + int id = getPurifyId( s ); return it->second.size()==1 && it->second[0]==id; } } @@ -790,7 +790,7 @@ 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], args, var_parent ) ){ + if( isVariableElim( lit[i], lit[1-i], 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] ); @@ -809,7 +809,7 @@ 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, args, var_parent ) ){ + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, 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 ); @@ -1689,17 +1689,17 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, return it->second; }else{ Node ret = body; - if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::containsTerms( ret, args ) ){ + if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::hasBoundVarAttr( ret ) ){ std::vector< Node > children; bool childrenChanged = false; - int id = getPurifyId( body, args ); + int id = getPurifyId( body ); for( unsigned i=0; i<body.getNumChildren(); i++ ){ Node bi; if( body.getKind()==EQUAL && i==1 ){ - int cid = getPurifyId( children[0], args ); + int cid = getPurifyId( children[0] ); bi = computePurify2( body[i], args, visited, var_to_term, var_parent, cid ); if( children[0].getKind()==BOUND_VARIABLE ){ - cid = getPurifyId( bi, args ); + cid = getPurifyId( bi ); 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 ); } |