1 /********************* */
2 /*! \file bv_eager_atoms.cpp
4 ** Top contributors (to current version):
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
12 ** \brief Wrap assertions in BITVECTOR_EAGER_ATOM nodes.
14 ** This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes
15 ** and allows to use eager bit-blasting in the BV solver.
19 #include "preprocessing/passes/bv_eager_atoms.h"
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"
27 namespace preprocessing
{
30 BvEagerAtoms::BvEagerAtoms(PreprocessingPassContext
* preprocContext
)
31 : PreprocessingPass(preprocContext
, "bv-eager-atoms"){};
33 PreprocessingPassResult
BvEagerAtoms::applyInternal(
34 AssertionPipeline
* assertionsToPreprocess
)
36 theory::TheoryModel
* tm
= d_preprocContext
->getTheoryEngine()->getModel();
37 NodeManager
* nm
= NodeManager::currentNM();
38 for (unsigned i
= 0, size
= assertionsToPreprocess
->size(); i
< size
; ++i
)
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
);
45 return PreprocessingPassResult::NO_CONFLICT
;
50 } // namespace preprocessing