diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-17 15:40:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-17 15:40:28 -0500 |
commit | d2b692cb2c054199d75a05f0f700e54fcb4f6c3c (patch) | |
tree | ce69ae1d1d547d48cf771896410208061949049e /src/theory/strings/skolem_cache.h | |
parent | c90b5b15ca93e64683c2bbf85def8d7afb4edab8 (diff) |
More aggressive skolem caching for strings, document and clean preprocessor (#2478)
Diffstat (limited to 'src/theory/strings/skolem_cache.h')
-rw-r--r-- | src/theory/strings/skolem_cache.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 2984ccfe4..c9b9fbe5a 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -42,9 +42,13 @@ class SkolemCache * * The skolems with _REV suffixes are used for the reverse version of the * preconditions below, e.g. where we are considering a' ++ a = b' ++ b. + * + * All skolems assume a and b are strings unless otherwise stated. */ enum SkolemId { + // exists k. k = a + SK_PURIFY, // a != "" ^ b = "ccccd" ^ a ++ "d" ++ a' = b ++ b' => // exists k. a = "cccc" + k SK_ID_C_SPT, @@ -78,12 +82,30 @@ class SkolemCache SK_ID_DEQ_X, SK_ID_DEQ_Y, SK_ID_DEQ_Z, + // contains( a, b ) => + // exists k_pre, k_post. a = k_pre ++ b ++ k_post ^ + // ~contains(k_pre ++ substr( b, 0, len(b)-1 ), b) + SK_FIRST_CTN_PRE, + SK_FIRST_CTN_POST, + // For integer b, + // len( a ) > b => + // exists k. a = k ++ a' ^ len( k ) = b + SK_PREFIX, + // For integer b, + // b > 0 => + // exists k. a = a' ++ k ^ len( k ) = ite( len(a)>b, len(a)-b, 0 ) + SK_SUFFIX_REM, }; /** * Returns a skolem of type string that is cached for (a,b,id) and has * name c. */ Node mkSkolemCached(Node a, Node b, SkolemId id, const char* c); + /** + * Returns a skolem of type string that is cached for (a,[null],id) and has + * name c. + */ + Node mkSkolemCached(Node a, SkolemId id, const char* c); /** Returns a (uncached) skolem of type string with name c */ Node mkSkolem(const char* c); /** Returns true if n is a skolem allocated by this class */ |