VeriFIT / z3-noodler

The Z3-Noodler String Solver
Other
6 stars 5 forks source link

Remove useless int variables for conversions #151

Closed jurajsic closed 3 months ago

jurajsic commented 3 months ago

In handling conversions to/from_int/code we created int variables that were not really used. For example for from_int(arg), we created a new variable i for arg, where we wanted to put arg=i. However, this did not work for some reason, so it was "fixed" by just remembering that i stands for arg during the decision procedure.

This PR then removes these int variables (i.e., they are not created as z3 variables, just as noodler ones, using them internally in the decision procedure) + these variables were used in axioms, however, as they were not connected, these axioms had no impact. They should have an impact now.

jurajsic commented 3 months ago

Results for benchmarks with conversions:

Benchmark stringfuzz
# of formulae: 1608
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-69644b5-d95fe13  1606     2   40.94   0.03   0.01   0.17    284     1322          1     1         0        0
z3-noodler-4bcf006-d95fe13  1605     3  137.39   0.09   0.01   2.57    283     1322          1     2         0        0
cvc5-1.1.2                  1579    29   24.92   0.02   0.01   0.07    284     1295          0    29         0        0
z3-4.13.0                   1565    43  289.57   0.19   0.01   3.71    286     1279          0    43         0        0
--------------------------------------------------

Benchmark str_small_rw
# of formulae: 80
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-69644b5-d95fe13    77     3    0.73   0.01   0.01   0.00      0       77          2     1         0        0
z3-noodler-4bcf006-d95fe13    78     2   95.74   1.23   0.01  10.76      1       77          2     0         0        0
cvc5-1.1.2                    78     2    0.04   0.00   0.00   0.00      1       77          2     0         0        0
z3-4.13.0                     78     2    0.66   0.01   0.01   0.01      1       77          0     2         0        0
--------------------------------------------------

Benchmark full_str_int
# of formulae: 16130
--------------------------------------------------
tool                           ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-69644b5-d95fe13  15944   186   1481.37   0.09   0.01   1.31   2285    13659        125    61         0        0
z3-noodler-4bcf006-d95fe13  15928   202   2524.81   0.16   0.01   1.20   2274    13654        128    74         0        0
cvc5-1.1.2                  16125     5   5049.25   0.31   0.01   1.46   2337    13788          0     5         0        0
z3-4.13.0                   15896   234  20197.59   1.27   0.01   7.07   2294    13602          0   234         0        0
--------------------------------------------------

image