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.

2 files changed, 13 insertions, 12 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1d4b7d3d1..c647e128c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -81,8 +81,7 @@ struct NVReclaim {
 
 NodeManager::NodeManager(context::Context* ctxt,
                          ExprManager* exprManager) :
-  d_optionsAllocated(new Options()),
-  d_options(d_optionsAllocated),
+  d_options(),
   d_statisticsRegistry(new StatisticsRegistry()),
   next_id(0),
   d_attrManager(ctxt),
@@ -96,8 +95,7 @@ NodeManager::NodeManager(context::Context* ctxt,
 NodeManager::NodeManager(context::Context* ctxt,
                          ExprManager* exprManager,
                          const Options& options) :
-  d_optionsAllocated(NULL),
-  d_options(&options),
+  d_options(options),
   d_statisticsRegistry(new StatisticsRegistry()),
   next_id(0),
   d_attrManager(ctxt),
@@ -155,7 +153,6 @@ NodeManager::~NodeManager() {
   }
 
   delete d_statisticsRegistry;
-  delete d_optionsAllocated;
 }
 
 void NodeManager::reclaimZombies() {
@@ -254,7 +251,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
   Debug("getType") << "getting type for " << n << std::endl;
 
-  if(needsCheck && !d_options->earlyTypeChecking) {
+  if(needsCheck && !d_options.earlyTypeChecking) {
     /* Iterate and compute the children bottom up. This avoids stack
        overflows in computeType() when the Node graph is really deep,
        which should only affect us when we're type checking lazily. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index e446b7d71..704e930b5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -82,8 +82,7 @@ class NodeManager {
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
-  const Options* d_optionsAllocated;
-  const Options* d_options;
+  Options d_options;
   StatisticsRegistry* d_statisticsRegistry;
 
   NodeValuePool d_nodeValuePool;
@@ -266,9 +265,14 @@ public:
   /** The node manager in the current public-facing CVC4 library context */
   static NodeManager* currentNM() { return s_current; }
 
-  /** Get this node manager's options */
+  /** Get this node manager's options (const version) */
   const Options* getOptions() const {
-    return d_options;
+    return &d_options;
+  }
+
+  /** Get this node manager's options (non-const version) */
+  Options* getOptions() {
+    return &d_options;
   }
 
   /** Get this node manager's statistics registry */
@@ -752,14 +756,14 @@ public:
     // Expr is destructed, there's no active node manager.
     //Assert(nm != NULL);
     NodeManager::s_current = nm;
-    Options::s_current = nm ? nm->d_options : NULL;
+    Options::s_current = nm ? &nm->d_options : NULL;
     Debug("current") << "node manager scope: "
                      << NodeManager::s_current << "\n";
   }
 
   ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
-    Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
+    Options::s_current = d_oldNodeManager ? &d_oldNodeManager->d_options : NULL;
     Debug("current") << "node manager scope: "
                      << "returning to " << NodeManager::s_current << "\n";
   }