to_int/from_int optimization

[jurajsic]

I added different handling for the part that contain some non-digit during the creation of LIA formula for to_int/from_int so that only the part of the language with words containing only digits must be finite.

[jurajsic]

Impact on stringfuzz (nearly no impact on other benchmarks):

Benchmark stringfuzz/to120.csv
# of formulae: 11618
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-7421e81-2cddb2f  11347   271   0.03   0.01    291.77   6165     5182        266     5         0        0
cvc5-1.1.1                  10522  1096   2.65   0.00  27893.23   5756     4766          0  1095         1        0
z3-4.12.5                   11072   546   4.09   0.01  45283.01   5986     5086          0   421       125        0
z3-noodler-147a0e0-fb6e2b1  10574  1044   0.02   0.01    264.03   6087     4487       1044     0         0        0
--------------------------------------------------

[Adda0]

I cannot see anything wrong. But I only skimmed the code. I am too ill to do a proper review.

[Adda0]

Typo

Suggested change

	} // "else" part is not needed, that should be solved by setting "|s_i| = |w_i|" and by using the forula from function get_formula_for_code_subst_vars()
	} // "else" part is not needed, that should be solved by setting "|s_i| = |w_i|" and by using the formula from function get_formula_for_code_subst_vars()

[jurajsic]

Fixed in the next PR

[jurajsic]

Ok, I will merge it for now, @vhavlena can look at it after he comes back (if he wants).