From 5a20a19a30929ad58a9e64a9d8d1f877f3a07ae6 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 23 Feb 2012 23:08:03 +0000
Subject: 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.
---
 src/smt/smt_engine.cpp | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

(limited to 'src/smt/smt_engine.cpp')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f9539a1a4..12288e40a 100644
--- 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" ||
-- 
cgit v1.2.3