Bug 593 fix: if the type is finite, it is now considered for detecting theories of...

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 0e573ce62cae13366750e395f28b8172885c7a90..7ece4594d3a12f5d69ae6d4d0323d3b33acfef10 100644 (file)
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -50,13 +50,36 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
   d_theories = Theory::setInsert(parentTheoryId, d_theories);
 
   // Should we use the theory of the type
-  bool useType = current != parent && currentTheoryId != parentTheoryId;
+  bool useType = false;
+  TheoryId typeTheoryId = THEORY_LAST;
 
+  if (current != parent) {
+    if (currentTheoryId != parentTheoryId) {
+      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
+      TypeNode type = current.getType();
+      useType = true;
+      typeTheoryId = Theory::theoryOf(type);
+    } else {
+      TypeNode type = current.getType();
+      typeTheoryId = Theory::theoryOf(type);
+      if (typeTheoryId != currentTheoryId) {
+        if (options::finiteModelFind() && type.isSort()) {
+          // We're looking for finite models
+          useType = true;
+        } else {
+          Cardinality card = type.getCardinality();
+          if (card.isFinite()) {
+            useType = true;
+          }
+        }
+      }
+    }
+  }
+  
   // Get the theories that have already visited this node
   TNodeToTheorySetMap::iterator find = d_visited.find(current);
   if (find == d_visited.end()) {
     if (useType) {
-      TheoryId typeTheoryId = Theory::theoryOf(current.getType());
       d_theories = Theory::setInsert(typeTheoryId, d_theories);
     }
     return false;
@@ -93,8 +116,32 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 
   // Should we use the theory of the type
-  bool useType = current != parent && currentTheoryId != parentTheoryId;
+  bool useType = false;
+  TheoryId typeTheoryId = THEORY_LAST;
 
+  if (current != parent) {
+    if (currentTheoryId != parentTheoryId) {
+      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
+      TypeNode type = current.getType();
+      useType = true;
+      typeTheoryId = Theory::theoryOf(type);
+    } else {
+      TypeNode type = current.getType();
+      typeTheoryId = Theory::theoryOf(type);
+      if (typeTheoryId != currentTheoryId) {
+        if (options::finiteModelFind() && type.isSort()) {
+          // We're looking for finite models
+          useType = true;
+        } else {
+          Cardinality card = type.getCardinality();
+          if (card.isFinite()) {
+            useType = true;
+          }
+        }
+      }
+    }
+  }
+  
   Theory::Set visitedTheories = d_visited[current];
   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
@@ -112,7 +159,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
   }
   if (useType) {
-    TheoryId typeTheoryId  = Theory::theoryOf(current.getType());
     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
       d_visited[current] = visitedTheories;
@@ -165,6 +211,28 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
   bool useType = false;
   TheoryId typeTheoryId = THEORY_LAST;
 
+  if (current != parent) {
+    if (currentTheoryId != parentTheoryId) {
+      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
+      TypeNode type = current.getType();
+      useType = true;
+      typeTheoryId = Theory::theoryOf(type);
+    } else {
+      TypeNode type = current.getType();
+      typeTheoryId = Theory::theoryOf(type);
+      if (typeTheoryId != currentTheoryId) {
+        if (options::finiteModelFind() && type.isSort()) {
+          // We're looking for finite models
+          useType = true;
+        } else {
+          Cardinality card = type.getCardinality();
+          if (card.isFinite()) {
+            useType = true;
+          }
+        }
+      }
+    }
+  }
   if (current != parent) {
     if (currentTheoryId != parentTheoryId) {
       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers

diff --git a/test/regress/README b/test/regress/README
index 58cd2f2e7dce9004c6fbd5c9141de5c591c1a767..6fcdf16a313a13dc5cbae1d1c0024e8b2b5bb9ac 100644 (file)
--- a/test/regress/README
+++ b/test/regress/README
@@ -3,7 +3,7 @@ Regressions
 
 To insert a new regression, add the file to Subversion, for example:
 
-  svn add regress/regress0/testMyFunctionality.cvc
+  git add regress/regress0/testMyFunctionality.cvc
 
 Also add it to the relevant Makefile.am, here, in regress/regress0/Makefile.am.
 

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index ad4e8a6021aedf91b43e04667ae509de6b1211ec..68d0023676831767b8edfd68d689c8751d3396af 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -167,6 +167,7 @@ BUG_TESTS = \
        bug585.cvc \
        bug586.cvc \
        bug590.smt2 \
+       bug593.smt2 \
        bug595.cvc \
        bug596.cvc \
        bug596b.cvc

diff --git a/test/regress/regress0/bug593.smt2 b/test/regress/regress0/bug593.smt2
new file mode 100644 (file)
index 0000000..2c28bb4
--- /dev/null
+++ b/test/regress/regress0/bug593.smt2
@@ -0,0 +1,20 @@
+(set-logic QF_UFBV)
+(set-info :status unsat)
+
+(declare-sort A 0)
+
+(declare-fun f ((_ BitVec 1)) A)
+(declare-fun g (A) (_ BitVec 1))
+
+(declare-fun x () A)
+(declare-fun y () A)
+(declare-fun z () A)
+ 
+(assert (and
+ 
+(not (= (f (g x)) (f (g y))))
+(not (= (f (g x)) (f (g z))))
+(not (= (f (g y)) (f (g z))))))
+  
+(check-sat)
+