ddsmt / ddSMT

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

Mutator to erase entries from "declare-datatypes" and "define-funs-rec" #26

Closed krobelus closed 3 years ago

krobelus commented 3 years ago

Hi, I have written this some time ago to reduce some of my formulas that use those recursive definitions. I'm not sure if it fits in well with the rest of the mutators.


This allows to reduce a file like

(define-funs-rec ((a () Bool) (b () Bool) (c () Bool)) (true false (or a b)))
(assert (= a b))
(check-sat)

where "c" is not relevant. The generic "erase" mutator doesn't work because we also need to remove the definition of "c" - in this example "(or a b)".

nafur commented 3 years ago

This looks like a good start for some other mutators for datatypes that have been on my todo list for quite a while. Thank you very much for this contribution!