rewriterules: fix a correction bug with --simplification=batch

  Rewriterules used ppAssert to obtain early the rewriterules in order
  to use them in ppRewrite. But all the simplifications (ex. f x = b :
  [f x/b]) are not done at that point. Since --simplification=batch
  remove the equality (unlike =incremental), for
  reachability_bbttf_eT_arrays.smt2 the answer was sat instead of
  unsat (thx Andy).

  Partial fix: don't take the rewriterules during ppAssert. That changes
  nothing since early rewrite was already disabled. But the complete
  fix (when early rewrite will be enabled again) will need to take the
  rewriterules more than once.

diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 6bf4ca22d6733bf010057643c5b51db5dfaef3de..b08b770d210ee7aaca83d619d73e7fa632fedfee 100644 (file)
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -592,8 +592,15 @@ void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){
 }
 
 Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  addRewriteRule(in);
-  d_ppAssert_on = true;
+  //TODO: here add only to the rewriterules database for ppRewrite,
+  //and not for the general one. Otherwise rewriting that occur latter
+  //on this rewriterules will be lost. But if the rewriting of the
+  //body is not done in "in", will it be done latter after
+  //substitution? Perhaps we should add the rewriterules to the
+  //database for ppRewrite also after the subtitution at the levvel of check
+
+  // addRewriteRule(in);
+  // d_ppAssert_on = true;
   return PP_ASSERT_STATUS_UNSOLVED;
 }