GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bitblast/proof_bitblaster.cpp Lines: 30 30 100.0 %
Date: 2021-03-22 Branches: 54 100 54.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_bitblaster.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, 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 A bit-blaster wrapper around BBSimple for proof logging.
13
 **/
14
#include "theory/bv/bitblast/proof_bitblaster.h"
15
16
#include <unordered_set>
17
18
#include "theory/theory_model.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace bv {
23
24
10
BBProof::BBProof(TheoryState* state) : d_bb(new BBSimple(state)) {}
25
26
120
void BBProof::bbAtom(TNode node)
27
{
28
240
  std::vector<TNode> visit;
29
120
  visit.push_back(node);
30
240
  std::unordered_set<TNode, TNodeHashFunction> visited;
31
1464
  while (!visit.empty())
32
  {
33
1160
    TNode n = visit.back();
34
856
    if (hasBBAtom(n) || hasBBTerm(n))
35
    {
36
184
      visit.pop_back();
37
184
      continue;
38
    }
39
40
488
    if (visited.find(n) == visited.end())
41
    {
42
244
      visited.insert(n);
43
244
      if (!Theory::isLeafOf(n, theory::THEORY_BV))
44
      {
45
154
        visit.insert(visit.end(), n.begin(), n.end());
46
      }
47
    }
48
    else
49
    {
50
244
      if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
51
      {
52
        // unused for now, will be needed for proof logging
53
124
        Bits bits;
54
62
        d_bb->makeVariable(n, bits);
55
      }
56
182
      else if (n.getType().isBitVector())
57
      {
58
124
        Bits bits;
59
62
        d_bb->bbTerm(n, bits);
60
      }
61
      else
62
      {
63
120
        d_bb->bbAtom(n);
64
      }
65
244
      visit.pop_back();
66
    }
67
  }
68
120
}
69
70
1264
bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
71
72
672
bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
73
74
592
Node BBProof::getStoredBBAtom(TNode node)
75
{
76
592
  return d_bb->getStoredBBAtom(node);
77
}
78
79
6
bool BBProof::collectModelValues(TheoryModel* m,
80
                                 const std::set<Node>& relevantTerms)
81
{
82
6
  return d_bb->collectModelValues(m, relevantTerms);
83
}
84
85
}  // namespace bv
86
}  // namespace theory
87
26676
}  // namespace CVC4