Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_algorithm.cpp	Lines:	321	378	84.9 %
Date:	2021-09-13	Branches:	517	1044	49.5 %


/******************************************************************************
 * 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)
{
  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	690607	bool hasSubterm(TNode n, TNode t, bool strict)
27		{
28	690607	if (!strict && n == t)
29		{
30	9	return true;
31		}
32
33	1381196	std::unordered_set<TNode> visited;
34	1381196	std::vector<TNode> toProcess;
35
36	690598	toProcess.push_back(n);
37
38		// incrementally iterate and add to toProcess
39	2194314	for (unsigned i = 0; i < toProcess.size(); ++i)
40		{
41	3568321	TNode current = toProcess[i];
42	16863504	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
43		{
44	28741359	TNode child;
45		// try children then operator
46	16007656	if (j < j_end)
47		{
48	14503938	child = current[j];
49		}
50	1503718	else if (current.hasOperator())
51		{
52	855850	child = current.getOperator();
53		}
54		else
55		{
56	647868	break;
57		}
58	15359788	if (child == t)
59		{
60	560889	return true;
61		}
62	14798899	if (visited.find(child) != visited.end())
63		{
64	2065196	continue;
65		}
66		else
67		{
68	12733703	visited.insert(child);
69	12733703	toProcess.push_back(child);
70		}
71		}
72		}
73
74	129709	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	1083469	bool hasSubtermKind(Kind k, Node n)
133		{
134	2166938	std::unordered_set<TNode> visited;
135	2166938	std::vector<TNode> visit;
136	2166938	TNode cur;
137	1083469	visit.push_back(n);
138	6817182	do
139		{
140	7900651	cur = visit.back();
141	7900651	visit.pop_back();
142	7900651	if (visited.find(cur) == visited.end())
143		{
144	6763141	visited.insert(cur);
145	6763141	if (cur.getKind() == k)
146		{
147	164	return true;
148		}
149	13580290	for (const Node& cn : cur)
150		{
151	6817313	visit.push_back(cn);
152		}
153		}
154	7900487	} while (!visit.empty());
155	1083305	return false;
156		}
157
158	10265	bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
159		Node n)
160		{
161	10265	if (ks.empty())
162		{
163		return false;
164		}
165	20530	std::unordered_set<TNode> visited;
166	20530	std::vector<TNode> visit;
167	20530	TNode cur;
168	10265	visit.push_back(n);
169	17379	do
170		{
171	27644	cur = visit.back();
172	27644	visit.pop_back();
173	27644	if (visited.find(cur) == visited.end())
174		{
175	25612	if (ks.find(cur.getKind()) != ks.end())
176		{
177	127	return true;
178		}
179	25485	visited.insert(cur);
180	25485	visit.insert(visit.end(), cur.begin(), cur.end());
181		}
182	27517	} while (!visit.empty());
183	10138	return false;
184		}
185
186	1562	bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
187		{
188	1562	if (t.empty())
189		{
190		return false;
191		}
192	1562	if (!strict && std::find(t.begin(), t.end(), n) != t.end())
193		{
194	4	return true;
195		}
196
197	3116	std::unordered_set<TNode> visited;
198	3116	std::vector<TNode> toProcess;
199
200	1558	toProcess.push_back(n);
201
202		// incrementally iterate and add to toProcess
203	13541	for (unsigned i = 0; i < toProcess.size(); ++i)
204		{
205	24233	TNode current = toProcess[i];
206	26265	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
207		{
208	34630	TNode child;
209		// try children then operator
210	22389	if (j < j_end)
211		{
212	10406	child = current[j];
213		}
214	11983	else if (current.hasOperator())
215		{
216	3876	child = current.getOperator();
217		}
218		else
219		{
220	8107	break;
221		}
222	14282	if (std::find(t.begin(), t.end(), child) != t.end())
223		{
224	267	return true;
225		}
226	14015	if (visited.find(child) != visited.end())
227		{
228	1774	continue;
229		}
230		else
231		{
232	12241	visited.insert(child);
233	12241	toProcess.push_back(child);
234		}
235		}
236		}
237
238	1291	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	13935460	bool hasBoundVar(TNode n)
252		{
253	13935460	if (!n.getAttribute(HasBoundVarComputedAttr()))
254		{
255	2694624	bool hasBv = false;
256	2694624	if (n.getKind() == kind::BOUND_VARIABLE)
257		{
258	63764	hasBv = true;
259		}
260		else
261		{
262	8247769	for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
263		{
264	6009332	if (hasBoundVar(*i))
265		{
266	392423	hasBv = true;
267	392423	break;
268		}
269		}
270		}
271	2694624	if (!hasBv && n.hasOperator())
272		{
273	1991888	hasBv = hasBoundVar(n.getOperator());
274		}
275	2694624	n.setAttribute(HasBoundVarAttr(), hasBv);
276	2694624	n.setAttribute(HasBoundVarComputedAttr(), true);
277	5389248	Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
278	2694624	<< std::endl;
279	2694624	return hasBv;
280		}
281	11240836	return n.getAttribute(HasBoundVarAttr());
282		}
283
284	466144	bool hasFreeVar(TNode n)
285		{
286	932288	std::unordered_set<Node> fvs;
287	932288	return getFreeVariables(n, fvs, false);
288		}
289
290		struct HasClosureTag
291		{
292		};
293		struct HasClosureComputedTag
294		{
295		};
296		/** Attribute true for expressions with closures in them */
297		typedef expr::Attribute<HasClosureTag, bool> HasClosureAttr;
298		typedef expr::Attribute<HasClosureComputedTag, bool> HasClosureComputedAttr;
299
300	2623	bool hasClosure(Node n)
301		{
302	2623	if (!n.getAttribute(HasClosureComputedAttr()))
303		{
304	1547	bool hasC = false;
305	1547	if (n.isClosure())
306		{
307	28	hasC = true;
308		}
309		else
310		{
311	2980	for (auto i = n.begin(); i != n.end() && !hasC; ++i)
312		{
313	1461	hasC = hasClosure(*i);
314		}
315		}
316	1547	if (!hasC && n.hasOperator())
317		{
318	704	hasC = hasClosure(n.getOperator());
319		}
320	1547	n.setAttribute(HasClosureAttr(), hasC);
321	1547	n.setAttribute(HasClosureComputedAttr(), true);
322	1547	return hasC;
323		}
324	1076	return n.getAttribute(HasClosureAttr());
325		}
326
327	1616919	bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
328		{
329	3233838	std::unordered_set<TNode> scope;
330	3233838	return getFreeVariablesScope(n, fvs, scope, computeFv);
331		}
332
333	1723052	bool getFreeVariablesScope(TNode n,
334		std::unordered_set<Node>& fvs,
335		std::unordered_set<TNode>& scope,
336		bool computeFv)
337		{
338	3446104	std::unordered_set<TNode> visited;
339	3446104	std::vector<TNode> visit;
340	3446104	TNode cur;
341	1723052	visit.push_back(n);
342	3331425	do
343		{
344	5054477	cur = visit.back();
345	5054477	visit.pop_back();
346		// can skip if it doesn't have a bound variable
347	5054477	if (!hasBoundVar(cur))
348		{
349	2976508	continue;
350		}
351	2077969	std::unordered_set<TNode>::iterator itv = visited.find(cur);
352	2077969	if (itv == visited.end())
353		{
354	1526260	visited.insert(cur);
355	1526260	if (cur.getKind() == kind::BOUND_VARIABLE)
356		{
357	351649	if (scope.find(cur) == scope.end())
358		{
359	81232	if (computeFv)
360		{
361	80895	fvs.insert(cur);
362		}
363		else
364		{
365	674	return true;
366		}
367		}
368		}
369	1174611	else if (cur.isClosure())
370		{
371		// add to scope
372	356420	for (const TNode& cn : cur[0])
373		{
374		// should not shadow
375	503510	Assert(scope.find(cn) == scope.end())
376	251755	<< "Shadowed variable " << cn << " in " << cur << "\n";
377	251755	scope.insert(cn);
378		}
379		// must make recursive call to use separate cache
380	104665	if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
381		{
382		return true;
383		}
384		// cleanup
385	356420	for (const TNode& cn : cur[0])
386		{
387	251755	scope.erase(cn);
388		}
389		}
390		else
391		{
392	1069946	if (cur.hasOperator())
393		{
394	1069946	visit.push_back(cur.getOperator());
395		}
396	1069946	visit.insert(visit.end(), cur.begin(), cur.end());
397		}
398		}
399	5054140	} while (!visit.empty());
400
401	1722715	return !fvs.empty();
402		}
403
404	804	bool getVariables(TNode n, std::unordered_set<TNode>& vs)
405		{
406	1608	std::unordered_set<TNode> visited;
407	1608	std::vector<TNode> visit;
408	1608	TNode cur;
409	804	visit.push_back(n);
410	6141	do
411		{
412	6945	cur = visit.back();
413	6945	visit.pop_back();
414	6945	std::unordered_set<TNode>::iterator itv = visited.find(cur);
415	6945	if (itv == visited.end())
416		{
417	5778	if (cur.isVar())
418		{
419	2321	vs.insert(cur);
420		}
421		else
422		{
423	3457	visit.insert(visit.end(), cur.begin(), cur.end());
424		}
425	5778	visited.insert(cur);
426		}
427	6945	} while (!visit.empty());
428
429	1608	return !vs.empty();
430		}
431
432	3843	void getSymbols(TNode n, std::unordered_set<Node>& syms)
433		{
434	7686	std::unordered_set<TNode> visited;
435	3843	getSymbols(n, syms, visited);
436	3843	}
437
438	29211	void getSymbols(TNode n,
439		std::unordered_set<Node>& syms,
440		std::unordered_set<TNode>& visited)
441		{
442	58422	std::vector<TNode> visit;
443	58422	TNode cur;
444	29211	visit.push_back(n);
445	869721	do
446		{
447	898932	cur = visit.back();
448	898932	visit.pop_back();
449	898932	if (visited.find(cur) == visited.end())
450		{
451	423708	visited.insert(cur);
452	423708	if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
453		{
454	47474	syms.insert(cur);
455		}
456	423708	if (cur.hasOperator())
457		{
458	274513	visit.push_back(cur.getOperator());
459		}
460	423708	visit.insert(visit.end(), cur.begin(), cur.end());
461		}
462	898932	} while (!visit.empty());
463	29211	}
464
465	123	void getKindSubterms(TNode n,
466		Kind k,
467		bool topLevel,
468		std::unordered_set<Node>& ts)
469		{
470	246	std::unordered_set<TNode> visited;
471	246	std::vector<TNode> visit;
472	246	TNode cur;
473	123	visit.push_back(n);
474	3525	do
475		{
476	3648	cur = visit.back();
477	3648	visit.pop_back();
478	3648	if (visited.find(cur) == visited.end())
479		{
480	2089	visited.insert(cur);
481	2089	if (cur.getKind() == k)
482		{
483	37	ts.insert(cur);
484	37	if (topLevel)
485		{
486		// only considering top-level applications
487	37	continue;
488		}
489		}
490	2052	if (cur.hasOperator())
491		{
492	1091	visit.push_back(cur.getOperator());
493		}
494	2052	visit.insert(visit.end(), cur.begin(), cur.end());
495		}
496	3648	} while (!visit.empty());
497	123	}
498
499	3	void getOperatorsMap(TNode n, std::map<TypeNode, std::unordered_set<Node>>& ops)
500		{
501	6	std::unordered_set<TNode> visited;
502	3	getOperatorsMap(n, ops, visited);
503	3	}
504
505	3	void getOperatorsMap(TNode n,
506		std::map<TypeNode, std::unordered_set<Node>>& ops,
507		std::unordered_set<TNode>& visited)
508		{
509		// nodes that we still need to visit
510	6	std::vector<TNode> visit;
511		// current node
512	6	TNode cur;
513	3	visit.push_back(n);
514	76	do
515		{
516	79	cur = visit.back();
517	79	visit.pop_back();
518		// if cur is in the cache, do nothing
519	79	if (visited.find(cur) == visited.end())
520		{
521		// fetch the correct type
522	158	TypeNode tn = cur.getType();
523		// add the current operator to the result
524	79	if (cur.hasOperator())
525		{
526	78	Node o;
527	39	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
528	4	o = cur.getOperator();
529		} else {
530	35	o = NodeManager::currentNM()->operatorOf(cur.getKind());
531		}
532	39	ops[tn].insert(o);
533		}
534		// add children to visit in the future
535	79	visit.insert(visit.end(), cur.begin(), cur.end());
536		}
537	79	} while (!visit.empty());
538	3	}
539
540	36029	Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
541		{
542	36029	if (n == src)
543		{
544		return dest;
545		}
546	36029	if (src == dest)
547		{
548		return n;
549		}
550	72058	std::vector<Node> srcs;
551	72058	std::vector<Node> dests;
552	36029	srcs.push_back(src);
553	36029	dests.push_back(dest);
554	36029	return substituteCaptureAvoiding(n, srcs, dests);
555		}
556
557	36323	Node substituteCaptureAvoiding(TNode n,
558		std::vector<Node>& src,
559		std::vector<Node>& dest)
560		{
561	72646	std::unordered_map<TNode, Node> visited;
562	36323	std::unordered_map<TNode, Node>::iterator it;
563	72646	std::vector<TNode> visit;
564	72646	TNode curr;
565	36323	visit.push_back(n);
566	36323	Assert(src.size() == dest.size())
567		<< "Substitution domain and range must be equal size";
568	324338	do
569		{
570	360661	curr = visit.back();
571	360661	visit.pop_back();
572	360661	it = visited.find(curr);
573
574	360661	if (it == visited.end())
575		{
576	231442	auto itt = std::find(src.rbegin(), src.rend(), curr);
577	267954	if (itt != src.rend())
578		{
579	36512	Assert(
580		(std::distance(src.begin(), itt.base()) - 1) >= 0
581		&& static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1)
582		< dest.size());
583	36512	visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1];
584	159549	continue;
585		}
586	281455	if (curr.getNumChildren() == 0)
587		{
588	86525	visited[curr] = curr;
589	86525	continue;
590		}
591
592	108405	visited[curr] = Node::null();
593		// if binder, rename variables to avoid capture
594	108405	if (curr.isClosure())
595		{
596	138	NodeManager* nm = NodeManager::currentNM();
597		// have new vars -> renames subs in the end of current sub
598	319	for (const Node& v : curr[0])
599		{
600	181	src.push_back(v);
601	181	dest.push_back(nm->mkBoundVar(v.getType()));
602		}
603		}
604		// save for post-visit
605	108405	visit.push_back(curr);
606		// visit children
607	108405	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
608		{
609		// push the operator
610	1350	visit.push_back(curr.getOperator());
611		}
612	322988	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
613		{
614	214583	visit.push_back(curr[i]);
615		}
616		}
617	129219	else if (it->second.isNull())
618		{
619		// build node
620	216810	NodeBuilder nb(curr.getKind());
621	108405	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
622		{
623		// push the operator
624	1350	Assert(visited.find(curr.getOperator()) != visited.end());
625	1350	nb << visited[curr.getOperator()];
626		}
627		// collect substituted children
628	322988	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
629		{
630	214583	Assert(visited.find(curr[i]) != visited.end());
631	214583	nb << visited[curr[i]];
632		}
633	108405	visited[curr] = nb;
634
635		// remove renaming
636	108405	if (curr.isClosure())
637		{
638		// remove beginning of sub which correspond to renaming of variables in
639		// this binder
640	138	unsigned nchildren = curr[0].getNumChildren();
641	138	src.resize(src.size() - nchildren);
642	138	dest.resize(dest.size() - nchildren);
643		}
644		}
645	360661	} while (!visit.empty());
646	36323	Assert(visited.find(n) != visited.end());
647	72646	return visited[n];
648		}
649
650		void getTypes(TNode n, std::unordered_set<TypeNode>& types)
651		{
652		std::unordered_set<TNode> visited;
653		getTypes(n, types, visited);
654		}
655
656		void getTypes(TNode n,
657		std::unordered_set<TypeNode>& types,
658		std::unordered_set<TNode>& visited)
659		{
660		std::unordered_set<TNode>::iterator it;
661		std::vector<TNode> visit;
662		TNode cur;
663		visit.push_back(n);
664		do
665		{
666		cur = visit.back();
667		visit.pop_back();
668		it = visited.find(cur);
669		if (it == visited.end())
670		{
671		visited.insert(cur);
672		types.insert(cur.getType());
673		visit.insert(visit.end(), cur.begin(), cur.end());
674		}
675		} while (!visit.empty());
676		}
677
678	12484	void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
679		{
680	24968	std::vector<TypeNode> toProcess;
681	12484	toProcess.push_back(t);
682	176	do
683		{
684	25320	TypeNode curr = toProcess.back();
685	12660	toProcess.pop_back();
686		// if not already visited
687	12660	if (types.find(curr) == types.end())
688		{
689	12515	types.insert(curr);
690		// get component types from the children
691	12691	for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
692		{
693	176	toProcess.push_back(curr[i]);
694		}
695		}
696	12660	} while (!toProcess.empty());
697	12484	}
698
699	1166	bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
700		{
701	2332	std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
702		std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
703	1166	it;
704	1166	std::unordered_map<Node, Node>::iterator subsIt;
705
706	2332	std::vector<std::pair<TNode, TNode>> stack;
707	1166	stack.emplace_back(x, y);
708	2332	std::pair<TNode, TNode> curr;
709
710	1554	while (!stack.empty())
711		{
712	1313	curr = stack.back();
713	1313	stack.pop_back();
714	1313	if (curr.first == curr.second)
715		{
716		// holds trivially
717	13	continue;
718		}
719	1300	it = visited.find(curr);
720	1300	if (it != visited.end())
721		{
722		// already processed
723	2	continue;
724		}
725	1298	visited.insert(curr);
726	1298	if (curr.first.getNumChildren() == 0)
727		{
728	135	if (!curr.first.getType().isComparableTo(curr.second.getType()))
729		{
730		// the two subterms have different types
731	2	return false;
732		}
733		// if the two subterms are not equal and the first one is a bound
734		// variable...
735	133	if (curr.first.getKind() == kind::BOUND_VARIABLE)
736		{
737		// and we have not seen this variable before...
738	100	subsIt = subs.find(curr.first);
739	100	if (subsIt == subs.cend())
740		{
741		// add the two subterms to `sub`
742	94	subs.emplace(curr.first, curr.second);
743		}
744		else
745		{
746		// if we saw this variable before, make sure that (now and before) it
747		// maps to the same subterm
748	6	if (curr.second != subsIt->second)
749		{
750	2	return false;
751		}
752		}
753		}
754		else
755		{
756		// the two subterms are not equal
757	33	return false;
758		}
759		}
760		else
761		{
762		// if the two subterms are not equal, make sure that their operators are
763		// equal
764		// we compare operators instead of kinds because different terms may have
765		// the same kind (both `(id x)` and `(square x)` have kind APPLY_UF)
766		// since many builtin operators like `PLUS` allow arbitrary number of
767		// arguments, we also need to check if the two subterms have the same
768		// number of children
769	2326	if (curr.first.getNumChildren() != curr.second.getNumChildren()
770	2326	\|\| curr.first.getOperator() != curr.second.getOperator())
771		{
772	1082	return false;
773		}
774		// recurse on children
775	243	for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
776		{
777	162	stack.emplace_back(curr.first[i], curr.second[i]);
778		}
779		}
780		}
781	47	return true;
782		}
783
784		} // namespace expr
785	29514	} // namespace cvc5