mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 20:05:51 +00:00
3 commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
Lev
|
c4c52ad104 |
enable printing in Release
Signed-off-by: Lev <levnach@hotmail.com> |
||
|
Lev Nachmanson
|
9ba4026bc6 |
avoid going creating hnf_cuts if all involved vars have integral values
Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add explanations to hnf cuts Signed-off-by: Lev Nachmanson <levnach@hotmail.com> nits and virtual methods (#68) * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> cleanup from std::cout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> handle the case when the number of terms is greater than the number of variables in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> method name's fix Signed-off-by: Lev Nachmanson <levnach@hotmail.com> restore hnf_cutter to work with m_row_count <= m_column_count Signed-off-by: Lev Nachmanson <levnach@hotmail.com> tune addition of rational numbers (#70) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> give shorter explanations, call hnf only when have a not integral var Signed-off-by: Lev Nachmanson <levnach@hotmail.com> overhaul of mpq (#71) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> fix for 32 bit build (#72) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> yes (#74) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactor Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> fix the merge Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in maximize_term untested Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix compilation (#75) * log quantifiers only if present Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * local Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method in bound propagator Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for mixed integer-real Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix default tactic usage Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * overhaul of mpz/mpq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disabled temporary setting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove prints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * customize for 64 bit Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactor Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * relax check Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * change for gcc Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> |
||
|
Lev Nachmanson
|
3b5337823a |
extract gomory cut functionality in one method
Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> prepare calculate U in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> naive algorithm for HNF and m <= n Signed-off-by: Lev Nachmanson <levnach@hotmail.com> naive algorithm for HNF Signed-off-by: Lev Nachmanson <levnach@hotmail.com> introduces reverse matrix into Hermite Normal Form calculation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on more efficient hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use smarter templates in lu.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> the new lu scheme compiles Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simple test passes with the modified lu Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix the build on windows Signed-off-by: Lev Nachmanson <levnach@hotmail.com> playing with the example from cutting the mix Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf, add extended_gcd_minimal_uv() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on extended_gcd_minimal_uv Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf, add extended_gcd_minimal_uv() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> more tests and bug fixes in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf modulo version Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf modulo version, more tests pass Signed-off-by: Lev Nachmanson <levnach@hotmail.com> a rough version of hnf passed the tests Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix build in release Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in determinant calculations Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> create a stub for hnf_cuts Signed-off-by: Lev Nachmanson <levnach@hotmail.com> create a stub for hnf_cuts Signed-off-by: Lev Nachmanson <levnach@hotmail.com> create a stub for hnf_cuts Signed-off-by: Lev Nachmanson <levnach@hotmail.com> general_matrix etc. Signed-off-by: Lev Nachmanson <levnach@hotmail.com> general_matrix etc. Signed-off-by: Lev Nachmanson <levnach@hotmail.com> rename cut_solver to chase_cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> rename cut_solver to chase_cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> hnf_cutter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> |
Renamed from src/util/lp/sparse_matrix.h (Browse further)