1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* Utilities for computing letification of proofs. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/proof_letify.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
namespace proof { |
20 |
|
|
21 |
|
bool ProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) |
22 |
|
{ |
23 |
|
return pn->getRule() != PfRule::SCOPE; |
24 |
|
} |
25 |
|
|
26 |
|
void ProofLetify::computeProofLet(const ProofNode* pn, |
27 |
|
std::vector<const ProofNode*>& pletList, |
28 |
|
std::map<const ProofNode*, size_t>& pletMap, |
29 |
|
size_t thresh, |
30 |
|
ProofLetifyTraverseCallback* pltc) |
31 |
|
{ |
32 |
|
Assert(pletList.empty() && pletMap.empty()); |
33 |
|
if (thresh == 0) |
34 |
|
{ |
35 |
|
// value of 0 means do not introduce let |
36 |
|
return; |
37 |
|
} |
38 |
|
std::vector<const ProofNode*> visitList; |
39 |
|
std::map<const ProofNode*, size_t> pcount; |
40 |
|
if (pltc == nullptr) |
41 |
|
{ |
42 |
|
// use default callback |
43 |
|
ProofLetifyTraverseCallback defaultPltc; |
44 |
|
computeProofCounts(pn, visitList, pcount, &defaultPltc); |
45 |
|
} |
46 |
|
else |
47 |
|
{ |
48 |
|
computeProofCounts(pn, visitList, pcount, pltc); |
49 |
|
} |
50 |
|
// Now populate the pletList and pletMap |
51 |
|
convertProofCountToLet(visitList, pcount, pletList, pletMap, thresh); |
52 |
|
} |
53 |
|
|
54 |
|
void ProofLetify::computeProofCounts(const ProofNode* pn, |
55 |
|
std::vector<const ProofNode*>& visitList, |
56 |
|
std::map<const ProofNode*, size_t>& pcount, |
57 |
|
ProofLetifyTraverseCallback* pltc) |
58 |
|
{ |
59 |
|
std::map<const ProofNode*, size_t>::iterator it; |
60 |
|
std::vector<const ProofNode*> visit; |
61 |
|
const ProofNode* cur; |
62 |
|
visit.push_back(pn); |
63 |
|
do |
64 |
|
{ |
65 |
|
cur = visit.back(); |
66 |
|
it = pcount.find(cur); |
67 |
|
if (it == pcount.end()) |
68 |
|
{ |
69 |
|
pcount[cur] = 0; |
70 |
|
if (!pltc->shouldTraverse(cur)) |
71 |
|
{ |
72 |
|
// callback indicated we should not traverse |
73 |
|
continue; |
74 |
|
} |
75 |
|
const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); |
76 |
|
for (const std::shared_ptr<ProofNode>& cp : pc) |
77 |
|
{ |
78 |
|
visit.push_back(cp.get()); |
79 |
|
} |
80 |
|
} |
81 |
|
else |
82 |
|
{ |
83 |
|
if (it->second == 0) |
84 |
|
{ |
85 |
|
visitList.push_back(cur); |
86 |
|
} |
87 |
|
pcount[cur]++; |
88 |
|
visit.pop_back(); |
89 |
|
} |
90 |
|
} while (!visit.empty()); |
91 |
|
} |
92 |
|
|
93 |
|
void ProofLetify::convertProofCountToLet( |
94 |
|
const std::vector<const ProofNode*>& visitList, |
95 |
|
const std::map<const ProofNode*, size_t>& pcount, |
96 |
|
std::vector<const ProofNode*>& pletList, |
97 |
|
std::map<const ProofNode*, size_t>& pletMap, |
98 |
|
size_t thresh) |
99 |
|
{ |
100 |
|
Assert(pletList.empty() && pletMap.empty()); |
101 |
|
if (thresh == 0) |
102 |
|
{ |
103 |
|
// value of 0 means do not introduce let |
104 |
|
return; |
105 |
|
} |
106 |
|
// Assign ids for those whose count is > 1, traverse in reverse order |
107 |
|
// so that deeper proofs are assigned lower identifiers |
108 |
|
std::map<const ProofNode*, size_t>::const_iterator itc; |
109 |
|
for (const ProofNode* pn : visitList) |
110 |
|
{ |
111 |
|
itc = pcount.find(pn); |
112 |
|
Assert(itc != pcount.end()); |
113 |
|
if (itc->second >= thresh && pn->getRule() != PfRule::ASSUME) |
114 |
|
{ |
115 |
|
pletList.push_back(pn); |
116 |
|
// start with id 1 |
117 |
|
size_t id = pletMap.size() + 1; |
118 |
|
pletMap[pn] = id; |
119 |
|
} |
120 |
|
} |
121 |
|
} |
122 |
|
|
123 |
|
} // namespace proof |
124 |
29280 |
} // namespace cvc5 |