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 : : * Implementation of proof node algorithm utilities.
11 : : */
12 : :
13 : : #include "proof/proof_node_algorithm.h"
14 : :
15 : : #include "proof/proof.h"
16 : : #include "proof/proof_checker.h"
17 : : #include "proof/proof_node.h"
18 : : #include "proof/proof_node_manager.h"
19 : : #include "proof/proof_rule_checker.h"
20 : : #include "theory/builtin/generic_op.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace expr {
24 : :
25 : 510424 : void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
26 : : {
27 : 510424 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
28 : : std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
29 : 510424 : pn->getRule(), pn->getChildren(), pn->getArguments());
30 : 510424 : getFreeAssumptionsMap(spn, amap);
31 : 510424 : for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
32 [ + + ]: 1672851 : amap)
33 : : {
34 : 652003 : assump.push_back(p.first);
35 : : }
36 : 510424 : }
37 : :
38 : 2826547 : void getFreeAssumptionsMap(
39 : : std::shared_ptr<ProofNode> pn,
40 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
41 : : {
42 : : // proof should not be cyclic
43 : 2826547 : std::unordered_set<ProofNode*> visited;
44 : 2826547 : std::unordered_set<ProofNode*>::iterator it;
45 : 2826547 : std::vector<std::shared_ptr<ProofNode>> visit;
46 : 2826547 : std::shared_ptr<ProofNode> cur;
47 : 2826547 : visit.push_back(pn);
48 : : do
49 : : {
50 : 177213869 : cur = visit.back();
51 : 177213869 : visit.pop_back();
52 : 177213869 : it = visited.find(cur.get());
53 : 177213869 : const std::vector<Node>& cargs = cur->getArguments();
54 [ + + ]: 177213869 : if (it == visited.end())
55 : : {
56 : 75272055 : visited.insert(cur.get());
57 : 75272055 : ProofRule id = cur->getRule();
58 [ + + ]: 75272055 : if (id == ProofRule::ASSUME)
59 : : {
60 [ - + ][ - + ]: 21386869 : Assert(cargs.size() == 1);
[ - - ]
61 : 21386869 : Node f = cargs[0];
62 : 21386869 : amap[f].push_back(cur);
63 : 21386869 : }
64 : : else
65 : : {
66 : 53885186 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
67 [ + + ]: 53885186 : if (id == ProofRule::SCOPE)
68 : : {
69 : : // make a recursive call, which is bound in depth by the number of
70 : : // nested SCOPE (never expected to be more than 1 or 2).
71 : 1222031 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amapTmp;
72 : 1222031 : expr::getFreeAssumptionsMap(cs[0], amapTmp);
73 : 1222031 : for (std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
74 [ + + ]: 9927708 : a : amapTmp)
75 : : {
76 [ + + ]: 7483646 : if (std::find(cargs.begin(), cargs.end(), a.first) == cargs.end())
77 : : {
78 : 670442 : std::vector<std::shared_ptr<ProofNode>>& pfs = amap[a.first];
79 : 670442 : pfs.insert(pfs.end(), a.second.begin(), a.second.end());
80 : : }
81 : : }
82 : 1222031 : continue;
83 : 1222031 : }
84 : : // traverse on children
85 : 52663155 : visit.insert(visit.end(), cs.begin(), cs.end());
86 : : }
87 : : }
88 [ + + ]: 177213869 : } while (!visit.empty());
89 : 2826547 : }
90 : :
91 : 0 : void getSubproofRule(std::shared_ptr<ProofNode> pn,
92 : : ProofRule r,
93 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
94 : : {
95 : 0 : std::unordered_set<ProofRule> rs{r};
96 : 0 : getSubproofRules(pn, rs, pfs);
97 : 0 : }
98 : :
99 : 6400 : void getSubproofRules(std::shared_ptr<ProofNode> pn,
100 : : std::unordered_set<ProofRule> rs,
101 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
102 : : {
103 : : // proof should not be cyclic
104 : 6400 : std::unordered_set<ProofNode*> visited;
105 : 6400 : std::unordered_set<ProofNode*>::iterator it;
106 : 6400 : std::vector<std::shared_ptr<ProofNode>> visit;
107 : 6400 : std::shared_ptr<ProofNode> cur;
108 : 6400 : visit.push_back(pn);
109 : : do
110 : : {
111 : 11730804 : cur = visit.back();
112 : 11730804 : visit.pop_back();
113 : 11730804 : it = visited.find(cur.get());
114 [ + + ]: 11730804 : if (it == visited.end())
115 : : {
116 : 5539066 : visited.insert(cur.get());
117 [ + + ]: 5539066 : if (rs.find(cur->getRule()) != rs.end())
118 : : {
119 : 526564 : pfs.push_back(cur);
120 : : }
121 : : else
122 : : {
123 : 5012502 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
124 : : // traverse on children
125 : 5012502 : visit.insert(visit.end(), cs.begin(), cs.end());
126 : : }
127 : : }
128 [ + + ]: 11730804 : } while (!visit.empty());
129 : 6400 : }
130 : :
131 : 8175140 : bool containsAssumption(const ProofNode* pn,
132 : : std::unordered_map<const ProofNode*, bool>& caMap,
133 : : const std::unordered_set<Node>& allowed)
134 : : {
135 : 8175140 : std::unordered_map<const ProofNode*, bool> visited;
136 : 8175140 : std::unordered_map<const ProofNode*, bool>::iterator it;
137 : 8175140 : std::vector<const ProofNode*> visit;
138 : 8175140 : visit.push_back(pn);
139 : 8175140 : bool foundAssumption = false;
140 : : const ProofNode* cur;
141 [ + + ]: 39057097 : while (!visit.empty())
142 : : {
143 : 30881957 : cur = visit.back();
144 : 30881957 : visit.pop_back();
145 : : // have we already computed?
146 : 30881957 : it = caMap.find(cur);
147 [ + + ]: 30881957 : if (it != caMap.end())
148 : : {
149 : : // if cached, we set found assumption to true if applicable and continue
150 [ + + ]: 15709529 : if (it->second)
151 : : {
152 : 4959112 : foundAssumption = true;
153 : : }
154 : 15709529 : continue;
155 : : }
156 : 15172428 : it = visited.find(cur);
157 [ + + ]: 15172428 : if (it == visited.end())
158 : : {
159 : 8175140 : ProofRule r = cur->getRule();
160 [ + + ]: 8175140 : if (r == ProofRule::ASSUME)
161 : : {
162 : 1177852 : bool ret = allowed.find(cur->getArguments()[0]) == allowed.end();
163 : 1177852 : visited[cur] = ret;
164 : 1177852 : caMap[cur] = ret;
165 : 1177852 : foundAssumption = ret;
166 : : }
167 [ + - ]: 6997288 : else if (!foundAssumption)
168 : : {
169 : : // if we haven't found an assumption yet, recurse. Otherwise, we will
170 : : // not bother computing whether this subproof contains an assumption
171 : : // since we know its parent already contains one by another child.
172 : 6997288 : visited[cur] = false;
173 : 6997288 : visit.push_back(cur);
174 : : const std::vector<std::shared_ptr<ProofNode>>& children =
175 : 6997288 : cur->getChildren();
176 [ + + ]: 22706817 : for (const std::shared_ptr<ProofNode>& cp : children)
177 : : {
178 : 15709529 : visit.push_back(cp.get());
179 : : }
180 : : }
181 : : }
182 [ + - ]: 6997288 : else if (!it->second)
183 : : {
184 : 6997288 : visited[cur] = true;
185 : : // we contain an assumption if we've found an assumption in a child
186 : 6997288 : caMap[cur] = foundAssumption;
187 : : }
188 : : }
189 : 16350280 : return caMap[cur];
190 : 8175140 : }
191 : 0 : bool containsAssumption(const ProofNode* pn,
192 : : std::unordered_map<const ProofNode*, bool>& caMap)
193 : : {
194 : 0 : std::unordered_set<Node> allowed;
195 : 0 : return containsAssumption(pn, caMap, allowed);
196 : 0 : }
197 : :
198 : 0 : bool containsAssumption(const ProofNode* pn)
199 : : {
200 : 0 : std::unordered_map<const ProofNode*, bool> caMap;
201 : 0 : std::unordered_set<Node> allowed;
202 : 0 : return containsAssumption(pn, caMap, allowed);
203 : 0 : }
204 : :
205 : 0 : bool containsSubproof(ProofNode* pn, ProofNode* pnc)
206 : : {
207 : 0 : std::unordered_set<const ProofNode*> visited;
208 : 0 : return containsSubproof(pn, pnc, visited);
209 : 0 : }
210 : :
211 : 14934 : bool containsSubproof(ProofNode* pn,
212 : : ProofNode* pnc,
213 : : std::unordered_set<const ProofNode*>& visited)
214 : : {
215 : 14934 : std::unordered_map<const ProofNode*, bool>::iterator it;
216 : 14934 : std::vector<const ProofNode*> visit;
217 : 14934 : visit.push_back(pn);
218 : : const ProofNode* cur;
219 [ + + ]: 265500 : while (!visit.empty())
220 : : {
221 : 250566 : cur = visit.back();
222 : 250566 : visit.pop_back();
223 [ + + ]: 250566 : if (visited.find(cur) == visited.end())
224 : : {
225 : 223209 : visited.insert(cur);
226 [ - + ]: 223209 : if (cur == pnc)
227 : : {
228 : 0 : return true;
229 : : }
230 : : const std::vector<std::shared_ptr<ProofNode>>& children =
231 : 223209 : cur->getChildren();
232 [ + + ]: 458841 : for (const std::shared_ptr<ProofNode>& cp : children)
233 : : {
234 : 235632 : visit.push_back(cp.get());
235 : : }
236 : : }
237 : : }
238 : 14934 : return false;
239 : 14934 : }
240 : :
241 : 2633760 : ProofRule getCongRule(const Node& n, std::vector<Node>& args)
242 : : {
243 : 2633760 : Kind k = n.getKind();
244 : 2633760 : ProofRule r = ProofRule::CONG;
245 [ + + ][ + + ]: 2633760 : switch (k)
[ + ]
246 : : {
247 : 2882 : case Kind::DISTINCT: r = ProofRule::PAIRWISE_CONG; break;
248 : 504392 : case Kind::APPLY_UF:
249 : : case Kind::FLOATINGPOINT_LT:
250 : : case Kind::FLOATINGPOINT_LEQ:
251 : : case Kind::FLOATINGPOINT_GT:
252 : : case Kind::FLOATINGPOINT_GEQ:
253 : : case Kind::NULLABLE_LIFT:
254 : : case Kind::APPLY_INDEXED_SYMBOLIC:
255 : : // takes arbitrary but we use CONG
256 : 504392 : break;
257 : 1070 : case Kind::HO_APPLY:
258 : : // Use HO_CONG, since HO_APPLY is encoded as native function application.
259 : : // This requires no arguments so we return.
260 : 1070 : r = ProofRule::HO_CONG;
261 : 1070 : break;
262 : 9093 : case Kind::APPLY_CONSTRUCTOR:
263 : : // tuples are n-ary, others are fixed
264 [ + + ]: 9093 : r = n.getType().isTuple() ? ProofRule::NARY_CONG : ProofRule::CONG;
265 : 9093 : break;
266 : 2116323 : default:
267 [ + + ]: 2116323 : if (NodeManager::isNAryKind(k))
268 : : {
269 : : // n-ary operators that are not handled as exceptions above use
270 : : // NARY_CONG
271 : 922974 : r = ProofRule::NARY_CONG;
272 : : }
273 : 2116323 : break;
274 : : }
275 [ + + ]: 2633760 : if (r != ProofRule::HO_CONG)
276 : : {
277 : 2632690 : args.push_back(n);
278 : : }
279 : 2633760 : return r;
280 : : }
281 : :
282 : 2686 : Node proveCong(Env& env,
283 : : CDProof* cdp,
284 : : const Node& n,
285 : : const std::vector<Node>& premises)
286 : : {
287 : 2686 : std::vector<Node> cpremises = premises;
288 : 2686 : std::vector<Node> cargs;
289 : 2686 : ProofRule cr = getCongRule(n, cargs);
290 : 2686 : cpremises.resize(n.getNumChildren());
291 : : // add REFL if a premise is not provided
292 [ + + ]: 83820 : for (size_t i = 0, npremises = cpremises.size(); i < npremises; i++)
293 : : {
294 [ + + ]: 81134 : if (cpremises[i].isNull())
295 : : {
296 : 156632 : Node refl = n[i].eqNode(n[i]);
297 : 156632 : cdp->addStep(refl, ProofRule::REFL, {}, {n[i]});
298 : 78316 : cpremises[i] = refl;
299 : 78316 : }
300 : : }
301 : 2686 : ProofChecker* pc = env.getProofNodeManager()->getChecker();
302 : 2686 : Node eq = pc->checkDebug(cr, cpremises, cargs);
303 [ + - ]: 2686 : if (!eq.isNull())
304 : : {
305 : 2686 : cdp->addStep(eq, cr, cpremises, cargs);
306 : : }
307 : 5372 : return eq;
308 : 2686 : }
309 : :
310 : : } // namespace expr
311 : : } // namespace cvc5::internal
|
