mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
16435 commits 24 branches 48 tags 158 MiB
Commit graph

1670 commits

Author SHA1 Message Date
Nikolaj Bjorner
91c95aab16 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-12-11 08:41:17 -08:00
Nikolaj Bjorner
83efb1413a na 2021-12-11 08:41:04 -08:00
Nikolaj Bjorner
4c2231897f more general simplification 2021-12-10 04:45:48 -08:00
Nikolaj Bjorner
9c3489ba4b na 2021-12-09 15:58:23 -08:00
Nikolaj Bjorner
bf258ee29d add bit shorthand 2021-12-09 15:25:44 -08:00
Nikolaj Bjorner
a4fc63c542 initial overflow test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 14:39:00 -08:00
Nikolaj Bjorner
99e2247ccb ovfl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 13:15:59 -08:00
Nikolaj Bjorner
dcdbbfb925 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 09:50:53 -08:00
Nikolaj Bjorner
bd08d766d2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 09:44:45 -08:00
Nikolaj Bjorner
0dcaf9b9f9 add ovfl constraint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 09:05:23 -08:00
Nikolaj Bjorner
6ddca4091a merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 08:26:51 -08:00
Nikolaj Bjorner
d7f16d0622 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 08:26:34 -08:00
Nikolaj Bjorner
f3ac879fa4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 08:25:52 -08:00
Nikolaj Bjorner
ed9c0b84f6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-09 08:25:24 -08:00
Nikolaj Bjorner
ca9fbcf6f4 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-08 12:44:55 -08:00
Nikolaj Bjorner
8d3c3ede39 save 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-08 12:40:44 -08:00
Nikolaj Bjorner
b69ad786f2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-08 09:04:13 -08:00
Nikolaj Bjorner
e45ae32685 unsound equality propagation #5676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-08 09:02:05 -08:00
Nikolaj Bjorner
9f2b18cac5 add tactic name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 13:37:57 -08:00
Lev Nachmanson
7758b519bc
Handle correctly cancelled run (#5695) 
* remove the bound on total iterations in simplex

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove unncesseray checks in  get_freedom_interval_for_column()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the build of test-z3

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Revert "remove unncesseray checks in  get_freedom_interval_for_column()"

This reverts commit 6770ed85e3.

* optimize get_freedom_interval_for_column() for feasible case

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add function lar_solver::status_feasible

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* rename status_is_feasible() to is_feasible()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the linux build

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-12-05 18:38:37 -08:00
Nikolaj Bjorner
98a0f37eec update viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-04 02:23:21 -08:00
Nikolaj Bjorner
4d0f55febd update viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 17:57:08 -08:00
Nikolaj Bjorner
1618c970df adding checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 13:17:48 -08:00
Nikolaj Bjorner
970347e797 infeas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 13:00:52 -08:00
Nikolaj Bjorner
a81a00a93c add support for non-unit coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 09:53:09 -08:00
Lev Nachmanson
d50c4bfcc1 remove an unused var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-11-28 09:44:50 -08:00
Nikolaj Bjorner
90bd5f186b tune based on test_l5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-26 20:14:00 +01:00
Nikolaj Bjorner
7b85afbe9c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-26 18:27:44 +01:00
Nikolaj Bjorner
fc6e127cca don't add viable premises on decisions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-25 20:19:58 +01:00
Nikolaj Bjorner
a4e29ecd7e interval 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-25 18:46:43 +01:00
Nikolaj Bjorner
adf41c5d02 another bug fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-24 13:37:15 +01:00
Nikolaj Bjorner
caef8d026f add unsat core, activity, quick pass for viable 2021-11-24 13:23:28 +01:00
Nikolaj Bjorner
b82c3cfd33 remove deprecated comment 2021-11-24 11:26:13 +01:00
Nikolaj Bjorner
21c604e7b4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-23 18:56:32 +01:00
Nikolaj Bjorner
73ffd1c1cb na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 18:18:01 +01:00
Nikolaj Bjorner
8db711bc3c retire deprecated functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 18:14:15 +01:00
Nikolaj Bjorner
8ec5ccbb9a roll in new-viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 06:17:20 +01:00
Nikolaj Bjorner
d86570ce75 prepare for new viable 2021-11-21 06:18:35 +01:00
Nikolaj Bjorner
b0bf03457c conflict 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 08:23:50 -08:00
Nikolaj Bjorner
caaefef847 remove add_non_viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 15:57:55 -08:00
Nikolaj Bjorner
6bf4f001d9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 15:53:51 -08:00
Nikolaj Bjorner
1dcb7e6f6a remove justified vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 15:43:39 -08:00
Nikolaj Bjorner
de424713e4 if you are really reading this commit message, you must be a programmer who has no life. 2021-11-18 10:10:50 -08:00
Nikolaj Bjorner
a5fdf6ba8a Update viable2.cpp 2021-11-16 09:54:06 -08:00
Nikolaj Bjorner
69a17d0c60 test and fix viable2 2021-11-14 20:55:12 -08:00
Nikolaj Bjorner
4261345503 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-13 17:43:07 -08:00
Nikolaj Bjorner
d073583d88 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-13 06:50:11 -08:00
Nikolaj Bjorner
5708de4301 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-12 11:20:35 -08:00
Nikolaj Bjorner
3c16edc8d3 check for v1 == v2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-12 09:11:17 -08:00
Nikolaj Bjorner
63ac2ee0d1 #5614 turn on / off options to get better performance. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-11 17:54:46 -08:00