src/theory/quantifiers/inst_strategy_cbqi.cpp

   1 /*********************                                                        */
   2 /*! \file inst_strategy_cbqi.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   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 counterexample-guided quantifier instantiation strategies
  13  **/
  14 #include "theory/quantifiers/inst_strategy_cbqi.h"
  15
  16 #include "options/quantifiers_options.h"
  17 #include "smt/ite_removal.h"
  18 #include "theory/arith/partial_model.h"
  19 #include "theory/arith/theory_arith.h"
  20 #include "theory/arith/theory_arith_private.h"
  21 #include "theory/quantifiers/first_order_model.h"
  22 #include "theory/quantifiers/term_database.h"
  23 #include "theory/quantifiers/trigger.h"
  24 #include "theory/theory_engine.h"
  25
  26 using namespace std;
  27 using namespace CVC4;
  28 using namespace CVC4::kind;
  29 using namespace CVC4::context;
  30 using namespace CVC4::theory;
  31 using namespace CVC4::theory::quantifiers;
  32 using namespace CVC4::theory::arith;
  33
  34 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
  35
  36 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
  37   : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() )
  38 //, d_added_inst( qe->getUserContext() )
  39 {
  40 }
  41
  42 InstStrategyCbqi::~InstStrategyCbqi() throw(){}
  43
  44 bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
  45   return e>=Theory::EFFORT_LAST_CALL;
  46 }
  47
  48 unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
  49   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
  50     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
  51     if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
  52       return QuantifiersEngine::QEFFORT_STANDARD;
  53     }
  54   }
  55   return QuantifiersEngine::QEFFORT_NONE;
  56 }
  57
  58 void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
  59   d_cbqi_set_quant_inactive = false;
  60   d_incomplete_check = false;
  61   //check if any cbqi lemma has not been added yet
  62   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
  63     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
  64     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
  65     if( doCbqi( q ) ){
  66       if( !hasAddedCbqiLemma( q ) ){
  67         d_added_cbqi_lemma.insert( q );
  68         Trace("cbqi") << "Do cbqi for " << q << std::endl;
  69         //add cbqi lemma
  70         //get the counterexample literal
  71         Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
  72         Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
  73         if( !ceBody.isNull() ){
  74           //add counterexample lemma
  75           Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
  76           //require any decision on cel to be phase=true
  77           d_quantEngine->addRequirePhase( ceLit, true );
  78           Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
  79           //add counterexample lemma
  80           lem = Rewriter::rewrite( lem );
  81           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
  82           registerCounterexampleLemma( q, lem );
  83         }
  84       //set inactive the quantified formulas whose CE literals are asserted false
  85       }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
  86         Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
  87         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
  88         bool value;
  89         if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
  90           Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
  91           if( !value ){
  92             if( d_quantEngine->getValuation().isDecision( cel ) ){
  93               Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
  94             }else{
  95               d_quantEngine->getModel()->setQuantifierActive( q, false );
  96               d_cbqi_set_quant_inactive = true;
  97             }
  98           }
  99         }else{
 100           Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
 101         }
 102       }
 103     }
 104   }
 105   processResetInstantiationRound( effort );
 106 }
 107
 108 void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
 109   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
 110     Assert( !d_quantEngine->inConflict() );
 111     double clSet = 0;
 112     if( Trace.isOn("cbqi-engine") ){
 113       clSet = double(clock())/double(CLOCKS_PER_SEC);
 114       Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
 115     }
 116     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
 117     for( int ee=0; ee<=1; ee++ ){
 118       for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 119         Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
 120         if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
 121           process( q, e, ee );
 122           if( d_quantEngine->inConflict() ){
 123             break;
 124           }
 125         }
 126       }
 127       if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
 128         break;
 129       }
 130     }
 131     if( Trace.isOn("cbqi-engine") ){
 132       if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
 133         Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
 134       }
 135       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 136       Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
 137     }
 138   }
 139 }
 140
 141 bool InstStrategyCbqi::checkComplete() {
 142   if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
 143     return false;
 144   }else{
 145     return true;
 146   }
 147 }
 148
 149 void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
 150   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
 151     if( !options::cbqiAll() && !options::cbqiSplx() ){
 152       //take full ownership of the quantified formula
 153       d_quantEngine->setOwner( q, this );
 154     }
 155   }
 156 }
 157
 158 void InstStrategyCbqi::registerQuantifier( Node q ) {
 159
 160 }
 161
 162 void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
 163   Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
 164   d_quantEngine->addLemma( lem, false );
 165 }
 166
 167 bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
 168   if( visited.find( n )==visited.end() ){
 169     visited[n] = true;
 170     if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){
 171       if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
 172         Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
 173         return true;
 174       }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
 175         Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
 176         return true;
 177       }else if( n.getKind()==FORALL ){
 178         return hasNonCbqiOperator( n[1], visited );
 179       }else{
 180         for( unsigned i=0; i<n.getNumChildren(); i++ ){
 181           if( hasNonCbqiOperator( n[i], visited ) ){
 182             return true;
 183           }
 184         }
 185       }
 186     }
 187   }
 188   return false;
 189 }
 190 bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){
 191   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
 192     TypeNode tn = q[0][i].getType();
 193     if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
 194       if( options::cbqiSplx() ){
 195         return true;
 196       }else{
 197         //datatypes supported in new implementation
 198         if( !tn.isDatatype() ){
 199           return true;
 200         }
 201       }
 202     }
 203   }
 204   return false;
 205 }
 206
 207 bool InstStrategyCbqi::doCbqi( Node q ){
 208   std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
 209   if( it==d_do_cbqi.end() ){
 210     bool ret = false;
 211     if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
 212       ret = true;
 213     }else{
 214       //if has an instantiation pattern, don't do it
 215       if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
 216         ret = false;
 217       }else{
 218         if( options::cbqiAll() ){
 219           ret = true;
 220         }else{
 221           //if quantifier has a non-arithmetic variable, then do not use cbqi
 222           //if quantifier has an APPLY_UF term, then do not use cbqi
 223           //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
 224           std::map< Node, bool > visited;
 225           ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited );
 226         }
 227       }
 228     }
 229     Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl;
 230     d_do_cbqi[q] = ret;
 231     return ret;
 232   }else{
 233     return it->second;
 234   }
 235 }
 236
 237 Node InstStrategyCbqi::getNextDecisionRequest(){
 238   // all counterexample literals that are not asserted
 239   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 240     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
 241     if( hasAddedCbqiLemma( q ) ){
 242       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
 243       bool value;
 244       if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
 245         Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl;
 246         return cel;
 247       }
 248     }
 249   }
 250   return Node::null();
 251 }
 252
 253
 254
 255
 256 //old implementation
 257
 258 InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategyCbqi( ie ), d_th( th ), d_counter( 0 ){
 259   d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
 260   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
 261 }
 262
 263 void getInstantiationConstants( Node n, std::vector< Node >& ics ){
 264   if( n.getKind()==INST_CONSTANT ){
 265     if( std::find( ics.begin(), ics.end(), n )==ics.end() ){
 266       ics.push_back( n );
 267     }
 268   }else{
 269     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 270       getInstantiationConstants( n[i], ics );
 271     }
 272   }
 273 }
 274
 275
 276 void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
 277   Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
 278   d_quantActive.clear();
 279   d_instRows.clear();
 280   d_tableaux_term.clear();
 281   d_tableaux.clear();
 282   d_ceTableaux.clear();
 283   //search for instantiation rows in simplex tableaux
 284   ArithVariables& avnm = d_th->d_internal->d_partialModel;
 285   ArithVariables::var_iterator vi, vend;
 286   for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
 287     ArithVar x = *vi;
 288     Node n = avnm.asNode(x);
 289
 290     //collect instantiation constants
 291     std::vector< Node > ics;
 292     getInstantiationConstants( n, ics );
 293     for( unsigned i=0; i<ics.size(); i++ ){
 294       NodeBuilder<> t(kind::PLUS);
 295       if( n.getKind()==PLUS ){
 296         for( int j=0; j<(int)n.getNumChildren(); j++ ){
 297           addTermToRow( ics[i], x, n[j], t );
 298         }
 299       }else{
 300         addTermToRow( ics[i], x, n, t );
 301       }
 302       d_instRows[ics[i]].push_back( x );
 303       //this theory has constraints from f
 304       Node f = TermDb::getInstConstAttr(ics[i]);
 305       Debug("quant-arith") << "Has constraints from " << f << std::endl;
 306       //set that we should process it
 307       d_quantActive[ f ] = true;
 308       //set tableaux term
 309       if( t.getNumChildren()==0 ){
 310         d_tableaux_term[ics[i]][x] = d_zero;
 311       }else if( t.getNumChildren()==1 ){
 312         d_tableaux_term[ics[i]][x] = t.getChild( 0 );
 313       }else{
 314         d_tableaux_term[ics[i]][x] = t;
 315       }
 316     }
 317   }
 318   //print debug
 319   if( Debug.isOn("quant-arith-debug") ){
 320     Debug("quant-arith-debug") << std::endl;
 321     debugPrint( "quant-arith-debug" );
 322   }
 323   d_counter++;
 324 }
 325
 326 void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){
 327   if( n.getKind()==MULT ){
 328     if( TermDb::hasInstConstAttr(n[1]) && n[0].getKind()==CONST_RATIONAL ){
 329       if( n[1]==i ){
 330         d_ceTableaux[i][x][ n[1] ] = n[0];
 331       }else{
 332         d_tableaux_ce_term[i][x][ n[1] ] = n[0];
 333       }
 334     }else{
 335       d_tableaux[i][x][ n[1] ] = n[0];
 336       t << n;
 337     }
 338   }else{
 339     if( TermDb::hasInstConstAttr(n) ){
 340       if( n==i ){
 341         d_ceTableaux[i][x][ n ] = Node::null();
 342       }else{
 343         d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
 344       }
 345     }else{
 346       d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
 347       t << n;
 348     }
 349   }
 350 }
 351
 352 void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
 353   if( e==0 ){
 354     if( d_quantActive.find( f )!=d_quantActive.end() ){
 355       //the point instantiation
 356       InstMatch m_point( f );
 357       bool m_point_valid = true;
 358       int lem = 0;
 359       //scan over all instantiation rows
 360       for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
 361         Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
 362         Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
 363         for( unsigned j=0; j<d_instRows[ic].size(); j++ ){
 364           ArithVar x = d_instRows[ic][j];
 365           if( !d_ceTableaux[ic][x].empty() ){
 366             if( Debug.isOn("quant-arith-simplex") ){
 367               Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
 368               Debug("quant-arith-simplex") << "  ";
 369               for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
 370                 if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
 371                 Debug("quant-arith-simplex") << it->first << " * " << it->second;
 372               }
 373               Debug("quant-arith-simplex") << " = ";
 374               Node v = getTableauxValue( x, false );
 375               Debug("quant-arith-simplex") << v << std::endl;
 376               Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
 377               Debug("quant-arith-simplex") << "  ce-term : ";
 378               for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
 379                 if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
 380                 Debug("quant-arith-simplex") << it->first << " * " << it->second;
 381               }
 382               Debug("quant-arith-simplex") << std::endl;
 383             }
 384             //instantiation row will be A*e + B*t = beta,
 385             // where e is a vector of terms , and t is vector of ground terms.
 386             // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
 387             // We will construct the term ( beta - B*t)/coeff to use for e_i.
 388             InstMatch m( f );
 389             for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
 390               if( f[0][k].getType().isInteger() ){
 391                 m.setValue( k, d_zero );
 392               }
 393             }
 394             //By default, choose the first instantiation constant to be e_i.
 395             Node var = d_ceTableaux[ic][x].begin()->first;
 396             //if it is integer, we need to find variable with coefficent +/- 1
 397             if( var.getType().isInteger() ){
 398               std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
 399               while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
 400                 ++it;
 401                 if( it==d_ceTableaux[ic][x].end() ){
 402                   var = Node::null();
 403                 }else{
 404                   var = it->first;
 405                 }
 406               }
 407               //Otherwise, try one that divides all ground term coefficients?
 408               //  Might be futile, if rewrite ensures gcd of coeffs is 1.
 409             }
 410             if( !var.isNull() ){
 411               //add to point instantiation if applicable
 412               if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
 413                 Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
 414                 Node v = getTableauxValue( x, false );
 415                 if( !var.getType().isInteger() || v.getType().isInteger() ){
 416                   m_point.setValue( i, v );
 417                 }else{
 418                   m_point_valid = false;
 419                 }
 420               }
 421               Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
 422               if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
 423                 lem++;
 424               }
 425             }else{
 426               Debug("quant-arith-simplex") << "Could not find var." << std::endl;
 427             }
 428           }
 429         }
 430       }
 431       if( lem==0 && m_point_valid ){
 432         if( d_quantEngine->addInstantiation( f, m_point ) ){
 433           Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
 434         }
 435       }
 436     }
 437   }
 438 }
 439
 440
 441 void InstStrategySimplex::debugPrint( const char* c ){
 442   ArithVariables& avnm = d_th->d_internal->d_partialModel;
 443   ArithVariables::var_iterator vi, vend;
 444   for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
 445     ArithVar x = *vi;
 446     Node n = avnm.asNode(x);
 447     //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
 448       Debug(c) << x << " : " << n << ", bounds = ";
 449       if( d_th->d_internal->d_partialModel.hasLowerBound( x ) ){
 450         Debug(c) << d_th->d_internal->d_partialModel.getLowerBound( x );
 451       }else{
 452         Debug(c) << "-infty";
 453       }
 454       Debug(c) << " <= ";
 455       Debug(c) << d_th->d_internal->d_partialModel.getAssignment( x );
 456       Debug(c) << " <= ";
 457       if( d_th->d_internal->d_partialModel.hasUpperBound( x ) ){
 458         Debug(c) << d_th->d_internal->d_partialModel.getUpperBound( x );
 459       }else{
 460         Debug(c) << "+infty";
 461       }
 462       Debug(c) << std::endl;
 463       //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;
 464       //Debug(c) << "   ";
 465       //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
 466       //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
 467       //}
 468       //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
 469       //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
 470       //}
 471       //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
 472       //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
 473       //}
 474       //Debug(c) << std::endl;
 475     //}
 476   }
 477   Debug(c) << std::endl;
 478
 479   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 480     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
 481     Debug(c) << f << std::endl;
 482     Debug(c) << "   Inst constants: ";
 483     for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
 484       if( j>0 ){
 485         Debug( c ) << ", ";
 486       }
 487       Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
 488     }
 489     Debug(c) << std::endl;
 490     for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
 491       Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
 492       Debug(c) << "   Instantiation rows for " << ic << " : ";
 493       for( unsigned k=0; k<d_instRows[ic].size(); k++ ){
 494         if( k>0 ){
 495           Debug(c) << ", ";
 496         }
 497         Debug(c) << d_instRows[ic][k];
 498       }
 499       Debug(c) << std::endl;
 500     }
 501   }
 502 }
 503
 504 //say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
 505 // where var is an instantiation constant from f,
 506 // t[e] is a vector of terms containing instantiation constants from f,
 507 // and term is a ground term (c1*t1 + ... + cn*tn).
 508 // We construct the term ( beta - term )/coeff to use as an instantiation for var.
 509 bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){
 510   //first try +delta
 511   if( doInstantiation2( f, ic, term, x, m, var ) ){
 512     ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
 513     return true;
 514   }else{
 515 #ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
 516     //otherwise try -delta
 517     if( doInstantiation2( f, ic, term, x, m, var, true ) ){
 518       ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
 519       return true;
 520     }else{
 521       return false;
 522     }
 523 #else
 524     return false;
 525 #endif
 526   }
 527 }
 528
 529 bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
 530   // make term ( beta - term )/coeff
 531   bool vIsInteger = var.getType().isInteger();
 532   Node beta = getTableauxValue( x, minus_delta );
 533   if( !vIsInteger || beta.getType().isInteger() ){
 534     Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
 535     if( !d_ceTableaux[ic][x][var].isNull() ){
 536       if( vIsInteger ){
 537         Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
 538         instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal );
 539       }else{
 540         Assert( d_ceTableaux[ic][x][var].getKind()==CONST_RATIONAL );
 541         Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() );
 542         instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
 543       }
 544     }
 545     instVal = Rewriter::rewrite( instVal );
 546     //use as instantiation value for var
 547     int vn = var.getAttribute(InstVarNumAttribute());
 548     m.setValue( vn, instVal );
 549     Debug("quant-arith") << "Add instantiation " << m << std::endl;
 550     return d_quantEngine->addInstantiation( f, m );
 551   }else{
 552     return false;
 553   }
 554 }
 555 /*
 556 Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
 557   if( d_th->d_internal->d_partialModel.hasArithVar(n) ){
 558     ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n );
 559     return getTableauxValue( v, minus_delta );
 560   }else{
 561     return NodeManager::currentNM()->mkConst( Rational(0) );
 562   }
 563 }
 564 */
 565 Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
 566   const Rational& delta = d_th->d_internal->d_partialModel.getDelta();
 567   DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v );
 568   Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
 569   return mkRationalNode(qmodel);
 570 }
 571
 572
 573
 574 //new implementation
 575
 576 bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) {
 577   return d_out->doAddInstantiation( subs );
 578 }
 579
 580 bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
 581   return d_out->isEligibleForInstantiation( n );
 582 }
 583
 584 bool CegqiOutputInstStrategy::addLemma( Node lem ) {
 585   return d_out->addLemma( lem );
 586 }
 587
 588
 589 InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
 590   : InstStrategyCbqi( qe ) {
 591   d_out = new CegqiOutputInstStrategy( this );
 592   d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
 593 }
 594
 595 InstStrategyCegqi::~InstStrategyCegqi() throw () {
 596   delete d_out;
 597
 598   for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(),
 599           iend = d_cinst.end(); i != iend; ++i) {
 600     CegInstantiator * instantiator = (*i).second;
 601     delete instantiator;
 602   }
 603   d_cinst.clear();
 604 }
 605
 606 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
 607   d_check_vts_lemma_lc = false;
 608 }
 609
 610 void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
 611   if( e==0 ){
 612     CegInstantiator * cinst = getInstantiator( q );
 613     Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
 614     d_curr_quant = q;
 615     if( !cinst->check() ){
 616       d_incomplete_check = true;
 617       d_check_vts_lemma_lc = true;
 618     }
 619     d_curr_quant = Node::null();
 620   }else if( e==1 ){
 621     //minimize the free delta heuristically on demand
 622     if( d_check_vts_lemma_lc ){
 623       Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
 624       d_check_vts_lemma_lc = false;
 625       d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
 626       d_small_const = Rewriter::rewrite( d_small_const );
 627       //heuristic for now, until we know how to do nested quantification
 628       Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
 629       if( !delta.isNull() ){
 630         Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
 631         Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
 632         d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
 633       }
 634       std::vector< Node > inf;
 635       d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false );
 636       for( unsigned i=0; i<inf.size(); i++ ){
 637         Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
 638         Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
 639         d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
 640       }
 641     }
 642   }
 643 }
 644
 645 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
 646   Assert( !d_curr_quant.isNull() );
 647   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
 648   if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
 649     d_cbqi_set_quant_inactive = true;
 650     d_incomplete_check = true;
 651     d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
 652     return true;
 653   }else{
 654     //check if we need virtual term substitution (if used delta or infinity)
 655     bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
 656     if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
 657       //d_added_inst.insert( d_curr_quant );
 658       return true;
 659     }else{
 660       return false;
 661     }
 662   }
 663 }
 664
 665 bool InstStrategyCegqi::addLemma( Node lem ) {
 666   return d_quantEngine->addLemma( lem );
 667 }
 668
 669 bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
 670   if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
 671     if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){
 672       return true;
 673     }else{
 674       //only legal if current quantified formula contains n
 675       return TermDb::containsTerm( d_curr_quant, n );
 676     }
 677   }else{
 678     return true;
 679   }
 680 }
 681
 682 CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
 683   std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
 684   if( it==d_cinst.end() ){
 685     CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
 686     d_cinst[q] = cinst;
 687     return cinst;
 688   }else{
 689    return it->second;
 690   }
 691 }
 692
 693 void InstStrategyCegqi::registerQuantifier( Node q ) {
 694   if( options::cbqiPreRegInst() ){
 695     //just get the instantiator
 696     getInstantiator( q );
 697   }
 698 }
 699
 700 void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
 701   //must register with the instantiator
 702   //must explicitly remove ITEs so that we record dependencies
 703   std::vector< Node > ce_vars;
 704   for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
 705     ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
 706   }
 707   std::vector< Node > lems;
 708   lems.push_back( lem );
 709   CegInstantiator * cinst = getInstantiator( q );
 710   cinst->registerCounterexampleLemma( lems, ce_vars );
 711   for( unsigned i=0; i<lems.size(); i++ ){
 712     Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl;
 713     d_quantEngine->addLemma( lems[i], false );
 714   }
 715 }
 716
 717 void InstStrategyCegqi::presolve() {
 718   if( options::cbqiPreRegInst() ){
 719     for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
 720       it->second->presolve( it->first );
 721     }
 722   }
 723 }