Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of proof node algorithm utilities.
14 : : */
15 : :
16 : : #include "proof/proof_node_algorithm.h"
17 : :
18 : : #include "proof/proof.h"
19 : : #include "proof/proof_checker.h"
20 : : #include "proof/proof_node.h"
21 : : #include "proof/proof_node_manager.h"
22 : : #include "proof/proof_rule_checker.h"
23 : : #include "theory/builtin/generic_op.h"
24 : :
25 : : namespace cvc5::internal {
26 : : namespace expr {
27 : :
28 : 424473 : void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
29 : : {
30 : 848946 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
31 : : std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
32 : 848946 : pn->getRule(), pn->getChildren(), pn->getArguments());
33 : 424473 : getFreeAssumptionsMap(spn, amap);
34 : 704156 : for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
35 [ + + ]: 1832780 : amap)
36 : : {
37 : 704156 : assump.push_back(p.first);
38 : : }
39 : 424473 : }
40 : :
41 : 2440560 : void getFreeAssumptionsMap(
42 : : std::shared_ptr<ProofNode> pn,
43 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
44 : : {
45 : : // proof should not be cyclic
46 : 4881120 : std::unordered_set<ProofNode*> visited;
47 : 2440560 : std::unordered_set<ProofNode*>::iterator it;
48 : 4881120 : std::vector<std::shared_ptr<ProofNode>> visit;
49 : 2440560 : std::shared_ptr<ProofNode> cur;
50 : 2440560 : visit.push_back(pn);
51 : 249891000 : do
52 : : {
53 : 252332000 : cur = visit.back();
54 : 252332000 : visit.pop_back();
55 : 252332000 : it = visited.find(cur.get());
56 : 252332000 : const std::vector<Node>& cargs = cur->getArguments();
57 [ + + ]: 252332000 : if (it == visited.end())
58 : : {
59 : 68611400 : visited.insert(cur.get());
60 : 68611400 : ProofRule id = cur->getRule();
61 [ + + ]: 68611400 : if (id == ProofRule::ASSUME)
62 : : {
63 [ - + ][ - + ]: 21669900 : Assert(cargs.size() == 1);
[ - - ]
64 : 43339800 : Node f = cargs[0];
65 : 21669900 : amap[f].push_back(cur);
66 : : }
67 : : else
68 : : {
69 : 46941500 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
70 [ + + ]: 46941500 : if (id == ProofRule::SCOPE)
71 : : {
72 : : // make a recursive call, which is bound in depth by the number of
73 : : // nested SCOPE (never expected to be more than 1 or 2).
74 : 1993760 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amapTmp;
75 : 996879 : expr::getFreeAssumptionsMap(cs[0], amapTmp);
76 : 5394390 : for (std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
77 [ + + ]: 11785700 : a : amapTmp)
78 : : {
79 [ + + ]: 5394390 : if (std::find(cargs.begin(), cargs.end(), a.first) == cargs.end())
80 : : {
81 : 603944 : std::vector<std::shared_ptr<ProofNode>>& pfs = amap[a.first];
82 : 603944 : pfs.insert(pfs.end(), a.second.begin(), a.second.end());
83 : : }
84 : : }
85 : 996879 : continue;
86 : : }
87 : : // traverse on children
88 : 45944600 : visit.insert(visit.end(), cs.begin(), cs.end());
89 : : }
90 : : }
91 [ + + ]: 252332000 : } while (!visit.empty());
92 : 2440560 : }
93 : :
94 : 0 : void getSubproofRule(std::shared_ptr<ProofNode> pn,
95 : : ProofRule r,
96 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
97 : : {
98 : 0 : std::unordered_set<ProofRule> rs{r};
99 : 0 : getSubproofRules(pn, rs, pfs);
100 : 0 : }
101 : :
102 : 5605 : void getSubproofRules(std::shared_ptr<ProofNode> pn,
103 : : std::unordered_set<ProofRule> rs,
104 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
105 : : {
106 : : // proof should not be cyclic
107 : 11210 : std::unordered_set<ProofNode*> visited;
108 : 5605 : std::unordered_set<ProofNode*>::iterator it;
109 : 11210 : std::vector<std::shared_ptr<ProofNode>> visit;
110 : 5605 : std::shared_ptr<ProofNode> cur;
111 : 5605 : visit.push_back(pn);
112 : 8267270 : do
113 : : {
114 : 8272870 : cur = visit.back();
115 : 8272870 : visit.pop_back();
116 : 8272870 : it = visited.find(cur.get());
117 [ + + ]: 8272870 : if (it == visited.end())
118 : : {
119 : 3555990 : visited.insert(cur.get());
120 [ + + ]: 3555990 : if (rs.find(cur->getRule()) != rs.end())
121 : : {
122 : 361101 : pfs.push_back(cur);
123 : : }
124 : : else
125 : : {
126 : 3194890 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
127 : : // traverse on children
128 : 3194890 : visit.insert(visit.end(), cs.begin(), cs.end());
129 : : }
130 : : }
131 [ + + ]: 8272870 : } while (!visit.empty());
132 : 5605 : }
133 : :
134 : 7261830 : bool containsAssumption(const ProofNode* pn,
135 : : std::unordered_map<const ProofNode*, bool>& caMap,
136 : : const std::unordered_set<Node>& allowed)
137 : : {
138 : 14523700 : std::unordered_map<const ProofNode*, bool> visited;
139 : 7261830 : std::unordered_map<const ProofNode*, bool>::iterator it;
140 : 7261830 : std::vector<const ProofNode*> visit;
141 : 7261830 : visit.push_back(pn);
142 : 7261830 : bool foundAssumption = false;
143 : : const ProofNode* cur;
144 [ + + ]: 37600700 : while (!visit.empty())
145 : : {
146 : 30338800 : cur = visit.back();
147 : 30338800 : visit.pop_back();
148 : : // have we already computed?
149 : 30338800 : it = caMap.find(cur);
150 [ + + ]: 30338800 : if (it != caMap.end())
151 : : {
152 : : // if cached, we set found assumption to true if applicable and continue
153 [ + + ]: 16725200 : if (it->second)
154 : : {
155 : 4387980 : foundAssumption = true;
156 : : }
157 : 16725200 : continue;
158 : : }
159 : 13613700 : it = visited.find(cur);
160 [ + + ]: 13613700 : if (it == visited.end())
161 : : {
162 : 7261830 : ProofRule r = cur->getRule();
163 [ + + ]: 7261830 : if (r == ProofRule::ASSUME)
164 : : {
165 : 909975 : bool ret = allowed.find(cur->getArguments()[0]) == allowed.end();
166 : 909975 : visited[cur] = ret;
167 : 909975 : caMap[cur] = ret;
168 : 909975 : foundAssumption = ret;
169 : : }
170 [ + - ]: 6351850 : else if (!foundAssumption)
171 : : {
172 : : // if we haven't found an assumption yet, recurse. Otherwise, we will
173 : : // not bother computing whether this subproof contains an assumption
174 : : // since we know its parent already contains one by another child.
175 : 6351850 : visited[cur] = false;
176 : 6351850 : visit.push_back(cur);
177 : : const std::vector<std::shared_ptr<ProofNode>>& children =
178 : 6351850 : cur->getChildren();
179 [ + + ]: 23077000 : for (const std::shared_ptr<ProofNode>& cp : children)
180 : : {
181 : 16725200 : visit.push_back(cp.get());
182 : : }
183 : : }
184 : : }
185 [ + - ]: 6351850 : else if (!it->second)
186 : : {
187 : 6351850 : visited[cur] = true;
188 : : // we contain an assumption if we've found an assumption in a child
189 : 6351850 : caMap[cur] = foundAssumption;
190 : : }
191 : : }
192 : 14523700 : return caMap[cur];
193 : : }
194 : 0 : bool containsAssumption(const ProofNode* pn,
195 : : std::unordered_map<const ProofNode*, bool>& caMap)
196 : : {
197 : 0 : std::unordered_set<Node> allowed;
198 : 0 : return containsAssumption(pn, caMap, allowed);
199 : : }
200 : :
201 : 0 : bool containsAssumption(const ProofNode* pn)
202 : : {
203 : 0 : std::unordered_map<const ProofNode*, bool> caMap;
204 : 0 : std::unordered_set<Node> allowed;
205 : 0 : return containsAssumption(pn, caMap, allowed);
206 : : }
207 : :
208 : 0 : bool containsSubproof(ProofNode* pn, ProofNode* pnc)
209 : : {
210 : 0 : std::unordered_set<const ProofNode*> visited;
211 : 0 : return containsSubproof(pn, pnc, visited);
212 : : }
213 : :
214 : 11547 : bool containsSubproof(ProofNode* pn,
215 : : ProofNode* pnc,
216 : : std::unordered_set<const ProofNode*>& visited)
217 : : {
218 : 11547 : std::unordered_map<const ProofNode*, bool>::iterator it;
219 : 23094 : std::vector<const ProofNode*> visit;
220 : 11547 : visit.push_back(pn);
221 : : const ProofNode* cur;
222 [ + + ]: 134164 : while (!visit.empty())
223 : : {
224 : 122617 : cur = visit.back();
225 : 122617 : visit.pop_back();
226 [ + + ]: 122617 : if (visited.find(cur) == visited.end())
227 : : {
228 : 108275 : visited.insert(cur);
229 [ - + ]: 108275 : if (cur == pnc)
230 : : {
231 : 0 : return true;
232 : : }
233 : : const std::vector<std::shared_ptr<ProofNode>>& children =
234 : 108275 : cur->getChildren();
235 [ + + ]: 219345 : for (const std::shared_ptr<ProofNode>& cp : children)
236 : : {
237 : 111070 : visit.push_back(cp.get());
238 : : }
239 : : }
240 : : }
241 : 11547 : return false;
242 : : }
243 : :
244 : 2373760 : ProofRule getCongRule(const Node& n, std::vector<Node>& args)
245 : : {
246 : 2373760 : Kind k = n.getKind();
247 : 2373760 : ProofRule r = ProofRule::CONG;
248 [ + + ][ + + ]: 2373760 : switch (k)
[ + ]
249 : : {
250 : 2680 : case Kind::DISTINCT: r = ProofRule::PAIRWISE_CONG; break;
251 : 484586 : case Kind::APPLY_UF:
252 : : case Kind::FLOATINGPOINT_LT:
253 : : case Kind::FLOATINGPOINT_LEQ:
254 : : case Kind::FLOATINGPOINT_GT:
255 : : case Kind::FLOATINGPOINT_GEQ:
256 : : case Kind::NULLABLE_LIFT:
257 : : case Kind::APPLY_INDEXED_SYMBOLIC:
258 : : // takes arbitrary but we use CONG
259 : 484586 : break;
260 : 979 : case Kind::HO_APPLY:
261 : : // Use HO_CONG, since HO_APPLY is encoded as native function application.
262 : : // This requires no arguments so we return.
263 : 979 : r = ProofRule::HO_CONG;
264 : 979 : break;
265 : 8913 : case Kind::APPLY_CONSTRUCTOR:
266 : : // tuples are n-ary, others are fixed
267 [ + + ]: 8913 : r = n.getType().isTuple() ? ProofRule::NARY_CONG : ProofRule::CONG;
268 : 8913 : break;
269 : 1876610 : default:
270 [ + + ]: 1876610 : if (NodeManager::isNAryKind(k))
271 : : {
272 : : // n-ary operators that are not handled as exceptions above use
273 : : // NARY_CONG
274 : 884912 : r = ProofRule::NARY_CONG;
275 : : }
276 : 1876610 : break;
277 : : }
278 [ + + ]: 2373760 : if (r != ProofRule::HO_CONG)
279 : : {
280 : 2372780 : args.push_back(n);
281 : : }
282 : 2373760 : return r;
283 : : }
284 : :
285 : 2352 : Node proveCong(Env& env,
286 : : CDProof* cdp,
287 : : const Node& n,
288 : : const std::vector<Node>& premises)
289 : : {
290 : 4704 : std::vector<Node> cpremises = premises;
291 : 4704 : std::vector<Node> cargs;
292 : 2352 : ProofRule cr = getCongRule(n, cargs);
293 : 2352 : cpremises.resize(n.getNumChildren());
294 : : // add REFL if a premise is not provided
295 [ + + ]: 81828 : for (size_t i = 0, npremises = cpremises.size(); i < npremises; i++)
296 : : {
297 [ + + ]: 79476 : if (cpremises[i].isNull())
298 : : {
299 : 231372 : Node refl = n[i].eqNode(n[i]);
300 : 154248 : cdp->addStep(refl, ProofRule::REFL, {}, {n[i]});
301 : 77124 : cpremises[i] = refl;
302 : : }
303 : : }
304 : 2352 : ProofChecker* pc = env.getProofNodeManager()->getChecker();
305 : 2352 : Node eq = pc->checkDebug(cr, cpremises, cargs);
306 [ + - ]: 2352 : if (!eq.isNull())
307 : : {
308 : 2352 : cdp->addStep(eq, cr, cpremises, cargs);
309 : : }
310 : 4704 : return eq;
311 : : }
312 : :
313 : : } // namespace expr
314 : : } // namespace cvc5::internal
|
