diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:07 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:21 -0500 |
commit | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (patch) | |
tree | 409009a6ab55986308cc73d030db53489beef26d /src/theory/rep_set.cpp | |
parent | 3eaf02c01e74a2a43b2eff7638d6c16171a11a13 (diff) |
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 99e28714f..f2cb22b85 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -295,11 +295,18 @@ void RepSetIterator::increment2( int counter ){ d_index.clear(); }else{ d_index[counter]++; + bool emptyDomain = false; for( int i=(int)d_index.size()-1; i>counter; i-- ){ if (!resetIndex(i)){ break; + }else if( domainSize(i)<=0 ){ + emptyDomain = true; } } + if( emptyDomain ){ + Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl; + increment(); + } } } |