src/theory/quantifiers/bounded_integers.cpp

   1 /*********************                                                        */
   2 /*! \file bounded_integers.cpp
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Bounded integers module
  13  **
  14  ** This class manages integer bounds for quantifiers
  15  **/
  16
  17 #include "theory/quantifiers/bounded_integers.h"
  18 #include "theory/quantifiers/quant_util.h"
  19 #include "theory/quantifiers/first_order_model.h"
  20 #include "theory/quantifiers/model_engine.h"
  21 #include "theory/quantifiers/term_database.h"
  22
  23 using namespace CVC4;
  24 using namespace std;
  25 using namespace CVC4::theory;
  26 using namespace CVC4::theory::quantifiers;
  27 using namespace CVC4::kind;
  28
  29 void BoundedIntegers::RangeModel::initialize() {
  30   //add initial split lemma
  31   Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
  32   ltr = Rewriter::rewrite( ltr );
  33   Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl;
  34   d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
  35   Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
  36   d_range_literal[-1] = ltr_lit;
  37   d_lit_to_range[ltr_lit] = -1;
  38   d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
  39   //register with bounded integers
  40   Trace("bound-int-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;
  41   d_bi->addLiteralFromRange(ltr_lit, d_range);
  42 }
  43
  44 void BoundedIntegers::RangeModel::assertNode(Node n) {
  45   bool pol = n.getKind()!=NOT;
  46   Node nlit = n.getKind()==NOT ? n[0] : n;
  47   if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){
  48     Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";
  49     Trace("bound-int-assert") << ", found literal " << nlit;
  50     Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;
  51     d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);
  52     if( pol!=d_lit_to_pol[nlit] ){
  53       //check if we need a new split?
  54       if( !d_has_range ){
  55         bool needsRange = true;
  56         for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
  57           if( d_range_assertions.find( it->first )==d_range_assertions.end() ){
  58             needsRange = false;
  59             break;
  60           }
  61         }
  62         if( needsRange ){
  63           allocateRange();
  64         }
  65       }
  66     }else{
  67       if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){
  68         Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;
  69         d_curr_range = d_lit_to_range[nlit];
  70       }
  71       //set the range
  72       d_has_range = true;
  73     }
  74   }else{
  75     Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;
  76     exit(0);
  77   }
  78 }
  79
  80 void BoundedIntegers::RangeModel::allocateRange() {
  81   d_curr_max++;
  82   int newBound = d_curr_max;
  83   Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
  84   //TODO: newBound should be chosen in a smarter way
  85   Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );
  86   ltr = Rewriter::rewrite( ltr );
  87   Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl;
  88   d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
  89   Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
  90   d_range_literal[newBound] = ltr_lit;
  91   d_lit_to_range[ltr_lit] = newBound;
  92   d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
  93   //register with bounded integers
  94   d_bi->addLiteralFromRange(ltr_lit, d_range);
  95 }
  96
  97 Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
  98   //request the current cardinality as a decision literal, if not already asserted
  99   for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
 100     int i = it->second;
 101     if( !d_has_range || i<d_curr_range ){
 102       Node rn = it->first;
 103       Assert( !rn.isNull() );
 104       if( d_range_assertions.find( rn )==d_range_assertions.end() ){
 105         if (!d_lit_to_pol[it->first]) {
 106           rn = rn.negate();
 107         }
 108         Trace("bound-int-dec-debug") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;
 109         return rn;
 110       }
 111     }
 112   }
 113   return Node::null();
 114 }
 115
 116
 117 BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :
 118 QuantifiersModule(qe), d_assertions(c){
 119
 120 }
 121
 122 bool BoundedIntegers::isBound( Node f, Node v ) {
 123   return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
 124 }
 125
 126 bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
 127   if( b.getKind()==BOUND_VARIABLE ){
 128     if( !isBound( f, b ) ){
 129       return true;
 130     }
 131   }else{
 132     for( unsigned i=0; i<b.getNumChildren(); i++ ){
 133       if( hasNonBoundVar( f, b[i] ) ){
 134         return true;
 135       }
 136     }
 137   }
 138   return false;
 139 }
 140
 141 void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
 142                                       std::map< int, std::map< Node, Node > >& bound_lit_map,
 143                                       std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) {
 144   if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
 145     std::map< Node, Node > msum;
 146     if (QuantArith::getMonomialSumLit( lit, msum )){
 147       Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
 148       for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
 149         Trace("bound-int-debug") << "  ";
 150         if( !it->second.isNull() ){
 151           Trace("bound-int-debug") << it->second;
 152           if( !it->first.isNull() ){
 153             Trace("bound-int-debug") << " * ";
 154           }
 155         }
 156         if( !it->first.isNull() ){
 157           Trace("bound-int-debug") << it->first;
 158         }
 159         Trace("bound-int-debug") << std::endl;
 160       }
 161       Trace("bound-int-debug") << std::endl;
 162       for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
 163         if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){
 164           Node veq;
 165           if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){
 166             Node n1 = veq[0];
 167             Node n2 = veq[1];
 168             if(pol){
 169               //flip
 170               n1 = veq[1];
 171               n2 = veq[0];
 172               if( n1.getKind()==BOUND_VARIABLE ){
 173                 n2 = QuantArith::offset( n2, 1 );
 174               }else{
 175                 n1 = QuantArith::offset( n1, -1 );
 176               }
 177               veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
 178             }
 179             Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
 180             Node t = n1==it->first ? n2 : n1;
 181             if( !hasNonBoundVar( f, t ) ) {
 182               Trace("bound-int-debug") << "The bound is relevant." << std::endl;
 183               int loru = n1==it->first ? 0 : 1;
 184               d_bounds[loru][f][it->first] = t;
 185               bound_lit_map[loru][it->first] = lit;
 186               bound_lit_pol_map[loru][it->first] = pol;
 187             }else{
 188               Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
 189             }
 190           }
 191         }
 192       }
 193     }
 194   }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
 195     Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
 196   }
 197 }
 198
 199 void BoundedIntegers::process( Node f, Node n, bool pol,
 200                                std::map< int, std::map< Node, Node > >& bound_lit_map,
 201                                std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){
 202   if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){
 203     for( unsigned i=0; i<n.getNumChildren(); i++) {
 204       process( f, n[i], pol, bound_lit_map, bound_lit_pol_map );
 205     }
 206   }else if( n.getKind()==NOT ){
 207     process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map );
 208   }else {
 209     processLiteral( f, n, pol, bound_lit_map, bound_lit_pol_map );
 210   }
 211 }
 212
 213 void BoundedIntegers::check( Theory::Effort e ) {
 214
 215 }
 216
 217
 218 void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
 219   d_lit_to_ranges[lit].push_back(r);
 220   //check if it is already asserted?
 221   if(d_assertions.find(lit)!=d_assertions.end()){
 222     d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() );
 223   }
 224 }
 225
 226 void BoundedIntegers::registerQuantifier( Node f ) {
 227   Trace("bound-int") << "Register quantifier " << f << std::endl;
 228   bool hasIntType = false;
 229   int finiteTypes = 0;
 230   std::map< Node, int > numMap;
 231   for( unsigned i=0; i<f[0].getNumChildren(); i++) {
 232     numMap[f[0][i]] = i;
 233     if( f[0][i].getType().isInteger() ){
 234       hasIntType = true;
 235     }
 236     else if( f[0][i].getType().isSort() || f[0][i].getType().getCardinality().isFinite() ){
 237       finiteTypes++;
 238     }
 239   }
 240   if( hasIntType ){
 241     bool success;
 242     do{
 243       std::map< int, std::map< Node, Node > > bound_lit_map;
 244       std::map< int, std::map< Node, bool > > bound_lit_pol_map;
 245       success = false;
 246       process( f, f[1], true, bound_lit_map, bound_lit_pol_map );
 247       for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
 248         Node v = it->first;
 249         if( !isBound(f,v) ){
 250           if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){
 251             d_set[f].push_back(v);
 252             d_set_nums[f].push_back(numMap[v]);
 253             success = true;
 254             //set Attributes on literals
 255             for( unsigned b=0; b<2; b++ ){
 256               Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() );
 257               Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() );
 258               BoundIntLitAttribute bila;
 259               bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 );
 260             }
 261             Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
 262           }
 263         }
 264       }
 265     }while( success );
 266     Trace("bound-int") << "Bounds are : " << std::endl;
 267     for( unsigned i=0; i<d_set[f].size(); i++) {
 268       Node v = d_set[f][i];
 269       Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
 270       d_range[f][v] = Rewriter::rewrite( r );
 271       Trace("bound-int") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
 272     }
 273     if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){
 274       d_bound_quants.push_back( f );
 275       for( unsigned i=0; i<d_set[f].size(); i++) {
 276         Node v = d_set[f][i];
 277         Node r = d_range[f][v];
 278         if( r.hasBoundVar() ){
 279           //introduce a new bound
 280           Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" );
 281           d_nground_range[f][v] = d_range[f][v];
 282           d_range[f][v] = new_range;
 283           r = new_range;
 284         }
 285         if( r.getKind()!=CONST_RATIONAL ){
 286           if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
 287             Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl;
 288             d_ranges.push_back( r );
 289             d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );
 290             d_rms[r]->initialize();
 291           }
 292         }
 293       }
 294     }else{
 295       Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl;
 296       //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl;
 297     }
 298   }
 299 }
 300
 301 void BoundedIntegers::assertNode( Node n ) {
 302   Trace("bound-int-assert") << "Assert " << n << std::endl;
 303   Node nlit = n.getKind()==NOT ? n[0] : n;
 304   if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){
 305     Trace("bound-int-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;
 306     for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) {
 307       Node r = d_lit_to_ranges[nlit][i];
 308       Trace("bound-int-assert") << "  ...this is a bounding literal for " << r << std::endl;
 309       d_rms[r]->assertNode( n );
 310     }
 311   }
 312   d_assertions[nlit] = n.getKind()!=NOT;
 313 }
 314
 315 Node BoundedIntegers::getNextDecisionRequest() {
 316   Trace("bound-int-dec-debug") << "bi: Get next decision request?" << std::endl;
 317   for( unsigned i=0; i<d_ranges.size(); i++) {
 318     Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();
 319     if (!d.isNull()) {
 320       bool polLit = d.getKind()!=NOT;
 321       Node lit = d.getKind()==NOT ? d[0] : d;
 322       bool value;
 323       if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
 324         if( value==polLit ){
 325           Trace("bound-int-dec-debug") << "...already asserted properly." << std::endl;
 326           //already true, we're already fine
 327         }else{
 328           Trace("bound-int-dec-debug") << "...already asserted with wrong polarity, re-assert." << std::endl;
 329           assertNode( d.negate() );
 330           i--;
 331         }
 332       }else{
 333         Trace("bound-int-dec") << "Bounded Integers : Decide " << d << std::endl;
 334         return d;
 335       }
 336     }
 337   }
 338   return Node::null();
 339 }
 340
 341 void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
 342   l = d_bounds[0][f][v];
 343   u = d_bounds[1][f][v];
 344   if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){
 345     //must create substitution
 346     std::vector< Node > vars;
 347     std::vector< Node > subs;
 348     Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
 349     for( unsigned i=0; i<d_set[f].size(); i++) {
 350       if( d_set[f][i]!=v ){
 351         Trace("bound-int-rsi") << "Look up the value for " << d_set[f][i] << " " << rsi->d_var_order[d_set_nums[f][i]] << std::endl;
 352         Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl;
 353         vars.push_back(d_set[f][i]);
 354         subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]));
 355       }else{
 356         break;
 357       }
 358     }
 359     Trace("bound-int-rsi") << "Do substitution..." << std::endl;
 360     //check if it has been instantiated
 361     if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){
 362       //must add the lemma
 363       Node nn = d_nground_range[f][v];
 364       nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
 365       Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] );
 366       Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
 367       d_quantEngine->getOutputChannel().lemma(lem, false, true);
 368       l = Node::null();
 369       u = Node::null();
 370       return;
 371     }else{
 372       u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
 373       l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
 374     }
 375   }
 376 }
 377
 378 void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
 379   getBounds( f, v, rsi, l, u );
 380   Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
 381   l = d_quantEngine->getModel()->getCurrentModelValue( l );
 382   u = d_quantEngine->getModel()->getCurrentModelValue( u );
 383   Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
 384   return;
 385 }
 386
 387 bool BoundedIntegers::isGroundRange(Node f, Node v) {
 388   return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
 389 }