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 : 1107 : BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
42 : 1107 : Env& env, Node r, Valuation valuation, bool isProxy)
43 : : : DecisionStrategyFmf(env, valuation),
44 : 1107 : d_range(r),
45 : 1107 : d_ranges_proxied(userContext())
46 : : {
47 : : // we require a proxy if the term is set.card
48 [ + + ][ + + ]: 1107 : 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 : 1043 : d_proxy_range = r;
56 : : }
57 [ + + ]: 1107 : if( !isProxy ){
58 [ + - ]: 980 : Trace("bound-int") << "Introduce proxy " << d_proxy_range << " for " << d_range << std::endl;
59 : : }
60 : 1107 : }
61 : 3122 : Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n)
62 : : {
63 : 3122 : NodeManager* nm = nodeManager();
64 [ + + ]: 3122 : Node cn = nm->mkConstInt(Rational(n == 0 ? 0 : n - 1));
65 [ + + ]: 6244 : return nm->mkNode(n == 0 ? Kind::LT : Kind::LEQ, d_proxy_range, cn);
66 : 3122 : }
67 : :
68 : 2950 : Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
69 : : {
70 [ + + ]: 2950 : if (d_range == d_proxy_range)
71 : : {
72 : 2577 : return Node::null();
73 : : }
74 : 373 : unsigned curr = 0;
75 [ + + ]: 373 : if (!getAssertedLiteralIndex(curr))
76 : : {
77 : 2 : return Node::null();
78 : : }
79 [ + + ]: 371 : if (d_ranges_proxied.find(curr) != d_ranges_proxied.end())
80 : : {
81 : 154 : return Node::null();
82 : : }
83 : 217 : d_ranges_proxied[curr] = true;
84 : 217 : NodeManager* nm = nodeManager();
85 : 217 : Node currLit = getLiteral(curr);
86 : 217 : Node lit;
87 [ + + ]: 217 : if (d_range.getKind() == Kind::SET_CARD)
88 : : {
89 : : // Instead of introducing (set.card s) < n, we introduce the literal
90 : : // s = characteristicSet(s, n-1) for n>0 and false for n=0. We do this
91 : : // to avoid introducing set.card.
92 [ + + ]: 210 : if (curr == 0)
93 : : {
94 : 57 : lit = nodeManager()->mkConst(false);
95 : : }
96 : : else
97 : : {
98 : : Node cset = sets::NormalForm::getCharacteristicSet(
99 : 153 : nodeManager(), d_range[0], curr - 1);
100 : 153 : lit = d_range[0].eqNode(cset);
101 : 153 : }
102 : : }
103 : : else
104 : : {
105 [ + - ]: 21 : lit = nm->mkNode(curr == 0 ? Kind::LT : Kind::LEQ,
106 : 7 : d_range,
107 [ - + ]: 21 : nm->mkConstInt(Rational(curr == 0 ? 0 : curr - 1)));
108 : : }
109 : 434 : Node lem = nm->mkNode(Kind::EQUAL, currLit, lit);
110 : 217 : return lem;
111 : 217 : }
112 : :
113 : 32832 : BoundedIntegers::BoundedIntegers(Env& env,
114 : : QuantifiersState& qs,
115 : : QuantifiersInferenceManager& qim,
116 : : QuantifiersRegistry& qr,
117 : 32832 : TermRegistry& tr)
118 [ + + ]: 98496 : : QuantifiersModule(env, qs, qim, qr, tr)
119 : : {
120 : 32832 : }
121 : :
122 [ + - ][ + + ]: 130220 : BoundedIntegers::~BoundedIntegers() {}
123 : :
124 : 29400 : void BoundedIntegers::presolve() {
125 : 29400 : d_bnd_it.clear();
126 : 29400 : }
127 : :
128 : 24922 : bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) {
129 [ + + ]: 24922 : if( visited.find( b )==visited.end() ){
130 : 20976 : visited[b] = true;
131 [ + + ]: 20976 : if (b.getKind() == Kind::BOUND_VARIABLE)
132 : : {
133 [ + + ]: 1649 : if( !isBound( f, b ) ){
134 : 856 : return true;
135 : : }
136 : : }
137 : : else
138 : : {
139 [ + + ]: 37811 : for( unsigned i=0; i<b.getNumChildren(); i++ ){
140 [ + + ]: 19961 : if( hasNonBoundVar( f, b[i], visited ) ){
141 : 1477 : return true;
142 : : }
143 : : }
144 : : }
145 : : }
146 : 22589 : return false;
147 : : }
148 : 4961 : bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
149 : 4961 : std::map< Node, bool > visited;
150 : 9922 : return hasNonBoundVar( f, b, visited );
151 : 4961 : }
152 : :
153 : 1004 : bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ) {
154 [ + + ]: 1004 : if (n.getKind() == Kind::EQUAL)
155 : : {
156 [ + + ]: 2910 : for( unsigned i=0; i<2; i++ ){
157 : 1964 : Node t = n[i];
158 [ + + ]: 1964 : if( !hasNonBoundVar( q, n[1-i] ) ){
159 [ + + ]: 1353 : if( t==v ){
160 : 24 : v_cases.push_back( n[1-i] );
161 : 24 : return true;
162 : : }
163 [ + + ][ + + ]: 1329 : else if (v.isNull() && t.getKind() == Kind::BOUND_VARIABLE)
[ + + ]
164 : : {
165 : 26 : v = t;
166 : 26 : v_cases.push_back( n[1-i] );
167 : 26 : return true;
168 : : }
169 : : }
170 [ + + ]: 1964 : }
171 : : }
172 : 954 : return false;
173 : : }
174 : :
175 : 400 : void BoundedIntegers::processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ){
176 [ + - ]: 400 : if( visited.find( n )==visited.end() ){
177 : 400 : visited[n] = true;
178 : 400 : if (n.getKind() == Kind::BOUND_VARIABLE && !isBound(q, n))
179 : : {
180 : 125 : bvs.push_back( n );
181 : : //injective operators
182 : : }
183 [ + + ]: 275 : else if (n.getKind() == Kind::APPLY_CONSTRUCTOR)
184 : : {
185 [ + + ]: 308 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
186 : 172 : processMatchBoundVars( q, n[i], bvs, visited );
187 : : }
188 : : }
189 : : }
190 : 400 : }
191 : :
192 : 16338 : void BoundedIntegers::process( Node q, Node n, bool pol,
193 : : std::map< Node, unsigned >& bound_lit_type_map,
194 : : std::map< int, std::map< Node, Node > >& bound_lit_map,
195 : : std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
196 : : std::map< int, std::map< Node, Node > >& bound_int_range_term,
197 : : std::map< Node, std::vector< Node > >& bound_fixed_set ){
198 [ + + ][ + + ]: 16338 : if (n.getKind() == Kind::OR || n.getKind() == Kind::AND)
[ + + ]
199 : : {
200 [ + + ]: 3425 : if ((n.getKind() == Kind::OR) == pol)
201 : : {
202 [ + + ]: 11354 : for( unsigned i=0; i<n.getNumChildren(); i++) {
203 : 8843 : process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
204 : : }
205 : : }
206 : : else
207 : : {
208 : : //if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn }
209 : 914 : Node conj = n;
210 [ - + ]: 914 : if( !pol ){
211 : 0 : conj = TermUtil::simpleNegate( conj );
212 : : }
213 [ + - ]: 914 : Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl;
214 [ - + ][ - + ]: 914 : Assert(conj.getKind() == Kind::AND);
[ - - ]
215 : 914 : Node v;
216 : 914 : std::vector< Node > v_cases;
217 : 914 : bool success = true;
218 [ + + ]: 964 : for( unsigned i=0; i<conj.getNumChildren(); i++ ){
219 [ + + ][ - - ]: 940 : if (conj[i].getKind() == Kind::NOT
220 : 940 : && processEqDisjunct(q, conj[i][0], v, v_cases))
221 : : {
222 : : //continue
223 : : }
224 : : else
225 : : {
226 [ + - ][ - + ]: 890 : Trace("bound-int-debug") << "...failed due to " << conj[i] << std::endl;
[ - - ]
227 : 890 : success = false;
228 : 890 : break;
229 : : }
230 : : }
231 : 914 : if( success && !isBound( q, v ) ){
232 [ + - ]: 10 : Trace("bound-int-debug") << "Success with variable " << v << std::endl;
233 : 10 : bound_lit_type_map[v] = BOUND_FIXED_SET;
234 : 10 : bound_lit_map[3][v] = n;
235 : 10 : bound_lit_pol_map[3][v] = pol;
236 : 10 : bound_fixed_set[v].clear();
237 : 10 : bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() );
238 : : }
239 : 914 : }
240 : : }
241 [ + + ]: 12913 : else if (n.getKind() == Kind::EQUAL)
242 : : {
243 [ + + ]: 1618 : if( !pol ){
244 : : // non-applied DER on x != t, x can be bound to { t }
245 : 746 : Node v;
246 : 746 : std::vector< Node > v_cases;
247 [ - + ]: 746 : if( processEqDisjunct( q, n, v, v_cases ) ){
248 [ - - ]: 0 : if( !isBound( q, v ) ){
249 : 0 : bound_lit_type_map[v] = BOUND_FIXED_SET;
250 : 0 : bound_lit_map[3][v] = n;
251 : 0 : bound_lit_pol_map[3][v] = pol;
252 : 0 : Assert(v_cases.size() == 1);
253 : 0 : bound_fixed_set[v].clear();
254 : 0 : bound_fixed_set[v].push_back( v_cases[0] );
255 : : }
256 : : }
257 : 746 : }
258 : : }
259 [ + + ]: 11295 : else if (n.getKind() == Kind::NOT)
260 : : {
261 : 4718 : process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
262 : : }
263 [ + + ]: 6577 : else if (n.getKind() == Kind::GEQ)
264 : : {
265 [ + + ]: 5462 : if( n[0].getType().isInteger() ){
266 : 5457 : std::map< Node, Node > msum;
267 [ + - ]: 5457 : if (ArithMSum::getMonomialSumLit(n, msum))
268 : : {
269 : 5457 : NodeManager* nm = nodeManager();
270 [ + - ]: 5457 : Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is monomial sum : " << std::endl;
271 : 5457 : ArithMSum::debugPrintMonomialSum(msum, "bound-int-debug");
272 [ + + ]: 16487 : for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
273 [ + + ]: 19939 : if (!it->first.isNull() && it->first.getKind() == Kind::BOUND_VARIABLE
274 : 30969 : && !isBound(q, it->first))
275 : : {
276 : : //if not bound in another way
277 [ + + ][ + + ]: 2797 : if( bound_lit_type_map.find( it->first )==bound_lit_type_map.end() || bound_lit_type_map[it->first] == BOUND_INT_RANGE ){
[ + + ]
278 : 2762 : Node veq;
279 [ + - ]: 2762 : if (ArithMSum::isolate(it->first, msum, veq, Kind::GEQ) != 0)
280 : : {
281 : 2762 : Node n1 = veq[0];
282 : 2762 : Node n2 = veq[1];
283 [ + + ]: 2762 : if(pol){
284 : : //flip
285 : 1219 : n1 = veq[1];
286 : 1219 : n2 = veq[0];
287 [ + + ]: 1219 : if (n1.getKind() == Kind::BOUND_VARIABLE)
288 : : {
289 : 2 : n2 = nm->mkNode(Kind::ADD, n2, nm->mkConstInt(Rational(1)));
290 : : }
291 : : else
292 : : {
293 : : n1 =
294 : 1217 : nm->mkNode(Kind::ADD, n1, nm->mkConstInt(Rational(-1)));
295 : : }
296 : 1219 : veq = nm->mkNode(Kind::GEQ, n1, n2);
297 : : }
298 [ + - ]: 2762 : Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
299 [ + + ]: 2762 : Node t = n1==it->first ? n2 : n1;
300 [ + + ]: 2762 : if( !hasNonBoundVar( q, t ) ) {
301 [ + - ]: 2524 : Trace("bound-int-debug") << "The bound is relevant." << std::endl;
302 [ + + ]: 2524 : int loru = n1==it->first ? 0 : 1;
303 : 2524 : bound_lit_type_map[it->first] = BOUND_INT_RANGE;
304 : 2524 : bound_int_range_term[loru][it->first] = t;
305 : 2524 : bound_lit_map[loru][it->first] = n;
306 : 2524 : bound_lit_pol_map[loru][it->first] = pol;
307 : : }else{
308 [ + - ]: 238 : Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
309 : : }
310 : 2762 : }
311 : 2762 : }
312 : : }
313 : : }
314 : : }
315 : 5457 : }
316 : : }
317 [ + + ]: 1115 : else if (n.getKind() == Kind::SET_MEMBER)
318 : : {
319 : : // Note this is incomplete when combined with cardinality constraints,
320 : : // since we may introduce slack elements during model construction.
321 : : // Here, fmfBound should be enabled, otherwise the incompleteness check
322 : : // in the theory of sets is out of sync.
323 [ - + ][ - + ]: 235 : Assert(options().quantifiers.fmfBound);
[ - - ]
324 : 235 : if( !pol && !hasNonBoundVar( q, n[1] ) ){
325 : 228 : std::vector< Node > bound_vars;
326 : 228 : std::map< Node, bool > visited;
327 : 228 : processMatchBoundVars( q, n[0], bound_vars, visited );
328 [ + + ]: 353 : for( unsigned i=0; i<bound_vars.size(); i++ ){
329 : 125 : Node v = bound_vars[i];
330 [ + - ]: 125 : Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
331 : 125 : bound_lit_type_map[v] = BOUND_SET_MEMBER;
332 : 125 : bound_lit_map[2][v] = n;
333 : 125 : bound_lit_pol_map[2][v] = pol;
334 : 125 : }
335 : 228 : }
336 : : }
337 : : else
338 : : {
339 [ + - ][ + - ]: 880 : Assert(n.getKind() != Kind::LEQ && n.getKind() != Kind::LT
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
340 : : && n.getKind() != Kind::GT);
341 : : }
342 : 16338 : }
343 : :
344 : 80342 : bool BoundedIntegers::needsCheck( Theory::Effort e ) {
345 : 80342 : return e==Theory::EFFORT_LAST_CALL;
346 : : }
347 : :
348 : 28337 : void BoundedIntegers::check(CVC5_UNUSED Theory::Effort e, QEffort quant_e)
349 : : {
350 [ + + ]: 28337 : if (quant_e != QEFFORT_STANDARD)
351 : : {
352 : 18544 : return;
353 : : }
354 [ + - ]: 9793 : Trace("bint-engine") << "---Bounded Integers---" << std::endl;
355 : 9793 : bool addedLemma = false;
356 : : // make sure proxies are up-to-date with range
357 [ + + ]: 12743 : for (const Node& r : d_ranges)
358 : : {
359 : 2950 : Node prangeLem = d_rms[r]->proxyCurrentRangeLemma();
360 [ + + ]: 2950 : if (!prangeLem.isNull())
361 : : {
362 [ + - ]: 434 : Trace("bound-int-lemma")
363 : 217 : << "*** bound int : proxy lemma : " << prangeLem << std::endl;
364 : 217 : d_qim.addPendingLemma(prangeLem, InferenceId::QUANTIFIERS_BINT_PROXY);
365 : 217 : addedLemma = true;
366 : : }
367 : 2950 : }
368 [ + - ]: 9793 : Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl;
369 : : }
370 : 1471 : void BoundedIntegers::setBoundedVar(Node q, Node v, BoundVarType bound_type)
371 : : {
372 : 1471 : d_bound_type[q][v] = bound_type;
373 : 1471 : d_set_nums[q][v] = d_set[q].size();
374 : 1471 : d_set[q].push_back( v );
375 [ + - ]: 2942 : Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v
376 : 1471 : << std::endl;
377 : 1471 : }
378 : :
379 : 25356 : void BoundedIntegers::checkOwnership(Node f)
380 : : {
381 : : //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
382 [ + - ]: 25356 : Trace("bound-int") << "check ownership quantifier " << f << std::endl;
383 : :
384 : : // determine if we should look at the quantified formula at all
385 [ + + ]: 25356 : if (!options().quantifiers.fmfBound)
386 : : {
387 : : // only applying it to internal quantifiers
388 : 24935 : QuantAttributes& qattr = d_qreg.getQuantAttributes();
389 [ + + ]: 24935 : if (!qattr.isQuantBounded(f))
390 : : {
391 [ + - ]: 24025 : Trace("bound-int") << "...not bounded, skip" << std::endl;
392 : 24025 : return;
393 : : }
394 : : }
395 : :
396 : 1331 : NodeManager* nm = nodeManager();
397 : :
398 : : bool success;
399 [ + + ]: 2777 : do{
400 : 2777 : std::map< Node, unsigned > bound_lit_type_map;
401 : 2777 : std::map< int, std::map< Node, Node > > bound_lit_map;
402 : 2777 : std::map< int, std::map< Node, bool > > bound_lit_pol_map;
403 : 2777 : std::map< int, std::map< Node, Node > > bound_int_range_term;
404 : 2777 : std::map< Node, std::vector< Node > > bound_fixed_set;
405 : 2777 : success = false;
406 : 2777 : process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
407 : : //for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
408 [ + + ]: 4184 : for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){
409 : 1407 : Node v = it->first;
410 [ + - ]: 1407 : if( !isBound( f, v ) ){
411 : 1407 : bool setBoundVar = false;
412 [ + + ]: 1407 : if( it->second==BOUND_INT_RANGE ){
413 : : //must have both
414 : 1284 : std::map<Node, Node>& blm0 = bound_lit_map[0];
415 : 1284 : std::map<Node, Node>& blm1 = bound_lit_map[1];
416 [ + + ][ + + ]: 1284 : if (blm0.find(v) != blm0.end() && blm1.find(v) != blm1.end())
[ + + ]
417 : : {
418 : 1157 : setBoundedVar( f, v, BOUND_INT_RANGE );
419 : 1157 : setBoundVar = true;
420 [ + + ]: 3471 : for( unsigned b=0; b<2; b++ ){
421 : : //set the bounds
422 [ - + ][ - + ]: 2314 : Assert(bound_int_range_term[b].find(v)
[ - - ]
423 : : != bound_int_range_term[b].end());
424 : 2314 : d_bounds[b][f][v] = bound_int_range_term[b][v];
425 : : }
426 : : Node r =
427 : 2314 : nm->mkNode(Kind::SUB, d_bounds[1][f][v], d_bounds[0][f][v]);
428 : 1157 : d_range[f][v] = rewrite(r);
429 [ + - ]: 1157 : Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
430 : 1157 : }
431 [ + + ]: 123 : }else if( it->second==BOUND_SET_MEMBER ){
432 : 113 : setBoundedVar(f, v, BOUND_SET_MEMBER);
433 : 113 : setBoundVar = true;
434 : 113 : d_setm_range[f][v] = bound_lit_map[2][v][1];
435 : 113 : d_setm_range_lit[f][v] = bound_lit_map[2][v];
436 : 113 : Node cardTerm = nm->mkNode(Kind::SET_CARD, d_setm_range[f][v]);
437 : : // Note that we avoid reasoning about cardinality by eagerly
438 : : // eliminating set.card for literals as they are introduced.
439 : 113 : d_range[f][v] = cardTerm;
440 [ + - ]: 226 : Trace("bound-int") << "Variable " << v
441 : 0 : << " is bound because of set membership literal "
442 : 113 : << bound_lit_map[2][v] << std::endl;
443 [ + - ]: 123 : }else if( it->second==BOUND_FIXED_SET ){
444 : 10 : setBoundedVar(f, v, BOUND_FIXED_SET);
445 : 10 : setBoundVar = true;
446 [ + + ]: 30 : for (unsigned i = 0; i < bound_fixed_set[v].size(); i++)
447 : : {
448 : 20 : Node t = bound_fixed_set[v][i];
449 [ + + ]: 20 : if (expr::hasBoundVar(t))
450 : : {
451 : 6 : d_fixed_set_ngr_range[f][v].push_back(t);
452 : : }
453 : : else
454 : : {
455 : 14 : d_fixed_set_gr_range[f][v].push_back(t);
456 : : }
457 : 20 : }
458 [ + - ]: 20 : Trace("bound-int") << "Variable " << v
459 : 0 : << " is bound because of disequality conjunction "
460 : 10 : << bound_lit_map[3][v] << std::endl;
461 : : }
462 [ + + ]: 1407 : if( setBoundVar ){
463 : 1280 : success = true;
464 : : //set Attributes on literals
465 [ + + ]: 3840 : for( unsigned b=0; b<2; b++ ){
466 : 2560 : std::map<Node, Node>& blm = bound_lit_map[b];
467 [ + + ]: 2560 : if (blm.find(v) != blm.end())
468 : : {
469 : 2321 : std::map<Node, bool>& blmp = bound_lit_pol_map[b];
470 : : // WARNING_CANDIDATE:
471 : : // This assertion may fail. We intentionally do not enable this in
472 : : // production as it is considered safe for this to fail. We fail
473 : : // the assertion in debug mode to have this instance raised to
474 : : // our attention.
475 [ - + ][ - + ]: 2321 : Assert(blmp.find(v) != blmp.end());
[ - - ]
476 : : BoundIntLitAttribute bila;
477 [ + + ]: 2321 : bound_lit_map[b][v].setAttribute(bila, blmp[v] ? 1 : 0);
478 : : }
479 : : else
480 : : {
481 [ - + ][ - + ]: 239 : Assert(it->second != BOUND_INT_RANGE);
[ - - ]
482 : : }
483 : : }
484 : : }
485 : : }
486 : 1407 : }
487 [ + + ]: 2777 : if( !success ){
488 : : //resort to setting a finite bound on a variable
489 [ + + ]: 3130 : for( unsigned i=0; i<f[0].getNumChildren(); i++) {
490 [ + + ]: 1799 : if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
491 : 566 : TypeNode tn = f[0][i].getType();
492 [ + + ][ + + ]: 332 : if ((tn.isUninterpretedSort() && d_env.isFiniteType(tn))
[ - - ]
493 [ + + ][ + + ]: 332 : || d_qreg.getQuantifiersBoundInference().mayComplete(tn))
[ + + ][ + + ]
[ - - ]
494 : : {
495 : 191 : success = true;
496 : 191 : setBoundedVar( f, f[0][i], BOUND_FINITE );
497 : 191 : break;
498 : : }
499 [ + + ]: 283 : }
500 : : }
501 : : }
502 : 2777 : }while( success );
503 : :
504 [ - + ]: 1331 : if( TraceIsOn("bound-int") ){
505 [ - - ]: 0 : Trace("bound-int") << "Bounds are : " << std::endl;
506 [ - - ]: 0 : for( unsigned i=0; i<f[0].getNumChildren(); i++) {
507 : 0 : Node v = f[0][i];
508 [ - - ]: 0 : if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){
509 : 0 : Assert(d_bound_type[f].find(v) != d_bound_type[f].end());
510 [ - - ]: 0 : if( d_bound_type[f][v]==BOUND_INT_RANGE ){
511 [ - - ]: 0 : Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
512 [ - - ]: 0 : }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
513 [ - - ]: 0 : if( d_setm_range_lit[f][v][0]==v ){
514 [ - - ]: 0 : Trace("bound-int") << " " << v << " in " << d_setm_range[f][v] << std::endl;
515 : : }else{
516 [ - - ]: 0 : Trace("bound-int") << " " << v << " unifiable in " << d_setm_range_lit[f][v] << std::endl;
517 : : }
518 [ - - ]: 0 : }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
519 [ - - ]: 0 : Trace("bound-int") << " " << v << " in { ";
520 [ - - ]: 0 : for (TNode fnr : d_fixed_set_ngr_range[f][v])
521 : : {
522 [ - - ]: 0 : Trace("bound-int") << fnr << " ";
523 : 0 : }
524 [ - - ]: 0 : for (TNode fgr : d_fixed_set_gr_range[f][v])
525 : : {
526 [ - - ]: 0 : Trace("bound-int") << fgr << " ";
527 : 0 : }
528 [ - - ]: 0 : Trace("bound-int") << "}" << std::endl;
529 [ - - ]: 0 : }else if( d_bound_type[f][v]==BOUND_FINITE ){
530 [ - - ]: 0 : Trace("bound-int") << " " << v << " has small finite type." << std::endl;
531 : : }else{
532 [ - - ]: 0 : Trace("bound-int") << " " << v << " has unknown bound." << std::endl;
533 : 0 : DebugUnhandled();
534 : : }
535 : : }else{
536 [ - - ]: 0 : Trace("bound-int") << " " << "*** " << v << " is unbounded." << std::endl;
537 : : }
538 : 0 : }
539 : : }
540 : :
541 : 1331 : bool bound_success = true;
542 [ + + ]: 2800 : for( unsigned i=0; i<f[0].getNumChildren(); i++) {
543 [ + + ]: 1537 : if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
544 : 68 : Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl;
545 : 68 : bound_success = false;
546 : 68 : break;
547 : : }
548 : : }
549 : :
550 [ + + ]: 1331 : if( bound_success ){
551 : 1263 : d_bound_quants.push_back( f );
552 : 1263 : DecisionManager* dm = d_qim.getDecisionManager();
553 [ + + ]: 2729 : for( unsigned i=0; i<d_set[f].size(); i++) {
554 : 1466 : Node v = d_set[f][i];
555 : 1466 : std::map< Node, Node >::iterator itr = d_range[f].find( v );
556 [ + + ]: 1466 : if( itr != d_range[f].end() ){
557 : 1268 : Node r = itr->second;
558 [ - + ][ - + ]: 1268 : Assert(!r.isNull());
[ - - ]
559 : 1268 : bool isProxy = false;
560 [ + + ]: 1268 : if (expr::hasBoundVar(r))
561 : : {
562 : : // introduce a new bound
563 : 254 : Node new_range = NodeManager::mkDummySkolem("bir", r.getType());
564 : 127 : d_nground_range[f][v] = r;
565 : 127 : d_range[f][v] = new_range;
566 : 127 : r = new_range;
567 : 127 : isProxy = true;
568 : 127 : }
569 [ + + ]: 1268 : if( !r.isConst() ){
570 [ + + ]: 1211 : if (d_rms.find(r) == d_rms.end())
571 : : {
572 [ + - ]: 1107 : Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
573 : 1107 : d_ranges.push_back( r );
574 : 2214 : d_rms[r].reset(new IntRangeDecisionHeuristic(
575 : 1107 : d_env, r, d_qstate.getValuation(), isProxy));
576 : 1107 : dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
577 : 1107 : d_rms[r].get());
578 : : }
579 : : }
580 : 1268 : }
581 : 1466 : }
582 : : }
583 : : }
584 : :
585 : 16219 : bool BoundedIntegers::isBound(Node q, Node v) const
586 : : {
587 : 16219 : std::map<Node, std::vector<Node> >::const_iterator its = d_set.find(q);
588 [ + + ]: 16219 : if (its == d_set.end())
589 : : {
590 : 10732 : return false;
591 : : }
592 : 5487 : return std::find(its->second.begin(), its->second.end(), v)
593 : 10974 : != its->second.end();
594 : : }
595 : :
596 : 10095 : BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const
597 : : {
598 : : std::map<Node, std::map<Node, BoundVarType> >::const_iterator itb =
599 : 10095 : d_bound_type.find(q);
600 [ + + ]: 10095 : if (itb == d_bound_type.end())
601 : : {
602 : 1852 : return BOUND_NONE;
603 : : }
604 : 8243 : std::map<Node, BoundVarType>::const_iterator it = itb->second.find(v);
605 [ + + ]: 8243 : if (it == itb->second.end())
606 : : {
607 : 346 : return BOUND_NONE;
608 : : }
609 : 7897 : return it->second;
610 : : }
611 : :
612 : 8713 : void BoundedIntegers::getBoundVarIndices(Node q,
613 : : std::vector<size_t>& indices) const
614 : : {
615 : 8713 : std::map<Node, std::vector<Node> >::const_iterator it = d_set.find(q);
616 [ + + ]: 8713 : if (it != d_set.end())
617 : : {
618 [ + + ]: 11632 : for (const Node& v : it->second)
619 : : {
620 : 6619 : indices.push_back(TermUtil::getVariableNum(q, v));
621 : : }
622 : : }
623 : 8713 : }
624 : :
625 : 5155 : void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
626 : 5155 : l = d_bounds[0][f][v];
627 : 5155 : u = d_bounds[1][f][v];
628 [ + + ]: 5155 : if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){
629 : : //get the substitution
630 : 1427 : std::vector< Node > vars;
631 : 1427 : std::vector< Node > subs;
632 [ + + ]: 1427 : if( getRsiSubsitution( f, v, vars, subs, rsi ) ){
633 : 1346 : u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
634 : 1346 : l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
635 : : }else{
636 : 81 : u = Node::null();
637 : 81 : l = Node::null();
638 : : }
639 : 1427 : }
640 : 5155 : }
641 : :
642 : 2618 : void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
643 : 2618 : getBounds( f, v, rsi, l, u );
644 [ + - ]: 2618 : Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
645 [ + + ]: 2618 : if( !l.isNull() ){
646 : 2537 : l = d_treg.getModel()->getValue(l);
647 : : }
648 [ + + ]: 2618 : if( !u.isNull() ){
649 : 2537 : u = d_treg.getModel()->getValue(u);
650 : : }
651 [ + - ]: 2618 : Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
652 : 2618 : return;
653 : : }
654 : :
655 : 834 : bool BoundedIntegers::isGroundRange(Node q, Node v)
656 : : {
657 [ + - ]: 834 : if (isBound(q, v))
658 : : {
659 [ + + ]: 834 : if (d_bound_type[q][v] == BOUND_INT_RANGE)
660 : : {
661 : 1300 : return !expr::hasBoundVar(getLowerBound(q, v))
662 : 1300 : && !expr::hasBoundVar(getUpperBound(q, v));
663 : : }
664 [ + + ]: 184 : else if (d_bound_type[q][v] == BOUND_SET_MEMBER)
665 : : {
666 : 52 : return !expr::hasBoundVar(d_setm_range[q][v]);
667 : : }
668 [ + - ]: 132 : else if (d_bound_type[q][v] == BOUND_FIXED_SET)
669 : : {
670 : 132 : return !d_fixed_set_ngr_range[q][v].empty();
671 : : }
672 : : }
673 : 0 : return false;
674 : : }
675 : :
676 : 239 : Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) {
677 : 239 : Node sr = d_setm_range[q][v];
678 [ + + ]: 239 : if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){
679 [ + - ]: 28 : Trace("bound-int-rsi-debug")
680 : 14 : << sr << " is non-ground, apply substitution..." << std::endl;
681 : : //get the substitution
682 : 14 : std::vector< Node > vars;
683 : 14 : std::vector< Node > subs;
684 [ + + ]: 14 : if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
685 [ + - ]: 14 : Trace("bound-int-rsi-debug")
686 : 7 : << " apply " << vars << " -> " << subs << std::endl;
687 : 7 : sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
688 : : }else{
689 : 7 : sr = Node::null();
690 : : }
691 : 14 : }
692 : 239 : return sr;
693 : 0 : }
694 : :
695 : 239 : Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
696 : 478 : Node sr = getSetRange( q, v, rsi );
697 [ + + ]: 239 : if (sr.isNull())
698 : : {
699 : 7 : return sr;
700 : : }
701 [ + - ]: 232 : Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
702 [ - + ][ - + ]: 232 : Assert(!expr::hasFreeVar(sr));
[ - - ]
703 : 232 : Node sro = sr;
704 : 232 : sr = d_treg.getModel()->getValue(sr);
705 : : // if non-constant, then sr does not occur in the model, we fail
706 [ - + ]: 232 : if (!sr.isConst())
707 : : {
708 : 0 : return Node::null();
709 : : }
710 [ + - ]: 232 : Trace("bound-int-rsi") << "Value is " << sr << std::endl;
711 [ + + ]: 232 : if (sr.getKind() == Kind::SET_EMPTY)
712 : : {
713 : 4 : return sr;
714 : : }
715 : : // we can use choice functions for canonical symbolic instantiations
716 : 228 : unsigned srCard = 0;
717 [ + + ]: 445 : while (sr.getKind() == Kind::SET_UNION)
718 : : {
719 [ - + ][ - + ]: 217 : Assert(sr[0].getKind() == Kind::SET_SINGLETON);
[ - - ]
720 : 217 : srCard++;
721 : 217 : sr = sr[1];
722 : : }
723 [ - + ][ - + ]: 228 : Assert(sr.getKind() == Kind::SET_SINGLETON);
[ - - ]
724 : 228 : srCard++;
725 [ + - ]: 228 : Trace("bound-int-rsi") << "...cardinality is " << srCard << std::endl;
726 : : // get the characteristic set
727 : 228 : Node nsr = sets::NormalForm::getCharacteristicSet(nodeManager(), sro, srCard);
728 : : // turns the concrete set value of sro into a canonical representation
729 : : // e.g.
730 : : // singleton(0) union singleton(1)
731 : : // becomes
732 : : // C1 union (set.singleton (set.choose (set.minus S C1)))
733 : : // where C1 = (set.singleton (set.choose S)).
734 [ + - ]: 228 : Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
735 : 228 : return nsr;
736 : 239 : }
737 : :
738 : 1493 : bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) {
739 : :
740 [ + - ]: 1493 : Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
741 [ - + ][ - + ]: 1493 : Assert(d_set_nums[q].find(v) != d_set_nums[q].end());
[ - - ]
742 : 1493 : int vindex = d_set_nums[q][v];
743 [ - + ][ - + ]: 1493 : Assert(d_set_nums[q][v] == vindex);
[ - - ]
744 [ + - ]: 1493 : Trace("bound-int-rsi-debug") << " index order is " << vindex << std::endl;
745 : : //must take substitution for all variables that are iterating at higher level
746 [ + + ]: 3266 : for( int i=0; i<vindex; i++) {
747 [ - + ][ - + ]: 1773 : Assert(d_set_nums[q][d_set[q][i]] == i);
[ - - ]
748 [ + - ]: 1773 : Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
749 : 1773 : int vo = rsi->getVariableOrder(i);
750 [ - + ][ - + ]: 1773 : Assert(q[0][vo] == d_set[q][i]);
[ - - ]
751 : 1773 : TypeNode tn = d_set[q][i].getType();
752 : : // If the type of tn is not closed enumerable, we must map the value back
753 : : // to a term that appears in the same equivalence class as the constant.
754 : : // Notice that this is to ensure that unhandled values (e.g. uninterpreted
755 : : // constants, datatype values) do not enter instantiations/lemmas, which
756 : : // can lead to refutation unsoundness. However, it is important that we
757 : : // conversely do *not* map terms to values in other cases. In particular,
758 : : // replacing a constant c with a term t can lead to solution unsoundness
759 : : // if we are instantiating a quantified formula that corresponds to a
760 : : // reduction for t, since then the reduction is using circular reasoning:
761 : : // the current value of t is being used to reason about the range of
762 : : // its axiomatization. This is limited to reductions in the theory of
763 : : // strings, which use quantification on integers only. Note this
764 : : // impacts only quantified formulas with 2+ dimensions and dependencies
765 : : // between dimensions, e.g. str.indexof_re reduction.
766 : 1773 : Node t = rsi->getCurrentTerm(vo, !tn.isClosedEnumerable());
767 [ + - ]: 1773 : Trace("bound-int-rsi") << "term : " << t << std::endl;
768 : 1773 : vars.push_back( d_set[q][i] );
769 : 1773 : subs.push_back( t );
770 : 1773 : }
771 : :
772 : : //check if it has been instantiated
773 [ + - ][ + + ]: 1493 : if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){
[ + + ]
774 [ + + ][ + + ]: 96 : if( d_bound_type[q][v]==BOUND_INT_RANGE || d_bound_type[q][v]==BOUND_SET_MEMBER ){
[ + + ]
775 : : //must add the lemma
776 : 88 : Node nn = d_nground_range[q][v];
777 : 88 : nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
778 : 176 : Node lem = nodeManager()->mkNode(Kind::LEQ, nn, d_range[q][v]);
779 [ + - ]: 88 : Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
780 : 88 : d_qim.lemma(lem, InferenceId::QUANTIFIERS_BINT_MIN_NG);
781 : 88 : }
782 : 96 : return false;
783 : : }else{
784 : 1397 : return true;
785 : : }
786 : : }
787 : :
788 : 680 : Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
789 [ + + ]: 680 : if( t==v ){
790 : 302 : return e;
791 : : }
792 [ + + ]: 378 : else if (t.getKind() == Kind::APPLY_CONSTRUCTOR)
793 : : {
794 [ - + ]: 302 : if (e.getKind() == Kind::APPLY_CONSTRUCTOR)
795 : : {
796 [ - - ]: 0 : if( t.getOperator() != e.getOperator() ) {
797 : 0 : return Node::null();
798 : : }
799 : : }
800 : 302 : const DType& dt = datatypes::utils::datatypeOf(t.getOperator());
801 : 302 : unsigned index = datatypes::utils::indexOf(t.getOperator());
802 : 302 : bool sharedSel = options().datatypes.dtSharedSelectors;
803 [ + - ]: 378 : for( unsigned i=0; i<t.getNumChildren(); i++ ){
804 : 378 : Node u;
805 [ - + ]: 378 : if (e.getKind() == Kind::APPLY_CONSTRUCTOR)
806 : : {
807 : 0 : u = matchBoundVar( v, t[i], e[i] );
808 : : }
809 : : else
810 : : {
811 : 378 : Node se = datatypes::utils::applySelector(dt[index], i, sharedSel, e);
812 : 378 : u = matchBoundVar( v, t[i], se );
813 : 378 : }
814 [ + + ]: 378 : if( !u.isNull() ){
815 : 302 : return u;
816 : : }
817 [ + + ]: 378 : }
818 : : }
819 : 76 : return Node::null();
820 : : }
821 : :
822 : 3429 : bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
823 : 3429 : if( initial || !isGroundRange( q, v ) ){
824 : 3119 : elements.clear();
825 : 3119 : BoundVarType bvt = getBoundVarType(q, v);
826 [ + + ]: 3119 : if( bvt==BOUND_INT_RANGE ){
827 : 2618 : Node l, u;
828 : 2618 : getBoundValues( q, v, rsi, l, u );
829 [ + + ][ - + ]: 2618 : if( l.isNull() || u.isNull() ){
[ + + ]
830 [ + - ]: 81 : Trace("bound-int-warn") << "WARNING: Could not find integer bounds in model for " << v << " in " << q << std::endl;
831 : : //failed, abort the iterator
832 : 81 : return false;
833 : : }else{
834 : 2537 : NodeManager* nm = nodeManager();
835 [ + - ]: 2537 : Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl;
836 : 5074 : Node range = rewrite(nm->mkNode(Kind::SUB, u, l));
837 [ - + ]: 2537 : if (!range.isConst())
838 : : {
839 [ - - ]: 0 : Trace("fmf-incomplete") << "Incomplete because of integer "
840 : 0 : "quantification, bounds are unknown for "
841 : 0 : << v << "." << std::endl;
842 : 0 : return false;
843 : : }
844 : 2537 : Rational rat = range.getConst<Rational>();
845 : : // 9999 is an arbitrary range past which we do not do exhaustive
846 : : // bounded instantation, based on the check below.
847 : 2537 : Node tl = l;
848 : 2537 : Node tu = u;
849 : 2537 : getBounds( q, v, rsi, tl, tu );
850 [ + - ][ + - ]: 2537 : Assert(!tl.isNull() && !tu.isNull());
[ - + ][ - + ]
[ - - ]
851 [ + - ]: 2537 : if (rat < Rational(9999))
852 : : {
853 : : // if negative, elements are empty
854 [ + + ]: 2537 : if (rat.sgn() >= 0)
855 : : {
856 : 2201 : long rr = rat.getNumerator().getLong() + 1;
857 [ + - ]: 4402 : Trace("bound-int-rsi")
858 : 2201 : << "Actual bound range is " << rr << std::endl;
859 [ + + ]: 10941 : for (long k = 0; k < rr; k++)
860 : : {
861 : 17480 : Node t = nm->mkNode(Kind::ADD, tl, nm->mkConstInt(Rational(k)));
862 : 8740 : t = rewrite(t);
863 : 8740 : elements.push_back(t);
864 : 8740 : }
865 : : }
866 : 2537 : return true;
867 : : }else{
868 [ - - ]: 0 : Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << v << "." << std::endl;
869 : 0 : return false;
870 : : }
871 : 2537 : }
872 [ + + ]: 3119 : }else if( bvt==BOUND_SET_MEMBER ){
873 : 478 : Node srv = getSetRangeValue( q, v, rsi );
874 [ + + ]: 239 : if( srv.isNull() ){
875 [ + - ]: 7 : Trace("bound-int-warn") << "WARNING: Could not find set bound in model for " << v << " in " << q << std::endl;
876 : 7 : return false;
877 : : }else{
878 [ + - ]: 232 : Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
879 [ + + ]: 232 : if (srv.getKind() != Kind::SET_EMPTY)
880 : : {
881 : : //collect the elements
882 [ + + ]: 445 : while (srv.getKind() == Kind::SET_UNION)
883 : : {
884 [ - + ][ - + ]: 217 : Assert(srv[1].getKind() == Kind::SET_SINGLETON);
[ - - ]
885 : 217 : elements.push_back( srv[1][0] );
886 : 217 : srv = srv[0];
887 : : }
888 [ - + ][ - + ]: 228 : Assert(srv.getKind() == Kind::SET_SINGLETON);
[ - - ]
889 : 228 : elements.push_back( srv[0] );
890 : : //check if we need to do matching, for literals like ( tuple( v ) in S )
891 : 228 : Node t = d_setm_range_lit[q][v][0];
892 [ + + ]: 228 : if( t!=v ){
893 : 157 : std::vector< Node > elements_tmp;
894 : 157 : elements_tmp.insert( elements_tmp.end(), elements.begin(), elements.end() );
895 : 157 : elements.clear();
896 [ + + ]: 459 : for( unsigned i=0; i<elements_tmp.size(); i++ ){
897 : : //do matching to determine v -> u
898 : 604 : Node u = matchBoundVar( v, t, elements_tmp[i] );
899 [ + - ]: 302 : Trace("bound-int-rsi-debug") << " unification : " << elements_tmp[i] << " = " << t << " yields " << v << " -> " << u << std::endl;
900 [ + - ]: 302 : if( !u.isNull() ){
901 : 302 : elements.push_back( u );
902 : : }
903 : 302 : }
904 : 157 : }
905 : 228 : }
906 : 232 : return true;
907 : : }
908 [ + + ]: 501 : }else if( bvt==BOUND_FIXED_SET ){
909 : 82 : std::map< Node, std::vector< Node > >::iterator it = d_fixed_set_gr_range[q].find( v );
910 [ + + ]: 82 : if( it!=d_fixed_set_gr_range[q].end() ){
911 [ + + ]: 166 : for( unsigned i=0; i<it->second.size(); i++ ){
912 : 104 : elements.push_back( it->second[i] );
913 : : }
914 : : }
915 : 82 : it = d_fixed_set_ngr_range[q].find( v );
916 [ + + ]: 82 : if( it!=d_fixed_set_ngr_range[q].end() ){
917 : 52 : std::vector< Node > vars;
918 : 52 : std::vector< Node > subs;
919 [ + + ]: 52 : if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
920 [ + + ]: 98 : for( unsigned i=0; i<it->second.size(); i++ ){
921 : 54 : Node t = it->second[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
922 : 54 : elements.push_back( t );
923 : 54 : }
924 : 44 : return true;
925 : : }else{
926 : 8 : return false;
927 : : }
928 : 52 : }else{
929 : 30 : return true;
930 : : }
931 : : }else{
932 : 180 : return false;
933 : : }
934 : : }else{
935 : : //no change required
936 : 310 : return true;
937 : : }
938 : : }
939 : :
940 : : /**
941 : : * Attribute true for quantifiers that have been internally generated and
942 : : * should be processed with the bounded integers module, e.g. quantified
943 : : * formulas from reductions of string operators.
944 : : *
945 : : * Currently, this attribute is used for indicating that E-matching should
946 : : * not be applied, as E-matching should not be applied to quantifiers
947 : : * generated internally.
948 : : *
949 : : * This attribute can potentially be generalized to an identifier indicating
950 : : * the internal source of the quantified formula (of which strings reduction
951 : : * is one possibility).
952 : : */
953 : : struct BoundedQuantAttributeId
954 : : {
955 : : };
956 : : typedef expr::Attribute<BoundedQuantAttributeId, bool> BoundedQuantAttribute;
957 : : /**
958 : : * Mapping to a dummy node for marking an attribute on internal quantified
959 : : * formulas. This ensures that reductions are deterministic.
960 : : */
961 : : struct QInternalVarAttributeId
962 : : {
963 : : };
964 : : typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
965 : :
966 : 1314 : Node BoundedIntegers::mkBoundedForall(NodeManager* nm, Node bvl, Node body)
967 : : {
968 : : QInternalVarAttribute qiva;
969 : 1314 : Node qvar;
970 [ + + ]: 1314 : if (bvl.hasAttribute(qiva))
971 : : {
972 : 406 : qvar = bvl.getAttribute(qiva);
973 : : }
974 : : else
975 : : {
976 : 908 : qvar = NodeManager::mkDummySkolem("qinternal", nm->booleanType());
977 : : // this dummy variable marks that the quantified formula is internal
978 : 908 : qvar.setAttribute(BoundedQuantAttribute(), true);
979 : : // remember the dummy variable
980 : 908 : bvl.setAttribute(qiva, qvar);
981 : : }
982 : : // make the internal attribute, and put it in a singleton list
983 : 1314 : Node ip = nm->mkNode(Kind::INST_ATTRIBUTE, qvar);
984 : 1314 : Node ipl = nm->mkNode(Kind::INST_PATTERN_LIST, ip);
985 : : // make the overall formula
986 : 2628 : return nm->mkNode(Kind::FORALL, bvl, body, ipl);
987 : 1314 : }
988 : :
989 : 37462 : bool BoundedIntegers::isBoundedForallAttribute(Node var)
990 : : {
991 : 37462 : return var.getAttribute(BoundedQuantAttribute());
992 : : }
993 : :
994 : : } // namespace quantifiers
995 : : } // namespace theory
996 : : } // namespace cvc5::internal
|
