blob: a441e769e3286c55f0e87d405be4975e97a26d60 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
/********************* */
/*! \file proof_bitblaster.cpp
** \verbatim
** Top contributors (to current version):
** Aina Niemetz, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief A bit-blaster wrapper around BBSimple for proof logging.
**/
#include "theory/bv/bitblast/proof_bitblaster.h"
#include <unordered_set>
#include "theory/theory_model.h"
namespace cvc5 {
namespace theory {
namespace bv {
BBProof::BBProof(TheoryState* state) : d_bb(new BBSimple(state)) {}
void BBProof::bbAtom(TNode node)
{
std::vector<TNode> visit;
visit.push_back(node);
std::unordered_set<TNode, TNodeHashFunction> visited;
while (!visit.empty())
{
TNode n = visit.back();
if (hasBBAtom(n) || hasBBTerm(n))
{
visit.pop_back();
continue;
}
if (visited.find(n) == visited.end())
{
visited.insert(n);
if (!Theory::isLeafOf(n, theory::THEORY_BV))
{
visit.insert(visit.end(), n.begin(), n.end());
}
}
else
{
if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
{
// unused for now, will be needed for proof logging
Bits bits;
d_bb->makeVariable(n, bits);
}
else if (n.getType().isBitVector())
{
Bits bits;
d_bb->bbTerm(n, bits);
}
else
{
d_bb->bbAtom(n);
}
visit.pop_back();
}
}
}
bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
Node BBProof::getStoredBBAtom(TNode node)
{
return d_bb->getStoredBBAtom(node);
}
bool BBProof::collectModelValues(TheoryModel* m,
const std::set<Node>& relevantTerms)
{
return d_bb->collectModelValues(m, relevantTerms);
}
} // namespace bv
} // namespace theory
} // namespace cvc5
|
