Is there an incremental Max-SMT solver?

Question

I'm working with a problem over Bit-Vector arrays encoding logical relationships between different time series data at different timescales to generate synthetic data with arbitrary properties. I have found that I do best by incrementally providing the constraints for each time step rather than having Z3 assign them all at once, but it still is very time consuming. I was wondering if it would be possible to use Max-SMT to deal with this by explicitly stating that previous time series assignments should be kept the same as much as possible, and in addition by returning the closest possible model if a certain time threshold is reached and an exact solution isn't found. However, I don't think Z3 provides the combination of incrementality and Max-SMT. In addition, I don't think it's possible to get Z3 to provide "the closest model possible" in solver mode.

Does anyone know of a tool which does provide those functions?

Thanks!

Answer 1

It's true that z3's optimizer is not incremental. Nor it supports any notion of "close-enough possible." (Although you can query some internal values to glean ranges, they aren't guaranteed to even satisfy your constraints.)

I'll defer to @PatrickTrenton for the exact capabilities, but you might want to look into OptiMathSAT: http://optimathsat.disi.unitn.it/. Quoting from their web page:

OptiMathSAT allows for incremental multi-objective optimization over linear arithmetic objective functions, it supports a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, arrays).