summaryrefslogtreecommitdiff
path: root/src/theory/strings/skolem_cache.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/skolem_cache.h')
-rw-r--r--src/theory/strings/skolem_cache.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index c1e3c7214..f91b3cd9f 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -112,6 +112,10 @@ class SkolemCache
// k(x) is the end index of the x^th occurrence of b in a
// where n is the number of occurrences of b in a, and k(0)=0.
SK_OCCUR_INDEX,
+
+ SK_STOI_U,
+ SK_STOI_US,
+ SK_STOI_UD,
};
/**
* Returns a skolem of type string that is cached for (a,b,id) and has
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback