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 : : * Alpha equivalence checking.
11 : : */
12 : :
13 : : #include "theory/quantifiers/alpha_equivalence.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "proof/method_id.h"
17 : : #include "proof/proof.h"
18 : : #include "proof/proof_node.h"
19 : : #include "theory/builtin/proof_checker.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace quantifiers {
26 : :
27 : : struct sortTypeOrder
28 : : {
29 : : expr::TermCanonize* d_tu;
30 : 36207 : bool operator()(TypeNode i, TypeNode j)
31 : : {
32 : 36207 : return d_tu->getIdForType(i) < d_tu->getIdForType(j);
33 : : }
34 : : };
35 : :
36 : 68301 : AlphaEquivalenceTypeNode::AlphaEquivalenceTypeNode(context::Context* c)
37 : 68301 : : d_quant(c)
38 : : {
39 : 68301 : }
40 : :
41 : 59699 : Node AlphaEquivalenceTypeNode::registerNode(
42 : : context::Context* c,
43 : : Node q,
44 : : Node t,
45 : : std::vector<TypeNode>& typs,
46 : : std::map<TypeNode, size_t>& typCount)
47 : : {
48 : 59699 : AlphaEquivalenceTypeNode* aetn = this;
49 : 59699 : size_t index = 0;
50 : : std::map<std::pair<TypeNode, size_t>,
51 : 59699 : std::unique_ptr<AlphaEquivalenceTypeNode>>::iterator itc;
52 [ + + ]: 142780 : while (index < typs.size())
53 : : {
54 : 83081 : TypeNode curr = typs[index];
55 [ - + ][ - + ]: 83081 : Assert(typCount.find(curr) != typCount.end());
[ - - ]
56 [ + - ]: 83081 : Trace("aeq-debug") << "[" << curr << " " << typCount[curr] << "] ";
57 : 83081 : std::pair<TypeNode, size_t> key(curr, typCount[curr]);
58 : 83081 : itc = aetn->d_children.find(key);
59 [ + + ]: 83081 : if (itc == aetn->d_children.end())
60 : : {
61 : 23819 : aetn->d_children[key] = std::make_unique<AlphaEquivalenceTypeNode>(c);
62 : 23819 : aetn = aetn->d_children[key].get();
63 : : }
64 : : else
65 : : {
66 : 59262 : aetn = itc->second.get();
67 : : }
68 : 83081 : index = index + 1;
69 : 83081 : }
70 [ + - ]: 59699 : Trace("aeq-debug") << " : ";
71 : 59699 : NodeMap::iterator it = aetn->d_quant.find(t);
72 [ + + ][ + - ]: 59699 : if (it != aetn->d_quant.end() && !it->second.isNull())
[ + + ]
73 : : {
74 [ + - ]: 5267 : Trace("aeq-debug") << it->second << std::endl;
75 : 5267 : return it->second;
76 : : }
77 [ + - ]: 54432 : Trace("aeq-debug") << "(new)" << std::endl;
78 : 54432 : aetn->d_quant[t] = q;
79 : 54432 : return q;
80 : : }
81 : :
82 : 44482 : AlphaEquivalenceDb::AlphaEquivalenceDb(context::Context* c,
83 : : expr::TermCanonize* tc,
84 : 44482 : bool sortCommChildren)
85 : 44482 : : d_context(c),
86 : 44482 : d_ae_typ_trie(c),
87 : 44482 : d_tc(tc),
88 : 44482 : d_sortCommutativeOpChildren(sortCommChildren)
89 : : {
90 : 44482 : }
91 : 26528 : Node AlphaEquivalenceDb::addTerm(Node q)
92 : : {
93 [ - + ][ - + ]: 26528 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
94 [ + - ]: 26528 : Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
95 : : // construct canonical quantified formula
96 : 53056 : Node t = d_tc->getCanonicalTerm(q[1], d_sortCommutativeOpChildren);
97 [ + - ]: 26528 : Trace("aeq") << " canonical form: " << t << std::endl;
98 : 53056 : return addTermToTypeTrie(t, q);
99 : 26528 : }
100 : :
101 : 33171 : Node AlphaEquivalenceDb::addTermWithSubstitution(Node q,
102 : : std::vector<Node>& vars,
103 : : std::vector<Node>& subs)
104 : : {
105 [ + - ]: 33171 : Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
106 : : // construct canonical quantified formula with visited cache
107 : 33171 : std::map<TNode, Node> visited;
108 : 66342 : Node t = d_tc->getCanonicalTerm(q[1], visited, d_sortCommutativeOpChildren);
109 : : // only need to store BOUND_VARIABLE in substitution
110 : 33171 : std::map<Node, TNode>& bm = d_bvmap[q];
111 [ + + ]: 445412 : for (const std::pair<const TNode, Node>& b : visited)
112 : : {
113 [ + + ]: 412241 : if (b.first.getKind() == Kind::BOUND_VARIABLE)
114 : : {
115 [ - + ][ - + ]: 84206 : Assert(b.second.getKind() == Kind::BOUND_VARIABLE);
[ - - ]
116 : 84206 : bm[b.second] = b.first;
117 : : }
118 : : }
119 : 66342 : Node qret = addTermToTypeTrie(t, q);
120 [ + + ]: 33171 : if (qret != q)
121 : : {
122 [ - + ][ - + ]: 3126 : Assert(d_bvmap.find(qret) != d_bvmap.end());
[ - - ]
123 : 3126 : std::map<Node, TNode>& bmr = d_bvmap[qret];
124 : 3126 : std::map<Node, TNode>::iterator itb;
125 [ + + ]: 8640 : for (const std::pair<const Node, TNode>& b : bmr)
126 : : {
127 : 5514 : itb = bm.find(b.first);
128 [ - + ]: 5514 : if (itb == bm.end())
129 : : {
130 : : // didn't use the same variables, fail
131 : 0 : vars.clear();
132 : 0 : subs.clear();
133 : 0 : break;
134 : : }
135 : : // otherwise, we map the variable in the returned quantified formula
136 : : // to the variable that used the same canonical variable
137 : 5514 : vars.push_back(b.second);
138 : 5514 : subs.push_back(itb->second);
139 : : }
140 : : }
141 : 66342 : return qret;
142 : 33171 : }
143 : :
144 : 59699 : Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q)
145 : : {
146 : : // compute variable type counts
147 : 59699 : std::map<TypeNode, size_t> typCount;
148 : 59699 : std::vector<TypeNode> typs;
149 [ + + ]: 185961 : for (const Node& v : q[0])
150 : : {
151 : 126262 : TypeNode tn = v.getType();
152 : 126262 : typCount[tn]++;
153 [ + + ]: 126262 : if (std::find(typs.begin(), typs.end(), tn) == typs.end())
154 : : {
155 : 83081 : typs.push_back(tn);
156 : : }
157 : 185961 : }
158 : : sortTypeOrder sto;
159 : 59699 : sto.d_tu = d_tc;
160 : 59699 : std::sort(typs.begin(), typs.end(), sto);
161 [ + - ]: 59699 : Trace("aeq-debug") << " ";
162 : 119398 : Node ret = d_ae_typ_trie.registerNode(d_context, q, t, typs, typCount);
163 [ + - ]: 59699 : Trace("aeq") << " ...result : " << ret << std::endl;
164 : 119398 : return ret;
165 : 59699 : }
166 : :
167 : 44482 : AlphaEquivalence::AlphaEquivalence(Env& env)
168 : : : EnvObj(env),
169 : 44482 : d_termCanon(),
170 : 44482 : d_aedb(userContext(), &d_termCanon, true),
171 : 44482 : d_pfAlpha(env.isTheoryProofProducing() ? new EagerProofGenerator(env)
172 : 44482 : : nullptr)
173 : : {
174 : 44482 : }
175 : :
176 : 59699 : TrustNode AlphaEquivalence::reduceQuantifier(Node q)
177 : : {
178 [ - + ][ - + ]: 59699 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
179 : 59699 : Node ret;
180 : 59699 : std::vector<Node> vars;
181 : 59699 : std::vector<Node> subs;
182 [ + + ]: 59699 : if (isProofEnabled())
183 : : {
184 : 33171 : ret = d_aedb.addTermWithSubstitution(q, vars, subs);
185 : : }
186 : : else
187 : : {
188 : 26528 : ret = d_aedb.addTerm(q);
189 : : }
190 [ + + ]: 59699 : if (ret == q)
191 : : {
192 : 54432 : return TrustNode::null();
193 : : }
194 : 5267 : Node lem;
195 : 5267 : ProofGenerator* pg = nullptr;
196 : : // lemma ( q <=> d_quant )
197 : : // Notice that we infer this equivalence regardless of whether q or ret
198 : : // have annotations (e.g. user patterns, names, etc.).
199 [ + - ]: 5267 : Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
200 [ + - ]: 5267 : Trace("alpha-eq") << " " << q << std::endl;
201 [ + - ]: 5267 : Trace("alpha-eq") << " " << ret << std::endl;
202 : 5267 : lem = ret.eqNode(q);
203 [ + + ]: 5267 : if (q.getNumChildren() == 3)
204 : : {
205 : 84 : verbose(1) << "Ignoring annotated quantified formula based on alpha "
206 : 84 : "equivalence: "
207 : 84 : << q << std::endl;
208 : : }
209 : : // if successfully computed the substitution above
210 [ + + ][ + + ]: 5267 : if (isProofEnabled() && !vars.empty())
[ + + ]
211 : : {
212 : 3122 : NodeManager* nm = nodeManager();
213 : 3122 : Node proveLem = lem;
214 : 6244 : CDProof cdp(d_env);
215 : : // remove patterns from both sides
216 [ + + ]: 3122 : if (q.getNumChildren() == 3)
217 : : {
218 : 44 : Node qo = q;
219 : 44 : q = builtin::BuiltinProofRuleChecker::getEncodeEqIntro(nm, q);
220 [ + - ]: 44 : if (q != qo)
221 : : {
222 : 44 : Node eqq = qo.eqNode(q);
223 : 88 : cdp.addStep(eqq, ProofRule::ENCODE_EQ_INTRO, {}, {qo});
224 : 44 : Node eqqs = q.eqNode(qo);
225 : 88 : cdp.addStep(eqqs, ProofRule::SYMM, {eqq}, {});
226 : 44 : Node eqq2 = ret.eqNode(q);
227 [ + + ][ - - ]: 132 : cdp.addStep(proveLem, ProofRule::TRANS, {eqq2, eqqs}, {});
228 : 44 : proveLem = eqq2;
229 : 44 : }
230 : 44 : }
231 [ + + ]: 3122 : if (ret.getNumChildren() == 3)
232 : : {
233 : 36 : Node reto = ret;
234 : 36 : ret = builtin::BuiltinProofRuleChecker::getEncodeEqIntro(nm, ret);
235 [ + - ]: 36 : if (ret != reto)
236 : : {
237 : 36 : Node eqq = reto.eqNode(ret);
238 : 72 : cdp.addStep(eqq, ProofRule::ENCODE_EQ_INTRO, {}, {reto});
239 : 36 : Node eqq2 = ret.eqNode(q);
240 [ + + ][ - - ]: 108 : cdp.addStep(proveLem, ProofRule::TRANS, {eqq, eqq2}, {});
241 : 36 : proveLem = eqq2;
242 : 36 : }
243 : 36 : }
244 [ + - ]: 3122 : if (Configuration::isAssertionBuild())
245 : : {
246 : : // all variables should be unique since we are processing rewritten
247 : : // quantified formulas
248 : 3122 : std::unordered_set<Node> vset(vars.begin(), vars.end());
249 [ - + ][ - + ]: 3122 : Assert(vset.size() == vars.size());
[ - - ]
250 : 3122 : std::unordered_set<Node> sset(subs.begin(), subs.end());
251 [ - + ][ - + ]: 3122 : Assert(sset.size() == subs.size());
[ - - ]
252 : 3122 : }
253 : 3122 : std::vector<Node> transEq;
254 : : // if there is variable shadowing, we do an intermediate step with fresh
255 : : // variables
256 [ + + ]: 3122 : if (expr::hasSubterm(ret, subs))
257 : : {
258 : 1164 : std::vector<Node> isubs;
259 [ + + ]: 3764 : for (const Node& v : subs)
260 : : {
261 : 2600 : isubs.emplace_back(NodeManager::mkBoundVar(v.getType()));
262 : : }
263 : : // ---------- ALPHA_EQUIV
264 : : // ret = iret
265 : 1164 : Node ieq = addAlphaEquivStep(cdp, ret, vars, isubs);
266 : 1164 : transEq.emplace_back(ieq);
267 : 1164 : ret = ieq[1];
268 : 1164 : vars = isubs;
269 : 1164 : }
270 : : // ---------- ALPHA_EQUIV
271 : : // ret = sret
272 : 3122 : Node eq = addAlphaEquivStep(cdp, ret, vars, subs);
273 [ - + ][ - + ]: 3122 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
274 : 3122 : Node sret = eq[1];
275 : 3122 : transEq.emplace_back(eq);
276 [ - + ][ - + ]: 3122 : Assert(sret.getKind() == Kind::FORALL);
[ - - ]
277 [ + + ]: 3122 : if (sret[0] != q[0])
278 : : {
279 : : // variable reorder?
280 : 204 : std::vector<Node> children;
281 : 204 : children.push_back(q[0]);
282 : 204 : children.push_back(sret[1]);
283 [ - + ]: 204 : if (sret.getNumChildren() == 3)
284 : : {
285 : 0 : children.push_back(sret[2]);
286 : : }
287 : 204 : Node sreorder = nm->mkNode(Kind::FORALL, children);
288 : 204 : Node eqqr = sret.eqNode(sreorder);
289 [ + + ][ + - ]: 408 : if (cdp.addStep(eqqr, ProofRule::QUANT_VAR_REORDERING, {}, {eqqr}))
[ - - ]
290 : : {
291 : 204 : transEq.push_back(eqqr);
292 : 204 : sret = sreorder;
293 : : }
294 : : // if var reordering did not apply, we likely will not succeed below
295 : 204 : }
296 : : // if not syntactically equal, maybe it can be transformed
297 : 3122 : bool success = false;
298 [ + + ]: 3122 : if (sret == q)
299 : : {
300 : 2934 : success = true;
301 : : }
302 : : else
303 : : {
304 : 188 : Node eq2 = sret.eqNode(q);
305 : 188 : transEq.push_back(eq2);
306 : 188 : Node eq2r = extendedRewrite(eq2);
307 [ + - ][ + - ]: 188 : if (eq2r.isConst() && eq2r.getConst<bool>())
[ + - ]
308 : : {
309 : : // ---------- MACRO_SR_PRED_INTRO
310 : : // sret = q
311 : 188 : std::vector<Node> pfArgs2;
312 : 188 : pfArgs2.push_back(eq2);
313 : 188 : addMethodIds(nodeManager(),
314 : : pfArgs2,
315 : : MethodId::SB_DEFAULT,
316 : : MethodId::SBA_SEQUENTIAL,
317 : : MethodId::RW_EXT_REWRITE);
318 : 188 : cdp.addStep(eq2, ProofRule::MACRO_SR_PRED_INTRO, {}, pfArgs2);
319 : 188 : success = true;
320 : 188 : }
321 : 188 : }
322 : : // if successful, store the proof and remember the proof generator
323 [ + - ]: 3122 : if (success)
324 : : {
325 [ + + ]: 3122 : if (transEq.size() > 1)
326 : : {
327 : : // TRANS of ALPHA_EQ and MACRO_SR_PRED_INTRO steps from above
328 : 1332 : cdp.addStep(proveLem, ProofRule::TRANS, transEq, {});
329 : : }
330 : 3122 : std::shared_ptr<ProofNode> pn = cdp.getProofFor(lem);
331 [ + - ]: 3122 : Trace("alpha-eq") << "Proof is " << *pn.get() << std::endl;
332 : 3122 : d_pfAlpha->setProofFor(lem, pn);
333 [ + - ]: 3122 : pg = d_pfAlpha.get();
334 : 3122 : }
335 : 3122 : }
336 : 5267 : return TrustNode::mkTrustLemma(lem, pg);
337 : 59699 : }
338 : :
339 : 4286 : Node AlphaEquivalence::addAlphaEquivStep(CDProof& cdp,
340 : : const Node& f,
341 : : const std::vector<Node>& vars,
342 : : const std::vector<Node>& subs)
343 : : {
344 : 4286 : std::vector<Node> pfArgs;
345 : 4286 : pfArgs.push_back(f);
346 : 4286 : NodeManager* nm = nodeManager();
347 : 4286 : pfArgs.push_back(nm->mkNode(Kind::SEXPR, vars));
348 : 4286 : pfArgs.push_back(nm->mkNode(Kind::SEXPR, subs));
349 : 4286 : Node sf = f.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
350 : 4286 : std::vector<Node> transEq;
351 : 4286 : Node eq = f.eqNode(sf);
352 : 4286 : cdp.addStep(eq, ProofRule::ALPHA_EQUIV, {}, pfArgs);
353 : : // if not syntactically equal, maybe it can be transform
354 : 8572 : return eq;
355 : 4286 : }
356 : :
357 : 64966 : bool AlphaEquivalence::isProofEnabled() const { return d_pfAlpha != nullptr; }
358 : :
359 : : } // namespace quantifiers
360 : : } // namespace theory
361 : : } // namespace cvc5::internal
|
