src/theory/quantifiers/fmf/bounded_integers.cpp

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