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 utility for blocking models.
11 : : */
12 : :
13 : : #include "smt/model_blocker.h"
14 : :
15 : : #include "base/modal_exception.h"
16 : : #include "expr/node.h"
17 : : #include "expr/node_algorithm.h"
18 : : #include "expr/non_closed_node_converter.h"
19 : : #include "expr/subs.h"
20 : : #include "options/base_options.h"
21 : : #include "theory/logic_info.h"
22 : : #include "theory/quantifiers/term_util.h"
23 : : #include "theory/rewriter.h"
24 : : #include "theory/theory_model.h"
25 : :
26 : : using namespace cvc5::internal::kind;
27 : :
28 : : namespace cvc5::internal {
29 : :
30 : 52 : ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {}
31 : :
32 : 52 : Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
33 : : theory::TheoryModel* m,
34 : : modes::BlockModelsMode mode,
35 : : const std::vector<Node>& exprToBlock)
36 : : {
37 : 52 : NodeManager* nm = nodeManager();
38 : : // convert to nodes
39 : 52 : std::vector<Node> tlAsserts = assertions;
40 : 52 : std::vector<Node> nodesToBlock = exprToBlock;
41 [ + - ]: 52 : Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
42 : : // the list of literals that should be blocked
43 : 52 : std::unordered_set<Node> blockers;
44 : : // a subset of the above vector that holds on top level
45 : 52 : std::unordered_set<Node> blockersTriv;
46 [ + + ]: 52 : if (mode == modes::BlockModelsMode::LITERALS)
47 : : {
48 [ - + ][ - + ]: 20 : Assert(nodesToBlock.empty());
[ - - ]
49 : : // optimization: filter out top-level unit assertions, as they cannot
50 : : // contribute to model blocking.
51 : 20 : unsigned counter = 0;
52 : 20 : std::vector<Node> asserts;
53 [ + + ]: 59 : while (counter < tlAsserts.size())
54 : : {
55 : 39 : Node cur = tlAsserts[counter];
56 : 39 : counter++;
57 [ + + ]: 39 : Node catom = cur.getKind() == Kind::NOT ? cur[0] : cur;
58 : 39 : bool cpol = cur.getKind() != Kind::NOT;
59 [ - + ]: 39 : if (catom.getKind() == Kind::NOT)
60 : : {
61 : 0 : tlAsserts.push_back(catom[0]);
62 : : }
63 [ + + ][ - + ]: 39 : else if (catom.getKind() == Kind::AND && cpol)
[ - + ]
64 : : {
65 : 0 : tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end());
66 : : }
67 [ + + ]: 39 : else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
68 : : {
69 : 18 : asserts.push_back(cur);
70 [ + - ]: 18 : Trace("model-blocker") << " " << cur << std::endl;
71 : : }
72 : : else
73 : : {
74 : : // otherwise store that the blocker is trivial
75 : 21 : blockersTriv.insert(cur);
76 : 21 : blockers.insert(cur);
77 : : }
78 : 39 : }
79 : 20 : std::unordered_set<Node> visited;
80 : 20 : std::unordered_set<Node>::iterator it;
81 : 20 : std::vector<Node> visit;
82 : 20 : visit.insert(visit.end(), asserts.begin(), asserts.end());
83 : 20 : Node cur;
84 [ + + ]: 59 : while (!visit.empty())
85 : : {
86 : 39 : cur = visit.back();
87 : 39 : visit.pop_back();
88 : 39 : it = visited.find(cur);
89 : :
90 [ + - ]: 39 : Trace("model-blocker-debug") << "Visit : " << cur << std::endl;
91 : :
92 [ + + ]: 39 : if (it == visited.end())
93 : : {
94 : 36 : visited.insert(cur);
95 [ + + ]: 36 : Node catom = cur.getKind() == Kind::NOT ? cur[0] : cur;
96 : 36 : bool cpol = cur.getKind() != Kind::NOT;
97 : : // compute the implicant
98 : : // impl is a formula that implies cur that is also satisfied by m
99 : 36 : Node impl;
100 [ - + ]: 36 : if (catom.getKind() == Kind::NOT)
101 : : {
102 : : // double negation
103 : 0 : impl = catom[0];
104 : : }
105 [ + + ][ + + ]: 36 : else if (catom.getKind() == Kind::OR || catom.getKind() == Kind::AND)
[ + + ]
106 : : {
107 : : // if disjunctive
108 [ + - ]: 12 : if ((catom.getKind() == Kind::OR) == cpol)
109 : : {
110 : : // take the first literal that is satisfied
111 [ + + ]: 32 : for (const Node& n : catom)
112 : : {
113 : : // rewrite, this ensures that e.g. the propositional value of
114 : : // quantified formulas can be queried
115 : 31 : Node nr = rewrite(n);
116 : 31 : Node vn = m->getValue(nr);
117 [ + + ][ + + ]: 31 : if (vn.isConst() && vn.getConst<bool>() == cpol)
[ + + ]
118 : : {
119 [ + + ]: 11 : impl = cpol ? nr : nr.negate();
120 : 11 : break;
121 : : }
122 [ + + ][ + + ]: 53 : }
[ + + ]
123 [ + + ]: 12 : if (impl.isNull())
124 : : {
125 : : // unknown value, take self
126 : 1 : blockers.insert(cur);
127 : : }
128 : : }
129 [ - - ]: 0 : else if (catom.getKind() == Kind::OR)
130 : : {
131 : : // one step NNF
132 : 0 : std::vector<Node> children;
133 [ - - ]: 0 : for (const Node& cn : catom)
134 : : {
135 : 0 : children.push_back(cn.negate());
136 : 0 : }
137 : 0 : impl = nm->mkNode(Kind::AND, children);
138 : 0 : }
139 : : else
140 : : {
141 : : // otherwise a positive AND, recurse on this below
142 : 0 : impl = cur;
143 : : }
144 : : }
145 [ + + ]: 24 : else if (catom.getKind() == Kind::ITE)
146 : : {
147 : 8 : Node vcond = m->getValue(catom[0]);
148 [ + + ]: 4 : if (vcond.isConst())
149 : : {
150 : 3 : Node cond = catom[0];
151 : 3 : Node branch;
152 [ + + ]: 3 : if (vcond.getConst<bool>())
153 : : {
154 : 1 : branch = catom[1];
155 : : }
156 : : else
157 : : {
158 : 2 : cond = cond.negate();
159 : 2 : branch = catom[2];
160 : : }
161 [ + + ]: 3 : impl = nm->mkNode(Kind::AND, cond, cpol ? branch : branch.negate());
162 : 3 : }
163 : : else
164 : : {
165 : : // unknown value, take self
166 : 1 : blockers.insert(cur);
167 : : }
168 : 4 : }
169 : 60 : else if ((catom.getKind() == Kind::EQUAL
170 : 35 : && catom[0].getType().isBoolean())
171 [ + + ][ - + ]: 35 : || catom.getKind() == Kind::XOR)
[ + + ]
172 : : {
173 : : // based on how the children evaluate in the model
174 : 3 : std::vector<Node> children;
175 : 3 : bool success = true;
176 [ + + ]: 7 : for (const Node& cn : catom)
177 : : {
178 : 5 : Node vn = m->getValue(cn);
179 [ + + ]: 5 : if (!vn.isConst())
180 : : {
181 : 1 : success = false;
182 : 1 : break;
183 : : }
184 [ - + ]: 4 : children.push_back(vn.getConst<bool>() ? cn : cn.negate());
185 [ + + ][ + + ]: 6 : }
186 [ + + ]: 3 : if (success)
187 : : {
188 : 2 : impl = nm->mkNode(Kind::AND, children);
189 : : }
190 : : else
191 : : {
192 : : // unknown value, take self
193 : 1 : blockers.insert(cur);
194 : : }
195 : 3 : }
196 : : else
197 : : {
198 : : // literals justified by themselves
199 : 17 : blockers.insert(cur);
200 [ + - ]: 17 : Trace("model-blocker-debug") << "...self justified" << std::endl;
201 : : }
202 [ + + ]: 36 : if (!impl.isNull())
203 : : {
204 [ + + ]: 16 : if (impl.getKind() == Kind::AND)
205 : : {
206 [ + - ]: 5 : Trace("model-blocker-debug") << "...recurse" << std::endl;
207 : 5 : visit.insert(visit.end(), impl.begin(), impl.end());
208 : : }
209 : : else
210 : : {
211 : 11 : visit.emplace_back(impl);
212 : : }
213 : : }
214 : 36 : }
215 : : }
216 : 20 : }
217 : : else
218 : : {
219 [ - + ][ - + ]: 32 : Assert(mode == modes::BlockModelsMode::VALUES);
[ - - ]
220 : : // if specific terms were not specified, block all variables of
221 : : // the model
222 [ + + ]: 32 : if (nodesToBlock.empty())
223 : : {
224 [ + - ]: 20 : Trace("model-blocker")
225 : 10 : << "no specific terms to block recognized" << std::endl;
226 : 10 : std::unordered_set<Node> symbols;
227 [ + + ]: 45 : for (Node n : tlAsserts)
228 : : {
229 : 35 : expr::getSymbols(n, symbols);
230 : 35 : }
231 [ + + ]: 40 : for (Node s : symbols)
232 : : {
233 [ + + ]: 30 : if (!s.getType().isFirstClass())
234 : : {
235 : : // ignore e.g. constructors
236 : 4 : continue;
237 : : }
238 : 26 : if (!logicInfo().isHigherOrder()
239 [ + - ][ + + ]: 52 : && s.getType().getKind() == Kind::FUNCTION_TYPE)
[ + - ][ + + ]
[ - - ]
240 : : {
241 : : // ignore functions if not higher-order
242 : 10 : continue;
243 : : }
244 : 16 : nodesToBlock.push_back(s);
245 [ + + ]: 30 : }
246 : 10 : }
247 : : // otherwise, block all terms that were specified in get-value
248 : 32 : std::map<TypeNode, std::vector<Node> > allEnum;
249 : 32 : std::unordered_set<TypeNode> nonClosedType;
250 : 32 : std::map<Node, Node> nonClosedValue;
251 : 32 : std::unordered_set<Node> terms;
252 [ + + ]: 92 : for (const Node& n : nodesToBlock)
253 : : {
254 : 60 : Node v = m->getValue(n);
255 : 60 : TypeNode tn = n.getType();
256 : 60 : allEnum[tn].push_back(n);
257 [ + + ]: 60 : if (NonClosedNodeConverter::isClosed(d_env, v))
258 : : {
259 : : // if its value is closed, then we can block its value
260 : 50 : Node a = n.eqNode(v);
261 : 50 : blockers.insert(a);
262 : 50 : }
263 : : else
264 : : {
265 : : // otherwise we will block (dis)equality with other variables of its
266 : : // type below
267 : 10 : nonClosedValue[n] = v;
268 : : // remember this type has at least one non-closed value
269 : 10 : nonClosedType.insert(tn);
270 : : }
271 : 60 : }
272 : 32 : std::map<Node, Node>::iterator itn;
273 [ + + ]: 42 : for (const TypeNode& tn : nonClosedType)
274 : : {
275 : 10 : const std::vector<Node>& enums = allEnum[tn];
276 : 10 : size_t nenum = enums.size();
277 [ + + ]: 20 : for (size_t i = 0; i < nenum; i++)
278 : : {
279 : 10 : itn = nonClosedValue.find(enums[i]);
280 [ - + ]: 10 : if (itn == nonClosedValue.end())
281 : : {
282 : : // closed value, already blocked its value above
283 : 0 : continue;
284 : : }
285 : : // Given x that has a non-closed value, the following loop adds
286 : : // blockers of the form x != y or x = y, depending on whether y
287 : : // has the same value as x in the current model, for all other
288 : : // variables y of the same type as x. We do this even
289 : : // if y has a closed value in the model.
290 : 10 : Node vi = itn->second;
291 [ + + ]: 20 : for (size_t j = 0; j < nenum; j++)
292 : : {
293 [ + - ]: 10 : if (i == j)
294 : : {
295 : 10 : continue;
296 : : }
297 : 0 : Node vj = enums[j];
298 : 0 : itn = nonClosedValue.find(enums[j]);
299 [ - - ]: 0 : if (itn != nonClosedValue.end())
300 : : {
301 [ - - ]: 0 : if (j < i)
302 : : {
303 : : // already processed reverse
304 : 0 : continue;
305 : : }
306 : 0 : vj = itn->second;
307 : : }
308 : : // ...otherwise, we are comparing a non-closed and closed value, we
309 : : // assume these are disequal and leave vj unchanged.
310 : 0 : Node eq = enums[i].eqNode(enums[j]);
311 [ - - ]: 0 : if (vi != vj)
312 : : {
313 : 0 : eq = eq.notNode();
314 : : }
315 : 0 : blockers.insert(eq);
316 [ - - ]: 0 : }
317 : 10 : }
318 : : }
319 : 32 : }
320 : : // minimize, if in literals mode
321 : 52 : bool minBlocker = (mode == modes::BlockModelsMode::LITERALS);
322 [ + + ]: 52 : if (minBlocker)
323 : : {
324 : 20 : Subs s;
325 : 20 : std::vector<Node> possible;
326 : 20 : std::vector<Node> bvec(blockers.begin(), blockers.end());
327 : 20 : blockers.clear();
328 [ + + ]: 61 : for (const Node& a : bvec)
329 : : {
330 [ + + ]: 41 : if (a.getKind() == Kind::EQUAL)
331 : : {
332 : : // if it is an equality between a variable, turn into a substitution,
333 : : // which will help prune below.
334 : 11 : Node as = s.apply(a);
335 [ + + ]: 33 : for (size_t i = 0; i < 2; i++)
336 : : {
337 : 22 : if (as[i].isVar() && !expr::hasSubterm(as[1 - i], as[i]))
338 : : {
339 : 10 : s.add(as[i], as[1 - i]);
340 : : // this equality is definitely relevant
341 : 10 : blockers.insert(a);
342 : 10 : continue;
343 : : }
344 : : }
345 : 11 : }
346 : : // otherwise, it may be relevant below
347 : 41 : possible.push_back(a);
348 : : }
349 : : // do not add blockers that are implied by the substitution
350 [ + + ]: 61 : for (const Node& a : possible)
351 : : {
352 : 82 : Node as = rewrite(s.apply(a));
353 [ + + ]: 41 : if (as.isConst())
354 : : {
355 : 35 : continue;
356 : : }
357 : 6 : blockers.insert(a);
358 [ + + ]: 41 : }
359 : 20 : }
360 [ + + ]: 52 : if (isOutputOn(OutputTag::BLOCK_MODEL))
361 : : {
362 : 2 : std::vector<Node> bvec(blockers.begin(), blockers.end());
363 : 2 : Node bu = nm->mkAnd(bvec);
364 : 2 : output(OutputTag::BLOCK_MODEL) << "(block-model " << bu << ")" << std::endl;
365 : 2 : }
366 : : // go back and erase the trivial blockers
367 [ + + ]: 73 : for (const Node& bt : blockersTriv)
368 : : {
369 : 21 : blockers.erase(bt);
370 : : }
371 : 52 : std::vector<Node> bvec(blockers.begin(), blockers.end());
372 : 52 : Node blocker = nm->mkAnd(bvec).notNode();
373 [ + - ]: 52 : Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
374 : 104 : return blocker;
375 : 52 : }
376 : :
377 : : } // namespace cvc5::internal
|
