1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of the lazy tree proof generator class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/lazy_tree_proof_generator.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
|
20 |
|
#include "expr/node.h" |
21 |
|
#include "expr/proof_generator.h" |
22 |
|
#include "expr/proof_node.h" |
23 |
|
#include "expr/proof_node_manager.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
|
28 |
1 |
LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm, |
29 |
1 |
const std::string& name) |
30 |
1 |
: d_pnm(pnm), d_name(name) |
31 |
|
{ |
32 |
1 |
d_stack.emplace_back(&d_proof); |
33 |
1 |
} |
34 |
11 |
void LazyTreeProofGenerator::openChild() |
35 |
|
{ |
36 |
11 |
detail::TreeProofNode& pn = getCurrent(); |
37 |
11 |
pn.d_children.emplace_back(); |
38 |
11 |
d_stack.emplace_back(&pn.d_children.back()); |
39 |
11 |
} |
40 |
12 |
void LazyTreeProofGenerator::closeChild() |
41 |
|
{ |
42 |
12 |
Assert(getCurrent().d_rule != PfRule::UNKNOWN); |
43 |
12 |
d_stack.pop_back(); |
44 |
12 |
} |
45 |
43 |
detail::TreeProofNode& LazyTreeProofGenerator::getCurrent() |
46 |
|
{ |
47 |
43 |
Assert(!d_stack.empty()) << "Proof construction has already been finished."; |
48 |
43 |
return *d_stack.back(); |
49 |
|
} |
50 |
12 |
void LazyTreeProofGenerator::setCurrent(PfRule rule, |
51 |
|
const std::vector<Node>& premise, |
52 |
|
std::vector<Node> args, |
53 |
|
Node proven) |
54 |
|
{ |
55 |
12 |
detail::TreeProofNode& pn = getCurrent(); |
56 |
12 |
pn.d_rule = rule; |
57 |
12 |
pn.d_premise = premise; |
58 |
12 |
pn.d_args = args; |
59 |
12 |
pn.d_proven = proven; |
60 |
12 |
} |
61 |
3 |
std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof() const |
62 |
|
{ |
63 |
|
// Check cache |
64 |
3 |
if (d_cached) return d_cached; |
65 |
1 |
Assert(d_stack.empty()) << "Proof construction has not yet been finished."; |
66 |
2 |
std::vector<std::shared_ptr<ProofNode>> scope; |
67 |
1 |
d_cached = getProof(scope, d_proof); |
68 |
1 |
return d_cached; |
69 |
|
} |
70 |
|
|
71 |
1 |
std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProofFor(Node f) |
72 |
|
{ |
73 |
1 |
Assert(hasProofFor(f)); |
74 |
1 |
return getProof(); |
75 |
|
} |
76 |
|
|
77 |
2 |
bool LazyTreeProofGenerator::hasProofFor(Node f) |
78 |
|
{ |
79 |
2 |
return f == getProof()->getResult(); |
80 |
|
} |
81 |
|
|
82 |
10 |
std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof( |
83 |
|
std::vector<std::shared_ptr<ProofNode>>& scope, |
84 |
|
const detail::TreeProofNode& pn) const |
85 |
|
{ |
86 |
|
// Store scope size to reset scope afterwards |
87 |
10 |
std::size_t before = scope.size(); |
88 |
20 |
std::vector<std::shared_ptr<ProofNode>> children; |
89 |
10 |
if (pn.d_rule == PfRule::SCOPE) |
90 |
|
{ |
91 |
|
// Extend scope for all but the root node |
92 |
5 |
if (&pn != &d_proof) |
93 |
|
{ |
94 |
8 |
for (const auto& a : pn.d_args) |
95 |
|
{ |
96 |
4 |
scope.emplace_back(d_pnm->mkAssume(a)); |
97 |
|
} |
98 |
|
} |
99 |
|
} |
100 |
|
else |
101 |
|
{ |
102 |
|
// Initialize the children with the scope |
103 |
5 |
children = scope; |
104 |
|
} |
105 |
19 |
for (auto& c : pn.d_children) |
106 |
|
{ |
107 |
|
// Recurse into tree |
108 |
9 |
children.emplace_back(getProof(scope, c)); |
109 |
|
} |
110 |
13 |
for (const auto& p : pn.d_premise) |
111 |
|
{ |
112 |
|
// Add premises as assumptions |
113 |
3 |
children.emplace_back(d_pnm->mkAssume(p)); |
114 |
|
} |
115 |
|
// Reset scope |
116 |
10 |
scope.resize(before); |
117 |
20 |
return d_pnm->mkNode(pn.d_rule, children, pn.d_args); |
118 |
|
} |
119 |
|
|
120 |
|
void LazyTreeProofGenerator::print(std::ostream& os, |
121 |
|
const std::string& prefix, |
122 |
|
const detail::TreeProofNode& pn) const |
123 |
|
{ |
124 |
|
os << prefix << pn.d_rule << ": "; |
125 |
|
container_to_stream(os, pn.d_premise); |
126 |
|
os << " ==> " << pn.d_proven << std::endl; |
127 |
|
if (!pn.d_args.empty()) |
128 |
|
{ |
129 |
|
os << prefix << ":args "; |
130 |
|
container_to_stream(os, pn.d_args); |
131 |
|
std::cout << std::endl; |
132 |
|
} |
133 |
|
for (const auto& c : pn.d_children) |
134 |
|
{ |
135 |
|
print(os, prefix + '\t', c); |
136 |
|
} |
137 |
|
} |
138 |
|
|
139 |
|
std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg) |
140 |
|
{ |
141 |
|
ltpg.print(os, "", ltpg.d_proof); |
142 |
|
return os; |
143 |
|
} |
144 |
|
|
145 |
|
} // namespace theory |
146 |
28194 |
} // namespace cvc5 |