diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-02 00:01:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-02 00:01:21 -0500 |
commit | aa6fb6fa3df0b1519e6763e72541c022396ab1dc (patch) | |
tree | c01a620079998579583150ef117c08b2db2318c4 /src/theory/strings/infer_info.h | |
parent | 3915eb7b497bd185385048f8c7f2b4c8f2bf7c03 (diff) |
Introduce enums for all string inferences, excluding the core solver (#4195)
Introduce enum values for all calls to sendInference outside of the core solver.
This included some minor refactoring.
Diffstat (limited to 'src/theory/strings/infer_info.h')
-rw-r--r-- | src/theory/strings/infer_info.h | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index e13a5a2ff..252445cb4 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -38,6 +38,31 @@ namespace strings { */ enum class Inference : uint32_t { + //-------------------------------------- base solver + // initial normalize singular + // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" => + // x1 ++ ... ++ xn = xi + I_NORM_S, + // initial constant merge + // explain_constant(x, c) => x = c + // Above, explain_constant(x,c) is a basic explanation of why x must be equal + // to string constant c, which is computed by taking arguments of + // concatentation terms that are entailed to be constants. For example: + // ( y = "AB" ^ z = "C" ) => y ++ z = "ABC" + I_CONST_MERGE, + // initial constant conflict + // ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false + // where c1 != c2. + I_CONST_CONFLICT, + // initial normalize + // Given two concatenation terms, this is applied when we find that they are + // equal after e.g. removing strings that are currently empty. For example: + // y = "" ^ z = "" => x ++ y = z ++ x + I_NORM, + // The cardinality inference for strings, see Liang et al CAV 2014. + CARDINALITY, + //-------------------------------------- end base solver + //-------------------------------------- core solver // Given two normal forms, infers that the remainder one of them has to be // empty. For example: // If x1 ++ x2 = y1 and x1 = y1, then x2 = "" @@ -94,6 +119,73 @@ enum class Inference : uint32_t // for fresh u, u1, u2. // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014. FLOOP, + //-------------------------------------- end core solver + //-------------------------------------- regexp solver + // regular expression normal form conflict + // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false + // where y is the normal form computed for x. + RE_NF_CONFLICT, + // regular expression unfolding + // This is a general class of inferences of the form: + // (x in R) => F + // where F is formula expressing the next step of checking whether x is in + // R. For example: + // (x in (R)*) => + // x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R) + RE_UNFOLD_POS, + // Same as above, for negative memberships + RE_UNFOLD_NEG, + // intersection inclusion conflict + // (x in R1 ^ ~ x in R2) => false where [[includes(R2,R1)]] + // Where includes(R2,R1) is a heuristic check for whether R2 includes R1. + RE_INTER_INCLUDE, + // intersection conflict, using regexp intersection computation + // (x in R1 ^ x in R2) => false where [[intersect(R1, R2) = empty]] + RE_INTER_CONF, + // intersection inference + // (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2)) + RE_INTER_INFER, + // regular expression delta + // (x = "" ^ x in R) => C + // where "" in R holds if and only if C holds. + RE_DELTA, + // regular expression delta conflict + // (x = "" ^ x in R) => false + // where R does not accept the empty string. + RE_DELTA_CONF, + // regular expression derive ??? + RE_DERIVE, + //-------------------------------------- end regexp solver + //-------------------------------------- extended function solver + // All extended function inferences from context-dependent rewriting produced + // by constant substitutions. See Reynolds et al CAV 2017. These are + // inferences of the form: + // X = Y => f(X) = t when rewrite( f(Y) ) = t + // where X = Y is a vector of equalities, where some of Y may be constants. + EXTF, + // Same as above, for normal form substitutions. + EXTF_N, + // contain transitive + // ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ). + CTN_TRANS, + // contain decompose + // str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or + // ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y ) + CTN_DECOMPOSE, + // contain neg equal + // ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s + CTN_NEG_EQUAL, + // contain positive + // str.contains( x, y ) => x = w1 ++ y ++ w2 + // where w1 and w2 are skolem variables. + CTN_POS, + // All reduction inferences of the form: + // f(x1, .., xn) = y ^ P(x1, ..., xn, y) + // where f is an extended function, y is the purification variable for + // f(x1, .., xn) and P is the reduction predicate for f + // (see theory_strings_preprocess). + REDUCTION, + //-------------------------------------- end extended function solver NONE, }; |