Fixes to theoryof-mode; no longer static in Theory class.

5 files changed, 21 insertions, 22 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6e09408d9..b2a0ba771 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -835,12 +835,9 @@ void SmtEngine::setLogicInternal() throw() {
   // Set the options for the theoryOf
   if(!options::theoryOfMode.wasSetByUser()) {
     if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
-      Theory::setTheoryOfMode(THEORY_OF_TERM_BASED);
-    } else {
-      Theory::setTheoryOfMode(THEORY_OF_TYPE_BASED);
+      Trace("smt") << "setting theoryof-mode to term-based" << endl;
+      options::theoryOfMode.set(THEORY_OF_TERM_BASED);
     }
-  } else {
-    Theory::setTheoryOfMode(options::theoryOfMode());
   }
 
   // by default, symmetry breaker is on only for QF_UF
diff --git a/src/theory/options b/src/theory/options
index 5d752fca1..9944264c8 100644
--- a/src/theory/options
+++ b/src/theory/options
@@ -5,8 +5,8 @@
 
 module THEORY "theory/options.h" Theory layer
 
-expert-option theoryOfMode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h"
- mode for theoryof
+expert-option theoryOfMode theoryof-mode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h" :read-write
+ mode for Theory::theoryof()
 
 option - use-theory --use-theory=NAME argument :handler CVC4::theory::useTheory :handler-include "theory/options_handlers.h"
  use alternate theory implementation NAME (--use-theory=help for a list)
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 3e30645e8..a1a835170 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -28,9 +28,6 @@ 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:
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 6b1974bb8..d1734674d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -26,6 +26,7 @@
 #include "theory/substitutions.h"
 #include "theory/output_channel.h"
 #include "theory/logic_info.h"
+#include "theory/options.h"
 #include "theory/theoryof_mode.h"
 #include "context/context.h"
 #include "context/cdlist.h"
@@ -298,9 +299,6 @@ protected:
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
-  /** Mode of the theoryOf operation */
-  static TheoryOfMode s_theoryOfMode;
-
 public:
 
   /**
@@ -333,12 +331,7 @@ public:
    * Returns the ID of the theory responsible for the given node.
    */
   static inline TheoryId theoryOf(TNode node) {
-    return theoryOf(s_theoryOfMode, node);
-  }
-
-  /** Set the theoryOf mode */
-  static void setTheoryOfMode(TheoryOfMode mode) {
-    s_theoryOfMode = mode;
+    return theoryOf(options::theoryOfMode(), node);
   }
 
   /**
@@ -349,7 +342,7 @@ public:
   }
 
   /**
-   * Set the owner of the uninterpreted sort.
+   * Get the owner of the uninterpreted sort.
    */
   static TheoryId getUninterpretedSortOwner() {
     return s_uninterpretedSortOwner;
diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h
index cd8c68b1a..c50960257 100644
--- a/src/theory/theoryof_mode.h
+++ b/src/theory/theoryof_mode.h
@@ -14,10 +14,10 @@
  ** Option selection for theoryOf() operation.
  **/
 
-#pragma once
-
 #include "cvc4_public.h"
 
+#pragma once
+
 namespace CVC4 {
 namespace theory {
 
@@ -29,6 +29,18 @@ enum TheoryOfMode {
   THEORY_OF_TERM_BASED
 };/* enum TheoryOfMode */
 
+inline std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC;
+
+inline std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() {
+  switch(m) {
+  case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED";
+  case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED";
+  default: return out << "TheoryOfMode!UNKNOWN";
+  }
+
+  Unreachable();
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */