Head

GCC Code Coverage Report

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


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

#include "expr/node_algorithm.h"

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

namespace cvc5 {
namespace expr {

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

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

  toProcess.push_back(n);

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

  return false;
}

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

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

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

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

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

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

  toProcess.push_back(n);

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

  return false;
}

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

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

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

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

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

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

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

  return !fvs.empty();
}

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

  return !vs.empty();
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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