From 45af307478241b1fc8278406549d297f7f80fdb3 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 30 Aug 2018 15:49:45 -0700 Subject: [PATCH] Refactor theory preprocess into preprocessing pass. (#2395) --- src/Makefile.am | 2 + .../passes/theory_preprocess.cpp | 49 +++++++++++++++++++ src/preprocessing/passes/theory_preprocess.h | 43 ++++++++++++++++ src/smt/smt_engine.cpp | 46 +++++------------ 4 files changed, 105 insertions(+), 35 deletions(-) create mode 100644 src/preprocessing/passes/theory_preprocess.cpp create mode 100644 src/preprocessing/passes/theory_preprocess.h diff --git a/src/Makefile.am b/src/Makefile.am index 1a55d3810..5577b4b23 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -117,6 +117,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/symmetry_detect.h \ preprocessing/passes/synth_rew_rules.cpp \ preprocessing/passes/synth_rew_rules.h \ + preprocessing/passes/theory_preprocess.cpp \ + preprocessing/passes/theory_preprocess.h \ preprocessing/passes/unconstrained_simplifier.cpp \ preprocessing/passes/unconstrained_simplifier.h \ preprocessing/preprocessing_pass.cpp \ diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp new file mode 100644 index 000000000..edb0fc800 --- /dev/null +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -0,0 +1,49 @@ +/********************* */ +/*! \file bv_abstraction.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** 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 TheoryPreprocess preprocessing pass + ** + ** Calls Theory::preprocess(...) on every assertion of the formula. + **/ + +#include "preprocessing/passes/theory_preprocess.h" + +#include "theory/rewriter.h" +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "theory-preprocess"){}; + +PreprocessingPassResult TheoryPreprocess::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + TheoryEngine* te = d_preprocContext->getTheoryEngine(); + te->preprocessStart(); + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + TNode a = (*assertionsToPreprocess)[i]; + Assert(Rewriter::rewrite(a) == a); + assertionsToPreprocess->replace(i, te->preprocess(a)); + a = (*assertionsToPreprocess)[i]; + Assert(Rewriter::rewrite(a) == a); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h new file mode 100644 index 000000000..58eaee611 --- /dev/null +++ b/src/preprocessing/passes/theory_preprocess.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file theory_preprocess.h + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** 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 TheoryPreprocess preprocessing pass + ** + ** Calls Theory::preprocess(...) on every assertion of the formula. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H +#define __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class TheoryPreprocess : public PreprocessingPass +{ + public: + TheoryPreprocess(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2b388275a..914d781d4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -87,7 +87,6 @@ #include "preprocessing/passes/miplib_trick.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/quantifier_macros.h" -#include "preprocessing/passes/quantifier_macros.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" #include "preprocessing/passes/rewrite.h" @@ -98,6 +97,7 @@ #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/passes/synth_rew_rules.h" +#include "preprocessing/passes/theory_preprocess.h" #include "preprocessing/passes/unconstrained_simplifier.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -202,8 +202,6 @@ struct SmtEngineStatistics { TimerStat d_nonclausalSimplificationTime; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; - /** time spent in theory preprocessing */ - TimerStat d_theoryPreprocessTime; /** time spent converting to CNF */ TimerStat d_cnfConversionTime; /** Num of assertions before ite removal */ @@ -232,7 +230,6 @@ struct SmtEngineStatistics { d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), @@ -248,7 +245,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); smtStatisticsRegistry()->registerStat(&d_numAssertionsPre); smtStatisticsRegistry()->registerStat(&d_numAssertionsPost); @@ -266,7 +262,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime); smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre); smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost); @@ -2638,6 +2633,8 @@ void SmtEnginePrivate::finishInit() new SynthRewRulesPass(d_preprocessingPassContext.get())); std::unique_ptr sepSkolemEmp( new SepSkolemEmp(d_preprocessingPassContext.get())); + std::unique_ptr theoryPreprocess( + new TheoryPreprocess(d_preprocessingPassContext.get())); std::unique_ptr unconstrainedSimplifier( new UnconstrainedSimplifier(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("apply-substs", @@ -2684,6 +2681,8 @@ void SmtEnginePrivate::finishInit() std::move(sygusInfer)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); + d_preprocessingPassRegistry.registerPass("theory-preprocess", + std::move(theoryPreprocess)); d_preprocessingPassRegistry.registerPass("quantifier-macros", std::move(quantifierMacros)); d_preprocessingPassRegistry.registerPass("unconstrained-simplifier", @@ -3274,25 +3273,13 @@ bool SmtEnginePrivate::simplifyAssertions() // before ppRewrite check if only core theory for BV theory d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref()); - dumpAssertions("pre-theorypp", d_assertions); - // Theory preprocessing - if (d_smt.d_earlyTheoryPP) { - Chat() << "...doing early theory preprocessing..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); - // Call the theory preprocessors - d_smt.d_theoryEngine->preprocessStart(); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); - d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i])); - Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); - } + if (d_smt.d_earlyTheoryPP) + { + d_preprocessingPassRegistry.getPass("theory-preprocess") + ->apply(&d_assertions); } - dumpAssertions("post-theorypp", d_assertions); - Trace("smt") << "POST theoryPP" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - // ITE simplification if (options::doITESimp() && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) @@ -3821,19 +3808,8 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl; - dumpAssertions("pre-theory-preprocessing", d_assertions); - { - Chat() << "theory preprocessing..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); - // Call the theory preprocessors - d_smt.d_theoryEngine->preprocessStart(); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i])); - } - } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl; - dumpAssertions("post-theory-preprocessing", d_assertions); + d_preprocessingPassRegistry.getPass("theory-preprocess") + ->apply(&d_assertions); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { -- 2.30.2