CODEWITHSUNDEEP
z3smtz3py
Ilya Zlatkin
Ilya Zlatkin

Reputation: 86

How can smt2 file be optimised?

Is any way how I can read smt2 file and optimize it somehow? Decrease number of lines, remove unnecessary conditions etc.

Upvotes: 0

Views: 268

Answers (1)

alias
alias

Reputation: 30450

Your question is rather vague, and it's not clear exactly what this "optimization" would do. Reducing the size of a file hardly serves any purpose, so I presume you actually mean getting a "simple" but "equi-satisfiable" smt2 description. That is, the "optimized" file would have the exact same sat/unsat status, with the exact same models as the original; but somehow "simpler."

If that's the case, you really need to be very clear about what "simpler" means. Simpler as in "easier to solve"? Simpler as in "easier to read for humans"?

Assuming you mean "easier to solve" (which is the interesting case I believe), then what you're asking for is how to determine if two sets of constraints are equi-satisfiable; which in general is an NP-complete problem. So, no; there won't be an easy way to do this. Can you drop "redundant" assertions: Sure, but that'd mean you need to find what those are, and that'll be a costly analysis of the benchmark itself.

So, without knowing any further detail and specifying what "optimize" means, the answer is a simple "no, there's no easy way." But each case is different, and different domains (for instance integer-difference logic) might make it easier to spot unnecessary constraints. You'll really have to be very specific about what you mean by optimizing to get a better answer.

Upvotes: 2

Related Questions