Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/skolem_manager.cpp	Lines:	187	198	94.4 %
Date:	2021-11-07	Branches:	346	807	42.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"
#include "expr/node_manager_attributes.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::STRINGS_NUM_OCCUR: return "STRINGS_NUM_OCCUR";
    case SkolemFunId::STRINGS_OCCUR_INDEX: return "STRINGS_OCCUR_INDEX";
    case SkolemFunId::STRINGS_OCCUR_LEN: return "STRINGS_OCCUR_LEN";
    case SkolemFunId::STRINGS_DEQ_DIFF: return "STRINGS_DEQ_DIFF";
    case SkolemFunId::STRINGS_REPLACE_ALL_RESULT:
      return "STRINGS_REPLACE_ALL_RESULT";
    case SkolemFunId::STRINGS_ITOS_RESULT: return "STRINGS_ITOS_RESULT";
    case SkolemFunId::STRINGS_STOI_RESULT: return "STRINGS_STOI_RESULT";
    case SkolemFunId::STRINGS_STOI_NON_DIGIT: return "STRINGS_STOI_NON_DIGIT";
    case SkolemFunId::SK_FIRST_MATCH_PRE: return "SK_FIRST_MATCH_PRE";
    case SkolemFunId::SK_FIRST_MATCH: return "SK_FIRST_MATCH";
    case SkolemFunId::SK_FIRST_MATCH_POST: return "SK_FIRST_MATCH_POST";
    case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT";
    case SkolemFunId::BAGS_MAP_PREIMAGE: return "BAGS_MAP_PREIMAGE";
    case SkolemFunId::BAGS_MAP_SUM: return "BAGS_MAP_SUM";
    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;
}

SkolemManager::SkolemManager() : d_skolemCounter(0) {}

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())
  {
    std::stringstream ss;
    ss << "SKOLEM_FUN_" << id;
    Node k = mkSkolemNode(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)
{
  Node cacheVal;
  // use null node if cacheVals is empty
  if (!cacheVals.empty())
  {
    cacheVal = cacheVals.size() == 1
                   ? cacheVals[0]
                   : 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 mkSkolemNode(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
  // w is not necessarily a witness term
  SkolemFormAttribute sfa;
  // could already have a skolem if we used w already
  if (w.hasAttribute(sfa))
  {
    return w.getAttribute(sfa);
  }
  // make the new skolem
  Node k = mkSkolemNode(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;
}

Node SkolemManager::mkSkolemNode(const std::string& prefix,
                                 const TypeNode& type,
                                 const std::string& comment,
                                 int flags)
{
  NodeManager* nm = NodeManager::currentNM();
  Node n;
  if (flags & SKOLEM_BOOL_TERM_VAR)
  {
    Assert(type.isBoolean());
    n = NodeBuilder(nm, BOOLEAN_TERM_VARIABLE);
  }
  else
  {
    n = NodeBuilder(nm, SKOLEM);
    if ((flags & SKOLEM_EXACT_NAME) == 0)
    {
      std::stringstream name;
      name << prefix << '_' << ++d_skolemCounter;
      n.setAttribute(expr::VarNameAttr(), name.str());
    }
    else
    {
      n.setAttribute(expr::VarNameAttr(), prefix);
    }
  }
  n.setAttribute(expr::TypeAttr(), type);
  n.setAttribute(expr::TypeCheckedAttr(), true);
  return n;
}

}  // 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		#include "expr/node_manager_attributes.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28
29		// Attributes are global maps from Nodes to data. Thus, note that these could
30		// be implemented as internal maps in SkolemManager.
31		struct WitnessFormAttributeId
32		{
33		};
34		typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
35
36		struct SkolemFormAttributeId
37		{
38		};
39		typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
40
41		struct OriginalFormAttributeId
42		{
43		};
44		typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
45
46	3573	const char* toString(SkolemFunId id)
47		{
48	3573	switch (id)
49		{
50	98	case SkolemFunId::DIV_BY_ZERO: return "DIV_BY_ZERO";
51	72	case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
52	43	case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
53	13	case SkolemFunId::SQRT: return "SQRT";
54	791	case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
55	1357	case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
56	25	case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
57	32	case SkolemFunId::STRINGS_NUM_OCCUR: return "STRINGS_NUM_OCCUR";
58	32	case SkolemFunId::STRINGS_OCCUR_INDEX: return "STRINGS_OCCUR_INDEX";
59	18	case SkolemFunId::STRINGS_OCCUR_LEN: return "STRINGS_OCCUR_LEN";
60		case SkolemFunId::STRINGS_DEQ_DIFF: return "STRINGS_DEQ_DIFF";
61	34	case SkolemFunId::STRINGS_REPLACE_ALL_RESULT:
62	34	return "STRINGS_REPLACE_ALL_RESULT";
63	26	case SkolemFunId::STRINGS_ITOS_RESULT: return "STRINGS_ITOS_RESULT";
64	45	case SkolemFunId::STRINGS_STOI_RESULT: return "STRINGS_STOI_RESULT";
65	45	case SkolemFunId::STRINGS_STOI_NON_DIGIT: return "STRINGS_STOI_NON_DIGIT";
66	30	case SkolemFunId::SK_FIRST_MATCH_PRE: return "SK_FIRST_MATCH_PRE";
67	30	case SkolemFunId::SK_FIRST_MATCH: return "SK_FIRST_MATCH";
68	30	case SkolemFunId::SK_FIRST_MATCH_POST: return "SK_FIRST_MATCH_POST";
69	820	case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT";
70	4	case SkolemFunId::BAGS_MAP_PREIMAGE: return "BAGS_MAP_PREIMAGE";
71	4	case SkolemFunId::BAGS_MAP_SUM: return "BAGS_MAP_SUM";
72	24	case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
73		default: return "?";
74		}
75		}
76
77	3573	std::ostream& operator<<(std::ostream& out, SkolemFunId id)
78		{
79	3573	out << toString(id);
80	3573	return out;
81		}
82
83	10379	SkolemManager::SkolemManager() : d_skolemCounter(0) {}
84
85	3793	Node SkolemManager::mkSkolem(Node v,
86		Node pred,
87		const std::string& prefix,
88		const std::string& comment,
89		int flags,
90		ProofGenerator* pg)
91		{
92		// We do not currently insist that pred does not contain witness terms
93	3793	Assert(v.getKind() == BOUND_VARIABLE);
94		// make the witness term
95	3793	NodeManager* nm = NodeManager::currentNM();
96	7586	Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
97		// Make the witness term, where notice that pred may contain skolems. We do
98		// not recursively convert pred to witness form, since witness terms should
99		// be treated as opaque. Moreover, the use of witness forms leads to
100		// variable shadowing issues in e.g. skolemization.
101	7586	Node w = nm->mkNode(WITNESS, bvl, pred);
102		// store the mapping to proof generator if it exists
103	3793	if (pg != nullptr)
104		{
105		// We cache based on the existential of the original predicate
106	3712	Node q = nm->mkNode(EXISTS, bvl, pred);
107		// Notice this may overwrite an existing proof generator. This does not
108		// matter since either should be able to prove q.
109	1856	d_gens[q] = pg;
110		}
111	3793	Node k = mkSkolemInternal(w, prefix, comment, flags);
112		// set witness form attribute for k
113		WitnessFormAttribute wfa;
114	3793	k.setAttribute(wfa, w);
115	7586	Trace("sk-manager-skolem")
116	3793	<< "skolem: " << k << " witness " << w << std::endl;
117	7586	return k;
118		}
119
120	535	Node SkolemManager::mkSkolemize(Node q,
121		std::vector<Node>& skolems,
122		const std::string& prefix,
123		const std::string& comment,
124		int flags,
125		ProofGenerator* pg)
126		{
127	535	Trace("sk-manager-debug") << "mkSkolemize " << q << std::endl;
128	535	Assert(q.getKind() == EXISTS);
129	535	Node currQ = q;
130	1435	for (const Node& av : q[0])
131		{
132	900	Assert(currQ.getKind() == EXISTS && av == currQ[0][0]);
133		// currQ is updated to the result of skolemizing its first variable in
134		// the method below.
135	1800	Node sk = skolemize(currQ, currQ, prefix, comment, flags);
136	1800	Trace("sk-manager-debug")
137	900	<< "made skolem " << sk << " for " << av << std::endl;
138	900	skolems.push_back(sk);
139		}
140	535	if (pg != nullptr)
141		{
142		// Same as above, this may overwrite an existing proof generator
143		d_gens[q] = pg;
144		}
145	535	Trace("sk-manager-debug") << "...mkSkolemize returns " << currQ << std::endl;
146	535	return currQ;
147		}
148
149	900	Node SkolemManager::skolemize(Node q,
150		Node& qskolem,
151		const std::string& prefix,
152		const std::string& comment,
153		int flags)
154		{
155	900	Assert(q.getKind() == EXISTS);
156	1800	Node v;
157	1800	std::vector<Node> ovars;
158	900	Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
159	900	NodeManager* nm = NodeManager::currentNM();
160	4572	for (const Node& av : q[0])
161		{
162	5472	if (v.isNull())
163		{
164	900	v = av;
165	900	continue;
166		}
167	3672	ovars.push_back(av);
168		}
169	900	Assert(!v.isNull());
170		// make the predicate with one variable stripped off
171	1800	Node pred = q[1];
172	900	Trace("sk-manager-debug") << "make exists predicate" << std::endl;
173	900	if (!ovars.empty())
174		{
175		// keeps the same variables
176	730	Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
177		// update the predicate
178	365	pred = nm->mkNode(EXISTS, bvl, pred);
179		}
180	900	Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
181		// don't use a proof generator, since this may be an intermediate, partially
182		// skolemized formula.
183	900	Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr);
184	900	Assert(k.getType() == v.getType());
185	1800	TNode tv = v;
186	1800	TNode tk = k;
187	1800	Trace("sk-manager-debug")
188	900	<< "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
189		// the quantified formula with one step of skolemization
190	900	qskolem = pred.substitute(tv, tk);
191	900	Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
192	1800	return k;
193		}
194
195	54775	Node SkolemManager::mkPurifySkolem(Node t,
196		const std::string& prefix,
197		const std::string& comment,
198		int flags)
199		{
200	109550	Node to = getOriginalForm(t);
201		// We do not currently insist that to does not contain witness terms
202
203	54775	Node k = mkSkolemInternal(to, prefix, comment, flags);
204		// set original form attribute for k
205		OriginalFormAttribute ofa;
206	54775	k.setAttribute(ofa, to);
207
208	109550	Trace("sk-manager-skolem")
209	54775	<< "skolem: " << k << " purify " << to << std::endl;
210	109550	return k;
211		}
212
213	8506	Node SkolemManager::mkSkolemFunction(SkolemFunId id,
214		TypeNode tn,
215		Node cacheVal,
216		int flags)
217		{
218	17012	std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal);
219		std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it =
220	8506	d_skolemFuns.find(key);
221	8506	if (it == d_skolemFuns.end())
222		{
223	7146	std::stringstream ss;
224	3573	ss << "SKOLEM_FUN_" << id;
225	7146	Node k = mkSkolemNode(ss.str(), tn, "an internal skolem function", flags);
226	3573	d_skolemFuns[key] = k;
227	3573	d_skolemFunMap[k] = key;
228	3573	return k;
229		}
230	4933	return it->second;
231		}
232
233	1473	Node SkolemManager::mkSkolemFunction(SkolemFunId id,
234		TypeNode tn,
235		const std::vector<Node>& cacheVals,
236		int flags)
237		{
238	2946	Node cacheVal;
239		// use null node if cacheVals is empty
240	1473	if (!cacheVals.empty())
241		{
242	2946	cacheVal = cacheVals.size() == 1
243	2946	? cacheVals[0]
244		: NodeManager::currentNM()->mkNode(SEXPR, cacheVals);
245		}
246	2946	return mkSkolemFunction(id, tn, cacheVal, flags);
247		}
248
249		bool SkolemManager::isSkolemFunction(Node k,
250		SkolemFunId& id,
251		Node& cacheVal) const
252		{
253		std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>>::const_iterator it =
254		d_skolemFunMap.find(k);
255		if (it == d_skolemFunMap.end())
256		{
257		return false;
258		}
259		id = std::get<0>(it->second);
260		cacheVal = std::get<2>(it->second);
261		return true;
262		}
263
264	164174	Node SkolemManager::mkDummySkolem(const std::string& prefix,
265		const TypeNode& type,
266		const std::string& comment,
267		int flags)
268		{
269	164174	return mkSkolemNode(prefix, type, comment, flags);
270		}
271
272	48	ProofGenerator* SkolemManager::getProofGenerator(Node t) const
273		{
274	48	std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
275	48	if (it != d_gens.end())
276		{
277		return it->second;
278		}
279	48	return nullptr;
280		}
281
282	1862	Node SkolemManager::getWitnessForm(Node k)
283		{
284	1862	Assert(k.getKind() == SKOLEM);
285		// simply look up the witness form for k via an attribute
286		WitnessFormAttribute wfa;
287	1862	return k.getAttribute(wfa);
288		}
289
290	651961	Node SkolemManager::getOriginalForm(Node n)
291		{
292	651961	if (n.isNull())
293		{
294	3	return n;
295		}
296	1303916	Trace("sk-manager-debug")
297	651958	<< "SkolemManager::getOriginalForm " << n << std::endl;
298		OriginalFormAttribute ofa;
299	651958	NodeManager* nm = NodeManager::currentNM();
300	1303916	std::unordered_map<TNode, Node> visited;
301	651958	std::unordered_map<TNode, Node>::iterator it;
302	1303916	std::vector<TNode> visit;
303	1303916	TNode cur;
304	651958	visit.push_back(n);
305	585467	do
306		{
307	1237425	cur = visit.back();
308	1237425	visit.pop_back();
309	1237425	it = visited.find(cur);
310
311	1237425	if (it == visited.end())
312		{
313	967358	if (cur.hasAttribute(ofa))
314		{
315	775100	visited[cur] = cur.getAttribute(ofa);
316		}
317		else
318		{
319	192258	visited[cur] = Node::null();
320	192258	visit.push_back(cur);
321	192258	if (cur.getMetaKind() == metakind::PARAMETERIZED)
322		{
323	29953	visit.push_back(cur.getOperator());
324		}
325	555514	for (const Node& cn : cur)
326		{
327	363256	visit.push_back(cn);
328		}
329		}
330		}
331	270067	else if (it->second.isNull())
332		{
333	384516	Node ret = cur;
334	192258	bool childChanged = false;
335	384516	std::vector<Node> children;
336	192258	if (cur.getMetaKind() == metakind::PARAMETERIZED)
337		{
338	29953	it = visited.find(cur.getOperator());
339	29953	Assert(it != visited.end());
340	29953	Assert(!it->second.isNull());
341	29953	childChanged = childChanged \|\| cur.getOperator() != it->second;
342	29953	children.push_back(it->second);
343		}
344	555514	for (const Node& cn : cur)
345		{
346	363256	it = visited.find(cn);
347	363256	Assert(it != visited.end());
348	363256	Assert(!it->second.isNull());
349	363256	childChanged = childChanged \|\| cn != it->second;
350	363256	children.push_back(it->second);
351		}
352	192258	if (childChanged)
353		{
354	51500	ret = nm->mkNode(cur.getKind(), children);
355		}
356	192258	cur.setAttribute(ofa, ret);
357	192258	visited[cur] = ret;
358		}
359	1237425	} while (!visit.empty());
360	651958	Assert(visited.find(n) != visited.end());
361	651958	Assert(!visited.find(n)->second.isNull());
362	651958	Trace("sk-manager-debug") << "..return " << visited[n] << std::endl;
363	651958	return visited[n];
364		}
365
366	58568	Node SkolemManager::mkSkolemInternal(Node w,
367		const std::string& prefix,
368		const std::string& comment,
369		int flags)
370		{
371		// note that witness, original forms are independent, but share skolems
372		// w is not necessarily a witness term
373		SkolemFormAttribute sfa;
374		// could already have a skolem if we used w already
375	58568	if (w.hasAttribute(sfa))
376		{
377	11478	return w.getAttribute(sfa);
378		}
379		// make the new skolem
380	94180	Node k = mkSkolemNode(prefix, w.getType(), comment, flags);
381		// set skolem form attribute for w
382	47090	w.setAttribute(sfa, k);
383	94180	Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
384	47090	<< std::endl;
385	47090	return k;
386		}
387
388	214837	Node SkolemManager::mkSkolemNode(const std::string& prefix,
389		const TypeNode& type,
390		const std::string& comment,
391		int flags)
392		{
393	214837	NodeManager* nm = NodeManager::currentNM();
394	214837	Node n;
395	214837	if (flags & SKOLEM_BOOL_TERM_VAR)
396		{
397	898	Assert(type.isBoolean());
398	898	n = NodeBuilder(nm, BOOLEAN_TERM_VARIABLE);
399		}
400		else
401		{
402	213939	n = NodeBuilder(nm, SKOLEM);
403	213939	if ((flags & SKOLEM_EXACT_NAME) == 0)
404		{
405	193106	std::stringstream name;
406	96553	name << prefix << '_' << ++d_skolemCounter;
407	96553	n.setAttribute(expr::VarNameAttr(), name.str());
408		}
409		else
410		{
411	117386	n.setAttribute(expr::VarNameAttr(), prefix);
412		}
413		}
414	214837	n.setAttribute(expr::TypeAttr(), type);
415	214837	n.setAttribute(expr::TypeCheckedAttr(), true);
416	214837	return n;
417		}
418
419	31137	} // namespace cvc5