From f40ec39fe48f83e1cc1a31f9e18635687bd63c76 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 21 Mar 2012 20:51:02 +0000
Subject: [PATCH] Disable nonclausal simplification for QF_SAT benchmarks by
 default. (Can be overridden with --simplification=batch, for example.)

---
 src/parser/smt/Smt.g   | 11 +++++++++--
 src/smt/smt_engine.cpp |  6 ++++++
 src/util/options.cpp   |  4 ++++
 src/util/options.h     |  2 ++
 4 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 932d9be78..53a05a9a4 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -533,7 +533,14 @@ annotation[CVC4::Command*& smt_command]
 }
   : attribute[key]
     ( USER_VALUE
-      { smt_command = new SetInfoCommand(key, AntlrInput::tokenText($USER_VALUE)); }
+      { std::string value = AntlrInput::tokenText($USER_VALUE);
+        Assert(*value.begin() == '{');
+        Assert(*value.rbegin() == '}');
+        value.erase(value.begin(), value.begin() + 1);
+        value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
+        value.erase(value.end() - 1);
+        value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end());
+        smt_command = new SetInfoCommand(key, value); }
     )?
     { if(smt_command == NULL) {
         smt_command = new EmptyCommand(std::string("annotation: ") + key);
@@ -715,7 +722,7 @@ FLET_IDENTIFIER
  * with an open brace and end with closed brace.
  */
 USER_VALUE
-  : '{' ( '\\{' | '\\}' | ~('{' | '}') )* '}'
+  : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}'
   ;
 
 /**
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fee77df39..4f28225af 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -362,8 +362,14 @@ void SmtEngine::setLogicInternal(const std::string& s) throw() {
 
   // by default, symmetry breaker is on only for QF_UF
   if(! Options::current()->ufSymmetryBreakerSetByUser) {
+    Trace("smt") << "setting uf symmetry breaker to " << (s == "QF_UF") << std::endl;
     NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF");
   }
+  // by default, nonclausal simplification is off for QF_SAT
+  if(! Options::current()->simplificationModeSetByUser) {
+    Trace("smt") << "setting simplification mode to <" << s << "> " << (s != "QF_SAT") << std::endl;
+    NodeManager::currentNM()->getOptions()->simplificationMode = (s == "QF_SAT" ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
+  }
 
   // If in arrays, set the UF handler to arrays
   if(s == "QF_AX") {
diff --git a/src/util/options.cpp b/src/util/options.cpp
index f9ab0b480..175b7f228 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -78,6 +78,7 @@ Options::Options() :
   lazyDefinitionExpansion(false),
   printWinner(false),
   simplificationMode(SIMPLIFICATION_MODE_BATCH),
+  simplificationModeSetByUser(false),
   doStaticLearning(true),
   interactive(false),
   interactiveSetByUser(false),
@@ -674,10 +675,13 @@ throw(OptionException) {
     case SIMPLIFICATION_MODE:
       if(!strcmp(optarg, "batch")) {
         simplificationMode = SIMPLIFICATION_MODE_BATCH;
+        simplificationModeSetByUser = true;
       } else if(!strcmp(optarg, "incremental")) {
         simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL;
+        simplificationModeSetByUser = true;
       } else if(!strcmp(optarg, "none")) {
         simplificationMode = SIMPLIFICATION_MODE_NONE;
+        simplificationModeSetByUser = true;
       } else if(!strcmp(optarg, "help")) {
         puts(simplificationHelp.c_str());
         exit(1);
diff --git a/src/util/options.h b/src/util/options.h
index 6b8054a13..cdcefa14f 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -123,6 +123,8 @@ struct CVC4_PUBLIC Options {
 
   /** When/whether to perform nonclausal simplifications. */
   SimplificationMode simplificationMode;
+  /** Whether the user set the nonclausal simplification mode. */
+  bool simplificationModeSetByUser;
 
   /** Whether to perform the static learning pass. */
   bool doStaticLearning;
-- 
2.30.2