search

VeriFIT / z3-noodler

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

Solver extension to handle underapproximation #129

Closed vhavlena closed 8 months ago

vhavlena commented 8 months ago

Lightweight extension of a solver to handle underapproximation in the string theory.

vhavlena commented 8 months ago

Restriction to conversions:

# of formulae: 17818
###################################################################################
####                                   Table 1                                 ####
###################################################################################
| method                     |    max |     mean |   median |   std. dev |   TO+MO+ERR |   unknowns |
|----------------------------|--------|----------|----------|------------|-------------|------------|
| z3-noodler-77f7c04-2cddb2f | 117.21 | 0.227874 |     0.01 |    2.45486 |         148 |        129 |
| cvc5-1.0.8                 |  82.08 | 0.295888 |     0.03 |    1.16243 |          29 |          2 |
| z3-4.12.2                  | 118.32 | 1.38219  |     0.04 |    7.66078 |         278 |          0 |
| cvc5-1.1.1                 |  74.58 | 0.260832 |     0.01 |    1.46495 |          34 |          2 |
| z3-4.12.5                  | 118.74 | 1.17092  |     0.01 |    6.86134 |         281 |          0 |
| z3-noodler-789525b-2cddb2f | 110.14 | 0.197812 |     0.01 |    2.39778 |         120 |        583 |