mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 11:55:51 +00:00
6 commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
Lev Nachmanson
|
e5eea467b7 |
adjust hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com> change in settings + random in adding terms to hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add terms in hnf from the beginning Signed-off-by: Lev Nachmanson <levnach@hotmail.com> adjusting settings Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove non used determinant() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> |
||
|
Lev Nachmanson
|
eeaca949e0 |
cleanup in hnf.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixex in maximize_term Signed-off-by: Lev Nachmanson <levnach@hotmail.com> prepare for LIRA (#76) * merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * simple mixed integer example Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Nikolaj's fixes in theory_lra.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in maximize_term, disable find_cube for mixed case Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix cube heuristic for the mixed case Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix the build Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix in find cube delta's calculation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove a printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove a blank line Signed-off-by: Lev Nachmanson <levnach@microsoft.com> test credentials Signed-off-by: Lev Nachmanson <levnach@microsoft.com> avoid double checks to add terms in hnf_cutter Signed-off-by: Lev Nachmanson <levnach@microsoft.com> fixes in add terms to hnf_cutter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove a variable used for debug only Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove a field Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove a warning and hide m_A_orig under debug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use var_register to deal with mapping between external and local variables Signed-off-by: Lev Nachmanson <levnach@hotmail.com> tighten the loop in explain_implied_bound Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in theory_lra and relaxing debug checks in pop(), for the case when push() has been done from not fully initialized state Signed-off-by: Lev Nachmanson <levnach@hotmail.com> suppress hnf cutter when the numbers become too large Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove some debug code Signed-off-by: Lev Nachmanson <levnach@hotmail.com> adjusting hnf Signed-off-by: Lev Nachmanson <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
|
9be49ff6ff |
add cancel to hnf_cutter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com> exit earlier on a large matrix in hnf_cutter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> call hnf only for the boundary points Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix a bug in hnf_cutter initialization Signed-off-by: Lev Nachmanson <levnach@hotmail.com> initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x Signed-off-by: Lev Nachmanson <levnach@hotmail.com> initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x Signed-off-by: Lev Nachmanson <levnach@hotmail.com> initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x Signed-off-by: Lev Nachmanson <levnach@hotmail.com> initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in determinant_of_rectangular_matrix calculations Signed-off-by: Lev Nachmanson <levnach@hotmail.com> changes in debug code Signed-off-by: Lev Nachmanson <levnach@hotmail.com> init m_hnf_cut_period from globals settings Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix some warnings Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Lev2 (#66) * 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> remove a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify gomory cut return's logic Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify uniformly int_solver::check() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> making new arith solver default for LIA (#67) * 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> remove chase_cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove integer_domain Signed-off-by: Lev Nachmanson <levnach@hotmail.com> restore call for find_cube() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove a method Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove some debug code Signed-off-by: Lev Nachmanson <levnach@hotmail.com> |
||
|
Lev Nachmanson
|
82eb80de6d |
add var_register
Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fill the matrix A in hnf_cutter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fill the matrix A in hnf_cutter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> first steps of hnf cutter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> handle generated cases in hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> call hnf only for a full rank matrix Signed-off-by: Lev Nachmanson <levnach@hotmail.com> get (H reversed) * b Signed-off-by: Lev Nachmanson <levnach@hotmail.com> finding the cut row randomly, exiting if is not there Signed-off-by: Lev Nachmanson <levnach@hotmail.com> produce first cuts with hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> produce first cuts with hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> define by lp_settings if to avoid calling hnf_cutter when the solution is not on the boundary Signed-off-by: Lev Nachmanson <levnach@hotmail.com> hnf Signed-off-by: Lev Nachmanson <levnach@hotmail.com> revert to the previous version Signed-off-by: Lev Nachmanson <levnach@hotmail.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> |