From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 20 Mar 2014 21:10:04 +0000 (-0500)
Subject: Minor fix for CBQI, ignore inst constant nodes.
X-Git-Tag: cvc5-1.0.0~7003
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e162eac469e010921250637760e9d23bdc5316a;p=cvc5.git

Minor fix for CBQI, ignore inst constant nodes.
---

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++;