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 : : * proof rewrite rule class
11 : : */
12 : :
13 : : #include "rewriter/rewrite_proof_rule.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/aci_norm.h"
18 : : #include "expr/nary_term_util.h"
19 : : #include "expr/node_algorithm.h"
20 : : #include "proof/proof_checker.h"
21 : :
22 : : using namespace cvc5::internal::kind;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace rewriter {
26 : :
27 : 3906960 : RewriteProofRule::RewriteProofRule() : d_id(ProofRewriteRule::NONE) {}
28 : :
29 : 3906960 : void RewriteProofRule::init(ProofRewriteRule id,
30 : : const std::vector<Node>& userFvs,
31 : : const std::vector<Node>& fvs,
32 : : const std::vector<Node>& cond,
33 : : Node conc,
34 : : Node context,
35 : : Level _level)
36 : : {
37 : : // not initialized yet
38 [ + - ][ + - ]: 3906960 : Assert(d_cond.empty() && d_fvs.empty());
[ - + ][ - + ]
[ - - ]
39 : 3906960 : d_id = id;
40 : 3906960 : d_userFvs = userFvs;
41 : 3906960 : d_level = _level;
42 : 3906960 : std::map<Node, Node> condDef;
43 [ + + ]: 7046800 : for (const Node& c : cond)
44 : : {
45 [ - + ]: 3139840 : if (!expr::getListVarContext(c, d_listVarCtx))
46 : : {
47 : 0 : Unhandled() << "Ambiguous or illegal context for list variables in "
48 : 0 : "condition of rule "
49 : 0 : << id;
50 : : }
51 : 3139840 : d_cond.push_back(c);
52 [ + - ][ + + ]: 3139840 : if (c.getKind() == Kind::EQUAL && c[0].getKind() == Kind::BOUND_VARIABLE)
[ + - ][ + + ]
[ - - ]
53 : : {
54 : 1311240 : condDef[c[0]] = c[1];
55 : : }
56 : : }
57 : 3906960 : d_conc = conc;
58 : 3906960 : d_context = context;
59 [ - + ]: 3906960 : if (!expr::getListVarContext(conc, d_listVarCtx))
60 : : {
61 : 0 : Unhandled() << "Ambiguous or illegal context for list variables in "
62 : 0 : "conclusion of rule "
63 : 0 : << id;
64 : : }
65 : :
66 : 3906960 : std::unordered_set<Node> fvsCond;
67 [ + + ]: 7046800 : for (const Node& c : d_cond)
68 : : {
69 : 3139840 : expr::getFreeVariables(c, fvsCond);
70 : : }
71 : :
72 : : // ensure free variables in conditions and right hand side are either matched
73 : : // or are in defined conditions.
74 : 3906960 : std::unordered_set<Node> fvsLhs;
75 : 3906960 : expr::getFreeVariables(d_conc[0], fvsLhs);
76 : 3906960 : std::unordered_set<Node> fvsUnmatched;
77 : 3906960 : expr::getFreeVariables(d_conc[1], fvsUnmatched);
78 : 3906960 : fvsUnmatched.insert(fvsCond.begin(), fvsCond.end());
79 : 3906960 : std::map<Node, Node>::iterator itc;
80 [ + + ]: 13317560 : for (const Node& v : fvsUnmatched)
81 : : {
82 [ + + ]: 9410600 : if (fvsLhs.find(v) != fvsLhs.end())
83 : : {
84 : : // variable on left hand side
85 : 8268840 : continue;
86 : : }
87 : 1141760 : itc = condDef.find(v);
88 [ - + ]: 1141760 : if (itc == condDef.end())
89 : : {
90 : 0 : Unhandled()
91 : 0 : << "Free variable " << v << " in rule " << id
92 : 0 : << " is not on the left hand side, nor is defined in a condition";
93 : : }
94 : : // variable defined in the condition
95 : 1141760 : d_condDefinedVars[v] = itc->second;
96 : : // ensure the defining term does not itself contain free variables
97 : 1141760 : std::unordered_set<Node> fvst;
98 : 1141760 : expr::getFreeVariables(itc->second, fvst);
99 [ + + ]: 2872240 : for (const Node& vt : fvst)
100 : : {
101 [ - + ]: 1730480 : if (fvsLhs.find(vt) == fvsLhs.end())
102 : : {
103 : 0 : Unhandled() << "Free variable " << vt << " in rule " << id
104 : : << " is not on the left hand side of the rule, and it is "
105 : 0 : "used to give a definition to the free variable "
106 : 0 : << v;
107 : : }
108 : : }
109 : 1141760 : }
110 : :
111 : 3906960 : d_numFv = fvs.size();
112 : :
113 [ + + ]: 15217520 : for (const Node& v : fvs)
114 : : {
115 : 11310560 : d_fvs.push_back(v);
116 [ + + ]: 11310560 : if (fvsCond.find(v) == fvsCond.end())
117 : : {
118 : 6609720 : d_noOccVars.insert(v);
119 : : }
120 : : }
121 : : // if fixed point, initialize match utility
122 [ + + ]: 3906960 : if (d_context != Node::null())
123 : : {
124 : 151640 : d_mt.addTerm(conc[0]);
125 : :
126 [ - + ][ - + ]: 151640 : Assert(d_context.getKind() == Kind::LAMBDA);
[ - - ]
127 : 151640 : Node var = d_context[0][0];
128 : 151640 : Node curr = d_context[1];
129 [ + + ]: 258680 : while (curr != var)
130 : : {
131 : 107040 : size_t nchild = curr.getNumChildren();
132 : 107040 : size_t cfind = nchild;
133 [ + - ]: 223000 : for (size_t i = 0; i < nchild; i++)
134 : : {
135 : : // TODO (wishue #160): could use utility for finding path
136 [ + + ]: 223000 : if (expr::hasSubterm(curr[i], var))
137 : : {
138 : 107040 : cfind = i;
139 : 107040 : break;
140 : : }
141 : : }
142 [ - + ]: 107040 : if (cfind == nchild)
143 : : {
144 : 0 : Unhandled() << "Failed to find context variable";
145 : : }
146 : 107040 : d_pathToCtx.emplace_back(cfind);
147 : 107040 : curr = curr[cfind];
148 : : }
149 : 151640 : }
150 : 3906960 : }
151 : :
152 : 1827283 : ProofRewriteRule RewriteProofRule::getId() const { return d_id; }
153 : :
154 : 0 : const char* RewriteProofRule::getName() const { return toString(d_id); }
155 : :
156 : 2 : const std::vector<Node>& RewriteProofRule::getUserVarList() const
157 : : {
158 : 2 : return d_userFvs;
159 : : }
160 : 386215 : const std::vector<Node>& RewriteProofRule::getVarList() const { return d_fvs; }
161 : :
162 : 10045 : std::vector<Node> RewriteProofRule::getExplicitTypeOfList() const
163 : : {
164 : 10045 : std::vector<Node> ret;
165 : 10045 : Node conc = getConclusion(true);
166 : 10045 : std::unordered_set<Node> ccts;
167 : 10045 : expr::getKindSubterms(conc, Kind::TYPE_OF, true, ccts);
168 [ + + ]: 12007 : for (const Node& c : d_cond)
169 : : {
170 : 1962 : expr::getKindSubterms(c, Kind::TYPE_OF, true, ccts);
171 : : }
172 [ + + ]: 10204 : for (const Node& t : ccts)
173 : : {
174 : 159 : ret.emplace_back(t);
175 : : }
176 : 20090 : return ret;
177 : 10045 : }
178 : :
179 : 12 : bool RewriteProofRule::isExplicitVar(Node v) const
180 : : {
181 [ - + ][ - + ]: 12 : Assert(std::find(d_fvs.begin(), d_fvs.end(), v) != d_fvs.end());
[ - - ]
182 : 12 : return d_noOccVars.find(v) != d_noOccVars.end();
183 : : }
184 : 0 : Kind RewriteProofRule::getListContext(Node v) const
185 : : {
186 : 0 : std::map<Node, Node>::const_iterator it = d_listVarCtx.find(v);
187 [ - - ]: 0 : if (it != d_listVarCtx.end())
188 : : {
189 : 0 : return it->second.getKind();
190 : : }
191 : 0 : return Kind::UNDEFINED_KIND;
192 : : }
193 : 0 : bool RewriteProofRule::hasConditions() const { return !d_cond.empty(); }
194 : :
195 : 93237 : const std::vector<Node>& RewriteProofRule::getConditions() const
196 : : {
197 : 93237 : return d_cond;
198 : : }
199 : :
200 : 2093326 : bool RewriteProofRule::getObligations(const std::vector<Node>& vs,
201 : : const std::vector<Node>& ss,
202 : : std::vector<Node>& vcs) const
203 : : {
204 : : // substitute into each condition
205 [ + + ]: 2727362 : for (const Node& c : d_cond)
206 : : {
207 : 634036 : Node sc = expr::narySubstitute(c, vs, ss);
208 : 634036 : vcs.push_back(sc);
209 : 634036 : }
210 : 2093326 : return true;
211 : : }
212 : :
213 : 105976 : void RewriteProofRule::getMatches(Node h, expr::NotifyMatch* ntm) const
214 : : {
215 : 105976 : d_mt.getMatches(h, ntm);
216 : 105976 : }
217 : :
218 : 4292144 : Node RewriteProofRule::getConclusion(bool includeContext) const
219 : : {
220 : 4292144 : Node conc = d_conc;
221 : : // if the rule has conclusion s, and term context (lambda x. t[x]), then the
222 : : // conclusion is t[s], which we compute in the block below.
223 [ + + ][ + + ]: 4292144 : if (includeContext && isFixedPoint())
[ + + ]
224 : : {
225 : 213839 : Node context = d_context;
226 : 427678 : Node rhs = context[1].substitute(TNode(context[0][0]), TNode(conc[1]));
227 : 213839 : conc = conc[0].eqNode(rhs);
228 : 213839 : }
229 : 4292144 : return conc;
230 : 0 : }
231 : :
232 : 385679 : Node RewriteProofRule::getConclusionFor(const std::vector<Node>& ss) const
233 : : {
234 [ - + ][ - + ]: 385679 : Assert(d_fvs.size() == ss.size());
[ - - ]
235 : 385679 : Node conc = getConclusion(true);
236 : 771358 : return expr::narySubstitute(conc, d_fvs, ss);
237 : 385679 : }
238 : :
239 : 211313 : Node RewriteProofRule::getConclusionFor(
240 : : const std::vector<Node>& ss,
241 : : std::vector<std::pair<Kind, std::vector<Node>>>& witnessTerms) const
242 : : {
243 [ - + ][ - + ]: 211313 : Assert(d_fvs.size() == ss.size());
[ - - ]
244 : 211313 : Node conc = getConclusion(true);
245 : 211313 : NodeManager* nm = conc.getNodeManager();
246 : 211313 : std::unordered_map<TNode, Node> visited;
247 : 211313 : Node ret = expr::narySubstitute(conc, d_fvs, ss, visited);
248 : : // also compute for the condition
249 [ + + ]: 220000 : for (const Node& c : d_cond)
250 : : {
251 : 8687 : expr::narySubstitute(c, d_fvs, ss, visited);
252 : : }
253 : 211313 : std::map<Node, Node>::const_iterator itl;
254 [ + + ]: 611646 : for (size_t i = 0, nfvs = ss.size(); i < nfvs; i++)
255 : : {
256 : 400333 : TNode v = d_fvs[i];
257 : 400333 : Kind wk = Kind::UNDEFINED_KIND;
258 : 400333 : std::vector<Node> wargs;
259 [ + + ]: 400333 : if (!expr::isListVar(v))
260 : : {
261 : : // if not a list variable, it is the given term
262 : 384823 : wargs.push_back(ss[i]);
263 : : }
264 : : else
265 : : {
266 : 15510 : itl = d_listVarCtx.find(v);
267 [ - + ][ - + ]: 15510 : Assert(itl != d_listVarCtx.end());
[ - - ]
268 : 15510 : Node ctx = itl->second;
269 [ + + ]: 15510 : if (ss[i].getNumChildren() == 0)
270 : : {
271 : : // to determine the type, we get the type of the substitution of the
272 : : // list context of the variable.
273 : 7927 : Node subsCtx = visited[ctx];
274 [ - + ][ - - ]: 7927 : Assert(!subsCtx.isNull())
275 [ - + ][ - + ]: 7927 : << "Failed to get context for " << ctx << " in " << d_id;
[ - - ]
276 : 7927 : Node nt = expr::getNullTerminator(nm, ctx.getKind(), subsCtx.getType());
277 : 7927 : wargs.push_back(nt);
278 : 7927 : }
279 : : else
280 : : {
281 : 7583 : wk = ctx.getKind();
282 : 7583 : wargs.insert(wargs.end(), ss[i].begin(), ss[i].end());
283 : : }
284 : 15510 : }
285 : 400333 : witnessTerms.emplace_back(wk, wargs);
286 : 400333 : }
287 : 422626 : return ret;
288 : 211313 : }
289 : :
290 : 4211325 : bool RewriteProofRule::isFixedPoint() const
291 : : {
292 : 4211325 : return d_context != Node::null();
293 : : }
294 : :
295 : 137271 : void RewriteProofRule::getConditionalDefinitions(const std::vector<Node>& vs,
296 : : const std::vector<Node>& ss,
297 : : std::vector<Node>& dvs,
298 : : std::vector<Node>& dss) const
299 : : {
300 [ + + ]: 212662 : for (const std::pair<const Node, Node>& cv : d_condDefinedVars)
301 : : {
302 : 75391 : dvs.push_back(cv.first);
303 : 75391 : Node cvs = expr::narySubstitute(cv.second, vs, ss);
304 : 75391 : dss.push_back(cvs);
305 : 75391 : }
306 : 137271 : }
307 : :
308 : 0 : Level RewriteProofRule::getSignatureLevel() const { return d_level; }
309 : :
310 : : } // namespace rewriter
311 : : } // namespace cvc5::internal
|
