mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-16 17:36:39 +00:00
Code Activity
17697 commits 43 branches 51 tags 169 MiB
Commit graph

128 commits

Author SHA1 Message Date
Lev Nachmanson
1fb24ebc35 fix lp_tst 2023-03-08 10:27:05 -08:00
Lev Nachmanson
11eab94321 more dead code 2023-03-08 10:27:05 -08:00
Lev Nachmanson
e430f28813 remove dead code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
f33f8c265e more cleanup 2023-03-08 10:27:05 -08:00
Lev Nachmanson
0fb65dea3f rm square_sparse_matrix 2023-03-08 10:27:05 -08:00
Lev Nachmanson
6eedbd4f35 rm lu 2023-03-08 10:27:05 -08:00
Lev Nachmanson
2e9dc3d090 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
9a7c99da33 rm lu 2023-03-08 10:27:05 -08:00
Lev Nachmanson
c251151d66 rm_lu 2023-03-08 10:27:05 -08:00
Lev Nachmanson
25f103db1a rm_lp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
a38be43264 rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
ea16f6608c before rm lu 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-08 10:27:05 -08:00
Lev Nachmanson
92fe8c5968 restore the previous state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-03-03 18:30:17 -08:00
Lev Nachmanson
2dd30fa350 rm lp_primal_simplex 2023-03-03 15:44:50 -08:00
Lev Nachmanson
2ec09944d7 removals 2023-03-03 15:32:44 -08:00
Lev Nachmanson
a44772424c more removals 2023-03-03 15:30:15 -08:00
Lev Nachmanson
cd24c99739 remove a lp_primal_simplex.cpp from CMakeLists 2023-03-03 15:26:06 -08:00
Lev Nachmanson
f986ac6a75 remove mps_reader 2023-03-03 14:50:10 -08:00
Nikolaj Bjorner
7767144051 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 11:07:47 -08:00
Nikolaj Bjorner
ad49dd739b initialize variables to avoid warning messages whether real or spurious 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-01 17:08:02 -04:00
Bruce Mitchener
d8c99480c6 test/lp: Replace if linux with if not windows. 
This is stuff that works on posix, so we can flip the check.
 2022-08-03 08:22:54 +03:00
Bruce Mitchener
8313282cda Use char version of find_last_of when possible. 2022-08-02 17:38:11 +03: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
Lev Nachmanson
742be83503
Lpbounds (#4492) 
* remove inheritance from bound propagation

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

* less inheritance

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

* less inheritance

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

* fix the build

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-02 01:00:06 -07:00
Lev Nachmanson
af2f74c05f
smarter explanation.h (#4385) 
* smarter explanation.h

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

* clean explanation API

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

* suppress warnings

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

* disable the warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-19 12:38:44 -07:00
Lev Nachmanson
8921ed56b5 fix a bug in Horner heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-23 15:58:53 -07:00
Lev Nachmanson
1f23ae8aae fix the test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-16 12:58:39 -07:00
Nikolaj Bjorner
296a97d0d3 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 01:03:38 -07:00
Lev Nachmanson
fd219abe8c fix test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
26631ce38d add a unit test for monics, plus some cosmetic changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner
2512a958b9 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 08:25:52 -08:00
Nikolaj Bjorner
e964973f19 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-08 16:01:12 -08:00
Nikolaj Bjorner
88374a15d0 build errors/warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-07 10:09:10 -08:00
Lev Nachmanson
9694dc0c74 change in the test lp.cpp and in a trace statement 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-29 11:03:18 -08:00
Lev Nachmanson
0bb29bca69 change core::get_var_weight() to return unsigned, remove some warnings from test/lp/lp.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
efe4d6c53c fix the build and restore the nex_pow gt() comparison 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
0f948d7a07 reverse the order in nex expressions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
dc39ef761c fix nex order and cross_nested 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
d5f574ffc5 fixes in nex order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f71cd72d7b fixes in nex order, add nex_mul::m_coeff 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
0c126031b0 init of m_active_vars_weights and fixes in is_simplified 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
b2d1bcc8cd cleanup some warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
93f52cf20b cleanup the tests from warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
3e009a237f implement canonization of nex expressions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f8a45d2fb3 fixes in nex expressions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f9beef19ce fixes in nex expressions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
3929e002a5 simplify nex_creator 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
a888e79696 fix nex simplification 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
43294cea16 fix nex simplification 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
13434a2589 fix nex simplification 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00