src/theory/quantifiers/term_database.cpp

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