Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Trust substitutions.
11 : : */
12 : :
13 : : #include "theory/trust_substitutions.h"
14 : :
15 : : #include "smt/env.h"
16 : : #include "theory/rewriter.h"
17 : :
18 : : namespace cvc5::internal {
19 : : namespace theory {
20 : :
21 : 127015 : TrustSubstitutionMap::TrustSubstitutionMap(Env& env,
22 : : context::Context* c,
23 : : std::string name,
24 : : TrustId trustId,
25 : 127015 : MethodId ids)
26 : : : EnvObj(env),
27 : 127015 : d_ctx(c),
28 : 127015 : d_subs(c),
29 : 127015 : d_tsubs(c),
30 : 127015 : d_tspb(nullptr),
31 : 127015 : d_subsPg(nullptr),
32 : 127015 : d_applyPg(nullptr),
33 : 127015 : d_helperPf(nullptr),
34 : 127015 : d_name(name),
35 : 127015 : d_trustId(trustId),
36 : 127015 : d_ids(ids),
37 : 254030 : d_eqtIndex(c)
38 : : {
39 : 127015 : ProofNodeManager* pnm = d_env.getProofNodeManager();
40 [ + + ]: 127015 : if (pnm != nullptr)
41 : : {
42 : 50096 : d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker()));
43 : 100192 : d_subsPg.reset(
44 : 50096 : new LazyCDProof(env, nullptr, d_ctx, "TrustSubstitutionMap::subsPg"));
45 : 100192 : d_applyPg.reset(
46 : 50096 : new LazyCDProof(env, nullptr, d_ctx, "TrustSubstitutionMap::applyPg"));
47 : 50096 : d_helperPf.reset(new CDProofSet<LazyCDProof>(env, d_ctx));
48 : : }
49 : 127015 : }
50 : :
51 : 110537 : void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
52 : : {
53 [ + - ]: 221074 : Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x
54 : 110537 : << " -> " << t << std::endl;
55 : 110537 : d_subs.addSubstitution(x, t);
56 [ + + ]: 110537 : if (isProofEnabled())
57 : : {
58 : 143798 : TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg);
59 : 71899 : d_tsubs.push_back(tnl);
60 : : // add to lazy proof
61 : 71899 : d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
62 : 71899 : }
63 : 110537 : }
64 : :
65 : 0 : void TrustSubstitutionMap::addSubstitution(TNode x,
66 : : TNode t,
67 : : ProofRule id,
68 : : const std::vector<Node>& children,
69 : : const std::vector<Node>& args)
70 : : {
71 [ - - ]: 0 : if (!isProofEnabled())
72 : : {
73 : 0 : addSubstitution(x, t, nullptr);
74 : 0 : return;
75 : : }
76 : 0 : LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx);
77 : 0 : Node eq = x.eqNode(t);
78 : 0 : stepPg->addStep(eq, id, children, args);
79 [ - - ]: 0 : addSubstitution(x, t, stepPg);
80 : 0 : }
81 : :
82 : 70224 : ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
83 : : TNode t,
84 : : TrustNode tn)
85 : : {
86 [ + - ]: 140448 : Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
87 [ - + ][ - - ]: 70224 : << x << " -> " << t << " from " << tn.getProven()
88 : 70224 : << std::endl;
89 [ + + ][ - + ]: 70224 : if (!isProofEnabled() || tn.getGenerator() == nullptr)
[ + + ]
90 : : {
91 : : // no generator or not proof enabled, nothing to do
92 : 30300 : addSubstitution(x, t, nullptr);
93 [ + - ]: 30300 : Trace("trust-subs") << "...no proof" << std::endl;
94 : 30300 : return nullptr;
95 : : }
96 : 39924 : Node eq = x.eqNode(t);
97 : 39924 : Node proven = tn.getProven();
98 : : // notice that this checks syntactic equality, not CDProof::isSame since
99 : : // tn.getGenerator() is not necessarily robust to symmetry.
100 [ + + ]: 39924 : if (eq == proven)
101 : : {
102 : : // no rewrite required, just use the generator
103 : 35118 : addSubstitution(x, t, tn.getGenerator());
104 [ + - ]: 35118 : Trace("trust-subs") << "...use generator directly" << std::endl;
105 : 35118 : return tn.getGenerator();
106 : : }
107 : 4806 : LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx);
108 : : // Try to transform tn.getProven() to (= x t) here, if necessary
109 [ + + ]: 4806 : if (!d_tspb->applyPredTransform(proven, eq, {}))
110 : : {
111 : : // failed to rewrite, we add a trust step which assumes eq is provable
112 : : // from proven, and proceed as normal.
113 [ + - ]: 89 : Trace("trust-subs") << "...failed to rewrite " << proven << std::endl;
114 : 89 : Node seq = proven.eqNode(eq);
115 : 89 : d_tspb->addTrustedStep(TrustId::SUBS_EQ, {}, {}, seq);
116 [ + + ][ - - ]: 267 : d_tspb->addStep(ProofRule::EQ_RESOLVE, {proven, seq}, {}, eq);
117 : 89 : }
118 [ + - ]: 4806 : Trace("trust-subs") << "...successful rewrite" << std::endl;
119 : 4806 : solvePg->addSteps(*d_tspb.get());
120 : 4806 : d_tspb->clear();
121 : : // link the given generator
122 : 4806 : solvePg->addLazyStep(proven, tn.getGenerator());
123 [ + - ]: 4806 : addSubstitution(x, t, solvePg);
124 [ + - ]: 4806 : return solvePg;
125 : 39924 : }
126 : :
127 : 36593 : void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
128 : : {
129 [ + + ]: 36593 : if (!isProofEnabled())
130 : : {
131 : : // just use the basic utility
132 : 21839 : d_subs.addSubstitutions(t.get());
133 : 21839 : return;
134 : : }
135 : : // call addSubstitution above in sequence
136 [ + + ]: 42553 : for (const TrustNode& tns : t.d_tsubs)
137 : : {
138 : 27799 : Node proven = tns.getProven();
139 : 27799 : addSubstitution(proven[0], proven[1], tns.getGenerator());
140 : 27799 : }
141 : : }
142 : :
143 : 2025955 : TrustNode TrustSubstitutionMap::applyTrusted(Node n, Rewriter* r)
144 : : {
145 [ + - ]: 4051910 : Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
146 : 2025955 : << std::endl;
147 : 2025955 : Node ns = d_subs.apply(n, r);
148 [ + - ]: 2025955 : Trace("trust-subs") << "...subs " << ns << std::endl;
149 [ + + ]: 2025955 : if (n == ns)
150 : : {
151 : : // no change
152 : 1619114 : return TrustNode::null();
153 : : }
154 [ + + ]: 406841 : if (!isProofEnabled())
155 : : {
156 : : // no proofs, use null generator
157 : 160031 : return TrustNode::mkTrustRewrite(n, ns, nullptr);
158 : : }
159 : 246810 : Node eq = n.eqNode(ns);
160 : : // If we haven't already stored an index, remember the index. Otherwise, a
161 : : // (possibly shorter) prefix of the substitution already suffices to show eq
162 [ + + ]: 246810 : if (d_eqtIndex.find(eq) == d_eqtIndex.end())
163 : : {
164 : 202929 : d_eqtIndex[eq] = d_tsubs.size();
165 : : }
166 : : // this class will provide a proof if asked
167 : 246810 : return TrustNode::mkTrustRewrite(n, ns, this);
168 : 2025955 : }
169 : :
170 : 659891 : Node TrustSubstitutionMap::apply(Node n, Rewriter* r)
171 : : {
172 : 659891 : return d_subs.apply(n, r);
173 : : }
174 : :
175 : 48331 : std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
176 : : {
177 [ - + ][ - + ]: 48331 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
178 : 48331 : Node n = eq[0];
179 : 48331 : Node ns = eq[1];
180 : : // Easy case: if n is in the domain of the substitution, maybe it is already
181 : : // a proof in the substitution proof generator. This is moreover required
182 : : // to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution,
183 : : // and we are asked to transform x, resulting in 5, we hence must provide
184 : : // a proof of (= x 5) based on the substitution. However, it must be the
185 : : // case that (= x 5) is a proven fact of the substitution generator. Hence
186 : : // we avoid a proof that looks like:
187 : : // ---------- from d_subsPg
188 : : // (= x 5)
189 : : // ---------- MACRO_SR_EQ_INTRO{x}
190 : : // (= x 5)
191 : : // by taking the premise proof directly.
192 : 48331 : if (d_subsPg->hasStep(eq) || d_subsPg->hasGenerator(eq))
193 : : {
194 : 135 : return d_subsPg->getProofFor(eq);
195 : : }
196 [ + - ]: 48196 : Trace("trust-subs-pf") << "getProofFor " << eq << std::endl;
197 : 48196 : AlwaysAssert(d_proving.find(eq) == d_proving.end())
198 : 0 : << "Repeat getProofFor in TrustSubstitutionMap " << eq;
199 : 48196 : d_proving.insert(eq);
200 : 48196 : NodeUIntMap::iterator it = d_eqtIndex.find(eq);
201 [ - + ][ - + ]: 48196 : Assert(it != d_eqtIndex.end());
[ - - ]
202 [ + - ]: 96392 : Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= "
203 : 48196 : << it->second << std::endl;
204 : 48196 : Node cs = getSubstitution(it->second);
205 [ + - ]: 48196 : Trace("trust-subs-pf") << "getProofFor substitution is " << cs << std::endl;
206 [ - + ][ - + ]: 48196 : Assert(eq != cs);
[ - - ]
207 : 48196 : std::vector<Node> pfChildren;
208 [ + + ]: 48196 : if (!cs.isConst())
209 : : {
210 : : // note that cs may be an AND node, in which case it specifies multiple
211 : : // substitutions
212 : 21750 : pfChildren.push_back(cs);
213 : : // connect substitution generator into apply generator
214 [ + - ]: 21750 : d_applyPg->addLazyStep(cs, d_subsPg.get());
215 : : }
216 [ + - ]: 48196 : Trace("trust-subs-pf") << "...apply eq intro" << std::endl;
217 : : // We use fixpoint as the substitution-apply identifier. Notice that it
218 : : // suffices to use SBA_SEQUENTIAL here, but SBA_FIXPOINT is typically
219 : : // more efficient. This is because for substitution of size n, sequential
220 : : // substitution can either be implemented as n traversals of the term to
221 : : // apply the substitution to, or a single traversal of the term, but n^2/2
222 : : // traversals of the range of the substitution to prepare a simultaneous
223 : : // substitution. Both of these options are inefficient. Note that we
224 : : // expect this rule to succeed, so useExpected is set to true.
225 [ - + ]: 48196 : if (!d_tspb->applyEqIntro(n,
226 : : ns,
227 : : pfChildren,
228 : : d_ids,
229 : : MethodId::SBA_FIXPOINT,
230 : : MethodId::RW_REWRITE,
231 : : true))
232 : : {
233 : : // if we fail for any reason, we must use a trusted step instead
234 : 0 : d_tspb->addTrustedStep(TrustId::SUBS_MAP, pfChildren, {}, eq);
235 : : }
236 [ + - ]: 48196 : 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 : 48196 : d_applyPg->addSteps(*d_tspb.get());
253 : 48196 : d_tspb->clear();
254 [ + - ]: 48196 : Trace("trust-subs-pf") << "...finish, make proof" << std::endl;
255 : 48196 : std::shared_ptr<ProofNode> ret = d_applyPg->getProofFor(eq);
256 : 48196 : d_proving.erase(eq);
257 : 48196 : return ret;
258 : 48331 : }
259 : :
260 : 0 : std::string TrustSubstitutionMap::identify() const { return d_name; }
261 : :
262 : 215552 : SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
263 : :
264 : 624195 : bool TrustSubstitutionMap::isProofEnabled() const
265 : : {
266 : 624195 : return d_subsPg != nullptr;
267 : : }
268 : :
269 : 48196 : Node TrustSubstitutionMap::getSubstitution(size_t index)
270 : : {
271 [ - + ][ - + ]: 48196 : Assert(index <= d_tsubs.size());
[ - - ]
272 : 48196 : std::vector<Node> csubsChildren;
273 [ + + ]: 2170800 : for (size_t i = 0; i < index; i++)
274 : : {
275 : 2122604 : csubsChildren.push_back(d_tsubs[i].getProven());
276 : : }
277 : 48196 : std::reverse(csubsChildren.begin(), csubsChildren.end());
278 : 48196 : Node cs = nodeManager()->mkAnd(csubsChildren);
279 [ + + ]: 48196 : if (cs.getKind() == Kind::AND)
280 : : {
281 : 18653 : d_subsPg->addStep(cs, ProofRule::AND_INTRO, csubsChildren, {});
282 : : }
283 : 96392 : return cs;
284 : 48196 : }
285 : :
286 : : } // namespace theory
287 : : } // namespace cvc5::internal
|
