From d829ef207bf2c3551c99c528f1809bd096c6b10b Mon Sep 17 00:00:00 2001 From: Caleb Donovick Date: Tue, 10 Jul 2018 17:27:16 -0700 Subject: [PATCH] Move rewrite to pass (#2128) --- src/Makefile.am | 2 ++ src/preprocessing/passes/rewrite.cpp | 44 ++++++++++++++++++++++++++++ src/preprocessing/passes/rewrite.h | 44 ++++++++++++++++++++++++++++ src/smt/smt_engine.cpp | 14 ++++----- 4 files changed, 96 insertions(+), 8 deletions(-) create mode 100644 src/preprocessing/passes/rewrite.cpp create mode 100644 src/preprocessing/passes/rewrite.h diff --git a/src/Makefile.am b/src/Makefile.am index 71a66db59..d0621bf5b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -84,6 +84,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_to_bool.h \ preprocessing/passes/real_to_int.cpp \ preprocessing/passes/real_to_int.h \ + preprocessing/passes/rewrite.cpp \ + preprocessing/passes/rewrite.h \ preprocessing/passes/static_learning.cpp \ preprocessing/passes/static_learning.h \ preprocessing/passes/symmetry_breaker.cpp \ diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp new file mode 100644 index 000000000..dff807d58 --- /dev/null +++ b/src/preprocessing/passes/rewrite.cpp @@ -0,0 +1,44 @@ +/********************* */ +/*! \file rewrite.cpp + ** \verbatim + ** Top contributors (to current version): + ** Caleb Donovick + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The rewrite preprocessing pass + ** + ** Calls the rewriter on every assertion + **/ + +#include "preprocessing/passes/rewrite.h" + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + + +Rewrite::Rewrite(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "rewrite"){}; + + +PreprocessingPassResult Rewrite::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { + assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i])); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h new file mode 100644 index 000000000..1ab614fcd --- /dev/null +++ b/src/preprocessing/passes/rewrite.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file rewrite.h + ** \verbatim + ** Top contributors (to current version): + ** Caleb Donovick + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The rewrite preprocessing pass + ** + ** Calls the rewriter on every assertion + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__REWRITE_H +#define __CVC4__PREPROCESSING__PASSES__REWRITE_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class Rewrite : public PreprocessingPass +{ + public: + Rewrite(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__REWRITE_H */ + diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 22916e354..5d9f08343 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -78,6 +78,7 @@ #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/real_to_int.h" +#include "preprocessing/passes/rewrite.h" #include "preprocessing/passes/static_learning.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -2716,6 +2717,8 @@ void SmtEnginePrivate::finishInit() new PseudoBooleanProcessor(d_preprocessingPassContext.get())); std::unique_ptr realToInt( new RealToInt(d_preprocessingPassContext.get())); + std::unique_ptr rewrite( + new Rewrite(d_preprocessingPassContext.get())); std::unique_ptr staticLearning( new StaticLearning(d_preprocessingPassContext.get())); std::unique_ptr sbProc( @@ -2737,6 +2740,7 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", std::move(pbProc)); d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt)); + d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite)); d_preprocessingPassRegistry.registerPass("static-learning", std::move(staticLearning)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); @@ -4168,10 +4172,7 @@ void SmtEnginePrivate::processAssertions() { if(options::unconstrainedSimp()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; dumpAssertions("pre-unconstrained-simp", d_assertions); - Chat() << "...doing unconstrained simplification..." << endl; - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); - } + d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); unconstrainedSimp(); Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; dumpAssertions("post-unconstrained-simp", d_assertions); @@ -4189,10 +4190,7 @@ void SmtEnginePrivate::processAssertions() { { // special rewriting pass for unsat cores, since many of the passes below // are skipped - for (unsigned i = 0; i < d_assertions.size(); ++i) - { - d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); - } + d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); } else { -- 2.30.2