merge with z3prover

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

src/tactic/smtlogics/qflia_tactic.cpp

@@ -212,9 +212,6 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
     
 
     tactic * st = using_params(and_then(preamble_st,
-#if 1
-                                        mk_smt_tactic()),
-#else
                                         or_else(mk_ilp_model_finder_tactic(m),
                                                 mk_pb_tactic(m),
                                                 and_then(fail_if_not(mk_is_quasi_pb_probe()), 
@@ -222,7 +219,6 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
                                                          mk_fail_if_undecided_tactic()),
                                                 mk_bounded_tactic(m),
                                                 mk_smt_tactic())),
-#endif
                                main_p);
 
     

src/util/lp/bound_propagator.cpp

@@ -16,8 +16,6 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const {
     return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j];
 }
 void bound_propagator::try_add_bound(mpq  v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
-    TRACE("try_add_bound",
-          tout << "v = " << v << ", j = " << j << std::endl;);
     j = m_lar_solver.adjust_column_index_to_term_index(j);    
     if (m_lar_solver.is_term(j)) {
         // lp treats terms as not having a free coefficient, restoring it below for the outside consumption

src/util/lp/lp_core_solver_base_def.h

@@ -108,8 +108,6 @@ pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
         if (r.var() != j)
             m_d[r.var()] -= a * r.get_val();
     }
-ls
-
     a = zero_of_type<T>(); // zero the pivot column's m_d finally
 }
 

src/util/lp/lp_primal_core_solver.h

@@ -280,17 +280,14 @@ public:
         if (m_bland_mode_tableau)
             return find_beneficial_column_in_row_tableau_rows_bland_mode(i, a_ent);
         // a short row produces short infeasibility explanation and benefits at least one pivot operation
-        int choice = -1;
+        vector<const row_cell<T>*> choices;
-        int nchoices = 0;
+        unsigned num_of_non_free_basics = 1000000;
         unsigned len = 100000000;
         unsigned bj = this->m_basis[i];
         bool bj_needs_to_grow = needs_to_grow(bj);
         for (unsigned k = 0; k < this->m_A.m_rows[i].m_cells.size(); k++) {
             const row_cell<T>& rc = this->m_A.m_rows[i].m_cells[k];
             if (rc.dead()) continue;
-			const row_cell<T>& rc = this->m_A.m_rows[i].m_cells[k];
-			if (rc.dead()) continue;
->>>>>>> e6c612f... trying the new scheme in static_matrix : in progress
             unsigned j = rc.var();
             if (j == bj)
                 continue;
@@ -305,23 +302,24 @@ public:
             if (damage < num_of_non_free_basics) {
                 num_of_non_free_basics = damage;
                 len = this->m_A.m_columns[j].live_size();
-                choice = k;
+                choices.clear();
-                nchoices = 1;
+                choices.push_back(&rc);
             } else if (damage == num_of_non_free_basics &&
-                       this->m_A.m_columns[j].live_size() <= len && (this->m_settings.random_next() % (++nchoices))) {
+                       this->m_A.m_columns[j].live_size() <= len && (this->m_settings.random_next() % 2)) {
-                choice = k;
+                choices.push_back(&rc);
                 len = this->m_A.m_columns[j].live_size();
             }
         }
         
 
-        if (choice == -1) {
+         if (choices.size() == 0) {
             m_inf_row_index_for_tableau = i;
             return -1;
         }
-        const row_cell<T>& rc = this->m_A.m_rows[i].m_cells[choice];
+        const row_cell<T>* rc = choices.size() == 1? choices[0] :
-        a_ent = rc.coeff();
+            choices[this->m_settings.random_next() % choices.size()];
-        return rc.var();
+        a_ent = rc->coeff();
+        return rc->var();
     }
     static X positive_infinity() {
         return convert_struct<X, unsigned>::convert(std::numeric_limits<unsigned>::max());

src/util/lp/static_matrix.h

@@ -64,9 +64,6 @@ public:
     bool alive() const { return !dead(); }
     bool dead() const { return m_i == static_cast<unsigned>(-1); }
     void set_dead() { m_i = -1;}
-
-
-
 };
 
 template <typename T>
@@ -79,6 +76,7 @@ public:
     }
     row_cell(unsigned j, T const & val) : m_j(j), m_value(val) {
     }
+
     const T & get_val() const {
         lp_assert(alive());
         return m_value;
@@ -126,8 +124,6 @@ public:
     bool alive() const { return !dead(); }
     bool dead() const { return m_j == static_cast<unsigned>(-1); }
     void set_dead() { m_j = static_cast<unsigned>(-1); }
-
-
 };
 
 template <typename T>
@@ -252,10 +248,6 @@ public:
         return m_live_size;
     }
 
-    unsigned cells_size() const {
-        return m_cells.size();
-    }
-
     unsigned cells_size() const {
         return m_cells.size();
     }
@@ -304,7 +296,7 @@ public:
         }
         m_cells.pop_back();
     }
-
+    bool is_correct() const {
         std::set<unsigned> d0;
         std::set<unsigned> d1;
         unsigned alive = 0;
@@ -341,38 +333,6 @@ public:
         lp_assert(is_correct());
     }
 
-    void swap_with_head_cell(unsigned i) {
-        lp_assert(i > 0);
-        lp_assert(m_cells[i].alive());
-        column_cell head_copy = m_cells[0];
-        if (head_copy.dead()) {
-            if (m_first_dead == 0) {
-                m_first_dead = i;
-            } else {
-                column_cell * c = &m_cells[m_first_dead];
-                for (; c->next_dead_index() != 0; c = &m_cells[c->next_dead_index()]);
-                lp_assert(c->next_dead_index() == 0);
-                c->next_dead_index() = i;
-            }
-        }
-        m_cells[0] = m_cells[i];
-        m_cells[i] = head_copy;
-        lp_assert(is_correct());
-    }
-
-    column_cell & add_cell(unsigned i, unsigned & index) {
-        if (m_first_dead != -1) {
-            auto & ret = m_cells[index = m_first_dead];
-            m_first_dead = ret.next_dead_index();
-            m_live_size++;
-            ret.var() = i;
-            return ret;
-        }
-        lp_assert(m_live_size == m_cells.size());
-        index = m_live_size++;
-        m_cells.push_back(column_cell(i));
-        return m_cells.back();
-    }
     column_cell & add_cell(unsigned i, unsigned & index) {
         if (m_first_dead != -1) {
             auto & ret = m_cells[index = m_first_dead];