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.
This update allows the python bindings for user-propagator to handle functions that are declared to be registered with the user propagator plugin. It fixes a bug in UserPropagateBase.add to allow registering terms dynamically during search.
It also fixes a bug in theory_user_propagate as scopes were not fully pushed when the solver gets the callbacks for new equalities and new disequalities.
It also adds equality and disequality interfaces to the sat/smt solver version (which isn't being exercised in earnest yet)
* 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.
expression pointers were changed within a function, but not pinned. So the pointers got stale. To enforce their life-time within the function body (for use in logging) pin the expressions.
recfun decl plugin does not get copied so recursive functions are lost when cloning.
Fix is risky and use case is limited to threads + recursive definitions
Adding new API object to maintain state between calls to parser.
The state is incremental: all declarations of sorts and functions are valid in the next parse. The parser produces an ast-vector of assertions that are parsed in the current calls.
The following is a unit test:
```
from z3 import *
pc = ParserContext()
A = DeclareSort('A')
pc.add_sort(A)
print(pc.from_string("(declare-const x A) (declare-const y A) (assert (= x y))"))
print(pc.from_string("(declare-const z A) (assert (= x z))"))
print(parse_smt2_string("(declare-const x Int) (declare-const y Int) (assert (= x y))"))
s = Solver()
s.from_string("(declare-sort A)")
s.from_string("(declare-const x A)")
s.from_string("(declare-const y A)")
s.from_string("(assert (= x y))")
print(s.assertions())
s.from_string("(declare-const z A)")
print(s.assertions())
s.from_string("(assert (= x z))")
print(s.assertions())
```
It produces results of the form
```
[x == y]
[x == z]
[x == y]
[x == y]
[x == y]
[x == y, x == z]
```
Thus, the set of assertions returned by a parse call is just the set of assertions added.
The solver maintains state between parser calls so that declarations made in a previous call are still available when declaring the constant 'z'.
The same holds for the parser_context_from_string function: function and sort declarations either added externally or declared using SMTLIB2 command line format as strings are valid for later calls.
remove option for uzers (users who are in reality fuzzers) to toggle flat option. The legacy arithmetic solver bakes in assumptions about flat format so it isn't helpful to expose this to fuzzers, I mean uzers.
* make JS api more idiomatic
* make JS api type-safe by default
* use strings, not symbols, for results
* add toString
* add miracle sudoku example
* ints should be ints
* add error handling
* add missing Cond to Context
* fewer side-effecting getters
remaining perf bug is dealing with very large bit-widths. mod 2^n should be computed natively based on n instead of 2^n because we pre-populate an array with all values up to n. Suppose n is 10000, the array has size 10000.
