Merge pull request #1744 from levnach/master

enable printing from Release

src/util/lp/binary_heap_priority_queue.h

@@ -78,8 +78,6 @@ public:
         lp_assert(m_heap_size > 0);
         return m_heap[1];
     }
-#ifdef Z3DEBUG
     void print(std::ostream & out);
-#endif
 };
 }

src/util/lp/binary_heap_priority_queue_def.h

@@ -194,7 +194,6 @@ template <typename T> unsigned binary_heap_priority_queue<T>::dequeue() {
     m_heap_inverse[ret] = -1;
     return ret;
 }
-#ifdef Z3DEBUG
 template <typename T> void binary_heap_priority_queue<T>::print(std::ostream & out) {
     vector<int> index;
     vector<T> prs;
@@ -210,5 +209,4 @@ template <typename T> void binary_heap_priority_queue<T>::print(std::ostream & o
     for (int i = 0; i < index.size(); i++)
         enqueue(index[i], prs[i]);
 }
-#endif
 }

src/util/lp/general_matrix.h

@@ -71,7 +71,6 @@ public:
     ref_row operator[](unsigned i) { return ref_row(*this, m_data[adjust_row(i)]); }
     ref_row_const operator[](unsigned i) const { return ref_row_const(*this, m_data[adjust_row(i)]); }
 
-#ifdef Z3DEBUG
     void print(std::ostream & out, unsigned blanks = 0) const {
         unsigned m = row_count();
         unsigned n = column_count();
@@ -96,8 +95,6 @@ public:
         print_matrix<mpq>(m.m_data, out, blanks);
     }
 
-#endif
-
     void clear() { m_data.clear(); }
 
     bool row_is_initialized_correctly(const vector<mpq>& row) {

src/util/lp/indexed_vector.cpp

@@ -37,10 +37,10 @@ template bool indexed_vector<unsigned>::is_OK() const;
 template bool indexed_vector<double>::is_OK() const;
 template bool indexed_vector<mpq>::is_OK() const;
 template bool indexed_vector<lp::numeric_pair<mpq> >::is_OK() const;
+#endif
 template void lp::indexed_vector< lp::mpq>::print(std::basic_ostream<char,struct std::char_traits<char> > &);
 template void lp::indexed_vector<double>::print(std::basic_ostream<char,struct std::char_traits<char> > &);
 template void lp::indexed_vector<lp::numeric_pair<lp::mpq> >::print(std::ostream&);
-#endif
 }
 // template void lp::print_vector<double, vectro>(vector<double> const&, std::ostream&);
 // template void lp::print_vector<unsigned int>(vector<unsigned int> const&, std::ostream&);

src/util/lp/indexed_vector.h

@@ -216,7 +216,7 @@ public:
     
 #ifdef Z3DEBUG
     bool is_OK() const;
-    void print(std::ostream & out);
 #endif
+    void print(std::ostream & out);
 };
 }

src/util/lp/indexed_vector_def.h

@@ -96,6 +96,7 @@ bool indexed_vector<T>::is_OK() const {
 
     return true;
 }
+#endif
 template <typename T>
 void indexed_vector<T>::print(std::ostream & out) {
     out << "m_index " << std::endl;
@@ -105,6 +106,5 @@ void indexed_vector<T>::print(std::ostream & out) {
     out << std::endl;
     print_vector(m_data, out);
 }
-#endif
 
 }

src/util/lp/int_solver.cpp

@@ -599,7 +599,7 @@ lia_move int_solver::make_hnf_cut() {
 }
 
 lia_move int_solver::hnf_cut() {
-    if ((m_number_of_calls) % settings().m_hnf_cut_period == 0) {
+    if ((m_number_of_calls) % settings().hnf_cut_period() == 0) {
         return make_hnf_cut();
     }
     return lia_move::undef;

src/util/lp/lar_solver.cpp

@@ -2263,16 +2263,16 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
 }
 
 void lar_solver::set_cut_strategy(unsigned cut_frequency) {
-    if (cut_frequency < 4) { // enable only gomory cut
-        settings().m_int_gomory_cut_period = 2;
-        settings().m_hnf_cut_period = 100000000;
+    if (cut_frequency < 4) {
+        settings().m_int_gomory_cut_period = 2; // do it often
+        settings().set_hnf_cut_period(4); // also create hnf cuts
     } else if (cut_frequency == 4) { // enable all cuts and cube equally
         settings().m_int_gomory_cut_period = 4;
-        settings().m_hnf_cut_period = 4;
+        settings().set_hnf_cut_period(4);
     } else {
-        // disable all heuristics
+        // disable all heuristics except cube
         settings().m_int_gomory_cut_period = 10000000;
-        settings().m_hnf_cut_period = 100000000;
+        settings().set_hnf_cut_period(100000000);
     } 
 }
 

src/util/lp/lp_settings.h

@@ -189,13 +189,18 @@ public:
     unsigned         column_number_threshold_for_using_lu_in_lar_solver;
     unsigned         m_int_gomory_cut_period;
     unsigned         m_int_find_cube_period;
+private:
     unsigned         m_hnf_cut_period;
+public:
     bool             m_int_run_gcd_test;
     bool             m_int_pivot_fixed_vars_from_basis;
     bool             m_int_patch_only_integer_values;
     unsigned         limit_on_rows_for_hnf_cutter;
     unsigned         limit_on_columns_for_hnf_cutter;
 
+
+    unsigned hnf_cut_period() const { return m_hnf_cut_period; }
+    void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period;  }
     unsigned random_next() { return m_rand(); }
     void set_random_seed(unsigned s) { m_rand.set_seed(s); }
 

src/util/lp/lu.cpp

@@ -42,11 +42,11 @@ template void init_factorization<static_matrix<double, double>>
 template void init_factorization<static_matrix<mpq, mpq>>
     (lu<static_matrix<mpq,mpq>>*&, static_matrix<mpq, mpq>&, vector<unsigned int>&, lp_settings&);
 template void init_factorization<static_matrix<mpq, impq>>(lu<static_matrix<mpq, impq> >*&, static_matrix<mpq, impq >&, vector<unsigned int>&, lp_settings&);
-#ifdef Z3DEBUG
 template void print_matrix<square_sparse_matrix<double, double>>(square_sparse_matrix<double, double>&, std::ostream & out);
 template void print_matrix<static_matrix<mpq,mpq>>(static_matrix<mpq, mpq>&, std::ostream&);
 template void print_matrix<static_matrix<mpq, impq> >(static_matrix<mpq, impq >&, std::ostream&);
 template void print_matrix<static_matrix<double, double>>(static_matrix<double, double>&, std::ostream & out);
+#ifdef Z3DEBUG
 template bool lu<static_matrix<double, double>>::is_correct(const vector<unsigned>& basis);
 template bool lu<static_matrix<mpq, impq>>::is_correct( vector<unsigned int> const &);
 template dense_matrix<double, double> get_B<static_matrix<double, double>>(lu<static_matrix<double, double>>&, const vector<unsigned>& basis);

src/util/lp/lu.h

@@ -39,15 +39,12 @@ Revision History:
 #include "util/lp/square_dense_submatrix.h"
 #include "util/lp/dense_matrix.h"
 namespace lp {
-#ifdef Z3DEBUG
 template <typename T, typename X> // print the nr x nc submatrix at the top left corner
 void print_submatrix(square_sparse_matrix<T, X> & m, unsigned mr, unsigned nc);
 
 template <typename M>
 void print_matrix(M &m, std::ostream & out);
 
-#endif
-
 template <typename T, typename X>
 X dot_product(const vector<T> & a, const vector<X> & b) {
     lp_assert(a.size() == b.size());

src/util/lp/lu_def.h

@@ -25,7 +25,6 @@ Revision History:
 #include "util/debug.h"
 #include "util/lp/lu.h"
 namespace lp {
-#ifdef Z3DEBUG
 template <typename T, typename X, typename M> // print the nr x nc submatrix at the top left corner
 void print_submatrix(square_sparse_matrix<T, X> & m, unsigned mr, unsigned nc, std::ostream & out) {
     vector<vector<std::string>> A;
@@ -62,9 +61,6 @@ void print_matrix(M &m, std::ostream & out) {
     print_matrix_with_widths(A, widths, out);
 }
 
-#endif
-
-
 template <typename T, typename X>
 one_elem_on_diag<T, X>::one_elem_on_diag(const one_elem_on_diag & o) {
     m_i = o.m_i;

src/util/lp/matrix.cpp

@@ -18,14 +18,14 @@ Revision History:
 
 --*/
 #include "util/lp/lp_settings.h"
-#ifdef Z3DEBUG
 #include "util/lp/matrix_def.h"
 #include "util/lp/static_matrix.h"
 #include <string>
-template void lp::print_matrix<double, double>(lp::matrix<double, double> const*, std::ostream & out);
+#ifdef Z3DEBUG
 template bool lp::matrix<double, double>::is_equal(lp::matrix<double, double> const&);
-template void lp::print_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const *, std::basic_ostream<char, std::char_traits<char> > &);
-template void lp::print_matrix<lp::mpq, lp::mpq>(lp::matrix<lp::mpq, lp::mpq> const*, std::ostream&);
 template bool lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::is_equal(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const&);
 template bool lp::matrix<lp::mpq, lp::mpq>::is_equal(lp::matrix<lp::mpq, lp::mpq> const&);
 #endif
+template void lp::print_matrix<double, double>(lp::matrix<double, double> const*, std::ostream & out);
+template void lp::print_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const *, std::basic_ostream<char, std::char_traits<char> > &);
+template void lp::print_matrix<lp::mpq, lp::mpq>(lp::matrix<lp::mpq, lp::mpq> const*, std::ostream&);

src/util/lp/matrix.h

@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-#ifdef Z3DEBUG
 #pragma once
 #include "util/lp/numeric_pair.h"
 #include "util/vector.h"
@@ -70,4 +69,3 @@ void print_matrix(const vector<vector<T>> & A, std::ostream & out, unsigned blan
 
 
 }
-#endif

src/util/lp/matrix_def.h

@@ -18,11 +18,11 @@ Revision History:
 
 --*/
 
-#ifdef Z3DEBUG
 #include <cmath>
 #include <string>
 #include "util/lp/matrix.h"
 namespace lp {
+#ifdef Z3DEBUG
 template <typename T, typename X>
 bool matrix<T, X>::is_equal(const matrix<T, X>& other) {
     if (other.row_count() != row_count() || other.column_count() != column_count())
@@ -67,7 +67,7 @@ void apply_to_vector(matrix<T, X> & m, T * w) {
     delete [] wc;
 }
 
-
+#endif
 
 unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
     unsigned r = 0;
@@ -132,4 +132,3 @@ void print_matrix(matrix<T, X> const * m, std::ostream & out) {
 }
 
 }
-#endif

src/util/lp/square_sparse_matrix.h

@@ -40,9 +40,7 @@ namespace lp {
 // it is a square matrix
 template <typename T, typename X>
 class square_sparse_matrix
-#ifdef Z3DEBUG
     : public matrix<T, X>
-#endif
 {
     struct col_header {
         unsigned m_shortened_markovitz;
@@ -173,10 +171,8 @@ public:
 
     unsigned dimension() const {return static_cast<unsigned>(m_row_permutation.size());}
 
-#ifdef Z3DEBUG
     unsigned row_count() const override {return dimension();}
     unsigned column_count() const override {return dimension();}
-#endif
 
     void init_row_headers();
 
@@ -309,13 +305,11 @@ public:
     template <typename L>
     void solve_U_y_indexed_only(indexed_vector<L> & y, const lp_settings&, vector<unsigned> & sorted_active_rows );
 
-#ifdef Z3DEBUG
     T get_elem(unsigned i, unsigned j) const override { return get(i, j); }
     unsigned get_number_of_rows() const { return dimension(); }
     unsigned get_number_of_columns() const { return dimension(); }
     void set_number_of_rows(unsigned /*m*/) override { }
     void set_number_of_columns(unsigned /*n*/) override { }
-#endif
     template <typename L>
     L dot_product_with_row (unsigned row, const vector<L> & y) const;