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 D | theory_strings_skolem_cache_black.h | 61 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 D | skolem_cache.cpp | 103 id = SK_FIRST_CTN_PRE; in normalizeStringSkolem() 110 if (id == SK_FIRST_CTN_PRE) in normalizeStringSkolem()
|
H A D | skolem_cache.h | 95 SK_FIRST_CTN_PRE, enumerator
|
H A D | theory_strings_preprocess.cpp | 125 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 D | theory_strings.cpp | 510 d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1"); in doReduction()
|