Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_algorithm.cpp	Lines:	338	380	88.9 %
Date:	2021-11-07	Branches:	535	1050	51.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 * Common algorithms on nodes.
 *
 * This file implements common algorithms applied to nodes, such as checking if
 * a node contains a free or a bound variable.
 */

#include "expr/node_algorithm.h"

#include "expr/attribute.h"
#include "expr/dtype.h"

namespace cvc5 {
namespace expr {

bool hasSubterm(TNode n, TNode t, bool strict)
{
  if (!strict && n == t)
  {
    return true;
  }

  std::unordered_set<TNode> visited;
  std::vector<TNode> toProcess;

  toProcess.push_back(n);

  // incrementally iterate and add to toProcess
  for (unsigned i = 0; i < toProcess.size(); ++i)
  {
    TNode current = toProcess[i];
    for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
    {
      TNode child;
      // try children then operator
      if (j < j_end)
      {
        child = current[j];
      }
      else if (current.hasOperator())
      {
        child = current.getOperator();
      }
      else
      {
        break;
      }
      if (child == t)
      {
        return true;
      }
      if (visited.find(child) != visited.end())
      {
        continue;
      }
      else
      {
        visited.insert(child);
        toProcess.push_back(child);
      }
    }
  }

  return false;
}

bool hasSubtermMulti(TNode n, TNode t)
{
  std::unordered_map<TNode, bool> visited;
  std::unordered_map<TNode, bool> contains;
  std::unordered_map<TNode, bool>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      if (cur == t)
      {
        visited[cur] = true;
        contains[cur] = true;
      }
      else
      {
        visited[cur] = false;
        visit.push_back(cur);
        for (const Node& cc : cur)
        {
          visit.push_back(cc);
        }
      }
    }
    else if (!it->second)
    {
      bool doesContain = false;
      for (const Node& cn : cur)
      {
        it = contains.find(cn);
        Assert(it != contains.end());
        if (it->second)
        {
          if (doesContain)
          {
            // two children have t, return true
            return true;
          }
          doesContain = true;
        }
      }
      contains[cur] = doesContain;
      visited[cur] = true;
    }
  } while (!visit.empty());
  return false;
}

bool hasSubtermKind(Kind k, Node n)
{
  std::unordered_set<TNode> visited;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (visited.find(cur) == visited.end())
    {
      visited.insert(cur);
      if (cur.getKind() == k)
      {
        return true;
      }
      for (const Node& cn : cur)
      {
        visit.push_back(cn);
      }
    }
  } while (!visit.empty());
  return false;
}

bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
                     Node n)
{
  if (ks.empty())
  {
    return false;
  }
  std::unordered_set<TNode> visited;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (visited.find(cur) == visited.end())
    {
      if (ks.find(cur.getKind()) != ks.end())
      {
        return true;
      }
      visited.insert(cur);
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
  return false;
}

bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
{
  if (t.empty())
  {
    return false;
  }
  if (!strict && std::find(t.begin(), t.end(), n) != t.end())
  {
    return true;
  }

  std::unordered_set<TNode> visited;
  std::vector<TNode> toProcess;

  toProcess.push_back(n);

  // incrementally iterate and add to toProcess
  for (unsigned i = 0; i < toProcess.size(); ++i)
  {
    TNode current = toProcess[i];
    for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
    {
      TNode child;
      // try children then operator
      if (j < j_end)
      {
        child = current[j];
      }
      else if (current.hasOperator())
      {
        child = current.getOperator();
      }
      else
      {
        break;
      }
      if (std::find(t.begin(), t.end(), child) != t.end())
      {
        return true;
      }
      if (visited.find(child) != visited.end())
      {
        continue;
      }
      else
      {
        visited.insert(child);
        toProcess.push_back(child);
      }
    }
  }

  return false;
}

struct HasBoundVarTag
{
};
struct HasBoundVarComputedTag
{
};
/** Attribute true for expressions with bound variables in them */
typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;

bool hasBoundVar(TNode n)
{
  if (!n.getAttribute(HasBoundVarComputedAttr()))
  {
    bool hasBv = false;
    if (n.getKind() == kind::BOUND_VARIABLE)
    {
      hasBv = true;
    }
    else
    {
      for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
      {
        if (hasBoundVar(*i))
        {
          hasBv = true;
          break;
        }
      }
    }
    if (!hasBv && n.hasOperator())
    {
      hasBv = hasBoundVar(n.getOperator());
    }
    n.setAttribute(HasBoundVarAttr(), hasBv);
    n.setAttribute(HasBoundVarComputedAttr(), true);
    Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
                 << std::endl;
    return hasBv;
  }
  return n.getAttribute(HasBoundVarAttr());
}

bool hasFreeVar(TNode n)
{
  // optimization for variables and constants
  if (n.getNumChildren() == 0)
  {
    return n.getKind() == kind::BOUND_VARIABLE;
  }
  std::unordered_set<Node> fvs;
  return getFreeVariables(n, fvs, false);
}

struct HasClosureTag
{
};
struct HasClosureComputedTag
{
};
/** Attribute true for expressions with closures in them */
typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;

bool hasClosure(Node n)
{
  if (!n.getAttribute(HasClosureComputedAttr()))
  {
    bool hasC = false;
    if (n.isClosure())
    {
      hasC = true;
    }
    else
    {
      for (auto i = n.begin(); i != n.end() && !hasC; ++i)
      {
        hasC = hasClosure(*i);
      }
    }
    if (!hasC && n.hasOperator())
    {
      hasC = hasClosure(n.getOperator());
    }
    n.setAttribute(HasClosureAttr(), hasC);
    n.setAttribute(HasClosureComputedAttr(), true);
    return hasC;
  }
  return n.getAttribute(HasClosureAttr());
}

bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
{
  std::unordered_set<TNode> scope;
  return getFreeVariablesScope(n, fvs, scope, computeFv);
}

bool getFreeVariablesScope(TNode n,
                           std::unordered_set<Node>& fvs,
                           std::unordered_set<TNode>& scope,
                           bool computeFv)
{
  std::unordered_set<TNode> visited;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    // can skip if it doesn't have a bound variable
    if (!hasBoundVar(cur))
    {
      continue;
    }
    std::unordered_set<TNode>::iterator itv = visited.find(cur);
    if (itv == visited.end())
    {
      visited.insert(cur);
      if (cur.getKind() == kind::BOUND_VARIABLE)
      {
        if (scope.find(cur) == scope.end())
        {
          if (computeFv)
          {
            fvs.insert(cur);
          }
          else
          {
            return true;
          }
        }
      }
      else if (cur.isClosure())
      {
        // add to scope
        for (const TNode& cn : cur[0])
        {
          // should not shadow
          Assert(scope.find(cn) == scope.end())
              << "Shadowed variable " << cn << " in " << cur << "\n";
          scope.insert(cn);
        }
        // must make recursive call to use separate cache
        if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
        {
          return true;
        }
        // cleanup
        for (const TNode& cn : cur[0])
        {
          scope.erase(cn);
        }
      }
      else
      {
        if (cur.hasOperator())
        {
          visit.push_back(cur.getOperator());
        }
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
  } while (!visit.empty());

  return !fvs.empty();
}

bool getVariables(TNode n, std::unordered_set<TNode>& vs)
{
  std::unordered_set<TNode> visited;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    std::unordered_set<TNode>::iterator itv = visited.find(cur);
    if (itv == visited.end())
    {
      if (cur.isVar())
      {
        vs.insert(cur);
      }
      else
      {
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
      visited.insert(cur);
    }
  } while (!visit.empty());

  return !vs.empty();
}

void getSymbols(TNode n, std::unordered_set<Node>& syms)
{
  std::unordered_set<TNode> visited;
  getSymbols(n, syms, visited);
}

void getSymbols(TNode n,
                std::unordered_set<Node>& syms,
                std::unordered_set<TNode>& visited)
{
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (visited.find(cur) == visited.end())
    {
      visited.insert(cur);
      if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
      {
        syms.insert(cur);
      }
      if (cur.hasOperator())
      {
        visit.push_back(cur.getOperator());
      }
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
}

void getKindSubterms(TNode n,
                     Kind k,
                     bool topLevel,
                     std::unordered_set<Node>& ts)
{
  std::unordered_set<TNode> visited;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (visited.find(cur) == visited.end())
    {
      visited.insert(cur);
      if (cur.getKind() == k)
      {
        ts.insert(cur);
        if (topLevel)
        {
          // only considering top-level applications
          continue;
        }
      }
      if (cur.hasOperator())
      {
        visit.push_back(cur.getOperator());
      }
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
}

void getOperatorsMap(TNode n, std::map<TypeNode, std::unordered_set<Node>>& ops)
{
  std::unordered_set<TNode> visited;
  getOperatorsMap(n, ops, visited);
}

void getOperatorsMap(TNode n,
                     std::map<TypeNode, std::unordered_set<Node>>& ops,
                     std::unordered_set<TNode>& visited)
{
  // nodes that we still need to visit
  std::vector<TNode> visit;
  // current node
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    // if cur is in the cache, do nothing
    if (visited.find(cur) == visited.end())
    {
      // fetch the correct type
      TypeNode tn = cur.getType();
      // add the current operator to the result
      if (cur.hasOperator())
      {
       Node o;
       if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
         o = cur.getOperator();
       } else {
         o = NodeManager::currentNM()->operatorOf(cur.getKind());
       }
        ops[tn].insert(o);
      }
      // add children to visit in the future
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
}

Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
{
  if (n == src)
  {
    return dest;
  }
  if (src == dest)
  {
    return n;
  }
  std::vector<Node> srcs;
  std::vector<Node> dests;
  srcs.push_back(src);
  dests.push_back(dest);
  return substituteCaptureAvoiding(n, srcs, dests);
}

Node substituteCaptureAvoiding(TNode n,
                               std::vector<Node>& src,
                               std::vector<Node>& dest)
{
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<TNode> visit;
  TNode curr;
  visit.push_back(n);
  Assert(src.size() == dest.size())
      << "Substitution domain and range must be equal size";
  do
  {
    curr = visit.back();
    visit.pop_back();
    it = visited.find(curr);

    if (it == visited.end())
    {
      auto itt = std::find(src.rbegin(), src.rend(), curr);
      if (itt != src.rend())
      {
        Assert(
            (std::distance(src.begin(), itt.base()) - 1) >= 0
            && static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1)
                   < dest.size());
        visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1];
        continue;
      }
      if (curr.getNumChildren() == 0)
      {
        visited[curr] = curr;
        continue;
      }

      visited[curr] = Node::null();
      // if binder, rename variables to avoid capture
      if (curr.isClosure())
      {
        NodeManager* nm = NodeManager::currentNM();
        // have new vars -> renames subs in the end of current sub
        for (const Node& v : curr[0])
        {
          src.push_back(v);
          dest.push_back(nm->mkBoundVar(v.getType()));
        }
      }
      // save for post-visit
      visit.push_back(curr);
      // visit children
      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        // push the operator
        visit.push_back(curr.getOperator());
      }
      for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
      {
        visit.push_back(curr[i]);
      }
    }
    else if (it->second.isNull())
    {
      // build node
      NodeBuilder nb(curr.getKind());
      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        // push the operator
        Assert(visited.find(curr.getOperator()) != visited.end());
        nb << visited[curr.getOperator()];
      }
      // collect substituted children
      for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
      {
        Assert(visited.find(curr[i]) != visited.end());
        nb << visited[curr[i]];
      }
      visited[curr] = nb;

      // remove renaming
      if (curr.isClosure())
      {
        // remove beginning of sub which correspond to renaming of variables in
        // this binder
        unsigned nchildren = curr[0].getNumChildren();
        src.resize(src.size() - nchildren);
        dest.resize(dest.size() - nchildren);
      }
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  return visited[n];
}

void getTypes(TNode n, std::unordered_set<TypeNode>& types)
{
  std::unordered_set<TNode> visited;
  getTypes(n, types, visited);
}

void getTypes(TNode n,
              std::unordered_set<TypeNode>& types,
              std::unordered_set<TNode>& visited)
{
  std::unordered_set<TNode>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      visited.insert(cur);
      types.insert(cur.getType());
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
}

void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
{
  std::vector<TypeNode> toProcess;
  toProcess.push_back(t);
  do
  {
    TypeNode curr = toProcess.back();
    toProcess.pop_back();
    // if not already visited
    if (types.find(curr) == types.end())
    {
      types.insert(curr);
      // get component types from the children
      for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
      {
        toProcess.push_back(curr[i]);
      }
    }
  } while (!toProcess.empty());
}

bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
{
  std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
  std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
      it;
  std::unordered_map<Node, Node>::iterator subsIt;

  std::vector<std::pair<TNode, TNode>> stack;
  stack.emplace_back(x, y);
  std::pair<TNode, TNode> curr;

  while (!stack.empty())
  {
    curr = stack.back();
    stack.pop_back();
    if (curr.first == curr.second)
    {
      // holds trivially
      continue;
    }
    it = visited.find(curr);
    if (it != visited.end())
    {
      // already processed
      continue;
    }
    visited.insert(curr);
    if (curr.first.getNumChildren() == 0)
    {
      if (!curr.first.getType().isComparableTo(curr.second.getType()))
      {
        // the two subterms have different types
        return false;
      }
      // if the two subterms are not equal and the first one is a bound
      // variable...
      if (curr.first.getKind() == kind::BOUND_VARIABLE)
      {
        // and we have not seen this variable before...
        subsIt = subs.find(curr.first);
        if (subsIt == subs.cend())
        {
          // add the two subterms to `sub`
          subs.emplace(curr.first, curr.second);
        }
        else
        {
          // if we saw this variable before, make sure that (now and before) it
          // maps to the same subterm
          if (curr.second != subsIt->second)
          {
            return false;
          }
        }
      }
      else
      {
        // the two subterms are not equal
        return false;
      }
    }
    else
    {
      // if the two subterms are not equal, make sure that their operators are
      // equal
      // we compare operators instead of kinds because different terms may have
      // the same kind (both `(id x)` and `(square x)` have kind APPLY_UF)
      // since many builtin operators like `PLUS` allow arbitrary number of
      // arguments, we also need to check if the two subterms have the same
      // number of children
      if (curr.first.getNumChildren() != curr.second.getNumChildren()
          || curr.first.getOperator() != curr.second.getOperator())
      {
        return false;
      }
      // recurse on children
      for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
      {
        stack.emplace_back(curr.first[i], curr.second[i]);
      }
    }
  }
  return true;
}

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Haniel Barbosa
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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.
11		* ****************************************************************************
12		* 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 cvc5 {
24		namespace expr {
25
26	368328	bool hasSubterm(TNode n, TNode t, bool strict)
27		{
28	368328	if (!strict && n == t)
29		{
30	14	return true;
31		}
32
33	736628	std::unordered_set<TNode> visited;
34	736628	std::vector<TNode> toProcess;
35
36	368314	toProcess.push_back(n);
37
38		// incrementally iterate and add to toProcess
39	1860965	for (unsigned i = 0; i < toProcess.size(); ++i)
40		{
41	3227654	TNode current = toProcess[i];
42	16034284	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
43		{
44	27466635	TNode child;
45		// try children then operator
46	15184763	if (j < j_end)
47		{
48	13692110	child = current[j];
49		}
50	1492653	else if (current.hasOperator())
51		{
52	849523	child = current.getOperator();
53		}
54		else
55		{
56	643130	break;
57		}
58	14541633	if (child == t)
59		{
60	242352	return true;
61		}
62	14299281	if (visited.find(child) != visited.end())
63		{
64	2017409	continue;
65		}
66		else
67		{
68	12281872	visited.insert(child);
69	12281872	toProcess.push_back(child);
70		}
71		}
72		}
73
74	125962	return false;
75		}
76
77		bool hasSubtermMulti(TNode n, TNode t)
78		{
79		std::unordered_map<TNode, bool> visited;
80		std::unordered_map<TNode, bool> contains;
81		std::unordered_map<TNode, bool>::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	1219168	bool hasSubtermKind(Kind k, Node n)
133		{
134	2438336	std::unordered_set<TNode> visited;
135	2438336	std::vector<TNode> visit;
136	2438336	TNode cur;
137	1219168	visit.push_back(n);
138	7486364	do
139		{
140	8705532	cur = visit.back();
141	8705532	visit.pop_back();
142	8705532	if (visited.find(cur) == visited.end())
143		{
144	7447998	visited.insert(cur);
145	7447998	if (cur.getKind() == k)
146		{
147	164	return true;
148		}
149	14934329	for (const Node& cn : cur)
150		{
151	7486495	visit.push_back(cn);
152		}
153		}
154	8705368	} while (!visit.empty());
155	1219004	return false;
156		}
157
158	11181	bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
159		Node n)
160		{
161	11181	if (ks.empty())
162		{
163		return false;
164		}
165	22362	std::unordered_set<TNode> visited;
166	22362	std::vector<TNode> visit;
167	22362	TNode cur;
168	11181	visit.push_back(n);
169	18792	do
170		{
171	29973	cur = visit.back();
172	29973	visit.pop_back();
173	29973	if (visited.find(cur) == visited.end())
174		{
175	27731	if (ks.find(cur.getKind()) != ks.end())
176		{
177	127	return true;
178		}
179	27604	visited.insert(cur);
180	27604	visit.insert(visit.end(), cur.begin(), cur.end());
181		}
182	29846	} while (!visit.empty());
183	11054	return false;
184		}
185
186	1551	bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
187		{
188	1551	if (t.empty())
189		{
190		return false;
191		}
192	1551	if (!strict && std::find(t.begin(), t.end(), n) != t.end())
193		{
194	4	return true;
195		}
196
197	3094	std::unordered_set<TNode> visited;
198	3094	std::vector<TNode> toProcess;
199
200	1547	toProcess.push_back(n);
201
202		// incrementally iterate and add to toProcess
203	13369	for (unsigned i = 0; i < toProcess.size(); ++i)
204		{
205	23911	TNode current = toProcess[i];
206	25962	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
207		{
208	34219	TNode child;
209		// try children then operator
210	22124	if (j < j_end)
211		{
212	10302	child = current[j];
213		}
214	11822	else if (current.hasOperator())
215		{
216	3838	child = current.getOperator();
217		}
218		else
219		{
220	7984	break;
221		}
222	14140	if (std::find(t.begin(), t.end(), child) != t.end())
223		{
224	267	return true;
225		}
226	13873	if (visited.find(child) != visited.end())
227		{
228	1778	continue;
229		}
230		else
231		{
232	12095	visited.insert(child);
233	12095	toProcess.push_back(child);
234		}
235		}
236		}
237
238	1280	return false;
239		}
240
241		struct HasBoundVarTag
242		{
243		};
244		struct HasBoundVarComputedTag
245		{
246		};
247		/** Attribute true for expressions with bound variables in them */
248		typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
249		typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;
250
251	15577216	bool hasBoundVar(TNode n)
252		{
253	15577216	if (!n.getAttribute(HasBoundVarComputedAttr()))
254		{
255	2975671	bool hasBv = false;
256	2975671	if (n.getKind() == kind::BOUND_VARIABLE)
257		{
258	68344	hasBv = true;
259		}
260		else
261		{
262	9054168	for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
263		{
264	6581210	if (hasBoundVar(*i))
265		{
266	434369	hasBv = true;
267	434369	break;
268		}
269		}
270		}
271	2975671	if (!hasBv && n.hasOperator())
272		{
273	2210386	hasBv = hasBoundVar(n.getOperator());
274		}
275	2975671	n.setAttribute(HasBoundVarAttr(), hasBv);
276	2975671	n.setAttribute(HasBoundVarComputedAttr(), true);
277	5951342	Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
278	2975671	<< std::endl;
279	2975671	return hasBv;
280		}
281	12601545	return n.getAttribute(HasBoundVarAttr());
282		}
283
284	596101	bool hasFreeVar(TNode n)
285		{
286		// optimization for variables and constants
287	596101	if (n.getNumChildren() == 0)
288		{
289	72564	return n.getKind() == kind::BOUND_VARIABLE;
290		}
291	1047074	std::unordered_set<Node> fvs;
292	523537	return getFreeVariables(n, fvs, false);
293		}
294
295		struct HasClosureTag
296		{
297		};
298		struct HasClosureComputedTag
299		{
300		};
301		/** Attribute true for expressions with closures in them */
302		typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
303		typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
304
305	2617	bool hasClosure(Node n)
306		{
307	2617	if (!n.getAttribute(HasClosureComputedAttr()))
308		{
309	1541	bool hasC = false;
310	1541	if (n.isClosure())
311		{
312	28	hasC = true;
313		}
314		else
315		{
316	2970	for (auto i = n.begin(); i != n.end() && !hasC; ++i)
317		{
318	1457	hasC = hasClosure(*i);
319		}
320		}
321	1541	if (!hasC && n.hasOperator())
322		{
323	702	hasC = hasClosure(n.getOperator());
324		}
325	1541	n.setAttribute(HasClosureAttr(), hasC);
326	1541	n.setAttribute(HasClosureComputedAttr(), true);
327	1541	return hasC;
328		}
329	1076	return n.getAttribute(HasClosureAttr());
330		}
331
332	1833220	bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
333		{
334	3666440	std::unordered_set<TNode> scope;
335	3666440	return getFreeVariablesScope(n, fvs, scope, computeFv);
336		}
337
338	1948440	bool getFreeVariablesScope(TNode n,
339		std::unordered_set<Node>& fvs,
340		std::unordered_set<TNode>& scope,
341		bool computeFv)
342		{
343	3896880	std::unordered_set<TNode> visited;
344	3896880	std::vector<TNode> visit;
345	3896880	TNode cur;
346	1948440	visit.push_back(n);
347	3803490	do
348		{
349	5751930	cur = visit.back();
350	5751930	visit.pop_back();
351		// can skip if it doesn't have a bound variable
352	5751930	if (!hasBoundVar(cur))
353		{
354	3370695	continue;
355		}
356	2381235	std::unordered_set<TNode>::iterator itv = visited.find(cur);
357	2381235	if (itv == visited.end())
358		{
359	1752195	visited.insert(cur);
360	1752195	if (cur.getKind() == kind::BOUND_VARIABLE)
361		{
362	408444	if (scope.find(cur) == scope.end())
363		{
364	110104	if (computeFv)
365		{
366	110092	fvs.insert(cur);
367		}
368		else
369		{
370	24	return true;
371		}
372		}
373		}
374	1343751	else if (cur.isClosure())
375		{
376		// add to scope
377	391637	for (const TNode& cn : cur[0])
378		{
379		// should not shadow
380	558310	Assert(scope.find(cn) == scope.end())
381	279155	<< "Shadowed variable " << cn << " in " << cur << "\n";
382	279155	scope.insert(cn);
383		}
384		// must make recursive call to use separate cache
385	112482	if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
386		{
387		return true;
388		}
389		// cleanup
390	391637	for (const TNode& cn : cur[0])
391		{
392	279155	scope.erase(cn);
393		}
394		}
395		else
396		{
397	1231269	if (cur.hasOperator())
398		{
399	1231269	visit.push_back(cur.getOperator());
400		}
401	1231269	visit.insert(visit.end(), cur.begin(), cur.end());
402		}
403		}
404	5751918	} while (!visit.empty());
405
406	1948428	return !fvs.empty();
407		}
408
409	812	bool getVariables(TNode n, std::unordered_set<TNode>& vs)
410		{
411	1624	std::unordered_set<TNode> visited;
412	1624	std::vector<TNode> visit;
413	1624	TNode cur;
414	812	visit.push_back(n);
415	6165	do
416		{
417	6977	cur = visit.back();
418	6977	visit.pop_back();
419	6977	std::unordered_set<TNode>::iterator itv = visited.find(cur);
420	6977	if (itv == visited.end())
421		{
422	5804	if (cur.isVar())
423		{
424	2321	vs.insert(cur);
425		}
426		else
427		{
428	3483	visit.insert(visit.end(), cur.begin(), cur.end());
429		}
430	5804	visited.insert(cur);
431		}
432	6977	} while (!visit.empty());
433
434	1624	return !vs.empty();
435		}
436
437	4976	void getSymbols(TNode n, std::unordered_set<Node>& syms)
438		{
439	9952	std::unordered_set<TNode> visited;
440	4976	getSymbols(n, syms, visited);
441	4976	}
442
443	37120	void getSymbols(TNode n,
444		std::unordered_set<Node>& syms,
445		std::unordered_set<TNode>& visited)
446		{
447	74240	std::vector<TNode> visit;
448	74240	TNode cur;
449	37120	visit.push_back(n);
450	945872	do
451		{
452	982992	cur = visit.back();
453	982992	visit.pop_back();
454	982992	if (visited.find(cur) == visited.end())
455		{
456	475230	visited.insert(cur);
457	475230	if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
458		{
459	55122	syms.insert(cur);
460		}
461	475230	if (cur.hasOperator())
462		{
463	298901	visit.push_back(cur.getOperator());
464		}
465	475230	visit.insert(visit.end(), cur.begin(), cur.end());
466		}
467	982992	} while (!visit.empty());
468	37120	}
469
470	125	void getKindSubterms(TNode n,
471		Kind k,
472		bool topLevel,
473		std::unordered_set<Node>& ts)
474		{
475	250	std::unordered_set<TNode> visited;
476	250	std::vector<TNode> visit;
477	250	TNode cur;
478	125	visit.push_back(n);
479	4416	do
480		{
481	4541	cur = visit.back();
482	4541	visit.pop_back();
483	4541	if (visited.find(cur) == visited.end())
484		{
485	2421	visited.insert(cur);
486	2421	if (cur.getKind() == k)
487		{
488	37	ts.insert(cur);
489	37	if (topLevel)
490		{
491		// only considering top-level applications
492	37	continue;
493		}
494		}
495	2384	if (cur.hasOperator())
496		{
497	1346	visit.push_back(cur.getOperator());
498		}
499	2384	visit.insert(visit.end(), cur.begin(), cur.end());
500		}
501	4541	} while (!visit.empty());
502	125	}
503
504	3	void getOperatorsMap(TNode n, std::map<TypeNode, std::unordered_set<Node>>& ops)
505		{
506	6	std::unordered_set<TNode> visited;
507	3	getOperatorsMap(n, ops, visited);
508	3	}
509
510	3	void getOperatorsMap(TNode n,
511		std::map<TypeNode, std::unordered_set<Node>>& ops,
512		std::unordered_set<TNode>& visited)
513		{
514		// nodes that we still need to visit
515	6	std::vector<TNode> visit;
516		// current node
517	6	TNode cur;
518	3	visit.push_back(n);
519	76	do
520		{
521	79	cur = visit.back();
522	79	visit.pop_back();
523		// if cur is in the cache, do nothing
524	79	if (visited.find(cur) == visited.end())
525		{
526		// fetch the correct type
527	158	TypeNode tn = cur.getType();
528		// add the current operator to the result
529	79	if (cur.hasOperator())
530		{
531	78	Node o;
532	39	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
533	4	o = cur.getOperator();
534		} else {
535	35	o = NodeManager::currentNM()->operatorOf(cur.getKind());
536		}
537	39	ops[tn].insert(o);
538		}
539		// add children to visit in the future
540	79	visit.insert(visit.end(), cur.begin(), cur.end());
541		}
542	79	} while (!visit.empty());
543	3	}
544
545	298	Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
546		{
547	298	if (n == src)
548		{
549		return dest;
550		}
551	298	if (src == dest)
552		{
553		return n;
554		}
555	596	std::vector<Node> srcs;
556	596	std::vector<Node> dests;
557	298	srcs.push_back(src);
558	298	dests.push_back(dest);
559	298	return substituteCaptureAvoiding(n, srcs, dests);
560		}
561
562	677	Node substituteCaptureAvoiding(TNode n,
563		std::vector<Node>& src,
564		std::vector<Node>& dest)
565		{
566	1354	std::unordered_map<TNode, Node> visited;
567	677	std::unordered_map<TNode, Node>::iterator it;
568	1354	std::vector<TNode> visit;
569	1354	TNode curr;
570	677	visit.push_back(n);
571	677	Assert(src.size() == dest.size())
572		<< "Substitution domain and range must be equal size";
573	8839	do
574		{
575	9516	curr = visit.back();
576	9516	visit.pop_back();
577	9516	it = visited.find(curr);
578
579	9516	if (it == visited.end())
580		{
581	5416	auto itt = std::find(src.rbegin(), src.rend(), curr);
582	6341	if (itt != src.rend())
583		{
584	925	Assert(
585		(std::distance(src.begin(), itt.base()) - 1) >= 0
586		&& static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1)
587		< dest.size());
588	925	visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1];
589	3631	continue;
590		}
591	6272	if (curr.getNumChildren() == 0)
592		{
593	1781	visited[curr] = curr;
594	1781	continue;
595		}
596
597	2710	visited[curr] = Node::null();
598		// if binder, rename variables to avoid capture
599	2710	if (curr.isClosure())
600		{
601	144	NodeManager* nm = NodeManager::currentNM();
602		// have new vars -> renames subs in the end of current sub
603	331	for (const Node& v : curr[0])
604		{
605	187	src.push_back(v);
606	187	dest.push_back(nm->mkBoundVar(v.getType()));
607		}
608		}
609		// save for post-visit
610	2710	visit.push_back(curr);
611		// visit children
612	2710	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
613		{
614		// push the operator
615	228	visit.push_back(curr.getOperator());
616		}
617	8611	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
618		{
619	5901	visit.push_back(curr[i]);
620		}
621		}
622	4100	else if (it->second.isNull())
623		{
624		// build node
625	5420	NodeBuilder nb(curr.getKind());
626	2710	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
627		{
628		// push the operator
629	228	Assert(visited.find(curr.getOperator()) != visited.end());
630	228	nb << visited[curr.getOperator()];
631		}
632		// collect substituted children
633	8611	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
634		{
635	5901	Assert(visited.find(curr[i]) != visited.end());
636	5901	nb << visited[curr[i]];
637		}
638	2710	visited[curr] = nb;
639
640		// remove renaming
641	2710	if (curr.isClosure())
642		{
643		// remove beginning of sub which correspond to renaming of variables in
644		// this binder
645	144	unsigned nchildren = curr[0].getNumChildren();
646	144	src.resize(src.size() - nchildren);
647	144	dest.resize(dest.size() - nchildren);
648		}
649		}
650	9516	} while (!visit.empty());
651	677	Assert(visited.find(n) != visited.end());
652	1354	return visited[n];
653		}
654
655		void getTypes(TNode n, std::unordered_set<TypeNode>& types)
656		{
657		std::unordered_set<TNode> visited;
658		getTypes(n, types, visited);
659		}
660
661	7	void getTypes(TNode n,
662		std::unordered_set<TypeNode>& types,
663		std::unordered_set<TNode>& visited)
664		{
665	7	std::unordered_set<TNode>::iterator it;
666	14	std::vector<TNode> visit;
667	14	TNode cur;
668	7	visit.push_back(n);
669	34	do
670		{
671	41	cur = visit.back();
672	41	visit.pop_back();
673	41	it = visited.find(cur);
674	41	if (it == visited.end())
675		{
676	27	visited.insert(cur);
677	27	types.insert(cur.getType());
678	27	visit.insert(visit.end(), cur.begin(), cur.end());
679		}
680	41	} while (!visit.empty());
681	7	}
682
683	16490	void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
684		{
685	32980	std::vector<TypeNode> toProcess;
686	16490	toProcess.push_back(t);
687	144	do
688		{
689	33268	TypeNode curr = toProcess.back();
690	16634	toProcess.pop_back();
691		// if not already visited
692	16634	if (types.find(curr) == types.end())
693		{
694	16514	types.insert(curr);
695		// get component types from the children
696	16658	for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
697		{
698	144	toProcess.push_back(curr[i]);
699		}
700		}
701	16634	} while (!toProcess.empty());
702	16490	}
703
704	1205	bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
705		{
706	2410	std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
707		std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
708	1205	it;
709	1205	std::unordered_map<Node, Node>::iterator subsIt;
710
711	2410	std::vector<std::pair<TNode, TNode>> stack;
712	1205	stack.emplace_back(x, y);
713	2410	std::pair<TNode, TNode> curr;
714
715	1629	while (!stack.empty())
716		{
717	1364	curr = stack.back();
718	1364	stack.pop_back();
719	1364	if (curr.first == curr.second)
720		{
721		// holds trivially
722	15	continue;
723		}
724	1349	it = visited.find(curr);
725	1349	if (it != visited.end())
726		{
727		// already processed
728	2	continue;
729		}
730	1347	visited.insert(curr);
731	1347	if (curr.first.getNumChildren() == 0)
732		{
733	147	if (!curr.first.getType().isComparableTo(curr.second.getType()))
734		{
735		// the two subterms have different types
736	2	return false;
737		}
738		// if the two subterms are not equal and the first one is a bound
739		// variable...
740	145	if (curr.first.getKind() == kind::BOUND_VARIABLE)
741		{
742		// and we have not seen this variable before...
743	108	subsIt = subs.find(curr.first);
744	108	if (subsIt == subs.cend())
745		{
746		// add the two subterms to `sub`
747	102	subs.emplace(curr.first, curr.second);
748		}
749		else
750		{
751		// if we saw this variable before, make sure that (now and before) it
752		// maps to the same subterm
753	6	if (curr.second != subsIt->second)
754		{
755	2	return false;
756		}
757		}
758		}
759		else
760		{
761		// the two subterms are not equal
762	37	return false;
763		}
764		}
765		else
766		{
767		// if the two subterms are not equal, make sure that their operators are
768		// equal
769		// we compare operators instead of kinds because different terms may have
770		// the same kind (both `(id x)` and `(square x)` have kind APPLY_UF)
771		// since many builtin operators like `PLUS` allow arbitrary number of
772		// arguments, we also need to check if the two subterms have the same
773		// number of children
774	2400	if (curr.first.getNumChildren() != curr.second.getNumChildren()
775	2400	\|\| curr.first.getOperator() != curr.second.getOperator())
776		{
777	1111	return false;
778		}
779		// recurse on children
780	263	for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
781		{
782	174	stack.emplace_back(curr.first[i], curr.second[i]);
783		}
784		}
785		}
786	53	return true;
787		}
788
789		} // namespace expr
790	31137	} // namespace cvc5