src/preprocessing/passes/theory_preprocess.cpp

   1 /*********************                                                        */
   2 /*! \file theory_preprocess.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-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 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 "theory/rewriter.h"
  20 #include "theory/theory_engine.h"
  21
  22 namespace CVC4 {
  23 namespace preprocessing {
  24 namespace passes {
  25
  26 using namespace CVC4::theory;
  27
  28 TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
  29     : PreprocessingPass(preprocContext, "theory-preprocess"){};
  30
  31 PreprocessingPassResult TheoryPreprocess::applyInternal(
  32     AssertionPipeline* assertionsToPreprocess)
  33 {
  34   TheoryEngine* te = d_preprocContext->getTheoryEngine();
  35   te->preprocessStart();
  36   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  37   {
  38     TNode a = (*assertionsToPreprocess)[i];
  39     Assert(Rewriter::rewrite(a) == a);
  40     assertionsToPreprocess->replace(i, te->preprocess(a));
  41     a = (*assertionsToPreprocess)[i];
  42     Assert(Rewriter::rewrite(a) == a);
  43   }
  44   return PreprocessingPassResult::NO_CONFLICT;
  45 }
  46
  47
  48 }  // namespace passes
  49 }  // namespace preprocessing
  50 }  // namespace CVC4