1 files changed, 18 insertions, 0 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 01b9648ff..e9ef7d959 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -85,6 +85,8 @@ Options::Options() :
   doStaticLearning(true),
   doITESimp(false),
   doITESimpSetByUser(false),
+  unconstrainedSimp(false),
+  unconstrainedSimpSetByUser(false),
   repeatSimp(false),
   repeatSimpSetByUser(false),
   interactive(false),
@@ -189,6 +191,8 @@ Additional CVC4 options:\n\
    --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
    --ite-simp             turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
    --no-ite-simp          turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
+   --unconstrained-simp   turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
+   --no-unconstrained-simp turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
    --repeat-simp          make multiple passes with nonclausal simplifier\n\
    --no-repeat-simp       do not make multiple passes with nonclausal simplifier\n\
    --replay=file          replay decisions from file\n\
@@ -430,6 +434,8 @@ enum OptionValue {
   NO_STATIC_LEARNING,
   ITE_SIMP,
   NO_ITE_SIMP,
+  UNCONSTRAINED_SIMP,
+  NO_UNCONSTRAINED_SIMP,
   REPEAT_SIMP,
   NO_REPEAT_SIMP,
   INTERACTIVE,
@@ -530,6 +536,8 @@ static struct option cmdlineOptions[] = {
   { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
   { "ite-simp", no_argument, NULL, ITE_SIMP },
   { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP },
+  { "unconstrained-simp", no_argument, NULL, UNCONSTRAINED_SIMP },
+  { "no-unconstrained-simp", no_argument, NULL, NO_UNCONSTRAINED_SIMP },
   { "repeat-simp", no_argument, NULL, REPEAT_SIMP },
   { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP },
   { "interactive", no_argument      , NULL, INTERACTIVE },
@@ -855,6 +863,16 @@ throw(OptionException) {
       doITESimpSetByUser = true;
       break;
 
+    case UNCONSTRAINED_SIMP:
+      unconstrainedSimp = true;
+      unconstrainedSimpSetByUser = true;
+      break;
+
+    case NO_UNCONSTRAINED_SIMP:
+      unconstrainedSimp = false;
+      unconstrainedSimpSetByUser = true;
+      break;
+
     case REPEAT_SIMP:
       repeatSimp = true;
       repeatSimpSetByUser = true;