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

4 files changed, 64 insertions, 13 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 90d21c60d..0d3a220c9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -424,13 +424,22 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
   } else {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
   }
-  // Turn on ite simplification only for QF_LIA
+  // Turn on ite simplification for QF_LIA and QF_AUFBV
   if(! Options::current()->doITESimpSetByUser) {
-    bool iteSimp = logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() && !logic.isQuantified() && !logic.areRealsUsed();
+    bool iteSimp = !logic.isQuantified() &&
+      ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() &&  !logic.areRealsUsed()) ||
+       (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV)));
     Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
     NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
   }
-  // Turn on ite simplification only for pure arithmetic
+  // Turn on multiple-pass non-clausal simplification for QF_AUFBV
+  if(! Options::current()->repeatSimpSetByUser) {
+    bool repeatSimp = !logic.isQuantified() &&
+      (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV));
+    Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
+    NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
+  }
+  // Turn on arith rewrite equalities only for pure arithmetic
   if(! Options::current()->arithRewriteEqSetByUser) {
     bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified();
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
@@ -867,6 +876,14 @@ void SmtEnginePrivate::nonClausalSimplify() {
     d_nonClausalLearnedLiterals.resize(j);
   }
 
+  for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+    d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])));
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                      << "non-clausal preprocessed: "
+                      << d_assertionsToCheck.back() << endl;
+  }
+  d_assertionsToPreprocess.clear();
+
   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
     d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i])));
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -875,13 +892,6 @@ void SmtEnginePrivate::nonClausalSimplify() {
   }
   d_nonClausalLearnedLiterals.clear();
 
-  for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])));
-    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
-                      << "non-clausal preprocessed: "
-                      << d_assertionsToCheck.back() << endl;
-  }
-  d_assertionsToPreprocess.clear();
 }
 
 void SmtEnginePrivate::simpITE()
@@ -984,6 +994,11 @@ void SmtEnginePrivate::simplifyAssertions()
       simpITE();
     }
 
+    if(Options::current()->repeatSimp) {
+      d_assertionsToCheck.swap(d_assertionsToPreprocess);
+      nonClausalSimplify();
+    }
+
     if(Options::current()->doStaticLearning) {
       // Perform static learning
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
@@ -1100,6 +1115,12 @@ void SmtEnginePrivate::processAssertions() {
     // skipping for now --K
   }
 
+  if(Options::current()->repeatSimp) {
+    d_assertionsToCheck.swap(d_assertionsToPreprocess);
+    simplifyAssertions();
+    removeITEs();
+  }
+
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 #ifdef CVC4_ASSERTIONS
@@ -1112,6 +1133,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if(Dump.isOn("assertions")) {
     // Push the simplified assertions to the dump output stream
+    cout << "###Finished second removeITEs";
     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
       Dump("assertions")
         << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr()));
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 567f9dc46..d6de6edbd 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -516,17 +516,20 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
         RewriteRule<SimplifyEq>,
-        RewriteRule<ReflexivityEq>
+        RewriteRule<ReflexivityEq>,
+        RewriteRule<BitwiseEq>
         >::apply(node);
     return RewriteResponse(REWRITE_DONE, resultNode); 
   }
-
+  else if(RewriteRule<BitwiseEq>::applies(node)) {
+    Node resultNode = RewriteRule<BitwiseEq>::run<false>(node);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  }
   else {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
         RewriteRule<SimplifyEq>,
         RewriteRule<ReflexivityEq>,
-        //        ,RewriteRule<BitwiseEq>,
         RewriteRule<SolveEq>
         >::apply(node);
     return RewriteResponse(REWRITE_DONE, resultNode); 
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;