1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, 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 |
|
* Trust substitutions. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/trust_substitutions.h" |
17 |
|
|
18 |
|
#include "theory/rewriter.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace theory { |
22 |
|
|
23 |
33368 |
TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, |
24 |
|
ProofNodeManager* pnm, |
25 |
|
std::string name, |
26 |
|
PfRule trustId, |
27 |
33368 |
MethodId ids) |
28 |
|
: d_ctx(c), |
29 |
|
d_subs(c), |
30 |
|
d_tsubs(c), |
31 |
|
d_tspb(nullptr), |
32 |
|
d_subsPg(nullptr), |
33 |
|
d_applyPg(nullptr), |
34 |
|
d_helperPf(nullptr), |
35 |
|
d_name(name), |
36 |
|
d_trustId(trustId), |
37 |
|
d_ids(ids), |
38 |
33368 |
d_eqtIndex(c) |
39 |
|
{ |
40 |
33368 |
setProofNodeManager(pnm); |
41 |
33368 |
} |
42 |
|
|
43 |
37149 |
void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm) |
44 |
|
{ |
45 |
37149 |
if (pnm != nullptr) |
46 |
|
{ |
47 |
|
// should not set the proof node manager more than once |
48 |
7387 |
Assert(d_tspb == nullptr); |
49 |
7387 |
d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())), |
50 |
14774 |
d_subsPg.reset(new LazyCDProof( |
51 |
7387 |
pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg")); |
52 |
14774 |
d_applyPg.reset( |
53 |
7387 |
new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg")); |
54 |
7387 |
d_helperPf.reset(new CDProofSet<LazyCDProof>(pnm, d_ctx)); |
55 |
|
} |
56 |
37149 |
} |
57 |
|
|
58 |
61312 |
void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) |
59 |
|
{ |
60 |
122624 |
Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x |
61 |
61312 |
<< " -> " << t << std::endl; |
62 |
61312 |
d_subs.addSubstitution(x, t); |
63 |
61312 |
if (isProofEnabled()) |
64 |
|
{ |
65 |
24512 |
TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg); |
66 |
12256 |
d_tsubs.push_back(tnl); |
67 |
|
// add to lazy proof |
68 |
12256 |
d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId); |
69 |
|
} |
70 |
61312 |
} |
71 |
|
|
72 |
2366 |
void TrustSubstitutionMap::addSubstitution(TNode x, |
73 |
|
TNode t, |
74 |
|
PfRule id, |
75 |
|
const std::vector<Node>& children, |
76 |
|
const std::vector<Node>& args) |
77 |
|
{ |
78 |
2366 |
if (!isProofEnabled()) |
79 |
|
{ |
80 |
1437 |
addSubstitution(x, t, nullptr); |
81 |
1437 |
return; |
82 |
|
} |
83 |
929 |
LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx); |
84 |
1858 |
Node eq = x.eqNode(t); |
85 |
929 |
stepPg->addStep(eq, id, children, args); |
86 |
929 |
addSubstitution(x, t, stepPg); |
87 |
|
} |
88 |
|
|
89 |
53800 |
ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, |
90 |
|
TNode t, |
91 |
|
TrustNode tn) |
92 |
|
{ |
93 |
107600 |
Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add " |
94 |
107600 |
<< x << " -> " << t << " from " << tn.getProven() |
95 |
53800 |
<< std::endl; |
96 |
53800 |
if (!isProofEnabled() || tn.getGenerator() == nullptr) |
97 |
|
{ |
98 |
|
// no generator or not proof enabled, nothing to do |
99 |
47306 |
addSubstitution(x, t, nullptr); |
100 |
47306 |
Trace("trust-subs") << "...no proof" << std::endl; |
101 |
47306 |
return nullptr; |
102 |
|
} |
103 |
12988 |
Node eq = x.eqNode(t); |
104 |
12988 |
Node proven = tn.getProven(); |
105 |
|
// notice that this checks syntactic equality, not CDProof::isSame since |
106 |
|
// tn.getGenerator() is not necessarily robust to symmetry. |
107 |
6494 |
if (eq == proven) |
108 |
|
{ |
109 |
|
// no rewrite required, just use the generator |
110 |
5331 |
addSubstitution(x, t, tn.getGenerator()); |
111 |
5331 |
Trace("trust-subs") << "...use generator directly" << std::endl; |
112 |
5331 |
return tn.getGenerator(); |
113 |
|
} |
114 |
1163 |
LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx); |
115 |
|
// Try to transform tn.getProven() to (= x t) here, if necessary |
116 |
1163 |
if (!d_tspb->applyPredTransform(proven, eq, {})) |
117 |
|
{ |
118 |
|
// failed to rewrite, we add a trust step which assumes eq is provable |
119 |
|
// from proven, and proceed as normal. |
120 |
13 |
Trace("trust-subs") << "...failed to rewrite " << proven << std::endl; |
121 |
13 |
d_tspb->addStep(PfRule::TRUST_SUBS_EQ, {proven}, {eq}, eq); |
122 |
|
} |
123 |
1163 |
Trace("trust-subs") << "...successful rewrite" << std::endl; |
124 |
1163 |
solvePg->addSteps(*d_tspb.get()); |
125 |
1163 |
d_tspb->clear(); |
126 |
|
// link the given generator |
127 |
1163 |
solvePg->addLazyStep(proven, tn.getGenerator()); |
128 |
1163 |
addSubstitution(x, t, solvePg); |
129 |
1163 |
return solvePg; |
130 |
|
} |
131 |
|
|
132 |
9933 |
void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t) |
133 |
|
{ |
134 |
9933 |
if (!isProofEnabled()) |
135 |
|
{ |
136 |
|
// just use the basic utility |
137 |
8196 |
d_subs.addSubstitutions(t.get()); |
138 |
8196 |
return; |
139 |
|
} |
140 |
|
// call addSubstitution above in sequence |
141 |
6417 |
for (const TrustNode& tns : t.d_tsubs) |
142 |
|
{ |
143 |
9360 |
Node proven = tns.getProven(); |
144 |
4680 |
addSubstitution(proven[0], proven[1], tns.getGenerator()); |
145 |
|
} |
146 |
|
} |
147 |
|
|
148 |
724711 |
TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite) |
149 |
|
{ |
150 |
1449422 |
Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n |
151 |
724711 |
<< std::endl; |
152 |
1449422 |
Node ns = d_subs.apply(n, doRewrite); |
153 |
724709 |
Trace("trust-subs") << "...subs " << ns << std::endl; |
154 |
724709 |
if (n == ns) |
155 |
|
{ |
156 |
|
// no change |
157 |
607962 |
return TrustNode::null(); |
158 |
|
} |
159 |
116747 |
if (!isProofEnabled()) |
160 |
|
{ |
161 |
|
// no proofs, use null generator |
162 |
72557 |
return TrustNode::mkTrustRewrite(n, ns, nullptr); |
163 |
|
} |
164 |
88380 |
Node eq = n.eqNode(ns); |
165 |
|
// remember the index |
166 |
44190 |
d_eqtIndex[eq] = d_tsubs.size(); |
167 |
|
// this class will provide a proof if asked |
168 |
44190 |
return TrustNode::mkTrustRewrite(n, ns, this); |
169 |
|
} |
170 |
|
|
171 |
311683 |
Node TrustSubstitutionMap::apply(Node n, bool doRewrite) |
172 |
|
{ |
173 |
311683 |
return d_subs.apply(n, doRewrite); |
174 |
|
} |
175 |
|
|
176 |
11869 |
std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq) |
177 |
|
{ |
178 |
11869 |
Assert(eq.getKind() == kind::EQUAL); |
179 |
23738 |
Node n = eq[0]; |
180 |
23738 |
Node ns = eq[1]; |
181 |
|
// Easy case: if n is in the domain of the substitution, maybe it is already |
182 |
|
// a proof in the substitution proof generator. This is moreover required |
183 |
|
// to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution, |
184 |
|
// and we are asked to transform x, resulting in 5, we hence must provide |
185 |
|
// a proof of (= x 5) based on the substitution. However, it must be the |
186 |
|
// case that (= x 5) is a proven fact of the substitution generator. Hence |
187 |
|
// we avoid a proof that looks like: |
188 |
|
// ---------- from d_subsPg |
189 |
|
// (= x 5) |
190 |
|
// ---------- MACRO_SR_EQ_INTRO{x} |
191 |
|
// (= x 5) |
192 |
|
// by taking the premise proof directly. |
193 |
11869 |
if (d_subsPg->hasStep(eq) || d_subsPg->hasGenerator(eq)) |
194 |
|
{ |
195 |
78 |
return d_subsPg->getProofFor(eq); |
196 |
|
} |
197 |
11791 |
NodeUIntMap::iterator it = d_eqtIndex.find(eq); |
198 |
11791 |
Assert(it != d_eqtIndex.end()); |
199 |
23582 |
Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= " |
200 |
11791 |
<< it->second << std::endl; |
201 |
23582 |
Node cs = getSubstitution(it->second); |
202 |
11791 |
Assert(eq != cs); |
203 |
23582 |
std::vector<Node> pfChildren; |
204 |
11791 |
if (!cs.isConst()) |
205 |
|
{ |
206 |
|
// note we will get more proof reuse if we do not special case AND here. |
207 |
4295 |
if (cs.getKind() == kind::AND) |
208 |
|
{ |
209 |
663095 |
for (const Node& csc : cs) |
210 |
|
{ |
211 |
659170 |
pfChildren.push_back(csc); |
212 |
|
// connect substitution generator into apply generator |
213 |
659170 |
d_applyPg->addLazyStep(csc, d_subsPg.get()); |
214 |
|
} |
215 |
|
} |
216 |
|
else |
217 |
|
{ |
218 |
370 |
pfChildren.push_back(cs); |
219 |
|
// connect substitution generator into apply generator |
220 |
370 |
d_applyPg->addLazyStep(cs, d_subsPg.get()); |
221 |
|
} |
222 |
|
} |
223 |
11791 |
Trace("trust-subs-pf") << "...apply eq intro" << std::endl; |
224 |
|
// We use fixpoint as the substitution-apply identifier. Notice that it |
225 |
|
// suffices to use SBA_SEQUENTIAL here, but SBA_FIXPOINT is typically |
226 |
|
// more efficient. This is because for substitution of size n, sequential |
227 |
|
// substitution can either be implemented as n traversals of the term to |
228 |
|
// apply the substitution to, or a single traversal of the term, but n^2/2 |
229 |
|
// traversals of the range of the substitution to prepare a simultaneous |
230 |
|
// substitution. Both of these options are inefficient. |
231 |
11791 |
if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids, MethodId::SBA_FIXPOINT)) |
232 |
|
{ |
233 |
|
// if we fail for any reason, we must use a trusted step instead |
234 |
|
d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq); |
235 |
|
} |
236 |
11791 |
Trace("trust-subs-pf") << "...made steps" << std::endl; |
237 |
|
// ------- ------- from external proof generators |
238 |
|
// x1 = t1 ... xn = tn |
239 |
|
// ----------------------- AND_INTRO |
240 |
|
// ... |
241 |
|
// --------- MACRO_SR_EQ_INTRO (or TRUST_SUBS_MAP if we failed above) |
242 |
|
// n == ns |
243 |
|
// add it to the apply proof generator. |
244 |
|
// |
245 |
|
// Notice that we use a single child to MACRO_SR_EQ_INTRO here. This is an |
246 |
|
// optimization motivated by the fact that n may be large and reused many |
247 |
|
// time. For instance, if this class is being used to track substitutions |
248 |
|
// derived during non-clausal simplification during preprocessing, it is |
249 |
|
// a fixed (possibly) large substitution applied to many terms. Having |
250 |
|
// a single child saves us from creating many proofs with n children, where |
251 |
|
// notice this proof is reused. |
252 |
11791 |
d_applyPg->addSteps(*d_tspb.get()); |
253 |
11791 |
d_tspb->clear(); |
254 |
11791 |
Trace("trust-subs-pf") << "...finish, make proof" << std::endl; |
255 |
11791 |
return d_applyPg->getProofFor(eq); |
256 |
|
} |
257 |
|
|
258 |
492 |
std::string TrustSubstitutionMap::identify() const { return d_name; } |
259 |
|
|
260 |
40646 |
SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; } |
261 |
|
|
262 |
244158 |
bool TrustSubstitutionMap::isProofEnabled() const |
263 |
|
{ |
264 |
244158 |
return d_subsPg != nullptr; |
265 |
|
} |
266 |
|
|
267 |
11791 |
Node TrustSubstitutionMap::getSubstitution(size_t index) |
268 |
|
{ |
269 |
11791 |
Assert(index <= d_tsubs.size()); |
270 |
23582 |
std::vector<Node> csubsChildren; |
271 |
671331 |
for (size_t i = 0; i < index; i++) |
272 |
|
{ |
273 |
659540 |
csubsChildren.push_back(d_tsubs[i].getProven()); |
274 |
|
} |
275 |
11791 |
std::reverse(csubsChildren.begin(), csubsChildren.end()); |
276 |
11791 |
Node cs = NodeManager::currentNM()->mkAnd(csubsChildren); |
277 |
11791 |
if (cs.getKind() == kind::AND) |
278 |
|
{ |
279 |
3925 |
d_subsPg->addStep(cs, PfRule::AND_INTRO, csubsChildren, {}); |
280 |
|
} |
281 |
23582 |
return cs; |
282 |
|
} |
283 |
|
|
284 |
|
} // namespace theory |
285 |
29502 |
} // namespace cvc5 |