src/preprocessing/passes/strings_eager_pp.cpp

   1 /*********************                                                        */
   2 /*! \file strings_eager_pp.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 strings eager preprocess utility
  13  **/
  14
  15 #include "preprocessing/passes/strings_eager_pp.h"
  16
  17 #include "theory/strings/theory_strings_preprocess.h"
  18 #include "theory/rewriter.h"
  19
  20 using namespace CVC4::theory;
  21
  22 namespace CVC4 {
  23 namespace preprocessing {
  24 namespace passes {
  25
  26 StringsEagerPp::StringsEagerPp(PreprocessingPassContext* preprocContext)
  27     : PreprocessingPass(preprocContext, "strings-eager-pp"){};
  28
  29 PreprocessingPassResult StringsEagerPp::applyInternal(
  30     AssertionPipeline* assertionsToPreprocess)
  31 {
  32   NodeManager* nm = NodeManager::currentNM();
  33   theory::strings::SkolemCache skc(false);
  34   theory::strings::StringsPreprocess pp(&skc);
  35   for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
  36        ++i)
  37   {
  38     Node prev = (*assertionsToPreprocess)[i];
  39     std::vector<Node> asserts;
  40     Node rew = pp.processAssertion(prev, asserts);
  41     if (!asserts.empty())
  42     {
  43       std::vector<Node> conj;
  44       conj.push_back(rew);
  45       conj.insert(conj.end(), asserts.begin(), asserts.end());
  46       rew = nm->mkAnd(conj);
  47     }
  48     if (prev != rew)
  49     {
  50       assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew));
  51     }
  52   }
  53
  54   return PreprocessingPassResult::NO_CONFLICT;
  55 }
  56
  57 }  // namespace passes
  58 }  // namespace preprocessing
  59 }  // namespace CVC4