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