[wip] major refactoring for perf and modularity

[c-cube]

• move to ~jbuilder~ dune
• style stuff
• migrate to 4.03
• cut into small sub-libraries
• use sequence
• make state explicit, remove stateful functors
• heavy perf improvements
• remove smt-related libs
• add sudoku solver to test the functor
• remove push/pop, replaced by faster assumptions-powered unsat-core

[Gbury]

Looks good (as long as the Travis check pass). Is there a reason for having filenames capitalized ? I usually keep all my folders/filenames lowcase because it's easier to type in the terminal (but it's not an absolute rule).

[Gbury]

Travis configuration and opam file should be updated to reflect the changes in ocaml versions

[c-cube]

I use capitalized file names these days, because it maps exactly to the module name. When using acronyms, if avoids having files named cNF.ml.

[c-cube]

Questions:

• why, in External, is solve calling pop then push? If there were local assumptions they will be lost…
• should we move all the test stuff into a new library msmt, with corresponding opam file? or is it just hidden?
  • if so, should we have a proper internal AST with hashconsing (I have several of those already)?

[Gbury]

In External, since the functions returned in the sat_state and unsat_state use the mutable state of the solver, if you pop after solving, these function will not work anymore. The curreent approach is correct because there are really only two states the solver should be in when using external:

• nothing happened, the solver is at level 0, thus popping does not do anything
• External.solve has been called previously, which left exactly one level of local assumptions to be popped. The assumption was that a user of External wouldn't use functions from Internal that could change the state of the solver. If you find a way to make it work without this assumption then all the better, that that would probably require some additional state to be remembered.

The test stuff is currently hidden (and ideally not part of what is installed), but it could indeed be moved to a separate library. I didn't make it visible because I felt the code wasn't really good enough, but feel free to improve it.

[c-cube]

I think the major changes are there. You might want to start by looking at the API changes, and if it's ok, then look into the code itself.

Note that in mc2 there are still some parts that I consider more elegant:

• the separation between values and terms
• conflict analysis: https://github.com/c-cube/mc2/blob/6f77e4f346fb676b262a4be194543958e61b278b/src/core/Internal.ml#L788 and below
• most of the proof post-processing (and types): https://github.com/c-cube/mc2/blob/6f77e4f346fb676b262a4be194543958e61b278b/src/core/Proof.ml

[timothee-haudebourg]

You have a msat.exe file that appeared and I don't think its supposed to be there.

[c-cube]

The msat.exe is convenient for running msat, is all.

Otherwise: this PR is a bit old, another pass might be useful to get it ready ot be merged I think.

[Gbury]

I'll try and do a serious review soon (as in in a few days, one week max). @c-cube do you think you'll have some time to address the potential comments ?

[c-cube]

I think so, yes. I'm spending too much time on my own fork (sidekick) but well.

[c-cube]

rebased

[c-cube]

Ugh, I hate travis -_-

[c-cube]

:tada: :tada: :tada: :taco: :fireworks: