diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-14 12:25:07 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-14 12:25:14 +0100 |
| commit | 83c0e6c14955e04b3dca56037508e4ceb6691f10 (patch) | |
| tree | 3e242ad90f0e34d03888e78267a4afe59e8a4ce3 /src/theory/quantifiers/term_database.cpp | |
| parent | f48855b3f7ebff4d6de916d6e433b3949afdbd1b (diff) | |
Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 9a4961e2c..4979a3dfd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -356,6 +356,7 @@ void TermDb::reset( Theory::Effort effort ){ TNode r = (*eqcs_i); bool addedFirst = false; Node first; + //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); |