diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-29 20:06:21 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-29 20:06:21 +0000 |
commit | 9062483193f4ec9b38aaa57b228cae1fb551566a (patch) | |
tree | 09f8ccefbd00ff5f63b12a501076e0e0aa4aac80 /src/theory | |
parent | 39af3d2f0391aba90a1941433dfd57e37218f3c2 (diff) |
fixing bug310
* theories that are parametric and therefore need the combination framwork should be tagged as "parametric" in the kinds file
* default care graph computation was not sufficient, fixed
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/kinds | 2 | ||||
-rw-r--r-- | src/theory/theory.cpp | 9 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 16 |
3 files changed, 15 insertions, 12 deletions
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index e90712129..7acb6d17d 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -7,7 +7,7 @@ theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h" typechecker "theory/datatypes/theory_datatypes_type_rules.h" -properties check presolve +properties check presolve parametric rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h" diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index fa2eed861..1998498f5 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -52,11 +52,12 @@ void Theory::addSharedTermInternal(TNode n) { } void Theory::computeCareGraph(CareGraph& careGraph) { - for (; d_sharedTermsIndex < d_sharedTerms.size(); d_sharedTermsIndex = d_sharedTermsIndex + 1) { - TNode a = d_sharedTerms[d_sharedTermsIndex]; + Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << std::endl; + for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { + TNode a = d_sharedTerms[i]; TypeNode aType = a.getType(); - for (unsigned i = 0; i < d_sharedTermsIndex; ++ i) { - TNode b = d_sharedTerms[i]; + for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) { + TNode b = d_sharedTerms[j]; if (b.getType() != aType) { // We don't care about the terms of different types continue; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0019b7b43..91d6beead 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -117,13 +117,13 @@ void TheoryEngine::check(Theory::Effort effort) { // Clear any leftover propagated equalities d_propagatedEqualities.clear(); - // Mark the lemmas flag (no lemmas added) - d_lemmasAdded = false; - // Mark the output channel unused (if this is FULL_EFFORT, and nothing // is done by the theories, no additional check will be needed) d_outputChannelUsed = false; + // Mark the lemmas flag (no lemmas added) + d_lemmasAdded = false; + while (true) { Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl; @@ -274,12 +274,14 @@ void TheoryEngine::combineTheories() { if (value) { SharedEquality sharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory); - Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()); - d_propagatedEqualities.push_back(sharedEquality); + if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) { + d_propagatedEqualities.push_back(sharedEquality); + } } else { SharedEquality sharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory); - Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()); - d_propagatedEqualities.push_back(sharedEquality); + if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) { + d_propagatedEqualities.push_back(sharedEquality); + } } } else { Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; |