[native] Build native code from scratch

[pkriens]

Currently native libraries are included directly. We should build them from scratch.

Question: Is native code needed since sat4j seems to work very well?

[thedotmatrix]

Is this still an open question? If so, the following may be useful. Also, I may be able to assist with this enhancement.

First, this seems like two questions:

1. Are other SAT solvers needed since SAT4j seems to work very well?
2. Is native code support for other solvers required?

For # 1, I'd say yes, based on our preliminary user study findings. Having different solving strategies (solvers, or various options), can have a significant impact on the models a user ends up seeing, especially if they only look at the first few scenarios available in the stream. Performance can also greatly vary depending on the Alloy model and chosen solver / options.

For # 2, I would say there are better options, based on my experience extending Alloy/Kodkod. For our work modifying Alloy 4.2 to support alternative model streams and provenance, we extended the native interface for minisatProver. Modifying the JNI interface to expose more solver functions, and incorporating our changes into Kodkod's current SolverFactory was quite a bit of work; this also limited our ability to support other solvers immediately. However, most solvers now support standard languages, like SMT-LIB 2, and this is how I added basic support for z3 solving cnf in Alloy 5. The implementation is similar to the ExternalSolver / Output to CNF option, with an additional process call to the external solver, and a method to parse the resulting scenario from standard out. If Alloy 5 was to have sat4j be the only internal solver, the clunky SAT Factory pattern could be scraped, and replaced with a Solver Strategy pattern in the SolutionIterator, with an Adapter pattern for external solvers to properly call an executable/options (assumed installed separately) and parse the resulting scenario. This also encapsulates all scenario altering behavior beyond translation in a single class.

Hope this helps, Natasha Danas

[pkriens]

Will you do a Pull Request for Z3? Would love to include this!

I had come to the same conclusions regarding the solvers. We need a SolverFactory and then register this using the Java services model.

[aleksandarmilicevic]

I'd welcome that PR too.

Regarding # 2: I agree that using SMT-LIB 2 to communicate with an external solver is much nicer than using JNI. That said, making Sat4J as the only internal solver has the problem of requiring people who want good performance to install native solvers manually. Personally, I would be perfectly fine with that; in practice, however, for some users that would be nothing but an unpleasant inconvenience.

[thedotmatrix]

As to your comment on my prototyping fork, yes the command / standard out parsing are the only solver specific behaviors, in what otherwise is an abstract external SMT-LIB-2 class.

As @tnelson and I move our Amalgam features (additional solver support, alternative solution iteration strategies, provenance) into Alloy 5, we can submit pull requests when applicable.

I agree with your concern re: my # 2, and I think I may have a decent solution. Replace the JNI/shared library support code with wrapper executables that consume an SMT-LIB-2 spec, call the appropriate shared object functions, and produce solutions. This solver execution method would afford the same brittleness as the current JNI/C++ code. I believe the code reduction in Alloy and Kodkod would be quite significant. Building these executables with gradle would be no more work than building the shared objects themselves. And then the Alloy/Kodkod core would be two compilers that only produce an SMT-LIB-2 spec.

This viewpoint comes from a long painful experience getting our modified Alloy from the aforementioned paper (and minisat prover) built on all three major platforms to pass our conference's artifact evaluation. Though I understand this viewpoint may not align with the future of Alloy, which I'm looking forward to hearing more about soon.

[pkriens]

I am currently working on a much more abstract API. I am following a 'reversed' strategy. That is, I am making the API as good as possible and then map that currently back to the existing codebase, doing conversions where necessary. It might be easiest to plugin the new SMT solvers into the new API while still supporting all the current stuff. (Forty years of experience with attempted big bangs ...)

I have a question here. Do we need an intermediate layer between the AST and the solvers? Looking at the Kodkod translation I got the feeling that an intermediate representation for the relations + constraints would make the mapping for the lower level solvers a lot easier and would reduce the 'interface surface' between the solvers and the AST? This would make it easier to add solvers since they would not have to interpret the AST itself to construct the relations and constraints?

Anyway. This approach would allow testing and command lines. We should then do the grunt work of changing the UI to use the new API, this will be some serious work.

[thedotmatrix]

Thanks for the info here and in your reply to Tim. What I was suggesting, in essence, is an intermediate layer between the AST and the solvers, in the form of SMT2 as a target language. Kodkod sort of has an API targeting cnf, which does not capture the expressive power of modern solvers many Alloy modifications may want to use, but the real issue is the API not the target language. The new API will most likely solve the frustrations with the current interface to support all solvers, making the task of extending from cnf to SMT2 trivial.

[pkriens]

I am not sure if SMT2 is sufficient? If we chose that as intermediate layers, do we not exclude solvers like Minisat that only support SAT?

I am going to be in Boston for the workshop. Will you be there? Might be an interesting and important topic.

[thedotmatrix]

Yes, that's true; my previous comment stated the target language choice does not impact me as long as the API improves (since cnf is an expressive subset of SMT2).

I am hoping to make it to the workshop. Worst case scenario, my colleague Tim will be there.

[pkriens]

Hope you'll be there ...