How can I execute delta debugging for formula that takes 10s to solve?

[whangdo]

Greetings,

Recently, I've been trying delta debugging on a formula that SMT solver took more than 10 seconds to solve. In other words, if there is a formula that takes more than 10 seconds for the solver to solve, I wanted to transform it into as small a form as possible while maintaining its properties (which take more than 10 seconds to solve). I'm trying to use your tool ddSMT however, I do not know how to achieve what I wanna do. I looked at the document file, but I couldn't understand it well. If you are okay, could you let me know what to do?

Thanks for reading.

[nafur]

To achieve this, you need to write a custom wrapper script that returns (for example) 0 if the solver takes more than 10 seconds and 1 if it takes less than 10 seconds. I'd recommend you start with the compare_time.py from here, remove solver B from it and only look at the runtime of A for the exit code in the end (i.e. dur["A"]). This should do the job.

[whangdo]

@nafur First of all, thanks for your answer! To be honest, I want more detailed information. I had seen a document about compare_time.py and I tried to execute delta-debugging for my objective following your suggestion. However, I still don't get it.

I don't get your explanation perfectly, but I tried something. What I tried is as follows: I changed solvers A into target solver and option. Also, I converted subprocess to execute the target solver in foreground to count seconds while the solver solves a target formula. And I saw the following result.

A -> 10.012523853220046
Factor: 1.0
-> 0

It was done with 0 just. It was expected cause I didn't set a path to save a result of delta-debugging. I think I need information more to do what I wanna do. If you are okay, could you let me know more information?

[nafur]

Sure. I assume you have read the quickstart, at least the first section. The important point here is that you need to come up with an executable that has a specific exit code if and only if the solver is slow (>10s). To do that, we use a wrapper script around the actual solver. The compare_time.py does something similar: it runs two solvers and decides whether one solver is significantly slower than the other. I pointed you to this script, because it has the infrastructure in place (running a solver, getting it's output, looking at the runtime, dealing with solvers acting in weird ways). I'm not entirely sure what you did concerning running the target solver in foreground. What I think you need to do is replace the lower part of the script (everything after the for loop) by a simple

if dur['A'] > 10:
    sys.exit(1)
else:
    sys.exit(0)

With these changes, simply running ddsmt with this (modified) script as solver should minimize your input, keeping the solver runtime above 10s. As a final comment: any timing-related delta-debugging is somewhat fragile. It might happen that the solver runs a bit faster once (e.g. because of caching or whatever) leaving you with an smt2 file that will take slightly less than 10s in any subsequent calls. It's a bit hard to explain, but you'll see what I mean once you do this a few times :-)

[whangdo]

@nafur Thanks for your kindness, I get it right!