* 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.
* Remove size argument in OCaml's `Z3.mk_re_intersect`
Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern.
* Enable the ocaml documentation in Seq.
Turn all the comments into proper documentation comments.
* Fix flake8 violations in z3.py
* Fix flake8 violations in z3printer.py
* Fix flake8 violations in z3rcf.py and z3util.py
* do not allocate list on every call to set_default_rounding_mode
* reformat python code using autopep8
* manually wrap some too long lines and adjust some checks
* run autopep8 in aggressive mode
* run autopep8 in very aggressive mode
* manually reformat z3types.py
* unify: use double quotes
* use sys.version_info instead of sys.version
* drop accidentally commited src/util/z3_version.h
