mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
16b71fe911
Signed-off-by: Lev <levnach@hotmail.com> trying the new scheme in static_matrix : in progress Signed-off-by: Lev Nachmanson <levnach@hotmail.com> in the middle of changes in static_matrix Signed-off-by: Lev Nachmanson <levnach@hotmail.com> more fixes in static_matrix.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> debug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in static_matrix Signed-off-by: Lev <levnach@hotmail.com> fixes in static_matrix, column_strip Signed-off-by: Lev <levnach@hotmail.com> fixes in static_matrix Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes for static_matrix Signed-off-by: Lev <levnach@hotmail.com> work on static_matrix Signed-off-by: Lev <levnach@hotmail.com> work on static_matrix Signed-off-by: Lev <levnach@hotmail.com> progress in static_matrix Signed-off-by: Lev <levnach@hotmail.com> fix a bug in swap_with_head_cell Signed-off-by: Lev <levnach@hotmail.com> progress in static_matrix Signed-off-by: Lev <levnach@hotmail.com> compress rows and columns if needed Signed-off-by: Lev <levnach@hotmail.com> fix in compression of cells Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
84 lines
4.2 KiB
C++
84 lines
4.2 KiB
C++
/*++
|
|
Copyright (c) 2017 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
<name>
|
|
|
|
Abstract:
|
|
|
|
<abstract>
|
|
|
|
Author:
|
|
|
|
Lev Nachmanson (levnach)
|
|
|
|
Revision History:
|
|
|
|
|
|
--*/
|
|
#include <memory>
|
|
#include "util/vector.h"
|
|
#include <set>
|
|
#include <utility>
|
|
#include "util/lp/static_matrix_def.h"
|
|
#include "util/lp/lp_core_solver_base.h"
|
|
#include "util/lp/lp_dual_core_solver.h"
|
|
#include "util/lp/lp_dual_simplex.h"
|
|
#include "util/lp/lp_primal_core_solver.h"
|
|
#include "util/lp/scaler.h"
|
|
#include "util/lp/lar_solver.h"
|
|
namespace lp {
|
|
template void static_matrix<double, double>::add_columns_at_the_end(unsigned int);
|
|
template void static_matrix<double, double>::add_new_element(unsigned i, unsigned j, const double & v);
|
|
template void static_matrix<mpq, mpq>::add_new_element(unsigned i, unsigned j, const mpq & v);
|
|
template void static_matrix<mpq, impq>::add_new_element(unsigned i, unsigned j, const mpq & v);
|
|
template void static_matrix<double, double>::clear();
|
|
#ifdef Z3DEBUG
|
|
template bool static_matrix<double, double>::is_correct() const;
|
|
#endif
|
|
template void static_matrix<double, double>::copy_column_to_indexed_vector(unsigned int, indexed_vector<double>&) const;
|
|
|
|
template double static_matrix<double, double>::get_balance() const;
|
|
template std::set<std::pair<unsigned, unsigned>> static_matrix<double, double>::get_domain();
|
|
template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::mpq>::get_domain();
|
|
template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_domain();
|
|
template double static_matrix<double, double>::get_elem(unsigned int, unsigned int) const;
|
|
template double static_matrix<double, double>::get_max_abs_in_column(unsigned int) const;
|
|
template double static_matrix<double, double>::get_min_abs_in_column(unsigned int) const;
|
|
template double static_matrix<double, double>::get_min_abs_in_row(unsigned int) const;
|
|
template void static_matrix<double, double>::init_empty_matrix(unsigned int, unsigned int);
|
|
template void static_matrix<double, double>::init_row_columns(unsigned int, unsigned int);
|
|
template static_matrix<double, double>::ref & static_matrix<double, double>::ref::operator=(double const&);
|
|
template static_matrix<double, double>::static_matrix(unsigned int, unsigned int);
|
|
template void static_matrix<mpq, mpq>::add_column_to_vector(mpq const&, unsigned int, mpq*) const;
|
|
template void static_matrix<mpq, mpq>::add_columns_at_the_end(unsigned int);
|
|
template bool static_matrix<mpq, mpq>::is_correct() const;
|
|
template void static_matrix<mpq, mpq>::copy_column_to_indexed_vector(unsigned int, indexed_vector<mpq>&) const;
|
|
|
|
template mpq static_matrix<mpq, mpq>::get_balance() const;
|
|
template mpq static_matrix<mpq, mpq>::get_elem(unsigned int, unsigned int) const;
|
|
template mpq static_matrix<mpq, mpq>::get_max_abs_in_column(unsigned int) const;
|
|
template mpq static_matrix<mpq, mpq>::get_max_abs_in_row(unsigned int) const;
|
|
template double static_matrix<double, double>::get_max_abs_in_row(unsigned int) const;
|
|
template mpq static_matrix<mpq, mpq>::get_min_abs_in_column(unsigned int) const;
|
|
template mpq static_matrix<mpq, mpq>::get_min_abs_in_row(unsigned int) const;
|
|
template void static_matrix<mpq, mpq>::init_row_columns(unsigned int, unsigned int);
|
|
template static_matrix<mpq, mpq>::ref& static_matrix<mpq, mpq>::ref::operator=(mpq const&);
|
|
|
|
template static_matrix<mpq, mpq>::static_matrix(unsigned int, unsigned int);
|
|
#ifdef Z3DEBUG
|
|
template bool static_matrix<mpq, numeric_pair<mpq> >::is_correct() const;
|
|
#endif
|
|
template void static_matrix<mpq, numeric_pair<mpq> >::copy_column_to_indexed_vector(unsigned int, indexed_vector<mpq>&) const;
|
|
template mpq static_matrix<mpq, numeric_pair<mpq> >::get_elem(unsigned int, unsigned int) const;
|
|
template void static_matrix<mpq, numeric_pair<mpq> >::init_empty_matrix(unsigned int, unsigned int);
|
|
|
|
template bool lp::static_matrix<double, double>::pivot_row_to_row_given_cell(unsigned int, column_cell &, unsigned int);
|
|
template bool lp::static_matrix<lp::mpq, lp::mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
|
|
template bool lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
|
|
template void lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_element(lp::row_cell<lp::mpq>&);
|
|
|
|
}
|
|
|