changing theoryOf in shared mode with arrays to move equalities to arrays

disabled in bitvectors due to non-stably infinite problems

the option to enable it is --theoryof-mode=term

8 files changed, 149 insertions, 22 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 19e7d588a..84af80035 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -18,6 +18,7 @@ libtheory_la_SOURCES = \
 	theory_test_utils.h \
 	theory.h \
 	theory.cpp \
+	theoryof_mode.h \
 	theory_registrar.h \
 	rewriter.h \
 	rewriter_attributes.h \
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9717f6286..041a5924a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1315,7 +1315,7 @@ void TheoryArrays::dischargeLemmas()
 }
 
 void TheoryArrays::conflict(TNode a, TNode b) {
-  if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+  if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b));
   } else {
     d_conflictNode = explain(a.eqNode(b));
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 8c20c84c1..a91243343 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -26,6 +26,10 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
+static TheoryId theoryOf(TNode node) {
+  return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
+}
+
 std::hash_set<Node, NodeHashFunction> d_rewriteStack;
 
 /**
@@ -61,7 +65,7 @@ struct RewriteStackElement {
 };
 
 Node Rewriter::rewrite(TNode node) {
-  return rewriteTo(theory::Theory::theoryOf(node), node);
+  return rewriteTo(theoryOf(node), node);
 }
 
 Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
@@ -102,7 +106,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
           RewriteResponse response = Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
           // Put the rewritten node to the top of the stack
           rewriteStackTop.node = response.node;
-          TheoryId newTheory = Theory::theoryOf(rewriteStackTop.node);
+          TheoryId newTheory = theoryOf(rewriteStackTop.node);
           // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
           if (newTheory == (TheoryId) rewriteStackTop.theoryId && response.status == REWRITE_DONE) {
             break;
@@ -116,7 +120,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
       else {
         // Continue with the cached version
         rewriteStackTop.node = cached;
-        rewriteStackTop.theoryId = Theory::theoryOf(cached);
+        rewriteStackTop.theoryId = theoryOf(cached);
       }
     }
 
@@ -145,7 +149,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
         // The child node
         Node childNode = rewriteStackTop.node[child];
         // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
-        rewriteStack.push_back(RewriteStackElement(childNode, Theory::theoryOf(childNode)));
+        rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
         // Go on with the rewriting
         continue;
       }
@@ -153,7 +157,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
       // Incorporate the children if necessary
       if (rewriteStackTop.node.getNumChildren() > 0) {
         rewriteStackTop.node = rewriteStackTop.builder;
-        rewriteStackTop.theoryId = Theory::theoryOf(rewriteStackTop.node);
+        rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node);
       }
 
       // Done with all pre-rewriting, so let's do the post rewrite
@@ -161,7 +165,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
         // Do the post-rewrite
         RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
         // We continue with the response we got
-        TheoryId newTheoryId = Theory::theoryOf(response.node);
+        TheoryId newTheoryId = theoryOf(response.node);
         if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) {
           // In the post rewrite if we've changed theories, we must do a full rewrite
           Assert(response.node != rewriteStackTop.node);
@@ -194,7 +198,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
     } else {
       // We were already in cache, so just remember it
       rewriteStackTop.node = cached;
-      rewriteStackTop.theoryId = Theory::theoryOf(cached);
+      rewriteStackTop.theoryId = theoryOf(cached);
     }
 
     // If this is the last node, just return
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 7555282d8..1dd0a1209 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -31,6 +31,9 @@ namespace theory {
 /** Default value for the uninterpreted sorts is the UF theory */
 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
 
+/** By default, we use the type based theoryOf */
+TheoryOfMode Theory::s_theoryOfMode = THEORY_OF_TYPE_BASED;
+
 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   switch(level){
   case Theory::EFFORT_STANDARD:
@@ -56,6 +59,78 @@ Theory::~Theory() {
   StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
 }
 
+TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
+
+  Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
+
+  switch(mode) {
+  case THEORY_OF_TYPE_BASED:
+    // Constants, variables, 0-ary constructors
+    if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
+      return theoryOf(node.getType());
+    }
+    // Equality is owned by the theory that owns the domain
+    if (node.getKind() == kind::EQUAL) {
+      return theoryOf(node[0].getType());
+    }
+    // Regular nodes are owned by the kind
+    return kindToTheoryId(node.getKind());
+    break;
+  case THEORY_OF_TERM_BASED:
+    // Variables
+    if (node.getMetaKind() == kind::metakind::VARIABLE) {      
+      if (theoryOf(node.getType()) != theory::THEORY_BOOL) {      
+        // We treat the varibables as uninterpreted
+        return s_uninterpretedSortOwner;
+      } else {
+        // Except for the Boolean ones, which we just ignore anyhow
+        return theory::THEORY_BOOL;
+      }
+    }    
+    // Constants
+    if (node.getMetaKind() == kind::metakind::CONSTANT) {
+      // Constants go to the theory of the type 
+      return theoryOf(node.getType());
+    }    
+    // Equality 
+    if (node.getKind() == kind::EQUAL) {
+      // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
+      if (node[0].getKind() == kind::ITE) {
+        return theoryOf(node[0].getType());
+      }
+      if (node[1].getKind() == kind::ITE) {
+        return theoryOf(node[1].getType());
+      }  
+      // If both sides belong to the same theory the choice is easy
+      TheoryId T1 = theoryOf(node[0]);
+      TheoryId T2 = theoryOf(node[1]);
+      if (T1 == T2) {
+        return T1;
+      }
+      TheoryId T3 = theoryOf(node[0].getType());
+      // This is a case of 
+      // * x*y = f(z) -> UF
+      // * x = c      -> UF
+      // * f(x) = read(a, y) -> either UF or ARRAY
+      // at least one of the theories has to be parametric, i.e. theory of the type is different
+      // from the theory of the term     
+      if (T1 == T3) {
+        return T2;
+      }
+      if (T2 == T3) {
+        return T1;
+      }
+      // If both are parametric, we take the smaller one (arbitraty)
+      return T1 < T2 ? T1 : T2;
+    }      
+    // Regular nodes are owned by the kind
+    return kindToTheoryId(node.getKind());  
+    break;    
+  default:
+    Unreachable();
+  }   
+}
+
 void Theory::addSharedTermInternal(TNode n) {
   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 8c830f8a2..217972dce 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -28,6 +28,7 @@
 #include "theory/substitutions.h"
 #include "theory/output_channel.h"
 #include "theory/logic_info.h"
+#include "theory/theoryof_mode.h"
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
@@ -122,6 +123,7 @@ typedef std::set<CarePair> CareGraph;
  * all calls to them.)
  */
 class Theory {
+
 private:
 
   friend class ::CVC4::TheoryEngine;
@@ -291,6 +293,9 @@ protected:
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
+  /** Mode of the theoryOf operation */
+  static TheoryOfMode s_theoryOfMode;
+
 public:
 
   /**
@@ -314,24 +319,23 @@ public:
     return id;
   }
 
+  /**
+   * Returns the ID of the theory responsible for the given node.
+   */
+  static TheoryId theoryOf(TheoryOfMode mode, TNode node);
 
   /**
    * Returns the ID of the theory responsible for the given node.
    */
   static inline TheoryId theoryOf(TNode node) {
-    Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
-    // Constants, variables, 0-ary constructors
-    if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
-      return theoryOf(node.getType());
-    }
-    // Equality is owned by the theory that owns the domain
-    if (node.getKind() == kind::EQUAL) {
-      return theoryOf(node[0].getType());
-    }
-    // Regular nodes are owned by the kind
-    return kindToTheoryId(node.getKind());
+    return theoryOf(s_theoryOfMode, node);
   }
-
+  
+  /** Set the theoryOf mode */
+  static void setTheoryOfMode(TheoryOfMode mode) {
+    s_theoryOfMode = mode;
+  }
+  
   /**
    * Set the owner of the uninterpreted sort.
    */
@@ -340,6 +344,13 @@ public:
   }
 
   /**
+   * Set the owner of the uninterpreted sort.
+   */
+  static TheoryId getUninterpretedSortOwner() {
+    return s_uninterpretedSortOwner;
+  }
+
+  /**
    * Checks if the node is a leaf node of this theory
    */
   inline bool isLeaf(TNode node) const {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 30b9cd098..0c0d65d74 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -904,7 +904,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
   // Try and assert (note that we assert the non-normalized one)
   if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
     // Check if has been pre-registered with the theory
-    bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAssertion) == toTheoryId;
+    bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId;
     // Assert away
     theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered);
     d_factsAsserted = true;
diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h
new file mode 100644
index 000000000..533704a39
--- /dev/null
+++ b/src/theory/theoryof_mode.h
@@ -0,0 +1,36 @@
+/*********************                                                        */
+/*! \file theory.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking, barrett
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Base of the theory interface.
+ **
+ ** Base of the theory interface.
+ **/
+
+#pragma once
+
+#include "cvc4_public.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** How do we associate theories with the terms */
+enum TheoryOfMode {
+  /** Equality, variables and constants are associated with the types */
+  THEORY_OF_TYPE_BASED,
+  /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */
+  THEORY_OF_TERM_BASED
+};
+
+}
+}
+
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index dc7bb7c92..5d36cd082 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -418,7 +418,7 @@ void TheoryUF::computeCareGraph() {
 }/* TheoryUF::computeCareGraph() */
 
 void TheoryUF::conflict(TNode a, TNode b) {
-  if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+  if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b));
   } else {
     d_conflictNode = explain(a.eqNode(b));