* Added function to select the next variable to split on
* Fixed typo
* Small fixes
* uint -> int
* Fixed missing assignment for binary clauses
* Added missing decide-callback for tactics
Add Z3_enable_concurrent_dec_ref to the API.
It is enables behavior of dec_ref functions that are exposed over the API to work with concurrent GC. The API calls to dec_ref are queued and processed in the main thread where context operations take place (in a way that is assumed thread safe as context operations are only allowed to be serialized on one thread at a time).
The idea is to set _concurrent_dec_ref from the API
(function not yet provided externally, but you can experiment with it by setting the default of m_concurrent_dec_ref to true).
It then provides concurrency support for dec_ref operations.
\brief convert p == 0 into a solved form v == r, such that
v has bounds [lo, oo) iff r has bounds [lo', oo)
v has bounds (oo,hi] iff r has bounds (oo,hi']
The solved form allows the Grobner solver identify more bounds conflicts.
A bad leading term can miss bounds conflicts.
For example for x + y + z == 0 where x, y : [0, oo) and z : (oo,0]
we prefer to solve z == -x - y instead of x == -z - y
because the solution -z - y has neither an upper, nor a lower bound.
The Grobner solver is augmented with a notion of a substitution that is applied before the solver is run.
For Grobner we want to preserve directions of intervals for finding sign conflicts. This means that it makes sense to have external control over linear solutions.
* 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.
Deadlock/Race is as follows:
1. get_task() reads m_shutdown == false and enters loop body
2. shutdown() is called; sets m_shutdown = true
3. shutdown() calls m_cond.notify_all()
4. get_task() finds no task in try_get_task()
5. get_task() calls m_cond.wait(), missing the notification
6. solve() waits forever on join()
Provided patch wraps (2) and (3) with the condition variable lock so that
step (5) cannot miss the notification.
Co-authored-by: Anthony Romano <anthony@forallsecure.com>
* Use int64 for ocaml api functions that require it
Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
* Use elif
Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2.
The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct.
The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2.
