Added BitwiseEq bitvector rewrite

Added option "--repeat-simp" which repeats nonclausal simplification: 4 times,
twice before ite removal and twice after
Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant
speedup on dwp examples

2 files changed, 26 insertions, 0 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index a510f35f8..01b9648ff 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -85,6 +85,8 @@ Options::Options() :
   doStaticLearning(true),
   doITESimp(false),
   doITESimpSetByUser(false),
+  repeatSimp(false),
+  repeatSimpSetByUser(false),
   interactive(false),
   interactiveSetByUser(false),
   perCallResourceLimit(0),
@@ -187,6 +189,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\
+   --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\
    --replay-log=file      log decisions and propagations to file\n\
   SAT:\n\
@@ -426,6 +430,8 @@ enum OptionValue {
   NO_STATIC_LEARNING,
   ITE_SIMP,
   NO_ITE_SIMP,
+  REPEAT_SIMP,
+  NO_REPEAT_SIMP,
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_ASSIGNMENTS,
@@ -524,6 +530,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 },
+  { "repeat-simp", no_argument, NULL, REPEAT_SIMP },
+  { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, 'm' },
@@ -847,6 +855,16 @@ throw(OptionException) {
       doITESimpSetByUser = true;
       break;
 
+    case REPEAT_SIMP:
+      repeatSimp = true;
+      repeatSimpSetByUser = true;
+      break;
+
+    case NO_REPEAT_SIMP:
+      repeatSimp = false;
+      repeatSimpSetByUser = true;
+      break;
+
     case INTERACTIVE:
       interactive = true;
       interactiveSetByUser = true;
diff --git a/src/util/options.h b/src/util/options.h
index 9c36a471d..e6135dacb 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -154,6 +154,14 @@ struct CVC4_PUBLIC Options {
    */
   bool doITESimpSetByUser;
 
+  /** Whether to do multiple rounds of nonclausal simplification */
+  bool repeatSimp;
+
+  /**
+   * Whether the user explicitly requested multiple rounds of nonclausal simplification
+   */
+  bool repeatSimpSetByUser;
+
   /** Whether we're in interactive mode or not */
   bool interactive;