GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fmf/bounded_integers.cpp Lines: 487 521 93.5 %
Date: 2021-03-23 Branches: 1218 2690 45.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bounded_integers.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Bounded integers module
13
 **
14
 ** This class manages integer bounds for quantifiers
15
 **/
16
17
#include "theory/quantifiers/fmf/bounded_integers.h"
18
19
#include "expr/dtype_cons.h"
20
#include "expr/node_algorithm.h"
21
#include "options/quantifiers_options.h"
22
#include "theory/arith/arith_msum.h"
23
#include "theory/datatypes/theory_datatypes_utils.h"
24
#include "theory/decision_manager.h"
25
#include "theory/quantifiers/first_order_model.h"
26
#include "theory/quantifiers/fmf/model_engine.h"
27
#include "theory/quantifiers/term_enumeration.h"
28
#include "theory/quantifiers/term_util.h"
29
#include "theory/quantifiers_engine.h"
30
#include "theory/theory_engine.h"
31
32
using namespace CVC4;
33
using namespace std;
34
using namespace CVC4::theory;
35
using namespace CVC4::theory::quantifiers;
36
using namespace CVC4::kind;
37
38
315
BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
39
    Node r,
40
    context::Context* c,
41
    context::Context* u,
42
    Valuation valuation,
43
315
    bool isProxy)
44
315
    : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u)
45
{
46
315
  if( options::fmfBoundLazy() ){
47
4
    d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
48
  }else{
49
311
    d_proxy_range = r;
50
  }
51
315
  if( !isProxy ){
52
303
    Trace("bound-int") << "Introduce proxy " << d_proxy_range << " for " << d_range << std::endl;
53
  }
54
315
}
55
1057
Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n)
56
{
57
1057
  NodeManager* nm = NodeManager::currentNM();
58
2114
  Node cn = nm->mkConst(Rational(n == 0 ? 0 : n - 1));
59
2114
  return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn);
60
}
61
62
1165
Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
63
{
64
1165
  if (d_range == d_proxy_range)
65
  {
66
1161
    return Node::null();
67
  }
68
4
  unsigned curr = 0;
69
4
  if (!getAssertedLiteralIndex(curr))
70
  {
71
    return Node::null();
72
  }
73
4
  if (d_ranges_proxied.find(curr) != d_ranges_proxied.end())
74
  {
75
    return Node::null();
76
  }
77
4
  d_ranges_proxied[curr] = true;
78
4
  NodeManager* nm = NodeManager::currentNM();
79
8
  Node currLit = getLiteral(curr);
80
  Node lem =
81
      nm->mkNode(EQUAL,
82
                 currLit,
83
8
                 nm->mkNode(curr == 0 ? LT : LEQ,
84
                            d_range,
85
16
                            nm->mkConst(Rational(curr == 0 ? 0 : curr - 1))));
86
4
  return lem;
87
}
88
89
611
BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
90
                                 QuantifiersState& qs,
91
                                 QuantifiersInferenceManager& qim,
92
                                 QuantifiersRegistry& qr,
93
611
                                 DecisionManager* dm)
94
611
    : QuantifiersModule(qs, qim, qr, qe), d_dm(dm)
95
{
96
611
}
97
98
1222
BoundedIntegers::~BoundedIntegers() {}
99
100
708
void BoundedIntegers::presolve() {
101
708
  d_bnd_it.clear();
102
708
}
103
104
5865
bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) {
105
5865
  if( visited.find( b )==visited.end() ){
106
5479
    visited[b] = true;
107
5479
    if( b.getKind()==BOUND_VARIABLE ){
108
597
      if( !isBound( f, b ) ){
109
314
        return true;
110
      }
111
    }else{
112
8601
      for( unsigned i=0; i<b.getNumChildren(); i++ ){
113
4065
        if( hasNonBoundVar( f, b[i], visited ) ){
114
346
          return true;
115
        }
116
      }
117
    }
118
  }
119
5205
  return false;
120
}
121
1800
bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
122
3600
  std::map< Node, bool > visited;
123
3600
  return hasNonBoundVar( f, b, visited );
124
}
125
126
511
bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ) {
127
511
  if( n.getKind()==EQUAL ){
128
1439
    for( unsigned i=0; i<2; i++ ){
129
1918
      Node t = n[i];
130
986
      if( !hasNonBoundVar( q, n[1-i] ) ){
131
698
        if( t==v ){
132
24
          v_cases.push_back( n[1-i] );
133
24
          return true;
134
674
        }else if( v.isNull() && t.getKind()==BOUND_VARIABLE ){
135
30
          v = t;
136
30
          v_cases.push_back( n[1-i] );
137
30
          return true;
138
        }
139
      }
140
    }
141
  }
142
457
  return false;
143
}
144
145
104
void BoundedIntegers::processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ){
146
104
  if( visited.find( n )==visited.end() ){
147
104
    visited[n] = true;
148
104
    if( n.getKind()==BOUND_VARIABLE && !isBound( q, n ) ){
149
39
      bvs.push_back( n );
150
    //injective operators
151
65
    }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
152
60
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
153
36
        processMatchBoundVars( q, n[i], bvs, visited );
154
      }
155
    }
156
  }
157
104
}
158
159
5346
void BoundedIntegers::process( Node q, Node n, bool pol,
160
                               std::map< Node, unsigned >& bound_lit_type_map,
161
                               std::map< int, std::map< Node, Node > >& bound_lit_map,
162
                               std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
163
                               std::map< int, std::map< Node, Node > >& bound_int_range_term,
164
                               std::map< Node, std::vector< Node > >& bound_fixed_set ){
165
5346
  if( n.getKind()==OR || n.getKind()==AND ){
166
1081
    if( (n.getKind()==OR)==pol ){
167
3642
      for( unsigned i=0; i<n.getNumChildren(); i++) {
168
2787
        process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
169
      }
170
    }else{
171
      //if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn }
172
452
      Node conj = n;
173
226
      if( !pol ){
174
        conj = TermUtil::simpleNegate( conj );
175
      }
176
226
      Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl;
177
226
      Assert(conj.getKind() == AND);
178
452
      Node v;
179
452
      std::vector< Node > v_cases;
180
226
      bool success = true;
181
276
      for( unsigned i=0; i<conj.getNumChildren(); i++ ){
182
252
        if( conj[i].getKind()==NOT && processEqDisjunct( q, conj[i][0], v, v_cases ) ){
183
          //continue
184
        }else{
185
202
          Trace("bound-int-debug") << "...failed due to " << conj[i] << std::endl;
186
202
          success = false;
187
202
          break;
188
        }
189
      }
190
226
      if( success && !isBound( q, v ) ){
191
10
        Trace("bound-int-debug") << "Success with variable " << v << std::endl;
192
10
        bound_lit_type_map[v] = BOUND_FIXED_SET;
193
10
        bound_lit_map[3][v] = n;
194
10
        bound_lit_pol_map[3][v] = pol;
195
10
        bound_fixed_set[v].clear();
196
10
        bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() );
197
      }
198
    }
199
4265
  }else if( n.getKind()==EQUAL ){
200
752
    if( !pol ){
201
      // non-applied DER on x != t, x can be bound to { t }
202
866
      Node v;
203
866
      std::vector< Node > v_cases;
204
433
      if( processEqDisjunct( q, n, v, v_cases ) ){
205
4
        if( !isBound( q, v ) ){
206
2
          bound_lit_type_map[v] = BOUND_FIXED_SET;
207
2
          bound_lit_map[3][v] = n;
208
2
          bound_lit_pol_map[3][v] = pol;
209
2
          Assert(v_cases.size() == 1);
210
2
          bound_fixed_set[v].clear();
211
2
          bound_fixed_set[v].push_back( v_cases[0] );
212
        }
213
      }
214
    }
215
3513
  }else if( n.getKind()==NOT ){
216
1557
    process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
217
1956
  }else if( n.getKind()==GEQ ){
218
1548
    if( n[0].getType().isInteger() ){
219
3088
      std::map< Node, Node > msum;
220
1544
      if (ArithMSum::getMonomialSumLit(n, msum))
221
      {
222
1544
        Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is monomial sum : " << std::endl;
223
1544
        ArithMSum::debugPrintMonomialSum(msum, "bound-int-debug");
224
4628
        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
225
3084
          if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){
226
            //if not bound in another way
227
746
            if( bound_lit_type_map.find( it->first )==bound_lit_type_map.end() || bound_lit_type_map[it->first] == BOUND_INT_RANGE ){
228
1484
              Node veq;
229
742
              if (ArithMSum::isolate(it->first, msum, veq, GEQ) != 0)
230
              {
231
1484
                Node n1 = veq[0];
232
1484
                Node n2 = veq[1];
233
742
                if(pol){
234
                  //flip
235
335
                  n1 = veq[1];
236
335
                  n2 = veq[0];
237
335
                  if( n1.getKind()==BOUND_VARIABLE ){
238
6
                    n2 = ArithMSum::offset(n2, 1);
239
                  }else{
240
329
                    n1 = ArithMSum::offset(n1, -1);
241
                  }
242
335
                  veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
243
                }
244
742
                Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
245
1484
                Node t = n1==it->first ? n2 : n1;
246
742
                if( !hasNonBoundVar( q, t ) ) {
247
720
                  Trace("bound-int-debug") << "The bound is relevant." << std::endl;
248
720
                  int loru = n1==it->first ? 0 : 1;
249
720
                  bound_lit_type_map[it->first] = BOUND_INT_RANGE;
250
720
                  bound_int_range_term[loru][it->first] = t;
251
720
                  bound_lit_map[loru][it->first] = n;
252
720
                  bound_lit_pol_map[loru][it->first] = pol;
253
                }else{
254
22
                  Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
255
                }
256
              }
257
            }
258
          }
259
        }
260
      }
261
    }
262
408
  }else if( n.getKind()==MEMBER ){
263
72
    if( !pol && !hasNonBoundVar( q, n[1] ) ){
264
136
      std::vector< Node > bound_vars;
265
136
      std::map< Node, bool > visited;
266
68
      processMatchBoundVars( q, n[0], bound_vars, visited );
267
107
      for( unsigned i=0; i<bound_vars.size(); i++ ){
268
78
        Node v = bound_vars[i];
269
39
        Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
270
39
        bound_lit_type_map[v] = BOUND_SET_MEMBER;
271
39
        bound_lit_map[2][v] = n;
272
39
        bound_lit_pol_map[2][v] = pol;
273
      }
274
    }
275
  }else{
276
336
    Assert(n.getKind() != LEQ && n.getKind() != LT && n.getKind() != GT);
277
  }
278
5346
}
279
280
8938
bool BoundedIntegers::needsCheck( Theory::Effort e ) {
281
8938
  return e==Theory::EFFORT_LAST_CALL;
282
}
283
284
2493
void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
285
{
286
2493
  if (quant_e != QEFFORT_STANDARD)
287
  {
288
1642
    return;
289
  }
290
851
  Trace("bint-engine") << "---Bounded Integers---" << std::endl;
291
851
  bool addedLemma = false;
292
  // make sure proxies are up-to-date with range
293
2016
  for (const Node& r : d_ranges)
294
  {
295
2330
    Node prangeLem = d_rms[r]->proxyCurrentRangeLemma();
296
1165
    if (!prangeLem.isNull())
297
    {
298
8
      Trace("bound-int-lemma")
299
4
          << "*** bound int : proxy lemma : " << prangeLem << std::endl;
300
4
      d_qim.addPendingLemma(prangeLem, InferenceId::UNKNOWN);
301
4
      addedLemma = true;
302
    }
303
  }
304
851
  Trace("bint-engine") << "   addedLemma = " << addedLemma << std::endl;
305
}
306
519
void BoundedIntegers::setBoundedVar(Node q, Node v, BoundVarType bound_type)
307
{
308
519
  d_bound_type[q][v] = bound_type;
309
519
  d_set_nums[q][v] = d_set[q].size();
310
519
  d_set[q].push_back( v );
311
1038
  Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v
312
519
                         << std::endl;
313
519
}
314
315
499
void BoundedIntegers::checkOwnership(Node f)
316
{
317
  //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
318
499
  Trace("bound-int") << "check ownership quantifier " << f << std::endl;
319
499
  NodeManager* nm = NodeManager::currentNM();
320
321
  bool success;
322
1002
  do{
323
2004
    std::map< Node, unsigned > bound_lit_type_map;
324
2004
    std::map< int, std::map< Node, Node > > bound_lit_map;
325
2004
    std::map< int, std::map< Node, bool > > bound_lit_pol_map;
326
2004
    std::map< int, std::map< Node, Node > > bound_int_range_term;
327
2004
    std::map< Node, std::vector< Node > > bound_fixed_set;
328
1002
    success = false;
329
1002
    process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
330
    //for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
331
1406
    for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){
332
808
      Node v = it->first;
333
404
      if( !isBound( f, v ) ){
334
404
        bool setBoundVar = false;
335
404
        if( it->second==BOUND_INT_RANGE ){
336
          //must have both
337
361
          std::map<Node, Node>& blm0 = bound_lit_map[0];
338
361
          std::map<Node, Node>& blm1 = bound_lit_map[1];
339
361
          if (blm0.find(v) != blm0.end() && blm1.find(v) != blm1.end())
340
          {
341
341
            setBoundedVar( f, v, BOUND_INT_RANGE );
342
341
            setBoundVar = true;
343
1023
            for( unsigned b=0; b<2; b++ ){
344
              //set the bounds
345
682
              Assert(bound_int_range_term[b].find(v)
346
                     != bound_int_range_term[b].end());
347
682
              d_bounds[b][f][v] = bound_int_range_term[b][v];
348
            }
349
682
            Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]);
350
341
            d_range[f][v] = Rewriter::rewrite(r);
351
341
            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;
352
          }
353
43
        }else if( it->second==BOUND_SET_MEMBER ){
354
          // only handles infinite element types currently (cardinality is not
355
          // supported for finite element types #1123). Regardless, this is
356
          // typically not a limitation since this variable can be bound in a
357
          // standard way below since its type is finite.
358
31
          if (!v.getType().isInterpretedFinite())
359
          {
360
31
            setBoundedVar(f, v, BOUND_SET_MEMBER);
361
31
            setBoundVar = true;
362
31
            d_setm_range[f][v] = bound_lit_map[2][v][1];
363
31
            d_setm_range_lit[f][v] = bound_lit_map[2][v];
364
31
            d_range[f][v] = nm->mkNode(CARD, d_setm_range[f][v]);
365
62
            Trace("bound-int") << "Variable " << v
366
31
                               << " is bound because of set membership literal "
367
31
                               << bound_lit_map[2][v] << std::endl;
368
          }
369
12
        }else if( it->second==BOUND_FIXED_SET ){
370
12
          setBoundedVar(f, v, BOUND_FIXED_SET);
371
12
          setBoundVar = true;
372
34
          for (unsigned i = 0; i < bound_fixed_set[v].size(); i++)
373
          {
374
44
            Node t = bound_fixed_set[v][i];
375
22
            if (expr::hasBoundVar(t))
376
            {
377
6
              d_fixed_set_ngr_range[f][v].push_back(t);
378
            }
379
            else
380
            {
381
16
              d_fixed_set_gr_range[f][v].push_back(t);
382
            }
383
          }
384
24
          Trace("bound-int") << "Variable " << v
385
12
                             << " is bound because of disequality conjunction "
386
12
                             << bound_lit_map[3][v] << std::endl;
387
        }
388
404
        if( setBoundVar ){
389
384
          success = true;
390
          //set Attributes on literals
391
1152
          for( unsigned b=0; b<2; b++ ){
392
768
            std::map<Node, Node>& blm = bound_lit_map[b];
393
768
            if (blm.find(v) != blm.end())
394
            {
395
682
              std::map<Node, bool>& blmp = bound_lit_pol_map[b];
396
              // WARNING_CANDIDATE:
397
              // This assertion may fail. We intentionally do not enable this in
398
              // production as it is considered safe for this to fail. We fail
399
              // the assertion in debug mode to have this instance raised to
400
              // our attention.
401
682
              Assert(blmp.find(v) != blmp.end());
402
              BoundIntLitAttribute bila;
403
682
              bound_lit_map[b][v].setAttribute(bila, blmp[v] ? 1 : 0);
404
            }
405
            else
406
            {
407
86
              Assert(it->second != BOUND_INT_RANGE);
408
            }
409
          }
410
        }
411
      }
412
    }
413
1002
    if( !success ){
414
      //resort to setting a finite bound on a variable
415
1254
      for( unsigned i=0; i<f[0].getNumChildren(); i++) {
416
755
        if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
417
285
          TypeNode tn = f[0][i].getType();
418
483
          if ((tn.isSort() && tn.isInterpretedFinite())
419
573
              || d_qreg.getQuantifiersBoundInference().mayComplete(tn))
420
          {
421
135
            success = true;
422
135
            setBoundedVar( f, f[0][i], BOUND_FINITE );
423
135
            break;
424
          }
425
        }
426
      }
427
    }
428
  }while( success );
429
430
499
  if( Trace.isOn("bound-int") ){
431
    Trace("bound-int") << "Bounds are : " << std::endl;
432
    for( unsigned i=0; i<f[0].getNumChildren(); i++) {
433
      Node v = f[0][i];
434
      if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){
435
        Assert(d_bound_type[f].find(v) != d_bound_type[f].end());
436
        if( d_bound_type[f][v]==BOUND_INT_RANGE ){
437
          Trace("bound-int") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
438
        }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
439
          if( d_setm_range_lit[f][v][0]==v ){
440
            Trace("bound-int") << "  " << v << " in " << d_setm_range[f][v] << std::endl;
441
          }else{
442
            Trace("bound-int") << "  " << v << " unifiable in " << d_setm_range_lit[f][v] << std::endl;
443
          }
444
        }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
445
          Trace("bound-int") << "  " << v << " in { ";
446
          for (TNode fnr : d_fixed_set_ngr_range[f][v])
447
          {
448
            Trace("bound-int") << fnr << " ";
449
          }
450
          for (TNode fgr : d_fixed_set_gr_range[f][v])
451
          {
452
            Trace("bound-int") << fgr << " ";
453
          }
454
          Trace("bound-int") << "}" << std::endl;
455
        }else if( d_bound_type[f][v]==BOUND_FINITE ){
456
          Trace("bound-int") << "  " << v << " has small finite type." << std::endl;
457
        }else{
458
          Trace("bound-int") << "  " << v << " has unknown bound." << std::endl;
459
          Assert(false);
460
        }
461
      }else{
462
        Trace("bound-int") << "  " << "*** " << v << " is unbounded." << std::endl;
463
      }
464
    }
465
  }
466
467
499
  bool bound_success = true;
468
1016
  for( unsigned i=0; i<f[0].getNumChildren(); i++) {
469
559
    if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
470
42
      Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl;
471
42
      bound_success = false;
472
42
      break;
473
    }
474
  }
475
476
499
  if( bound_success ){
477
457
    d_bound_quants.push_back( f );
478
974
    for( unsigned i=0; i<d_set[f].size(); i++) {
479
1034
      Node v = d_set[f][i];
480
517
      std::map< Node, Node >::iterator itr = d_range[f].find( v );
481
517
      if( itr != d_range[f].end() ){
482
740
        Node r = itr->second;
483
370
        Assert(!r.isNull());
484
370
        bool isProxy = false;
485
370
        if (expr::hasBoundVar(r))
486
        {
487
          // introduce a new bound
488
          Node new_range = NodeManager::currentNM()->mkSkolem(
489
24
              "bir", r.getType(), "bound for term");
490
12
          d_nground_range[f][v] = r;
491
12
          d_range[f][v] = new_range;
492
12
          r = new_range;
493
12
          isProxy = true;
494
        }
495
370
        if( !r.isConst() ){
496
345
          if (d_rms.find(r) == d_rms.end())
497
          {
498
315
            Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
499
315
            d_ranges.push_back( r );
500
945
            d_rms[r].reset(
501
                new IntRangeDecisionHeuristic(r,
502
315
                                              d_qstate.getSatContext(),
503
315
                                              d_qstate.getUserContext(),
504
315
                                              d_qstate.getValuation(),
505
315
                                              isProxy));
506
630
            d_dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
507
315
                                   d_rms[r].get());
508
          }
509
        }
510
      }
511
    }
512
  }
513
499
}
514
515
3509
bool BoundedIntegers::isBound(Node q, Node v) const
516
{
517
3509
  std::map<Node, std::vector<Node> >::const_iterator its = d_set.find(q);
518
3509
  if (its == d_set.end())
519
  {
520
1443
    return false;
521
  }
522
4132
  return std::find(its->second.begin(), its->second.end(), v)
523
6198
         != its->second.end();
524
}
525
526
6762
BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const
527
{
528
  std::map<Node, std::map<Node, BoundVarType> >::const_iterator itb =
529
6762
      d_bound_type.find(q);
530
6762
  if (itb == d_bound_type.end())
531
  {
532
    return BOUND_NONE;
533
  }
534
6762
  std::map<Node, BoundVarType>::const_iterator it = itb->second.find(v);
535
6762
  if (it == itb->second.end())
536
  {
537
22
    return BOUND_NONE;
538
  }
539
6740
  return it->second;
540
}
541
542
3373
void BoundedIntegers::getBoundVarIndices(Node q,
543
                                         std::vector<unsigned>& indices) const
544
{
545
3373
  std::map<Node, std::vector<Node> >::const_iterator it = d_set.find(q);
546
3373
  if (it != d_set.end())
547
  {
548
7802
    for (const Node& v : it->second)
549
    {
550
4437
      indices.push_back(TermUtil::getVariableNum(q, v));
551
    }
552
  }
553
3373
}
554
555
4264
void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
556
4264
  l = d_bounds[0][f][v];
557
4264
  u = d_bounds[1][f][v];
558
4264
  if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){
559
    //get the substitution
560
2384
    std::vector< Node > vars;
561
2384
    std::vector< Node > subs;
562
1192
    if( getRsiSubsitution( f, v, vars, subs, rsi ) ){
563
1156
      u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
564
1156
      l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
565
    }else{
566
36
      u = Node::null();
567
36
      l = Node::null();
568
    }
569
  }
570
4264
}
571
572
2150
void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
573
2150
  getBounds( f, v, rsi, l, u );
574
2150
  Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
575
2150
  if( !l.isNull() ){
576
2114
    l = d_quantEngine->getModel()->getValue( l );
577
  }
578
2150
  if( !u.isNull() ){
579
2114
    u = d_quantEngine->getModel()->getValue( u );
580
  }
581
2150
  Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
582
2150
  return;
583
}
584
585
768
bool BoundedIntegers::isGroundRange(Node q, Node v)
586
{
587
768
  if (isBound(q, v))
588
  {
589
768
    if (d_bound_type[q][v] == BOUND_INT_RANGE)
590
    {
591
1872
      return !expr::hasBoundVar(getLowerBound(q, v))
592
1872
             && !expr::hasBoundVar(getUpperBound(q, v));
593
    }
594
144
    else if (d_bound_type[q][v] == BOUND_SET_MEMBER)
595
    {
596
12
      return !expr::hasBoundVar(d_setm_range[q][v]);
597
    }
598
132
    else if (d_bound_type[q][v] == BOUND_FIXED_SET)
599
    {
600
132
      return !d_fixed_set_ngr_range[q][v].empty();
601
    }
602
  }
603
  return false;
604
}
605
606
67
Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) {
607
67
  Node sr = d_setm_range[q][v];
608
67
  if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){
609
16
    Trace("bound-int-rsi-debug")
610
8
        << sr << " is non-ground, apply substitution..." << std::endl;
611
    //get the substitution
612
16
    std::vector< Node > vars;
613
16
    std::vector< Node > subs;
614
8
    if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
615
8
      Trace("bound-int-rsi-debug")
616
4
          << "  apply " << vars << " -> " << subs << std::endl;
617
4
      sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
618
    }else{
619
4
      sr = Node::null();
620
    }
621
  }
622
67
  return sr;
623
}
624
625
67
Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
626
134
  Node sr = getSetRange( q, v, rsi );
627
67
  if (sr.isNull())
628
  {
629
4
    return sr;
630
  }
631
63
  Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
632
63
  Assert(!expr::hasFreeVar(sr));
633
126
  Node sro = sr;
634
63
  sr = d_quantEngine->getModel()->getValue(sr);
635
  // if non-constant, then sr does not occur in the model, we fail
636
63
  if (!sr.isConst())
637
  {
638
    return Node::null();
639
  }
640
63
  Trace("bound-int-rsi") << "Value is " << sr << std::endl;
641
63
  if (sr.getKind() == EMPTYSET)
642
  {
643
2
    return sr;
644
  }
645
61
  NodeManager* nm = NodeManager::currentNM();
646
122
  Node nsr;
647
122
  TypeNode tne = sr.getType().getSetElementType();
648
649
  // we can use choice functions for canonical symbolic instantiations
650
61
  unsigned srCard = 0;
651
119
  while (sr.getKind() == UNION)
652
  {
653
29
    srCard++;
654
29
    sr = sr[0];
655
  }
656
61
  Assert(sr.getKind() == SINGLETON);
657
61
  srCard++;
658
  // choices[i] stores the canonical symbolic representation of the (i+1)^th
659
  // element of sro
660
122
  std::vector<Node> choices;
661
122
  Node srCardN = nm->mkNode(CARD, sro);
662
122
  Node choice_i;
663
151
  for (unsigned i = 0; i < srCard; i++)
664
  {
665
90
    if (i == d_setm_choice[sro].size())
666
    {
667
34
      choice_i = nm->mkBoundVar(tne);
668
34
      choices.push_back(choice_i);
669
68
      Node cBody = nm->mkNode(MEMBER, choice_i, sro);
670
34
      if (choices.size() > 1)
671
      {
672
12
        cBody = nm->mkNode(AND, cBody, nm->mkNode(DISTINCT, choices));
673
      }
674
34
      choices.pop_back();
675
68
      Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i);
676
68
      Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i)));
677
34
      choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody));
678
34
      d_setm_choice[sro].push_back(choice_i);
679
    }
680
90
    Assert(i < d_setm_choice[sro].size());
681
90
    choice_i = d_setm_choice[sro][i];
682
90
    choices.push_back(choice_i);
683
180
    Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i);
684
90
    if (nsr.isNull())
685
    {
686
61
      nsr = sChoiceI;
687
    }
688
    else
689
    {
690
29
      nsr = nm->mkNode(UNION, nsr, sChoiceI);
691
    }
692
  }
693
  // turns the concrete model value of sro into a canonical representation
694
  //   e.g.
695
  // singleton(0) union singleton(1)
696
  //   becomes
697
  // C1 union ( witness y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) )
698
  // where C1 = ( witness x. card(S)<=0 OR x in S ).
699
61
  Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl;
700
61
  return nsr;
701
}
702
703
1252
bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) {
704
705
1252
  Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
706
1252
  Assert(d_set_nums[q].find(v) != d_set_nums[q].end());
707
1252
  int vindex = d_set_nums[q][v];
708
1252
  Assert(d_set_nums[q][v] == vindex);
709
1252
  Trace("bound-int-rsi-debug") << "  index order is " << vindex << std::endl;
710
  //must take substitution for all variables that are iterating at higher level
711
2784
  for( int i=0; i<vindex; i++) {
712
1532
    Assert(d_set_nums[q][d_set[q][i]] == i);
713
1532
    Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
714
1532
    int vo = rsi->getVariableOrder(i);
715
1532
    Assert(q[0][vo] == d_set[q][i]);
716
3064
    Node t = rsi->getCurrentTerm(vo, true);
717
1532
    Trace("bound-int-rsi") << "term : " << t << std::endl;
718
1532
    vars.push_back( d_set[q][i] );
719
1532
    subs.push_back( t );
720
  }
721
722
  //check if it has been instantiated
723
1252
  if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){
724
48
    if( d_bound_type[q][v]==BOUND_INT_RANGE || d_bound_type[q][v]==BOUND_SET_MEMBER ){
725
      //must add the lemma
726
80
      Node nn = d_nground_range[q][v];
727
40
      nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
728
80
      Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
729
40
      Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
730
40
      d_qim.lemma(lem, InferenceId::UNKNOWN);
731
    }
732
48
    return false;
733
  }else{
734
1204
    return true;
735
  }
736
}
737
738
80
Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
739
80
  if( t==v ){
740
32
    return e;
741
48
  }else if( t.getKind()==kind::APPLY_CONSTRUCTOR ){
742
32
    if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
743
      if( t.getOperator() != e.getOperator() ) {
744
        return Node::null();
745
      }
746
    }
747
32
    NodeManager* nm = NodeManager::currentNM();
748
32
    const DType& dt = datatypes::utils::datatypeOf(t.getOperator());
749
32
    unsigned index = datatypes::utils::indexOf(t.getOperator());
750
48
    for( unsigned i=0; i<t.getNumChildren(); i++ ){
751
64
      Node u;
752
48
      if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
753
        u = matchBoundVar( v, t[i], e[i] );
754
      }else{
755
        Node se = nm->mkNode(APPLY_SELECTOR_TOTAL,
756
96
                             dt[index].getSelectorInternal(e.getType(), i),
757
192
                             e);
758
48
        u = matchBoundVar( v, t[i], se );
759
      }
760
48
      if( !u.isNull() ){
761
32
        return u;
762
      }
763
    }
764
  }
765
16
  return Node::null();
766
}
767
768
2581
bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
769
2581
  if( initial || !isGroundRange( q, v ) ){
770
2311
    elements.clear();
771
2311
    BoundVarType bvt = getBoundVarType(q, v);
772
2311
    if( bvt==BOUND_INT_RANGE ){
773
4300
      Node l, u;
774
2150
      getBoundValues( q, v, rsi, l, u );
775
2150
      if( l.isNull() || u.isNull() ){
776
36
        Trace("bound-int-warn") << "WARNING: Could not find integer bounds in model for " << v << " in " << q << std::endl;
777
        //failed, abort the iterator
778
36
        return false;
779
      }else{
780
2114
        Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl;
781
4228
        Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
782
4228
        Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
783
4228
        Node tl = l;
784
4228
        Node tu = u;
785
2114
        getBounds( q, v, rsi, tl, tu );
786
2114
        Assert(!tl.isNull() && !tu.isNull());
787
2114
        if (ra.isConst() && ra.getConst<bool>())
788
        {
789
2114
          long rr = range.getConst<Rational>().getNumerator().getLong()+1;
790
2114
          Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
791
15026
          for (long k = 0; k < rr; k++)
792
          {
793
25824
            Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) );
794
12912
            t = Rewriter::rewrite( t );
795
12912
            elements.push_back( t );
796
          }
797
2114
          return true;
798
        }else{
799
          Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << v << "." << std::endl;
800
          return false;
801
        }
802
      }
803
161
    }else if( bvt==BOUND_SET_MEMBER  ){
804
134
      Node srv = getSetRangeValue( q, v, rsi );
805
67
      if( srv.isNull() ){
806
4
        Trace("bound-int-warn") << "WARNING: Could not find set bound in model for " << v << " in " << q << std::endl;
807
4
        return false;
808
      }else{
809
63
        Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
810
63
        if( srv.getKind()!=EMPTYSET ){
811
          //collect the elements
812
119
          while( srv.getKind()==UNION ){
813
29
            Assert(srv[1].getKind() == kind::SINGLETON);
814
29
            elements.push_back( srv[1][0] );
815
29
            srv = srv[0];
816
          }
817
61
          Assert(srv.getKind() == kind::SINGLETON);
818
61
          elements.push_back( srv[0] );
819
          //check if we need to do matching, for literals like ( tuple( v ) in S )
820
122
          Node t = d_setm_range_lit[q][v][0];
821
61
          if( t!=v ){
822
32
            std::vector< Node > elements_tmp;
823
16
            elements_tmp.insert( elements_tmp.end(), elements.begin(), elements.end() );
824
16
            elements.clear();
825
48
            for( unsigned i=0; i<elements_tmp.size(); i++ ){
826
              //do matching to determine v -> u
827
64
              Node u = matchBoundVar( v, t, elements_tmp[i] );
828
32
              Trace("bound-int-rsi-debug") << "  unification : " << elements_tmp[i] << " = " << t << " yields " << v << " -> " << u << std::endl;
829
32
              if( !u.isNull() ){
830
32
                elements.push_back( u );
831
              }
832
            }
833
          }
834
        }
835
63
        return true;
836
      }
837
94
    }else if( bvt==BOUND_FIXED_SET ){
838
86
      std::map< Node, std::vector< Node > >::iterator it = d_fixed_set_gr_range[q].find( v );
839
86
      if( it!=d_fixed_set_gr_range[q].end() ){
840
174
        for( unsigned i=0; i<it->second.size(); i++ ){
841
108
          elements.push_back( it->second[i] );
842
        }
843
      }
844
86
      it = d_fixed_set_ngr_range[q].find( v );
845
86
      if( it!=d_fixed_set_ngr_range[q].end() ){
846
104
        std::vector< Node > vars;
847
104
        std::vector< Node > subs;
848
52
        if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
849
98
          for( unsigned i=0; i<it->second.size(); i++ ){
850
108
            Node t = it->second[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
851
54
            elements.push_back( t );
852
          }
853
44
          return true;
854
        }else{
855
8
          return false;
856
        }
857
      }else{
858
34
        return true;
859
      }
860
    }else{
861
8
      return false;
862
    }
863
  }else{
864
    //no change required
865
270
    return true;
866
  }
867
26685
}