Added preprocessing pass that propagates unconstrained values - solves all of

the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

2 files changed, 26 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;
diff --git a/src/util/options.h b/src/util/options.h
index e6135dacb..f48b45b49 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -154,6 +154,14 @@ struct CVC4_PUBLIC Options {
    */
   bool doITESimpSetByUser;
 
+  /** Whether to do the unconstrained simplification pass */
+  bool unconstrainedSimp;
+
+  /**
+   * Whether the user explicitly requested unconstrained simplification
+   */
+  bool unconstrainedSimpSetByUser;
+
   /** Whether to do multiple rounds of nonclausal simplification */
   bool repeatSimp;