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