diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-03 09:31:36 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-03 09:31:36 -0600 |
commit | 1cec37904f1d770d7756d5661ff9b86fbca6d7ac (patch) | |
tree | a825b2e38b734fcf20d9176840478aea8d73138f /src/theory | |
parent | 413bd34cee7aad26b1138e4412b5ceb44ae74405 (diff) |
Fix corner case of empty domains in bounded fmf (#3690)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/rep_set.cpp | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 55cef5ea7..243846b33 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -350,6 +350,7 @@ int RepSetIterator::incrementAtIndex(int i) #ifdef DISABLE_EVAL_SKIP_MULTIPLE i = (int)d_index.size()-1; #endif + Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i << std::endl; //increment d_index if( i>=0){ Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; @@ -361,6 +362,7 @@ int RepSetIterator::incrementAtIndex(int i) } } if( i==-1 ){ + Trace("rsi-debug") << "increment failed" << std::endl; d_index.clear(); return -1; }else{ @@ -371,6 +373,8 @@ int RepSetIterator::incrementAtIndex(int i) } int RepSetIterator::do_reset_increment( int i, bool initial ) { + Trace("rsi-debug") << "RepSetIterator::do_reset_increment: " << i + << ", initial=" << initial << std::endl; for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){ bool emptyDomain = false; int ri_res = resetIndex( ii, initial ); @@ -385,10 +389,22 @@ int RepSetIterator::do_reset_increment( int i, bool initial ) { //force next iteration if currently an empty domain if (emptyDomain) { - Trace("rsi-debug") << "This is an empty domain, increment." << std::endl; - return increment(); + Trace("rsi-debug") << "This is an empty domain (index " << ii << ")." + << std::endl; + if (ii > 0) + { + // increment at the previous index + return incrementAtIndex(ii - 1); + } + else + { + // this is the first index, we are done + d_index.clear(); + return -1; + } } } + Trace("rsi-debug") << "Finished, return " << i << std::endl; return i; } |