src/preprocessing/passes/theory_preprocess.cpp

   1 /*********************                                                        */
   2 /*! \file bv_abstraction.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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 TheoryPreprocess preprocessing pass
  13  **
  14  ** Calls Theory::preprocess(...) on every assertion of the formula.
  15  **/
  16
  17 #include "preprocessing/passes/theory_preprocess.h"
  18
  19 #include "preprocessing/preprocessing_pass_registry.h"
  20 #include "theory/rewriter.h"
  21 #include "theory/theory_engine.h"
  22
  23 namespace CVC4 {
  24 namespace preprocessing {
  25 namespace passes {
  26
  27 using namespace CVC4::theory;
  28
  29 TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
  30     : PreprocessingPass(preprocContext, "theory-preprocess"){};
  31
  32 PreprocessingPassResult TheoryPreprocess::applyInternal(
  33     AssertionPipeline* assertionsToPreprocess)
  34 {
  35   TheoryEngine* te = d_preprocContext->getTheoryEngine();
  36   te->preprocessStart();
  37   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  38   {
  39     TNode a = (*assertionsToPreprocess)[i];
  40     Assert(Rewriter::rewrite(a) == a);
  41     assertionsToPreprocess->replace(i, te->preprocess(a));
  42     a = (*assertionsToPreprocess)[i];
  43     Assert(Rewriter::rewrite(a) == a);
  44   }
  45   return PreprocessingPassResult::NO_CONFLICT;
  46 }
  47
  48 static RegisterPass<TheoryPreprocess> X("theory-preprocess");
  49
  50 }  // namespace passes
  51 }  // namespace preprocessing
  52 }  // namespace CVC4