From 3eaa11b288348aeb71d3fad4f3719525c253fc91 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Fran=C3=A7ois=20Bobot?= Date: Tue, 21 Aug 2012 20:53:49 +0000 Subject: [PATCH] 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. --- src/theory/rewriterules/theory_rewriterules.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 6bf4ca22d..b08b770d2 100644 --- 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; } -- 2.30.2