src/preprocessing/passes/bv_eager_atoms.cpp

   1 /*********************                                                        */
   2 /*! \file bv_eager_atoms.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 Wrap assertions in BITVECTOR_EAGER_ATOM nodes.
  13  **
  14  ** This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes
  15  ** and allows to use eager bit-blasting in the BV solver.
  16  **/
  17
  18
  19 #include "preprocessing/passes/bv_eager_atoms.h"
  20
  21 #include "preprocessing/assertion_pipeline.h"
  22 #include "preprocessing/preprocessing_pass_context.h"
  23 #include "theory/theory_engine.h"
  24 #include "theory/theory_model.h"
  25
  26 namespace CVC4 {
  27 namespace preprocessing {
  28 namespace passes {
  29
  30 BvEagerAtoms::BvEagerAtoms(PreprocessingPassContext* preprocContext)
  31     : PreprocessingPass(preprocContext, "bv-eager-atoms"){};
  32
  33 PreprocessingPassResult BvEagerAtoms::applyInternal(
  34     AssertionPipeline* assertionsToPreprocess)
  35 {
  36   theory::TheoryModel* tm = d_preprocContext->getTheoryEngine()->getModel();
  37   NodeManager* nm = NodeManager::currentNM();
  38   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  39   {
  40     TNode atom = (*assertionsToPreprocess)[i];
  41     Node eager_atom = nm->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
  42     tm->addSubstitution(eager_atom, atom);
  43     assertionsToPreprocess->replace(i, eager_atom);
  44   }
  45   return PreprocessingPassResult::NO_CONFLICT;
  46 }
  47
  48
  49 }  // namespace passes
  50 }  // namespace preprocessing
  51 }  // namespace CVC4