Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_algorithm.cpp	Lines:	321	378	84.9 %
Date:	2021-08-17	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	680205	bool hasSubterm(TNode n, TNode t, bool strict)
27		{
28	680205	if (!strict && n == t)
29		{
30	7	return true;
31		}
32
33	1360396	std::unordered_set<TNode> visited;
34	1360396	std::vector<TNode> toProcess;
35
36	680198	toProcess.push_back(n);
37
38		// incrementally iterate and add to toProcess
39	2099397	for (unsigned i = 0; i < toProcess.size(); ++i)
40		{
41	3398787	TNode current = toProcess[i];
42	16640202	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
43		{
44	28488067	TNode child;
45		// try children then operator
46	15824992	if (j < j_end)
47		{
48	14405791	child = current[j];
49		}
50	1419201	else if (current.hasOperator())
51		{
52	815212	child = current.getOperator();
53		}
54		else
55		{
56	603989	break;
57		}
58	15221003	if (child == t)
59		{
60	560389	return true;
61		}
62	14660614	if (visited.find(child) != visited.end())
63		{
64	1997539	continue;
65		}
66		else
67		{
68	12663075	visited.insert(child);
69	12663075	toProcess.push_back(child);
70		}
71		}
72		}
73
74	119809	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	1051721	bool hasSubtermKind(Kind k, Node n)
133		{
134	2103442	std::unordered_set<TNode> visited;
135	2103442	std::vector<TNode> visit;
136	2103442	TNode cur;
137	1051721	visit.push_back(n);
138	6591589	do
139		{
140	7643310	cur = visit.back();
141	7643310	visit.pop_back();
142	7643310	if (visited.find(cur) == visited.end())
143		{
144	6528434	visited.insert(cur);
145	6528434	if (cur.getKind() == k)
146		{
147	164	return true;
148		}
149	13119990	for (const Node& cn : cur)
150		{
151	6591720	visit.push_back(cn);
152		}
153		}
154	7643146	} while (!visit.empty());
155	1051557	return false;
156		}
157
158	10185	bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
159		Node n)
160		{
161	10185	if (ks.empty())
162		{
163		return false;
164		}
165	20370	std::unordered_set<TNode> visited;
166	20370	std::vector<TNode> visit;
167	20370	TNode cur;
168	10185	visit.push_back(n);
169	16819	do
170		{
171	27004	cur = visit.back();
172	27004	visit.pop_back();
173	27004	if (visited.find(cur) == visited.end())
174		{
175	25235	if (ks.find(cur.getKind()) != ks.end())
176		{
177	129	return true;
178		}
179	25106	visited.insert(cur);
180	25106	visit.insert(visit.end(), cur.begin(), cur.end());
181		}
182	26875	} while (!visit.empty());
183	10056	return false;
184		}
185
186	1553	bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
187		{
188	1553	if (t.empty())
189		{
190		return false;
191		}
192	1553	if (!strict && std::find(t.begin(), t.end(), n) != t.end())
193		{
194	4	return true;
195		}
196
197	3098	std::unordered_set<TNode> visited;
198	3098	std::vector<TNode> toProcess;
199
200	1549	toProcess.push_back(n);
201
202		// incrementally iterate and add to toProcess
203	13274	for (unsigned i = 0; i < toProcess.size(); ++i)
204		{
205	23721	TNode current = toProcess[i];
206	25786	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
207		{
208	33997	TNode child;
209		// try children then operator
210	21989	if (j < j_end)
211		{
212	10264	child = current[j];
213		}
214	11725	else if (current.hasOperator())
215		{
216	3797	child = current.getOperator();
217		}
218		else
219		{
220	7928	break;
221		}
222	14061	if (std::find(t.begin(), t.end(), child) != t.end())
223		{
224	271	return true;
225		}
226	13790	if (visited.find(child) != visited.end())
227		{
228	1782	continue;
229		}
230		else
231		{
232	12008	visited.insert(child);
233	12008	toProcess.push_back(child);
234		}
235		}
236		}
237
238	1278	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	13541727	bool hasBoundVar(TNode n)
252		{
253	13541727	if (!n.getAttribute(HasBoundVarComputedAttr()))
254		{
255	2641430	bool hasBv = false;
256	2641430	if (n.getKind() == kind::BOUND_VARIABLE)
257		{
258	63126	hasBv = true;
259		}
260		else
261		{
262	8080611	for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
263		{
264	5889713	if (hasBoundVar(*i))
265		{
266	387406	hasBv = true;
267	387406	break;
268		}
269		}
270		}
271	2641430	if (!hasBv && n.hasOperator())
272		{
273	1943379	hasBv = hasBoundVar(n.getOperator());
274		}
275	2641430	n.setAttribute(HasBoundVarAttr(), hasBv);
276	2641430	n.setAttribute(HasBoundVarComputedAttr(), true);
277	5282860	Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
278	2641430	<< std::endl;
279	2641430	return hasBv;
280		}
281	10900297	return n.getAttribute(HasBoundVarAttr());
282		}
283
284	1494456	bool hasFreeVar(TNode n)
285		{
286	2988912	std::unordered_set<Node> fvs;
287	2988912	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	2919	bool hasClosure(Node n)
301		{
302	2919	if (!n.getAttribute(HasClosureComputedAttr()))
303		{
304	1648	bool hasC = false;
305	1648	if (n.isClosure())
306		{
307	18	hasC = true;
308		}
309		else
310		{
311	3279	for (auto i = n.begin(); i != n.end() && !hasC; ++i)
312		{
313	1649	hasC = hasClosure(*i);
314		}
315		}
316	1648	if (!hasC && n.hasOperator())
317		{
318	795	hasC = hasClosure(n.getOperator());
319		}
320	1648	n.setAttribute(HasClosureAttr(), hasC);
321	1648	n.setAttribute(HasClosureComputedAttr(), true);
322	1648	return hasC;
323		}
324	1271	return n.getAttribute(HasClosureAttr());
325		}
326
327	1535066	bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
328		{
329	3070132	std::unordered_set<TNode> scope;
330	3070132	return getFreeVariablesScope(n, fvs, scope, computeFv);
331		}
332
333	1640295	bool getFreeVariablesScope(TNode n,
334		std::unordered_set<Node>& fvs,
335		std::unordered_set<TNode>& scope,
336		bool computeFv)
337		{
338	3280590	std::unordered_set<TNode> visited;
339	3280590	std::vector<TNode> visit;
340	3280590	TNode cur;
341	1640295	visit.push_back(n);
342	3184559	do
343		{
344	4824854	cur = visit.back();
345	4824854	visit.pop_back();
346		// can skip if it doesn't have a bound variable
347	4824854	if (!hasBoundVar(cur))
348		{
349	2845632	continue;
350		}
351	1979222	std::unordered_set<TNode>::iterator itv = visited.find(cur);
352	1979222	if (itv == visited.end())
353		{
354	1439997	visited.insert(cur);
355	1439997	if (cur.getKind() == kind::BOUND_VARIABLE)
356		{
357	315937	if (scope.find(cur) == scope.end())
358		{
359	49176	if (computeFv)
360		{
361	48843	fvs.insert(cur);
362		}
363		else
364		{
365	666	return true;
366		}
367		}
368		}
369	1124060	else if (cur.isClosure())
370		{
371		// add to scope
372	352498	for (const TNode& cn : cur[0])
373		{
374		// should not shadow
375	497552	Assert(scope.find(cn) == scope.end())
376	248776	<< "Shadowed variable " << cn << " in " << cur << "\n";
377	248776	scope.insert(cn);
378		}
379		// must make recursive call to use separate cache
380	103722	if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
381		{
382		return true;
383		}
384		// cleanup
385	352498	for (const TNode& cn : cur[0])
386		{
387	248776	scope.erase(cn);
388		}
389		}
390		else
391		{
392	1020338	if (cur.hasOperator())
393		{
394	1020338	visit.push_back(cur.getOperator());
395		}
396	1020338	visit.insert(visit.end(), cur.begin(), cur.end());
397		}
398		}
399	4824521	} while (!visit.empty());
400
401	1639962	return !fvs.empty();
402		}
403
404	780	bool getVariables(TNode n, std::unordered_set<TNode>& vs)
405		{
406	1560	std::unordered_set<TNode> visited;
407	1560	std::vector<TNode> visit;
408	1560	TNode cur;
409	780	visit.push_back(n);
410	6015	do
411		{
412	6795	cur = visit.back();
413	6795	visit.pop_back();
414	6795	std::unordered_set<TNode>::iterator itv = visited.find(cur);
415	6795	if (itv == visited.end())
416		{
417	5652	if (cur.isVar())
418		{
419	2285	vs.insert(cur);
420		}
421		else
422		{
423	3367	visit.insert(visit.end(), cur.begin(), cur.end());
424		}
425	5652	visited.insert(cur);
426		}
427	6795	} while (!visit.empty());
428
429	1560	return !vs.empty();
430		}
431
432	3840	void getSymbols(TNode n, std::unordered_set<Node>& syms)
433		{
434	7680	std::unordered_set<TNode> visited;
435	3840	getSymbols(n, syms, visited);
436	3840	}
437
438	29195	void getSymbols(TNode n,
439		std::unordered_set<Node>& syms,
440		std::unordered_set<TNode>& visited)
441		{
442	58390	std::vector<TNode> visit;
443	58390	TNode cur;
444	29195	visit.push_back(n);
445	868417	do
446		{
447	897612	cur = visit.back();
448	897612	visit.pop_back();
449	897612	if (visited.find(cur) == visited.end())
450		{
451	422954	visited.insert(cur);
452	422954	if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
453		{
454	47588	syms.insert(cur);
455		}
456	422954	if (cur.hasOperator())
457		{
458	274062	visit.push_back(cur.getOperator());
459		}
460	422954	visit.insert(visit.end(), cur.begin(), cur.end());
461		}
462	897612	} while (!visit.empty());
463	29195	}
464
465	131	void getKindSubterms(TNode n,
466		Kind k,
467		bool topLevel,
468		std::unordered_set<Node>& ts)
469		{
470	262	std::unordered_set<TNode> visited;
471	262	std::vector<TNode> visit;
472	262	TNode cur;
473	131	visit.push_back(n);
474	3578	do
475		{
476	3709	cur = visit.back();
477	3709	visit.pop_back();
478	3709	if (visited.find(cur) == visited.end())
479		{
480	2152	visited.insert(cur);
481	2152	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	2115	if (cur.hasOperator())
491		{
492	1106	visit.push_back(cur.getOperator());
493		}
494	2115	visit.insert(visit.end(), cur.begin(), cur.end());
495		}
496	3709	} while (!visit.empty());
497	131	}
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	32983	Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
541		{
542	32983	if (n == src)
543		{
544		return dest;
545		}
546	32983	if (src == dest)
547		{
548		return n;
549		}
550	65966	std::vector<Node> srcs;
551	65966	std::vector<Node> dests;
552	32983	srcs.push_back(src);
553	32983	dests.push_back(dest);
554	32983	return substituteCaptureAvoiding(n, srcs, dests);
555		}
556
557	33287	Node substituteCaptureAvoiding(TNode n,
558		std::vector<Node>& src,
559		std::vector<Node>& dest)
560		{
561	66574	std::unordered_map<TNode, Node> visited;
562	33287	std::unordered_map<TNode, Node>::iterator it;
563	66574	std::vector<TNode> visit;
564	66574	TNode curr;
565	33287	visit.push_back(n);
566	33287	Assert(src.size() == dest.size())
567		<< "Substitution domain and range must be equal size";
568	293535	do
569		{
570	326822	curr = visit.back();
571	326822	visit.pop_back();
572	326822	it = visited.find(curr);
573
574	326822	if (it == visited.end())
575		{
576	210479	auto itt = std::find(src.rbegin(), src.rend(), curr);
577	243951	if (itt != src.rend())
578		{
579	33472	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	33472	visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1];
584	145831	continue;
585		}
586	255894	if (curr.getNumChildren() == 0)
587		{
588	78887	visited[curr] = curr;
589	78887	continue;
590		}
591
592	98120	visited[curr] = Node::null();
593		// if binder, rename variables to avoid capture
594	98120	if (curr.isClosure())
595		{
596	139	NodeManager* nm = NodeManager::currentNM();
597		// have new vars -> renames subs in the end of current sub
598	321	for (const Node& v : curr[0])
599		{
600	182	src.push_back(v);
601	182	dest.push_back(nm->mkBoundVar(v.getType()));
602		}
603		}
604		// save for post-visit
605	98120	visit.push_back(curr);
606		// visit children
607	98120	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
608		{
609		// push the operator
610	1368	visit.push_back(curr.getOperator());
611		}
612	292167	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
613		{
614	194047	visit.push_back(curr[i]);
615		}
616		}
617	116343	else if (it->second.isNull())
618		{
619		// build node
620	196240	NodeBuilder nb(curr.getKind());
621	98120	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
622		{
623		// push the operator
624	1368	Assert(visited.find(curr.getOperator()) != visited.end());
625	1368	nb << visited[curr.getOperator()];
626		}
627		// collect substituted children
628	292167	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
629		{
630	194047	Assert(visited.find(curr[i]) != visited.end());
631	194047	nb << visited[curr[i]];
632		}
633	98120	visited[curr] = nb;
634
635		// remove renaming
636	98120	if (curr.isClosure())
637		{
638		// remove beginning of sub which correspond to renaming of variables in
639		// this binder
640	139	unsigned nchildren = curr[0].getNumChildren();
641	139	src.resize(src.size() - nchildren);
642	139	dest.resize(dest.size() - nchildren);
643		}
644		}
645	326822	} while (!visit.empty());
646	33287	Assert(visited.find(n) != visited.end());
647	66574	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	12077	void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
679		{
680	24154	std::vector<TypeNode> toProcess;
681	12077	toProcess.push_back(t);
682	176	do
683		{
684	24506	TypeNode curr = toProcess.back();
685	12253	toProcess.pop_back();
686		// if not already visited
687	12253	if (types.find(curr) == types.end())
688		{
689	12108	types.insert(curr);
690		// get component types from the children
691	12284	for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
692		{
693	176	toProcess.push_back(curr[i]);
694		}
695		}
696	12253	} while (!toProcess.empty());
697	12077	}
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	29337	} // namespace cvc5