src/theory/quantifiers/term_database.cpp

   1 /*********************                                                        */
   2 /*! \file term_database.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 term databse class
  13  **/
  14
  15 #include "theory/quantifiers/term_database.h"
  16
  17 #include "options/base_options.h"
  18 #include "options/quantifiers_options.h"
  19 #include "options/uf_options.h"
  20 #include "theory/quantifiers/quantifiers_attributes.h"
  21 #include "theory/quantifiers/term_util.h"
  22 #include "theory/quantifiers/ematching/trigger.h"
  23 #include "theory/quantifiers_engine.h"
  24 #include "theory/theory_engine.h"
  25
  26 using namespace std;
  27 using namespace CVC4::kind;
  28 using namespace CVC4::context;
  29 using namespace CVC4::theory::inst;
  30
  31 namespace CVC4 {
  32 namespace theory {
  33 namespace quantifiers {
  34
  35 TermDb::TermDb(context::Context* c, context::UserContext* u,
  36                QuantifiersEngine* qe)
  37     : d_quantEngine(qe),
  38       d_inactive_map(c) {
  39   d_consistent_ee = true;
  40   d_true = NodeManager::currentNM()->mkConst(true);
  41   d_false = NodeManager::currentNM()->mkConst(false);
  42 }
  43
  44 TermDb::~TermDb(){
  45
  46 }
  47
  48 void TermDb::registerQuantifier( Node q ) {
  49   Assert( q[0].getNumChildren()==d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ) );
  50   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
  51     Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
  52     setTermInactive( ic );
  53   }
  54 }
  55
  56 unsigned TermDb::getNumOperators() { return d_ops.size(); }
  57 Node TermDb::getOperator(unsigned i)
  58 {
  59   Assert(i < d_ops.size());
  60   return d_ops[i];
  61 }
  62
  63 /** ground terms */
  64 unsigned TermDb::getNumGroundTerms(Node f) const
  65 {
  66   std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
  67   if( it!=d_op_map.end() ){
  68     return it->second.size();
  69   }else{
  70     return 0;
  71   }
  72 }
  73
  74 Node TermDb::getGroundTerm(Node f, unsigned i) const
  75 {
  76   std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
  77   if (it != d_op_map.end())
  78   {
  79     Assert(i < it->second.size());
  80     return it->second[i];
  81   }
  82   else
  83   {
  84     Assert(false);
  85     return Node::null();
  86   }
  87 }
  88
  89 unsigned TermDb::getNumTypeGroundTerms(TypeNode tn) const
  90 {
  91   std::map<TypeNode, std::vector<Node> >::const_iterator it =
  92       d_type_map.find(tn);
  93   if( it!=d_type_map.end() ){
  94     return it->second.size();
  95   }else{
  96     return 0;
  97   }
  98 }
  99
 100 Node TermDb::getTypeGroundTerm(TypeNode tn, unsigned i) const
 101 {
 102   std::map<TypeNode, std::vector<Node> >::const_iterator it =
 103       d_type_map.find(tn);
 104   if (it != d_type_map.end())
 105   {
 106     Assert(i < it->second.size());
 107     return it->second[i];
 108   }
 109   else
 110   {
 111     Assert(false);
 112     return Node::null();
 113   }
 114 }
 115
 116 Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn)
 117 {
 118   std::map<TypeNode, std::vector<Node> >::const_iterator it =
 119       d_type_map.find(tn);
 120   if (it != d_type_map.end())
 121   {
 122     Assert(!it->second.empty());
 123     return it->second[0];
 124   }
 125   else
 126   {
 127     return getOrMakeTypeFreshVariable(tn);
 128   }
 129 }
 130
 131 Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
 132 {
 133   std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
 134       d_type_fv.find(tn);
 135   if (it == d_type_fv.end())
 136   {
 137     std::stringstream ss;
 138     ss << language::SetLanguage(options::outputLanguage());
 139     ss << "e_" << tn;
 140     Node k = NodeManager::currentNM()->mkSkolem(
 141         ss.str(), tn, "is a termDb fresh variable");
 142     Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
 143                    << std::endl;
 144     if (options::instMaxLevel() != -1)
 145     {
 146       QuantAttributes::setInstantiationLevelAttr(k, 0);
 147     }
 148     d_type_fv[tn] = k;
 149     return k;
 150   }
 151   else
 152   {
 153     return it->second;
 154   }
 155 }
 156
 157 Node TermDb::getMatchOperator( Node n ) {
 158   Kind k = n.getKind();
 159   //datatype operators may be parametric, always assume they are
 160   if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
 161       k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO || k==HO_APPLY ){
 162     //since it is parametric, use a particular one as op
 163     TypeNode tn = n[0].getType();
 164     Node op = n.getOperator();
 165     std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op );
 166     if( ito!=d_par_op_map.end() ){
 167       std::map< TypeNode, Node >::iterator it = ito->second.find( tn );
 168       if( it!=ito->second.end() ){
 169         return it->second;
 170       }
 171     }
 172     Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl;
 173     d_par_op_map[op][tn] = n;
 174     return n;
 175   }else if( inst::Trigger::isAtomicTriggerKind( k ) ){
 176     return n.getOperator();
 177   }else{
 178     return Node::null();
 179   }
 180 }
 181
 182 void TermDb::addTerm(Node n,
 183                      std::set<Node>& added,
 184                      bool withinQuant,
 185                      bool withinInstClosure)
 186 {
 187   //don't add terms in quantifier bodies
 188   if( withinQuant && !options::registerQuantBodyTerms() ){
 189     return;
 190   }
 191   bool rec = false;
 192   if (d_processed.find(n) == d_processed.end())
 193   {
 194     d_processed.insert(n);
 195     if (!TermUtil::hasInstConstAttr(n))
 196     {
 197       Trace("term-db-debug") << "register term : " << n << std::endl;
 198       d_type_map[n.getType()].push_back(n);
 199       // if this is an atomic trigger, consider adding it
 200       if (inst::Trigger::isAtomicTrigger(n))
 201       {
 202         Trace("term-db") << "register term in db " << n << std::endl;
 203
 204         Node op = getMatchOperator(n);
 205         Trace("term-db-debug") << "  match operator is : " << op << std::endl;
 206         if (d_op_map.find(op) == d_op_map.end())
 207         {
 208           d_ops.push_back(op);
 209         }
 210         d_op_map[op].push_back(n);
 211         added.insert(n);
 212         // If we are higher-order, we may need to register more terms.
 213         if (options::ufHo())
 214         {
 215           addTermHo(n, added, withinQuant, withinInstClosure);
 216         }
 217       }
 218     }
 219     else
 220     {
 221       setTermInactive(n);
 222     }
 223     rec = true;
 224   }
 225   if (withinInstClosure
 226       && d_iclosure_processed.find(n) == d_iclosure_processed.end())
 227   {
 228     d_iclosure_processed.insert(n);
 229     rec = true;
 230   }
 231   if (rec && !n.isClosure())
 232   {
 233     for (const Node& nc : n)
 234     {
 235       addTerm(nc, added, withinQuant, withinInstClosure);
 236     }
 237   }
 238 }
 239
 240 void TermDb::computeArgReps( TNode n ) {
 241   if (d_arg_reps.find(n) == d_arg_reps.end())
 242   {
 243     eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
 244     for (const TNode& nc : n)
 245     {
 246       TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
 247       d_arg_reps[n].push_back( r );
 248     }
 249   }
 250 }
 251
 252 void TermDb::computeUfEqcTerms( TNode f ) {
 253   Assert( f==getOperatorRepresentative( f ) );
 254   if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
 255   {
 256     return;
 257   }
 258   d_func_map_eqc_trie[f].clear();
 259   // get the matchable operators in the equivalence class of f
 260   std::vector<TNode> ops;
 261   ops.push_back(f);
 262   if (options::ufHo())
 263   {
 264     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
 265   }
 266   eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
 267   for (const Node& ff : ops)
 268   {
 269     for (const TNode& n : d_op_map[ff])
 270     {
 271       if (hasTermCurrent(n) && isTermActive(n))
 272       {
 273         computeArgReps(n);
 274         TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : n;
 275         d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]);
 276       }
 277     }
 278   }
 279 }
 280
 281 void TermDb::computeUfTerms( TNode f ) {
 282   if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
 283   {
 284     // already computed
 285     return;
 286   }
 287   Assert( f==getOperatorRepresentative( f ) );
 288   d_op_nonred_count[f] = 0;
 289   // get the matchable operators in the equivalence class of f
 290   std::vector<TNode> ops;
 291   ops.push_back(f);
 292   if (options::ufHo())
 293   {
 294     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
 295   }
 296   Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
 297   unsigned congruentCount = 0;
 298   unsigned nonCongruentCount = 0;
 299   unsigned alreadyCongruentCount = 0;
 300   unsigned relevantCount = 0;
 301   eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
 302   NodeManager* nm = NodeManager::currentNM();
 303   for (const Node& ff : ops)
 304   {
 305     std::map<Node, std::vector<Node> >::iterator it = d_op_map.find(ff);
 306     if (it == d_op_map.end())
 307     {
 308       // no terms for this operator
 309       continue;
 310     }
 311     Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
 312     for (const Node& n : it->second)
 313     {
 314       // to be added to term index, term must be relevant, and exist in EE
 315       if (!hasTermCurrent(n) || !ee->hasTerm(n))
 316       {
 317         Trace("term-db-debug") << n << " is not relevant." << std::endl;
 318         continue;
 319       }
 320
 321       relevantCount++;
 322       if (!isTermActive(n))
 323       {
 324         Trace("term-db-debug") << n << " is already redundant." << std::endl;
 325         alreadyCongruentCount++;
 326         continue;
 327       }
 328
 329       computeArgReps(n);
 330       Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
 331       for (unsigned i = 0, size = d_arg_reps[n].size(); i < size; i++)
 332       {
 333         Trace("term-db-debug") << d_arg_reps[n][i] << " ";
 334         if (std::find(d_func_map_rel_dom[f][i].begin(),
 335                       d_func_map_rel_dom[f][i].end(),
 336                       d_arg_reps[n][i])
 337             == d_func_map_rel_dom[f][i].end())
 338         {
 339           d_func_map_rel_dom[f][i].push_back(d_arg_reps[n][i]);
 340         }
 341       }
 342       Trace("term-db-debug") << std::endl;
 343       Assert(ee->hasTerm(n));
 344       Trace("term-db-debug") << "  and value : " << ee->getRepresentative(n)
 345                              << std::endl;
 346       Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]);
 347       Assert(ee->hasTerm(at));
 348       Trace("term-db-debug2") << "...add term returned " << at << std::endl;
 349       if (at != n && ee->areEqual(at, n))
 350       {
 351         setTermInactive(n);
 352         Trace("term-db-debug") << n << " is redundant." << std::endl;
 353         congruentCount++;
 354         continue;
 355       }
 356       if (ee->areDisequal(at, n, false))
 357       {
 358         std::vector<Node> lits;
 359         lits.push_back(nm->mkNode(EQUAL, at, n));
 360         bool success = true;
 361         if (options::ufHo())
 362         {
 363           // operators might be disequal
 364           if (ops.size() > 1)
 365           {
 366             Node atf = getMatchOperator(at);
 367             Node nf = getMatchOperator(n);
 368             if (atf != nf)
 369             {
 370               if (at.getKind() == APPLY_UF && n.getKind() == APPLY_UF)
 371               {
 372                 lits.push_back(atf.eqNode(nf).negate());
 373               }
 374               else
 375               {
 376                 success = false;
 377                 Assert(false);
 378               }
 379             }
 380           }
 381         }
 382         if (success)
 383         {
 384           Assert(at.getNumChildren() == n.getNumChildren());
 385           for (unsigned k = 0, size = at.getNumChildren(); k < size; k++)
 386           {
 387             if (at[k] != n[k])
 388             {
 389               lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate());
 390             }
 391           }
 392           Node lem = lits.size() == 1 ? lits[0] : nm->mkNode(OR, lits);
 393           if (Trace.isOn("term-db-lemma"))
 394           {
 395             Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
 396                                    << n << "!!!!" << std::endl;
 397             if (!d_quantEngine->getTheoryEngine()->needCheck())
 398             {
 399               Trace("term-db-lemma") << "  all theories passed with no lemmas."
 400                                      << std::endl;
 401               // we should be a full effort check, prior to theory combination
 402             }
 403             Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
 404           }
 405           d_quantEngine->addLemma(lem);
 406           d_quantEngine->setConflict();
 407           d_consistent_ee = false;
 408           return;
 409         }
 410       }
 411       nonCongruentCount++;
 412       d_op_nonred_count[f]++;
 413     }
 414     if (Trace.isOn("tdb"))
 415     {
 416       Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount
 417                    << " / ";
 418       Trace("tdb") << (nonCongruentCount + congruentCount) << " / "
 419                    << (nonCongruentCount + congruentCount
 420                        + alreadyCongruentCount)
 421                    << " / ";
 422       Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
 423     }
 424   }
 425 }
 426
 427 void TermDb::addTermHo(Node n,
 428                        std::set<Node>& added,
 429                        bool withinQuant,
 430                        bool withinInstClosure)
 431 {
 432   Assert(options::ufHo());
 433   if (n.getType().isFunction())
 434   {
 435     // nothing special to do with functions
 436     return;
 437   }
 438   NodeManager* nm = NodeManager::currentNM();
 439   Node curr = n;
 440   std::vector<Node> args;
 441   while (curr.getKind() == HO_APPLY)
 442   {
 443     args.insert(args.begin(), curr[1]);
 444     curr = curr[0];
 445     if (!curr.isVar())
 446     {
 447       // purify the term
 448       std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(curr);
 449       Node psk;
 450       if (itp == d_ho_fun_op_purify.end())
 451       {
 452         psk = nm->mkSkolem("pfun",
 453                            curr.getType(),
 454                            "purify for function operator term indexing");
 455         d_ho_fun_op_purify[curr] = psk;
 456         // we do not add it to d_ops since it is an internal operator
 457       }
 458       else
 459       {
 460         psk = itp->second;
 461       }
 462       std::vector<Node> children;
 463       children.push_back(psk);
 464       children.insert(children.end(), args.begin(), args.end());
 465       Node p_n = nm->mkNode(APPLY_UF, children);
 466       Trace("term-db") << "register term in db (via purify) " << p_n
 467                        << std::endl;
 468       // also add this one internally
 469       d_op_map[psk].push_back(p_n);
 470       // maintain backwards mapping
 471       d_ho_purify_to_term[p_n] = n;
 472     }
 473   }
 474   if (!args.empty() && curr.isVar())
 475   {
 476     // also add standard application version
 477     args.insert(args.begin(), curr);
 478     Node uf_n = nm->mkNode(APPLY_UF, args);
 479     addTerm(uf_n, added, withinQuant, withinInstClosure);
 480   }
 481 }
 482
 483 Node TermDb::getOperatorRepresentative( TNode op ) const {
 484   std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op );
 485   if( it!=d_ho_op_rep.end() ){
 486     return it->second;
 487   }else{
 488     return op;
 489   }
 490 }
 491
 492 bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
 493   if( options::ufHo() ){
 494     f = getOperatorRepresentative( f );
 495   }
 496   computeUfTerms( f );
 497   Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) ||
 498           d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r );
 499   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
 500   if( it != d_func_map_rel_dom.end() ){
 501     std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
 502     if( it2!=it->second.end() ){
 503       return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end();
 504     }else{
 505       return false;
 506     }
 507   }else{
 508     return false;
 509   }
 510 }
 511
 512 Node TermDb::evaluateTerm2(TNode n,
 513                            std::map<TNode, Node>& visited,
 514                            std::vector<Node>& exp,
 515                            EqualityQuery* qy,
 516                            bool useEntailmentTests,
 517                            bool computeExp,
 518                            bool reqHasTerm)
 519 {
 520   std::map< TNode, Node >::iterator itv = visited.find( n );
 521   if( itv != visited.end() ){
 522     return itv->second;
 523   }
 524   size_t prevSize = exp.size();
 525   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
 526   Node ret = n;
 527   if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
 528     //do nothing
 529   }
 530   else if (qy->hasTerm(n))
 531   {
 532     Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
 533     ret = qy->getRepresentative(n);
 534     if (computeExp)
 535     {
 536       if (n != ret)
 537       {
 538         exp.push_back(n.eqNode(ret));
 539       }
 540     }
 541     reqHasTerm = false;
 542   }
 543   else if (n.hasOperator())
 544   {
 545     std::vector<TNode> args;
 546     bool ret_set = false;
 547     Kind k = n.getKind();
 548     std::vector<Node> tempExp;
 549     for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
 550     {
 551       TNode c = evaluateTerm2(n[i],
 552                               visited,
 553                               tempExp,
 554                               qy,
 555                               useEntailmentTests,
 556                               computeExp,
 557                               reqHasTerm);
 558       if (c.isNull())
 559       {
 560         ret = Node::null();
 561         ret_set = true;
 562         break;
 563       }
 564       else if (c == d_true || c == d_false)
 565       {
 566         // short-circuiting
 567         if ((k == AND && c == d_false) || (k == OR && c == d_true))
 568         {
 569           ret = c;
 570           ret_set = true;
 571           reqHasTerm = false;
 572           break;
 573         }
 574         else if (k == ITE && i == 0)
 575         {
 576           ret = evaluateTerm2(n[c == d_true ? 1 : 2],
 577                               visited,
 578                               tempExp,
 579                               qy,
 580                               useEntailmentTests,
 581                               computeExp,
 582                               reqHasTerm);
 583           ret_set = true;
 584           reqHasTerm = false;
 585           break;
 586         }
 587       }
 588       if (computeExp)
 589       {
 590         exp.insert(exp.end(), tempExp.begin(), tempExp.end());
 591       }
 592       Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
 593       args.push_back(c);
 594     }
 595     if (ret_set)
 596     {
 597       // if we short circuited
 598       if (computeExp)
 599       {
 600         exp.clear();
 601         exp.insert(exp.end(), tempExp.begin(), tempExp.end());
 602       }
 603     }
 604     else
 605     {
 606       // get the (indexed) operator of n, if it exists
 607       TNode f = getMatchOperator(n);
 608       // if it is an indexed term, return the congruent term
 609       if (!f.isNull())
 610       {
 611         // if f is congruent to a term indexed by this class
 612         TNode nn = qy->getCongruentTerm(f, args);
 613         Trace("term-db-eval") << "  got congruent term " << nn
 614                               << " from DB for " << n << std::endl;
 615         if (!nn.isNull())
 616         {
 617           if (computeExp)
 618           {
 619             Assert(nn.getNumChildren() == n.getNumChildren());
 620             for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++)
 621             {
 622               if (nn[i] != n[i])
 623               {
 624                 exp.push_back(nn[i].eqNode(n[i]));
 625               }
 626             }
 627           }
 628           ret = qy->getRepresentative(nn);
 629           Trace("term-db-eval") << "return rep" << std::endl;
 630           ret_set = true;
 631           reqHasTerm = false;
 632           Assert(!ret.isNull());
 633           if (computeExp)
 634           {
 635             if (n != ret)
 636             {
 637               exp.push_back(nn.eqNode(ret));
 638             }
 639           }
 640         }
 641       }
 642       if( !ret_set ){
 643         Trace("term-db-eval") << "return rewrite" << std::endl;
 644         // a theory symbol or a new UF term
 645         if (n.getMetaKind() == metakind::PARAMETERIZED)
 646         {
 647           args.insert(args.begin(), n.getOperator());
 648         }
 649         ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
 650         ret = Rewriter::rewrite(ret);
 651         if (ret.getKind() == EQUAL)
 652         {
 653           if (qy->areDisequal(ret[0], ret[1]))
 654           {
 655             ret = d_false;
 656           }
 657         }
 658         if (useEntailmentTests)
 659         {
 660           if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
 661           {
 662             TheoryEngine* te = d_quantEngine->getTheoryEngine();
 663             for (unsigned j = 0; j < 2; j++)
 664             {
 665               std::pair<bool, Node> et = te->entailmentCheck(
 666                   THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate());
 667               if (et.first)
 668               {
 669                 ret = j == 0 ? d_true : d_false;
 670                 if (computeExp)
 671                 {
 672                   exp.push_back(et.second);
 673                 }
 674                 break;
 675               }
 676             }
 677           }
 678         }
 679       }
 680     }
 681   }
 682   // must have the term
 683   if (reqHasTerm && !ret.isNull())
 684   {
 685     Kind k = ret.getKind();
 686     if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
 687         && k != FORALL)
 688     {
 689       if (!qy->hasTerm(ret))
 690       {
 691         ret = Node::null();
 692       }
 693     }
 694   }
 695   Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
 696                         << ", reqHasTerm = " << reqHasTerm << std::endl;
 697   // clear the explanation if failed
 698   if (computeExp && ret.isNull())
 699   {
 700     exp.resize(prevSize);
 701   }
 702   visited[n] = ret;
 703   return ret;
 704 }
 705
 706
 707 TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
 708   Assert( !qy->extendsEngine() );
 709   Trace("term-db-entail") << "get entailed term : " << n << std::endl;
 710   if( qy->getEngine()->hasTerm( n ) ){
 711     Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
 712     return n;
 713   }else if( n.getKind()==BOUND_VARIABLE ){
 714     if( hasSubs ){
 715       std::map< TNode, TNode >::iterator it = subs.find( n );
 716       if( it!=subs.end() ){
 717         Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
 718         if( subsRep ){
 719           Assert( qy->getEngine()->hasTerm( it->second ) );
 720           Assert( qy->getEngine()->getRepresentative( it->second )==it->second );
 721           return it->second;
 722         }else{
 723           return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy );
 724         }
 725       }
 726     }
 727   }else if( n.getKind()==ITE ){
 728     for( unsigned i=0; i<2; i++ ){
 729       if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
 730         return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy );
 731       }
 732     }
 733   }else{
 734     if( n.hasOperator() ){
 735       TNode f = getMatchOperator( n );
 736       if( !f.isNull() ){
 737         std::vector< TNode > args;
 738         for( unsigned i=0; i<n.getNumChildren(); i++ ){
 739           TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy );
 740           if( c.isNull() ){
 741             return TNode::null();
 742           }
 743           c = qy->getEngine()->getRepresentative( c );
 744           Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
 745           args.push_back( c );
 746         }
 747         TNode nn = qy->getCongruentTerm( f, args );
 748         Trace("term-db-entail") << "  got congruent term " << nn << " for " << n << std::endl;
 749         return nn;
 750       }
 751     }
 752   }
 753   return TNode::null();
 754 }
 755
 756 Node TermDb::evaluateTerm(TNode n,
 757                           EqualityQuery* qy,
 758                           bool useEntailmentTests,
 759                           bool reqHasTerm)
 760 {
 761   if( qy==NULL ){
 762     qy = d_quantEngine->getEqualityQuery();
 763   }
 764   std::map< TNode, Node > visited;
 765   std::vector<Node> exp;
 766   return evaluateTerm2(
 767       n, visited, exp, qy, useEntailmentTests, false, reqHasTerm);
 768 }
 769
 770 Node TermDb::evaluateTerm(TNode n,
 771                           std::vector<Node>& exp,
 772                           EqualityQuery* qy,
 773                           bool useEntailmentTests,
 774                           bool reqHasTerm)
 775 {
 776   if (qy == NULL)
 777   {
 778     qy = d_quantEngine->getEqualityQuery();
 779   }
 780   std::map<TNode, Node> visited;
 781   return evaluateTerm2(
 782       n, visited, exp, qy, useEntailmentTests, true, reqHasTerm);
 783 }
 784
 785 TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
 786   if( qy==NULL ){
 787     qy = d_quantEngine->getEqualityQuery();
 788   }
 789   return getEntailedTerm2( n, subs, subsRep, true, qy );
 790 }
 791
 792 TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
 793   if( qy==NULL ){
 794     qy = d_quantEngine->getEqualityQuery();
 795   }
 796   std::map< TNode, TNode > subs;
 797   return getEntailedTerm2( n, subs, false, false, qy );
 798 }
 799
 800 bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
 801   Assert( !qy->extendsEngine() );
 802   Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
 803   Assert( n.getType().isBoolean() );
 804   if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
 805     TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
 806     if( !n1.isNull() ){
 807       TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
 808       if( !n2.isNull() ){
 809         if( n1==n2 ){
 810           return pol;
 811         }else{
 812           Assert( qy->getEngine()->hasTerm( n1 ) );
 813           Assert( qy->getEngine()->hasTerm( n2 ) );
 814           if( pol ){
 815             return qy->getEngine()->areEqual( n1, n2 );
 816           }else{
 817             return qy->getEngine()->areDisequal( n1, n2, false );
 818           }
 819         }
 820       }
 821     }
 822   }else if( n.getKind()==NOT ){
 823     return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy );
 824   }else if( n.getKind()==OR || n.getKind()==AND ){
 825     bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
 826     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 827       if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){
 828         if( simPol ){
 829           return true;
 830         }
 831       }else{
 832         if( !simPol ){
 833           return false;
 834         }
 835       }
 836     }
 837     return !simPol;
 838   //Boolean equality here
 839   }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
 840     for( unsigned i=0; i<2; i++ ){
 841       if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
 842         unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
 843         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
 844         return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
 845       }
 846     }
 847   }else if( n.getKind()==APPLY_UF ){
 848     TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
 849     if( !n1.isNull() ){
 850       Assert( qy->hasTerm( n1 ) );
 851       if( n1==d_true ){
 852         return pol;
 853       }else if( n1==d_false ){
 854         return !pol;
 855       }else{
 856         return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
 857       }
 858     }
 859   }else if( n.getKind()==FORALL && !pol ){
 860     return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy );
 861   }
 862   return false;
 863 }
 864
 865 bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
 866   if( qy==NULL ){
 867     Assert( d_consistent_ee );
 868     qy = d_quantEngine->getEqualityQuery();
 869   }
 870   std::map< TNode, TNode > subs;
 871   return isEntailed2( n, subs, false, false, pol, qy );
 872 }
 873
 874 bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
 875   if( qy==NULL ){
 876     Assert( d_consistent_ee );
 877     qy = d_quantEngine->getEqualityQuery();
 878   }
 879   return isEntailed2( n, subs, subsRep, true, pol, qy );
 880 }
 881
 882 bool TermDb::isTermActive( Node n ) {
 883   return d_inactive_map.find( n )==d_inactive_map.end();
 884   //return !n.getAttribute(NoMatchAttribute());
 885 }
 886
 887 void TermDb::setTermInactive( Node n ) {
 888   d_inactive_map[n] = true;
 889   //Trace("term-db-debug2") << "set no match attribute" << std::endl;
 890   //NoMatchAttribute nma;
 891   //n.setAttribute(nma,true);
 892 }
 893
 894 bool TermDb::hasTermCurrent( Node n, bool useMode ) {
 895   if( !useMode ){
 896     return d_has_map.find( n )!=d_has_map.end();
 897   }else{
 898     //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
 899     if( options::termDbMode()==TERM_DB_ALL ){
 900       return true;
 901     }else if( options::termDbMode()==TERM_DB_RELEVANT ){
 902       return d_has_map.find( n )!=d_has_map.end();
 903     }else{
 904       Assert( false );
 905       return false;
 906     }
 907   }
 908 }
 909
 910 bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
 911 {
 912   if( options::lteRestrictInstClosure() ){
 913     //has to be both in inst closure and in ground assertions
 914     if( !isInstClosure( n ) ){
 915       Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
 916       return false;
 917     }
 918     // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
 919     if( !hasTermCurrent( n, false ) ){
 920       Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
 921       return false;
 922     }
 923   }
 924   if( options::instMaxLevel()!=-1 ){
 925     if( n.hasAttribute(InstLevelAttribute()) ){
 926       int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f );
 927       unsigned ml = fml>=0 ? fml : options::instMaxLevel();
 928
 929       if( n.getAttribute(InstLevelAttribute())>ml ){
 930         Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
 931         Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
 932         return false;
 933       }
 934     }else{
 935       if( options::instLevelInputOnly() ){
 936         Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
 937         return false;
 938       }
 939     }
 940   }
 941   // it cannot have instantiation constants, which originate from
 942   // counterexample-guided instantiation strategies.
 943   return !TermUtil::hasInstConstAttr(n);
 944 }
 945
 946 Node TermDb::getEligibleTermInEqc( TNode r ) {
 947   if( isTermEligibleForInstantiation( r, TNode::null() ) ){
 948     return r;
 949   }else{
 950     std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
 951     if( it==d_term_elig_eqc.end() ){
 952       Node h;
 953       eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
 954       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
 955       while (!eqc_i.isFinished())
 956       {
 957         TNode n = (*eqc_i);
 958         ++eqc_i;
 959         if (isTermEligibleForInstantiation(n, TNode::null()))
 960         {
 961           h = n;
 962           break;
 963         }
 964       }
 965       d_term_elig_eqc[r] = h;
 966       return h;
 967     }else{
 968       return it->second;
 969     }
 970   }
 971 }
 972
 973 bool TermDb::isInstClosure( Node r ) {
 974   return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
 975 }
 976
 977 void TermDb::setHasTerm( Node n ) {
 978   Trace("term-db-debug2") << "hasTerm : " << n  << std::endl;
 979   //if( inst::Trigger::isAtomicTrigger( n ) ){
 980   if( d_has_map.find( n )==d_has_map.end() ){
 981     d_has_map[n] = true;
 982     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 983       setHasTerm( n[i] );
 984     }
 985   }
 986 }
 987
 988 void TermDb::presolve() {
 989   if( options::incrementalSolving() ){
 990     // reset the caches that are SAT context-independent but user
 991     // context-dependent
 992     d_ops.clear();
 993     d_op_map.clear();
 994     d_type_map.clear();
 995     d_processed.clear();
 996     d_iclosure_processed.clear();
 997   }
 998 }
 999
1000 bool TermDb::reset( Theory::Effort effort ){
1001   d_op_nonred_count.clear();
1002   d_arg_reps.clear();
1003   d_func_map_trie.clear();
1004   d_func_map_eqc_trie.clear();
1005   d_func_map_rel_dom.clear();
1006   d_consistent_ee = true;
1007
1008   eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
1009
1010   Assert(ee->consistent());
1011   // if higher-order, add equalities for the purification terms now
1012   if (options::ufHo())
1013   {
1014     Trace("quant-ho")
1015         << "TermDb::reset : assert higher-order purify equalities..."
1016         << std::endl;
1017     for (std::pair<const Node, Node>& pp : d_ho_purify_to_term)
1018     {
1019       if (ee->hasTerm(pp.second)
1020           && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first)))
1021       {
1022         Node eq;
1023         std::map<Node, Node>::iterator itpe = d_ho_purify_to_eq.find(pp.first);
1024         if (itpe == d_ho_purify_to_eq.end())
1025         {
1026           eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
1027           d_ho_purify_to_eq[pp.first] = eq;
1028         }
1029         else
1030         {
1031           eq = itpe->second;
1032         }
1033         Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
1034         ee->assertEquality(eq, true, eq);
1035         Assert(ee->consistent());
1036       }
1037     }
1038   }
1039
1040   //compute has map
1041   if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
1042     d_has_map.clear();
1043     d_term_elig_eqc.clear();
1044     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1045     while( !eqcs_i.isFinished() ){
1046       TNode r = (*eqcs_i);
1047       bool addedFirst = false;
1048       Node first;
1049       //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
1050       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1051       while( !eqc_i.isFinished() ){
1052         TNode n = (*eqc_i);
1053         if( first.isNull() ){
1054           first = n;
1055         }else{
1056           if( !addedFirst ){
1057             addedFirst = true;
1058             setHasTerm( first );
1059           }
1060           setHasTerm( n );
1061         }
1062         ++eqc_i;
1063       }
1064       ++eqcs_i;
1065     }
1066     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
1067       Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId];
1068       if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
1069         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
1070         for (unsigned i = 0; it != it_end; ++ it, ++i) {
1071           if( (*it).assertion.getKind()!=INST_CLOSURE ){
1072             setHasTerm( (*it).assertion );
1073           }
1074         }
1075       }
1076     }
1077   }
1078   //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
1079   for (const Node& n : d_iclosure_processed)
1080   {
1081     if( !ee->hasTerm( n ) ){
1082       ee->addTerm( n );
1083     }
1084   }
1085
1086   if( options::ufHo() && options::hoMergeTermDb() ){
1087     Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl;
1088     // build operator representative map
1089     d_ho_op_rep.clear();
1090     d_ho_op_slaves.clear();
1091     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1092     while( !eqcs_i.isFinished() ){
1093       TNode r = (*eqcs_i);
1094       if( r.getType().isFunction() ){
1095         Trace("quant-ho") << "  process function eqc " << r << std::endl;
1096         Node first;
1097         eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1098         while( !eqc_i.isFinished() ){
1099           TNode n = (*eqc_i);
1100           Node n_use;
1101           if (n.isVar())
1102           {
1103             n_use = n;
1104           }
1105           else
1106           {
1107             // use its purified variable, if it exists
1108             std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(n);
1109             if (itp != d_ho_fun_op_purify.end())
1110             {
1111               n_use = itp->second;
1112             }
1113           }
1114           Trace("quant-ho") << "  - process " << n_use << ", from " << n
1115                             << std::endl;
1116           if (!n_use.isNull() && d_op_map.find(n_use) != d_op_map.end())
1117           {
1118             if (first.isNull())
1119             {
1120               first = n_use;
1121               d_ho_op_rep[n_use] = n_use;
1122             }
1123             else
1124             {
1125               Trace("quant-ho") << "  have : " << n_use << " == " << first
1126                                 << ", type = " << n_use.getType() << std::endl;
1127               d_ho_op_rep[n_use] = first;
1128               d_ho_op_slaves[first].push_back(n_use);
1129             }
1130           }
1131           ++eqc_i;
1132         }
1133       }
1134       ++eqcs_i;
1135     }
1136     Trace("quant-ho") << "...finished compute equal functions." << std::endl;
1137   }
1138
1139 /*
1140   //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
1141   for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
1142     computeUfTerms( it->first );
1143     if( !d_consistent_ee ){
1144       return false;
1145     }
1146   }
1147 */
1148   return true;
1149 }
1150
1151 TNodeTrie* TermDb::getTermArgTrie(Node f)
1152 {
1153   if( options::ufHo() ){
1154     f = getOperatorRepresentative( f );
1155   }
1156   computeUfTerms( f );
1157   std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1158   if( itut!=d_func_map_trie.end() ){
1159     return &itut->second;
1160   }else{
1161     return NULL;
1162   }
1163 }
1164
1165 TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
1166 {
1167   if( options::ufHo() ){
1168     f = getOperatorRepresentative( f );
1169   }
1170   computeUfEqcTerms( f );
1171   std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
1172   if( itut==d_func_map_eqc_trie.end() ){
1173     return NULL;
1174   }else{
1175     if( eqc.isNull() ){
1176       return &itut->second;
1177     }else{
1178       std::map<TNode, TNodeTrie>::iterator itute =
1179           itut->second.d_data.find(eqc);
1180       if( itute!=itut->second.d_data.end() ){
1181         return &itute->second;
1182       }else{
1183         return NULL;
1184       }
1185     }
1186   }
1187 }
1188
1189 TNode TermDb::getCongruentTerm( Node f, Node n ) {
1190   if( options::ufHo() ){
1191     f = getOperatorRepresentative( f );
1192   }
1193   computeUfTerms( f );
1194   std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1195   if( itut!=d_func_map_trie.end() ){
1196     computeArgReps( n );
1197     return itut->second.existsTerm( d_arg_reps[n] );
1198   }else{
1199     return TNode::null();
1200   }
1201 }
1202
1203 TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
1204   if( options::ufHo() ){
1205     f = getOperatorRepresentative( f );
1206   }
1207   computeUfTerms( f );
1208   return d_func_map_trie[f].existsTerm( args );
1209 }
1210
1211 }/* CVC4::theory::quantifiers namespace */
1212 }/* CVC4::theory namespace */
1213 }/* CVC4 namespace */