src/preprocessing/preprocessing_pass.cpp

   1 /*********************                                                        */
   2 /*! \file preprocessing_pass.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Justin Xu, Abdalrhman Mohamed, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The preprocessing pass super class
  13  **
  14  ** Preprocessing pass super class.
  15  **/
  16
  17 #include "preprocessing/preprocessing_pass.h"
  18
  19 #include "smt/dump.h"
  20 #include "smt/smt_statistics_registry.h"
  21 #include "printer/printer.h"
  22
  23 namespace CVC4 {
  24 namespace preprocessing {
  25
  26 PreprocessingPassResult PreprocessingPass::apply(
  27     AssertionPipeline* assertionsToPreprocess) {
  28   TimerStat::CodeTimer codeTimer(d_timer);
  29   Trace("preprocessing") << "PRE " << d_name << std::endl;
  30   Chat() << d_name << "..." << std::endl;
  31   dumpAssertions(("pre-" + d_name).c_str(), *assertionsToPreprocess);
  32   PreprocessingPassResult result = applyInternal(assertionsToPreprocess);
  33   dumpAssertions(("post-" + d_name).c_str(), *assertionsToPreprocess);
  34   Trace("preprocessing") << "POST " << d_name << std::endl;
  35   return result;
  36 }
  37
  38 void PreprocessingPass::dumpAssertions(const char* key,
  39                                        const AssertionPipeline& assertionList) {
  40   if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
  41   {
  42     // Push the simplified assertions to the dump output stream
  43     OutputManager& outMgr = d_preprocContext->getSmt()->getOutputManager();
  44     const Printer& printer = outMgr.getPrinter();
  45     std::ostream& out = outMgr.getDumpOut();
  46
  47     for (const auto& n : assertionList)
  48     {
  49       printer.toStreamCmdAssert(out, n);
  50     }
  51   }
  52 }
  53
  54 PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
  55                                      const std::string& name)
  56     : d_name(name), d_timer("preprocessing::" + name) {
  57   d_preprocContext = preprocContext;
  58   smtStatisticsRegistry()->registerStat(&d_timer);
  59 }
  60
  61 PreprocessingPass::~PreprocessingPass() {
  62   Assert(smt::smtEngineInScope());
  63   if (smtStatisticsRegistry() != nullptr) {
  64     smtStatisticsRegistry()->unregisterStat(&d_timer);
  65   }
  66 }
  67
  68 }  // namespace preprocessing
  69 }  // namespace CVC4