GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bitblast/simple_bitblaster.cpp Lines: 61 70 87.1 %
Date: 2021-03-22 Branches: 100 270 37.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file simple_bitblaster.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 Bitblaster for simple BV solver.
13
 **
14
 **/
15
#include "theory/bv/bitblast/simple_bitblaster.h"
16
17
#include "theory/theory_model.h"
18
#include "theory/theory_state.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace bv {
23
24
10
BBSimple::BBSimple(TheoryState* s) : TBitblaster<Node>(), d_state(s) {}
25
26
120
void BBSimple::bbAtom(TNode node)
27
{
28
120
  node = node.getKind() == kind::NOT ? node[0] : node;
29
30
120
  if (hasBBAtom(node))
31
  {
32
    return;
33
  }
34
35
240
  Node normalized = Rewriter::rewrite(node);
36
  Node atom_bb =
37
120
      normalized.getKind() != kind::CONST_BOOLEAN
38
120
              && normalized.getKind() != kind::BITVECTOR_BITOF
39
240
          ? d_atomBBStrategies[normalized.getKind()](normalized, this)
40
360
          : normalized;
41
42
120
  storeBBAtom(node, Rewriter::rewrite(atom_bb));
43
}
44
45
120
void BBSimple::storeBBAtom(TNode atom, Node atom_bb)
46
{
47
120
  d_bbAtoms.emplace(atom, atom_bb);
48
120
}
49
50
124
void BBSimple::storeBBTerm(TNode node, const Bits& bits)
51
{
52
124
  d_termCache.emplace(node, bits);
53
124
}
54
55
1976
bool BBSimple::hasBBAtom(TNode lit) const
56
{
57
1976
  if (lit.getKind() == kind::NOT)
58
  {
59
    lit = lit[0];
60
  }
61
1976
  return d_bbAtoms.find(lit) != d_bbAtoms.end();
62
}
63
64
124
void BBSimple::makeVariable(TNode var, Bits& bits)
65
{
66
124
  Assert(bits.size() == 0);
67
988
  for (unsigned i = 0; i < utils::getSize(var); ++i)
68
  {
69
864
    bits.push_back(utils::mkBitOf(var, i));
70
  }
71
124
  d_variables.insert(var);
72
124
}
73
74
Node BBSimple::getBBAtom(TNode node) const { return node; }
75
76
370
void BBSimple::bbTerm(TNode node, Bits& bits)
77
{
78
370
  Assert(node.getType().isBitVector());
79
370
  if (hasBBTerm(node))
80
  {
81
246
    getBBTerm(node, bits);
82
246
    return;
83
  }
84
124
  d_termBBStrategies[node.getKind()](node, bits, this);
85
124
  Assert(bits.size() == utils::getSize(node));
86
124
  storeBBTerm(node, bits);
87
}
88
89
592
Node BBSimple::getStoredBBAtom(TNode node)
90
{
91
592
  bool negated = false;
92
592
  if (node.getKind() == kind::NOT)
93
  {
94
    node = node[0];
95
    negated = true;
96
  }
97
98
592
  Assert(hasBBAtom(node));
99
1184
  Node atom_bb = d_bbAtoms.at(node);
100
1184
  return negated ? atom_bb.negate() : atom_bb;
101
}
102
103
34
Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
104
{
105
34
  if (!hasBBTerm(a))
106
  {
107
    return utils::mkConst(utils::getSize(a), 0u);
108
  }
109
110
  bool assignment;
111
68
  Bits bits;
112
34
  getBBTerm(a, bits);
113
68
  Integer value(0);
114
68
  Integer one(1), zero(0);
115
257
  for (int i = bits.size() - 1; i >= 0; --i)
116
  {
117
446
    Integer bit;
118
223
    if (d_state->hasSatValue(bits[i], assignment))
119
    {
120
215
      bit = assignment ? one : zero;
121
    }
122
    else
123
    {
124
8
      bit = zero;
125
    }
126
223
    value = value * 2 + bit;
127
  }
128
34
  return utils::mkConst(bits.size(), value);
129
}
130
131
6
bool BBSimple::collectModelValues(TheoryModel* m,
132
                                  const std::set<Node>& relevantTerms)
133
{
134
294
  for (const auto& var : relevantTerms)
135
  {
136
288
    if (d_variables.find(var) == d_variables.end()) continue;
137
138
68
    Node const_value = getModelFromSatSolver(var, true);
139
34
    Assert(const_value.isNull() || const_value.isConst());
140
34
    if (!const_value.isNull())
141
    {
142
34
      if (!m->assertEquality(var, const_value, true))
143
      {
144
        return false;
145
      }
146
    }
147
  }
148
6
  return true;
149
}
150
151
bool BBSimple::isVariable(TNode node)
152
{
153
  return d_variables.find(node) != d_variables.end();
154
}
155
156
}  // namespace bv
157
}  // namespace theory
158
26676
}  // namespace CVC4