search

VeriFIT / z3-noodler

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

Nielsen: model generation updates #166

Closed vhavlena closed 3 months ago

vhavlena commented 3 months ago

Adjustment of the Nielsen decision procedure to the new model generation interface.

vhavlena commented 3 months ago

The results are OK (tested on kepler). Below slow down compared to models off. 

# of formulae: 587
--------------------------------------------------
tool                                ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-model-aad2489-2756940   584     3   54.70   0.09   0.02   0.18    284      300          0     3         0        0
z3-noodler-7525ba0-2756940         584     3   15.70   0.03   0.01   0.07    284      300          0     3         0        0
cvc5-1.1.2                         347   240    0.54   0.00   0.00   0.00     50      297          0   240         0        0
z3-4.13.0                          278   309   25.95   0.09   0.02   0.90    135      143          0   283        26        0
--------------------------------------------------

image