Disable nonclausal simplification for QF_SAT benchmarks by default.

(Can be overridden with --simplification=batch, for example.)

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 932d9be7885c242b518bba328e9e33f7c3306644..53a05a9a4d71e380fde6b78aa97d97d2fbdd4402 100644 (file)
--- 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 fee77df39283ad235932000db2511c7f43f711f7..4f28225af9956c372017ffdda3f35910c5ec2c9d 100644 (file)
--- 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 f9ab0b48026e173cdb5aba4275008755910acab7..175b7f228cacd9b3a21fb89df4da2018989b52a4 100644 (file)
--- 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 6b8054a139206075b7f3de7898ee0e7a74648d3e..cdcefa14fac6830675de2efc94d3014af8adb99a 100644 (file)
--- 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;