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.

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1d4b7d3d154a2dee62f05ba6b3d13baa5734a63a..c647e128c06be578812f8653740c5c7dde5c0c63 100644 (file)
--- 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 e446b7d71b60ff8e8e918238f4c12e814463db4f..704e930b52901e3953e8ad5c0e91220d9471abe1 100644 (file)
--- 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";
   }

diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index e9bfde02402842e6b6f3df809a84d07e3b93d3b6..fa42e0b283a8004ede0059ce5503d817a6aaa3a2 100644 (file)
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -331,14 +331,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
       status = doCommand(smt, *subcmd, options) && status;
     }
   } else {
-    // by default, symmetry breaker is on only for QF_UF
-    if(! options.ufSymmetryBreakerSetByUser) {
-      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
-      if(logic != NULL) {
-        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
-      }
-    }
-
     if(options.verbosity > 0) {
       *options.out << "Invoking: " << *cmd << endl;
     }

diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 5c8f908f876e6f331b03d65b80adb02d391ea8bc..7b0c70a8a1f3deccaafb4e347d7ee548396367b0 100644 (file)
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -655,14 +655,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
       status = doCommand(smt, *subcmd, options) && status;
     }
   } else {
-    // by default, symmetry breaker is on only for QF_UF
-    if(! options.ufSymmetryBreakerSetByUser) {
-      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
-      if(logic != NULL) {
-        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
-      }
-    }
-
     if(options.verbosity > 0) {
       *options.out << "Invoking: " << *cmd << endl;
     }

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f9539a1a46474810c31b408cac039bb76abc59f0..12288e40aaf8f8d01b877db369b6194d2d5ee56f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -303,12 +303,22 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
     Dump("benchmark") << SetBenchmarkLogicCommand(s) << endl;
   }
 
+  setLogicInternal(s);
+}
+
+void SmtEngine::setLogicInternal(const std::string& s) throw() {
   d_logic = s;
-  d_theoryEngine->setLogic(s);
+
+  // by default, symmetry breaker is on only for QF_UF
+  if(! Options::current()->ufSymmetryBreakerSetByUser) {
+    NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF");
+  }
 
   // If in arrays, set the UF handler to arrays
   if(s == "QF_AX") {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
+  } else {
+    theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
   }
 }
 
@@ -318,6 +328,24 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SetInfoCommand(key, value) << endl;
   }
+
+  // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
+  if(key.length() > 6) {
+    string prefix = key.substr(0, 6);
+    if(prefix == ":cvc4-" || prefix == ":cvc4_") {
+      string cvc4key = key.substr(6);
+      if(cvc4key == "logic") {
+        if(! value.isAtom()) {
+          throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
+        }
+        d_logic = "";
+        setLogic(value.getValue());
+        return;
+      }
+    }
+  }
+
+  // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
   if(key == ":name" ||
      key == ":source" ||
      key == ":category" ||

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 52a98f41493cf7b982ba120470881008861e21ac..17717e44018a91ea80e8e0691376c570d2e7ac5b 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -206,6 +206,11 @@ class CVC4_PUBLIC SmtEngine {
 
   void internalPop();
 
+  /**
+   * Internally handle the setting of a logic.
+   */
+  void setLogicInternal(const std::string& logic) throw();
+
   friend class ::CVC4::smt::SmtEnginePrivate;
 
   // === STATISTICS ===

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index ff2feb12141919924e1ed4c86d401135aa77d1b2..fa2eed861b3ac5c01d8570df474dfd0971752548 100644 (file)
--- 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 cf986a1f266e144fa7fa511fb30d8fdb3fb731dc..fade1e3c777677026d976655d89c2ca3044a34aa 100644 (file)
--- 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 c4a8dc59119dc2599edcd10f35c6f84807f9e91b..3486d9075fee0fa71745fd74825770a3cd8946c9 100644 (file)
--- 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 be1c3abafd830358591844ed52c12a52e3487063..2c1c9a436788c818b0558e0276257fbef9e45c6e 100644 (file)
--- 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