diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
commit | 1c779966545190efa59b019572237562eea66dbf (patch) | |
tree | f827fe0e4bcbbca8c84174f815948b3212391423 /src/theory/quantifiers_engine.cpp | |
parent | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (diff) |
more minor updates to inst gen and representative selection, clean up of equality query
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ebd6d32ea..3f6ba8a0f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -719,6 +719,22 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& e } } +int getDepth( Node n ){ + if( n.getNumChildren()==0 ){ + return 0; + }else{ + int maxDepth = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + int depth = getDepth( n[i] ); + if( depth>maxDepth ){ + maxDepth = depth; + } + } + return maxDepth; + } +} + int EqualityQueryQuantifiersEngine::getRepScore( Node n ){ - return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; + return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; //initial + //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth } |