diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-19 16:40:23 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-19 16:40:23 -0600 |
| commit | 09a2f1a01f5cf807112bc31d5f79f5f73e026b03 (patch) | |
| tree | 6940cecef421b7ef41872d97901cb2509f92d82c /src/theory/uf/theory_uf.cpp | |
| parent | 1acbb378d1658d613f9dc9788b8424455f445fc8 (diff) | |
Add fair strategy for finite model finding multiple sorts --uf-ss-fair.
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 41935984f..0ee7a2bdd 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -72,7 +72,6 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { }/* mkAnd() */ void TheoryUF::check(Effort level) { - while (!done() && !d_conflict) { // Get all the assertions @@ -94,7 +93,7 @@ void TheoryUF::check(Effort level) { TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); - } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) { + } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { // do nothing } else { d_equalityEngine.assertPredicate(atom, polarity, fact); @@ -136,6 +135,7 @@ void TheoryUF::preRegisterTerm(TNode node) { d_functionsTerms.push_back(node); break; case kind::CARDINALITY_CONSTRAINT: + case kind::COMBINED_CARDINALITY_CONSTRAINT: //do nothing break; default: |