src/theory/quantifiers/ambqi_builder.cpp

   1 /*********************                                                        */
   2 /*! \file ambqi_builder.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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 Implementation of abstract MBQI builder
  13  **/
  14
  15
  16 #include "options/quantifiers_options.h"
  17 #include "theory/quantifiers/ambqi_builder.h"
  18 #include "theory/quantifiers/term_database.h"
  19
  20 using namespace std;
  21 using namespace CVC4;
  22 using namespace CVC4::kind;
  23 using namespace CVC4::context;
  24 using namespace CVC4::theory;
  25 using namespace CVC4::theory::quantifiers;
  26
  27 void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) {
  28   d_def.clear();
  29   Assert( !fapps.empty() );
  30   if( depth==fapps[0].getNumChildren() ){
  31     //if( fapps.size()>1 ){
  32     //  for( unsigned i=0; i<fapps.size(); i++ ){
  33     //    std::cout << "...." << fapps[i] << " -> " << m->getRepresentativeId( fapps[i] ) << std::endl;
  34     //  }
  35     //}
  36     //get representative in model for this term
  37     d_value = m->getRepresentativeId( fapps[0] );
  38     Assert( d_value!=val_none );
  39   }else{
  40     TypeNode tn = fapps[0][depth].getType();
  41     std::map< unsigned, std::vector< TNode > > fapp_child;
  42
  43     //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
  44     for( unsigned i=0; i<fapps.size(); i++ ){
  45       unsigned r = m->getRepresentativeId( fapps[i][depth] );
  46       Assert( r < 32 );
  47       fapp_child[r].push_back( fapps[i] );
  48     }
  49
  50     //do completion
  51     std::map< unsigned, unsigned > fapp_child_index;
  52     unsigned def = m->d_domain[ tn ];
  53     unsigned minSize = fapp_child.begin()->second.size();
  54     unsigned minSizeIndex = fapp_child.begin()->first;
  55     for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
  56       fapp_child_index[it->first] = ( 1 << it->first );
  57       def = def & ~( 1 << it->first );
  58       if( it->second.size()<minSize ){
  59         minSize = it->second.size();
  60         minSizeIndex = it->first;
  61       }
  62     }
  63     fapp_child_index[minSizeIndex] |= def;
  64     d_default = fapp_child_index[minSizeIndex];
  65
  66     //construct children
  67     for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
  68       Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : ";
  69       debugPrintUInt( "abs-model-debug", m->d_rep_set.d_type_reps[tn].size(), fapp_child_index[it->first] );
  70       Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl;
  71       d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 );
  72     }
  73   }
  74 }
  75
  76 void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) {
  77   if( d_value==val_none && !d_def.empty() ){
  78     //process the default
  79     std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );
  80     Assert( defd!=d_def.end() );
  81     unsigned newDef = d_default;
  82     std::vector< unsigned > to_erase;
  83     defd->second.simplify( m, q, n, depth+1 );
  84     int defVal = defd->second.d_value;
  85     bool isConstant = ( defVal!=val_none );
  86     //process each child
  87     for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
  88       if( it->first!=d_default ){
  89         it->second.simplify( m, q, n, depth+1 );
  90         if( it->second.d_value==defVal && it->second.d_value!=val_none ){
  91           newDef = newDef | it->first;
  92           to_erase.push_back( it->first );
  93         }else{
  94           isConstant = false;
  95         }
  96       }
  97     }
  98     if( !to_erase.empty() ){
  99       //erase old default
 100       int defVal = defd->second.d_value;
 101       d_def.erase( d_default );
 102       //set new default
 103       d_default = newDef;
 104       d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 );
 105       //erase redundant entries
 106       for( unsigned i=0; i<to_erase.size(); i++ ){
 107         d_def.erase( to_erase[i] );
 108       }
 109     }
 110     //if constant, propagate the value upwards
 111     if( isConstant ){
 112       d_value = defVal;
 113     }else{
 114       d_value = val_none;
 115     }
 116   }
 117 }
 118
 119 void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{
 120   for( unsigned i=0; i<dSize; i++ ){
 121     Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
 122   }
 123   //Trace(c) << "(";
 124   //for( unsigned i=0; i<32; i++ ){
 125   //  Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
 126   //}
 127   //Trace(c) << ")";
 128 }
 129
 130 void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{
 131   if( Trace.isOn(c) ){
 132     if( depth==f.getNumChildren() ){
 133       for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  ";}
 134       Trace(c) << "V[" << d_value << "]" << std::endl;
 135     }else{
 136       TypeNode tn = f[depth].getType();
 137       unsigned dSize = m->d_rep_set.getNumRepresentatives( tn );
 138       Assert( dSize<32 );
 139       for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){
 140         for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  ";}
 141         debugPrintUInt( c, dSize, it->first );
 142         if( it->first==d_default ){
 143           Trace(c) << "*";
 144         }
 145         if( it->second.d_value!=val_none ){
 146           Trace(c) << " -> V[" << it->second.d_value << "]";
 147         }
 148         Trace(c) << std::endl;
 149         it->second.debugPrint( c, m, f, depth+1 );
 150       }
 151     }
 152   }
 153 }
 154
 155 bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) {
 156   if( inst==0 || !options::fmfOneInstPerRound() ){
 157     if( d_value==1 ){
 158       //instantiations are all true : ignore this
 159       return true;
 160     }else{
 161       if( depth==q[0].getNumChildren() ){
 162         if( qe->addInstantiation( q, terms ) ){
 163           Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
 164           inst++;
 165           return true;
 166         }else{
 167           Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;
 168           //we are incomplete
 169           return false;
 170         }
 171       }else{
 172         bool osuccess = true;
 173         TypeNode tn = m->getVariable( q, depth ).getType();
 174         for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
 175           //get witness term
 176           unsigned index = 0;
 177           bool success;
 178           do {
 179             success = false;
 180             index = getId( it->first, index );
 181             if( index<32 ){
 182               Assert( index<m->d_rep_set.d_type_reps[tn].size() );
 183               terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];
 184               //terms[depth] = m->d_rep_set.d_type_reps[tn][index];
 185               if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){
 186                 //if we are incomplete, and have not yet added an instantiation, keep trying
 187                 index++;
 188                 Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;
 189               }else{
 190                 success = true;
 191               }
 192             }
 193           }while( !qe->inConflict() && !success && index<32 );
 194           //mark if we are incomplete
 195           osuccess = osuccess && success;
 196         }
 197         return osuccess;
 198       }
 199     }
 200   }else{
 201     return true;
 202   }
 203 }
 204
 205 void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth ) {
 206   if( depth==entry.size() ){
 207     d_value = v;
 208   }else{
 209     d_def[entry[depth]].construct_entry( entry, entry_def, v, depth+1 );
 210     if( entry_def[depth] ){
 211       d_default = entry[depth];
 212     }
 213   }
 214 }
 215
 216 void AbsDef::get_defs( unsigned u, std::vector< AbsDef * >& defs ) {
 217   for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
 218     if( ( u & it->first )!=0 ){
 219       Assert( (u & it->first)==u );
 220       defs.push_back( &it->second );
 221     }
 222   }
 223 }
 224
 225 void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth ) {
 226   if( depth==q[0].getNumChildren() ){
 227     Assert( defs.size()==1 );
 228     d_value = defs[0]->d_value;
 229   }else{
 230     TypeNode tn = m->getVariable( q, depth ).getType();
 231     unsigned def = m->d_domain[tn];
 232     for( unsigned i=0; i<defs.size(); i++ ){
 233       //process each simple child
 234       for( std::map< unsigned, AbsDef >::iterator itd = defs[i]->d_def.begin(); itd != defs[i]->d_def.end(); ++itd ){
 235         if( isSimple( itd->first ) && ( def & itd->first )!=0 ){
 236           def &= ~( itd->first );
 237           //process this value
 238           std::vector< AbsDef * > cdefs;
 239           for( unsigned j=0; j<defs.size(); j++ ){
 240             defs[j]->get_defs( itd->first, cdefs );
 241           }
 242           d_def[itd->first].construct_normalize( m, q, cdefs, depth+1 );
 243           if( def==0 ){
 244             d_default = itd->first;
 245             break;
 246           }
 247         }
 248       }
 249       if( def==0 ){
 250         break;
 251       }
 252     }
 253     if( def!=0 ){
 254       d_default = def;
 255       //process the default
 256       std::vector< AbsDef * > cdefs;
 257       for( unsigned j=0; j<defs.size(); j++ ){
 258         defs[j]->get_defs( d_default, cdefs );
 259       }
 260       d_def[d_default].construct_normalize( m, q, cdefs, depth+1 );
 261     }
 262   }
 263 }
 264
 265 void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) {
 266   d_value = v;
 267   if( depth<n.getNumChildren() ){
 268     TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType();
 269     unsigned dom = m->d_domain[tn] ;
 270     d_def[dom].construct_def_entry( m, q, n, v, depth+1 );
 271     d_default = dom;
 272   }
 273 }
 274
 275 void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q,
 276                              std::vector< unsigned >& entry, std::vector< bool >& entry_def,
 277                              std::vector< int >& terms, std::map< unsigned, int >& vchildren,
 278                              AbsDef * a, unsigned depth ) {
 279   if( depth==terms.size() ){
 280     if( Trace.isOn("ambqi-check-debug2") ){
 281       Trace("ambqi-check-debug2") << "Add entry ( ";
 282       for( unsigned i=0; i<entry.size(); i++ ){
 283         unsigned dSize = m->d_rep_set.d_type_reps[m->getVariable( q, i ).getType()].size();
 284         debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] );
 285         Trace("ambqi-check-debug2") << " ";
 286       }
 287       Trace("ambqi-check-debug2") << ")" << std::endl;
 288     }
 289     a->construct_entry( entry, entry_def, d_value );
 290   }else{
 291     unsigned id;
 292     if( terms[depth]==val_none ){
 293       //a variable
 294       std::map< unsigned, int >::iterator itv = vchildren.find( depth );
 295       Assert( itv!=vchildren.end() );
 296       unsigned prev_v = entry[itv->second];
 297       bool prev_vd = entry_def[itv->second];
 298       for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
 299         entry[itv->second] = it->first & prev_v;
 300         entry_def[itv->second] = ( it->first==d_default ) && prev_vd;
 301         if( entry[itv->second]!=0 ){
 302           it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );
 303         }
 304       }
 305       entry[itv->second] = prev_v;
 306       entry_def[itv->second] = prev_vd;
 307     }else{
 308       id = (unsigned)terms[depth];
 309       Assert( id<32 );
 310       unsigned fid = 1 << id;
 311       std::map< unsigned, AbsDef >::iterator it = d_def.find( fid );
 312       if( it!=d_def.end() ){
 313         it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );
 314       }else{
 315         d_def[d_default].apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 );
 316       }
 317     }
 318   }
 319 }
 320
 321 void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) {
 322   if( depth==q[0].getNumChildren() ){
 323     Assert( currv!=val_none );
 324     d_value = currv;
 325   }else{
 326     TypeNode tn = m->getVariable( q, depth ).getType();
 327     unsigned dom = m->d_domain[tn];
 328     int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none );
 329     if( vindex==val_none ){
 330       d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );
 331       d_default = dom;
 332     }else{
 333       Assert( currv==val_none );
 334       if( curr==val_none ){
 335         unsigned numReps = m->d_rep_set.getNumRepresentatives( tn );
 336         Assert( numReps < 32 );
 337         for( unsigned i=0; i<numReps; i++ ){
 338           curr = 1 << i;
 339           d_def[curr].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );
 340         }
 341         d_default = curr;
 342       }else{
 343         d_def[curr].construct_var_eq( m, q, v1, v2, curr, 1, depth+1 );
 344         dom = dom & ~curr;
 345         d_def[dom].construct_var_eq( m, q, v1, v2, curr, 0, depth+1 );
 346         d_default = dom;
 347       }
 348     }
 349   }
 350 }
 351
 352 void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth ) {
 353   if( depth==q[0].getNumChildren() ){
 354     Assert( currv!=val_none );
 355     d_value = currv;
 356   }else{
 357     TypeNode tn = m->getVariable( q, depth ).getType();
 358     if( v==depth ){
 359       unsigned numReps = m->d_rep_set.d_type_reps[tn].size();
 360       Assert( numReps>0 && numReps < 32 );
 361       for( unsigned i=0; i<numReps; i++ ){
 362         d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
 363       }
 364       d_default = 1 << (numReps - 1);
 365     }else{
 366       unsigned dom = m->d_domain[tn];
 367       d_def[dom].construct_var( m, q, v, currv, depth+1 );
 368       d_default = dom;
 369     }
 370   }
 371 }
 372
 373 void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
 374                                 std::map< unsigned, AbsDef * >& children,
 375                                 std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
 376                                 std::vector< unsigned >& entry, std::vector< bool >& entry_def ) {
 377   if( n.getKind()==OR || n.getKind()==AND ){
 378     // short circuiting
 379     for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
 380       if( ( it->second->d_value==0 && n.getKind()==AND ) ||
 381           ( it->second->d_value==1 && n.getKind()==OR ) ){
 382         //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl;
 383         unsigned count = q[0].getNumChildren() - entry.size();
 384         for( unsigned i=0; i<count; i++ ){
 385           entry.push_back( m->d_domain[m->getVariable( q, entry.size() ).getType()] );
 386           entry_def.push_back( true );
 387         }
 388         construct_entry( entry, entry_def, it->second->d_value );
 389         for( unsigned i=0; i<count; i++ ){
 390           entry.pop_back();
 391           entry_def.pop_back();
 392         }
 393         return;
 394       }
 395     }
 396   }
 397   if( entry.size()==q[0].getNumChildren() ){
 398     if( f ){
 399       if( Trace.isOn("ambqi-check-debug2") ){
 400         for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
 401         Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl;
 402       }
 403       //we are composing with an uninterpreted function
 404       std::vector< int > values;
 405       values.resize( n.getNumChildren(), val_none );
 406       for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
 407         values[it->first] = it->second->d_value;
 408       }
 409       for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
 410         values[it->first] = it->second;
 411       }
 412       //look up value(s)
 413       f->apply_ucompose( m, q, entry, entry_def, values, vchildren, this );
 414     }else{
 415       bool incomplete = false;
 416       //we are composing with an interpreted function
 417       std::vector< TNode > values;
 418       values.resize( n.getNumChildren(), TNode::null() );
 419       for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
 420         Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value;
 421         if( it->second->d_value>=0 ){
 422           if( it->second->d_value>=(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ){
 423             std::cout << it->second->d_value << " " << n[it->first] << " " << n[it->first].getType() << " " << m->d_rep_set.d_type_reps[n[it->first].getType()].size() << std::endl;
 424           }
 425           Assert( it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
 426           values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second->d_value];
 427         }else{
 428           incomplete = true;
 429         }
 430         Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl;
 431       }
 432       for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
 433         Trace("ambqi-check-debug2") << "   basic :  " << it->first << " : " << it->second;
 434         if( it->second>=0 ){
 435           Assert( it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
 436           values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second];
 437         }else{
 438           incomplete = true;
 439         }
 440         Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl;
 441       }
 442       Assert( vchildren.empty() );
 443       if( incomplete ){
 444         Trace("ambqi-check-debug2") << "Construct incomplete entry." << std::endl;
 445
 446         //if a child is unknown, we must return unknown
 447         construct_entry( entry, entry_def, val_unk );
 448       }else{
 449         if( Trace.isOn("ambqi-check-debug2") ){
 450           for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
 451           Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( ";
 452           for( unsigned i=0; i<values.size(); i++ ){
 453             Assert( !values[i].isNull() );
 454             Trace("ambqi-check-debug2") << values[i] << " ";
 455           }
 456           Trace("ambqi-check-debug2") << ")..." << std::endl;
 457         }
 458         //evaluate
 459         Node vv = NodeManager::currentNM()->mkNode( n.getKind(), values );
 460         vv = Rewriter::rewrite( vv );
 461         int v = m->getRepresentativeId( vv );
 462         construct_entry( entry, entry_def, v );
 463       }
 464     }
 465   }else{
 466     //take product of arguments
 467     TypeNode tn = m->getVariable( q, entry.size() ).getType();
 468     Assert( m->isValidType( tn ) );
 469     unsigned def = m->d_domain[tn];
 470     if( Trace.isOn("ambqi-check-debug2") ){
 471       for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
 472       Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl;
 473     }
 474     for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
 475       Assert( it->second!=NULL );
 476       //process each child
 477       for( std::map< unsigned, AbsDef >::iterator itd = it->second->d_def.begin(); itd != it->second->d_def.end(); ++itd ){
 478         if( itd->first!=it->second->d_default && ( def & itd->first )!=0 ){
 479           def &= ~( itd->first );
 480           //process this value
 481           std::map< unsigned, AbsDef * > cchildren;
 482           for( std::map< unsigned, AbsDef * >::iterator it2 = children.begin(); it2 != children.end(); ++it2 ){
 483             Assert( it2->second!=NULL );
 484             std::map< unsigned, AbsDef >::iterator itdf = it2->second->d_def.find( itd->first );
 485             if( itdf!=it2->second->d_def.end() ){
 486               cchildren[it2->first] = &itdf->second;
 487             }else{
 488               Assert( it2->second->getDefault()!=NULL );
 489               cchildren[it2->first] = it2->second->getDefault();
 490             }
 491           }
 492           if( Trace.isOn("ambqi-check-debug2") ){
 493             for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
 494             Trace("ambqi-check-debug2") << "...process : ";
 495             debugPrintUInt("ambqi-check-debug2", m->d_rep_set.d_type_reps[tn].size(), itd->first );
 496             Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl;
 497           }
 498           entry.push_back( itd->first );
 499           entry_def.push_back( def==0 );
 500           construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def );
 501           entry_def.pop_back();
 502           entry.pop_back();
 503           if( def==0 ){
 504             break;
 505           }
 506         }
 507       }
 508       if( def==0 ){
 509         break;
 510       }
 511     }
 512     if( def!=0 ){
 513       if( Trace.isOn("ambqi-check-debug2") ){
 514         for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
 515         Trace("ambqi-check-debug2") << "Make default argument" << std::endl;
 516       }
 517       std::map< unsigned, AbsDef * > cdchildren;
 518       for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
 519         Assert( it->second->getDefault()!=NULL );
 520         cdchildren[it->first] = it->second->getDefault();
 521       }
 522       if( Trace.isOn("ambqi-check-debug2") ){
 523         for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
 524         Trace("ambqi-check-debug2") << "...process default : ";
 525         debugPrintUInt("ambqi-check-debug2", m->d_rep_set.getNumRepresentatives( tn ), def );
 526         Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl;
 527       }
 528       entry.push_back( def );
 529       entry_def.push_back( true );
 530       construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def );
 531       entry_def.pop_back();
 532       entry.pop_back();
 533     }
 534   }
 535 }
 536
 537 bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
 538                         std::map< unsigned, AbsDef * >& children,
 539                         std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
 540                         int varChCount ) {
 541   if( Trace.isOn("ambqi-check-debug3") ){
 542     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 543       Trace("ambqi-check-debug3") << i << " : ";
 544       Trace("ambqi-check-debug3") << ((children.find( i )!=children.end()) ? "X" : ".");
 545       if( bchildren.find( i )!=bchildren.end() ){
 546         Trace("ambqi-check-debug3") << bchildren[i];
 547       }else{
 548         Trace("ambqi-check-debug3") << ".";
 549       }
 550       if( vchildren.find( i )!=vchildren.end() ){
 551         Trace("ambqi-check-debug3") << vchildren[i];
 552       }else{
 553         Trace("ambqi-check-debug3") << ".";
 554       }
 555       Trace("ambqi-check-debug3") << std::endl;
 556     }
 557     Trace("ambqi-check-debug3") << "varChCount : " << varChCount << std::endl;
 558   }
 559   if( varChCount==0 || f ){
 560     //short-circuit
 561     if( n.getKind()==AND || n.getKind()==OR ){
 562       for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){
 563         if( ( it->second==0 && n.getKind()==AND ) ||
 564             ( it->second==1 && n.getKind()==OR ) ){
 565           construct_def_entry( m, q, q[0], it->second );
 566           return true;
 567         }
 568       }
 569     }
 570     Trace("ambqi-check-debug2") << "Construct compose..." << std::endl;
 571     std::vector< unsigned > entry;
 572     std::vector< bool > entry_def;
 573     if( f && varChCount>0 ){
 574       AbsDef unorm;
 575       unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
 576       //normalize
 577       std::vector< AbsDef* > defs;
 578       defs.push_back( &unorm );
 579       construct_normalize( m, q, defs );
 580     }else{
 581       construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
 582     }
 583     Assert( is_normalized() );
 584     //if( !is_normalized() ){
 585     //  std::cout << "NON NORMALIZED DEFINITION" << std::endl;
 586     //  exit( 10 );
 587     //}
 588     return true;
 589   }else if( varChCount==1 && n.getKind()==EQUAL ){
 590     Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;
 591     //expand the variable based on its finite domain
 592     AbsDef a;
 593     a.construct_var( m, q, vchildren.begin()->second, val_none );
 594     children[vchildren.begin()->first] = &a;
 595     vchildren.clear();
 596     std::vector< unsigned > entry;
 597     std::vector< bool > entry_def;
 598     Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl;
 599     construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
 600     return true;
 601   }else if( varChCount==2 && n.getKind()==EQUAL ){
 602     Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl;
 603     //efficient expansion of the equality
 604     construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none );
 605     return true;
 606   }else{
 607     return false;
 608   }
 609 }
 610
 611 void AbsDef::negate() {
 612   for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
 613     it->second.negate();
 614   }
 615   if( d_value==0 ){
 616     d_value = 1;
 617   }else if( d_value==1 ){
 618     d_value = 0;
 619   }
 620 }
 621
 622 Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) {
 623   if( depth==vars.size() ){
 624     TypeNode tn = op.getType();
 625     if( tn.getNumChildren()>0 ){
 626       tn = tn[tn.getNumChildren() - 1];
 627     }
 628     if( d_value>=0 ){
 629       Assert( d_value<(int)m->d_rep_set.d_type_reps[tn].size() );
 630       if( tn.isBoolean() ){
 631         return NodeManager::currentNM()->mkConst( d_value==1 );
 632       }else{
 633         return m->d_rep_set.d_type_reps[tn][d_value];
 634       }
 635     }else{
 636       return Node::null();
 637     }
 638   }else{
 639     TypeNode tn = vars[depth].getType();
 640     Node curr;
 641     curr = d_def[d_default].getFunctionValue( m, op, vars, depth+1 );
 642     for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
 643       if( it->first!=d_default ){
 644         unsigned id = getId( it->first );
 645         Assert( id<m->d_rep_set.d_type_reps[tn].size() );
 646         TNode n = m->d_rep_set.d_type_reps[tn][id];
 647         Node fv = it->second.getFunctionValue( m, op, vars, depth+1 );
 648         if( !curr.isNull() && !fv.isNull() ){
 649           curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr );
 650         }else{
 651           curr = Node::null();
 652         }
 653       }
 654     }
 655     return curr;
 656   }
 657 }
 658
 659 bool AbsDef::isSimple( unsigned n ) {
 660   return (n & (n - 1))==0;
 661 }
 662
 663 unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) {
 664   Assert( n!=0 );
 665   while( (n & ( 1 << start )) == 0 ){
 666     start++;
 667     if( start==end ){
 668       return start;
 669     }
 670   }
 671   return start;
 672 }
 673
 674 Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) {
 675   std::vector< unsigned > iargs;
 676   for( unsigned i=0; i<args.size(); i++ ){
 677     unsigned v = 1 << m->getRepresentativeId( args[i] );
 678     iargs.push_back( v );
 679   }
 680   return evaluate( m, retTyp, iargs, 0 );
 681 }
 682
 683 Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< unsigned >& iargs, unsigned depth ) {
 684   if( d_value!=val_none ){
 685     if( d_value==val_unk ){
 686       return Node::null();
 687     }else{
 688       Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() );
 689       return m->d_rep_set.d_type_reps[retTyp][d_value];
 690     }
 691   }else{
 692     std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] );
 693     if( it==d_def.end() ){
 694       return d_def[d_default].evaluate( m, retTyp, iargs, depth+1 );
 695     }else{
 696       return it->second.evaluate( m, retTyp, iargs, depth+1 );
 697     }
 698   }
 699 }
 700
 701 bool AbsDef::is_normalized() {
 702   for( std::map< unsigned, AbsDef >::iterator it1 = d_def.begin(); it1 != d_def.end(); ++it1 ){
 703     if( !it1->second.is_normalized() ){
 704       return false;
 705     }
 706     for( std::map< unsigned, AbsDef >::iterator it2 = d_def.begin(); it2 != d_def.end(); ++it2 ){
 707       if( it1->first!=it2->first && (( it1->first & it2->first )!=0) ){
 708         return false;
 709       }
 710     }
 711   }
 712   return true;
 713 }
 714
 715 AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) :
 716 QModelBuilder( c, qe ){
 717   d_true = NodeManager::currentNM()->mkConst( true );
 718   d_false = NodeManager::currentNM()->mkConst( false );
 719 }
 720
 721
 722 //------------------------model construction----------------------------
 723
 724 void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
 725   Trace("ambqi-debug") << "process build model " << fullModel << std::endl;
 726   FirstOrderModel* f = (FirstOrderModel*)m;
 727   FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
 728   if( fullModel ){
 729     Trace("ambqi-model") << "Construct model representation..." << std::endl;
 730     //make function values
 731     for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
 732       if( it->first.getType().getNumChildren()>1 ){
 733         Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;
 734         m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
 735       }
 736     }
 737     TheoryEngineModelBuilder::processBuildModel( m, fullModel );
 738     //mark that the model has been set
 739     fm->markModelSet();
 740     //debug the model
 741     debugModel( fm );
 742   }else{
 743     fm->initialize();
 744     //process representatives
 745     fm->d_rep_id.clear();
 746     fm->d_domain.clear();
 747
 748     //initialize boolean sort
 749     TypeNode b = d_true.getType();
 750     fm->d_rep_set.d_type_reps[b].clear();
 751     fm->d_rep_set.d_type_reps[b].push_back( d_false );
 752     fm->d_rep_set.d_type_reps[b].push_back( d_true );
 753     fm->d_rep_id[d_false] = 0;
 754     fm->d_rep_id[d_true] = 1;
 755
 756     //initialize unintpreted sorts
 757     Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
 758     for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
 759          it != fm->d_rep_set.d_type_reps.end(); ++it ){
 760       if( it->first.isSort() ){
 761         Assert( !it->second.empty() );
 762         //set the domain
 763         fm->d_domain[it->first] = 0;
 764         Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;
 765         for( unsigned i=0; i<it->second.size(); i++ ){
 766           if( i<32 ){
 767             fm->d_domain[it->first] |= ( 1 << i );
 768           }
 769           Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;
 770           fm->d_rep_id[it->second[i]] = i;
 771         }
 772         if( it->second.size()>=32 ){
 773           fm->d_domain.erase( it->first );
 774         }
 775       }
 776     }
 777
 778     Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;
 779     //construct the models for functions
 780     for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
 781       Node f = it->first;
 782       Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;
 783       //reset the model
 784       it->second->clear();
 785       //get all (non-redundant) f-applications
 786       std::vector< TNode > fapps;
 787       Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
 788       for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
 789         Node n = fm->d_uf_terms[f][i];
 790         if( !n.getAttribute(NoMatchAttribute()) ){
 791           Trace("ambqi-model-debug") << "  " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
 792           fapps.push_back( n );
 793         }
 794       }
 795       if( fapps.empty() ){
 796         //choose arbitrary value
 797         Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
 798         Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
 799         fapps.push_back( mbt );
 800       }
 801       bool fValid = true;
 802       for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){
 803         if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){
 804           Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";
 805           Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;
 806           fValid = false;
 807           break;
 808         }
 809       }
 810       fm->d_models_valid[f] = fValid;
 811       if( fValid ){
 812         //construct the ambqi model
 813         it->second->construct_func( fm, fapps );
 814         Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
 815         it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
 816         Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
 817         it->second->simplify( fm, TNode::null(), fapps[0] );
 818         Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
 819         it->second->debugPrint("ambqi-model", fm, fapps[0] );
 820
 821 /*
 822         if( Debug.isOn("ambqi-model-debug") ){
 823           for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
 824             Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
 825             Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
 826             Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
 827           }
 828         }
 829 */
 830       }
 831     }
 832   }
 833 }
 834
 835
 836 //--------------------model checking---------------------------------------
 837
 838 //do exhaustive instantiation
 839 bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
 840   Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
 841   if (effort==0) {
 842     FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
 843     bool quantValid = true;
 844     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
 845       if( !fma->isValidType( q[0][i].getType() ) ){
 846         quantValid = false;
 847         Trace("ambqi-inst") << "Interpretation of " << q << " is not valid because of type " << q[0][i].getType() << std::endl;
 848         break;
 849       }
 850     }
 851     if( quantValid ){
 852       Trace("ambqi-check") << "Compute interpretation..." << std::endl;
 853       AbsDef ad;
 854       doCheck( fma, q, ad, q[1] );
 855       //now process entries
 856       Trace("ambqi-inst-debug") << "...Current : " << d_addedLemmas << std::endl;
 857       Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;
 858       ad.debugPrint( "ambqi-inst", fma, q[0] );
 859       Trace("ambqi-inst") << std::endl;
 860       Trace("ambqi-check") << "Add instantiations..." << std::endl;
 861       int lem = 0;
 862       quantValid = ad.addInstantiations( fma, d_qe, q, lem );
 863       Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;
 864       if( lem>0 ){
 865         //if we were incomplete but added at least one lemma, we are ok
 866         quantValid = true;
 867       }
 868       d_addedLemmas += lem;
 869       Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl;
 870     }
 871     return quantValid;
 872   }
 873   return true;
 874 }
 875
 876 bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {
 877   Assert( n.getKind()!=FORALL );
 878   if( n.getKind()==NOT && n[0].getKind()!=FORALL ){
 879     doCheck( m, q, ad, n[0] );
 880     ad.negate();
 881     return true;
 882   }else{
 883     std::map< unsigned, AbsDef > children;
 884     std::map< unsigned, int > bchildren;
 885     std::map< unsigned, int > vchildren;
 886     int varChCount = 0;
 887     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 888       if( n[i].getKind()==FORALL ){
 889         bchildren[i] = AbsDef::val_unk;
 890       }else if( n[i].getKind() == BOUND_VARIABLE ){
 891         varChCount++;
 892         vchildren[i] = m->d_var_index[q][ m->getVariableId( q, n[i] ) ];
 893         //vchildren[i] = m->getVariableId( q, n[i] );
 894       }else if( m->hasTerm( n[i] ) ){
 895         bchildren[i] = m->getRepresentativeId( n[i] );
 896       }else{
 897         if( !doCheck( m, q, children[i], n[i] ) ){
 898           bchildren[i] = AbsDef::val_unk;
 899           children.erase( i );
 900         }
 901       }
 902     }
 903     //convert to pointers
 904     std::map< unsigned, AbsDef * > pchildren;
 905     for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){
 906       pchildren[it->first] = &it->second;
 907     }
 908     //construct the interpretation
 909     Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;
 910     if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){
 911       Node op;
 912       if( n.getKind() == APPLY_UF ){
 913         op = n.getOperator();
 914       }else{
 915         op = n;
 916       }
 917       //uninterpreted compose
 918       if( m->d_models_valid[op] ){
 919         ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount );
 920       }else{
 921         Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl;
 922         return false;
 923       }
 924     }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){
 925       Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl;
 926       return false;
 927     }
 928     Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;
 929     ad.debugPrint("ambqi-check-try", m, q[0] );
 930     ad.simplify( m, q, q[0] );
 931     Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;
 932     ad.debugPrint("ambqi-check-debug", m, q[0] );
 933     Trace("ambqi-check-debug") << std::endl;
 934     return true;
 935   }
 936 }