Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/skolem_manager.cpp	Lines:	162	172	94.2 %
Date:	2021-09-16	Branches:	320	782	40.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of skolem manager class.
 */

#include "expr/skolem_manager.h"

#include <sstream>

#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
#include "expr/node_algorithm.h"

using namespace cvc5::kind;

namespace cvc5 {

// Attributes are global maps from Nodes to data. Thus, note that these could
// be implemented as internal maps in SkolemManager.
struct WitnessFormAttributeId
{
};
typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;

struct SkolemFormAttributeId
{
};
typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;

struct OriginalFormAttributeId
{
};
typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;

const char* toString(SkolemFunId id)
{
  switch (id)
  {
    case SkolemFunId::DIV_BY_ZERO: return "DIV_BY_ZERO";
    case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
    case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
    case SkolemFunId::SQRT: return "SQRT";
    case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
    case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
    case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
    case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT";
    case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
    default: return "?";
  }
}

std::ostream& operator<<(std::ostream& out, SkolemFunId id)
{
  out << toString(id);
  return out;
}

Node SkolemManager::mkSkolem(Node v,
                             Node pred,
                             const std::string& prefix,
                             const std::string& comment,
                             int flags,
                             ProofGenerator* pg)
{
  // We do not currently insist that pred does not contain witness terms
  Assert(v.getKind() == BOUND_VARIABLE);
  // make the witness term
  NodeManager* nm = NodeManager::currentNM();
  Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
  // Make the witness term, where notice that pred may contain skolems. We do
  // not recursively convert pred to witness form, since witness terms should
  // be treated as opaque. Moreover, the use of witness forms leads to
  // variable shadowing issues in e.g. skolemization.
  Node w = nm->mkNode(WITNESS, bvl, pred);
  // store the mapping to proof generator if it exists
  if (pg != nullptr)
  {
    // We cache based on the existential of the original predicate
    Node q = nm->mkNode(EXISTS, bvl, pred);
    // Notice this may overwrite an existing proof generator. This does not
    // matter since either should be able to prove q.
    d_gens[q] = pg;
  }
  Node k = mkSkolemInternal(w, prefix, comment, flags);
  // set witness form attribute for k
  WitnessFormAttribute wfa;
  k.setAttribute(wfa, w);
  Trace("sk-manager-skolem")
      << "skolem: " << k << " witness " << w << std::endl;
  return k;
}

Node SkolemManager::mkSkolemize(Node q,
                                std::vector<Node>& skolems,
                                const std::string& prefix,
                                const std::string& comment,
                                int flags,
                                ProofGenerator* pg)
{
  Trace("sk-manager-debug") << "mkSkolemize " << q << std::endl;
  Assert(q.getKind() == EXISTS);
  Node currQ = q;
  for (const Node& av : q[0])
  {
    Assert(currQ.getKind() == EXISTS && av == currQ[0][0]);
    // currQ is updated to the result of skolemizing its first variable in
    // the method below.
    Node sk = skolemize(currQ, currQ, prefix, comment, flags);
    Trace("sk-manager-debug")
        << "made skolem " << sk << " for " << av << std::endl;
    skolems.push_back(sk);
  }
  if (pg != nullptr)
  {
    // Same as above, this may overwrite an existing proof generator
    d_gens[q] = pg;
  }
  Trace("sk-manager-debug") << "...mkSkolemize returns " << currQ << std::endl;
  return currQ;
}

Node SkolemManager::skolemize(Node q,
                              Node& qskolem,
                              const std::string& prefix,
                              const std::string& comment,
                              int flags)
{
  Assert(q.getKind() == EXISTS);
  Node v;
  std::vector<Node> ovars;
  Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
  NodeManager* nm = NodeManager::currentNM();
  for (const Node& av : q[0])
  {
    if (v.isNull())
    {
      v = av;
      continue;
    }
    ovars.push_back(av);
  }
  Assert(!v.isNull());
  // make the predicate with one variable stripped off
  Node pred = q[1];
  Trace("sk-manager-debug") << "make exists predicate" << std::endl;
  if (!ovars.empty())
  {
    // keeps the same variables
    Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
    // update the predicate
    pred = nm->mkNode(EXISTS, bvl, pred);
  }
  Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
  // don't use a proof generator, since this may be an intermediate, partially
  // skolemized formula.
  Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr);
  Assert(k.getType() == v.getType());
  TNode tv = v;
  TNode tk = k;
  Trace("sk-manager-debug")
      << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
  // the quantified formula with one step of skolemization
  qskolem = pred.substitute(tv, tk);
  Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
  return k;
}

Node SkolemManager::mkPurifySkolem(Node t,
                                   const std::string& prefix,
                                   const std::string& comment,
                                   int flags)
{
  Node to = getOriginalForm(t);
  // We do not currently insist that to does not contain witness terms

  Node k = mkSkolemInternal(to, prefix, comment, flags);
  // set original form attribute for k
  OriginalFormAttribute ofa;
  k.setAttribute(ofa, to);

  Trace("sk-manager-skolem")
      << "skolem: " << k << " purify " << to << std::endl;
  return k;
}

Node SkolemManager::mkSkolemFunction(SkolemFunId id,
                                     TypeNode tn,
                                     Node cacheVal,
                                     int flags)
{
  std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal);
  std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it =
      d_skolemFuns.find(key);
  if (it == d_skolemFuns.end())
  {
    NodeManager* nm = NodeManager::currentNM();
    std::stringstream ss;
    ss << "SKOLEM_FUN_" << id;
    Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags);
    d_skolemFuns[key] = k;
    d_skolemFunMap[k] = key;
    return k;
  }
  return it->second;
}

Node SkolemManager::mkSkolemFunction(SkolemFunId id,
                                     TypeNode tn,
                                     const std::vector<Node>& cacheVals,
                                     int flags)
{
  Assert(cacheVals.size() > 1);
  Node cacheVal = NodeManager::currentNM()->mkNode(SEXPR, cacheVals);
  return mkSkolemFunction(id, tn, cacheVal, flags);
}

bool SkolemManager::isSkolemFunction(Node k,
                                     SkolemFunId& id,
                                     Node& cacheVal) const
{
  std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>>::const_iterator it =
      d_skolemFunMap.find(k);
  if (it == d_skolemFunMap.end())
  {
    return false;
  }
  id = std::get<0>(it->second);
  cacheVal = std::get<2>(it->second);
  return true;
}

Node SkolemManager::mkDummySkolem(const std::string& prefix,
                                  const TypeNode& type,
                                  const std::string& comment,
                                  int flags)
{
  return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
}

ProofGenerator* SkolemManager::getProofGenerator(Node t) const
{
  std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
  if (it != d_gens.end())
  {
    return it->second;
  }
  return nullptr;
}

Node SkolemManager::getWitnessForm(Node k)
{
  Assert(k.getKind() == SKOLEM);
  // simply look up the witness form for k via an attribute
  WitnessFormAttribute wfa;
  return k.getAttribute(wfa);
}

Node SkolemManager::getOriginalForm(Node n)
{
  if (n.isNull())
  {
    return n;
  }
  Trace("sk-manager-debug")
      << "SkolemManager::getOriginalForm " << n << std::endl;
  OriginalFormAttribute ofa;
  NodeManager* nm = NodeManager::currentNM();
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::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.hasAttribute(ofa))
      {
        visited[cur] = cur.getAttribute(ofa);
      }
      else
      {
        visited[cur] = Node::null();
        visit.push_back(cur);
        if (cur.getMetaKind() == metakind::PARAMETERIZED)
        {
          visit.push_back(cur.getOperator());
        }
        for (const Node& cn : cur)
        {
          visit.push_back(cn);
        }
      }
    }
    else if (it->second.isNull())
    {
      Node ret = cur;
      bool childChanged = false;
      std::vector<Node> children;
      if (cur.getMetaKind() == metakind::PARAMETERIZED)
      {
        it = visited.find(cur.getOperator());
        Assert(it != visited.end());
        Assert(!it->second.isNull());
        childChanged = childChanged || cur.getOperator() != it->second;
        children.push_back(it->second);
      }
      for (const Node& cn : cur)
      {
        it = visited.find(cn);
        Assert(it != visited.end());
        Assert(!it->second.isNull());
        childChanged = childChanged || cn != it->second;
        children.push_back(it->second);
      }
      if (childChanged)
      {
        ret = nm->mkNode(cur.getKind(), children);
      }
      cur.setAttribute(ofa, ret);
      visited[cur] = ret;
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  Assert(!visited.find(n)->second.isNull());
  Trace("sk-manager-debug") << "..return " << visited[n] << std::endl;
  return visited[n];
}

Node SkolemManager::mkSkolemInternal(Node w,
                                     const std::string& prefix,
                                     const std::string& comment,
                                     int flags)
{
  // note that witness, original forms are independent, but share skolems
  NodeManager* nm = NodeManager::currentNM();
  // w is not necessarily a witness term
  SkolemFormAttribute sfa;
  Node k;
  // could already have a skolem if we used w already
  if (w.hasAttribute(sfa))
  {
    return w.getAttribute(sfa);
  }
  // make the new skolem
  if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
  {
    Assert (w.getType().isBoolean());
    k = nm->mkBooleanTermVariable();
  }
  else
  {
    k = nm->mkSkolem(prefix, w.getType(), comment, flags);
  }
  // set skolem form attribute for w
  w.setAttribute(sfa, k);
  Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
                      << std::endl;
  return k;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
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		*
13		* Implementation of skolem manager class.
14		*/
15
16		#include "expr/skolem_manager.h"
17
18		#include <sstream>
19
20		#include "expr/attribute.h"
21		#include "expr/bound_var_manager.h"
22		#include "expr/node_algorithm.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27
28		// Attributes are global maps from Nodes to data. Thus, note that these could
29		// be implemented as internal maps in SkolemManager.
30		struct WitnessFormAttributeId
31		{
32		};
33		typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
34
35		struct SkolemFormAttributeId
36		{
37		};
38		typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
39
40		struct OriginalFormAttributeId
41		{
42		};
43		typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
44
45	2465	const char* toString(SkolemFunId id)
46		{
47	2465	switch (id)
48		{
49	81	case SkolemFunId::DIV_BY_ZERO: return "DIV_BY_ZERO";
50	71	case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
51	35	case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
52	11	case SkolemFunId::SQRT: return "SQRT";
53	733	case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
54	755	case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
55	23	case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
56	732	case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT";
57	24	case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
58		default: return "?";
59		}
60		}
61
62	2465	std::ostream& operator<<(std::ostream& out, SkolemFunId id)
63		{
64	2465	out << toString(id);
65	2465	return out;
66		}
67
68	3793	Node SkolemManager::mkSkolem(Node v,
69		Node pred,
70		const std::string& prefix,
71		const std::string& comment,
72		int flags,
73		ProofGenerator* pg)
74		{
75		// We do not currently insist that pred does not contain witness terms
76	3793	Assert(v.getKind() == BOUND_VARIABLE);
77		// make the witness term
78	3793	NodeManager* nm = NodeManager::currentNM();
79	7586	Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
80		// Make the witness term, where notice that pred may contain skolems. We do
81		// not recursively convert pred to witness form, since witness terms should
82		// be treated as opaque. Moreover, the use of witness forms leads to
83		// variable shadowing issues in e.g. skolemization.
84	7586	Node w = nm->mkNode(WITNESS, bvl, pred);
85		// store the mapping to proof generator if it exists
86	3793	if (pg != nullptr)
87		{
88		// We cache based on the existential of the original predicate
89	3460	Node q = nm->mkNode(EXISTS, bvl, pred);
90		// Notice this may overwrite an existing proof generator. This does not
91		// matter since either should be able to prove q.
92	1730	d_gens[q] = pg;
93		}
94	3793	Node k = mkSkolemInternal(w, prefix, comment, flags);
95		// set witness form attribute for k
96		WitnessFormAttribute wfa;
97	3793	k.setAttribute(wfa, w);
98	7586	Trace("sk-manager-skolem")
99	3793	<< "skolem: " << k << " witness " << w << std::endl;
100	7586	return k;
101		}
102
103	515	Node SkolemManager::mkSkolemize(Node q,
104		std::vector<Node>& skolems,
105		const std::string& prefix,
106		const std::string& comment,
107		int flags,
108		ProofGenerator* pg)
109		{
110	515	Trace("sk-manager-debug") << "mkSkolemize " << q << std::endl;
111	515	Assert(q.getKind() == EXISTS);
112	515	Node currQ = q;
113	1382	for (const Node& av : q[0])
114		{
115	867	Assert(currQ.getKind() == EXISTS && av == currQ[0][0]);
116		// currQ is updated to the result of skolemizing its first variable in
117		// the method below.
118	1734	Node sk = skolemize(currQ, currQ, prefix, comment, flags);
119	1734	Trace("sk-manager-debug")
120	867	<< "made skolem " << sk << " for " << av << std::endl;
121	867	skolems.push_back(sk);
122		}
123	515	if (pg != nullptr)
124		{
125		// Same as above, this may overwrite an existing proof generator
126		d_gens[q] = pg;
127		}
128	515	Trace("sk-manager-debug") << "...mkSkolemize returns " << currQ << std::endl;
129	515	return currQ;
130		}
131
132	867	Node SkolemManager::skolemize(Node q,
133		Node& qskolem,
134		const std::string& prefix,
135		const std::string& comment,
136		int flags)
137		{
138	867	Assert(q.getKind() == EXISTS);
139	1734	Node v;
140	1734	std::vector<Node> ovars;
141	867	Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
142	867	NodeManager* nm = NodeManager::currentNM();
143	4523	for (const Node& av : q[0])
144		{
145	5390	if (v.isNull())
146		{
147	867	v = av;
148	867	continue;
149		}
150	3656	ovars.push_back(av);
151		}
152	867	Assert(!v.isNull());
153		// make the predicate with one variable stripped off
154	1734	Node pred = q[1];
155	867	Trace("sk-manager-debug") << "make exists predicate" << std::endl;
156	867	if (!ovars.empty())
157		{
158		// keeps the same variables
159	704	Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
160		// update the predicate
161	352	pred = nm->mkNode(EXISTS, bvl, pred);
162		}
163	867	Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
164		// don't use a proof generator, since this may be an intermediate, partially
165		// skolemized formula.
166	867	Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr);
167	867	Assert(k.getType() == v.getType());
168	1734	TNode tv = v;
169	1734	TNode tk = k;
170	1734	Trace("sk-manager-debug")
171	867	<< "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
172		// the quantified formula with one step of skolemization
173	867	qskolem = pred.substitute(tv, tk);
174	867	Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
175	1734	return k;
176		}
177
178	51495	Node SkolemManager::mkPurifySkolem(Node t,
179		const std::string& prefix,
180		const std::string& comment,
181		int flags)
182		{
183	102990	Node to = getOriginalForm(t);
184		// We do not currently insist that to does not contain witness terms
185
186	51495	Node k = mkSkolemInternal(to, prefix, comment, flags);
187		// set original form attribute for k
188		OriginalFormAttribute ofa;
189	51495	k.setAttribute(ofa, to);
190
191	102990	Trace("sk-manager-skolem")
192	51495	<< "skolem: " << k << " purify " << to << std::endl;
193	102990	return k;
194		}
195
196	6471	Node SkolemManager::mkSkolemFunction(SkolemFunId id,
197		TypeNode tn,
198		Node cacheVal,
199		int flags)
200		{
201	12942	std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal);
202		std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it =
203	6471	d_skolemFuns.find(key);
204	6471	if (it == d_skolemFuns.end())
205		{
206	2465	NodeManager* nm = NodeManager::currentNM();
207	4930	std::stringstream ss;
208	2465	ss << "SKOLEM_FUN_" << id;
209	4930	Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags);
210	2465	d_skolemFuns[key] = k;
211	2465	d_skolemFunMap[k] = key;
212	2465	return k;
213		}
214	4006	return it->second;
215		}
216
217	889	Node SkolemManager::mkSkolemFunction(SkolemFunId id,
218		TypeNode tn,
219		const std::vector<Node>& cacheVals,
220		int flags)
221		{
222	889	Assert(cacheVals.size() > 1);
223	1778	Node cacheVal = NodeManager::currentNM()->mkNode(SEXPR, cacheVals);
224	1778	return mkSkolemFunction(id, tn, cacheVal, flags);
225		}
226
227		bool SkolemManager::isSkolemFunction(Node k,
228		SkolemFunId& id,
229		Node& cacheVal) const
230		{
231		std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>>::const_iterator it =
232		d_skolemFunMap.find(k);
233		if (it == d_skolemFunMap.end())
234		{
235		return false;
236		}
237		id = std::get<0>(it->second);
238		cacheVal = std::get<2>(it->second);
239		return true;
240		}
241
242	122429	Node SkolemManager::mkDummySkolem(const std::string& prefix,
243		const TypeNode& type,
244		const std::string& comment,
245		int flags)
246		{
247	122429	return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
248		}
249
250	48	ProofGenerator* SkolemManager::getProofGenerator(Node t) const
251		{
252	48	std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
253	48	if (it != d_gens.end())
254		{
255		return it->second;
256		}
257	48	return nullptr;
258		}
259
260	1799	Node SkolemManager::getWitnessForm(Node k)
261		{
262	1799	Assert(k.getKind() == SKOLEM);
263		// simply look up the witness form for k via an attribute
264		WitnessFormAttribute wfa;
265	1799	return k.getAttribute(wfa);
266		}
267
268	128941	Node SkolemManager::getOriginalForm(Node n)
269		{
270	128941	if (n.isNull())
271		{
272	3	return n;
273		}
274	257876	Trace("sk-manager-debug")
275	128938	<< "SkolemManager::getOriginalForm " << n << std::endl;
276		OriginalFormAttribute ofa;
277	128938	NodeManager* nm = NodeManager::currentNM();
278	257876	std::unordered_map<TNode, Node> visited;
279	128938	std::unordered_map<TNode, Node>::iterator it;
280	257876	std::vector<TNode> visit;
281	257876	TNode cur;
282	128938	visit.push_back(n);
283	565626	do
284		{
285	694564	cur = visit.back();
286	694564	visit.pop_back();
287	694564	it = visited.find(cur);
288
289	694564	if (it == visited.end())
290		{
291	432671	if (cur.hasAttribute(ofa))
292		{
293	247298	visited[cur] = cur.getAttribute(ofa);
294		}
295		else
296		{
297	185373	visited[cur] = Node::null();
298	185373	visit.push_back(cur);
299	185373	if (cur.getMetaKind() == metakind::PARAMETERIZED)
300		{
301	26778	visit.push_back(cur.getOperator());
302		}
303	538848	for (const Node& cn : cur)
304		{
305	353475	visit.push_back(cn);
306		}
307		}
308		}
309	261893	else if (it->second.isNull())
310		{
311	370746	Node ret = cur;
312	185373	bool childChanged = false;
313	370746	std::vector<Node> children;
314	185373	if (cur.getMetaKind() == metakind::PARAMETERIZED)
315		{
316	26778	it = visited.find(cur.getOperator());
317	26778	Assert(it != visited.end());
318	26778	Assert(!it->second.isNull());
319	26778	childChanged = childChanged \|\| cur.getOperator() != it->second;
320	26778	children.push_back(it->second);
321		}
322	538848	for (const Node& cn : cur)
323		{
324	353475	it = visited.find(cn);
325	353475	Assert(it != visited.end());
326	353475	Assert(!it->second.isNull());
327	353475	childChanged = childChanged \|\| cn != it->second;
328	353475	children.push_back(it->second);
329		}
330	185373	if (childChanged)
331		{
332	47627	ret = nm->mkNode(cur.getKind(), children);
333		}
334	185373	cur.setAttribute(ofa, ret);
335	185373	visited[cur] = ret;
336		}
337	694564	} while (!visit.empty());
338	128938	Assert(visited.find(n) != visited.end());
339	128938	Assert(!visited.find(n)->second.isNull());
340	128938	Trace("sk-manager-debug") << "..return " << visited[n] << std::endl;
341	128938	return visited[n];
342		}
343
344	55288	Node SkolemManager::mkSkolemInternal(Node w,
345		const std::string& prefix,
346		const std::string& comment,
347		int flags)
348		{
349		// note that witness, original forms are independent, but share skolems
350	55288	NodeManager* nm = NodeManager::currentNM();
351		// w is not necessarily a witness term
352		SkolemFormAttribute sfa;
353	110576	Node k;
354		// could already have a skolem if we used w already
355	55288	if (w.hasAttribute(sfa))
356		{
357	9969	return w.getAttribute(sfa);
358		}
359		// make the new skolem
360	45319	if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
361		{
362	839	Assert (w.getType().isBoolean());
363	839	k = nm->mkBooleanTermVariable();
364		}
365		else
366		{
367	44480	k = nm->mkSkolem(prefix, w.getType(), comment, flags);
368		}
369		// set skolem form attribute for w
370	45319	w.setAttribute(sfa, k);
371	90638	Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
372	45319	<< std::endl;
373	45319	return k;
374		}
375
376	29577	} // namespace cvc5