other updates:
- change signature of advance_qhead to simplify call sites
- have model reconstruction replay work on a tail of dependent_expr state, while adding formulas to the tail.
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
* Added limit to "visit" to allow detecting multiple visits
* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)
* Bugfix
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
* Added 64-bit "1" counting
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)
`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
Previously, we were only using std::hexfloat on Windows on VS2013
and later.
Since std::hexfloat is part of C++11 and we require C++11 to build
the Z3 library, this should be supported everywhere.
* Fix finding Python on Mac
On Mac you have to specify the version.
It also works well on other platforms this way.
* Ignore CMake build directories from index
* Fix warning about unused variable in release
The variable is used in debug only,
but it's legit that the compiler does not warn us for that in release.
