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 : : * Bounded integers module
11 : : *
12 : : * This class manages integer bounds for quantifiers.
13 : : */
14 : :
15 : : #include "theory/quantifiers/fmf/bounded_integers.h"
16 : :
17 : : #include "expr/dtype_cons.h"
18 : : #include "expr/emptyset.h"
19 : : #include "expr/node_algorithm.h"
20 : : #include "expr/skolem_manager.h"
21 : : #include "options/datatypes_options.h"
22 : : #include "options/quantifiers_options.h"
23 : : #include "theory/arith/arith_msum.h"
24 : : #include "theory/datatypes/theory_datatypes_utils.h"
25 : : #include "theory/decision_manager.h"
26 : : #include "theory/quantifiers/first_order_model.h"
27 : : #include "theory/quantifiers/fmf/model_engine.h"
28 : : #include "theory/quantifiers/term_enumeration.h"
29 : : #include "theory/quantifiers/term_util.h"
30 : : #include "theory/rep_set_iterator.h"
31 : : #include "theory/rewriter.h"
32 : : #include "theory/sets/normal_form.h"
33 : : #include "util/rational.h"
34 : :
35 : : using namespace cvc5::internal::kind;
36 : :
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : : namespace quantifiers {
40 : :
41 : 1130 : BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
42 : 1130 : Env& env, Node r, Valuation valuation, bool isProxy)
43 : : : DecisionStrategyFmf(env, valuation),
44 : 1130 : d_range(r),
45 : 1130 : d_ranges_proxied(userContext())
46 : : {
47 : : // we require a proxy if the term is set.card
48 [ + + ][ + + ]: 1130 : if (options().quantifiers.fmfBoundLazy || r.getKind() == Kind::SET_CARD)
[ + + ]
49 : : {
50 : : d_proxy_range =
51 : 64 : isProxy ? r : NodeManager::mkDummySkolem("pbir", r.getType());
52 : : }
53 : : else
54 : : {
55 : 1066 : d_proxy_range = r;
56 : : }
57 [ + + ]: 1130 : if (!isProxy)
58 : : {
59 [ + - ]: 2006 : Trace("bound-int") << "Introduce proxy " << d_proxy_range << " for "
60 : 1003 : << d_range << std::endl;
61 : : }
62 : 1130 : }
63 : 3184 : Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n)
64 : : {
65 : 3184 : NodeManager* nm = nodeManager();
66 [ + + ]: 3184 : Node cn = nm->mkConstInt(Rational(n == 0 ? 0 : n - 1));
67 [ + + ]: 6368 : return nm->mkNode(n == 0 ? Kind::LT : Kind::LEQ, d_proxy_range, cn);
68 : 3184 : }
69 : :
70 : 3048 : Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
71 : : {
72 [ + + ]: 3048 : if (d_range == d_proxy_range)
73 : : {
74 : 2675 : return Node::null();
75 : : }
76 : 373 : unsigned curr = 0;
77 [ + + ]: 373 : if (!getAssertedLiteralIndex(curr))
78 : : {
79 : 2 : return Node::null();
80 : : }
81 [ + + ]: 371 : if (d_ranges_proxied.find(curr) != d_ranges_proxied.end())
82 : : {
83 : 154 : return Node::null();
84 : : }
85 : 217 : d_ranges_proxied[curr] = true;
86 : 217 : NodeManager* nm = nodeManager();
87 : 217 : Node currLit = getLiteral(curr);
88 : 217 : Node lit;
89 [ + + ]: 217 : if (d_range.getKind() == Kind::SET_CARD)
90 : : {
91 : : // Instead of introducing (set.card s) < n, we introduce the literal
92 : : // s = characteristicSet(s, n-1) for n>0 and false for n=0. We do this
93 : : // to avoid introducing set.card.
94 [ + + ]: 210 : if (curr == 0)
95 : : {
96 : 57 : lit = nodeManager()->mkConst(false);
97 : : }
98 : : else
99 : : {
100 : : Node cset = sets::NormalForm::getCharacteristicSet(
101 : 153 : nodeManager(), d_range[0], curr - 1);
102 : 153 : lit = d_range[0].eqNode(cset);
103 : 153 : }
104 : : }
105 : : else
106 : : {
107 [ + - ]: 21 : lit = nm->mkNode(curr == 0 ? Kind::LT : Kind::LEQ,
108 : 7 : d_range,
109 [ - + ]: 21 : nm->mkConstInt(Rational(curr == 0 ? 0 : curr - 1)));
110 : : }
111 : 434 : Node lem = nm->mkNode(Kind::EQUAL, currLit, lit);
112 : 217 : return lem;
113 : 217 : }
114 : :
115 : 13990 : BoundedIntegers::BoundedIntegers(Env& env,
116 : : QuantifiersState& qs,
117 : : QuantifiersInferenceManager& qim,
118 : : QuantifiersRegistry& qr,
119 : 13990 : TermRegistry& tr)
120 [ + + ]: 41970 : : QuantifiersModule(env, qs, qim, qr, tr)
121 : : {
122 : 13990 : }
123 : :
124 [ + - ][ + + ]: 55936 : BoundedIntegers::~BoundedIntegers() {}
125 : :
126 : 14004 : void BoundedIntegers::presolve() { d_bnd_it.clear(); }
127 : :
128 : 25323 : bool BoundedIntegers::hasNonBoundVar(Node f,
129 : : Node b,
130 : : std::map<Node, bool>& visited)
131 : : {
132 [ + + ]: 25323 : if (visited.find(b) == visited.end())
133 : : {
134 : 21354 : visited[b] = true;
135 [ + + ]: 21354 : if (b.getKind() == Kind::BOUND_VARIABLE)
136 : : {
137 [ + + ]: 1685 : if (!isBound(f, b))
138 : : {
139 : 874 : return true;
140 : : }
141 : : }
142 : : else
143 : : {
144 [ + + ]: 38408 : for (unsigned i = 0; i < b.getNumChildren(); i++)
145 : : {
146 [ + + ]: 20248 : if (hasNonBoundVar(f, b[i], visited))
147 : : {
148 : 1509 : return true;
149 : : }
150 : : }
151 : : }
152 : : }
153 : 22940 : return false;
154 : : }
155 : 5075 : bool BoundedIntegers::hasNonBoundVar(Node f, Node b)
156 : : {
157 : 5075 : std::map<Node, bool> visited;
158 : 10150 : return hasNonBoundVar(f, b, visited);
159 : 5075 : }
160 : :
161 : 1036 : bool BoundedIntegers::processEqDisjunct(Node q,
162 : : Node n,
163 : : Node& v,
164 : : std::vector<Node>& v_cases)
165 : : {
166 [ + + ]: 1036 : if (n.getKind() == Kind::EQUAL)
167 : : {
168 [ + + ]: 3006 : for (unsigned i = 0; i < 2; i++)
169 : : {
170 : 2028 : Node t = n[i];
171 [ + + ]: 2028 : if (!hasNonBoundVar(q, n[1 - i]))
172 : : {
173 [ + + ]: 1399 : if (t == v)
174 : : {
175 : 24 : v_cases.push_back(n[1 - i]);
176 : 24 : return true;
177 : : }
178 [ + + ][ + + ]: 1375 : else if (v.isNull() && t.getKind() == Kind::BOUND_VARIABLE)
[ + + ]
179 : : {
180 : 26 : v = t;
181 : 26 : v_cases.push_back(n[1 - i]);
182 : 26 : return true;
183 : : }
184 : : }
185 [ + + ]: 2028 : }
186 : : }
187 : 986 : return false;
188 : : }
189 : :
190 : 400 : void BoundedIntegers::processMatchBoundVars(Node q,
191 : : Node n,
192 : : std::vector<Node>& bvs,
193 : : std::map<Node, bool>& visited)
194 : : {
195 [ + - ]: 400 : if (visited.find(n) == visited.end())
196 : : {
197 : 400 : visited[n] = true;
198 : 400 : if (n.getKind() == Kind::BOUND_VARIABLE && !isBound(q, n))
199 : : {
200 : 125 : bvs.push_back(n);
201 : : // injective operators
202 : : }
203 [ + + ]: 275 : else if (n.getKind() == Kind::APPLY_CONSTRUCTOR)
204 : : {
205 [ + + ]: 308 : for (unsigned i = 0; i < n.getNumChildren(); i++)
206 : : {
207 : 172 : processMatchBoundVars(q, n[i], bvs, visited);
208 : : }
209 : : }
210 : : }
211 : 400 : }
212 : :
213 : 16620 : void BoundedIntegers::process(
214 : : Node q,
215 : : Node n,
216 : : bool pol,
217 : : std::map<Node, unsigned>& bound_lit_type_map,
218 : : std::map<int, std::map<Node, Node> >& bound_lit_map,
219 : : std::map<int, std::map<Node, bool> >& bound_lit_pol_map,
220 : : std::map<int, std::map<Node, Node> >& bound_int_range_term,
221 : : std::map<Node, std::vector<Node> >& bound_fixed_set)
222 : : {
223 [ + + ][ + + ]: 16620 : if (n.getKind() == Kind::OR || n.getKind() == Kind::AND)
[ + + ]
224 : : {
225 [ + + ]: 3517 : if ((n.getKind() == Kind::OR) == pol)
226 : : {
227 [ + + ]: 11554 : for (unsigned i = 0; i < n.getNumChildren(); i++)
228 : : {
229 : 8995 : process(q,
230 : : n[i],
231 : : pol,
232 : : bound_lit_type_map,
233 : : bound_lit_map,
234 : : bound_lit_pol_map,
235 : : bound_int_range_term,
236 : : bound_fixed_set);
237 : : }
238 : : }
239 : : else
240 : : {
241 : : // if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn
242 : : // }
243 : 958 : Node conj = n;
244 [ - + ]: 958 : if (!pol)
245 : : {
246 : 0 : conj = TermUtil::simpleNegate(conj);
247 : : }
248 [ + - ]: 1916 : Trace("bound-int-debug")
249 : 0 : << "Process possible finite disequality conjunction : " << conj
250 : 958 : << std::endl;
251 [ - + ][ - + ]: 958 : Assert(conj.getKind() == Kind::AND);
[ - - ]
252 : 958 : Node v;
253 : 958 : std::vector<Node> v_cases;
254 : 958 : bool success = true;
255 [ + + ]: 1008 : for (unsigned i = 0; i < conj.getNumChildren(); i++)
256 : : {
257 [ + + ][ - - ]: 984 : if (conj[i].getKind() == Kind::NOT
258 : 984 : && processEqDisjunct(q, conj[i][0], v, v_cases))
259 : : {
260 : : // continue
261 : : }
262 : : else
263 : : {
264 [ + - ]: 1868 : Trace("bound-int-debug")
265 [ - + ][ - - ]: 934 : << "...failed due to " << conj[i] << std::endl;
266 : 934 : success = false;
267 : 934 : break;
268 : : }
269 : : }
270 : 958 : if (success && !isBound(q, v))
271 : : {
272 [ + - ]: 10 : Trace("bound-int-debug") << "Success with variable " << v << std::endl;
273 : 10 : bound_lit_type_map[v] = BOUND_FIXED_SET;
274 : 10 : bound_lit_map[3][v] = n;
275 : 10 : bound_lit_pol_map[3][v] = pol;
276 : 10 : bound_fixed_set[v].clear();
277 : 20 : bound_fixed_set[v].insert(
278 : 20 : bound_fixed_set[v].end(), v_cases.begin(), v_cases.end());
279 : : }
280 : 958 : }
281 : : }
282 [ + + ]: 13103 : else if (n.getKind() == Kind::EQUAL)
283 : : {
284 [ + + ]: 1622 : if (!pol)
285 : : {
286 : : // non-applied DER on x != t, x can be bound to { t }
287 : 750 : Node v;
288 : 750 : std::vector<Node> v_cases;
289 [ - + ]: 750 : if (processEqDisjunct(q, n, v, v_cases))
290 : : {
291 [ - - ]: 0 : if (!isBound(q, v))
292 : : {
293 : 0 : bound_lit_type_map[v] = BOUND_FIXED_SET;
294 : 0 : bound_lit_map[3][v] = n;
295 : 0 : bound_lit_pol_map[3][v] = pol;
296 : 0 : Assert(v_cases.size() == 1);
297 : 0 : bound_fixed_set[v].clear();
298 : 0 : bound_fixed_set[v].push_back(v_cases[0]);
299 : : }
300 : : }
301 : 750 : }
302 : : }
303 [ + + ]: 11481 : else if (n.getKind() == Kind::NOT)
304 : : {
305 : 4800 : process(q,
306 : : n[0],
307 : 4800 : !pol,
308 : : bound_lit_type_map,
309 : : bound_lit_map,
310 : : bound_lit_pol_map,
311 : : bound_int_range_term,
312 : : bound_fixed_set);
313 : : }
314 [ + + ]: 6681 : else if (n.getKind() == Kind::GEQ)
315 : : {
316 [ + + ]: 5562 : if (n[0].getType().isInteger())
317 : : {
318 : 5557 : std::map<Node, Node> msum;
319 [ + - ]: 5557 : if (ArithMSum::getMonomialSumLit(n, msum))
320 : : {
321 : 5557 : NodeManager* nm = nodeManager();
322 [ + - ]: 11114 : Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n
323 : 5557 : << " is monomial sum : " << std::endl;
324 : 5557 : ArithMSum::debugPrintMonomialSum(msum, "bound-int-debug");
325 [ + + ]: 16773 : for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
326 : 11216 : ++it)
327 : : {
328 [ + + ]: 20273 : if (!it->first.isNull() && it->first.getKind() == Kind::BOUND_VARIABLE
329 : 31489 : && !isBound(q, it->first))
330 : : {
331 : : // if not bound in another way
332 : 2847 : if (bound_lit_type_map.find(it->first) == bound_lit_type_map.end()
333 [ + + ][ + + ]: 2847 : || bound_lit_type_map[it->first] == BOUND_INT_RANGE)
[ + + ]
334 : : {
335 : 2812 : Node veq;
336 [ + - ]: 2812 : if (ArithMSum::isolate(it->first, msum, veq, Kind::GEQ) != 0)
337 : : {
338 : 2812 : Node n1 = veq[0];
339 : 2812 : Node n2 = veq[1];
340 [ + + ]: 2812 : if (pol)
341 : : {
342 : : // flip
343 : 1230 : n1 = veq[1];
344 : 1230 : n2 = veq[0];
345 [ + + ]: 1230 : if (n1.getKind() == Kind::BOUND_VARIABLE)
346 : : {
347 : 2 : n2 = nm->mkNode(Kind::ADD, n2, nm->mkConstInt(Rational(1)));
348 : : }
349 : : else
350 : : {
351 : : n1 =
352 : 1228 : nm->mkNode(Kind::ADD, n1, nm->mkConstInt(Rational(-1)));
353 : : }
354 : 1230 : veq = nm->mkNode(Kind::GEQ, n1, n2);
355 : : }
356 [ + - ]: 5624 : Trace("bound-int-debug")
357 : 0 : << "Isolated for " << it->first << " : (" << n1
358 : 2812 : << " >= " << n2 << ")" << std::endl;
359 [ + + ]: 2812 : Node t = n1 == it->first ? n2 : n1;
360 [ + + ]: 2812 : if (!hasNonBoundVar(q, t))
361 : : {
362 [ + - ]: 5148 : Trace("bound-int-debug")
363 : 2574 : << "The bound is relevant." << std::endl;
364 [ + + ]: 2574 : int loru = n1 == it->first ? 0 : 1;
365 : 2574 : bound_lit_type_map[it->first] = BOUND_INT_RANGE;
366 : 2574 : bound_int_range_term[loru][it->first] = t;
367 : 2574 : bound_lit_map[loru][it->first] = n;
368 : 2574 : bound_lit_pol_map[loru][it->first] = pol;
369 : : }
370 : : else
371 : : {
372 [ + - ]: 476 : Trace("bound-int-debug")
373 : 0 : << "The term " << t << " has non-bound variable."
374 : 238 : << std::endl;
375 : : }
376 : 2812 : }
377 : 2812 : }
378 : : }
379 : : }
380 : : }
381 : 5557 : }
382 : : }
383 [ + + ]: 1119 : else if (n.getKind() == Kind::SET_MEMBER)
384 : : {
385 : : // Note this is incomplete when combined with cardinality constraints,
386 : : // since we may introduce slack elements during model construction.
387 : : // Here, fmfBound should be enabled, otherwise the incompleteness check
388 : : // in the theory of sets is out of sync.
389 [ - + ][ - + ]: 235 : Assert(options().quantifiers.fmfBound);
[ - - ]
390 : 235 : if (!pol && !hasNonBoundVar(q, n[1]))
391 : : {
392 : 228 : std::vector<Node> bound_vars;
393 : 228 : std::map<Node, bool> visited;
394 : 228 : processMatchBoundVars(q, n[0], bound_vars, visited);
395 [ + + ]: 353 : for (unsigned i = 0; i < bound_vars.size(); i++)
396 : : {
397 : 125 : Node v = bound_vars[i];
398 [ + - ]: 250 : Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n
399 : 125 : << " is membership." << std::endl;
400 : 125 : bound_lit_type_map[v] = BOUND_SET_MEMBER;
401 : 125 : bound_lit_map[2][v] = n;
402 : 125 : bound_lit_pol_map[2][v] = pol;
403 : 125 : }
404 : 228 : }
405 : : }
406 : : else
407 : : {
408 [ + - ][ + - ]: 884 : Assert(n.getKind() != Kind::LEQ && n.getKind() != Kind::LT
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
409 : : && n.getKind() != Kind::GT);
410 : : }
411 : 16620 : }
412 : :
413 : 76723 : bool BoundedIntegers::needsCheck(Theory::Effort e)
414 : : {
415 : 76723 : return e == Theory::EFFORT_LAST_CALL;
416 : : }
417 : :
418 : 25817 : void BoundedIntegers::check(CVC5_UNUSED Theory::Effort e, QEffort quant_e)
419 : : {
420 [ + + ]: 25817 : if (quant_e != QEFFORT_STANDARD)
421 : : {
422 : 16841 : return;
423 : : }
424 [ + - ]: 8976 : Trace("bint-engine") << "---Bounded Integers---" << std::endl;
425 : 8976 : bool addedLemma = false;
426 : : // make sure proxies are up-to-date with range
427 [ + + ]: 12024 : for (const Node& r : d_ranges)
428 : : {
429 : 3048 : Node prangeLem = d_rms[r]->proxyCurrentRangeLemma();
430 [ + + ]: 3048 : if (!prangeLem.isNull())
431 : : {
432 [ + - ]: 434 : Trace("bound-int-lemma")
433 : 217 : << "*** bound int : proxy lemma : " << prangeLem << std::endl;
434 : 217 : d_qim.addPendingLemma(prangeLem, InferenceId::QUANTIFIERS_BINT_PROXY);
435 : 217 : addedLemma = true;
436 : : }
437 : 3048 : }
438 [ + - ]: 8976 : Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl;
439 : : }
440 : 1495 : void BoundedIntegers::setBoundedVar(Node q, Node v, BoundVarType bound_type)
441 : : {
442 : 1495 : d_bound_type[q][v] = bound_type;
443 : 1495 : d_set_nums[q][v] = d_set[q].size();
444 : 1495 : d_set[q].push_back(v);
445 [ + - ]: 2990 : Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v
446 : 1495 : << std::endl;
447 : 1495 : }
448 : :
449 : 24149 : void BoundedIntegers::checkOwnership(Node f)
450 : : {
451 : : // this needs to be done at preregister since it affects e.g. QuantDSplit's
452 : : // preregister
453 [ + - ]: 24149 : Trace("bound-int") << "check ownership quantifier " << f << std::endl;
454 : :
455 : : // determine if we should look at the quantified formula at all
456 [ + + ]: 24149 : if (!options().quantifiers.fmfBound)
457 : : {
458 : : // only applying it to internal quantifiers
459 : 23727 : QuantAttributes& qattr = d_qreg.getQuantAttributes();
460 [ + + ]: 23727 : if (!qattr.isQuantBounded(f))
461 : : {
462 [ + - ]: 22794 : Trace("bound-int") << "...not bounded, skip" << std::endl;
463 : 22794 : return;
464 : : }
465 : : }
466 : :
467 : 1355 : NodeManager* nm = nodeManager();
468 : :
469 : : bool success;
470 [ + + ]: 2825 : do
471 : : {
472 : 2825 : std::map<Node, unsigned> bound_lit_type_map;
473 : 2825 : std::map<int, std::map<Node, Node> > bound_lit_map;
474 : 2825 : std::map<int, std::map<Node, bool> > bound_lit_pol_map;
475 : 2825 : std::map<int, std::map<Node, Node> > bound_int_range_term;
476 : 2825 : std::map<Node, std::vector<Node> > bound_fixed_set;
477 : 2825 : success = false;
478 : 2825 : process(f,
479 : : f[1],
480 : : true,
481 : : bound_lit_type_map,
482 : : bound_lit_map,
483 : : bound_lit_pol_map,
484 : : bound_int_range_term,
485 : : bound_fixed_set);
486 : : // for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it !=
487 : : // d_bounds[0][f].end(); ++it ){
488 : 2825 : for (std::map<Node, unsigned>::iterator it = bound_lit_type_map.begin();
489 [ + + ]: 4256 : it != bound_lit_type_map.end();
490 : 1431 : ++it)
491 : : {
492 : 1431 : Node v = it->first;
493 [ + - ]: 1431 : if (!isBound(f, v))
494 : : {
495 : 1431 : bool setBoundVar = false;
496 [ + + ]: 1431 : if (it->second == BOUND_INT_RANGE)
497 : : {
498 : : // must have both
499 : 1308 : std::map<Node, Node>& blm0 = bound_lit_map[0];
500 : 1308 : std::map<Node, Node>& blm1 = bound_lit_map[1];
501 [ + + ][ + + ]: 1308 : if (blm0.find(v) != blm0.end() && blm1.find(v) != blm1.end())
[ + + ]
502 : : {
503 : 1181 : setBoundedVar(f, v, BOUND_INT_RANGE);
504 : 1181 : setBoundVar = true;
505 [ + + ]: 3543 : for (unsigned b = 0; b < 2; b++)
506 : : {
507 : : // set the bounds
508 [ - + ][ - + ]: 2362 : Assert(bound_int_range_term[b].find(v)
[ - - ]
509 : : != bound_int_range_term[b].end());
510 : 2362 : d_bounds[b][f][v] = bound_int_range_term[b][v];
511 : : }
512 : : Node r =
513 : 2362 : nm->mkNode(Kind::SUB, d_bounds[1][f][v], d_bounds[0][f][v]);
514 : 1181 : d_range[f][v] = rewrite(r);
515 [ + - ]: 2362 : Trace("bound-int") << "Variable " << v
516 : 0 : << " is bound because of int range literals "
517 : 0 : << bound_lit_map[0][v] << " and "
518 : 1181 : << bound_lit_map[1][v] << std::endl;
519 : 1181 : }
520 : : }
521 [ + + ]: 123 : else if (it->second == BOUND_SET_MEMBER)
522 : : {
523 : 113 : setBoundedVar(f, v, BOUND_SET_MEMBER);
524 : 113 : setBoundVar = true;
525 : 113 : d_setm_range[f][v] = bound_lit_map[2][v][1];
526 : 113 : d_setm_range_lit[f][v] = bound_lit_map[2][v];
527 : 113 : Node cardTerm = nm->mkNode(Kind::SET_CARD, d_setm_range[f][v]);
528 : : // Note that we avoid reasoning about cardinality by eagerly
529 : : // eliminating set.card for literals as they are introduced.
530 : 113 : d_range[f][v] = cardTerm;
531 [ + - ]: 226 : Trace("bound-int") << "Variable " << v
532 : 0 : << " is bound because of set membership literal "
533 : 113 : << bound_lit_map[2][v] << std::endl;
534 : 113 : }
535 [ + - ]: 10 : else if (it->second == BOUND_FIXED_SET)
536 : : {
537 : 10 : setBoundedVar(f, v, BOUND_FIXED_SET);
538 : 10 : setBoundVar = true;
539 [ + + ]: 30 : for (unsigned i = 0; i < bound_fixed_set[v].size(); i++)
540 : : {
541 : 20 : Node t = bound_fixed_set[v][i];
542 [ + + ]: 20 : if (expr::hasBoundVar(t))
543 : : {
544 : 6 : d_fixed_set_ngr_range[f][v].push_back(t);
545 : : }
546 : : else
547 : : {
548 : 14 : d_fixed_set_gr_range[f][v].push_back(t);
549 : : }
550 : 20 : }
551 [ + - ]: 20 : Trace("bound-int") << "Variable " << v
552 : 0 : << " is bound because of disequality conjunction "
553 : 10 : << bound_lit_map[3][v] << std::endl;
554 : : }
555 [ + + ]: 1431 : if (setBoundVar)
556 : : {
557 : 1304 : success = true;
558 : : // set Attributes on literals
559 [ + + ]: 3912 : for (unsigned b = 0; b < 2; b++)
560 : : {
561 : 2608 : std::map<Node, Node>& blm = bound_lit_map[b];
562 [ + + ]: 2608 : if (blm.find(v) != blm.end())
563 : : {
564 : 2369 : std::map<Node, bool>& blmp = bound_lit_pol_map[b];
565 : : // WARNING_CANDIDATE:
566 : : // This assertion may fail. We intentionally do not enable this in
567 : : // production as it is considered safe for this to fail. We fail
568 : : // the assertion in debug mode to have this instance raised to
569 : : // our attention.
570 [ - + ][ - + ]: 2369 : Assert(blmp.find(v) != blmp.end());
[ - - ]
571 : : BoundIntLitAttribute bila;
572 [ + + ]: 2369 : bound_lit_map[b][v].setAttribute(bila, blmp[v] ? 1 : 0);
573 : : }
574 : : else
575 : : {
576 [ - + ][ - + ]: 239 : Assert(it->second != BOUND_INT_RANGE);
[ - - ]
577 : : }
578 : : }
579 : : }
580 : : }
581 : 1431 : }
582 [ + + ]: 2825 : if (!success)
583 : : {
584 : : // resort to setting a finite bound on a variable
585 [ + + ]: 3178 : for (unsigned i = 0; i < f[0].getNumChildren(); i++)
586 : : {
587 [ + + ]: 1823 : if (d_bound_type[f].find(f[0][i]) == d_bound_type[f].end())
588 : : {
589 : 566 : TypeNode tn = f[0][i].getType();
590 [ + + ][ + + ]: 332 : if ((tn.isUninterpretedSort() && d_env.isFiniteType(tn))
[ - - ]
591 [ + + ][ + + ]: 332 : || d_qreg.getQuantifiersBoundInference().mayComplete(tn))
[ + + ][ + + ]
[ - - ]
592 : : {
593 : 191 : success = true;
594 : 191 : setBoundedVar(f, f[0][i], BOUND_FINITE);
595 : 191 : break;
596 : : }
597 [ + + ]: 283 : }
598 : : }
599 : : }
600 : 2825 : } while (success);
601 : :
602 [ - + ]: 1355 : if (TraceIsOn("bound-int"))
603 : : {
604 [ - - ]: 0 : Trace("bound-int") << "Bounds are : " << std::endl;
605 [ - - ]: 0 : for (unsigned i = 0; i < f[0].getNumChildren(); i++)
606 : : {
607 : 0 : Node v = f[0][i];
608 [ - - ]: 0 : if (std::find(d_set[f].begin(), d_set[f].end(), v) != d_set[f].end())
609 : : {
610 : 0 : Assert(d_bound_type[f].find(v) != d_bound_type[f].end());
611 [ - - ]: 0 : if (d_bound_type[f][v] == BOUND_INT_RANGE)
612 : : {
613 [ - - ]: 0 : Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v
614 : 0 : << " <= " << d_bounds[1][f][v] << " (range is "
615 : 0 : << d_range[f][v] << ")" << std::endl;
616 : : }
617 [ - - ]: 0 : else if (d_bound_type[f][v] == BOUND_SET_MEMBER)
618 : : {
619 [ - - ]: 0 : if (d_setm_range_lit[f][v][0] == v)
620 : : {
621 [ - - ]: 0 : Trace("bound-int")
622 : 0 : << " " << v << " in " << d_setm_range[f][v] << std::endl;
623 : : }
624 : : else
625 : : {
626 [ - - ]: 0 : Trace("bound-int") << " " << v << " unifiable in "
627 : 0 : << d_setm_range_lit[f][v] << std::endl;
628 : : }
629 : : }
630 [ - - ]: 0 : else if (d_bound_type[f][v] == BOUND_FIXED_SET)
631 : : {
632 [ - - ]: 0 : Trace("bound-int") << " " << v << " in { ";
633 [ - - ]: 0 : for (TNode fnr : d_fixed_set_ngr_range[f][v])
634 : : {
635 [ - - ]: 0 : Trace("bound-int") << fnr << " ";
636 : 0 : }
637 [ - - ]: 0 : for (TNode fgr : d_fixed_set_gr_range[f][v])
638 : : {
639 [ - - ]: 0 : Trace("bound-int") << fgr << " ";
640 : 0 : }
641 [ - - ]: 0 : Trace("bound-int") << "}" << std::endl;
642 : : }
643 [ - - ]: 0 : else if (d_bound_type[f][v] == BOUND_FINITE)
644 : : {
645 [ - - ]: 0 : Trace("bound-int")
646 : 0 : << " " << v << " has small finite type." << std::endl;
647 : : }
648 : : else
649 : : {
650 [ - - ]: 0 : Trace("bound-int") << " " << v << " has unknown bound." << std::endl;
651 : 0 : DebugUnhandled();
652 : : }
653 : : }
654 : : else
655 : : {
656 [ - - ]: 0 : Trace("bound-int") << " " << "*** " << v << " is unbounded."
657 : 0 : << std::endl;
658 : : }
659 : 0 : }
660 : : }
661 : :
662 : 1355 : bool bound_success = true;
663 [ + + ]: 2848 : for (unsigned i = 0; i < f[0].getNumChildren(); i++)
664 : : {
665 [ + + ]: 1561 : if (d_bound_type[f].find(f[0][i]) == d_bound_type[f].end())
666 : : {
667 [ + - ]: 136 : Trace("bound-int-warn")
668 : 68 : << "Warning : Bounded Integers : Due to quantification on " << f[0][i]
669 : 68 : << ", could not find bounds for " << f << std::endl;
670 : 68 : bound_success = false;
671 : 68 : break;
672 : : }
673 : : }
674 : :
675 [ + + ]: 1355 : if (bound_success)
676 : : {
677 : 1287 : d_bound_quants.push_back(f);
678 : 1287 : DecisionManager* dm = d_qim.getDecisionManager();
679 [ + + ]: 2777 : for (unsigned i = 0; i < d_set[f].size(); i++)
680 : : {
681 : 1490 : Node v = d_set[f][i];
682 : 1490 : std::map<Node, Node>::iterator itr = d_range[f].find(v);
683 [ + + ]: 1490 : if (itr != d_range[f].end())
684 : : {
685 : 1292 : Node r = itr->second;
686 [ - + ][ - + ]: 1292 : Assert(!r.isNull());
[ - - ]
687 : 1292 : bool isProxy = false;
688 [ + + ]: 1292 : if (expr::hasBoundVar(r))
689 : : {
690 : : // introduce a new bound
691 : 254 : Node new_range = NodeManager::mkDummySkolem("bir", r.getType());
692 : 127 : d_nground_range[f][v] = r;
693 : 127 : d_range[f][v] = new_range;
694 : 127 : r = new_range;
695 : 127 : isProxy = true;
696 : 127 : }
697 [ + + ]: 1292 : if (!r.isConst())
698 : : {
699 [ + + ]: 1235 : if (d_rms.find(r) == d_rms.end())
700 : : {
701 [ + - ]: 2260 : Trace("bound-int")
702 : 0 : << "For " << v
703 : 0 : << ", bounded Integer Module will try to minimize : " << r
704 : 1130 : << std::endl;
705 : 1130 : d_ranges.push_back(r);
706 : 2260 : d_rms[r].reset(new IntRangeDecisionHeuristic(
707 : 1130 : d_env, r, d_qstate.getValuation(), isProxy));
708 : 1130 : dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
709 : 1130 : d_rms[r].get());
710 : : }
711 : : }
712 : 1292 : }
713 : 1490 : }
714 : : }
715 : : }
716 : :
717 : 16408 : bool BoundedIntegers::isBound(Node q, Node v) const
718 : : {
719 : 16408 : std::map<Node, std::vector<Node> >::const_iterator its = d_set.find(q);
720 [ + + ]: 16408 : if (its == d_set.end())
721 : : {
722 : 10853 : return false;
723 : : }
724 : 5555 : return std::find(its->second.begin(), its->second.end(), v)
725 : 11110 : != its->second.end();
726 : : }
727 : :
728 : 10113 : BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const
729 : : {
730 : : std::map<Node, std::map<Node, BoundVarType> >::const_iterator itb =
731 : 10113 : d_bound_type.find(q);
732 [ + + ]: 10113 : if (itb == d_bound_type.end())
733 : : {
734 : 1858 : return BOUND_NONE;
735 : : }
736 : 8255 : std::map<Node, BoundVarType>::const_iterator it = itb->second.find(v);
737 [ + + ]: 8255 : if (it == itb->second.end())
738 : : {
739 : 354 : return BOUND_NONE;
740 : : }
741 : 7901 : return it->second;
742 : : }
743 : :
744 : 8744 : void BoundedIntegers::getBoundVarIndices(Node q,
745 : : std::vector<size_t>& indices) const
746 : : {
747 : 8744 : std::map<Node, std::vector<Node> >::const_iterator it = d_set.find(q);
748 [ + + ]: 8744 : if (it != d_set.end())
749 : : {
750 [ + + ]: 11682 : for (const Node& v : it->second)
751 : : {
752 : 6644 : indices.push_back(TermUtil::getVariableNum(q, v));
753 : : }
754 : : }
755 : 8744 : }
756 : :
757 : 5159 : void BoundedIntegers::getBounds(
758 : : Node f, Node v, RepSetIterator* rsi, Node& l, Node& u)
759 : : {
760 : 5159 : l = d_bounds[0][f][v];
761 : 5159 : u = d_bounds[1][f][v];
762 [ + + ]: 5159 : if (d_nground_range[f].find(v) != d_nground_range[f].end())
763 : : {
764 : : // get the substitution
765 : 1427 : std::vector<Node> vars;
766 : 1427 : std::vector<Node> subs;
767 [ + + ]: 1427 : if (getRsiSubsitution(f, v, vars, subs, rsi))
768 : : {
769 : 1346 : u = u.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
770 : 1346 : l = l.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
771 : : }
772 : : else
773 : : {
774 : 81 : u = Node::null();
775 : 81 : l = Node::null();
776 : : }
777 : 1427 : }
778 : 5159 : }
779 : :
780 : 2620 : void BoundedIntegers::getBoundValues(
781 : : Node f, Node v, RepSetIterator* rsi, Node& l, Node& u)
782 : : {
783 : 2620 : getBounds(f, v, rsi, l, u);
784 [ + - ]: 5240 : Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u
785 : 2620 : << std::endl;
786 [ + + ]: 2620 : if (!l.isNull())
787 : : {
788 : 2539 : l = d_treg.getModel()->getValue(l);
789 : : }
790 [ + + ]: 2620 : if (!u.isNull())
791 : : {
792 : 2539 : u = d_treg.getModel()->getValue(u);
793 : : }
794 [ + - ]: 2620 : Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
795 : 2620 : return;
796 : : }
797 : :
798 : 834 : bool BoundedIntegers::isGroundRange(Node q, Node v)
799 : : {
800 [ + - ]: 834 : if (isBound(q, v))
801 : : {
802 [ + + ]: 834 : if (d_bound_type[q][v] == BOUND_INT_RANGE)
803 : : {
804 : 1300 : return !expr::hasBoundVar(getLowerBound(q, v))
805 : 1300 : && !expr::hasBoundVar(getUpperBound(q, v));
806 : : }
807 [ + + ]: 184 : else if (d_bound_type[q][v] == BOUND_SET_MEMBER)
808 : : {
809 : 52 : return !expr::hasBoundVar(d_setm_range[q][v]);
810 : : }
811 [ + - ]: 132 : else if (d_bound_type[q][v] == BOUND_FIXED_SET)
812 : : {
813 : 132 : return !d_fixed_set_ngr_range[q][v].empty();
814 : : }
815 : : }
816 : 0 : return false;
817 : : }
818 : :
819 : 239 : Node BoundedIntegers::getSetRange(Node q, Node v, RepSetIterator* rsi)
820 : : {
821 : 239 : Node sr = d_setm_range[q][v];
822 [ + + ]: 239 : if (d_nground_range[q].find(v) != d_nground_range[q].end())
823 : : {
824 [ + - ]: 28 : Trace("bound-int-rsi-debug")
825 : 14 : << sr << " is non-ground, apply substitution..." << std::endl;
826 : : // get the substitution
827 : 14 : std::vector<Node> vars;
828 : 14 : std::vector<Node> subs;
829 [ + + ]: 14 : if (getRsiSubsitution(q, v, vars, subs, rsi))
830 : : {
831 [ + - ]: 14 : Trace("bound-int-rsi-debug")
832 : 7 : << " apply " << vars << " -> " << subs << std::endl;
833 : 7 : sr = sr.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
834 : : }
835 : : else
836 : : {
837 : 7 : sr = Node::null();
838 : : }
839 : 14 : }
840 : 239 : return sr;
841 : 0 : }
842 : :
843 : 239 : Node BoundedIntegers::getSetRangeValue(Node q, Node v, RepSetIterator* rsi)
844 : : {
845 : 478 : Node sr = getSetRange(q, v, rsi);
846 [ + + ]: 239 : if (sr.isNull())
847 : : {
848 : 7 : return sr;
849 : : }
850 [ + - ]: 232 : Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
851 [ - + ][ - + ]: 232 : Assert(!expr::hasFreeVar(sr));
[ - - ]
852 : 232 : Node sro = sr;
853 : 232 : sr = d_treg.getModel()->getValue(sr);
854 : : // if non-constant, then sr does not occur in the model, we fail
855 [ - + ]: 232 : if (!sr.isConst())
856 : : {
857 : 0 : return Node::null();
858 : : }
859 [ + - ]: 232 : Trace("bound-int-rsi") << "Value is " << sr << std::endl;
860 [ + + ]: 232 : if (sr.getKind() == Kind::SET_EMPTY)
861 : : {
862 : 4 : return sr;
863 : : }
864 : : // we can use choice functions for canonical symbolic instantiations
865 : 228 : unsigned srCard = 0;
866 [ + + ]: 445 : while (sr.getKind() == Kind::SET_UNION)
867 : : {
868 [ - + ][ - + ]: 217 : Assert(sr[0].getKind() == Kind::SET_SINGLETON);
[ - - ]
869 : 217 : srCard++;
870 : 217 : sr = sr[1];
871 : : }
872 [ - + ][ - + ]: 228 : Assert(sr.getKind() == Kind::SET_SINGLETON);
[ - - ]
873 : 228 : srCard++;
874 [ + - ]: 228 : Trace("bound-int-rsi") << "...cardinality is " << srCard << std::endl;
875 : : // get the characteristic set
876 : 228 : Node nsr = sets::NormalForm::getCharacteristicSet(nodeManager(), sro, srCard);
877 : : // turns the concrete set value of sro into a canonical representation
878 : : // e.g.
879 : : // singleton(0) union singleton(1)
880 : : // becomes
881 : : // C1 union (set.singleton (set.choose (set.minus S C1)))
882 : : // where C1 = (set.singleton (set.choose S)).
883 [ + - ]: 228 : Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
884 : 228 : return nsr;
885 : 239 : }
886 : :
887 : 1493 : bool BoundedIntegers::getRsiSubsitution(Node q,
888 : : Node v,
889 : : std::vector<Node>& vars,
890 : : std::vector<Node>& subs,
891 : : RepSetIterator* rsi)
892 : : {
893 [ + - ]: 2986 : Trace("bound-int-rsi") << "Get bound value in model of variable " << v
894 : 1493 : << std::endl;
895 [ - + ][ - + ]: 1493 : Assert(d_set_nums[q].find(v) != d_set_nums[q].end());
[ - - ]
896 : 1493 : int vindex = d_set_nums[q][v];
897 [ - + ][ - + ]: 1493 : Assert(d_set_nums[q][v] == vindex);
[ - - ]
898 [ + - ]: 1493 : Trace("bound-int-rsi-debug") << " index order is " << vindex << std::endl;
899 : : // must take substitution for all variables that are iterating at higher level
900 [ + + ]: 3266 : for (int i = 0; i < vindex; i++)
901 : : {
902 [ - + ][ - + ]: 1773 : Assert(d_set_nums[q][d_set[q][i]] == i);
[ - - ]
903 [ + - ]: 3546 : Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " "
904 : 1773 : << i << std::endl;
905 : 1773 : int vo = rsi->getVariableOrder(i);
906 [ - + ][ - + ]: 1773 : Assert(q[0][vo] == d_set[q][i]);
[ - - ]
907 : 1773 : TypeNode tn = d_set[q][i].getType();
908 : : // If the type of tn is not closed enumerable, we must map the value back
909 : : // to a term that appears in the same equivalence class as the constant.
910 : : // Notice that this is to ensure that unhandled values (e.g. uninterpreted
911 : : // constants, datatype values) do not enter instantiations/lemmas, which
912 : : // can lead to refutation unsoundness. However, it is important that we
913 : : // conversely do *not* map terms to values in other cases. In particular,
914 : : // replacing a constant c with a term t can lead to solution unsoundness
915 : : // if we are instantiating a quantified formula that corresponds to a
916 : : // reduction for t, since then the reduction is using circular reasoning:
917 : : // the current value of t is being used to reason about the range of
918 : : // its axiomatization. This is limited to reductions in the theory of
919 : : // strings, which use quantification on integers only. Note this
920 : : // impacts only quantified formulas with 2+ dimensions and dependencies
921 : : // between dimensions, e.g. str.indexof_re reduction.
922 : 1773 : Node t = rsi->getCurrentTerm(vo, !tn.isClosedEnumerable());
923 [ + - ]: 1773 : Trace("bound-int-rsi") << "term : " << t << std::endl;
924 : 1773 : vars.push_back(d_set[q][i]);
925 : 1773 : subs.push_back(t);
926 : 1773 : }
927 : :
928 : : // check if it has been instantiated
929 [ + - ][ + + ]: 1493 : if (!vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs))
[ + + ]
930 : : {
931 : 96 : if (d_bound_type[q][v] == BOUND_INT_RANGE
932 [ + + ][ + + ]: 96 : || d_bound_type[q][v] == BOUND_SET_MEMBER)
[ + + ]
933 : : {
934 : : // must add the lemma
935 : 88 : Node nn = d_nground_range[q][v];
936 : 88 : nn = nn.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
937 : 176 : Node lem = nodeManager()->mkNode(Kind::LEQ, nn, d_range[q][v]);
938 [ + - ]: 176 : Trace("bound-int-lemma")
939 : 0 : << "*** Add lemma to minimize instantiated non-ground term " << lem
940 : 88 : << std::endl;
941 : 88 : d_qim.lemma(lem, InferenceId::QUANTIFIERS_BINT_MIN_NG);
942 : 88 : }
943 : 96 : return false;
944 : : }
945 : : else
946 : : {
947 : 1397 : return true;
948 : : }
949 : : }
950 : :
951 : 680 : Node BoundedIntegers::matchBoundVar(Node v, Node t, Node e)
952 : : {
953 [ + + ]: 680 : if (t == v)
954 : : {
955 : 302 : return e;
956 : : }
957 [ + + ]: 378 : else if (t.getKind() == Kind::APPLY_CONSTRUCTOR)
958 : : {
959 [ - + ]: 302 : if (e.getKind() == Kind::APPLY_CONSTRUCTOR)
960 : : {
961 [ - - ]: 0 : if (t.getOperator() != e.getOperator())
962 : : {
963 : 0 : return Node::null();
964 : : }
965 : : }
966 : 302 : const DType& dt = datatypes::utils::datatypeOf(t.getOperator());
967 : 302 : unsigned index = datatypes::utils::indexOf(t.getOperator());
968 : 302 : bool sharedSel = options().datatypes.dtSharedSelectors;
969 [ + - ]: 378 : for (unsigned i = 0; i < t.getNumChildren(); i++)
970 : : {
971 : 378 : Node u;
972 [ - + ]: 378 : if (e.getKind() == Kind::APPLY_CONSTRUCTOR)
973 : : {
974 : 0 : u = matchBoundVar(v, t[i], e[i]);
975 : : }
976 : : else
977 : : {
978 : 378 : Node se = datatypes::utils::applySelector(dt[index], i, sharedSel, e);
979 : 378 : u = matchBoundVar(v, t[i], se);
980 : 378 : }
981 [ + + ]: 378 : if (!u.isNull())
982 : : {
983 : 302 : return u;
984 : : }
985 [ + + ]: 378 : }
986 : : }
987 : 76 : return Node::null();
988 : : }
989 : :
990 : 3437 : bool BoundedIntegers::getBoundElements(RepSetIterator* rsi,
991 : : bool initial,
992 : : Node q,
993 : : Node v,
994 : : std::vector<Node>& elements)
995 : : {
996 : 3437 : if (initial || !isGroundRange(q, v))
997 : : {
998 : 3127 : elements.clear();
999 : 3127 : BoundVarType bvt = getBoundVarType(q, v);
1000 [ + + ]: 3127 : if (bvt == BOUND_INT_RANGE)
1001 : : {
1002 : 2620 : Node l, u;
1003 : 2620 : getBoundValues(q, v, rsi, l, u);
1004 [ + + ][ - + ]: 2620 : if (l.isNull() || u.isNull())
[ + + ]
1005 : : {
1006 [ + - ]: 162 : Trace("bound-int-warn")
1007 : 0 : << "WARNING: Could not find integer bounds in model for " << v
1008 : 81 : << " in " << q << std::endl;
1009 : : // failed, abort the iterator
1010 : 81 : return false;
1011 : : }
1012 : : else
1013 : : {
1014 : 2539 : NodeManager* nm = nodeManager();
1015 [ + - ]: 5078 : Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l
1016 : 2539 : << "..." << u << std::endl;
1017 : 5078 : Node range = rewrite(nm->mkNode(Kind::SUB, u, l));
1018 [ - + ]: 2539 : if (!range.isConst())
1019 : : {
1020 [ - - ]: 0 : Trace("fmf-incomplete") << "Incomplete because of integer "
1021 : 0 : "quantification, bounds are unknown for "
1022 : 0 : << v << "." << std::endl;
1023 : 0 : return false;
1024 : : }
1025 : 2539 : Rational rat = range.getConst<Rational>();
1026 : : // 9999 is an arbitrary range past which we do not do exhaustive
1027 : : // bounded instantation, based on the check below.
1028 : 2539 : Node tl = l;
1029 : 2539 : Node tu = u;
1030 : 2539 : getBounds(q, v, rsi, tl, tu);
1031 [ + - ][ + - ]: 2539 : Assert(!tl.isNull() && !tu.isNull());
[ - + ][ - + ]
[ - - ]
1032 [ + - ]: 2539 : if (rat < Rational(9999))
1033 : : {
1034 : : // if negative, elements are empty
1035 [ + + ]: 2539 : if (rat.sgn() >= 0)
1036 : : {
1037 : 2205 : long rr = rat.getNumerator().getLong() + 1;
1038 [ + - ]: 4410 : Trace("bound-int-rsi")
1039 : 2205 : << "Actual bound range is " << rr << std::endl;
1040 [ + + ]: 10953 : for (long k = 0; k < rr; k++)
1041 : : {
1042 : 17496 : Node t = nm->mkNode(Kind::ADD, tl, nm->mkConstInt(Rational(k)));
1043 : 8748 : t = rewrite(t);
1044 : 8748 : elements.push_back(t);
1045 : 8748 : }
1046 : : }
1047 : 2539 : return true;
1048 : : }
1049 : : else
1050 : : {
1051 [ - - ]: 0 : Trace("fmf-incomplete") << "Incomplete because of integer "
1052 : 0 : "quantification, bounds are too big for "
1053 : 0 : << v << "." << std::endl;
1054 : 0 : return false;
1055 : : }
1056 : 2539 : }
1057 : 2620 : }
1058 [ + + ]: 507 : else if (bvt == BOUND_SET_MEMBER)
1059 : : {
1060 : 478 : Node srv = getSetRangeValue(q, v, rsi);
1061 [ + + ]: 239 : if (srv.isNull())
1062 : : {
1063 [ + - ]: 14 : Trace("bound-int-warn")
1064 : 0 : << "WARNING: Could not find set bound in model for " << v << " in "
1065 : 7 : << q << std::endl;
1066 : 7 : return false;
1067 : : }
1068 : : else
1069 : : {
1070 [ + - ]: 464 : Trace("bound-int-rsi")
1071 : 232 : << "Bounded by set membership : " << srv << std::endl;
1072 [ + + ]: 232 : if (srv.getKind() != Kind::SET_EMPTY)
1073 : : {
1074 : : // collect the elements
1075 [ + + ]: 445 : while (srv.getKind() == Kind::SET_UNION)
1076 : : {
1077 [ - + ][ - + ]: 217 : Assert(srv[1].getKind() == Kind::SET_SINGLETON);
[ - - ]
1078 : 217 : elements.push_back(srv[1][0]);
1079 : 217 : srv = srv[0];
1080 : : }
1081 [ - + ][ - + ]: 228 : Assert(srv.getKind() == Kind::SET_SINGLETON);
[ - - ]
1082 : 228 : elements.push_back(srv[0]);
1083 : : // check if we need to do matching, for literals like ( tuple( v ) in
1084 : : // S )
1085 : 228 : Node t = d_setm_range_lit[q][v][0];
1086 [ + + ]: 228 : if (t != v)
1087 : : {
1088 : 157 : std::vector<Node> elements_tmp;
1089 : 314 : elements_tmp.insert(
1090 : 157 : elements_tmp.end(), elements.begin(), elements.end());
1091 : 157 : elements.clear();
1092 [ + + ]: 459 : for (unsigned i = 0; i < elements_tmp.size(); i++)
1093 : : {
1094 : : // do matching to determine v -> u
1095 : 604 : Node u = matchBoundVar(v, t, elements_tmp[i]);
1096 [ + - ]: 604 : Trace("bound-int-rsi-debug")
1097 : 0 : << " unification : " << elements_tmp[i] << " = " << t
1098 : 302 : << " yields " << v << " -> " << u << std::endl;
1099 [ + - ]: 302 : if (!u.isNull())
1100 : : {
1101 : 302 : elements.push_back(u);
1102 : : }
1103 : 302 : }
1104 : 157 : }
1105 : 228 : }
1106 : 232 : return true;
1107 : : }
1108 : 239 : }
1109 [ + + ]: 268 : else if (bvt == BOUND_FIXED_SET)
1110 : : {
1111 : : std::map<Node, std::vector<Node> >::iterator it =
1112 : 82 : d_fixed_set_gr_range[q].find(v);
1113 [ + + ]: 82 : if (it != d_fixed_set_gr_range[q].end())
1114 : : {
1115 [ + + ]: 166 : for (unsigned i = 0; i < it->second.size(); i++)
1116 : : {
1117 : 104 : elements.push_back(it->second[i]);
1118 : : }
1119 : : }
1120 : 82 : it = d_fixed_set_ngr_range[q].find(v);
1121 [ + + ]: 82 : if (it != d_fixed_set_ngr_range[q].end())
1122 : : {
1123 : 52 : std::vector<Node> vars;
1124 : 52 : std::vector<Node> subs;
1125 [ + + ]: 52 : if (getRsiSubsitution(q, v, vars, subs, rsi))
1126 : : {
1127 [ + + ]: 98 : for (unsigned i = 0; i < it->second.size(); i++)
1128 : : {
1129 : 54 : Node t = it->second[i].substitute(
1130 : 54 : vars.begin(), vars.end(), subs.begin(), subs.end());
1131 : 54 : elements.push_back(t);
1132 : 54 : }
1133 : 44 : return true;
1134 : : }
1135 : : else
1136 : : {
1137 : 8 : return false;
1138 : : }
1139 : 52 : }
1140 : : else
1141 : : {
1142 : 30 : return true;
1143 : : }
1144 : : }
1145 : : else
1146 : : {
1147 : 186 : return false;
1148 : : }
1149 : : }
1150 : : else
1151 : : {
1152 : : // no change required
1153 : 310 : return true;
1154 : : }
1155 : : }
1156 : :
1157 : : /**
1158 : : * Attribute true for quantifiers that have been internally generated and
1159 : : * should be processed with the bounded integers module, e.g. quantified
1160 : : * formulas from reductions of string operators.
1161 : : *
1162 : : * Currently, this attribute is used for indicating that E-matching should
1163 : : * not be applied, as E-matching should not be applied to quantifiers
1164 : : * generated internally.
1165 : : *
1166 : : * This attribute can potentially be generalized to an identifier indicating
1167 : : * the internal source of the quantified formula (of which strings reduction
1168 : : * is one possibility).
1169 : : */
1170 : : struct BoundedQuantAttributeId
1171 : : {
1172 : : };
1173 : : typedef expr::Attribute<BoundedQuantAttributeId, bool> BoundedQuantAttribute;
1174 : : /**
1175 : : * Mapping to a dummy node for marking an attribute on internal quantified
1176 : : * formulas. This ensures that reductions are deterministic.
1177 : : */
1178 : : struct QInternalVarAttributeId
1179 : : {
1180 : : };
1181 : : typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
1182 : :
1183 : 1364 : Node BoundedIntegers::mkBoundedForall(NodeManager* nm, Node bvl, Node body)
1184 : : {
1185 : : QInternalVarAttribute qiva;
1186 : 1364 : Node qvar;
1187 [ + + ]: 1364 : if (bvl.hasAttribute(qiva))
1188 : : {
1189 : 430 : qvar = bvl.getAttribute(qiva);
1190 : : }
1191 : : else
1192 : : {
1193 : 934 : qvar = NodeManager::mkDummySkolem("qinternal", nm->booleanType());
1194 : : // this dummy variable marks that the quantified formula is internal
1195 : 934 : qvar.setAttribute(BoundedQuantAttribute(), true);
1196 : : // remember the dummy variable
1197 : 934 : bvl.setAttribute(qiva, qvar);
1198 : : }
1199 : : // make the internal attribute, and put it in a singleton list
1200 : 1364 : Node ip = nm->mkNode(Kind::INST_ATTRIBUTE, qvar);
1201 : 1364 : Node ipl = nm->mkNode(Kind::INST_PATTERN_LIST, ip);
1202 : : // make the overall formula
1203 : 2728 : return nm->mkNode(Kind::FORALL, bvl, body, ipl);
1204 : 1364 : }
1205 : :
1206 : 25444 : bool BoundedIntegers::isBoundedForallAttribute(Node var)
1207 : : {
1208 : 25444 : return var.getAttribute(BoundedQuantAttribute());
1209 : : }
1210 : :
1211 : : } // namespace quantifiers
1212 : : } // namespace theory
1213 : : } // namespace cvc5::internal
|
