src/preprocessing/passes/rewrite.cpp

   1 /*********************                                                        */
   2 /*! \file rewrite.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Caleb Donovick
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 rewrite preprocessing pass
  13  **
  14  ** Calls the rewriter on every assertion
  15  **/
  16
  17 #include "preprocessing/passes/rewrite.h"
  18
  19 #include "preprocessing/assertion_pipeline.h"
  20 #include "theory/rewriter.h"
  21
  22 namespace CVC5 {
  23 namespace preprocessing {
  24 namespace passes {
  25
  26 using namespace CVC5::theory;
  27
  28 Rewrite::Rewrite(PreprocessingPassContext* preprocContext)
  29     : PreprocessingPass(preprocContext, "rewrite"){};
  30
  31
  32 PreprocessingPassResult Rewrite::applyInternal(
  33   AssertionPipeline* assertionsToPreprocess)
  34 {
  35   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) {
  36     assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i]));
  37   }
  38
  39   return PreprocessingPassResult::NO_CONFLICT;
  40 }
  41
  42
  43 }  // namespace passes
  44 }  // namespace preprocessing
  45 }  // namespace CVC5