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

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index e90712129795f2bdd42cd8d3466e2f723985c74a..7acb6d17dc38f906739f18bd20bcd04b54be0154 100644 (file)
--- 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 fa2eed861b3ac5c01d8570df474dfd0971752548..1998498f51141e77b35404b30cbdb8cbda2103db 100644 (file)
--- 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 0019b7b43c27829d81a7c9a7a1c581aed58a8521..91d6beead8abc3f7fc502fbfe7e9a6737dc7c6a8 100644 (file)
--- 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;

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 6947ea7c4e483ebf0fc3d06c4df6b890f7533341..1c4071c0079e396529997b3ab4136c256284dc05 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -95,7 +95,8 @@ BUG_TESTS = \
        bug220.smt2 \
        bug239.smt \
        buggy-ite.smt2 \
-       bug303.smt2
+       bug303.smt2 \
+       bug310.cvc
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/bug310.cvc b/test/regress/regress0/bug310.cvc
new file mode 100644 (file)
index 0000000..66e2369
--- /dev/null
+++ b/test/regress/regress0/bug310.cvc
@@ -0,0 +1,5 @@
+% EXPECT: valid
+% EXIT: 20
+b : BOOLEAN;
+DATATYPE D = c(s:INT) END;
+QUERY c(IF b THEN 1 ELSE 0 ENDIF) = IF b THEN c(1) ELSE c(0) ENDIF;