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 : 2938383 : RewriteProofRule::RewriteProofRule() : d_id(ProofRewriteRule::NONE) {}
28 : :
29 : 2938383 : 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 [ + - ][ + - ]: 2938383 : Assert(d_cond.empty() && d_fvs.empty());
[ - + ][ - + ]
[ - - ]
39 : 2938383 : d_id = id;
40 : 2938383 : d_userFvs = userFvs;
41 : 2938383 : d_level = _level;
42 : 2938383 : std::map<Node, Node> condDef;
43 [ + + ]: 5283759 : for (const Node& c : cond)
44 : : {
45 [ - + ]: 2345376 : 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 : 2345376 : d_cond.push_back(c);
52 [ + - ][ + + ]: 2345376 : if (c.getKind() == Kind::EQUAL && c[0].getKind() == Kind::BOUND_VARIABLE)
[ + - ][ + + ]
[ - - ]
53 : : {
54 : 979461 : condDef[c[0]] = c[1];
55 : : }
56 : : }
57 : 2938383 : d_conc = conc;
58 : 2938383 : d_context = context;
59 [ - + ]: 2938383 : 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 : 2938383 : std::unordered_set<Node> fvsCond;
67 [ + + ]: 5283759 : for (const Node& c : d_cond)
68 : : {
69 : 2345376 : 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 : 2938383 : std::unordered_set<Node> fvsLhs;
75 : 2938383 : expr::getFreeVariables(d_conc[0], fvsLhs);
76 : 2938383 : std::unordered_set<Node> fvsUnmatched;
77 : 2938383 : expr::getFreeVariables(d_conc[1], fvsUnmatched);
78 : 2938383 : fvsUnmatched.insert(fvsCond.begin(), fvsCond.end());
79 : 2938383 : std::map<Node, Node>::iterator itc;
80 [ + + ]: 10001163 : for (const Node& v : fvsUnmatched)
81 : : {
82 [ + + ]: 7062780 : if (fvsLhs.find(v) != fvsLhs.end())
83 : : {
84 : : // variable on left hand side
85 : 6209916 : continue;
86 : : }
87 : 852864 : itc = condDef.find(v);
88 [ - + ]: 852864 : 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 : 852864 : d_condDefinedVars[v] = itc->second;
96 : : // ensure the defining term does not itself contain free variables
97 : 852864 : std::unordered_set<Node> fvst;
98 : 852864 : expr::getFreeVariables(itc->second, fvst);
99 [ + + ]: 2145486 : for (const Node& vt : fvst)
100 : : {
101 [ - + ]: 1292622 : 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 : 852864 : }
110 : :
111 : 2938383 : d_numFv = fvs.size();
112 : :
113 [ + + ]: 11420382 : for (const Node& v : fvs)
114 : : {
115 : 8481999 : d_fvs.push_back(v);
116 [ + + ]: 8481999 : if (fvsCond.find(v) == fvsCond.end())
117 : : {
118 : 4970598 : d_noOccVars.insert(v);
119 : : }
120 : : }
121 : : // if fixed point, initialize match utility
122 [ + + ]: 2938383 : if (d_context != Node::null())
123 : : {
124 : 113271 : d_mt.addTerm(conc[0]);
125 : :
126 [ - + ][ - + ]: 113271 : Assert(d_context.getKind() == Kind::LAMBDA);
[ - - ]
127 : 113271 : Node var = d_context[0][0];
128 : 113271 : Node curr = d_context[1];
129 [ + + ]: 193227 : while (curr != var)
130 : : {
131 : 79956 : size_t nchild = curr.getNumChildren();
132 : 79956 : size_t cfind = nchild;
133 [ + - ]: 166575 : for (size_t i = 0; i < nchild; i++)
134 : : {
135 : : // TODO (wishue #160): could use utility for finding path
136 [ + + ]: 166575 : if (expr::hasSubterm(curr[i], var))
137 : : {
138 : 79956 : cfind = i;
139 : 79956 : break;
140 : : }
141 : : }
142 [ - + ]: 79956 : if (cfind == nchild)
143 : : {
144 : 0 : Unhandled() << "Failed to find context variable";
145 : : }
146 : 79956 : d_pathToCtx.emplace_back(cfind);
147 : 79956 : curr = curr[cfind];
148 : : }
149 : 113271 : }
150 : 2938383 : }
151 : :
152 : 1234802 : 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 : 293251 : const std::vector<Node>& RewriteProofRule::getVarList() const { return d_fvs; }
161 : :
162 : 9884 : std::vector<Node> RewriteProofRule::getExplicitTypeOfList() const
163 : : {
164 : 9884 : std::vector<Node> ret;
165 : 9884 : Node conc = getConclusion(true);
166 : 9884 : std::unordered_set<Node> ccts;
167 : 9884 : expr::getKindSubterms(conc, Kind::TYPE_OF, true, ccts);
168 [ + + ]: 11803 : for (const Node& c : d_cond)
169 : : {
170 : 1919 : expr::getKindSubterms(c, Kind::TYPE_OF, true, ccts);
171 : : }
172 [ + + ]: 10040 : for (const Node& t : ccts)
173 : : {
174 : 156 : ret.emplace_back(t);
175 : : }
176 : 19768 : return ret;
177 : 9884 : }
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 : 91748 : const std::vector<Node>& RewriteProofRule::getConditions() const
196 : : {
197 : 91748 : return d_cond;
198 : : }
199 : :
200 : 1418552 : 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 [ + + ]: 1842431 : for (const Node& c : d_cond)
206 : : {
207 : 423879 : Node sc = expr::narySubstitute(c, vs, ss);
208 : 423879 : vcs.push_back(sc);
209 : 423879 : }
210 : 1418552 : return true;
211 : : }
212 : :
213 : 70230 : void RewriteProofRule::getMatches(Node h, expr::NotifyMatch* ntm) const
214 : : {
215 : 70230 : d_mt.getMatches(h, ntm);
216 : 70230 : }
217 : :
218 : 3000892 : Node RewriteProofRule::getConclusion(bool includeContext) const
219 : : {
220 : 3000892 : 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 [ + + ][ + + ]: 3000892 : if (includeContext && isFixedPoint())
[ + + ]
224 : : {
225 : 146968 : Node context = d_context;
226 : 293936 : Node rhs = context[1].substitute(TNode(context[0][0]), TNode(conc[1]));
227 : 146968 : conc = conc[0].eqNode(rhs);
228 : 146968 : }
229 : 3000892 : return conc;
230 : 0 : }
231 : :
232 : 292721 : Node RewriteProofRule::getConclusionFor(const std::vector<Node>& ss) const
233 : : {
234 [ - + ][ - + ]: 292721 : Assert(d_fvs.size() == ss.size());
[ - - ]
235 : 292721 : Node conc = getConclusion(true);
236 : 585442 : return expr::narySubstitute(conc, d_fvs, ss);
237 : 292721 : }
238 : :
239 : 207620 : Node RewriteProofRule::getConclusionFor(
240 : : const std::vector<Node>& ss,
241 : : std::vector<std::pair<Kind, std::vector<Node>>>& witnessTerms) const
242 : : {
243 [ - + ][ - + ]: 207620 : Assert(d_fvs.size() == ss.size());
[ - - ]
244 : 207620 : Node conc = getConclusion(true);
245 : 207620 : NodeManager* nm = conc.getNodeManager();
246 : 207620 : std::unordered_map<TNode, Node> visited;
247 : 207620 : Node ret = expr::narySubstitute(conc, d_fvs, ss, visited);
248 : : // also compute for the condition
249 [ + + ]: 216155 : for (const Node& c : d_cond)
250 : : {
251 : 8535 : expr::narySubstitute(c, d_fvs, ss, visited);
252 : : }
253 : 207620 : std::map<Node, Node>::const_iterator itl;
254 [ + + ]: 600916 : for (size_t i = 0, nfvs = ss.size(); i < nfvs; i++)
255 : : {
256 : 393296 : TNode v = d_fvs[i];
257 : 393296 : Kind wk = Kind::UNDEFINED_KIND;
258 : 393296 : std::vector<Node> wargs;
259 [ + + ]: 393296 : if (!expr::isListVar(v))
260 : : {
261 : : // if not a list variable, it is the given term
262 : 378086 : wargs.push_back(ss[i]);
263 : : }
264 : : else
265 : : {
266 : 15210 : itl = d_listVarCtx.find(v);
267 [ - + ][ - + ]: 15210 : Assert(itl != d_listVarCtx.end());
[ - - ]
268 : 15210 : Node ctx = itl->second;
269 [ + + ]: 15210 : 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 : 7744 : Node subsCtx = visited[ctx];
274 : 7744 : Assert(!subsCtx.isNull()) << "Failed to get context for " << ctx << " in " << d_id;
275 : 7744 : Node nt = expr::getNullTerminator(nm, ctx.getKind(), subsCtx.getType());
276 : 7744 : wargs.push_back(nt);
277 : 7744 : }
278 : : else
279 : : {
280 : 7466 : wk = ctx.getKind();
281 : 7466 : wargs.insert(wargs.end(), ss[i].begin(), ss[i].end());
282 : : }
283 : 15210 : }
284 : 393296 : witnessTerms.emplace_back(wk, wargs);
285 : 393296 : }
286 : 415240 : return ret;
287 : 207620 : }
288 : :
289 : 2947059 : bool RewriteProofRule::isFixedPoint() const
290 : : {
291 : 2947059 : return d_context != Node::null();
292 : : }
293 : :
294 : 91854 : void RewriteProofRule::getConditionalDefinitions(const std::vector<Node>& vs,
295 : : const std::vector<Node>& ss,
296 : : std::vector<Node>& dvs,
297 : : std::vector<Node>& dss) const
298 : : {
299 [ + + ]: 141775 : for (const std::pair<const Node, Node>& cv : d_condDefinedVars)
300 : : {
301 : 49921 : dvs.push_back(cv.first);
302 : 49921 : Node cvs = expr::narySubstitute(cv.second, vs, ss);
303 : 49921 : dss.push_back(cvs);
304 : 49921 : }
305 : 91854 : }
306 : :
307 : 0 : Level RewriteProofRule::getSignatureLevel() const { return d_level; }
308 : :
309 : : } // namespace rewriter
310 : : } // namespace cvc5::internal
|
