GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bv_eager_atoms.cpp Lines: 12 12 100.0 %
Date: 2021-03-23 Branches: 14 28 50.0 %

Line Exec Source
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-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 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
#include "preprocessing/passes/bv_eager_atoms.h"
19
20
#include "preprocessing/assertion_pipeline.h"
21
#include "preprocessing/preprocessing_pass_context.h"
22
#include "theory/theory_engine.h"
23
#include "theory/theory_model.h"
24
25
namespace CVC4 {
26
namespace preprocessing {
27
namespace passes {
28
29
8997
BvEagerAtoms::BvEagerAtoms(PreprocessingPassContext* preprocContext)
30
8997
    : PreprocessingPass(preprocContext, "bv-eager-atoms"){};
31
32
41
PreprocessingPassResult BvEagerAtoms::applyInternal(
33
    AssertionPipeline* assertionsToPreprocess)
34
{
35
41
  theory::TheoryModel* tm = d_preprocContext->getTheoryEngine()->getModel();
36
41
  NodeManager* nm = NodeManager::currentNM();
37
396
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
38
  {
39
710
    TNode atom = (*assertionsToPreprocess)[i];
40
710
    Node eager_atom = nm->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
41
355
    tm->addSubstitution(eager_atom, atom);
42
355
    assertionsToPreprocess->replace(i, eager_atom);
43
  }
44
41
  return PreprocessingPassResult::NO_CONFLICT;
45
}
46
47
48
}  // namespace passes
49
}  // namespace preprocessing
50
26685
}  // namespace CVC4