1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* Skolem definition manager. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "prop/skolem_def_manager.h" |
17 |
|
|
18 |
|
#include "expr/attribute.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace prop { |
22 |
|
|
23 |
10009 |
SkolemDefManager::SkolemDefManager(context::Context* context, |
24 |
10009 |
context::UserContext* userContext) |
25 |
10009 |
: d_skDefs(userContext), d_skActive(context) |
26 |
|
{ |
27 |
10009 |
} |
28 |
|
|
29 |
10006 |
SkolemDefManager::~SkolemDefManager() {} |
30 |
|
|
31 |
28444 |
void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def) |
32 |
|
{ |
33 |
|
// Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE |
34 |
56888 |
Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem |
35 |
28444 |
<< std::endl; |
36 |
|
// in very rare cases, a skolem may be generated twice for terms that are |
37 |
|
// equivalent up to purification |
38 |
28444 |
if (d_skDefs.find(skolem) == d_skDefs.end()) |
39 |
|
{ |
40 |
28438 |
d_skDefs.insert(skolem, def); |
41 |
|
} |
42 |
28444 |
} |
43 |
|
|
44 |
2431 |
TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const |
45 |
|
{ |
46 |
2431 |
NodeNodeMap::const_iterator it = d_skDefs.find(skolem); |
47 |
2431 |
Assert(it != d_skDefs.end()) << "No skolem def for " << skolem; |
48 |
2431 |
return it->second; |
49 |
|
} |
50 |
|
|
51 |
6793837 |
void SkolemDefManager::notifyAsserted(TNode literal, |
52 |
|
std::vector<TNode>& activatedSkolems, |
53 |
|
bool useDefs) |
54 |
|
{ |
55 |
13587674 |
std::unordered_set<Node> skolems; |
56 |
6793837 |
getSkolems(literal, skolems); |
57 |
10430195 |
for (const Node& k : skolems) |
58 |
|
{ |
59 |
3636358 |
if (d_skActive.find(k) != d_skActive.end()) |
60 |
|
{ |
61 |
|
// already active |
62 |
3271152 |
continue; |
63 |
|
} |
64 |
365206 |
d_skActive.insert(k); |
65 |
365206 |
if (useDefs) |
66 |
|
{ |
67 |
|
// add its definition to the activated list |
68 |
365206 |
NodeNodeMap::const_iterator it = d_skDefs.find(k); |
69 |
365206 |
Assert(it != d_skDefs.end()); |
70 |
365206 |
activatedSkolems.push_back(it->second); |
71 |
|
} |
72 |
|
else |
73 |
|
{ |
74 |
|
// add to the activated list |
75 |
|
activatedSkolems.push_back(k); |
76 |
|
} |
77 |
|
} |
78 |
6793837 |
} |
79 |
|
|
80 |
|
struct HasSkolemTag |
81 |
|
{ |
82 |
|
}; |
83 |
|
struct HasSkolemComputedTag |
84 |
|
{ |
85 |
|
}; |
86 |
|
/** Attribute true for nodes with skolems in them */ |
87 |
|
typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr; |
88 |
|
/** Attribute true for nodes where we have computed the above attribute */ |
89 |
|
typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr; |
90 |
|
|
91 |
19916662 |
bool SkolemDefManager::hasSkolems(TNode n) const |
92 |
|
{ |
93 |
39833324 |
std::unordered_set<TNode> visited; |
94 |
19916662 |
std::unordered_set<TNode>::iterator it; |
95 |
39833324 |
std::vector<TNode> visit; |
96 |
39833324 |
TNode cur; |
97 |
19916662 |
visit.push_back(n); |
98 |
2813559 |
do |
99 |
|
{ |
100 |
22730221 |
cur = visit.back(); |
101 |
43302626 |
if (cur.getAttribute(HasSkolemComputedAttr())) |
102 |
|
{ |
103 |
20572405 |
visit.pop_back(); |
104 |
|
// already computed |
105 |
20572405 |
continue; |
106 |
|
} |
107 |
2157816 |
it = visited.find(cur); |
108 |
2157816 |
if (it == visited.end()) |
109 |
|
{ |
110 |
1164251 |
visited.insert(cur); |
111 |
1164251 |
if (cur.getNumChildren() == 0) |
112 |
|
{ |
113 |
170686 |
visit.pop_back(); |
114 |
170686 |
bool hasSkolem = false; |
115 |
170686 |
if (cur.isVar()) |
116 |
|
{ |
117 |
126116 |
hasSkolem = (d_skDefs.find(cur) != d_skDefs.end()); |
118 |
|
} |
119 |
170686 |
cur.setAttribute(HasSkolemAttr(), hasSkolem); |
120 |
170686 |
cur.setAttribute(HasSkolemComputedAttr(), true); |
121 |
|
} |
122 |
|
else |
123 |
|
{ |
124 |
993565 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
125 |
|
} |
126 |
|
} |
127 |
|
else |
128 |
|
{ |
129 |
993565 |
visit.pop_back(); |
130 |
993565 |
bool hasSkolem = false; |
131 |
2599424 |
for (TNode i : cur) |
132 |
|
{ |
133 |
1744635 |
Assert(i.getAttribute(HasSkolemComputedAttr())); |
134 |
1744635 |
if (i.getAttribute(HasSkolemAttr())) |
135 |
|
{ |
136 |
138776 |
hasSkolem = true; |
137 |
138776 |
break; |
138 |
|
} |
139 |
|
} |
140 |
993565 |
cur.setAttribute(HasSkolemAttr(), hasSkolem); |
141 |
993565 |
cur.setAttribute(HasSkolemComputedAttr(), true); |
142 |
|
} |
143 |
22730221 |
} while (!visit.empty()); |
144 |
19916662 |
Assert(n.getAttribute(HasSkolemComputedAttr())); |
145 |
39833324 |
return n.getAttribute(HasSkolemAttr()); |
146 |
|
} |
147 |
|
|
148 |
6797154 |
void SkolemDefManager::getSkolems(TNode n, |
149 |
|
std::unordered_set<Node>& skolems) const |
150 |
|
{ |
151 |
13594308 |
std::unordered_set<TNode> visited; |
152 |
6797154 |
std::unordered_set<TNode>::iterator it; |
153 |
13594308 |
std::vector<TNode> visit; |
154 |
13594308 |
TNode cur; |
155 |
6797154 |
visit.push_back(n); |
156 |
13119508 |
do |
157 |
|
{ |
158 |
19916662 |
cur = visit.back(); |
159 |
19916662 |
visit.pop_back(); |
160 |
19916662 |
if (!hasSkolems(cur)) |
161 |
|
{ |
162 |
|
// does not have skolems, continue |
163 |
7883368 |
continue; |
164 |
|
} |
165 |
12033294 |
it = visited.find(cur); |
166 |
12033294 |
if (it == visited.end()) |
167 |
|
{ |
168 |
11616772 |
visited.insert(cur); |
169 |
11616772 |
if (cur.isVar()) |
170 |
|
{ |
171 |
3638789 |
if (d_skDefs.find(cur) != d_skDefs.end()) |
172 |
|
{ |
173 |
3638789 |
skolems.insert(cur); |
174 |
|
} |
175 |
|
} |
176 |
|
else |
177 |
|
{ |
178 |
7977983 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
179 |
|
} |
180 |
|
} |
181 |
19916662 |
} while (!visit.empty()); |
182 |
6797154 |
} |
183 |
|
|
184 |
|
} // namespace prop |
185 |
29577 |
} // namespace cvc5 |