diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-10 15:53:51 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-10 15:53:51 +0100 |
commit | be316870ef337a435d65f46a26f40ef0eab97934 (patch) | |
tree | 24db24b777180ea71d0e9078b7bcf4eff05ae9dc /src/util | |
parent | 8a43f6c6aa01f9b27434caf1c5dd9ef6b2dcd963 (diff) |
Do not eliminate variables only occurring in patterns. Minor improvements to sort inference. Remove unused code.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/sort_inference.cpp | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 066ba6103..dbd1dcd16 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -171,7 +171,9 @@ bool SortInference::simplify( std::vector< Node >& assertions ){ for( unsigned i=0; i<assertions.size(); i++ ){ Node prev = assertions[i]; std::map< Node, Node > var_bound; + Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl; assertions[i] = simplify( assertions[i], var_bound ); + Trace("sort-inference-debug") << "Done." << std::endl; if( prev!=assertions[i] ){ assertions[i] = theory::Rewriter::rewrite( assertions[i] ); rewritten = true; @@ -512,6 +514,7 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ } Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ + Trace("sort-inference-debug2") << "Simplify " << n << std::endl; std::vector< Node > children; if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ //recreate based on types of variables @@ -519,6 +522,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ for( size_t i=0; i<n[0].getNumChildren(); i++ ){ TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() ); Node v = getNewSymbol( n[0][i], tn ); + Trace("sort-inference-debug2") << "Map variable " << n[0][i] << " to " << v << std::endl; new_children.push_back( v ); var_bound[ n[0][i] ] = v; } @@ -529,13 +533,17 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ children.push_back( n.getOperator() ); } + bool childChanged = false; for( size_t i=0; i<n.getNumChildren(); i++ ){ bool processChild = true; if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1; } if( processChild ){ - children.push_back( simplify( n[i], var_bound ) ); + Node nc = simplify( n[i], var_bound ); + Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl; + children.push_back( nc ); + childChanged = childChanged || nc!=n[i]; } } @@ -543,6 +551,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ //erase from variable bound for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl; var_bound.erase( n[0][i] ); } return NodeManager::currentNM()->mkNode( n.getKind(), children ); @@ -596,7 +605,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ if( n[i].isConst() ){ children[i+1] = getNewSymbol( n[i], tna ); }else{ - Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl; + Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl; Assert( false ); } } @@ -616,7 +625,11 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ //just return n, we will fix at higher scope return n; }else{ - return NodeManager::currentNM()->mkNode( n.getKind(), children ); + if( childChanged ){ + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } } } |