Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_algorithm.cpp	Lines:	321	359	89.4 %
Date:	2021-05-21	Branches:	517	1018	50.8 %


/******************************************************************************
 * 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 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	679316	bool hasSubterm(TNode n, TNode t, bool strict)
27		{
28	679316	if (!strict && n == t)
29		{
30	7	return true;
31		}
32
33	1358618	std::unordered_set<TNode> visited;
34	1358618	std::vector<TNode> toProcess;
35
36	679309	toProcess.push_back(n);
37
38		// incrementally iterate and add to toProcess
39	2219098	for (unsigned i = 0; i < toProcess.size(); ++i)
40		{
41	3641698	TNode current = toProcess[i];
42	16980911	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
43		{
44	28886949	TNode child;
45		// try children then operator
46	16094653	if (j < j_end)
47		{
48	14554862	child = current[j];
49		}
50	1539791	else if (current.hasOperator())
51		{
52	886260	child = current.getOperator();
53		}
54		else
55		{
56	653531	break;
57		}
58	15441122	if (child == t)
59		{
60	562120	return true;
61		}
62	14879002	if (visited.find(child) != visited.end())
63		{
64	2086706	continue;
65		}
66		else
67		{
68	12792296	visited.insert(child);
69	12792296	toProcess.push_back(child);
70		}
71		}
72		}
73
74	117189	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	857703	bool hasSubtermKind(Kind k, Node n)
133		{
134	1715406	std::unordered_set<TNode> visited;
135	1715406	std::vector<TNode> visit;
136	1715406	TNode cur;
137	857703	visit.push_back(n);
138	6112652	do
139		{
140	6970355	cur = visit.back();
141	6970355	visit.pop_back();
142	6970355	if (visited.find(cur) == visited.end())
143		{
144	5843622	visited.insert(cur);
145	5843622	if (cur.getKind() == k)
146		{
147	124	return true;
148		}
149	11956249	for (const Node& cn : cur)
150		{
151	6112751	visit.push_back(cn);
152		}
153		}
154	6970231	} while (!visit.empty());
155	857579	return false;
156		}
157
158	2950	bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
159		Node n)
160		{
161	2950	if (ks.empty())
162		{
163		return false;
164		}
165	5900	std::unordered_set<TNode> visited;
166	5900	std::vector<TNode> visit;
167	5900	TNode cur;
168	2950	visit.push_back(n);
169	5196	do
170		{
171	8146	cur = visit.back();
172	8146	visit.pop_back();
173	8146	if (visited.find(cur) == visited.end())
174		{
175	7247	if (ks.find(cur.getKind()) != ks.end())
176		{
177	38	return true;
178		}
179	7209	visited.insert(cur);
180	7209	visit.insert(visit.end(), cur.begin(), cur.end());
181		}
182	8108	} while (!visit.empty());
183	2912	return false;
184		}
185
186	1588	bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
187		{
188	1588	if (t.empty())
189		{
190		return false;
191		}
192	1588	if (!strict && std::find(t.begin(), t.end(), n) != t.end())
193		{
194	4	return true;
195		}
196
197	3168	std::unordered_set<TNode> visited;
198	3168	std::vector<TNode> toProcess;
199
200	1584	toProcess.push_back(n);
201
202		// incrementally iterate and add to toProcess
203	13444	for (unsigned i = 0; i < toProcess.size(); ++i)
204		{
205	23993	TNode current = toProcess[i];
206	26037	for (unsigned j = 0, j_end = current.getNumChildren(); j <= j_end; ++j)
207		{
208	34300	TNode child;
209		// try children then operator
210	22200	if (j < j_end)
211		{
212	10340	child = current[j];
213		}
214	11860	else if (current.hasOperator())
215		{
216	3837	child = current.getOperator();
217		}
218		else
219		{
220	8023	break;
221		}
222	14177	if (std::find(t.begin(), t.end(), child) != t.end())
223		{
224	273	return true;
225		}
226	13904	if (visited.find(child) != visited.end())
227		{
228	1804	continue;
229		}
230		else
231		{
232	12100	visited.insert(child);
233	12100	toProcess.push_back(child);
234		}
235		}
236		}
237
238	1311	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	11657969	bool hasBoundVar(TNode n)
252		{
253	11657969	if (!n.getAttribute(HasBoundVarComputedAttr()))
254		{
255	2182541	bool hasBv = false;
256	2182541	if (n.getKind() == kind::BOUND_VARIABLE)
257		{
258	63451	hasBv = true;
259		}
260		else
261		{
262	6582948	for (auto i = n.begin(); i != n.end() && !hasBv; ++i)
263		{
264	4845067	if (hasBoundVar(*i))
265		{
266	381209	hasBv = true;
267	381209	break;
268		}
269		}
270		}
271	2182541	if (!hasBv && n.hasOperator())
272		{
273	1512606	hasBv = hasBoundVar(n.getOperator());
274		}
275	2182541	n.setAttribute(HasBoundVarAttr(), hasBv);
276	2182541	n.setAttribute(HasBoundVarComputedAttr(), true);
277	4365082	Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr())
278	2182541	<< std::endl;
279	2182541	return hasBv;
280		}
281	9475428	return n.getAttribute(HasBoundVarAttr());
282		}
283
284	1276341	bool hasFreeVar(TNode n)
285		{
286	2552682	std::unordered_set<Node> fvs;
287	2552682	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	3168	bool hasClosure(Node n)
301		{
302	3168	if (!n.getAttribute(HasClosureComputedAttr()))
303		{
304	1807	bool hasC = false;
305	1807	if (n.isClosure())
306		{
307	23	hasC = true;
308		}
309		else
310		{
311	3553	for (auto i = n.begin(); i != n.end() && !hasC; ++i)
312		{
313	1769	hasC = hasClosure(*i);
314		}
315		}
316	1807	if (!hasC && n.hasOperator())
317		{
318	855	hasC = hasClosure(n.getOperator());
319		}
320	1807	n.setAttribute(HasClosureAttr(), hasC);
321	1807	n.setAttribute(HasClosureComputedAttr(), true);
322	1807	return hasC;
323		}
324	1361	return n.getAttribute(HasClosureAttr());
325		}
326
327	1317656	bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
328		{
329	2635312	std::unordered_set<TNode> scope;
330	2635312	return getFreeVariablesScope(n, fvs, scope, computeFv);
331		}
332
333	1420896	bool getFreeVariablesScope(TNode n,
334		std::unordered_set<Node>& fvs,
335		std::unordered_set<TNode>& scope,
336		bool computeFv)
337		{
338	2841792	std::unordered_set<TNode> visited;
339	2841792	std::vector<TNode> visit;
340	2841792	TNode cur;
341	1420896	visit.push_back(n);
342	2941128	do
343		{
344	4362024	cur = visit.back();
345	4362024	visit.pop_back();
346		// can skip if it doesn't have a bound variable
347	4362024	if (!hasBoundVar(cur))
348		{
349	2537110	continue;
350		}
351	1824914	std::unordered_set<TNode>::iterator itv = visited.find(cur);
352	1824914	if (itv == visited.end())
353		{
354	1346817	visited.insert(cur);
355	1346817	if (cur.getKind() == kind::BOUND_VARIABLE)
356		{
357	294601	if (scope.find(cur) == scope.end())
358		{
359	49022	if (computeFv)
360		{
361	48693	fvs.insert(cur);
362		}
363		else
364		{
365	658	return true;
366		}
367		}
368		}
369	1052216	else if (cur.isClosure())
370		{
371		// add to scope
372	330031	for (const TNode& cn : cur[0])
373		{
374		// should not shadow
375	456528	Assert(scope.find(cn) == scope.end())
376	228264	<< "Shadowed variable " << cn << " in " << cur << "\n";
377	228264	scope.insert(cn);
378		}
379		// must make recursive call to use separate cache
380	101767	if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
381		{
382		return true;
383		}
384		// cleanup
385	330031	for (const TNode& cn : cur[0])
386		{
387	228264	scope.erase(cn);
388		}
389		}
390		else
391		{
392	950449	if (cur.hasOperator())
393		{
394	950449	visit.push_back(cur.getOperator());
395		}
396	950449	visit.insert(visit.end(), cur.begin(), cur.end());
397		}
398		}
399	4361695	} while (!visit.empty());
400
401	1420567	return !fvs.empty();
402		}
403
404	543	bool getVariables(TNode n, std::unordered_set<TNode>& vs)
405		{
406	1086	std::unordered_set<TNode> visited;
407	1086	std::vector<TNode> visit;
408	1086	TNode cur;
409	543	visit.push_back(n);
410	4992	do
411		{
412	5535	cur = visit.back();
413	5535	visit.pop_back();
414	5535	std::unordered_set<TNode>::iterator itv = visited.find(cur);
415	5535	if (itv == visited.end())
416		{
417	4409	if (cur.isVar())
418		{
419	1593	vs.insert(cur);
420		}
421		else
422		{
423	2816	visit.insert(visit.end(), cur.begin(), cur.end());
424		}
425	4409	visited.insert(cur);
426		}
427	5535	} while (!visit.empty());
428
429	1086	return !vs.empty();
430		}
431
432	3740	void getSymbols(TNode n, std::unordered_set<Node>& syms)
433		{
434	7480	std::unordered_set<TNode> visited;
435	3740	getSymbols(n, syms, visited);
436	3740	}
437
438	22160	void getSymbols(TNode n,
439		std::unordered_set<Node>& syms,
440		std::unordered_set<TNode>& visited)
441		{
442	44320	std::vector<TNode> visit;
443	44320	TNode cur;
444	22160	visit.push_back(n);
445	664776	do
446		{
447	686936	cur = visit.back();
448	686936	visit.pop_back();
449	686936	if (visited.find(cur) == visited.end())
450		{
451	336952	visited.insert(cur);
452	336952	if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE)
453		{
454	40668	syms.insert(cur);
455		}
456	336952	if (cur.hasOperator())
457		{
458	210359	visit.push_back(cur.getOperator());
459		}
460	336952	visit.insert(visit.end(), cur.begin(), cur.end());
461		}
462	686936	} while (!visit.empty());
463	22160	}
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	21741	Node substituteCaptureAvoiding(TNode n, Node src, Node dest)
541		{
542	21741	if (n == src)
543		{
544		return dest;
545		}
546	21741	if (src == dest)
547		{
548		return n;
549		}
550	43482	std::vector<Node> srcs;
551	43482	std::vector<Node> dests;
552	21741	srcs.push_back(src);
553	21741	dests.push_back(dest);
554	21741	return substituteCaptureAvoiding(n, srcs, dests);
555		}
556
557	22324	Node substituteCaptureAvoiding(TNode n,
558		std::vector<Node>& src,
559		std::vector<Node>& dest)
560		{
561	44648	std::unordered_map<TNode, Node> visited;
562	22324	std::unordered_map<TNode, Node>::iterator it;
563	44648	std::vector<TNode> visit;
564	44648	TNode curr;
565	22324	visit.push_back(n);
566	22324	Assert(src.size() == dest.size())
567		<< "Substitution domain and range must be equal size";
568	192205	do
569		{
570	214529	curr = visit.back();
571	214529	visit.pop_back();
572	214529	it = visited.find(curr);
573
574	214529	if (it == visited.end())
575		{
576	137193	auto itt = std::find(src.rbegin(), src.rend(), curr);
577	160618	if (itt != src.rend())
578		{
579	23425	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	23425	visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1];
584	95865	continue;
585		}
586	162783	if (curr.getNumChildren() == 0)
587		{
588	49015	visited[curr] = curr;
589	49015	continue;
590		}
591
592	64753	visited[curr] = Node::null();
593		// if binder, rename variables to avoid capture
594	64753	if (curr.isClosure())
595		{
596	779	NodeManager* nm = NodeManager::currentNM();
597		// have new vars -> renames subs in the end of current sub
598	1734	for (const Node& v : curr[0])
599		{
600	955	src.push_back(v);
601	955	dest.push_back(nm->mkBoundVar(v.getType()));
602		}
603		}
604		// save for post-visit
605	64753	visit.push_back(curr);
606		// visit children
607	64753	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
608		{
609		// push the operator
610	1411	visit.push_back(curr.getOperator());
611		}
612	190794	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
613		{
614	126041	visit.push_back(curr[i]);
615		}
616		}
617	77336	else if (it->second.isNull())
618		{
619		// build node
620	129506	NodeBuilder nb(curr.getKind());
621	64753	if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
622		{
623		// push the operator
624	1411	Assert(visited.find(curr.getOperator()) != visited.end());
625	1411	nb << visited[curr.getOperator()];
626		}
627		// collect substituted children
628	190794	for (unsigned i = 0, size = curr.getNumChildren(); i < size; ++i)
629		{
630	126041	Assert(visited.find(curr[i]) != visited.end());
631	126041	nb << visited[curr[i]];
632		}
633	64753	visited[curr] = nb;
634
635		// remove renaming
636	64753	if (curr.isClosure())
637		{
638		// remove beginning of sub which correspond to renaming of variables in
639		// this binder
640	779	unsigned nchildren = curr[0].getNumChildren();
641	779	src.resize(src.size() - nchildren);
642	779	dest.resize(dest.size() - nchildren);
643		}
644		}
645	214529	} while (!visit.empty());
646	22324	Assert(visited.find(n) != visited.end());
647	44648	return visited[n];
648		}
649
650	11905	void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
651		{
652	23810	std::vector<TypeNode> toProcess;
653	11905	toProcess.push_back(t);
654	116	do
655		{
656	24042	TypeNode curr = toProcess.back();
657	12021	toProcess.pop_back();
658		// if not already visited
659	12021	if (types.find(curr) == types.end())
660		{
661	11924	types.insert(curr);
662		// get component types from the children
663	12040	for (unsigned i = 0, nchild = curr.getNumChildren(); i < nchild; i++)
664		{
665	116	toProcess.push_back(curr[i]);
666		}
667		}
668	12021	} while (!toProcess.empty());
669	11905	}
670
671	1219	bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
672		{
673	2438	std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
674		std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
675	1219	it;
676	1219	std::unordered_map<Node, Node>::iterator subsIt;
677
678	2438	std::vector<std::pair<TNode, TNode>> stack;
679	1219	stack.emplace_back(x, y);
680	2438	std::pair<TNode, TNode> curr;
681
682	1593	while (!stack.empty())
683		{
684	1363	curr = stack.back();
685	1363	stack.pop_back();
686	1363	if (curr.first == curr.second)
687		{
688		// holds trivially
689	11	continue;
690		}
691	1352	it = visited.find(curr);
692	1352	if (it != visited.end())
693		{
694		// already processed
695	2	continue;
696		}
697	1350	visited.insert(curr);
698	1350	if (curr.first.getNumChildren() == 0)
699		{
700	130	if (!curr.first.getType().isComparableTo(curr.second.getType()))
701		{
702		// the two subterms have different types
703	2	return false;
704		}
705		// if the two subterms are not equal and the first one is a bound
706		// variable...
707	128	if (curr.first.getKind() == kind::BOUND_VARIABLE)
708		{
709		// and we have not seen this variable before...
710	98	subsIt = subs.find(curr.first);
711	98	if (subsIt == subs.cend())
712		{
713		// add the two subterms to `sub`
714	92	subs.emplace(curr.first, curr.second);
715		}
716		else
717		{
718		// if we saw this variable before, make sure that (now and before) it
719		// maps to the same subterm
720	6	if (curr.second != subsIt->second)
721		{
722	2	return false;
723		}
724		}
725		}
726		else
727		{
728		// the two subterms are not equal
729	30	return false;
730		}
731		}
732		else
733		{
734		// if the two subterms are not equal, make sure that their operators are
735		// equal
736		// we compare operators instead of kinds because different terms may have
737		// the same kind (both `(id x)` and `(square x)` have kind APPLY_UF)
738		// since many builtin operators like `PLUS` allow arbitrary number of
739		// arguments, we also need to check if the two subterms have the same
740		// number of children
741	2440	if (curr.first.getNumChildren() != curr.second.getNumChildren()
742	2440	\|\| curr.first.getOperator() != curr.second.getOperator())
743		{
744	1142	return false;
745		}
746		// recurse on children
747	236	for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
748		{
749	158	stack.emplace_back(curr.first[i], curr.second[i]);
750		}
751		}
752		}
753	43	return true;
754		}
755
756		} // namespace expr
757	27735	} // namespace cvc5