diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-20 16:10:04 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-20 16:10:04 -0500 |
commit | 2e162eac469e010921250637760e9d23bdc5316a (patch) | |
tree | 0d138825bad2989ac0c6ced663d8eca499377a78 /src/theory/quantifiers | |
parent | fd33dbfa378f0a1be4d5fbde9aecb800715e4aa1 (diff) |
Minor fix for CBQI, ignore inst constant nodes.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index f60e01a7d..0353b0b5f 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -389,6 +389,14 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ }else{ Assert( index==(int)(childIndex.size())-1 ); unsigned nv = childIndex[index]+1; + if( options::cbqi() ){ + //skip inst constant nodes + while( nv<maxs[index] && nv<=max_i && + r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ + childIndex[index]++; + nv = childIndex[index]+1; + } + } if( nv<maxs[index] && nv<=max_i ){ childIndex[index]++; index++; |