Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Hans-Joerg Schurr
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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_node.h"
19 : : #include "proof/proof_rule_checker.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace expr {
23 : :
24 : 382505 : void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
25 : : {
26 : 765010 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
27 : : std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
28 : 765010 : pn->getRule(), pn->getChildren(), pn->getArguments());
29 : 382505 : getFreeAssumptionsMap(spn, amap);
30 : 768015 : for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
31 [ + + ]: 1918540 : amap)
32 : : {
33 : 768015 : assump.push_back(p.first);
34 : : }
35 : 382505 : }
36 : :
37 : 2392270 : void getFreeAssumptionsMap(
38 : : std::shared_ptr<ProofNode> pn,
39 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
40 : : {
41 : : // proof should not be cyclic
42 : 4784550 : std::unordered_set<ProofNode*> visited;
43 : 2392270 : std::unordered_set<ProofNode*>::iterator it;
44 : 4784550 : std::vector<std::shared_ptr<ProofNode>> visit;
45 : 2392270 : std::shared_ptr<ProofNode> cur;
46 : 2392270 : visit.push_back(pn);
47 : 174166000 : do
48 : : {
49 : 176558000 : cur = visit.back();
50 : 176558000 : visit.pop_back();
51 : 176558000 : it = visited.find(cur.get());
52 : 176558000 : const std::vector<Node>& cargs = cur->getArguments();
53 [ + + ]: 176558000 : if (it == visited.end())
54 : : {
55 : 66738200 : visited.insert(cur.get());
56 : 66738200 : ProofRule id = cur->getRule();
57 [ + + ]: 66738200 : if (id == ProofRule::ASSUME)
58 : : {
59 [ - + ][ - + ]: 17062600 : Assert(cargs.size() == 1);
[ - - ]
60 : 34125100 : Node f = cargs[0];
61 : 17062600 : amap[f].push_back(cur);
62 : : }
63 : : else
64 : : {
65 : 49675600 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
66 [ + + ]: 49675600 : if (id == ProofRule::SCOPE)
67 : : {
68 : : // make a recursive call, which is bound in depth by the number of
69 : : // nested SCOPE (never expected to be more than 1 or 2).
70 : 1857370 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amapTmp;
71 : 928686 : expr::getFreeAssumptionsMap(cs[0], amapTmp);
72 : 4440640 : for (std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
73 [ + + ]: 9809980 : a : amapTmp)
74 : : {
75 [ + + ]: 4440640 : if (std::find(cargs.begin(), cargs.end(), a.first) == cargs.end())
76 : : {
77 : 1036640 : std::vector<std::shared_ptr<ProofNode>>& pfs = amap[a.first];
78 : 1036640 : pfs.insert(pfs.end(), a.second.begin(), a.second.end());
79 : : }
80 : : }
81 : 928686 : continue;
82 : : }
83 : : // traverse on children
84 : 48746900 : visit.insert(visit.end(), cs.begin(), cs.end());
85 : : }
86 : : }
87 [ + + ]: 176558000 : } while (!visit.empty());
88 : 2392270 : }
89 : :
90 : 2334 : void getSubproofRule(std::shared_ptr<ProofNode> pn,
91 : : ProofRule r,
92 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
93 : : {
94 : 2334 : std::unordered_set<ProofRule> rs{r};
95 : 2334 : getSubproofRules(pn, rs, pfs);
96 : 2334 : }
97 : :
98 : 2340 : void getSubproofRules(std::shared_ptr<ProofNode> pn,
99 : : std::unordered_set<ProofRule> rs,
100 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
101 : : {
102 : : // proof should not be cyclic
103 : 4680 : std::unordered_set<ProofNode*> visited;
104 : 2340 : std::unordered_set<ProofNode*>::iterator it;
105 : 4680 : std::vector<std::shared_ptr<ProofNode>> visit;
106 : 2340 : std::shared_ptr<ProofNode> cur;
107 : 2340 : visit.push_back(pn);
108 : 14735 : do
109 : : {
110 : 17075 : cur = visit.back();
111 : 17075 : visit.pop_back();
112 : 17075 : it = visited.find(cur.get());
113 [ + + ]: 17075 : if (it == visited.end())
114 : : {
115 : 17024 : visited.insert(cur.get());
116 [ + + ]: 17024 : if (rs.find(cur->getRule()) != rs.end())
117 : : {
118 : 3025 : pfs.push_back(cur);
119 : : }
120 : : else
121 : : {
122 : 13999 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
123 : : // traverse on children
124 : 13999 : visit.insert(visit.end(), cs.begin(), cs.end());
125 : : }
126 : : }
127 [ + + ]: 17075 : } while (!visit.empty());
128 : 2340 : }
129 : :
130 : 8295940 : bool containsAssumption(const ProofNode* pn,
131 : : std::unordered_map<const ProofNode*, bool>& caMap,
132 : : const std::unordered_set<Node>& allowed)
133 : : {
134 : 16591900 : std::unordered_map<const ProofNode*, bool> visited;
135 : 8295940 : std::unordered_map<const ProofNode*, bool>::iterator it;
136 : 8295940 : std::vector<const ProofNode*> visit;
137 : 8295940 : visit.push_back(pn);
138 : 8295940 : bool foundAssumption = false;
139 : : const ProofNode* cur;
140 [ + + ]: 41902200 : while (!visit.empty())
141 : : {
142 : 33606200 : cur = visit.back();
143 : 33606200 : visit.pop_back();
144 : : // have we already computed?
145 : 33606200 : it = caMap.find(cur);
146 [ + + ]: 33606200 : if (it != caMap.end())
147 : : {
148 : : // if cached, we set found assumption to true if applicable and continue
149 [ + + ]: 17043400 : if (it->second)
150 : : {
151 : 4985250 : foundAssumption = true;
152 : : }
153 : 17043400 : continue;
154 : : }
155 : 16562800 : it = visited.find(cur);
156 [ + + ]: 16562800 : if (it == visited.end())
157 : : {
158 : 8636600 : ProofRule r = cur->getRule();
159 [ + + ]: 8636600 : if (r == ProofRule::ASSUME)
160 : : {
161 : 710054 : bool ret = allowed.find(cur->getArguments()[0]) == allowed.end();
162 : 710054 : visited[cur] = ret;
163 : 710054 : caMap[cur] = ret;
164 : 710054 : foundAssumption = ret;
165 : : }
166 [ + + ]: 7926540 : else if (!foundAssumption)
167 : : {
168 : : // if we haven't found an assumption yet, recurse. Otherwise, we will
169 : : // not bother computing whether this subproof contains an assumption
170 : : // since we know its parent already contains one by another child.
171 : 7926240 : visited[cur] = false;
172 : 7926240 : visit.push_back(cur);
173 : : const std::vector<std::shared_ptr<ProofNode>>& children =
174 : 7926240 : cur->getChildren();
175 [ + + ]: 25310300 : for (const std::shared_ptr<ProofNode>& cp : children)
176 : : {
177 : 17384000 : visit.push_back(cp.get());
178 : : }
179 : : }
180 : : }
181 [ + - ]: 7926240 : else if (!it->second)
182 : : {
183 : 7926240 : visited[cur] = true;
184 : : // we contain an assumption if we've found an assumption in a child
185 : 7926240 : caMap[cur] = foundAssumption;
186 : : }
187 : : }
188 : 16591900 : return caMap[cur];
189 : : }
190 : 0 : bool containsAssumption(const ProofNode* pn,
191 : : std::unordered_map<const ProofNode*, bool>& caMap)
192 : : {
193 : 0 : std::unordered_set<Node> allowed;
194 : 0 : return containsAssumption(pn, caMap, allowed);
195 : : }
196 : :
197 : 0 : bool containsAssumption(const ProofNode* pn)
198 : : {
199 : 0 : std::unordered_map<const ProofNode*, bool> caMap;
200 : 0 : std::unordered_set<Node> allowed;
201 : 0 : return containsAssumption(pn, caMap, allowed);
202 : : }
203 : :
204 : 0 : bool containsSubproof(ProofNode* pn, ProofNode* pnc)
205 : : {
206 : 0 : std::unordered_set<const ProofNode*> visited;
207 : 0 : return containsSubproof(pn, pnc, visited);
208 : : }
209 : :
210 : 10486 : bool containsSubproof(ProofNode* pn,
211 : : ProofNode* pnc,
212 : : std::unordered_set<const ProofNode*>& visited)
213 : : {
214 : 10486 : std::unordered_map<const ProofNode*, bool>::iterator it;
215 : 20972 : std::vector<const ProofNode*> visit;
216 : 10486 : visit.push_back(pn);
217 : : const ProofNode* cur;
218 [ + + ]: 313355 : while (!visit.empty())
219 : : {
220 : 302869 : cur = visit.back();
221 : 302869 : visit.pop_back();
222 [ + + ]: 302869 : if (visited.find(cur) == visited.end())
223 : : {
224 : 263487 : visited.insert(cur);
225 [ - + ]: 263487 : if (cur == pnc)
226 : : {
227 : 0 : return true;
228 : : }
229 : : const std::vector<std::shared_ptr<ProofNode>>& children =
230 : 263487 : cur->getChildren();
231 [ + + ]: 555870 : for (const std::shared_ptr<ProofNode>& cp : children)
232 : : {
233 : 292383 : visit.push_back(cp.get());
234 : : }
235 : : }
236 : : }
237 : 10486 : return false;
238 : : }
239 : :
240 : 1962610 : ProofRule getCongRule(const Node& n, std::vector<Node>& args)
241 : : {
242 : 1962610 : Kind k = n.getKind();
243 : 1962610 : ProofRule r = ProofRule::CONG;
244 [ + + ][ + + ]: 1962610 : switch (k)
245 : : {
246 : 604686 : case Kind::APPLY_UF:
247 : : case Kind::DISTINCT:
248 : : case Kind::FLOATINGPOINT_LT:
249 : : case Kind::FLOATINGPOINT_LEQ:
250 : : case Kind::FLOATINGPOINT_GT:
251 : : case Kind::FLOATINGPOINT_GEQ:
252 : : case Kind::NULLABLE_LIFT:
253 : : case Kind::APPLY_INDEXED_SYMBOLIC:
254 : : // takes arbitrary but we use CONG
255 : 604686 : break;
256 : 1048 : case Kind::HO_APPLY:
257 : : // Use HO_CONG, since HO_APPLY is encoded as native function application.
258 : : // This requires no arguments so we return.
259 : 1048 : r = ProofRule::HO_CONG;
260 : 1048 : break;
261 : 7357 : case Kind::APPLY_CONSTRUCTOR:
262 : : // tuples are n-ary, others are fixed
263 [ + + ]: 7357 : r = n.getType().isTuple() ? ProofRule::NARY_CONG : ProofRule::CONG;
264 : 7357 : break;
265 : 1349520 : default:
266 [ + + ]: 1349520 : if (NodeManager::isNAryKind(k))
267 : : {
268 : : // n-ary operators that are not handled as exceptions above use
269 : : // NARY_CONG
270 : 462876 : r = ProofRule::NARY_CONG;
271 : : }
272 : 1349520 : break;
273 : : }
274 : : // Add the arguments
275 : 1962610 : args.push_back(ProofRuleChecker::mkKindNode(k));
276 [ + + ]: 1962610 : if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
277 : : {
278 : 649936 : args.push_back(n.getOperator());
279 : : }
280 [ + + ]: 1312670 : else if (n.isClosure())
281 : : {
282 : : // bound variable list is an argument for closure over congruence
283 : 16173 : args.push_back(n[0]);
284 : : }
285 : 1962610 : return r;
286 : : }
287 : :
288 : : } // namespace expr
289 : : } // namespace cvc5::internal
|
