search

ddsmt / ddSMT

A delta debugger for SMT benchmarks in SMT-LIB v2.
https://ddsmt.readthedocs.io
Other
50 stars 17 forks source link

Invalid `declare-sort` output? #35

Closed someplaceguy closed 7 months ago

someplaceguy commented 7 months ago

It seems that according to the SMT-LIB v2.6 standard, ddsmt v2.0.3 is outputting declare-sort commands with invalid syntax, e.g.:

(declare-sort t)

... instead of:

(declare-sort t 0)

I was wondering if this is expected or whether I'm missing something?

It doesn't seem to be a blocking issue for me because Z3 still seems to accept it, but it's still annoying because I'm doing work on an existing SMT-LIB parser that doesn't support this non-standard syntax and I'm not sure that this should be fixed in the parser rather than in ddsmt...

nafur commented 7 months ago

Hi, thanks for using ddsmt! The mutants that ddsmt generates may very well not be SMT-LIB compliant, as ddsmt only has a very limited understanding of SMT-LIB that is only used in an ad-hoc fashion. We generally assume that inputs that are syntactically invalid are rejected by solvers very quickly and it's thus not worth doing these checks on our side. Furthermore, doing so would restrict ddsmt to inputs that compliant in the first place, which was one of the limitations of the initial ddsmt implementation. This can, of course, also mean that we start with a compliant input and then modify it to be non-compliant but accepted by the solver.

In this particular case, I guess z3 was used as solver, ddsmt tried to simply remove the 0 and z3 accepted that. You could try to add (set-option :smtlib2_compliant true) (found here) which might make z3 reject this change. Note, though, that you should figure out how to set this option via the command line, otherwise ddsmt will first remove the set-option command and then remove the 0...

someplaceguy commented 7 months ago

Ah, I see. That makes sense.

I will close this issue, then. Thank you!