src/theory/quantifiers/trigger.cpp

   1 /*********************                                                        */
   2 /*! \file trigger.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-2017 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 trigger class
  13  **/
  14
  15 #include "theory/quantifiers/trigger.h"
  16 #include "theory/quantifiers/candidate_generator.h"
  17 #include "theory/quantifiers/ho_trigger.h"
  18 #include "theory/quantifiers/inst_match_generator.h"
  19 #include "theory/quantifiers/term_database.h"
  20 #include "theory/quantifiers/term_util.h"
  21 #include "theory/quantifiers_engine.h"
  22 #include "theory/theory_engine.h"
  23 #include "theory/uf/equality_engine.h"
  24 #include "util/hash.h"
  25
  26 using namespace std;
  27 using namespace CVC4::kind;
  28 using namespace CVC4::context;
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace inst {
  33
  34 void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
  35   if( d_fv.empty() ){
  36     quantifiers::TermUtil::getVarContainsNode( q, n, d_fv );
  37   }
  38   if( d_reqPol==0 ){
  39     d_reqPol = reqPol;
  40     d_reqPolEq = reqPolEq;
  41   }else{
  42     //determined a ground (dis)equality must hold or else q is a tautology?
  43   }
  44 }
  45
  46 /** trigger class constructor */
  47 Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
  48     : d_quantEngine( qe ), d_f( f ) {
  49   d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
  50   Trace("trigger") << "Trigger for " << f << ": " << std::endl;
  51   for( unsigned i=0; i<d_nodes.size(); i++ ){
  52     Trace("trigger") << "   " << d_nodes[i] << std::endl;
  53   }
  54   if( d_nodes.size()==1 ){
  55     if( isSimpleTrigger( d_nodes[0] ) ){
  56       d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe );
  57     }else{
  58       d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
  59     }
  60   }else{
  61     if( options::multiTriggerCache() ){
  62       d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
  63     }else{
  64       d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( f, d_nodes, qe );
  65     }
  66   }
  67   if( d_nodes.size()==1 ){
  68     if( isSimpleTrigger( d_nodes[0] ) ){
  69       ++(qe->d_statistics.d_triggers);
  70     }else{
  71       ++(qe->d_statistics.d_simple_triggers);
  72     }
  73   }else{
  74     Trace("multi-trigger") << "Trigger for " << f << ": " << std::endl;
  75     for( unsigned i=0; i<d_nodes.size(); i++ ){
  76       Trace("multi-trigger") << "   " << d_nodes[i] << std::endl;
  77     }
  78     ++(qe->d_statistics.d_multi_triggers);
  79   }
  80
  81   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
  82   Trace("trigger-debug") << "Finished making trigger." << std::endl;
  83 }
  84
  85 Trigger::~Trigger() {
  86   delete d_mg;
  87 }
  88
  89 void Trigger::resetInstantiationRound(){
  90   d_mg->resetInstantiationRound( d_quantEngine );
  91 }
  92
  93 void Trigger::reset( Node eqc ){
  94   d_mg->reset( eqc, d_quantEngine );
  95 }
  96
  97 Node Trigger::getInstPattern(){
  98   return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
  99 }
 100
 101 int Trigger::addInstantiations(InstMatch& baseMatch)
 102 {
 103   int addedLemmas =
 104       d_mg->addInstantiations(d_f, baseMatch, d_quantEngine, this);
 105   if( addedLemmas>0 ){
 106     if (Debug.isOn("inst-trigger"))
 107     {
 108       Debug("inst-trigger") << "Added " << addedLemmas
 109                             << " lemmas, trigger was ";
 110       for (unsigned i = 0; i < d_nodes.size(); i++)
 111       {
 112         Debug("inst-trigger") << d_nodes[i] << " ";
 113       }
 114       Debug("inst-trigger") << std::endl;
 115     }
 116   }
 117   return addedLemmas;
 118 }
 119
 120 bool Trigger::sendInstantiation(InstMatch& m)
 121 {
 122   return d_quantEngine->addInstantiation(d_f, m);
 123 }
 124
 125 bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
 126   //only take nodes that contribute variables to the trigger when added
 127   std::vector< Node > temp;
 128   temp.insert( temp.begin(), nodes.begin(), nodes.end() );
 129   std::map< Node, bool > vars;
 130   std::map< Node, std::vector< Node > > patterns;
 131   size_t varCount = 0;
 132   std::map< Node, std::vector< Node > > varContains;
 133   quantifiers::TermUtil::getVarContains( q, temp, varContains );
 134   for( unsigned i=0; i<temp.size(); i++ ){
 135     bool foundVar = false;
 136     for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
 137       Node v = varContains[ temp[i] ][j];
 138       Assert( quantifiers::TermUtil::getInstConstAttr(v)==q );
 139       if( vars.find( v )==vars.end() ){
 140         varCount++;
 141         vars[ v ] = true;
 142         foundVar = true;
 143       }
 144     }
 145     if( foundVar ){
 146       trNodes.push_back( temp[i] );
 147       for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
 148         Node v = varContains[ temp[i] ][j];
 149         patterns[ v ].push_back( temp[i] );
 150       }
 151     }
 152     if( varCount==n_vars ){
 153       break;
 154     }
 155   }
 156   if( varCount<n_vars ){
 157     Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
 158     for( unsigned i=0; i<nodes.size(); i++) {
 159       Trace("trigger-debug") << nodes[i] << " ";
 160     }
 161     Trace("trigger-debug") << std::endl;
 162
 163     //do not generate multi-trigger if it does not contain all variables
 164     return false;
 165   }else{
 166     //now, minimize the trigger
 167     for( unsigned i=0; i<trNodes.size(); i++ ){
 168       bool keepPattern = false;
 169       Node n = trNodes[i];
 170       for( unsigned j=0; j<varContains[ n ].size(); j++ ){
 171         Node v = varContains[ n ][j];
 172         if( patterns[v].size()==1 ){
 173           keepPattern = true;
 174           break;
 175         }
 176       }
 177       if( !keepPattern ){
 178         //remove from pattern vector
 179         for( unsigned j=0; j<varContains[ n ].size(); j++ ){
 180           Node v = varContains[ n ][j];
 181           for( unsigned k=0; k<patterns[v].size(); k++ ){
 182             if( patterns[v][k]==n ){
 183               patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
 184               break;
 185             }
 186           }
 187         }
 188         //remove from trigger nodes
 189         trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
 190         i--;
 191       }
 192     }
 193   }
 194   return true;
 195 }
 196
 197 Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){
 198   std::vector< Node > trNodes;
 199   if( !keepAll ){
 200     unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars;
 201     if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){
 202       return NULL;
 203     }
 204   }else{
 205     trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
 206   }
 207
 208   //check for duplicate?
 209   if( trOption!=TR_MAKE_NEW ){
 210     Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
 211     if( t ){
 212       if( trOption==TR_GET_OLD ){
 213         //just return old trigger
 214         return t;
 215       }else{
 216         return NULL;
 217       }
 218     }
 219   }
 220
 221   // check if higher-order
 222   Trace("trigger") << "Collect higher-order variable triggers..." << std::endl;
 223   std::map<Node, std::vector<Node> > ho_apps;
 224   HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
 225   Trigger* t;
 226   if (!ho_apps.empty())
 227   {
 228     t = new HigherOrderTrigger(qe, f, trNodes, ho_apps);
 229   }
 230   else
 231   {
 232     t = new Trigger(qe, f, trNodes);
 233   }
 234
 235   qe->getTriggerDatabase()->addTrigger( trNodes, t );
 236   return t;
 237 }
 238
 239 Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){
 240   std::vector< Node > nodes;
 241   nodes.push_back( n );
 242   return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars );
 243 }
 244
 245 bool Trigger::isUsable( Node n, Node q ){
 246   if( quantifiers::TermUtil::getInstConstAttr(n)==q ){
 247     if( isAtomicTrigger( n ) ){
 248       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 249         if( !isUsable( n[i], q ) ){
 250           return false;
 251         }
 252       }
 253       return true;
 254     }else if( n.getKind()==INST_CONSTANT ){
 255       return true;
 256     }else{
 257       std::map< Node, Node > coeffs;
 258       if( isBooleanTermTrigger( n ) ){
 259         return true;
 260       }else if( options::purifyTriggers() ){
 261         Node x = getInversionVariable( n );
 262         if( !x.isNull() ){
 263           return true;
 264         }
 265       }
 266     }
 267     return false;
 268   }else{
 269     return true;
 270   }
 271 }
 272
 273 Node Trigger::getIsUsableEq( Node q, Node n ) {
 274   Assert( isRelationalTrigger( n ) );
 275   for( unsigned i=0; i<2; i++) {
 276     if( isUsableEqTerms( q, n[i], n[1-i] ) ){
 277       if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
 278         return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
 279       }else{
 280         return n;
 281       }
 282     }
 283   }
 284   return Node::null();
 285 }
 286
 287 bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
 288   if( n1.getKind()==INST_CONSTANT ){
 289     if( options::relationalTriggers() ){
 290       if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
 291         return true;
 292       }else if( n2.getKind()==INST_CONSTANT ){
 293         return true;
 294       }
 295     }
 296   }else if( isUsableAtomicTrigger( n1, q ) ){
 297     if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermUtil::containsTerm( n1, n2 ) ){
 298       return true;
 299     }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
 300       return true;
 301     }
 302   }
 303   return false;
 304 }
 305
 306 Node Trigger::getIsUsableTrigger( Node n, Node q ) {
 307   bool pol = true;
 308   Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
 309   if( n.getKind()==NOT ){
 310     pol = !pol;
 311     n = n[0];
 312   }
 313   if( n.getKind()==INST_CONSTANT ){
 314     return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
 315   }else if( isRelationalTrigger( n ) ){
 316     Node rtr = getIsUsableEq( q, n );
 317     if( rtr.isNull() && n[0].getType().isReal() ){
 318       //try to solve relation
 319       std::map< Node, Node > m;
 320       if( QuantArith::getMonomialSumLit(n, m) ){
 321         for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
 322           bool trySolve = false;
 323           if( !it->first.isNull() ){
 324             if( it->first.getKind()==INST_CONSTANT ){
 325               trySolve = options::relationalTriggers();
 326             }else if( isUsableTrigger( it->first, q ) ){
 327               trySolve = true;
 328             }
 329           }
 330           if( trySolve ){
 331             Trace("trigger-debug") << "Try to solve for " << it->first << std::endl;
 332             Node veq;
 333             if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
 334               rtr = getIsUsableEq( q, veq );
 335             }
 336             //either all solves will succeed or all solves will fail
 337             break;
 338           }
 339         }
 340       }
 341     }
 342     if( !rtr.isNull() ){
 343       Trace("relational-trigger") << "Relational trigger : " << std::endl;
 344       Trace("relational-trigger") << "    " << rtr << " (from " << n << ")" << std::endl;
 345       Trace("relational-trigger") << "    in quantifier " << q << std::endl;
 346       Node rtr2 = pol ? rtr : rtr.negate();
 347       Trace("relational-trigger") << "    return : " << rtr2 << std::endl;
 348       return rtr2;
 349     }
 350   }else{
 351     Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
 352     if( isUsableAtomicTrigger( n, q ) ){
 353       return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
 354     }
 355   }
 356   return Node::null();
 357 }
 358
 359 bool Trigger::isUsableAtomicTrigger( Node n, Node q ) {
 360   return quantifiers::TermUtil::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
 361 }
 362
 363 bool Trigger::isUsableTrigger( Node n, Node q ){
 364   Node nu = getIsUsableTrigger( n, q );
 365   return !nu.isNull();
 366 }
 367
 368 bool Trigger::isAtomicTrigger( Node n ){
 369   return isAtomicTriggerKind( n.getKind() );
 370 }
 371
 372 bool Trigger::isAtomicTriggerKind( Kind k ) {
 373   return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
 374          || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == UNION
 375          || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER
 376          || k == SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
 377          || k == INT_TO_BITVECTOR || k == HO_APPLY;
 378 }
 379
 380 bool Trigger::isRelationalTrigger( Node n ) {
 381   return isRelationalTriggerKind( n.getKind() );
 382 }
 383
 384 bool Trigger::isRelationalTriggerKind( Kind k ) {
 385   return k==EQUAL || k==GEQ;
 386 }
 387
 388 bool Trigger::isCbqiKind( Kind k ) {
 389   if( quantifiers::TermUtil::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){
 390     return true;
 391   }else{
 392     //CBQI typically works for satisfaction-complete theories
 393     TheoryId t = kindToTheoryId( k );
 394     return t==THEORY_BV || t==THEORY_DATATYPES;
 395   }
 396 }
 397
 398 bool Trigger::isSimpleTrigger( Node n ){
 399   Node t = n.getKind()==NOT ? n[0] : n;
 400   if( t.getKind()==EQUAL ){
 401     if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){
 402       t = t[0];
 403     }
 404   }
 405   if( isAtomicTrigger( t ) ){
 406     for( unsigned i=0; i<t.getNumChildren(); i++ ){
 407       if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermUtil::hasInstConstAttr(t[i]) ){
 408         return false;
 409       }
 410     }
 411     if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){
 412       return false;
 413     }
 414     if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
 415     {
 416       return false;
 417     }
 418     return true;
 419   }else{
 420     return false;
 421   }
 422 }
 423
 424 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
 425 void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo,
 426                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
 427                                 bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){
 428   std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
 429   if( itv==visited.end() ){
 430     visited[ n ].clear();
 431     Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
 432     if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
 433       Node nu;
 434       bool nu_single = false;
 435       if( knowIsUsable ){
 436         nu = n;
 437       }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
 438         nu = getIsUsableTrigger( n, q );
 439         if( !nu.isNull() && nu!=n ){
 440           collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true );
 441           // copy to n
 442           visited[n].insert( visited[n].end(), added.begin(), added.end() );
 443           return;
 444         }
 445       }
 446       if( !nu.isNull() ){
 447         Assert( nu==n );
 448         Assert( nu.getKind()!=NOT );
 449         Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
 450         Node reqEq;
 451         if( nu.getKind()==EQUAL ){
 452           if( isAtomicTrigger( nu[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu[1]) ){
 453             if( hasPol ){
 454               reqEq = nu[1];
 455             }
 456             nu = nu[0];
 457           }
 458         }
 459         Assert( reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr( reqEq ) );
 460         Assert( isUsableTrigger( nu, q ) );
 461         //tinfo.find( nu )==tinfo.end()
 462         Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
 463         tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
 464         nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
 465       }
 466       Node nrec = nu.isNull() ? n : nu;
 467       std::vector< Node > added2;
 468       for( unsigned i=0; i<nrec.getNumChildren(); i++ ){
 469         bool newHasPol, newPol;
 470         bool newHasEPol, newEPol;
 471         QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
 472         QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
 473         collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
 474       }
 475       // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
 476       if( !nu.isNull() ){
 477         bool rm_nu = false;
 478         for( unsigned i=0; i<added2.size(); i++ ){
 479           Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl;
 480           Assert( added2[i]!=nu );
 481           // if child was not already removed
 482           if( tinfo.find( added2[i] )!=tinfo.end() ){
 483             if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
 484               //discard all subterms
 485               Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
 486               visited[ added2[i] ].clear();
 487               tinfo.erase( added2[i] );
 488             }else{
 489               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
 490                 //discard if we added a subterm as a trigger with all variables that nu has
 491                 Trace("auto-gen-trigger-debug2") << "......subsumes parent." << std::endl;
 492                 rm_nu = true;
 493               }
 494               if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){
 495                 added.push_back( added2[i] );
 496               }
 497             }
 498           }
 499         }
 500         if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
 501           tinfo.erase( nu );
 502         }else{
 503           if( std::find( added.begin(), added.end(), nu )==added.end() ){
 504             added.push_back( nu );
 505           }
 506         }
 507         visited[n].insert( visited[n].end(), added.begin(), added.end() );
 508       }
 509     }
 510   }else{
 511     for( unsigned i=0; i<itv->second.size(); ++i ){
 512       Node t = itv->second[i];
 513       if( std::find( added.begin(), added.end(), t )==added.end() ){
 514         added.push_back( t );
 515       }
 516     }
 517   }
 518 }
 519
 520 bool Trigger::isBooleanTermTrigger( Node n ) {
 521   if( n.getKind()==ITE ){
 522     //check for boolean term converted to ITE
 523     if( n[0].getKind()==INST_CONSTANT &&
 524         n[1].getKind()==CONST_BITVECTOR &&
 525         n[2].getKind()==CONST_BITVECTOR ){
 526       if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
 527           n[1].getConst<BitVector>().toInteger()==1 &&
 528           n[2].getConst<BitVector>().toInteger()==0 ){
 529         return true;
 530       }
 531     }
 532   }
 533   return false;
 534 }
 535
 536 bool Trigger::isPureTheoryTrigger( Node n ) {
 537   if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){  //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
 538     return false;
 539   }else{
 540     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 541       if( !isPureTheoryTrigger( n[i] ) ){
 542         return false;
 543       }
 544     }
 545     return true;
 546   }
 547 }
 548
 549 int Trigger::getTriggerWeight( Node n ) {
 550   if( isAtomicTrigger( n ) ){
 551     return 0;
 552   }else{
 553     if( options::relationalTriggers() ){
 554       if( isRelationalTrigger( n ) ){
 555         for( unsigned i=0; i<2; i++ ){
 556           if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermUtil::hasInstConstAttr( n[1-i] ) ){
 557             return 0;
 558           }
 559         }
 560       }
 561     }
 562     return 1;
 563   }
 564 }
 565
 566 bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
 567   if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
 568     if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
 569       bool hasVar = false;
 570       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 571         if( n[i].getKind()==INST_CONSTANT ){
 572           hasVar = true;
 573           if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
 574             vars.push_back( n[i] );
 575           }else{
 576             //do not allow duplicate variables
 577             return false;
 578           }
 579         }else{
 580           //do not allow nested function applications
 581           return false;
 582         }
 583       }
 584       if( hasVar ){
 585         patTerms.push_back( n );
 586       }
 587     }
 588   }else{
 589     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 590       if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
 591         return false;
 592       }
 593     }
 594   }
 595   return true;
 596 }
 597
 598 void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude,
 599                                std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
 600   std::map< Node, std::vector< Node > > visited;
 601   if( filterInst ){
 602     //immediately do not consider any term t for which another term is an instance of t
 603     std::vector< Node > patTerms2;
 604     std::map< Node, TriggerTermInfo > tinfo2;
 605     collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
 606     std::vector< Node > temp;
 607     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
 608     quantifiers::TermUtil::filterInstances( temp );
 609     if( temp.size()!=patTerms2.size() ){
 610       Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
 611       Trace("trigger-filter-instance") << "Old: ";
 612       for( unsigned i=0; i<patTerms2.size(); i++ ){
 613         Trace("trigger-filter-instance") << patTerms2[i] << " ";
 614       }
 615       Trace("trigger-filter-instance") << std::endl << "New: ";
 616       for( unsigned i=0; i<temp.size(); i++ ){
 617         Trace("trigger-filter-instance") << temp[i] << " ";
 618       }
 619       Trace("trigger-filter-instance") << std::endl;
 620     }
 621     if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
 622       for( unsigned i=0; i<temp.size(); i++ ){
 623         //copy information
 624         tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
 625         tinfo[temp[i]].d_reqPol = tinfo2[temp[i]].d_reqPol;
 626         tinfo[temp[i]].d_reqPolEq = tinfo2[temp[i]].d_reqPolEq;
 627         patTerms.push_back( temp[i] );
 628       }
 629       return;
 630     }else{
 631       //do not consider terms that have instances
 632       for( unsigned i=0; i<patTerms2.size(); i++ ){
 633         if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
 634           visited[ patTerms2[i] ].clear();
 635         }
 636       }
 637     }
 638   }
 639   std::vector< Node > added;
 640   collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
 641   for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
 642     patTerms.push_back( it->first );
 643   }
 644 }
 645
 646 Node Trigger::getInversionVariable( Node n ) {
 647   if( n.getKind()==INST_CONSTANT ){
 648     return n;
 649   }else if( n.getKind()==PLUS || n.getKind()==MULT ){
 650     Node ret;
 651     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 652       if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
 653         if( ret.isNull() ){
 654           ret = getInversionVariable( n[i] );
 655           if( ret.isNull() ){
 656             Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
 657             return Node::null();
 658           }
 659         }else{
 660           return Node::null();
 661         }
 662       }else if( n.getKind()==MULT ){
 663         if( !n[i].isConst() ){
 664           Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
 665           return Node::null();
 666         }
 667         /*
 668         else if( n.getType().isInteger() ){
 669           Rational r = n[i].getConst<Rational>();
 670           if( r!=Rational(-1) && r!=Rational(1) ){
 671             Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
 672             return Node::null();
 673           }
 674         }
 675         */
 676       }
 677     }
 678     return ret;
 679   }else{
 680     Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl;
 681   }
 682   return Node::null();
 683 }
 684
 685 Node Trigger::getInversion( Node n, Node x ) {
 686   if( n.getKind()==INST_CONSTANT ){
 687     return x;
 688   }else if( n.getKind()==PLUS || n.getKind()==MULT ){
 689     int cindex = -1;
 690     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 691       if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
 692         if( n.getKind()==PLUS ){
 693           x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
 694         }else if( n.getKind()==MULT ){
 695           Assert( n[i].isConst() );
 696           if( x.getType().isInteger() ){
 697             Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
 698             if( !n[i].getConst<Rational>().abs().isOne() ){
 699               x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff );
 700             }
 701             if( n[i].getConst<Rational>().sgn()<0 ){
 702               x = NodeManager::currentNM()->mkNode( UMINUS, x );
 703             }
 704           }else{
 705             Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
 706             x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
 707           }
 708         }
 709         x = Rewriter::rewrite( x );
 710       }else{
 711         Assert( cindex==-1 );
 712         cindex = i;
 713       }
 714     }
 715     Assert( cindex!=-1 );
 716     return getInversion( n[cindex], x );
 717   }
 718   return Node::null();
 719 }
 720
 721 void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars)
 722 {
 723   std::vector< Node > patTerms;
 724   std::map< Node, TriggerTermInfo > tinfo;
 725   // collect all patterns from n
 726   std::vector< Node > exclude;
 727   collectPatTerms(q, n, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo);
 728   //collect all variables from all patterns in patTerms, add to t_vars
 729   for( unsigned i=0; i<patTerms.size(); i++ ){
 730     quantifiers::TermUtil::getVarContainsNode( q, patTerms[i], t_vars );
 731   }
 732 }
 733
 734 int Trigger::getActiveScore() {
 735   return d_mg->getActiveScore( d_quantEngine );
 736 }
 737
 738 TriggerTrie::TriggerTrie()
 739 {}
 740
 741 TriggerTrie::~TriggerTrie() {
 742   for(std::map< TNode, TriggerTrie* >::iterator i = d_children.begin(), iend = d_children.end();
 743       i != iend; ++i) {
 744     TriggerTrie* current = (*i).second;
 745     delete current;
 746   }
 747   d_children.clear();
 748
 749   for( unsigned i=0; i<d_tr.size(); i++ ){
 750     delete d_tr[i];
 751   }
 752 }
 753
 754 inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
 755 {
 756   std::vector<Node> temp;
 757   temp.insert(temp.begin(), nodes.begin(), nodes.end());
 758   std::sort(temp.begin(), temp.end());
 759   TriggerTrie* tt = this;
 760   for (const Node& n : temp)
 761   {
 762     std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
 763     if (itt == tt->d_children.end())
 764     {
 765       return NULL;
 766     }
 767     else
 768     {
 769       tt = itt->second;
 770     }
 771   }
 772   return tt->d_tr.empty() ? NULL : tt->d_tr[0];
 773 }
 774
 775 void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
 776 {
 777   std::vector<Node> temp;
 778   temp.insert(temp.begin(), nodes.begin(), nodes.end());
 779   std::sort(temp.begin(), temp.end());
 780   TriggerTrie* tt = this;
 781   for (const Node& n : temp)
 782   {
 783     std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
 784     if (itt == tt->d_children.end())
 785     {
 786       TriggerTrie* ttn = new TriggerTrie;
 787       tt->d_children[n] = ttn;
 788       tt = ttn;
 789     }
 790     else
 791     {
 792       tt = itt->second;
 793     }
 794   }
 795   tt->d_tr.push_back(t);
 796 }
 797
 798 }/* CVC4::theory::inst namespace */
 799 }/* CVC4::theory namespace */
 800 }/* CVC4 namespace */