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                      std::set<Node>& added,
 203                      bool withinQuant,
 204                      bool withinInstClosure)
 205 {
 206   //don't add terms in quantifier bodies
 207   if( withinQuant && !options::registerQuantBodyTerms() ){
 208     return;
 209   }
 210   bool rec = false;
 211   if (d_processed.find(n) == d_processed.end())
 212   {
 213     d_processed.insert(n);
 214     if (!TermUtil::hasInstConstAttr(n))
 215     {
 216       Trace("term-db-debug") << "register term : " << n << std::endl;
 217       d_type_map[n.getType()].push_back(n);
 218       // if this is an atomic trigger, consider adding it
 219       if (inst::TriggerTermInfo::isAtomicTrigger(n))
 220       {
 221         Trace("term-db") << "register term in db " << n << std::endl;
 222
 223         Node op = getMatchOperator(n);
 224         Trace("term-db-debug") << "  match operator is : " << op << std::endl;
 225         if (d_op_map.find(op) == d_op_map.end())
 226         {
 227           d_ops.push_back(op);
 228         }
 229         d_op_map[op].push_back(n);
 230         added.insert(n);
 231         // If we are higher-order, we may need to register more terms.
 232         if (options::ufHo())
 233         {
 234           addTermHo(n, added, withinQuant, withinInstClosure);
 235         }
 236       }
 237     }
 238     else
 239     {
 240       setTermInactive(n);
 241     }
 242     rec = true;
 243   }
 244   if (withinInstClosure
 245       && d_iclosure_processed.find(n) == d_iclosure_processed.end())
 246   {
 247     d_iclosure_processed.insert(n);
 248     rec = true;
 249   }
 250   if (rec && !n.isClosure())
 251   {
 252     for (const Node& nc : n)
 253     {
 254       addTerm(nc, added, withinQuant, withinInstClosure);
 255     }
 256   }
 257 }
 258
 259 void TermDb::computeArgReps( TNode n ) {
 260   if (d_arg_reps.find(n) == d_arg_reps.end())
 261   {
 262     eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
 263     for (const TNode& nc : n)
 264     {
 265       TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
 266       d_arg_reps[n].push_back( r );
 267     }
 268   }
 269 }
 270
 271 void TermDb::computeUfEqcTerms( TNode f ) {
 272   Assert(f == getOperatorRepresentative(f));
 273   if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
 274   {
 275     return;
 276   }
 277   d_func_map_eqc_trie[f].clear();
 278   // get the matchable operators in the equivalence class of f
 279   std::vector<TNode> ops;
 280   ops.push_back(f);
 281   if (options::ufHo())
 282   {
 283     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
 284   }
 285   eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
 286   for (TNode ff : ops)
 287   {
 288     for (const Node& n : d_op_map[ff])
 289     {
 290       if (hasTermCurrent(n) && isTermActive(n))
 291       {
 292         computeArgReps(n);
 293         TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n);
 294         d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]);
 295       }
 296     }
 297   }
 298 }
 299
 300 void TermDb::computeUfTerms( TNode f ) {
 301   if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
 302   {
 303     // already computed
 304     return;
 305   }
 306   Assert(f == getOperatorRepresentative(f));
 307   d_op_nonred_count[f] = 0;
 308   // get the matchable operators in the equivalence class of f
 309   std::vector<TNode> ops;
 310   ops.push_back(f);
 311   if (options::ufHo())
 312   {
 313     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
 314   }
 315   Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
 316   unsigned congruentCount = 0;
 317   unsigned nonCongruentCount = 0;
 318   unsigned alreadyCongruentCount = 0;
 319   unsigned relevantCount = 0;
 320   NodeManager* nm = NodeManager::currentNM();
 321   for (TNode ff : ops)
 322   {
 323     std::map<Node, std::vector<Node> >::iterator it = d_op_map.find(ff);
 324     if (it == d_op_map.end())
 325     {
 326       // no terms for this operator
 327       continue;
 328     }
 329     Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
 330     for (const Node& n : it->second)
 331     {
 332       // to be added to term index, term must be relevant, and exist in EE
 333       if (!hasTermCurrent(n) || !d_qstate.hasTerm(n))
 334       {
 335         Trace("term-db-debug") << n << " is not relevant." << std::endl;
 336         continue;
 337       }
 338
 339       relevantCount++;
 340       if (!isTermActive(n))
 341       {
 342         Trace("term-db-debug") << n << " is already redundant." << std::endl;
 343         alreadyCongruentCount++;
 344         continue;
 345       }
 346
 347       computeArgReps(n);
 348       Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
 349       for (unsigned i = 0, size = d_arg_reps[n].size(); i < size; i++)
 350       {
 351         Trace("term-db-debug") << d_arg_reps[n][i] << " ";
 352         if (std::find(d_func_map_rel_dom[f][i].begin(),
 353                       d_func_map_rel_dom[f][i].end(),
 354                       d_arg_reps[n][i])
 355             == d_func_map_rel_dom[f][i].end())
 356         {
 357           d_func_map_rel_dom[f][i].push_back(d_arg_reps[n][i]);
 358         }
 359       }
 360       Trace("term-db-debug") << std::endl;
 361       Assert(d_qstate.hasTerm(n));
 362       Trace("term-db-debug")
 363           << "  and value : " << d_qstate.getRepresentative(n) << std::endl;
 364       Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]);
 365       Assert(d_qstate.hasTerm(at));
 366       Trace("term-db-debug2") << "...add term returned " << at << std::endl;
 367       if (at != n && d_qstate.areEqual(at, n))
 368       {
 369         setTermInactive(n);
 370         Trace("term-db-debug") << n << " is redundant." << std::endl;
 371         congruentCount++;
 372         continue;
 373       }
 374       if (d_qstate.areDisequal(at, n))
 375       {
 376         std::vector<Node> lits;
 377         lits.push_back(nm->mkNode(EQUAL, at, n));
 378         bool success = true;
 379         if (options::ufHo())
 380         {
 381           // operators might be disequal
 382           if (ops.size() > 1)
 383           {
 384             Node atf = getMatchOperator(at);
 385             Node nf = getMatchOperator(n);
 386             if (atf != nf)
 387             {
 388               if (at.getKind() == APPLY_UF && n.getKind() == APPLY_UF)
 389               {
 390                 lits.push_back(atf.eqNode(nf).negate());
 391               }
 392               else
 393               {
 394                 success = false;
 395                 Assert(false);
 396               }
 397             }
 398           }
 399         }
 400         if (success)
 401         {
 402           Assert(at.getNumChildren() == n.getNumChildren());
 403           for (unsigned k = 0, size = at.getNumChildren(); k < size; k++)
 404           {
 405             if (at[k] != n[k])
 406             {
 407               lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate());
 408             }
 409           }
 410           Node lem = lits.size() == 1 ? lits[0] : nm->mkNode(OR, lits);
 411           if (Trace.isOn("term-db-lemma"))
 412           {
 413             Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
 414                                    << n << "!!!!" << std::endl;
 415             if (!d_qstate.getValuation().needCheck())
 416             {
 417               Trace("term-db-lemma") << "  all theories passed with no lemmas."
 418                                      << std::endl;
 419               // we should be a full effort check, prior to theory combination
 420             }
 421             Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
 422           }
 423           d_quantEngine->addLemma(lem);
 424           d_qstate.notifyInConflict();
 425           d_consistent_ee = false;
 426           return;
 427         }
 428       }
 429       nonCongruentCount++;
 430       d_op_nonred_count[f]++;
 431     }
 432     if (Trace.isOn("tdb"))
 433     {
 434       Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount
 435                    << " / ";
 436       Trace("tdb") << (nonCongruentCount + congruentCount) << " / "
 437                    << (nonCongruentCount + congruentCount
 438                        + alreadyCongruentCount)
 439                    << " / ";
 440       Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
 441     }
 442   }
 443 }
 444
 445 void TermDb::addTermHo(Node n,
 446                        std::set<Node>& added,
 447                        bool withinQuant,
 448                        bool withinInstClosure)
 449 {
 450   Assert(options::ufHo());
 451   if (n.getType().isFunction())
 452   {
 453     // nothing special to do with functions
 454     return;
 455   }
 456   NodeManager* nm = NodeManager::currentNM();
 457   Node curr = n;
 458   std::vector<Node> args;
 459   while (curr.getKind() == HO_APPLY)
 460   {
 461     args.insert(args.begin(), curr[1]);
 462     curr = curr[0];
 463     if (!curr.isVar())
 464     {
 465       // purify the term
 466       std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(curr);
 467       Node psk;
 468       if (itp == d_ho_fun_op_purify.end())
 469       {
 470         psk = nm->mkSkolem("pfun",
 471                            curr.getType(),
 472                            "purify for function operator term indexing");
 473         d_ho_fun_op_purify[curr] = psk;
 474         // we do not add it to d_ops since it is an internal operator
 475       }
 476       else
 477       {
 478         psk = itp->second;
 479       }
 480       std::vector<Node> children;
 481       children.push_back(psk);
 482       children.insert(children.end(), args.begin(), args.end());
 483       Node p_n = nm->mkNode(APPLY_UF, children);
 484       Trace("term-db") << "register term in db (via purify) " << p_n
 485                        << std::endl;
 486       // also add this one internally
 487       d_op_map[psk].push_back(p_n);
 488       // maintain backwards mapping
 489       d_ho_purify_to_term[p_n] = n;
 490     }
 491   }
 492   if (!args.empty() && curr.isVar())
 493   {
 494     // also add standard application version
 495     args.insert(args.begin(), curr);
 496     Node uf_n = nm->mkNode(APPLY_UF, args);
 497     addTerm(uf_n, added, withinQuant, withinInstClosure);
 498   }
 499 }
 500
 501 Node TermDb::getOperatorRepresentative( TNode op ) const {
 502   std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op );
 503   if( it!=d_ho_op_rep.end() ){
 504     return it->second;
 505   }else{
 506     return op;
 507   }
 508 }
 509
 510 bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
 511   if( options::ufHo() ){
 512     f = getOperatorRepresentative( f );
 513   }
 514   computeUfTerms( f );
 515   Assert(!d_qstate.getEqualityEngine()->hasTerm(r)
 516          || d_qstate.getEqualityEngine()->getRepresentative(r) == r);
 517   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
 518   if( it != d_func_map_rel_dom.end() ){
 519     std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
 520     if( it2!=it->second.end() ){
 521       return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end();
 522     }else{
 523       return false;
 524     }
 525   }else{
 526     return false;
 527   }
 528 }
 529
 530 Node TermDb::evaluateTerm2(TNode n,
 531                            std::map<TNode, Node>& visited,
 532                            std::vector<Node>& exp,
 533                            bool useEntailmentTests,
 534                            bool computeExp,
 535                            bool reqHasTerm)
 536 {
 537   std::map< TNode, Node >::iterator itv = visited.find( n );
 538   if( itv != visited.end() ){
 539     return itv->second;
 540   }
 541   size_t prevSize = exp.size();
 542   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
 543   Node ret = n;
 544   if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
 545     //do nothing
 546   }
 547   else if (d_qstate.hasTerm(n))
 548   {
 549     Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
 550     ret = d_qstate.getRepresentative(n);
 551     if (computeExp)
 552     {
 553       if (n != ret)
 554       {
 555         exp.push_back(n.eqNode(ret));
 556       }
 557     }
 558     reqHasTerm = false;
 559   }
 560   else if (n.hasOperator())
 561   {
 562     std::vector<TNode> args;
 563     bool ret_set = false;
 564     Kind k = n.getKind();
 565     std::vector<Node> tempExp;
 566     for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
 567     {
 568       TNode c = evaluateTerm2(n[i],
 569                               visited,
 570                               tempExp,
 571                               useEntailmentTests,
 572                               computeExp,
 573                               reqHasTerm);
 574       if (c.isNull())
 575       {
 576         ret = Node::null();
 577         ret_set = true;
 578         break;
 579       }
 580       else if (c == d_true || c == d_false)
 581       {
 582         // short-circuiting
 583         if ((k == AND && c == d_false) || (k == OR && c == d_true))
 584         {
 585           ret = c;
 586           ret_set = true;
 587           reqHasTerm = false;
 588           break;
 589         }
 590         else if (k == ITE && i == 0)
 591         {
 592           ret = evaluateTerm2(n[c == d_true ? 1 : 2],
 593                               visited,
 594                               tempExp,
 595                               useEntailmentTests,
 596                               computeExp,
 597                               reqHasTerm);
 598           ret_set = true;
 599           reqHasTerm = false;
 600           break;
 601         }
 602       }
 603       if (computeExp)
 604       {
 605         exp.insert(exp.end(), tempExp.begin(), tempExp.end());
 606       }
 607       Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
 608       args.push_back(c);
 609     }
 610     if (ret_set)
 611     {
 612       // if we short circuited
 613       if (computeExp)
 614       {
 615         exp.clear();
 616         exp.insert(exp.end(), tempExp.begin(), tempExp.end());
 617       }
 618     }
 619     else
 620     {
 621       // get the (indexed) operator of n, if it exists
 622       TNode f = getMatchOperator(n);
 623       // if it is an indexed term, return the congruent term
 624       if (!f.isNull())
 625       {
 626         // if f is congruent to a term indexed by this class
 627         TNode nn = getCongruentTerm(f, args);
 628         Trace("term-db-eval") << "  got congruent term " << nn
 629                               << " from DB for " << n << std::endl;
 630         if (!nn.isNull())
 631         {
 632           if (computeExp)
 633           {
 634             Assert(nn.getNumChildren() == n.getNumChildren());
 635             for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++)
 636             {
 637               if (nn[i] != n[i])
 638               {
 639                 exp.push_back(nn[i].eqNode(n[i]));
 640               }
 641             }
 642           }
 643           ret = d_qstate.getRepresentative(nn);
 644           Trace("term-db-eval") << "return rep" << std::endl;
 645           ret_set = true;
 646           reqHasTerm = false;
 647           Assert(!ret.isNull());
 648           if (computeExp)
 649           {
 650             if (n != ret)
 651             {
 652               exp.push_back(nn.eqNode(ret));
 653             }
 654           }
 655         }
 656       }
 657       if( !ret_set ){
 658         Trace("term-db-eval") << "return rewrite" << std::endl;
 659         // a theory symbol or a new UF term
 660         if (n.getMetaKind() == metakind::PARAMETERIZED)
 661         {
 662           args.insert(args.begin(), n.getOperator());
 663         }
 664         ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
 665         ret = Rewriter::rewrite(ret);
 666         if (ret.getKind() == EQUAL)
 667         {
 668           if (d_qstate.areDisequal(ret[0], ret[1]))
 669           {
 670             ret = d_false;
 671           }
 672         }
 673         if (useEntailmentTests)
 674         {
 675           if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
 676           {
 677             TheoryEngine* te = d_quantEngine->getTheoryEngine();
 678             for (unsigned j = 0; j < 2; j++)
 679             {
 680               std::pair<bool, Node> et = te->entailmentCheck(
 681                   options::TheoryOfMode::THEORY_OF_TYPE_BASED,
 682                   j == 0 ? ret : ret.negate());
 683               if (et.first)
 684               {
 685                 ret = j == 0 ? d_true : d_false;
 686                 if (computeExp)
 687                 {
 688                   exp.push_back(et.second);
 689                 }
 690                 break;
 691               }
 692             }
 693           }
 694         }
 695       }
 696     }
 697   }
 698   // must have the term
 699   if (reqHasTerm && !ret.isNull())
 700   {
 701     Kind k = ret.getKind();
 702     if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
 703         && k != FORALL)
 704     {
 705       if (!d_qstate.hasTerm(ret))
 706       {
 707         ret = Node::null();
 708       }
 709     }
 710   }
 711   Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
 712                         << ", reqHasTerm = " << reqHasTerm << std::endl;
 713   // clear the explanation if failed
 714   if (computeExp && ret.isNull())
 715   {
 716     exp.resize(prevSize);
 717   }
 718   visited[n] = ret;
 719   return ret;
 720 }
 721
 722 TNode TermDb::getEntailedTerm2(TNode n,
 723                                std::map<TNode, TNode>& subs,
 724                                bool subsRep,
 725                                bool hasSubs)
 726 {
 727   Trace("term-db-entail") << "get entailed term : " << n << std::endl;
 728   if (d_qstate.hasTerm(n))
 729   {
 730     Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
 731     return n;
 732   }else if( n.getKind()==BOUND_VARIABLE ){
 733     if( hasSubs ){
 734       std::map< TNode, TNode >::iterator it = subs.find( n );
 735       if( it!=subs.end() ){
 736         Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
 737         if( subsRep ){
 738           Assert(d_qstate.hasTerm(it->second));
 739           Assert(d_qstate.getRepresentative(it->second) == it->second);
 740           return it->second;
 741         }
 742         return getEntailedTerm2(it->second, subs, subsRep, hasSubs);
 743       }
 744     }
 745   }else if( n.getKind()==ITE ){
 746     for( unsigned i=0; i<2; i++ ){
 747       if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
 748       {
 749         return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs);
 750       }
 751     }
 752   }else{
 753     if( n.hasOperator() ){
 754       TNode f = getMatchOperator( n );
 755       if( !f.isNull() ){
 756         std::vector< TNode > args;
 757         for( unsigned i=0; i<n.getNumChildren(); i++ ){
 758           TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs);
 759           if( c.isNull() ){
 760             return TNode::null();
 761           }
 762           c = d_qstate.getRepresentative(c);
 763           Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
 764           args.push_back( c );
 765         }
 766         TNode nn = getCongruentTerm(f, args);
 767         Trace("term-db-entail") << "  got congruent term " << nn << " for " << n << std::endl;
 768         return nn;
 769       }
 770     }
 771   }
 772   return TNode::null();
 773 }
 774
 775 Node TermDb::evaluateTerm(TNode n,
 776                           bool useEntailmentTests,
 777                           bool reqHasTerm)
 778 {
 779   std::map< TNode, Node > visited;
 780   std::vector<Node> exp;
 781   return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
 782 }
 783
 784 Node TermDb::evaluateTerm(TNode n,
 785                           std::vector<Node>& exp,
 786                           bool useEntailmentTests,
 787                           bool reqHasTerm)
 788 {
 789   std::map<TNode, Node> visited;
 790   return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
 791 }
 792
 793 TNode TermDb::getEntailedTerm(TNode n,
 794                               std::map<TNode, TNode>& subs,
 795                               bool subsRep)
 796 {
 797   return getEntailedTerm2(n, subs, subsRep, true);
 798 }
 799
 800 TNode TermDb::getEntailedTerm(TNode n)
 801 {
 802   std::map< TNode, TNode > subs;
 803   return getEntailedTerm2(n, subs, false, false);
 804 }
 805
 806 bool TermDb::isEntailed2(
 807     TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol)
 808 {
 809   Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
 810   Assert(n.getType().isBoolean());
 811   if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
 812     TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs);
 813     if( !n1.isNull() ){
 814       TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs);
 815       if( !n2.isNull() ){
 816         if( n1==n2 ){
 817           return pol;
 818         }else{
 819           Assert(d_qstate.hasTerm(n1));
 820           Assert(d_qstate.hasTerm(n2));
 821           if( pol ){
 822             return d_qstate.areEqual(n1, n2);
 823           }else{
 824             return d_qstate.areDisequal(n1, n2);
 825           }
 826         }
 827       }
 828     }
 829   }else if( n.getKind()==NOT ){
 830     return isEntailed2(n[0], subs, subsRep, hasSubs, !pol);
 831   }else if( n.getKind()==OR || n.getKind()==AND ){
 832     bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
 833     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 834       if (isEntailed2(n[i], subs, subsRep, hasSubs, pol))
 835       {
 836         if( simPol ){
 837           return true;
 838         }
 839       }else{
 840         if( !simPol ){
 841           return false;
 842         }
 843       }
 844     }
 845     return !simPol;
 846   //Boolean equality here
 847   }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
 848     for( unsigned i=0; i<2; i++ ){
 849       if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
 850       {
 851         unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
 852         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
 853         return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol);
 854       }
 855     }
 856   }else if( n.getKind()==APPLY_UF ){
 857     TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs);
 858     if( !n1.isNull() ){
 859       Assert(d_qstate.hasTerm(n1));
 860       if( n1==d_true ){
 861         return pol;
 862       }else if( n1==d_false ){
 863         return !pol;
 864       }else{
 865         return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
 866       }
 867     }
 868   }else if( n.getKind()==FORALL && !pol ){
 869     return isEntailed2(n[1], subs, subsRep, hasSubs, pol);
 870   }
 871   return false;
 872 }
 873
 874 bool TermDb::isEntailed(TNode n, bool pol)
 875 {
 876   Assert(d_consistent_ee);
 877   std::map< TNode, TNode > subs;
 878   return isEntailed2(n, subs, false, false, pol);
 879 }
 880
 881 bool TermDb::isEntailed(TNode n,
 882                         std::map<TNode, TNode>& subs,
 883                         bool subsRep,
 884                         bool pol)
 885 {
 886   Assert(d_consistent_ee);
 887   return isEntailed2(n, subs, subsRep, true, pol);
 888 }
 889
 890 bool TermDb::isTermActive( Node n ) {
 891   return d_inactive_map.find( n )==d_inactive_map.end();
 892   //return !n.getAttribute(NoMatchAttribute());
 893 }
 894
 895 void TermDb::setTermInactive( Node n ) {
 896   d_inactive_map[n] = true;
 897   //Trace("term-db-debug2") << "set no match attribute" << std::endl;
 898   //NoMatchAttribute nma;
 899   //n.setAttribute(nma,true);
 900 }
 901
 902 bool TermDb::hasTermCurrent( Node n, bool useMode ) {
 903   if( !useMode ){
 904     return d_has_map.find( n )!=d_has_map.end();
 905   }
 906   //some assertions are not sent to EE
 907   if (options::termDbMode() == options::TermDbMode::ALL)
 908   {
 909     return true;
 910   }
 911   else if (options::termDbMode() == options::TermDbMode::RELEVANT)
 912   {
 913     return d_has_map.find( n )!=d_has_map.end();
 914   }
 915   Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode();
 916   return false;
 917 }
 918
 919 bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
 920 {
 921   if( options::lteRestrictInstClosure() ){
 922     //has to be both in inst closure and in ground assertions
 923     if( !isInstClosure( n ) ){
 924       Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
 925       return false;
 926     }
 927     // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
 928     if( !hasTermCurrent( n, false ) ){
 929       Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
 930       return false;
 931     }
 932   }
 933   if( options::instMaxLevel()!=-1 ){
 934     if( n.hasAttribute(InstLevelAttribute()) ){
 935       int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f );
 936       unsigned ml = fml>=0 ? fml : options::instMaxLevel();
 937
 938       if( n.getAttribute(InstLevelAttribute())>ml ){
 939         Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
 940         Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
 941         return false;
 942       }
 943     }else{
 944       if( options::instLevelInputOnly() ){
 945         Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
 946         return false;
 947       }
 948     }
 949   }
 950   // it cannot have instantiation constants, which originate from
 951   // counterexample-guided instantiation strategies.
 952   return !TermUtil::hasInstConstAttr(n);
 953 }
 954
 955 Node TermDb::getEligibleTermInEqc( TNode r ) {
 956   if( isTermEligibleForInstantiation( r, TNode::null() ) ){
 957     return r;
 958   }else{
 959     std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
 960     if( it==d_term_elig_eqc.end() ){
 961       Node h;
 962       eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
 963       eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
 964       while (!eqc_i.isFinished())
 965       {
 966         TNode n = (*eqc_i);
 967         ++eqc_i;
 968         if (isTermEligibleForInstantiation(n, TNode::null()))
 969         {
 970           h = n;
 971           break;
 972         }
 973       }
 974       d_term_elig_eqc[r] = h;
 975       return h;
 976     }else{
 977       return it->second;
 978     }
 979   }
 980 }
 981
 982 bool TermDb::isInstClosure( Node r ) {
 983   return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
 984 }
 985
 986 void TermDb::setHasTerm( Node n ) {
 987   Trace("term-db-debug2") << "hasTerm : " << n  << std::endl;
 988   if( d_has_map.find( n )==d_has_map.end() ){
 989     d_has_map[n] = true;
 990     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 991       setHasTerm( n[i] );
 992     }
 993   }
 994 }
 995
 996 void TermDb::presolve() {
 997   if( options::incrementalSolving() ){
 998     // reset the caches that are SAT context-independent but user
 999     // context-dependent
1000     d_ops.clear();
1001     d_op_map.clear();
1002     d_type_map.clear();
1003     d_processed.clear();
1004     d_iclosure_processed.clear();
1005   }
1006 }
1007
1008 bool TermDb::reset( Theory::Effort effort ){
1009   d_op_nonred_count.clear();
1010   d_arg_reps.clear();
1011   d_func_map_trie.clear();
1012   d_func_map_eqc_trie.clear();
1013   d_func_map_rel_dom.clear();
1014   d_consistent_ee = true;
1015
1016   eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
1017
1018   Assert(ee->consistent());
1019   // if higher-order, add equalities for the purification terms now
1020   if (options::ufHo())
1021   {
1022     Trace("quant-ho")
1023         << "TermDb::reset : assert higher-order purify equalities..."
1024         << std::endl;
1025     for (std::pair<const Node, Node>& pp : d_ho_purify_to_term)
1026     {
1027       if (ee->hasTerm(pp.second)
1028           && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first)))
1029       {
1030         Node eq;
1031         std::map<Node, Node>::iterator itpe = d_ho_purify_to_eq.find(pp.first);
1032         if (itpe == d_ho_purify_to_eq.end())
1033         {
1034           eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
1035           d_ho_purify_to_eq[pp.first] = eq;
1036         }
1037         else
1038         {
1039           eq = itpe->second;
1040         }
1041         Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
1042         ee->assertEquality(eq, true, eq);
1043         if (!ee->consistent())
1044         {
1045           // In some rare cases, purification functions (in the domain of
1046           // d_ho_purify_to_term) may escape the term database. For example,
1047           // matching algorithms may construct instantiations involving these
1048           // functions. As a result, asserting these equalities internally may
1049           // cause a conflict. In this case, we insist that the purification
1050           // equality is sent out as a lemma here.
1051           Trace("term-db-lemma")
1052               << "Purify equality lemma: " << eq << std::endl;
1053           d_quantEngine->addLemma(eq);
1054           d_qstate.notifyInConflict();
1055           d_consistent_ee = false;
1056           return false;
1057         }
1058       }
1059     }
1060   }
1061
1062   //compute has map
1063   if (options::termDbMode() == options::TermDbMode::RELEVANT
1064       || options::lteRestrictInstClosure())
1065   {
1066     d_has_map.clear();
1067     d_term_elig_eqc.clear();
1068     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1069     while( !eqcs_i.isFinished() ){
1070       TNode r = (*eqcs_i);
1071       bool addedFirst = false;
1072       Node first;
1073       //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
1074       eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
1075       while( !eqc_i.isFinished() ){
1076         TNode n = (*eqc_i);
1077         if( first.isNull() ){
1078           first = n;
1079         }else{
1080           if( !addedFirst ){
1081             addedFirst = true;
1082             setHasTerm( first );
1083           }
1084           setHasTerm( n );
1085         }
1086         ++eqc_i;
1087       }
1088       ++eqcs_i;
1089     }
1090     TheoryEngine* te = d_quantEngine->getTheoryEngine();
1091     const LogicInfo& logicInfo = te->getLogicInfo();
1092     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
1093     {
1094       if (!logicInfo.isTheoryEnabled(theoryId))
1095       {
1096         continue;
1097       }
1098       Theory* theory = te->theoryOf(theoryId);
1099       Assert(theory != nullptr);
1100       for (context::CDList<Assertion>::const_iterator
1101                it = theory->facts_begin(),
1102                it_end = theory->facts_end();
1103            it != it_end;
1104            ++it)
1105       {
1106         if ((*it).d_assertion.getKind() != INST_CLOSURE)
1107         {
1108           setHasTerm((*it).d_assertion);
1109         }
1110       }
1111     }
1112   }
1113   //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
1114   for (const Node& n : d_iclosure_processed)
1115   {
1116     if (!ee->hasTerm(n))
1117     {
1118       ee->addTerm(n);
1119     }
1120   }
1121
1122   if( options::ufHo() && options::hoMergeTermDb() ){
1123     Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl;
1124     // build operator representative map
1125     d_ho_op_rep.clear();
1126     d_ho_op_slaves.clear();
1127     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1128     while( !eqcs_i.isFinished() ){
1129       TNode r = (*eqcs_i);
1130       if( r.getType().isFunction() ){
1131         Trace("quant-ho") << "  process function eqc " << r << std::endl;
1132         Node first;
1133         eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
1134         while( !eqc_i.isFinished() ){
1135           TNode n = (*eqc_i);
1136           Node n_use;
1137           if (n.isVar())
1138           {
1139             n_use = n;
1140           }
1141           else
1142           {
1143             // use its purified variable, if it exists
1144             std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(n);
1145             if (itp != d_ho_fun_op_purify.end())
1146             {
1147               n_use = itp->second;
1148             }
1149           }
1150           Trace("quant-ho") << "  - process " << n_use << ", from " << n
1151                             << std::endl;
1152           if (!n_use.isNull() && d_op_map.find(n_use) != d_op_map.end())
1153           {
1154             if (first.isNull())
1155             {
1156               first = n_use;
1157               d_ho_op_rep[n_use] = n_use;
1158             }
1159             else
1160             {
1161               Trace("quant-ho") << "  have : " << n_use << " == " << first
1162                                 << ", type = " << n_use.getType() << std::endl;
1163               d_ho_op_rep[n_use] = first;
1164               d_ho_op_slaves[first].push_back(n_use);
1165             }
1166           }
1167           ++eqc_i;
1168         }
1169       }
1170       ++eqcs_i;
1171     }
1172     Trace("quant-ho") << "...finished compute equal functions." << std::endl;
1173   }
1174
1175 /*
1176   //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
1177   for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
1178     computeUfTerms( it->first );
1179     if( !d_consistent_ee ){
1180       return false;
1181     }
1182   }
1183 */
1184   return true;
1185 }
1186
1187 TNodeTrie* TermDb::getTermArgTrie(Node f)
1188 {
1189   if( options::ufHo() ){
1190     f = getOperatorRepresentative( f );
1191   }
1192   computeUfTerms( f );
1193   std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1194   if( itut!=d_func_map_trie.end() ){
1195     return &itut->second;
1196   }else{
1197     return NULL;
1198   }
1199 }
1200
1201 TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
1202 {
1203   if( options::ufHo() ){
1204     f = getOperatorRepresentative( f );
1205   }
1206   computeUfEqcTerms( f );
1207   std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
1208   if( itut==d_func_map_eqc_trie.end() ){
1209     return NULL;
1210   }else{
1211     if( eqc.isNull() ){
1212       return &itut->second;
1213     }else{
1214       std::map<TNode, TNodeTrie>::iterator itute =
1215           itut->second.d_data.find(eqc);
1216       if( itute!=itut->second.d_data.end() ){
1217         return &itute->second;
1218       }else{
1219         return NULL;
1220       }
1221     }
1222   }
1223 }
1224
1225 TNode TermDb::getCongruentTerm( Node f, Node n ) {
1226   if( options::ufHo() ){
1227     f = getOperatorRepresentative( f );
1228   }
1229   computeUfTerms( f );
1230   std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1231   if( itut!=d_func_map_trie.end() ){
1232     computeArgReps( n );
1233     return itut->second.existsTerm( d_arg_reps[n] );
1234   }else{
1235     return TNode::null();
1236   }
1237 }
1238
1239 TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
1240   if( options::ufHo() ){
1241     f = getOperatorRepresentative( f );
1242   }
1243   computeUfTerms( f );
1244   return d_func_map_trie[f].existsTerm( args );
1245 }
1246
1247 Node TermDb::getHoTypeMatchPredicate(TypeNode tn)
1248 {
1249   std::map<TypeNode, Node>::iterator ithp = d_ho_type_match_pred.find(tn);
1250   if (ithp != d_ho_type_match_pred.end())
1251   {
1252     return ithp->second;
1253   }
1254   NodeManager* nm = NodeManager::currentNM();
1255   TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
1256   Node k = nm->mkSkolem("U", ptn, "predicate to force higher-order types");
1257   d_ho_type_match_pred[tn] = k;
1258   return k;
1259 }
1260
1261 }/* CVC4::theory::quantifiers namespace */
1262 }/* CVC4::theory namespace */
1263 }/* CVC4 namespace */