GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_eager_solver.cpp Lines: 38 46 82.6 %
Date: 2021-03-23 Branches: 51 200 25.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_eager_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Liana Hadarean, Tim King
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 Eager bit-blasting solver.
13
 **
14
 ** Eager bit-blasting solver.
15
 **/
16
17
#include "theory/bv/bv_eager_solver.h"
18
19
#include "options/bv_options.h"
20
#include "options/smt_options.h"
21
#include "theory/bv/bitblast/aig_bitblaster.h"
22
#include "theory/bv/bitblast/eager_bitblaster.h"
23
24
using namespace std;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace bv {
29
30
31
EagerBitblastSolver::EagerBitblastSolver(context::Context* c, BVSolverLazy* bv)
31
    : d_assertionSet(c),
32
      d_assumptionSet(c),
33
      d_context(c),
34
      d_bitblaster(),
35
      d_aigBitblaster(),
36
31
      d_useAig(options::bitvectorAig()),
37
62
      d_bv(bv)
38
{
39
31
}
40
41
31
EagerBitblastSolver::~EagerBitblastSolver() {}
42
43
void EagerBitblastSolver::turnOffAig() {
44
  Assert(d_aigBitblaster == nullptr && d_bitblaster == nullptr);
45
  d_useAig = false;
46
}
47
48
29
void EagerBitblastSolver::initialize() {
49
29
  Assert(!isInitialized());
50
29
  if (d_useAig) {
51
#ifdef CVC4_USE_ABC
52
    d_aigBitblaster.reset(new AigBitblaster());
53
#else
54
    Unreachable();
55
#endif
56
  } else {
57
29
    d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
58
  }
59
29
}
60
61
2630
bool EagerBitblastSolver::isInitialized() {
62
2630
  const bool init = d_aigBitblaster != nullptr || d_bitblaster != nullptr;
63
2630
  Assert(!init || !d_useAig || d_aigBitblaster);
64
2630
  Assert(!init || d_useAig || d_bitblaster);
65
2630
  return init;
66
}
67
68
588
void EagerBitblastSolver::assertFormula(TNode formula) {
69
588
  d_bv->spendResource(ResourceManager::Resource::BvEagerAssertStep);
70
588
  Assert(isInitialized());
71
1176
  Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula " << formula
72
588
                           << "\n";
73
588
  if (options::incrementalSolving() && d_context->getLevel() > 1)
74
  {
75
24
    d_assumptionSet.insert(formula);
76
  }
77
588
  d_assertionSet.insert(formula);
78
  // ensures all atoms are bit-blasted and converted to AIG
79
588
  if (d_useAig) {
80
#ifdef CVC4_USE_ABC
81
    d_aigBitblaster->bbFormula(formula);
82
#else
83
    Unreachable();
84
#endif
85
  }
86
  else
87
  {
88
588
    d_bitblaster->bbFormula(formula);
89
  }
90
588
}
91
92
47
bool EagerBitblastSolver::checkSat() {
93
47
  Assert(isInitialized());
94
47
  if (d_assertionSet.empty()) {
95
    return true;
96
  }
97
98
47
  if (d_useAig) {
99
#ifdef CVC4_USE_ABC
100
    const std::vector<Node> assertions = {d_assertionSet.key_begin(),
101
                                          d_assertionSet.key_end()};
102
    Assert(!assertions.empty());
103
104
    Node query = utils::mkAnd(assertions);
105
    return d_aigBitblaster->solve(query);
106
#else
107
    Unreachable();
108
#endif
109
  }
110
111
47
  if (options::incrementalSolving())
112
  {
113
    const std::vector<Node> assumptions = {d_assumptionSet.key_begin(),
114
48
                                           d_assumptionSet.key_end()};
115
24
    return d_bitblaster->solve(assumptions);
116
  }
117
23
  return d_bitblaster->solve();
118
}
119
120
9
bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
121
{
122
9
  AlwaysAssert(!d_useAig && d_bitblaster);
123
9
  return d_bitblaster->collectModelInfo(m, fullModel);
124
}
125
126
}  // namespace bv
127
}  // namespace theory
128
26685
}  // namespace CVC4