diff options
Diffstat (limited to 'src/theory/strings/eqc_info.h')
| -rw-r--r-- | src/theory/strings/eqc_info.h | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h index 1fd430c95..bfc753989 100644 --- a/src/theory/strings/eqc_info.h +++ b/src/theory/strings/eqc_info.h @@ -62,17 +62,34 @@ class EqcInfo context::CDO<unsigned> d_cardinalityLemK; context::CDO<Node> d_normalizedLength; /** - * A node that explains the longest constant prefix known of this + * If this is a string equivalence class, this is + * a node that explains the longest constant prefix known of this * equivalence class. This can either be: * (1) A term from this equivalence class, including a constant "ABC" or * concatenation term (str.++ "ABC" ...), or * (2) A membership of the form (str.in.re x R) where x is in this * equivalence class and R is a regular expression of the form * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...). + * + * If this is an integer equivalence class, this is the lower bound + * of the value of this equivalence class. + */ + context::CDO<Node> d_firstBound; + /** same as above, for suffix and integer upper bounds. */ + context::CDO<Node> d_secondBound; + /** + * Make merge conflict. Let "bound term" refer to a term that is set + * as the data member of this class for d_firstBound or d_secondBound. + * This method is called when this implies that two terms occur in an + * equivalence class that have conflicting properties. For example, + * t may be (str.in_re x (re.++ (str.to_re "A") R2)) and prev may be + * (str.++ "B" y), where the equivalence class of x has merged into + * the equivalence class of (str.++ "B" y). This method would return + * the conflict: + * (and (= x (str.++ "B" y)) (str.in_re x (re.++ (str.to_re "A") R2))) + * for this input. */ - context::CDO<Node> d_prefixC; - /** same as above, for suffix. */ - context::CDO<Node> d_suffixC; + static Node mkMergeConflict(Node t, Node prev); }; } // namespace strings |