Upstream requirements for CVC4?

[chadbrewbaker]

I've been tasked with creating more robust C/C++ bindings for CVC4. End goal of getting CVC4 JNI bindings more robust, but helping out sbv along the way would be a good side effect.

As a CVC4 C API consumer, what features are missing that you enjoy from Z3 etc? In terms of passing the ASTs and references to internals; implementing new solvers is out of scope.

[chadbrewbaker]

For reference:

https://github.com/Z3Prover/z3/tree/master/src/api https://github.com/CVC4/CVC4/tree/master/src/bindings/compat/c

At first glance Z3 has the C headers broken down into smaller chunks instead of one monolithic file.

[chadbrewbaker]

It seems sbv is currently just shelling out to the solvers using SMT-LIB syntax? Is there a benchmark that would serve as a baseline upper bound on how much time would be saved in passing the SMT-LIB AST in binary format? Perhaps logging the time it takes for sbv to pretty print the SMT formulas to a buffer, and on the solver side how long it takes to read them from the buffer into an AST?

[LeventErkok]

@chadbrewbaker That is correct; SBV generates SMT-Lib and calls the underlying solver via a named pipe. In my experience, the construction of the SMTLib string isn't usually the bottleneck. Symbolic simulation and the actual solver time dominate in majority of cases. With the way SBV is architected, it would be very low ROI to go to a programmatic interface.

@robdockins @brianhuffman might have some benchmarks for you though. SBV is used as the prover backend for Cryptol (http://github.com/GaloisInc/cryptol) and I do recall they did have some cases when the generated SMT-Lib was rather large and it consumed a nontrivial amount of time. @robdockins in particular did some optimizations to SBV to remedy those cases, but maybe there's still something to be squeezed out.

[chadbrewbaker]

That would be great! I'm instrumenting CVC4 and Z3 to tease out their SMT parse times; generating some Criterion comparisons.

How far is Eta (Haskell on JVM) from supporting SBV? If Eta support is still a ways off, and SMT-LIB parsing turns out to be insigificant I might just port SBV to Java and call it a day.

[LeventErkok]

I never tried Eta myself; I'd be interested to know if it can compile SBV.

I don't understand your commend about "port SBV to Java." I'm sure there are Java based interfaces already.

Honestly, I don't see much ROI for SBV moving to an API based interface for CVC4. What would be interesting is if SMT-Lib supported a "fixed" set of APIs that all the solvers supported. The API can be in C/Haskell/Java.. whatever; and that way tools like SBV that try to be solver agnostic can simply go through that interface. Then CVC4/Z3/Yices etc. can all support that API. But I'm not sure if that's your goal.

[chadbrewbaker]

Port as in use similar abstractions for wrapping the z3/cvc4 ... SMT-LIB shell utilities.

A generic C interface for SMT-LIB2 utilities might be the end product, and there is some support from the SMT-LIB2 language maintainers so it could happen. All of the current tools seem to be shell wrappers like SBV, or SMT-LIB2 parsers: http://smtlib.cs.uiowa.edu/utilities.shtml

[chadbrewbaker]

According to the Eta maintainer the biggest modification to get SBV running on the JVM is mitigating GHC dependencies. https://github.com/typelead/eta/issues/216

[LeventErkok]

@chadbrewbaker I'm closing this ticket as I don't think there's any actionable item on the SBV side for the time being. Feel free to re-open it as necessary.