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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
/********************* */
/*! \file proof.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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 Implementation of proof
**/
#include "expr/proof.h"
using namespace CVC4::kind;
namespace CVC4 {
CDProof::CDProof(ProofNodeManager* pnm, context::Context* c)
: d_manager(pnm), d_context(), d_nodes(c ? c : &d_context)
{
}
CDProof::~CDProof() {}
std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
{
NodeProofNodeMap::iterator it = d_nodes.find(fact);
if (it != d_nodes.end())
{
return (*it).second;
}
return nullptr;
}
bool CDProof::addStep(Node expected,
PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
bool ensureChildren,
bool forceOverwrite)
{
// we must provide expected
Assert(!expected.isNull());
NodeProofNodeMap::iterator it = d_nodes.find(expected);
if (it != d_nodes.end())
{
if (!forceOverwrite
&& ((*it).second->getId() != PfRule::ASSUME || id == PfRule::ASSUME))
{
// we do not overwrite if forceOverwrite is false and the previously
// provided step was not an assumption, or if the currently provided step
// is a (duplicate) assumption
return true;
}
// we will overwrite the existing proof node by updating its contents below
}
// collect the child proofs, for each premise
std::vector<std::shared_ptr<ProofNode>> pchildren;
for (const Node& c : children)
{
std::shared_ptr<ProofNode> pc = getProof(c);
if (pc == nullptr)
{
if (ensureChildren)
{
// failed to get a proof for a child, fail
return false;
}
// otherwise, we initialize it as an assumption
std::vector<Node> pcargs = {c};
std::vector<std::shared_ptr<ProofNode>> pcassume;
pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
// assumptions never fail to check
Assert(pc != nullptr);
d_nodes.insert(c, pc);
}
pchildren.push_back(pc);
}
// create or update it
std::shared_ptr<ProofNode> pthis;
if (it == d_nodes.end())
{
pthis = d_manager->mkNode(id, pchildren, args, expected);
if (pthis == nullptr)
{
// failed to construct the node, perhaps due to a proof checking failure
return false;
}
d_nodes.insert(expected, pthis);
}
else
{
// update its value
pthis = (*it).second;
d_manager->updateNode(pthis.get(), id, pchildren, args);
}
// the result of the proof node should be expected
Assert(pthis->getResult() == expected);
return true;
}
bool CDProof::addProof(ProofNode* pn, bool forceOverwrite)
{
std::unordered_map<ProofNode*, bool> visited;
std::unordered_map<ProofNode*, bool>::iterator it;
std::vector<ProofNode*> visit;
ProofNode* cur;
Node curFact;
visit.push_back(pn);
bool retValue = true;
do
{
cur = visit.back();
curFact = cur->getResult();
visit.pop_back();
it = visited.find(cur);
if (it == visited.end())
{
// visit the children
visited[cur] = false;
visit.push_back(cur);
const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
for (const std::shared_ptr<ProofNode>& c : cs)
{
visit.push_back(c.get());
}
}
else if (!it->second)
{
// we always call addStep, which may or may not overwrite the
// current step
std::vector<Node> pexp;
const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
for (const std::shared_ptr<ProofNode>& c : cs)
{
Assert(!c->getResult().isNull());
pexp.push_back(c->getResult());
}
// can ensure children at this point
bool res = addStep(curFact,
cur->getId(),
pexp,
cur->getArguments(),
true,
forceOverwrite);
// should always succeed
Assert(res);
retValue = retValue && res;
visited[cur] = true;
}
} while (!visit.empty());
return retValue;
}
} // namespace CVC4
|
