mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-15 00:46:38 +00:00
Code Activity
9738 commits 42 branches 51 tags 169 MiB
Commit graph

222 commits

Author SHA1 Message Date
Nikolaj Bjorner
dcda39e76e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 17:12:32 -07:00
Nikolaj Bjorner
3c553c17e8 fix dump utility for cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 14:32:56 -07:00
Nikolaj Bjorner
ed19af4c4e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 09:02:37 -07:00
Lev Nachmanson
b90d571d9a fixing the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-18 15:36:01 -07:00
Lev
041458f97a fixes the +- bug in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-18 14:42:32 -07:00
Lev
b940b7873b work on Gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-18 13:47:18 -07:00
Lev
ca3ce964ce work on Gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-18 13:34:05 -07:00
Lev
106b677201 fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:47:54 -07:00
Lev
34bdea750c fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:46:16 -07:00
Lev
8c122ba9bd fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:33:35 -07:00
Lev
03d55426bb fixes in gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-15 17:15:46 -07:00
Lev
324396e403 separate the gomory cut functionality in a separate file 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 17:12:49 -07:00
Lev
26764b076f adjust cuts and branch (m_t and m_k) for terms 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 12:39:46 -07:00
Lev
257ba6218f remove gomory.h 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:54:10 -07:00
Lev
22213a9e73 rebase 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:53:54 -07:00
Lev
5dee39721a rebase 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:52:14 -07:00
Lev
e705e5a309 branch on inf basic in gomory 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-14 11:49:39 -07:00
Nikolaj Bjorner
6ea4aff622 add validation code for cuts, fix missing unit propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-13 10:47:50 -07:00
Lev Nachmanson
f810a5d8c3 remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-10 15:22:48 -07:00
Lev Nachmanson
8068c64cab avoid using not initialized variables in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-09-10 11:02:38 -07:00
Lev Nachmanson
075cf106aa fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-08-01 08:46:03 -07:00
Lev Nachmanson
7370396c30 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-08-01 08:06:56 -07:00
Lev Nachmanson
0a51417804 unroll static_matrix to avoid dead cells 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-31 22:57:10 -07:00
Lev
3d274c2e6f use CASSERT for hnf 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-30 15:55:06 -07:00
Lev Nachmanson
0ee68220e1 use CASSERT instead of lp_assert for static_matrix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-30 14:34:03 -07:00
Lev
181bb60e36 remove some lp_asserts 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-30 12:54:53 -07:00
Lev Nachmanson
9cb713879e fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-30 09:56:39 -07:00
Lev Nachmanson
2de27ae3af uniform choice of a beneficial column 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-29 22:33:19 -07:00
Lev
e9595eb283 merge with z3prover 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-29 21:15:42 -07:00
Lev Nachmanson
16b71fe911 work on static_matrix's cells 
Signed-off-by: Lev <levnach@hotmail.com>

trying the new scheme in static_matrix : in progress

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

in the middle of changes in static_matrix

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

more fixes in static_matrix.h

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

debug

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

fixes in static_matrix

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

fixes in static_matrix, column_strip

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

fixes in static_matrix

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

fixes for static_matrix

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

work on static_matrix

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

work on static_matrix

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

progress in static_matrix

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

fix a bug in swap_with_head_cell

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

progress in static_matrix

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

compress rows and columns if needed

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

fix in compression of cells

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-29 20:45:13 -07:00
Nikolaj Bjorner
1cb3f7c792 fixing #1520 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-28 18:03:13 -07:00
Lev
ef2cdc226a a fix in maximize_term 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-26 22:46:28 -07:00
Nikolaj Bjorner
d74978c277 fix #1762, #1764, #1768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 20:29:26 +01:00
Lev Nachmanson
b71fe0b3b7 speed up find_cube 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-16 16:17:49 -07:00
Lev Nachmanson
35f7f1f62e fix in cube heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-16 12:29:42 -07:00
Nikolaj Bjorner
30330c79a1 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-15 22:36:02 -07:00
Nikolaj Bjorner
d00ffdda82 strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-15 22:35:47 -07:00
Lev Nachmanson
f7ac096696 avoid a vector copy 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-15 15:29:13 -07:00
Nikolaj Bjorner
1d408c1955 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-13 07:52:40 -07:00
Nikolaj Bjorner
167969d6c2 remove debug/non-debug difference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 07:52:36 -07:00
Lev Nachmanson
e0e893b791 fix in hnf for the lower bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 12:29:09 -07:00
Lev Nachmanson
2dfb8f53b6 do not add term to hnf if one of the vars has v.y value 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-11 10:59:55 -07:00
Nikolaj Bjorner
5e5f46f0f8 handle cancelation from nra_solver gracefully 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 17:34:45 -07:00
Lev
a4a468660d remove an assert 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-10 12:05:23 -07:00
Lev
c4c52ad104 enable printing in Release 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson
5c712d471f create hnf cuts too, when gomory_cut_period is 2 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-09 20:49:16 -07:00
Lev Nachmanson
852df6f7d9 reshufle var_register to faster access 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-05 16:35:05 -07:00
Nikolaj Bjorner
e8e786ae64 remove stale files from lp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 20:57:52 -07:00
Nikolaj Bjorner
7e0a7d73f2 remove unused files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 20:53:11 -07:00
Nikolaj Bjorner
c06ed77ff1 fix merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 15:37:33 -07:00