Reglan equality fix for #96

[OliverMa1]

Add preprocessing for RegLan equality and an early fast path for fully ground str.contains expressions. These changes address failures (soundness and stack overflow) encountered in the 20250410-matching benchmarks from the nonincremental QF_S release.

[pruemmer]

I don't think this commit is doing quite the right thing. According to SMT-LIB, the RegLan sort is interpreted by the set of regex ground terms, without any normalization of expressions. That means that the following equation should evaluate to false?

  (= (re.union (str.to_re "a") (str.to_re "b"))
     (re.range "a" "b"))

[OliverMa1]

I am trying to understand this conflict a bit more. As far as I understand the semantics of RegLan is defined as:

⟦RegLan⟧ is the powerset of ⟦String⟧, the set of all subsets of ⟦String⟧.
Each subset can be seen as a language with alphabet UC.
Each variable-free term of sort RegLan denotes a regular language in ⟦RegLan⟧. (Taken from https://smt-lib.org/theories-UnicodeStrings.shtml)

Does this not mean that ⟦(re.union (str.to_re "a") (str.to_re "b"))⟧ = {a,b} = ⟦(re.range "a" "b")⟧?

[pruemmer]

Ok, yes, I think you are right. The description in the SMT-LIB theory is a bit inconsistent, this part is confusing:

:values 
 "The set of values for String is the set of all string literals; 
  for RegLan it is the set of all ground terms of that sort.
 "

But you are right that, further down in the semantics part, the interpretation of a regex term is the corresponding regular language!