1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Aina Niemetz |
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 |
|
* Implementation of utility for blocking models. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "smt/model_blocker.h" |
17 |
|
|
18 |
|
#include "expr/node.h" |
19 |
|
#include "expr/node_algorithm.h" |
20 |
|
#include "theory/quantifiers/term_util.h" |
21 |
|
#include "theory/rewriter.h" |
22 |
|
#include "theory/theory_model.h" |
23 |
|
|
24 |
|
using namespace cvc5::kind; |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
|
28 |
26 |
Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions, |
29 |
|
theory::TheoryModel* m, |
30 |
|
options::BlockModelsMode mode, |
31 |
|
const std::vector<Node>& exprToBlock) |
32 |
|
{ |
33 |
26 |
NodeManager* nm = NodeManager::currentNM(); |
34 |
|
// convert to nodes |
35 |
52 |
std::vector<Node> tlAsserts = assertions; |
36 |
52 |
std::vector<Node> nodesToBlock = exprToBlock; |
37 |
26 |
Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl; |
38 |
52 |
Node blocker; |
39 |
26 |
if (mode == options::BlockModelsMode::LITERALS) |
40 |
|
{ |
41 |
10 |
Assert(nodesToBlock.empty()); |
42 |
|
// optimization: filter out top-level unit assertions, as they cannot |
43 |
|
// contribute to model blocking. |
44 |
10 |
unsigned counter = 0; |
45 |
20 |
std::vector<Node> asserts; |
46 |
62 |
while (counter < tlAsserts.size()) |
47 |
|
{ |
48 |
52 |
Node cur = tlAsserts[counter]; |
49 |
26 |
counter++; |
50 |
52 |
Node catom = cur.getKind() == NOT ? cur[0] : cur; |
51 |
26 |
bool cpol = cur.getKind() != NOT; |
52 |
26 |
if (catom.getKind() == NOT) |
53 |
|
{ |
54 |
|
tlAsserts.push_back(catom[0]); |
55 |
|
} |
56 |
26 |
else if (catom.getKind() == AND && cpol) |
57 |
|
{ |
58 |
|
tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end()); |
59 |
|
} |
60 |
26 |
else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom)) |
61 |
|
{ |
62 |
10 |
asserts.push_back(cur); |
63 |
10 |
Trace("model-blocker") << " " << cur << std::endl; |
64 |
|
} |
65 |
|
} |
66 |
10 |
if (asserts.empty()) |
67 |
|
{ |
68 |
|
Node blockTriv = nm->mkConst(false); |
69 |
|
Trace("model-blocker") |
70 |
|
<< "...model blocker is (trivially) " << blockTriv << std::endl; |
71 |
|
return blockTriv; |
72 |
|
} |
73 |
|
|
74 |
20 |
Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0]; |
75 |
20 |
std::unordered_map<TNode, Node> visited; |
76 |
20 |
std::unordered_map<TNode, Node> implicant; |
77 |
10 |
std::unordered_map<TNode, Node>::iterator it; |
78 |
20 |
std::vector<TNode> visit; |
79 |
20 |
TNode cur; |
80 |
10 |
visit.push_back(formula); |
81 |
26 |
do |
82 |
|
{ |
83 |
36 |
cur = visit.back(); |
84 |
36 |
visit.pop_back(); |
85 |
36 |
it = visited.find(cur); |
86 |
|
|
87 |
36 |
Trace("model-blocker-debug") << "Visit : " << cur << std::endl; |
88 |
|
|
89 |
36 |
if (it == visited.end()) |
90 |
|
{ |
91 |
22 |
visited[cur] = Node::null(); |
92 |
44 |
Node catom = cur.getKind() == NOT ? cur[0] : cur; |
93 |
22 |
bool cpol = cur.getKind() != NOT; |
94 |
|
// compute the implicant |
95 |
|
// impl is a formula that implies cur that is also satisfied by m |
96 |
44 |
Node impl; |
97 |
22 |
if (catom.getKind() == NOT) |
98 |
|
{ |
99 |
|
// double negation |
100 |
|
impl = catom[0]; |
101 |
|
} |
102 |
22 |
else if (catom.getKind() == OR || catom.getKind() == AND) |
103 |
|
{ |
104 |
|
// if disjunctive |
105 |
10 |
if ((catom.getKind() == OR) == cpol) |
106 |
|
{ |
107 |
|
// take the first literal that is satisfied |
108 |
24 |
for (Node n : catom) |
109 |
|
{ |
110 |
|
// rewrite, this ensures that e.g. the propositional value of |
111 |
|
// quantified formulas can be queried |
112 |
24 |
n = theory::Rewriter::rewrite(n); |
113 |
40 |
Node vn = m->getValue(n); |
114 |
24 |
Assert(vn.isConst()); |
115 |
24 |
if (vn.getConst<bool>() == cpol) |
116 |
|
{ |
117 |
8 |
impl = cpol ? n : n.negate(); |
118 |
8 |
break; |
119 |
|
} |
120 |
|
} |
121 |
|
} |
122 |
2 |
else if (catom.getKind() == OR) |
123 |
|
{ |
124 |
|
// one step NNF |
125 |
|
std::vector<Node> children; |
126 |
|
for (const Node& cn : catom) |
127 |
|
{ |
128 |
|
children.push_back(cn.negate()); |
129 |
|
} |
130 |
|
impl = nm->mkNode(AND, children); |
131 |
|
} |
132 |
|
} |
133 |
12 |
else if (catom.getKind() == ITE) |
134 |
|
{ |
135 |
|
Node vcond = m->getValue(cur[0]); |
136 |
|
Assert(vcond.isConst()); |
137 |
|
Node cond = cur[0]; |
138 |
|
Node branch; |
139 |
|
if (vcond.getConst<bool>()) |
140 |
|
{ |
141 |
|
branch = cur[1]; |
142 |
|
} |
143 |
|
else |
144 |
|
{ |
145 |
|
cond = cond.negate(); |
146 |
|
branch = cur[2]; |
147 |
|
} |
148 |
|
impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate()); |
149 |
|
} |
150 |
34 |
else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean()) |
151 |
34 |
|| catom.getKind() == XOR) |
152 |
|
{ |
153 |
|
// based on how the children evaluate in the model |
154 |
4 |
std::vector<Node> children; |
155 |
6 |
for (const Node& cn : catom) |
156 |
|
{ |
157 |
8 |
Node vn = m->getValue(cn); |
158 |
4 |
Assert(vn.isConst()); |
159 |
4 |
children.push_back(vn.getConst<bool>() ? cn : cn.negate()); |
160 |
|
} |
161 |
2 |
impl = nm->mkNode(AND, children); |
162 |
|
} |
163 |
|
else |
164 |
|
{ |
165 |
|
// literals justified by themselves |
166 |
10 |
visited[cur] = cur; |
167 |
10 |
Trace("model-blocker-debug") << "...self justified" << std::endl; |
168 |
|
} |
169 |
22 |
if (visited[cur].isNull()) |
170 |
|
{ |
171 |
12 |
visit.push_back(cur); |
172 |
12 |
if (impl.isNull()) |
173 |
|
{ |
174 |
2 |
Assert(cur.getKind() == AND); |
175 |
2 |
Trace("model-blocker-debug") << "...recurse" << std::endl; |
176 |
2 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
177 |
|
} |
178 |
|
else |
179 |
|
{ |
180 |
20 |
Trace("model-blocker-debug") |
181 |
10 |
<< "...implicant : " << impl << std::endl; |
182 |
10 |
implicant[cur] = impl; |
183 |
10 |
visit.push_back(impl); |
184 |
|
} |
185 |
|
} |
186 |
|
} |
187 |
14 |
else if (it->second.isNull()) |
188 |
|
{ |
189 |
24 |
Node ret = cur; |
190 |
12 |
it = implicant.find(cur); |
191 |
12 |
if (it != implicant.end()) |
192 |
|
{ |
193 |
20 |
Node impl = it->second; |
194 |
10 |
it = visited.find(impl); |
195 |
10 |
Assert(it != visited.end()); |
196 |
10 |
Assert(!it->second.isNull()); |
197 |
10 |
ret = it->second; |
198 |
20 |
Trace("model-blocker-debug") |
199 |
10 |
<< "...implicant res: " << ret << std::endl; |
200 |
|
} |
201 |
|
else |
202 |
|
{ |
203 |
2 |
bool childChanged = false; |
204 |
4 |
std::vector<Node> children; |
205 |
|
// we never recurse to parameterized nodes |
206 |
2 |
Assert(cur.getMetaKind() != metakind::PARAMETERIZED); |
207 |
6 |
for (const Node& cn : cur) |
208 |
|
{ |
209 |
4 |
it = visited.find(cn); |
210 |
4 |
Assert(it != visited.end()); |
211 |
4 |
Assert(!it->second.isNull()); |
212 |
4 |
childChanged = childChanged || cn != it->second; |
213 |
4 |
children.push_back(it->second); |
214 |
|
} |
215 |
2 |
if (childChanged) |
216 |
|
{ |
217 |
|
ret = nm->mkNode(cur.getKind(), children); |
218 |
|
} |
219 |
2 |
Trace("model-blocker-debug") << "...recons res: " << ret << std::endl; |
220 |
|
} |
221 |
12 |
visited[cur] = ret; |
222 |
|
} |
223 |
36 |
} while (!visit.empty()); |
224 |
10 |
Assert(visited.find(formula) != visited.end()); |
225 |
10 |
Assert(!visited.find(formula)->second.isNull()); |
226 |
10 |
blocker = visited[formula].negate(); |
227 |
|
} |
228 |
|
else |
229 |
|
{ |
230 |
16 |
Assert(mode == options::BlockModelsMode::VALUES); |
231 |
32 |
std::vector<Node> blockers; |
232 |
|
// if specific terms were not specified, block all variables of |
233 |
|
// the model |
234 |
16 |
if (nodesToBlock.empty()) |
235 |
|
{ |
236 |
12 |
Trace("model-blocker") |
237 |
6 |
<< "no specific terms to block recognized" << std::endl; |
238 |
12 |
std::unordered_set<Node> symbols; |
239 |
33 |
for (Node n : tlAsserts) |
240 |
|
{ |
241 |
27 |
expr::getSymbols(n, symbols); |
242 |
|
} |
243 |
24 |
for (Node s : symbols) |
244 |
|
{ |
245 |
18 |
if (s.getType().getKind() != kind::FUNCTION_TYPE) |
246 |
|
{ |
247 |
24 |
Node v = m->getValue(s); |
248 |
24 |
Node a = nm->mkNode(DISTINCT, s, v); |
249 |
12 |
blockers.push_back(a); |
250 |
|
} |
251 |
|
} |
252 |
|
} |
253 |
|
// otherwise, block all terms that were specified in get-value |
254 |
|
else |
255 |
|
{ |
256 |
20 |
std::unordered_set<Node> terms; |
257 |
20 |
for (Node n : nodesToBlock) |
258 |
|
{ |
259 |
20 |
Node v = m->getValue(n); |
260 |
20 |
Node a = nm->mkNode(DISTINCT, n, v); |
261 |
10 |
blockers.push_back(a); |
262 |
|
} |
263 |
|
} |
264 |
16 |
if (blockers.size() == 0) |
265 |
|
{ |
266 |
|
blocker = nm->mkConst<bool>(true); |
267 |
|
} |
268 |
16 |
else if (blockers.size() == 1) |
269 |
|
{ |
270 |
10 |
blocker = blockers[0]; |
271 |
|
} |
272 |
|
else |
273 |
|
{ |
274 |
6 |
blocker = nm->mkNode(OR, blockers); |
275 |
|
} |
276 |
|
} |
277 |
26 |
Trace("model-blocker") << "...model blocker is " << blocker << std::endl; |
278 |
26 |
return blocker; |
279 |
|
} |
280 |
|
|
281 |
29337 |
} // namespace cvc5 |