We are pleased to announce a new release of Alt-Ergo!
Alt-Ergo 2.4.0 is now available from Alt-Ergo’s website. An associated opam package will be published in the next few days.
This release contains some major novelties:
Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard.
We switched command line parsing to use cmdliner. You will need to use – instead of -. Some options have also been renamed, see the manpage or the documentation.
We improved the online documentation of your solver, available here.
This release also contains some minor novelties:
.mlw and .why extension are depreciated, the use of .ae extension is advised.
Add --input (resp --output) option to manually set the input (resp output) file format
Add --pretty-output option to add better debug formatting and to add colors
Add exponentiation operation, ** in native Alt-Ergo syntax. The operator is fully interpreted when applied to constants
Fix --steps-count and improve the way steps are counted (AdaCore contribution)
Add --instantiation-heuristic option that can enable lighter or heavier instantiation
Reduce the instantiation context (considered foralls / exists) in CDCL-Tableaux to better mimic the Tableaux-like SAT solver
Multiple bugfixes
The full list of changes is available here. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!
Do anybody know solvers which allow you to represent a backtracking history not as a stack (using push/pop commands) but as a tree? It seems mapping tree into a stack will be complicated, and pushing again all assertions will make calling a solver very slow… (If it is important I need only finite domain constraints with inequality. It will be cool to have order constraints but for now I can live without that)
A technique I have used is to assert all constraints under a propositional variable as a guard, where there is one guard per node of the backtracking tree you want. Then instead of using “check”, you can use “check_assumptions”. This keeps all the constraints in one single (huge) context, which might not be workable due to size. But it does allow jumping from branch to branch with much less overhead than sequences of pop and push.
I second that, push/pop can be slower and less convenient than using directly assumptions. Checking under assumptions, and returning an unsat core as a subset of these assumptions, is reasonably easy to implement for the solver, and typically very fast (e.g. in z3 it’s faster than using push/pop).
Internally (ie. in the CDCL SAT solver), push/pop are implemented with guards as described above, and check-sat becomes a check-sat-assuming [guards]. A pop command triggers the propagation of the associated guard to false (at level 0) without any extra cleaning.
(But some extra work is still needed on the binary side to take full advantage of these modifications in the lib. Some lifting of the internal representation of Alt-Ergo’s native input language is needed)
In addition to the push/pop command, Alt-Ergo also supports the check-sat-assuming command of the smt-lib standard that allow you to assume a list of propositional variable.