Added ability to set a "cvc4-specific logic" in standards-compliant

SMT-LIBv1 and SMT-LIBv2 input:

    In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance:

    (benchmark actually_a_sat_benchmark_but_looks_like_uf
      :logic QF_UF
      :cvc4_logic { QF_SAT }
      [...]

    In SMT-LIBv2, you use a set-info; for instance:

    (set-logic QF_UF)
    (set-info :cvc4-logic "QF_SAT")
    [...]

    Right now, the only thing this does is disable the symmetry breaker for
    benchmarks like the above ones.

As part of this work, TheoryEngine::setLogic() was removed (the logic field there
wasn't actually used anywhere, its need disappeared when
Theory::setUninterpretedSortOwner() was provided).

Also, Theory::d_uninterpretedSortOwner got a name change to
Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory
class.  This represents a breakage of our separation goals for CVC4, since it
means that two SmtEngines cannot be created separately to solve a QF_AX and
QF_UF problem.  A bug report is pending.

4 files changed, 7 insertions, 14 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index ff2feb121..fa2eed861 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -27,7 +27,7 @@ namespace CVC4 {
 namespace theory {
 
 /** Default value for the uninterpreted sorts is the UF theory */
-TheoryId Theory::d_uninterpretedSortOwner = THEORY_UF;
+TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   switch(level){
diff --git a/src/theory/theory.h b/src/theory/theory.h
index cf986a1f2..fade1e3c7 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -208,7 +208,7 @@ protected:
   /**
    * The theory that owns the uninterpreted sort.
    */
-  static TheoryId d_uninterpretedSortOwner;
+  static TheoryId s_uninterpretedSortOwner;
 
 public:
 
@@ -216,6 +216,7 @@ public:
    * Return the ID of the theory responsible for the given type.
    */
   static inline TheoryId theoryOf(TypeNode typeNode) {
+    Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl;
     TheoryId id;
     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
       id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
@@ -223,7 +224,8 @@ public:
       id = kindToTheoryId(typeNode.getKind());
     }
     if (id == THEORY_BUILTIN) {
-      return d_uninterpretedSortOwner;
+      Trace("theory") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
+      return s_uninterpretedSortOwner;
     }
     return id;
   }
@@ -233,6 +235,7 @@ public:
    * Returns the ID of the theory responsible for the given node.
    */
   static inline TheoryId theoryOf(TNode node) {
+    Trace("theory") << "theoryOf(" << node << ")" << std::endl;
     // Constants, variables, 0-ary constructors
     if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
       return theoryOf(node.getType());
@@ -249,7 +252,7 @@ public:
    * Set the owner of the uninterpreted sort.
    */
   static void setUninterpretedSortOwner(TheoryId theory) {
-    d_uninterpretedSortOwner = theory;
+    s_uninterpretedSortOwner = theory;
   }
 
   /**
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c4a8dc591..3486d9075 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -52,7 +52,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_hasShutDown(false),
   d_incomplete(context, false),
   d_sharedAssertions(context),
-  d_logic(""),
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
   d_decisionRequests(context),
@@ -78,12 +77,6 @@ TheoryEngine::~TheoryEngine() {
   }
 }
 
-void TheoryEngine::setLogic(std::string logic) {
-  Assert(d_logic.empty());
-  // Set the logic
-  d_logic = logic;
-}
-
 void TheoryEngine::preRegister(TNode preprocessed) {
   if(Dump.isOn("missed-t-propagations")) {
     d_possiblePropagations.push_back(preprocessed);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index be1c3abaf..2c1c9a436 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -323,9 +323,6 @@ class TheoryEngine {
    */
   void assertSharedEqualities();
 
-  /** The logic of the problem */
-  std::string d_logic;
-
   /**
    * Literals that are propagated by the theory. Note that these are TNodes.
    * The theory can only propagate nodes that have an assigned literal in the