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

1683 commits

Author SHA1 Message Date
Nikolaj Bjorner
842e9234c9 remove pragma 2021-12-14 14:38:12 -08:00
Nikolaj Bjorner
06f7ba2e78 add stubs for shr 2021-12-14 14:35:08 -08:00
Nikolaj Bjorner
934564882c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 12:34:34 -08:00
Nikolaj Bjorner
8c2735e68b prepare for diseq_lin viable 2021-12-13 12:00:19 -08:00
Nikolaj Bjorner
651b41f8c0 refactor fi functionality 2021-12-13 11:39:15 -08:00
Nikolaj Bjorner
ca3251b152 add widening in all cases 2021-12-13 10:55:03 -08:00
Nikolaj Bjorner
c7da31a67d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-13 10:24:42 -08:00
Nikolaj Bjorner
33d433d742 split out restart 2021-12-12 17:27:30 -08:00
Nikolaj Bjorner
30a2c32c3b add placeholder for simplification 2021-12-12 14:52:09 -08:00
Nikolaj Bjorner
d80b375ac3 accelerate 2021-12-12 14:33:57 -08:00
Nikolaj Bjorner
7bf76dd1f6 finally! 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-12 10:26:54 -08:00
Nikolaj Bjorner
f1d46b58a4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-11 17:38:09 -08:00
Nikolaj Bjorner
59acd77981 n 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-11 13:01:08 -08:00
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