Refactor theory preprocess into preprocessing pass. (#2395)

diff --git a/src/Makefile.am b/src/Makefile.am
index 1a55d38101a09f5b05f1e335a0404ddea501a680..5577b4b2329fbb15057d6dee5f2c6d78151b08ed 100644 (file)
--- 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 (file)
index 0000000..edb0fc8
--- /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 (file)
index 0000000..58eaee6
--- /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 2b388275a1f16849b43bd897328017b77e70cd29..914d781d4be38e24d4c285ba3cc6774e5f70cc49 100644 (file)
--- 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> sepSkolemEmp(
       new SepSkolemEmp(d_preprocessingPassContext.get()));
+  std::unique_ptr<TheoryPreprocess> theoryPreprocess(
+      new TheoryPreprocess(d_preprocessingPassContext.get()));
   std::unique_ptr<UnconstrainedSimplifier> 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)
   {