Home
last modified time | relevance | path

Searched refs:SK_FIRST_CTN_PRE (Results 1 – 5 of 5) sorted by relevance

/dports/math/cvc4/CVC4-1.7/test/unit/theory/
H A Dtheory_strings_skolem_cache_black.h61 Node s1 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); in testMkSkolemCached()
62 Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); in testMkSkolemCached()
72 Node s1 = sk.mkSkolemCached(c, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); in testMkSkolemCached()
73 Node s2 = sk.mkSkolemCached(sc, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); in testMkSkolemCached()
84 Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo"); in testMkSkolemCached()
/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dskolem_cache.cpp103 id = SK_FIRST_CTN_PRE; in normalizeStringSkolem()
110 if (id == SK_FIRST_CTN_PRE) in normalizeStringSkolem()
H A Dskolem_cache.h95 SK_FIRST_CTN_PRE, enumerator
H A Dtheory_strings_preprocess.cpp125 d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); in simplify()
362 d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre"); in simplify()
H A Dtheory_strings.cpp510 d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1"); in doReduction()