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 |
|
* Term conversion sequence proof generator utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/tconv_seq_proof_generator.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "expr/proof_node_manager.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
|
24 |
3614 |
TConvSeqProofGenerator::TConvSeqProofGenerator( |
25 |
|
ProofNodeManager* pnm, |
26 |
|
const std::vector<ProofGenerator*>& ts, |
27 |
|
context::Context* c, |
28 |
3614 |
std::string name) |
29 |
3614 |
: d_pnm(pnm), d_converted(c), d_name(name) |
30 |
|
{ |
31 |
3614 |
d_tconvs.insert(d_tconvs.end(), ts.begin(), ts.end()); |
32 |
3614 |
AlwaysAssert(!d_tconvs.empty()) |
33 |
|
<< "TConvSeqProofGenerator::TConvSeqProofGenerator: expecting non-empty " |
34 |
|
"sequence"; |
35 |
3614 |
} |
36 |
|
|
37 |
7228 |
TConvSeqProofGenerator::~TConvSeqProofGenerator() {} |
38 |
|
|
39 |
6112 |
void TConvSeqProofGenerator::registerConvertedTerm(Node t, Node s, size_t index) |
40 |
|
{ |
41 |
6112 |
if (t == s) |
42 |
|
{ |
43 |
|
// no need |
44 |
|
return; |
45 |
|
} |
46 |
12224 |
std::pair<Node, size_t> key = std::pair<Node, size_t>(t, index); |
47 |
6112 |
d_converted[key] = s; |
48 |
|
} |
49 |
|
|
50 |
388 |
std::shared_ptr<ProofNode> TConvSeqProofGenerator::getProofFor(Node f) |
51 |
|
{ |
52 |
776 |
Trace("tconv-seq-pf-gen") |
53 |
776 |
<< "TConvSeqProofGenerator::getProofFor: " << identify() << ": " << f |
54 |
388 |
<< std::endl; |
55 |
388 |
return getSubsequenceProofFor(f, 0, d_tconvs.size() - 1); |
56 |
|
} |
57 |
|
|
58 |
388 |
std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor( |
59 |
|
Node f, size_t start, size_t end) |
60 |
|
{ |
61 |
388 |
Assert(end < d_tconvs.size()); |
62 |
388 |
if (f.getKind() != kind::EQUAL) |
63 |
|
{ |
64 |
|
std::stringstream serr; |
65 |
|
serr << "TConvSeqProofGenerator::getProofFor: " << identify() |
66 |
|
<< ": fail, non-equality " << f; |
67 |
|
Unhandled() << serr.str(); |
68 |
|
Trace("tconv-seq-pf-gen") << serr.str() << std::endl; |
69 |
|
return nullptr; |
70 |
|
} |
71 |
|
// start with the left hand side of the equality |
72 |
776 |
Node curr = f[0]; |
73 |
|
// proofs forming transitivity chain |
74 |
776 |
std::vector<std::shared_ptr<ProofNode>> transChildren; |
75 |
776 |
std::pair<Node, size_t> currKey; |
76 |
388 |
NodeIndexNodeMap::iterator itc; |
77 |
|
// convert the term in sequence |
78 |
1164 |
for (size_t i = start; i <= end; i++) |
79 |
|
{ |
80 |
776 |
currKey = std::pair<Node, size_t>(curr, i); |
81 |
776 |
itc = d_converted.find(currKey); |
82 |
|
// if we provided a conversion at this index via registerConvertedTerm |
83 |
776 |
if (itc != d_converted.end()) |
84 |
|
{ |
85 |
1552 |
Node next = (*itc).second; |
86 |
776 |
Trace("tconv-seq-pf-gen") << "...convert to " << next << std::endl; |
87 |
1552 |
Node eq = curr.eqNode(next); |
88 |
1552 |
std::shared_ptr<ProofNode> pf = d_tconvs[i]->getProofFor(eq); |
89 |
776 |
transChildren.push_back(pf); |
90 |
776 |
curr = next; |
91 |
|
} |
92 |
|
} |
93 |
|
// should end up with the right hand side of the equality |
94 |
388 |
if (curr != f[1]) |
95 |
|
{ |
96 |
|
// unexpected |
97 |
|
std::stringstream serr; |
98 |
|
serr << "TConvSeqProofGenerator::getProofFor: " << identify() |
99 |
|
<< ": failed, mismatch (see -t tconv-seq-pf-gen-debug for details)" |
100 |
|
<< std::endl; |
101 |
|
serr << " source: " << f[0] << std::endl; |
102 |
|
serr << "expected after conversions: " << f[1] << std::endl; |
103 |
|
serr << " actual after conversions: " << curr << std::endl; |
104 |
|
|
105 |
|
if (Trace.isOn("tconv-seq-pf-gen-debug")) |
106 |
|
{ |
107 |
|
Trace("tconv-pf-gen-debug") |
108 |
|
<< "Printing conversion steps..." << std::endl; |
109 |
|
serr << "Conversions: " << std::endl; |
110 |
|
for (NodeIndexNodeMap::const_iterator it = d_converted.begin(); |
111 |
|
it != d_converted.end(); |
112 |
|
++it) |
113 |
|
{ |
114 |
|
serr << "(" << (*it).first.first << ", " << (*it).first.second |
115 |
|
<< ") -> " << (*it).second << std::endl; |
116 |
|
} |
117 |
|
} |
118 |
|
Unhandled() << serr.str(); |
119 |
|
return nullptr; |
120 |
|
} |
121 |
|
// otherwise, make transitivity |
122 |
388 |
return d_pnm->mkTrans(transChildren, f); |
123 |
|
} |
124 |
|
|
125 |
75520 |
theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence( |
126 |
|
const std::vector<Node>& cterms) |
127 |
|
{ |
128 |
75520 |
Assert(cterms.size() == d_tconvs.size() + 1); |
129 |
75520 |
if (cterms[0] == cterms[cterms.size() - 1]) |
130 |
|
{ |
131 |
|
return theory::TrustNode::null(); |
132 |
|
} |
133 |
75520 |
bool useThis = false; |
134 |
75520 |
ProofGenerator* pg = nullptr; |
135 |
223504 |
for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++) |
136 |
|
{ |
137 |
151040 |
if (cterms[i] == cterms[i + 1]) |
138 |
|
{ |
139 |
72464 |
continue; |
140 |
|
} |
141 |
78576 |
else if (pg == nullptr) |
142 |
|
{ |
143 |
|
// Maybe the i^th generator can explain it alone, which must be the case |
144 |
|
// if there is only one position in the sequence where the term changes. |
145 |
|
// We may overwrite pg with this class if another step is encountered in |
146 |
|
// this loop. |
147 |
75520 |
pg = d_tconvs[i]; |
148 |
|
} |
149 |
|
else |
150 |
|
{ |
151 |
|
// need more than a single generator, use this class |
152 |
3056 |
useThis = true; |
153 |
3056 |
break; |
154 |
|
} |
155 |
|
} |
156 |
75520 |
if (useThis) |
157 |
|
{ |
158 |
3056 |
pg = this; |
159 |
|
// if more than two steps, we must register each conversion step |
160 |
9168 |
for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++) |
161 |
|
{ |
162 |
6112 |
registerConvertedTerm(cterms[i], cterms[i + 1], i); |
163 |
|
} |
164 |
|
} |
165 |
75520 |
Assert(pg != nullptr); |
166 |
|
return theory::TrustNode::mkTrustRewrite( |
167 |
75520 |
cterms[0], cterms[cterms.size() - 1], pg); |
168 |
|
} |
169 |
|
|
170 |
3670 |
std::string TConvSeqProofGenerator::identify() const { return d_name; } |
171 |
|
|
172 |
28194 |
} // namespace cvc5 |