* Added user propagator example
* User propagator example code refactoring
(+ removed unused parameter warning)
* Moved user-propagator example to its own directory
Since doxygen 1.8.16, opening and closing a group must not be done as
C comment but as doxygen command. In other words, not one but two
asterisk characters are required so that doxygen finds a group.
* feat(api/ml): use custom block hints to guide the GC
this forces the GC to collect garbage when a few _large_ objects
(solver, etc.) are dead. The current code would let arbitrarily many
such objects die and not trigger a GC (which would have to come from
OCaml code instead)
* tuning
* try to use caml_alloc_custom_mem with fake sizes
* try to fix leak by explicitly finalizing OCaml context
* chore: use more recent ubuntu for azure CI
* remove finalizer causing segfault in example
* split sat2goal out of goal2sat
These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.
I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.
* limit solver_core methods to those needed by goal2sat
And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.
I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.
generation of escape sequences for output was not handling non-printable character ranges correctly and also not offsetting hexadecimal characters right.
@zwimer: I had to remove a different move constructor before in the same API due to a different bug that the coverage tool exposed. I was unable to reproduce the bug reported in #5493 in my environment, but the interaction with reference counting and move constructors is sufficiently opaque that I rather not have to fix more bugs introduced with move constructors in the API. I am therefore removing also this use of && and maybe this fixes#5493
This adds a String overload for AssertSoft.
Previously only integer weights could have been used,
limiting the user. With Strings the user can now use
e.g. Java's BigInteger class converted to a String instead.
