src/expr/node_algorithm.cpp

   1 /*********************                                                        */
   2 /*! \file node_algorithm.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Haniel Barbosa, Andres Noetzli
   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 Common algorithms on nodes
  13  **
  14  ** This file implements common algorithms applied to nodes, such as checking if
  15  ** a node contains a free or a bound variable.
  16  **/
  17
  18 #include "expr/node_algorithm.h"
  19
  20 #include "expr/attribute.h"
  21 #include "expr/dtype.h"
  22
  23 namespace CVC4 {
  24 namespace expr {
  25
  26 bool hasSubterm(TNode n, TNode t, bool strict)
  27 {
  28   if (!strict && n == t)
  29   {
  30     return true;
  31   }
  32
  33   std::unordered_set<TNode, TNodeHashFunction> visited;
  34   std::vector<TNode> toProcess;
  35
  36   toProcess.push_back(n);
  37
  38   // incrementally iterate and add to toProcess
  39   for (unsigned i = 0; i < toProcess.size(); ++i)
  40   {
  41     TNode current = toProcess[i];
  42     for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
  43     {
  44       TNode child;
  45       // try children then operator
  46       if (j < j_end)
  47       {
  48         child = current[j];
  49       }
  50       else if (current.hasOperator())
  51       {
  52         child = current.getOperator();
  53       }
  54       else
  55       {
  56         break;
  57       }
  58       if (child == t)
  59       {
  60         return true;
  61       }
  62       if (visited.find(child) != visited.end())
  63       {
  64         continue;
  65       }
  66       else
  67       {
  68         visited.insert(child);
  69         toProcess.push_back(child);
  70       }
  71     }
  72   }
  73
  74   return false;
  75 }
  76
  77 bool hasSubtermMulti(TNode n, TNode t)
  78 {
  79   std::unordered_map<TNode, bool, TNodeHashFunction> visited;
  80   std::unordered_map<TNode, bool, TNodeHashFunction> contains;
  81   std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
  82   std::vector<TNode> visit;
  83   TNode cur;
  84   visit.push_back(n);
  85   do
  86   {
  87     cur = visit.back();
  88     visit.pop_back();
  89     it = visited.find(cur);
  90
  91     if (it == visited.end())
  92     {
  93       if (cur == t)
  94       {
  95         visited[cur] = true;
  96         contains[cur] = true;
  97       }
  98       else
  99       {
 100         visited[cur] = false;
 101         visit.push_back(cur);
 102         for (const Node& cc : cur)
 103         {
 104           visit.push_back(cc);
 105         }
 106       }
 107     }
 108     else if (!it->second)
 109     {
 110       bool doesContain = false;
 111       for (const Node& cn : cur)
 112       {
 113         it = contains.find(cn);
 114         Assert(it != contains.end());
 115         if (it->second)
 116         {
 117           if (doesContain)
 118           {
 119             // two children have t, return true
 120             return true;
 121           }
 122           doesContain = true;
 123         }
 124       }
 125       contains[cur] = doesContain;
 126       visited[cur] = true;
 127     }
 128   } while (!visit.empty());
 129   return false;
 130 }
 131
 132 bool hasSubtermKind(Kind k, Node n)
 133 {
 134   std::unordered_set<TNode, TNodeHashFunction> visited;
 135   std::vector<TNode> visit;
 136   TNode cur;
 137   visit.push_back(n);
 138   do
 139   {
 140     cur = visit.back();
 141     visit.pop_back();
 142     if (visited.find(cur) == visited.end())
 143     {
 144       visited.insert(cur);
 145       if (cur.getKind() == k)
 146       {
 147         return true;
 148       }
 149       for (const Node& cn : cur)
 150       {
 151         visit.push_back(cn);
 152       }
 153     }
 154   } while (!visit.empty());
 155   return false;
 156 }
 157
 158 bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
 159 {
 160   if (t.empty())
 161   {
 162     return false;
 163   }
 164   if (!strict && std::find(t.begin(), t.end(), n) != t.end())
 165   {
 166     return true;
 167   }
 168
 169   std::unordered_set<TNode, TNodeHashFunction> visited;
 170   std::vector<TNode> toProcess;
 171
 172   toProcess.push_back(n);
 173
 174   // incrementally iterate and add to toProcess
 175   for (unsigned i = 0; i < toProcess.size(); ++i)
 176   {
 177     TNode current = toProcess[i];
 178     for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
 179     {
 180       TNode child;
 181       // try children then operator
 182       if (j < j_end)
 183       {
 184         child = current[j];
 185       }
 186       else if (current.hasOperator())
 187       {
 188         child = current.getOperator();
 189       }
 190       else
 191       {
 192         break;
 193       }
 194       if (std::find(t.begin(), t.end(), child) != t.end())
 195       {
 196         return true;
 197       }
 198       if (visited.find(child) != visited.end())
 199       {
 200         continue;
 201       }
 202       else
 203       {
 204         visited.insert(child);
 205         toProcess.push_back(child);
 206       }
 207     }
 208   }
 209
 210   return false;
 211 }
 212
 213 struct HasBoundVarTag
 214 {
 215 };
 216 struct HasBoundVarComputedTag
 217 {
 218 };
 219 /** Attribute true for expressions with bound variables in them */
 220 typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
 221 typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;
 222
 223 bool hasBoundVar(TNode n)
 224 {
 225   if (!n.getAttribute(HasBoundVarComputedAttr()))
 226   {
 227     bool hasBv = false;
 228     if (n.getKind() == kind::BOUND_VARIABLE)
 229     {
 230       hasBv = true;
 231     }
 232     else
 233     {
 234       for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
 235       {
 236         hasBv = hasBoundVar(*i);
 237       }
 238     }
 239     if (!hasBv && n.hasOperator())
 240     {
 241       hasBv = hasBoundVar(n.getOperator());
 242     }
 243     n.setAttribute(HasBoundVarAttr(), hasBv);
 244     n.setAttribute(HasBoundVarComputedAttr(), true);
 245     Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
 246                  << std::endl;
 247     return hasBv;
 248   }
 249   return n.getAttribute(HasBoundVarAttr());
 250 }
 251
 252 bool hasFreeVar(TNode n)
 253 {
 254   std::unordered_set<Node, NodeHashFunction> fvs;
 255   return getFreeVariables(n, fvs, false);
 256 }
 257
 258 struct HasClosureTag
 259 {
 260 };
 261 struct HasClosureComputedTag
 262 {
 263 };
 264 /** Attribute true for expressions with closures in them */
 265 typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
 266 typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
 267
 268 bool hasClosure(Node n)
 269 {
 270   if (!n.getAttribute(HasClosureComputedAttr()))
 271   {
 272     bool hasC = false;
 273     if (n.isClosure())
 274     {
 275       hasC = true;
 276     }
 277     else
 278     {
 279       for (auto i = n.begin(); i != n.end() && !hasC; ++i)
 280       {
 281         hasC = hasClosure(*i);
 282       }
 283     }
 284     if (!hasC && n.hasOperator())
 285     {
 286       hasC = hasClosure(n.getOperator());
 287     }
 288     n.setAttribute(HasClosureAttr(), hasC);
 289     n.setAttribute(HasClosureComputedAttr(), true);
 290     return hasC;
 291   }
 292   return n.getAttribute(HasClosureAttr());
 293 }
 294
 295 bool getFreeVariables(TNode n,
 296                       std::unordered_set<Node, NodeHashFunction>& fvs,
 297                       bool computeFv)
 298 {
 299   std::unordered_set<TNode, TNodeHashFunction> bound_var;
 300   std::unordered_map<TNode, bool, TNodeHashFunction> visited;
 301   std::vector<TNode> visit;
 302   TNode cur;
 303   visit.push_back(n);
 304   do
 305   {
 306     cur = visit.back();
 307     visit.pop_back();
 308     // can skip if it doesn't have a bound variable
 309     if (!hasBoundVar(cur))
 310     {
 311       continue;
 312     }
 313     Kind k = cur.getKind();
 314     bool isQuant = cur.isClosure();
 315     std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv =
 316         visited.find(cur);
 317     if (itv == visited.end())
 318     {
 319       if (k == kind::BOUND_VARIABLE)
 320       {
 321         if (bound_var.find(cur) == bound_var.end())
 322         {
 323           if (computeFv)
 324           {
 325             fvs.insert(cur);
 326           }
 327           else
 328           {
 329             return true;
 330           }
 331         }
 332       }
 333       else if (isQuant)
 334       {
 335         for (const TNode& cn : cur[0])
 336         {
 337           // should not shadow
 338           Assert(bound_var.find(cn) == bound_var.end());
 339           bound_var.insert(cn);
 340         }
 341         visit.push_back(cur);
 342       }
 343       // must visit quantifiers again to clean up below
 344       visited[cur] = !isQuant;
 345       if (cur.hasOperator())
 346       {
 347         visit.push_back(cur.getOperator());
 348       }
 349       for (const TNode& cn : cur)
 350       {
 351         visit.push_back(cn);
 352       }
 353     }
 354     else if (!itv->second)
 355     {
 356       Assert(isQuant);
 357       for (const TNode& cn : cur[0])
 358       {
 359         bound_var.erase(cn);
 360       }
 361       visited[cur] = true;
 362     }
 363   } while (!visit.empty());
 364
 365   return !fvs.empty();
 366 }
 367
 368 bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
 369 {
 370   std::unordered_set<TNode, TNodeHashFunction> visited;
 371   std::vector<TNode> visit;
 372   TNode cur;
 373   visit.push_back(n);
 374   do
 375   {
 376     cur = visit.back();
 377     visit.pop_back();
 378     std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
 379         visited.find(cur);
 380     if (itv == visited.end())
 381     {
 382       if (cur.isVar())
 383       {
 384         vs.insert(cur);
 385       }
 386       else
 387       {
 388         for (const TNode& cn : cur)
 389         {
 390           visit.push_back(cn);
 391         }
 392       }
 393       visited.insert(cur);
 394     }
 395   } while (!visit.empty());
 396
 397   return !vs.empty();
 398 }
 399
 400 void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)
 401 {
 402   std::unordered_set<TNode, TNodeHashFunction> visited;
 403   getSymbols(n, syms, visited);
 404 }
 405
 406 void getSymbols(TNode n,
 407                 std::unordered_set<Node, NodeHashFunction>& syms,
 408                 std::unordered_set<TNode, TNodeHashFunction>& visited)
 409 {
 410   std::vector<TNode> visit;
 411   TNode cur;
 412   visit.push_back(n);
 413   do
 414   {
 415     cur = visit.back();
 416     visit.pop_back();
 417     if (visited.find(cur) == visited.end())
 418     {
 419       visited.insert(cur);
 420       if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
 421       {
 422         syms.insert(cur);
 423       }
 424       if (cur.hasOperator())
 425       {
 426         visit.push_back(cur.getOperator());
 427       }
 428       for (TNode cn : cur)
 429       {
 430         visit.push_back(cn);
 431       }
 432     }
 433   } while (!visit.empty());
 434 }
 435
 436 void getOperatorsMap(
 437     TNode n,
 438     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops)
 439 {
 440   std::unordered_set<TNode, TNodeHashFunction> visited;
 441   getOperatorsMap(n, ops, visited);
 442 }
 443
 444 void getOperatorsMap(
 445     TNode n,
 446     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
 447     std::unordered_set<TNode, TNodeHashFunction>& visited)
 448 {
 449   // nodes that we still need to visit
 450   std::vector<TNode> visit;
 451   // current node
 452   TNode cur;
 453   visit.push_back(n);
 454   do
 455   {
 456     cur = visit.back();
 457     visit.pop_back();
 458     // if cur is in the cache, do nothing
 459     if (visited.find(cur) == visited.end())
 460     {
 461       // fetch the correct type
 462       TypeNode tn = cur.getType();
 463       // add the current operator to the result
 464       if (cur.hasOperator())
 465       {
 466         ops[tn].insert(NodeManager::currentNM()->operatorOf(cur.getKind()));
 467       }
 468       // add children to visit in the future
 469       for (TNode cn : cur)
 470       {
 471         visit.push_back(cn);
 472       }
 473     }
 474   } while (!visit.empty());
 475 }
 476
 477 Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
 478 {
 479   if (n == src)
 480   {
 481     return dest;
 482   }
 483   if (src == dest)
 484   {
 485     return n;
 486   }
 487   std::vector<Node> srcs;
 488   std::vector<Node> dests;
 489   srcs.push_back(src);
 490   dests.push_back(dest);
 491   return substituteCaptureAvoiding(n, srcs, dests);
 492 }
 493
 494 Node substituteCaptureAvoiding(TNode n,
 495                                std::vector<Node>& src,
 496                                std::vector<Node>& dest)
 497 {
 498   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
 499   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
 500   std::vector<TNode> visit;
 501   TNode curr;
 502   visit.push_back(n);
 503   Assert(src.size() == dest.size())
 504       << "Substitution domain and range must be equal size";
 505   do
 506   {
 507     curr = visit.back();
 508     visit.pop_back();
 509     it = visited.find(curr);
 510
 511     if (it == visited.end())
 512     {
 513       auto itt = std::find(src.rbegin(), src.rend(), curr);
 514       if (itt != src.rend())
 515       {
 516         Assert(
 517             (std::distance(src.begin(), itt.base()) - 1) >= 0
 518             && static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1)
 519                    < dest.size());
 520         Node n = dest[std::distance(src.begin(), itt.base()) - 1];
 521         visited[curr] = n;
 522         continue;
 523       }
 524       if (curr.getNumChildren() == 0)
 525       {
 526         visited[curr] = curr;
 527         continue;
 528       }
 529
 530       visited[curr] = Node::null();
 531       // if binder, rename variables to avoid capture
 532       if (curr.isClosure())
 533       {
 534         NodeManager* nm = NodeManager::currentNM();
 535         // have new vars -> renames subs in the end of current sub
 536         for (const Node& v : curr[0])
 537         {
 538           src.push_back(v);
 539           dest.push_back(nm->mkBoundVar(v.getType()));
 540         }
 541       }
 542       // save for post-visit
 543       visit.push_back(curr);
 544       // visit children
 545       if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
 546       {
 547         // push the operator
 548         visit.push_back(curr.getOperator());
 549       }
 550       for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
 551       {
 552         visit.push_back(curr[i]);
 553       }
 554     }
 555     else if (it->second.isNull())
 556     {
 557       // build node
 558       NodeBuilder<> nb(curr.getKind());
 559       if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
 560       {
 561         // push the operator
 562         Assert(visited.find(curr.getOperator()) != visited.end());
 563         nb << visited[curr.getOperator()];
 564       }
 565       // collect substituted children
 566       for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
 567       {
 568         Assert(visited.find(curr[i]) != visited.end());
 569         nb << visited[curr[i]];
 570       }
 571       Node n = nb;
 572       visited[curr] = n;
 573
 574       // remove renaming
 575       if (curr.isClosure())
 576       {
 577         // remove beginning of sub which correspond to renaming of variables in
 578         // this binder
 579         unsigned nchildren = curr[0].getNumChildren();
 580         src.resize(src.size() - nchildren);
 581         dest.resize(dest.size() - nchildren);
 582       }
 583     }
 584   } while (!visit.empty());
 585   Assert(visited.find(n) != visited.end());
 586   return visited[n];
 587 }
 588
 589 void getComponentTypes(
 590     TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types)
 591 {
 592   std::vector<TypeNode> toProcess;
 593   toProcess.push_back(t);
 594   do
 595   {
 596     TypeNode curr = toProcess.back();
 597     toProcess.pop_back();
 598     // if not already visited
 599     if (types.find(t) == types.end())
 600     {
 601       types.insert(t);
 602       // get component types from the children
 603       for (unsigned i = 0, nchild = t.getNumChildren(); i < nchild; i++)
 604       {
 605         toProcess.push_back(t[i]);
 606       }
 607     }
 608   } while (!toProcess.empty());
 609 }
 610
 611 }  // namespace expr
 612 }  // namespace CVC4