Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/skolem_cache.cpp	Lines:	133	152	87.5 %
Date:	2021-11-07	Branches:	294	625	47.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Yoni Zohar
 *
 * 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 a cache of skolems for theory of strings.
 */

#include "theory/strings/skolem_cache.h"

#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
#include "expr/skolem_manager.h"
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
#include "util/rational.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

/**
 * A bound variable corresponding to the universally quantified integer
 * variable used to range over the valid positions in a string, used
 * for axiomatizing the behavior of some term.
 */
struct IndexVarAttributeId
{
};
typedef expr::Attribute<IndexVarAttributeId, Node> IndexVarAttribute;

/**
 * A bound variable corresponding to the universally quantified integer
 * variable used to range over the valid lengths of a string, used for
 * axiomatizing the behavior of some term.
 */
struct LengthVarAttributeId
{
};
typedef expr::Attribute<LengthVarAttributeId, Node> LengthVarAttribute;

SkolemCache::SkolemCache(Rewriter* rr) : d_rr(rr)
{
  NodeManager* nm = NodeManager::currentNM();
  d_strType = nm->stringType();
  d_zero = nm->mkConst(Rational(0));
}

Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
{
  return mkTypedSkolemCached(d_strType, a, b, id, c);
}

Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
{
  return mkSkolemCached(a, Node::null(), id, c);
}

Node SkolemCache::mkTypedSkolemCached(
    TypeNode tn, Node a, Node b, SkolemId id, const char* c)
{
  Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
                        << ", " << b << ")" << std::endl;
  SkolemId idOrig = id;
  // do not rewrite beforehand if we are not using optimizations, this is so
  // that the proof checker does not depend on the rewriter.
  if (d_rr != nullptr)
  {
    a = a.isNull() ? a : d_rr->rewrite(a);
    b = b.isNull() ? b : d_rr->rewrite(b);
  }
  std::tie(id, a, b) = normalizeStringSkolem(id, a, b);

  // optimization: if we aren't asking for the purification skolem for constant
  // a, and the skolem is equivalent to a, then we just return a.
  if (d_rr != nullptr && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
  {
    Trace("skolem-cache") << "...optimization: return constant " << a
                          << std::endl;
    return a;
  }

  std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
  if (it != d_skolemCache[a][b].end())
  {
    Trace("skolem-cache") << "...return existing " << it->second << std::endl;
    // already cached
    return it->second;
  }

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Node sk;
  switch (id)
  {
    // exists k. k = a
    case SK_PURIFY:
    {
      // for sequences of Booleans, we may purify Boolean terms, in which case
      // they must be Boolean term variables.
      int flags = a.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR
                                          : SkolemManager::SKOLEM_DEFAULT;
      sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags);
    }
    break;
    // these are eliminated by normalizeStringSkolem
    case SK_ID_V_SPT:
    case SK_ID_V_SPT_REV:
    case SK_ID_VC_SPT:
    case SK_ID_VC_SPT_REV:
    case SK_ID_C_SPT:
    case SK_ID_C_SPT_REV:
    case SK_ID_DC_SPT:
    case SK_ID_DC_SPT_REM:
    case SK_ID_DEQ_X:
    case SK_ID_DEQ_Y:
    case SK_FIRST_CTN_PRE:
    case SK_FIRST_CTN_POST:
    case SK_PREFIX:
    case SK_SUFFIX_REM:
      Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
      break;
    default:
    {
      Trace("skolem-cache")
          << "Don't know how to handle Skolem ID " << id << std::endl;
      Node v = nm->mkBoundVar(tn);
      Node cond = nm->mkConst(true);
      sk = sm->mkSkolem(v, cond, c, "string skolem");
    }
    break;
  }
  Trace("skolem-cache") << "...returned " << sk << std::endl;
  d_allSkolems.insert(sk);
  d_skolemCache[a][b][id] = sk;
  return sk;
}
Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
                                      Node a,
                                      SkolemId id,
                                      const char* c)
{
  return mkTypedSkolemCached(tn, a, Node::null(), id, c);
}

Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
{
  // Note this method is static and does not rely on any local caching.
  // It is used by expand definitions and by (dynamic) reductions, thus
  // it is centrally located here.
  Assert(seqType.isSequence());
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  std::vector<TypeNode> argTypes;
  argTypes.push_back(seqType);
  argTypes.push_back(nm->integerType());
  TypeNode elemType = seqType.getSequenceElementType();
  TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
  return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType);
}

Node SkolemCache::mkSkolem(const char* c)
{
  // TODO: eliminate this
  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
  Node n = sm->mkDummySkolem(c, d_strType, "string skolem");
  d_allSkolems.insert(n);
  return n;
}

bool SkolemCache::isSkolem(Node n) const
{
  return d_allSkolems.find(n) != d_allSkolems.end();
}

std::tuple<SkolemCache::SkolemId, Node, Node>
SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
{

  NodeManager* nm = NodeManager::currentNM();

  // eliminate in terms of prefix/suffix_rem
  if (id == SK_FIRST_CTN_POST)
  {
    // SK_FIRST_CTN_POST(x, y) --->
    //   SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
    id = SK_SUFFIX_REM;
    Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
    b = nm->mkNode(
        PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b));
  }
  else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
  {
    // SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
    id = SK_SUFFIX_REM;
    b = nm->mkNode(STRING_LENGTH, b);
  }
  else if (id == SK_ID_V_SPT_REV || id == SK_ID_C_SPT_REV)
  {
    // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
    id = SK_PREFIX;
    b = nm->mkNode(
        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
  }
  else if (id == SK_ID_VC_SPT)
  {
    // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
    id = SK_SUFFIX_REM;
    b = nm->mkConst(Rational(1));
  }
  else if (id == SK_ID_VC_SPT_REV)
  {
    // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
    id = SK_PREFIX;
    b = nm->mkNode(
        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)));
  }
  else if (id == SK_ID_DC_SPT)
  {
    // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
    id = SK_PREFIX;
    b = nm->mkConst(Rational(1));
  }
  else if (id == SK_ID_DC_SPT_REM)
  {
    // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
    id = SK_SUFFIX_REM;
    b = nm->mkConst(Rational(1));
  }
  else if (id == SK_ID_DEQ_X)
  {
    // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x))
    id = SK_PREFIX;
    Node aOld = a;
    a = b;
    b = nm->mkNode(STRING_LENGTH, aOld);
  }
  else if (id == SK_ID_DEQ_Y)
  {
    // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
    id = SK_PREFIX;
    b = nm->mkNode(STRING_LENGTH, b);
  }
  else if (id == SK_FIRST_CTN_PRE)
  {
    // SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
    id = SK_PREFIX;
    b = nm->mkNode(STRING_INDEXOF, a, b, d_zero);
  }

  if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
  {
    bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
    Node la = nm->mkNode(STRING_LENGTH, a);
    Node lb = nm->mkNode(STRING_LENGTH, b);
    Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb))
                    : utils::mkSuffix(a, lb);
    Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la))
                    : utils::mkSuffix(b, la);
    id = SK_PURIFY;
    // SK_ID_V_UNIFIED_SPT(x,y) --->
    //   ite(len(x) >= len(y), substr(x,0,str.len(y)), substr(y,0,str.len(x))
    a = nm->mkNode(ITE, nm->mkNode(GEQ, la, lb), ta, tb);
    b = Node::null();
  }

  // now, eliminate prefix/suffix_rem in terms of purify
  if (id == SK_PREFIX)
  {
    // SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
    id = SK_PURIFY;
    a = utils::mkPrefix(a, b);
    b = Node::null();
  }
  else if (id == SK_SUFFIX_REM)
  {
    // SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
    id = SK_PURIFY;
    a = utils::mkSuffix(a, b);
    b = Node::null();
  }

  if (d_rr != nullptr)
  {
    a = a.isNull() ? a : d_rr->rewrite(a);
    b = b.isNull() ? b : d_rr->rewrite(b);
  }
  Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
                        << ", " << b << ")" << std::endl;
  return std::make_tuple(id, a, b);
}

Node SkolemCache::mkIndexVar(Node t)
{
  NodeManager* nm = NodeManager::currentNM();
  TypeNode intType = nm->integerType();
  BoundVarManager* bvm = nm->getBoundVarManager();
  return bvm->mkBoundVar<IndexVarAttribute>(t, intType);
}

Node SkolemCache::mkLengthVar(Node t)
{
  NodeManager* nm = NodeManager::currentNM();
  TypeNode intType = nm->integerType();
  BoundVarManager* bvm = nm->getBoundVarManager();
  return bvm->mkBoundVar<LengthVarAttribute>(t, intType);
}

Node SkolemCache::mkSkolemFun(SkolemFunId id, TypeNode tn, Node a, Node b)
{
  std::vector<Node> cacheVals;
  for (size_t i = 0; i < 2; i++)
  {
    Node n = i == 0 ? a : b;
    if (!n.isNull())
    {
      n = d_rr != nullptr ? d_rr->rewrite(n) : n;
      cacheVals.push_back(n);
    }
  }
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Node k = sm->mkSkolemFunction(id, tn, cacheVals);
  d_allSkolems.insert(k);
  return k;
}

}  // namespace strings
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Yoni Zohar
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 a cache of skolems for theory of strings.
14		*/
15
16		#include "theory/strings/skolem_cache.h"
17
18		#include "expr/attribute.h"
19		#include "expr/bound_var_manager.h"
20		#include "expr/skolem_manager.h"
21		#include "theory/rewriter.h"
22		#include "theory/strings/arith_entail.h"
23		#include "theory/strings/theory_strings_utils.h"
24		#include "theory/strings/word.h"
25		#include "util/rational.h"
26
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace strings {
32
33		/**
34		* A bound variable corresponding to the universally quantified integer
35		* variable used to range over the valid positions in a string, used
36		* for axiomatizing the behavior of some term.
37		*/
38		struct IndexVarAttributeId
39		{
40		};
41		typedef expr::Attribute<IndexVarAttributeId, Node> IndexVarAttribute;
42
43		/**
44		* A bound variable corresponding to the universally quantified integer
45		* variable used to range over the valid lengths of a string, used for
46		* axiomatizing the behavior of some term.
47		*/
48		struct LengthVarAttributeId
49		{
50		};
51		typedef expr::Attribute<LengthVarAttributeId, Node> LengthVarAttribute;
52
53	16427	SkolemCache::SkolemCache(Rewriter* rr) : d_rr(rr)
54		{
55	16427	NodeManager* nm = NodeManager::currentNM();
56	16427	d_strType = nm->stringType();
57	16427	d_zero = nm->mkConst(Rational(0));
58	16427	}
59
60	40972	Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
61		{
62	40972	return mkTypedSkolemCached(d_strType, a, b, id, c);
63		}
64
65	18028	Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
66		{
67	18028	return mkSkolemCached(a, Node::null(), id, c);
68		}
69
70	41315	Node SkolemCache::mkTypedSkolemCached(
71		TypeNode tn, Node a, Node b, SkolemId id, const char* c)
72		{
73	82630	Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
74	41315	<< ", " << b << ")" << std::endl;
75	41315	SkolemId idOrig = id;
76		// do not rewrite beforehand if we are not using optimizations, this is so
77		// that the proof checker does not depend on the rewriter.
78	41315	if (d_rr != nullptr)
79		{
80	39125	a = a.isNull() ? a : d_rr->rewrite(a);
81	39125	b = b.isNull() ? b : d_rr->rewrite(b);
82		}
83	41315	std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
84
85		// optimization: if we aren't asking for the purification skolem for constant
86		// a, and the skolem is equivalent to a, then we just return a.
87	41315	if (d_rr != nullptr && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
88		{
89	1764	Trace("skolem-cache") << "...optimization: return constant " << a
90	882	<< std::endl;
91	882	return a;
92		}
93
94	40433	std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
95	40433	if (it != d_skolemCache[a][b].end())
96		{
97	21968	Trace("skolem-cache") << "...return existing " << it->second << std::endl;
98		// already cached
99	21968	return it->second;
100		}
101
102	18465	NodeManager* nm = NodeManager::currentNM();
103	18465	SkolemManager* sm = nm->getSkolemManager();
104	36930	Node sk;
105	18465	switch (id)
106		{
107		// exists k. k = a
108	18465	case SK_PURIFY:
109		{
110		// for sequences of Booleans, we may purify Boolean terms, in which case
111		// they must be Boolean term variables.
112	36930	int flags = a.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR
113	18465	: SkolemManager::SKOLEM_DEFAULT;
114	18465	sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags);
115		}
116	18465	break;
117		// these are eliminated by normalizeStringSkolem
118		case SK_ID_V_SPT:
119		case SK_ID_V_SPT_REV:
120		case SK_ID_VC_SPT:
121		case SK_ID_VC_SPT_REV:
122		case SK_ID_C_SPT:
123		case SK_ID_C_SPT_REV:
124		case SK_ID_DC_SPT:
125		case SK_ID_DC_SPT_REM:
126		case SK_ID_DEQ_X:
127		case SK_ID_DEQ_Y:
128		case SK_FIRST_CTN_PRE:
129		case SK_FIRST_CTN_POST:
130		case SK_PREFIX:
131		case SK_SUFFIX_REM:
132		Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
133		break;
134		default:
135		{
136		Trace("skolem-cache")
137		<< "Don't know how to handle Skolem ID " << id << std::endl;
138		Node v = nm->mkBoundVar(tn);
139		Node cond = nm->mkConst(true);
140		sk = sm->mkSkolem(v, cond, c, "string skolem");
141		}
142		break;
143		}
144	18465	Trace("skolem-cache") << "...returned " << sk << std::endl;
145	18465	d_allSkolems.insert(sk);
146	18465	d_skolemCache[a][b][id] = sk;
147	18465	return sk;
148		}
149	343	Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
150		Node a,
151		SkolemId id,
152		const char* c)
153		{
154	343	return mkTypedSkolemCached(tn, a, Node::null(), id, c);
155		}
156
157	56	Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
158		{
159		// Note this method is static and does not rely on any local caching.
160		// It is used by expand definitions and by (dynamic) reductions, thus
161		// it is centrally located here.
162	56	Assert(seqType.isSequence());
163	56	NodeManager* nm = NodeManager::currentNM();
164	56	SkolemManager* sm = nm->getSkolemManager();
165	112	std::vector<TypeNode> argTypes;
166	56	argTypes.push_back(seqType);
167	56	argTypes.push_back(nm->integerType());
168	112	TypeNode elemType = seqType.getSequenceElementType();
169	112	TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
170	112	return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType);
171		}
172
173	1170	Node SkolemCache::mkSkolem(const char* c)
174		{
175		// TODO: eliminate this
176	1170	SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
177	1170	Node n = sm->mkDummySkolem(c, d_strType, "string skolem");
178	1170	d_allSkolems.insert(n);
179	1170	return n;
180		}
181
182	4648	bool SkolemCache::isSkolem(Node n) const
183		{
184	4648	return d_allSkolems.find(n) != d_allSkolems.end();
185		}
186
187		std::tuple<SkolemCache::SkolemId, Node, Node>
188	41315	SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
189		{
190
191	41315	NodeManager* nm = NodeManager::currentNM();
192
193		// eliminate in terms of prefix/suffix_rem
194	41315	if (id == SK_FIRST_CTN_POST)
195		{
196		// SK_FIRST_CTN_POST(x, y) --->
197		// SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
198	4473	id = SK_SUFFIX_REM;
199	8946	Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
200	13419	b = nm->mkNode(
201	17892	PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b));
202		}
203	36842	else if (id == SK_ID_V_SPT \|\| id == SK_ID_C_SPT)
204		{
205		// SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
206	492	id = SK_SUFFIX_REM;
207	492	b = nm->mkNode(STRING_LENGTH, b);
208		}
209	36350	else if (id == SK_ID_V_SPT_REV \|\| id == SK_ID_C_SPT_REV)
210		{
211		// SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
212	487	id = SK_PREFIX;
213	1948	b = nm->mkNode(
214	1948	MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
215		}
216	35863	else if (id == SK_ID_VC_SPT)
217		{
218		// SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
219	2677	id = SK_SUFFIX_REM;
220	2677	b = nm->mkConst(Rational(1));
221		}
222	33186	else if (id == SK_ID_VC_SPT_REV)
223		{
224		// SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
225	3216	id = SK_PREFIX;
226	9648	b = nm->mkNode(
227	12864	MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)));
228		}
229	29970	else if (id == SK_ID_DC_SPT)
230		{
231		// SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
232		id = SK_PREFIX;
233		b = nm->mkConst(Rational(1));
234		}
235	29970	else if (id == SK_ID_DC_SPT_REM)
236		{
237		// SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
238		id = SK_SUFFIX_REM;
239		b = nm->mkConst(Rational(1));
240		}
241	29970	else if (id == SK_ID_DEQ_X)
242		{
243		// SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x))
244		id = SK_PREFIX;
245		Node aOld = a;
246		a = b;
247		b = nm->mkNode(STRING_LENGTH, aOld);
248		}
249	29970	else if (id == SK_ID_DEQ_Y)
250		{
251		// SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
252		id = SK_PREFIX;
253		b = nm->mkNode(STRING_LENGTH, b);
254		}
255	29970	else if (id == SK_FIRST_CTN_PRE)
256		{
257		// SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
258	8950	id = SK_PREFIX;
259	8950	b = nm->mkNode(STRING_INDEXOF, a, b, d_zero);
260		}
261
262	41315	if (id == SK_ID_V_UNIFIED_SPT \|\| id == SK_ID_V_UNIFIED_SPT_REV)
263		{
264	4656	bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
265	9312	Node la = nm->mkNode(STRING_LENGTH, a);
266	9312	Node lb = nm->mkNode(STRING_LENGTH, b);
267	6659	Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb))
268	11315	: utils::mkSuffix(a, lb);
269	6659	Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la))
270	11315	: utils::mkSuffix(b, la);
271	4656	id = SK_PURIFY;
272		// SK_ID_V_UNIFIED_SPT(x,y) --->
273		// ite(len(x) >= len(y), substr(x,0,str.len(y)), substr(y,0,str.len(x))
274	4656	a = nm->mkNode(ITE, nm->mkNode(GEQ, la, lb), ta, tb);
275	4656	b = Node::null();
276		}
277
278		// now, eliminate prefix/suffix_rem in terms of purify
279	41315	if (id == SK_PREFIX)
280		{
281		// SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
282	14596	id = SK_PURIFY;
283	14596	a = utils::mkPrefix(a, b);
284	14596	b = Node::null();
285		}
286	26719	else if (id == SK_SUFFIX_REM)
287		{
288		// SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
289	9585	id = SK_PURIFY;
290	9585	a = utils::mkSuffix(a, b);
291	9585	b = Node::null();
292		}
293
294	41315	if (d_rr != nullptr)
295		{
296	39125	a = a.isNull() ? a : d_rr->rewrite(a);
297	39125	b = b.isNull() ? b : d_rr->rewrite(b);
298		}
299	82630	Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
300	41315	<< ", " << b << ")" << std::endl;
301	41315	return std::make_tuple(id, a, b);
302		}
303
304	455	Node SkolemCache::mkIndexVar(Node t)
305		{
306	455	NodeManager* nm = NodeManager::currentNM();
307	910	TypeNode intType = nm->integerType();
308	455	BoundVarManager* bvm = nm->getBoundVarManager();
309	910	return bvm->mkBoundVar<IndexVarAttribute>(t, intType);
310		}
311
312	176	Node SkolemCache::mkLengthVar(Node t)
313		{
314	176	NodeManager* nm = NodeManager::currentNM();
315	352	TypeNode intType = nm->integerType();
316	176	BoundVarManager* bvm = nm->getBoundVarManager();
317	352	return bvm->mkBoundVar<LengthVarAttribute>(t, intType);
318		}
319
320	446	Node SkolemCache::mkSkolemFun(SkolemFunId id, TypeNode tn, Node a, Node b)
321		{
322	892	std::vector<Node> cacheVals;
323	1338	for (size_t i = 0; i < 2; i++)
324		{
325	1784	Node n = i == 0 ? a : b;
326	892	if (!n.isNull())
327		{
328	706	n = d_rr != nullptr ? d_rr->rewrite(n) : n;
329	706	cacheVals.push_back(n);
330		}
331		}
332	446	NodeManager* nm = NodeManager::currentNM();
333	446	SkolemManager* sm = nm->getSkolemManager();
334	446	Node k = sm->mkSkolemFunction(id, tn, cacheVals);
335	446	d_allSkolems.insert(k);
336	892	return k;
337		}
338
339		} // namespace strings
340		} // namespace theory
341	31137	} // namespace cvc5