From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Fri, 7 Nov 2014 17:31:26 +0000 (-0500)
Subject: Bug 593 fix: if the type is finite, it is now considered for detecting theories of... 
X-Git-Tag: cvc5-1.0.0~6507
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9f3d26e4f34bfa0b03e05af6b827e7b72ea6ebd;p=cvc5.git

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

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 0e573ce62..7ece4594d 100644
--- 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 58cd2f2e7..6fcdf16a3 100644
--- 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 ad4e8a602..68d002367 100644
--- 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
index 000000000..2c28bb47c
--- /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)
+