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