mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-11 17:54:43 +00:00
Code Activity
19660 commits 25 branches 49 tags 159 MiB
Commit graph

19660 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
fe0807f21a testing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-09 16:33:00 -07:00
Lev Nachmanson
11a35d109b trying randomly shuffle the indices in the slack utilization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-09 12:47:35 -07:00
Lev Nachmanson
1e5ceea4f5 some refactoring of lar_solver.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-09 12:14:17 -07:00
Lev Nachmanson
0a0979f804 shring lar_solver.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-08 19:23:55 -07:00
Lev Nachmanson
0108a86490 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-08 17:28:34 -07:00
Lev Nachmanson
7da06df64f restore lar_solver::add_named_var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-08 17:18:41 -07:00
Lev Nachmanson
935f076a05 continue PIMPL refactor in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-08 16:45:00 -07:00
Lev Nachmanson
d4f45e1528 implement imp of lar_solver as lar_solver::imp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-07 13:53:28 -07:00
Lev Nachmanson
97c6074156 remove a function from lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-07 13:33:46 -07:00
Lev Nachmanson
67652dd8eb test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-07 13:14:23 -07:00
Lev Nachmanson
5487c5a963 shuffle more functionality from lar_solver.h to lar_solver::imp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-07 12:59:49 -07:00
Lev Nachmanson
fdcde925d6 apply the slack idea in a loop 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-05 16:21:37 -07:00
Lev Nachmanson
d413468dce slack 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-02 12:10:29 -07:00
Lev Nachmanson
f89e133d52
revert the behavior of add_zero_assumption (#7631) 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-28 16:07:46 -07:00
Nikolaj Bjorner
6af61fa0f4 remove experiment 2025-04-28 10:00:02 -07:00
Nikolaj Bjorner
b502126ebc fix #7634 2025-04-27 23:57:57 -07:00
Nikolaj Bjorner
24090fc48c move flush smc to first use 2025-04-27 11:44:45 -07:00
Nikolaj Bjorner
a626cd0fed flush smc before use in model construction 2025-04-27 11:18:18 -07:00
Nikolaj Bjorner
71b5e44058 #7596 - flush smc before copy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-04-27 10:36:27 -07:00
Nikolaj Bjorner
7a302239c2 fix #7630 2025-04-26 11:40:48 -07:00
Nikolaj Bjorner
d581dc1db4 #7630 propagate parameters on lazy tactics 2025-04-26 11:22:16 -07:00
Nuno Lopes
322e4441b3 Fix conversion of signed 1-bit BV to FP 
Fixes https://github.com/AliveToolkit/alive2/issues/1193
 2025-04-25 12:38:00 +01:00
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