3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Commit graph

19638 commits

Author SHA1 Message Date
Nikolaj Bjorner
792ffeeda7 fix latent sign bug 2025-04-23 17:22:57 -07:00
Nikolaj Bjorner
fe1fff3b7e add scaffolding for experiments with slack 2025-04-23 17:07:50 -07:00
Nikolaj Bjorner
12ccf59ab9 rename fields to compile on c++ platforms 2025-04-23 17:06:15 -07:00
Nikolaj Bjorner
e41acd7b50 convert m_r_upper and m_r_lower bounds to plain vectors
manage backtracking state together with backtracking of column data.
2025-04-23 16:33:38 -07:00
Nikolaj Bjorner
fae60946bf consolidate some bounds references 2025-04-23 15:45:44 -07:00
Nikolaj Bjorner
f6fbeda9d7 fix #7629 2025-04-23 15:22:44 -07:00
Nikolaj Bjorner
7641393f8a use inlined functions 2025-04-23 14:28:31 -07:00
Nikolaj Bjorner
5cc57b8958 coalesce updates to bounds 2025-04-23 14:05:17 -07:00
Nikolaj Bjorner
579ba8bd70 add power axioms to arith_solver 2025-04-23 10:48:29 -07:00
Nikolaj Bjorner
d73d104ded remove overwriting x,y,rval 2025-04-23 09:17:22 -07:00
Nikolaj Bjorner
ff920ba51b handle root expressions, and checking exponentiation with nlsat
this one is for you @matthai
2025-04-22 13:47:47 -07:00
Carson Radtke
2fe2735b5e
Replace _DEBUG with Z3DEBUG (#7628)
Fixes https://github.com/Z3Prover/z3/issues/7627
2025-04-22 13:39:01 -07:00
Lev Nachmanson
a1673f2bdd fallback to Gomory cuts and gcd conflicts if dio fails
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-21 17:10:32 -07:00
Nikolaj Bjorner
cc1bb0a255 remove superfluous makefile
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:56:30 -07:00
Nikolaj Bjorner
17cac7d87c provide shortcut to command-line version to retrieve parameters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:51:08 -07:00
Nikolaj Bjorner
6e88d91214 add badge for ocaml cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:46:40 -07:00
Nikolaj Bjorner
3761dd869a address build warning with overloaded virtual operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-04-19 13:42:11 -07:00
Shiwei Weng 翁士伟
f7aec02503
WIP: Migrating OCaml binding to CMake (#7254)
* Update doc for `mk_context`.

* Migrating to cmake.

* Migrating to cmake. It builds both internal or external libz3.

* Start to work on platform-specific problem.

* Messy notes.

* debug.

* Cleanup a bit.

* Fixing shared lib extension.

* Minor.

* Resume working on this PR.

* Remove including `AddOCaml`.

* Keep `z3.ml` and `z3.mli` in the src but specify the generated file in the bin.

* Keep `ml_example.ml` in the src.

* Try github action for ocaml.

* Add workflow using matrix.

* Fix mac linking once more.

* Bypass @rpath in building sanity check.
2025-04-19 13:41:27 -07:00
Lev Nachmanson
ab9f3307d6 change the default of running dio to true, and running gcd to false, remove branching in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
dbde713eb3 remove testing code in is_big_term_on_no_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
1131d5294d fix a bug in tracking the changes in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
d289495ca4 allow gcd when dio ignores some terms
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
17af18fe31 make gcd call in dio optional
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
436eefbce2 always remove the tightened term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
dc7185d0a4 change the name of m_changed_columns to m_changed_f_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
32e77d8214 typo
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
cb1818f4b8 reject more terms with big numbers
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
1cde40bddb dio_calls_period=4 2025-04-18 18:24:50 -07:00
Lev Nachmanson
87e2ce8948 Update lp_settings.h - m_dio_calls_period = 4 2025-04-18 18:24:50 -07:00
Lev Nachmanson
59edb81f86 Update lp_settings.cpp
white space change
2025-04-18 18:24:50 -07:00
Lev Nachmanson
8db9f52386 add parameter m_dio_calls_period
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
ae97ee09d9 throttle dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
972f80188a throttle dio for big numbers
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
Lev Nachmanson
3e49d9fcfe reuse dio branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-04-18 18:24:50 -07:00
mikulas-patocka
e31e9819b1
Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling (#7619)
Add this option, so that the z3 library can be used in programs that do
signal handling on their own.

Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
2025-04-18 10:34:54 -07:00
Nikolaj Bjorner
ed5dd26bb7 remove non-working ts mcp server, settle with python variant 2025-04-18 10:10:12 -07:00
Nikolaj Bjorner
741cb5c3b5 minimal z3 MCP server 2025-04-18 10:00:04 -07:00
Nikolaj Bjorner
f63c9e366f disable assignment for param_descrs 2025-04-17 17:29:09 -07:00
Nikolaj Bjorner
3f73c8b18f stab at SMTLIB REL mcp server 2025-04-17 17:23:09 -07:00
Nikolaj Bjorner
755f57931b fix #7622 2025-04-17 11:05:49 -07:00
Nikolaj Bjorner
81f10912ae remove unused bdd based variable elimination 2025-04-14 16:07:41 -07:00
Nikolaj Bjorner
e41090df83 fix #7602
add missing relevancy propagation so that relationship between rel and TC(rel) are not lost to the theory solver.
2025-04-14 15:38:22 -07:00
Nikolaj Bjorner
8035edbe65 remove lp_assert 2025-04-14 11:10:26 -07:00
Nikolaj Bjorner
1510b3112e fix build warnings 2025-04-14 10:34:09 -07:00
Kyle Bloom
5ad79f2864
Add Iterators as acceptable arguments to functions (#7620) 2025-04-12 10:32:56 -07:00
mikulas-patocka
6ecc7a2dd4
Fix a race condition in scoped_timer::finalize (#7618)
scoped_timer::finalize is called from fork. However, it may race with
other threads creating or freeing timer threads.

This patch removes the loop in scoped_timer::finalize (because it is not
needed and it may spin) and also removes two unlocked assignments.

The idle thread is added to "available_workers" in
scoped_timer::~scoped_timer destructor.

If we call the "finalize" method as a part of total memory cleanup, all
the scoped_timers' destructors were already executed and all the worker
threads are already on "available_workers" vector. So, we don't need to
loop; the first loop iteration will clean all the threads.

If the "finalize" method is called from single-threaded program's fork(),
then all the scoped timers' destructors are already called and the case
is analogous to the previous case.

If the "finalize" method is called from multi-threaded program's fork(),
then it breaks down - the "num_workers" variable is the total amount of
workers (both sleeping and busy), and we loop until we terminated
"num_workers" threads - that means that if the number of sleeping workers
is less than "num_workers", the function just spins.

Then, there is unlocked assignment to "num_workers = 0" and
"available_workers.clear()" that can race with other threads doing z3
work and corrupt memory. available_workers.clear() is not needed, because
it was already cleared by std::swap(available_workers, cleanup_workers)
(and that was correctly locked).

Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
2025-04-11 08:08:27 +01:00
Nikolaj Bjorner
a83efa68eb spacing 2025-04-09 20:24:09 -07:00
Nikolaj Bjorner
8138829231 fix #7616 2025-04-09 20:24:09 -07:00
Josh Berdine
d792840739
Add Z3_is_recursive_datatype_sort to the API (#7615)
It does not seem to be possible to test if a datatype sort is recursive.
2025-04-08 14:36:57 -07:00
Mark Ryan
14e2aadad0
include LICENSE.txt in wheels (#7614)
Update setup.py so that we copy LICENSE.TXT to src/api/python before
creating the sdist.  Any wheels built from this sdist will now
contain the LICENSE.txt file.

Fixes #7604
2025-04-07 08:41:50 -07:00