From 055593469ab78cd27689737a4f1aea0a5d58e8dd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jul 2017 20:47:07 -0700 Subject: [PATCH] Dev (#64) * introduce int_solver.h Signed-off-by: Lev Nachmanson * add int_solver class Signed-off-by: Lev Nachmanson * track which var is an integer Signed-off-by: Lev Nachmanson * add queries for integrality of vars Signed-off-by: Lev Nachmanson * resurrect lp_tst in its own director lp Signed-off-by: Lev Nachmanson * add file Signed-off-by: Lev Nachmanson * add_constraint has got a body Signed-off-by: Lev Nachmanson * fix add_constraint and substitute_terms_in_linear_expression Signed-off-by: Lev Nachmanson * after merge with Z3Prover Signed-off-by: Lev Nachmanson * adding stub check_int_feasibility() Signed-off-by: Lev Nachmanson * Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson * adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson * Dev (#51) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * test Signed-off-by: Lev Nachmanson * Dev (#53) * change in a comment Signed-off-by: Lev Nachmanson * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * adding nra Signed-off-by: Nikolaj Bjorner * debugging nra Signed-off-by: Nikolaj Bjorner * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner * n/a Signed-off-by: Nikolaj Bjorner * integrate nlsat Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * preserve is_int flag Signed-off-by: Lev Nachmanson * remove a debug printout Signed-off-by: Lev Nachmanson * Dev (#54) * change in a comment Signed-off-by: Lev Nachmanson * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * adding nra Signed-off-by: Nikolaj Bjorner * debugging nra Signed-off-by: Nikolaj Bjorner * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner * n/a Signed-off-by: Nikolaj Bjorner * integrate nlsat Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * use integer test from lra solver, updated it to work on term variables Signed-off-by: Nikolaj Bjorner * fix equality check in assume-eq Signed-off-by: Nikolaj Bjorner * fix model_is_int_feasible Signed-off-by: Lev Nachmanson * untested gcd_test() Signed-off-by: Lev Nachmanson * call fill_explanation_from_fixed_columns() Signed-off-by: Lev Nachmanson * add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check() Signed-off-by: Lev Nachmanson * port more of theory_arith_int.h Signed-off-by: Lev Nachmanson * use statistics of lar_solver by theory_lra.cpp Signed-off-by: Lev Nachmanson * port more code to int_solver.cpp Signed-off-by: Lev Nachmanson * add an assert Signed-off-by: Lev Nachmanson * more int porting Signed-off-by: Lev Nachmanson * fix a bug in pivot_fixed_vars_from_basis Signed-off-by: Lev Nachmanson * small change Signed-off-by: Lev Nachmanson * implement find_inf_int_base_column() Signed-off-by: Lev Nachmanson * catch unregistered vars in add_var_bound Signed-off-by: Lev Nachmanson * add a file Signed-off-by: Lev Nachmanson * compile for vs2012 Signed-off-by: Lev Nachmanson * fix asserts in add_var_bound Signed-off-by: Lev Nachmanson * fix the lp_solver init when workig on an mps file Signed-off-by: Lev Nachmanson * towards int_solver::check() Signed-off-by: Lev Nachmanson * change in int_solver::check() signature Signed-off-by: Lev Nachmanson * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * return branch from int_solver::check() Signed-off-by: Lev Nachmanson * add a stub for mk_gomory_cut Signed-off-by: Lev Nachmanson * Dev (#59) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * Dev (#60) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * Dev (#61) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * more TRACE(arith_int) Signed-off-by: Lev Nachmanson * fix the build Signed-off-by: Lev Nachmanson * loops Signed-off-by: Nikolaj Bjorner * Dev (#62) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * build fix Signed-off-by: Lev Nachmanson --- src/util/lp/lp_core_solver_base.hpp | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp index c2adb61c1..f3cee7fa8 100644 --- a/src/util/lp/lp_core_solver_base.hpp +++ b/src/util/lp/lp_core_solver_base.hpp @@ -83,8 +83,8 @@ pivot_for_tableau_on_basis() { // i is the pivot row, and j is the pivot column template void lp_core_solver_base:: pivot_to_reduced_costs_tableau(unsigned i, unsigned j) { - if (j >= m_d.size()) - return; + if (j >= m_d.size()) + return; T &a = m_d[j]; if (is_zero(a)) return; @@ -925,9 +925,9 @@ template void lp_core_solver_base::transpose_row } // j is the new basic column, j_basic - the leaving column template bool lp_core_solver_base::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector & w) { - lean_assert(m_basis_heading[j] < 0); - lean_assert(m_basis_heading[j_basic] >= 0); - unsigned row_index = m_basis_heading[j_basic]; + lean_assert(m_basis_heading[j] < 0); + lean_assert(m_basis_heading[j_basic] >= 0); + unsigned row_index = m_basis_heading[j_basic]; change_basis(j, j_basic); if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) { if (m_factorization->need_to_refactor()) { @@ -952,7 +952,7 @@ template void lp_core_solver_base::pivot_fixed_v indexed_vector w(m_basis.size()); // the buffer unsigned i = 0; // points to basis unsigned j = 0; // points to nonbasis - + for (; i < m_basis.size() && j < m_nbasis.size(); i++) { unsigned ii = m_basis[i]; unsigned jj; @@ -967,9 +967,9 @@ template void lp_core_solver_base::pivot_fixed_v if (j >= m_nbasis.size()) break; j++; - if (!pivot_column_general(jj, ii, w)) - return; // total failure - break; + if (!pivot_column_general(jj, ii, w)) + return; // total failure + break; } } }