mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
more cleanup
This commit is contained in:
Lev Nachmanson
parent
0fb65dea3f
commit
f33f8c265e
|
|
@ -4,7 +4,6 @@ z3_add_component(lp
|
||||||
binary_heap_upair_queue.cpp
|
binary_heap_upair_queue.cpp
|
||||||
core_solver_pretty_printer.cpp
|
core_solver_pretty_printer.cpp
|
||||||
dense_matrix.cpp
|
dense_matrix.cpp
|
||||||
eta_matrix.cpp
|
|
||||||
emonics.cpp
|
emonics.cpp
|
||||||
factorization.cpp
|
factorization.cpp
|
||||||
factorization_factory_imp.cpp
|
factorization_factory_imp.cpp
|
||||||
|
|
@ -40,7 +39,6 @@ z3_add_component(lp
|
||||||
nra_solver.cpp
|
nra_solver.cpp
|
||||||
permutation_matrix.cpp
|
permutation_matrix.cpp
|
||||||
random_updater.cpp
|
random_updater.cpp
|
||||||
row_eta_matrix.cpp
|
|
||||||
static_matrix.cpp
|
static_matrix.cpp
|
||||||
COMPONENT_DEPENDENCIES
|
COMPONENT_DEPENDENCIES
|
||||||
util
|
util
|
||||||
|
|
|
||||||
|
|
@ -1,43 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#include <memory>
|
|
||||||
#include "util/vector.h"
|
|
||||||
#include "math/lp/numeric_pair.h"
|
|
||||||
#include "math/lp/eta_matrix_def.h"
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
template double lp::eta_matrix<double, double>::get_elem(unsigned int, unsigned int) const;
|
|
||||||
template lp::mpq lp::eta_matrix<lp::mpq, lp::mpq>::get_elem(unsigned int, unsigned int) const;
|
|
||||||
template lp::mpq lp::eta_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_elem(unsigned int, unsigned int) const;
|
|
||||||
#endif
|
|
||||||
template void lp::eta_matrix<double, double>::apply_from_left(vector<double>&, lp::lp_settings&);
|
|
||||||
template void lp::eta_matrix<double, double>::apply_from_right(vector<double>&);
|
|
||||||
template void lp::eta_matrix<double, double>::conjugate_by_permutation(lp::permutation_matrix<double, double>&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::mpq>::apply_from_left(vector<lp::mpq>&, lp::lp_settings&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::mpq>::apply_from_right(vector<lp::mpq>&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::mpq>::conjugate_by_permutation(lp::permutation_matrix<lp::mpq, lp::mpq>&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_left(vector<lp::numeric_pair<lp::mpq> >&, lp::lp_settings&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_right(vector<lp::mpq>&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::conjugate_by_permutation(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
|
|
||||||
template void lp::eta_matrix<double, double>::apply_from_left_local<double>(lp::indexed_vector<double>&, lp::lp_settings&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::mpq>::apply_from_left_local<lp::mpq>(lp::indexed_vector<lp::mpq>&, lp::lp_settings&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_left_local<lp::mpq>(lp::indexed_vector<lp::mpq>&, lp::lp_settings&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_right(lp::indexed_vector<lp::mpq>&);
|
|
||||||
template void lp::eta_matrix<lp::mpq, lp::mpq>::apply_from_right(lp::indexed_vector<lp::mpq>&);
|
|
||||||
template void lp::eta_matrix<double, double>::apply_from_right(lp::indexed_vector<double>&);
|
|
||||||
|
|
@ -1,98 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
#include "util/vector.h"
|
|
||||||
#include "math/lp/tail_matrix.h"
|
|
||||||
#include "math/lp/permutation_matrix.h"
|
|
||||||
namespace lp {
|
|
||||||
|
|
||||||
// This is the sum of a unit matrix and a one-column matrix
|
|
||||||
template <typename T, typename X>
|
|
||||||
class eta_matrix
|
|
||||||
: public tail_matrix<T, X> {
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
unsigned m_length;
|
|
||||||
#endif
|
|
||||||
unsigned m_column_index;
|
|
||||||
public:
|
|
||||||
sparse_vector<T> m_column_vector;
|
|
||||||
T m_diagonal_element;
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
eta_matrix(unsigned column_index, unsigned length):
|
|
||||||
#else
|
|
||||||
eta_matrix(unsigned column_index):
|
|
||||||
#endif
|
|
||||||
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
m_length(length),
|
|
||||||
#endif
|
|
||||||
m_column_index(column_index) {}
|
|
||||||
|
|
||||||
bool is_dense() const override { return false; }
|
|
||||||
|
|
||||||
void print(std::ostream & out) {
|
|
||||||
print_matrix(*this, out);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool is_unit() {
|
|
||||||
return m_column_vector.size() == 0 && m_diagonal_element == 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool set_diagonal_element(T const & diagonal_element) {
|
|
||||||
m_diagonal_element = diagonal_element;
|
|
||||||
return !lp_settings::is_eps_small_general(diagonal_element, 1e-12);
|
|
||||||
}
|
|
||||||
|
|
||||||
const T & get_diagonal_element() const {
|
|
||||||
return m_diagonal_element;
|
|
||||||
}
|
|
||||||
|
|
||||||
void apply_from_left(vector<X> & w, lp_settings & ) override;
|
|
||||||
|
|
||||||
template <typename L>
|
|
||||||
void apply_from_left_local(indexed_vector<L> & w, lp_settings & settings);
|
|
||||||
|
|
||||||
void apply_from_left_to_T(indexed_vector<T> & w, lp_settings & settings) override {
|
|
||||||
apply_from_left_local(w, settings);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void push_back(unsigned row_index, T val ) {
|
|
||||||
lp_assert(row_index != m_column_index);
|
|
||||||
m_column_vector.push_back(row_index, val);
|
|
||||||
}
|
|
||||||
|
|
||||||
void apply_from_right(vector<T> & w) override;
|
|
||||||
void apply_from_right(indexed_vector<T> & w) override;
|
|
||||||
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
T get_elem(unsigned i, unsigned j) const override;
|
|
||||||
unsigned row_count() const override { return m_length; }
|
|
||||||
unsigned column_count() const override { return m_length; }
|
|
||||||
void set_number_of_rows(unsigned m) override { m_length = m; }
|
|
||||||
void set_number_of_columns(unsigned n) override { m_length = n; }
|
|
||||||
#endif
|
|
||||||
void divide_by_diagonal_element() {
|
|
||||||
m_column_vector.divide(m_diagonal_element);
|
|
||||||
}
|
|
||||||
void conjugate_by_permutation(permutation_matrix<T, X> & p);
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
@ -1,151 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
#include "util/vector.h"
|
|
||||||
#include "math/lp/eta_matrix.h"
|
|
||||||
namespace lp {
|
|
||||||
|
|
||||||
// This is the sum of a unit matrix and a one-column matrix
|
|
||||||
template <typename T, typename X>
|
|
||||||
void eta_matrix<T, X>::apply_from_left(vector<X> & w, lp_settings & ) {
|
|
||||||
auto & w_at_column_index = w[m_column_index];
|
|
||||||
for (auto & it : m_column_vector.m_data) {
|
|
||||||
w[it.first] += w_at_column_index * it.second;
|
|
||||||
}
|
|
||||||
w_at_column_index /= m_diagonal_element;
|
|
||||||
}
|
|
||||||
template <typename T, typename X>
|
|
||||||
template <typename L>
|
|
||||||
void eta_matrix<T, X>::
|
|
||||||
apply_from_left_local(indexed_vector<L> & w, lp_settings & settings) {
|
|
||||||
const L w_at_column_index = w[m_column_index];
|
|
||||||
if (is_zero(w_at_column_index)) return;
|
|
||||||
|
|
||||||
if (settings.abs_val_is_smaller_than_drop_tolerance(w[m_column_index] /= m_diagonal_element)) {
|
|
||||||
w[m_column_index] = zero_of_type<L>();
|
|
||||||
w.erase_from_index(m_column_index);
|
|
||||||
}
|
|
||||||
|
|
||||||
for (auto & it : m_column_vector.m_data) {
|
|
||||||
unsigned i = it.first;
|
|
||||||
if (is_zero(w[i])) {
|
|
||||||
L v = w[i] = w_at_column_index * it.second;
|
|
||||||
if (settings.abs_val_is_smaller_than_drop_tolerance(v)) {
|
|
||||||
w[i] = zero_of_type<L>();
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
w.m_index.push_back(i);
|
|
||||||
} else {
|
|
||||||
L v = w[i] += w_at_column_index * it.second;
|
|
||||||
if (settings.abs_val_is_smaller_than_drop_tolerance(v)) {
|
|
||||||
w[i] = zero_of_type<L>();
|
|
||||||
w.erase_from_index(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
template <typename T, typename X>
|
|
||||||
void eta_matrix<T, X>::apply_from_right(vector<T> & w) {
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// dense_matrix<T, X> deb(*this);
|
|
||||||
// auto clone_w = clone_vector<T>(w, get_number_of_rows());
|
|
||||||
// deb.apply_from_right(clone_w);
|
|
||||||
#endif
|
|
||||||
T t = w[m_column_index] / m_diagonal_element;
|
|
||||||
for (auto & it : m_column_vector.m_data) {
|
|
||||||
t += w[it.first] * it.second;
|
|
||||||
}
|
|
||||||
w[m_column_index] = t;
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// lp_assert(vectors_are_equal<T>(clone_w, w, get_number_of_rows()));
|
|
||||||
// delete clone_w;
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
template <typename T, typename X>
|
|
||||||
void eta_matrix<T, X>::apply_from_right(indexed_vector<T> & w) {
|
|
||||||
if (w.m_index.empty())
|
|
||||||
return;
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// vector<T> wcopy(w.m_data);
|
|
||||||
// apply_from_right(wcopy);
|
|
||||||
#endif
|
|
||||||
T & t = w[m_column_index];
|
|
||||||
t /= m_diagonal_element;
|
|
||||||
bool was_in_index = (!numeric_traits<T>::is_zero(t));
|
|
||||||
|
|
||||||
for (auto & it : m_column_vector.m_data) {
|
|
||||||
t += w[it.first] * it.second;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (numeric_traits<T>::precise() ) {
|
|
||||||
if (!numeric_traits<T>::is_zero(t)) {
|
|
||||||
if (!was_in_index)
|
|
||||||
w.m_index.push_back(m_column_index);
|
|
||||||
} else {
|
|
||||||
if (was_in_index)
|
|
||||||
w.erase_from_index(m_column_index);
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
if (!lp_settings::is_eps_small_general(t, 1e-14)) {
|
|
||||||
if (!was_in_index)
|
|
||||||
w.m_index.push_back(m_column_index);
|
|
||||||
} else {
|
|
||||||
if (was_in_index)
|
|
||||||
w.erase_from_index(m_column_index);
|
|
||||||
t = zero_of_type<T>();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// lp_assert(w.is_OK());
|
|
||||||
// lp_assert(vectors_are_equal<T>(wcopy, w.m_data));
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
template <typename T, typename X>
|
|
||||||
T eta_matrix<T, X>::get_elem(unsigned i, unsigned j) const {
|
|
||||||
if (j == m_column_index){
|
|
||||||
if (i == j) {
|
|
||||||
return 1 / m_diagonal_element;
|
|
||||||
}
|
|
||||||
return m_column_vector[i];
|
|
||||||
}
|
|
||||||
|
|
||||||
return i == j ? numeric_traits<T>::one() : numeric_traits<T>::zero();
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
template <typename T, typename X>
|
|
||||||
void eta_matrix<T, X>::conjugate_by_permutation(permutation_matrix<T, X> & p) {
|
|
||||||
// this = p * this * p(-1)
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// auto rev = p.get_reverse();
|
|
||||||
// auto deb = ((*this) * rev);
|
|
||||||
// deb = p * deb;
|
|
||||||
#endif
|
|
||||||
m_column_index = p.get_rev(m_column_index);
|
|
||||||
for (auto & pair : m_column_vector.m_data) {
|
|
||||||
pair.first = p.get_rev(pair.first);
|
|
||||||
}
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// lp_assert(deb == *this);
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,47 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#include <memory>
|
|
||||||
#include "util/vector.h"
|
|
||||||
#include "math/lp/row_eta_matrix_def.h"
|
|
||||||
namespace lp {
|
|
||||||
template void row_eta_matrix<double, double>::conjugate_by_permutation(permutation_matrix<double, double>&);
|
|
||||||
template void row_eta_matrix<mpq, numeric_pair<mpq> >::conjugate_by_permutation(permutation_matrix<mpq, numeric_pair<mpq> >&);
|
|
||||||
template void row_eta_matrix<mpq, mpq>::conjugate_by_permutation(permutation_matrix<mpq, mpq>&);
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
template mpq row_eta_matrix<mpq, mpq>::get_elem(unsigned int, unsigned int) const;
|
|
||||||
template mpq row_eta_matrix<mpq, numeric_pair<mpq> >::get_elem(unsigned int, unsigned int) const;
|
|
||||||
template double row_eta_matrix<double, double>::get_elem(unsigned int, unsigned int) const;
|
|
||||||
#endif
|
|
||||||
template void row_eta_matrix<mpq, mpq>::apply_from_left(vector<mpq>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<mpq, mpq>::apply_from_right(vector<mpq>&);
|
|
||||||
template void row_eta_matrix<mpq, mpq>::apply_from_right(indexed_vector<mpq>&);
|
|
||||||
template void row_eta_matrix<mpq, numeric_pair<mpq> >::apply_from_left(vector<numeric_pair<mpq>>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<mpq, numeric_pair<mpq> >::apply_from_right(vector<mpq>&);
|
|
||||||
template void row_eta_matrix<mpq, numeric_pair<mpq> >::apply_from_right(indexed_vector<mpq>&);
|
|
||||||
template void row_eta_matrix<double, double>::apply_from_left(vector<double>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<double, double>::apply_from_right(vector<double>&);
|
|
||||||
template void row_eta_matrix<double, double>::apply_from_right(indexed_vector<double>&);
|
|
||||||
template void row_eta_matrix<mpq, mpq>::apply_from_left_to_T(indexed_vector<mpq>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<mpq, mpq>::apply_from_left_local_to_T(indexed_vector<mpq>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<mpq, numeric_pair<mpq> >::apply_from_left_to_T(indexed_vector<mpq>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<mpq, numeric_pair<mpq> >::apply_from_left_local_to_T(indexed_vector<mpq>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<double, double>::apply_from_left_to_T(indexed_vector<double>&, lp_settings&);
|
|
||||||
template void row_eta_matrix<double, double>::apply_from_left_local_to_T(indexed_vector<double>&, lp_settings&);
|
|
||||||
}
|
|
||||||
|
|
@ -1,89 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
#include "util/vector.h"
|
|
||||||
#include "util/debug.h"
|
|
||||||
#include <string>
|
|
||||||
#include "math/lp/sparse_vector.h"
|
|
||||||
#include "math/lp/indexed_vector.h"
|
|
||||||
#include "math/lp/permutation_matrix.h"
|
|
||||||
namespace lp {
|
|
||||||
// This is the sum of a unit matrix and a lower triangular matrix
|
|
||||||
// with non-zero elements only in one row
|
|
||||||
template <typename T, typename X>
|
|
||||||
class row_eta_matrix
|
|
||||||
: public tail_matrix<T, X> {
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
unsigned m_dimension;
|
|
||||||
#endif
|
|
||||||
unsigned m_row_start;
|
|
||||||
unsigned m_row;
|
|
||||||
sparse_vector<T> m_row_vector;
|
|
||||||
public:
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
row_eta_matrix(unsigned row_start, unsigned row, unsigned dim):
|
|
||||||
#else
|
|
||||||
row_eta_matrix(unsigned row_start, unsigned row):
|
|
||||||
#endif
|
|
||||||
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
m_dimension(dim),
|
|
||||||
#endif
|
|
||||||
m_row_start(row_start), m_row(row) {
|
|
||||||
}
|
|
||||||
|
|
||||||
bool is_dense() const override { return false; }
|
|
||||||
|
|
||||||
void print(std::ostream & out) {
|
|
||||||
print_matrix(*this, out);
|
|
||||||
}
|
|
||||||
|
|
||||||
const T & get_diagonal_element() const {
|
|
||||||
return m_row_vector.m_data[m_row];
|
|
||||||
}
|
|
||||||
|
|
||||||
void apply_from_left(vector<X> & w, lp_settings &) override;
|
|
||||||
|
|
||||||
void apply_from_left_local_to_T(indexed_vector<T> & w, lp_settings & settings);
|
|
||||||
void apply_from_left_local_to_X(indexed_vector<X> & w, lp_settings & settings);
|
|
||||||
|
|
||||||
void apply_from_left_to_T(indexed_vector<T> & w, lp_settings & settings) override {
|
|
||||||
apply_from_left_local_to_T(w, settings);
|
|
||||||
}
|
|
||||||
|
|
||||||
void push_back(unsigned row_index, T val ) {
|
|
||||||
lp_assert(row_index != m_row);
|
|
||||||
m_row_vector.push_back(row_index, val);
|
|
||||||
}
|
|
||||||
|
|
||||||
void apply_from_right(vector<T> & w) override;
|
|
||||||
void apply_from_right(indexed_vector<T> & w) override;
|
|
||||||
|
|
||||||
void conjugate_by_permutation(permutation_matrix<T, X> & p);
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
T get_elem(unsigned row, unsigned col) const override;
|
|
||||||
unsigned row_count() const override { return m_dimension; }
|
|
||||||
unsigned column_count() const override { return m_dimension; }
|
|
||||||
void set_number_of_rows(unsigned m) override { m_dimension = m; }
|
|
||||||
void set_number_of_columns(unsigned n) override { m_dimension = n; }
|
|
||||||
#endif
|
|
||||||
}; // end of row_eta_matrix
|
|
||||||
}
|
|
||||||
|
|
@ -1,188 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#pragma once
|
|
||||||
|
|
||||||
#include "util/vector.h"
|
|
||||||
#include "math/lp/row_eta_matrix.h"
|
|
||||||
namespace lp {
|
|
||||||
template <typename T, typename X>
|
|
||||||
void row_eta_matrix<T, X>::apply_from_left(vector<X> & w, lp_settings &) {
|
|
||||||
// #ifdef Z3DEBUG
|
|
||||||
// dense_matrix<T> deb(*this);
|
|
||||||
// auto clone_w = clone_vector<T>(w, m_dimension);
|
|
||||||
// deb.apply_from_left(clone_w, settings);
|
|
||||||
// #endif
|
|
||||||
|
|
||||||
auto & w_at_row = w[m_row];
|
|
||||||
for (auto & it : m_row_vector.m_data) {
|
|
||||||
w_at_row += w[it.first] * it.second;
|
|
||||||
}
|
|
||||||
// w[m_row] = w_at_row;
|
|
||||||
// #ifdef Z3DEBUG
|
|
||||||
// lp_assert(vectors_are_equal<T>(clone_w, w, m_dimension));
|
|
||||||
// delete [] clone_w;
|
|
||||||
// #endif
|
|
||||||
}
|
|
||||||
|
|
||||||
template <typename T, typename X>
|
|
||||||
void row_eta_matrix<T, X>::apply_from_left_local_to_T(indexed_vector<T> & w, lp_settings & settings) {
|
|
||||||
auto w_at_row = w[m_row];
|
|
||||||
bool was_zero_at_m_row = is_zero(w_at_row);
|
|
||||||
|
|
||||||
for (auto & it : m_row_vector.m_data) {
|
|
||||||
w_at_row += w[it.first] * it.second;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (!settings.abs_val_is_smaller_than_drop_tolerance(w_at_row)){
|
|
||||||
if (was_zero_at_m_row) {
|
|
||||||
w.m_index.push_back(m_row);
|
|
||||||
}
|
|
||||||
w[m_row] = w_at_row;
|
|
||||||
} else if (!was_zero_at_m_row){
|
|
||||||
w[m_row] = zero_of_type<T>();
|
|
||||||
auto it = std::find(w.m_index.begin(), w.m_index.end(), m_row);
|
|
||||||
w.m_index.erase(it);
|
|
||||||
}
|
|
||||||
// TBD: lp_assert(check_vector_for_small_values(w, settings));
|
|
||||||
}
|
|
||||||
|
|
||||||
template <typename T, typename X>
|
|
||||||
void row_eta_matrix<T, X>::apply_from_left_local_to_X(indexed_vector<X> & w, lp_settings & settings) {
|
|
||||||
auto w_at_row = w[m_row];
|
|
||||||
bool was_zero_at_m_row = is_zero(w_at_row);
|
|
||||||
|
|
||||||
for (auto & it : m_row_vector.m_data) {
|
|
||||||
w_at_row += w[it.first] * it.second;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (!settings.abs_val_is_smaller_than_drop_tolerance(w_at_row)){
|
|
||||||
if (was_zero_at_m_row) {
|
|
||||||
w.m_index.push_back(m_row);
|
|
||||||
}
|
|
||||||
w[m_row] = w_at_row;
|
|
||||||
} else if (!was_zero_at_m_row){
|
|
||||||
w[m_row] = zero_of_type<X>();
|
|
||||||
auto it = std::find(w.m_index.begin(), w.m_index.end(), m_row);
|
|
||||||
w.m_index.erase(it);
|
|
||||||
}
|
|
||||||
// TBD: does not compile lp_assert(check_vector_for_small_values(w, settings));
|
|
||||||
}
|
|
||||||
|
|
||||||
template <typename T, typename X>
|
|
||||||
void row_eta_matrix<T, X>::apply_from_right(vector<T> & w) {
|
|
||||||
const T & w_row = w[m_row];
|
|
||||||
if (numeric_traits<T>::is_zero(w_row)) return;
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// dense_matrix<T> deb(*this);
|
|
||||||
// auto clone_w = clone_vector<T>(w, m_dimension);
|
|
||||||
// deb.apply_from_right(clone_w);
|
|
||||||
#endif
|
|
||||||
for (auto & it : m_row_vector.m_data) {
|
|
||||||
w[it.first] += w_row * it.second;
|
|
||||||
}
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// lp_assert(vectors_are_equal<T>(clone_w, w, m_dimension));
|
|
||||||
// delete clone_w;
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
|
|
||||||
template <typename T, typename X>
|
|
||||||
void row_eta_matrix<T, X>::apply_from_right(indexed_vector<T> & w) {
|
|
||||||
lp_assert(w.is_OK());
|
|
||||||
const T & w_row = w[m_row];
|
|
||||||
if (numeric_traits<T>::is_zero(w_row)) return;
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// vector<T> wcopy(w.m_data);
|
|
||||||
// apply_from_right(wcopy);
|
|
||||||
#endif
|
|
||||||
if (numeric_traits<T>::precise()) {
|
|
||||||
for (auto & it : m_row_vector.m_data) {
|
|
||||||
unsigned j = it.first;
|
|
||||||
bool was_zero = numeric_traits<T>::is_zero(w[j]);
|
|
||||||
const T & v = w[j] += w_row * it.second;
|
|
||||||
|
|
||||||
if (was_zero) {
|
|
||||||
if (!numeric_traits<T>::is_zero(v))
|
|
||||||
w.m_index.push_back(j);
|
|
||||||
} else {
|
|
||||||
if (numeric_traits<T>::is_zero(v))
|
|
||||||
w.erase_from_index(j);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
} else { // the non precise version
|
|
||||||
const double drop_eps = 1e-14;
|
|
||||||
for (auto & it : m_row_vector.m_data) {
|
|
||||||
unsigned j = it.first;
|
|
||||||
bool was_zero = numeric_traits<T>::is_zero(w[j]);
|
|
||||||
T & v = w[j] += w_row * it.second;
|
|
||||||
|
|
||||||
if (was_zero) {
|
|
||||||
if (!lp_settings::is_eps_small_general(v, drop_eps))
|
|
||||||
w.m_index.push_back(j);
|
|
||||||
else
|
|
||||||
v = zero_of_type<T>();
|
|
||||||
} else {
|
|
||||||
if (lp_settings::is_eps_small_general(v, drop_eps)) {
|
|
||||||
w.erase_from_index(j);
|
|
||||||
v = zero_of_type<T>();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// lp_assert(vectors_are_equal(wcopy, w.m_data));
|
|
||||||
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
|
|
||||||
template <typename T, typename X>
|
|
||||||
void row_eta_matrix<T, X>::conjugate_by_permutation(permutation_matrix<T, X> & p) {
|
|
||||||
// this = p * this * p(-1)
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// auto rev = p.get_reverse();
|
|
||||||
// auto deb = ((*this) * rev);
|
|
||||||
// deb = p * deb;
|
|
||||||
#endif
|
|
||||||
m_row = p.apply_reverse(m_row);
|
|
||||||
// copy aside the column indices
|
|
||||||
vector<unsigned> columns;
|
|
||||||
for (auto & it : m_row_vector.m_data)
|
|
||||||
columns.push_back(it.first);
|
|
||||||
for (unsigned i = static_cast<unsigned>(columns.size()); i-- > 0;)
|
|
||||||
m_row_vector.m_data[i].first = p.get_rev(columns[i]);
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
// lp_assert(deb == *this);
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
template <typename T, typename X>
|
|
||||||
T row_eta_matrix<T, X>::get_elem(unsigned row, unsigned col) const {
|
|
||||||
if (row == m_row){
|
|
||||||
if (col == row) {
|
|
||||||
return numeric_traits<T>::one();
|
|
||||||
}
|
|
||||||
return m_row_vector[col];
|
|
||||||
}
|
|
||||||
|
|
||||||
return col == row ? numeric_traits<T>::one() : numeric_traits<T>::zero();
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
@ -622,66 +622,8 @@ void test_dense_matrix() {
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
|
||||||
vector<permutation_matrix<double, double>> vector_of_permutations() {
|
|
||||||
vector<permutation_matrix<double, double>> ret;
|
|
||||||
{
|
|
||||||
permutation_matrix<double, double> p0(5);
|
|
||||||
p0[0] = 1; p0[1] = 2; p0[2] = 3; p0[3] = 4;
|
|
||||||
p0[4] = 0;
|
|
||||||
ret.push_back(p0);
|
|
||||||
}
|
|
||||||
{
|
|
||||||
permutation_matrix<double, double> p0(5);
|
|
||||||
p0[0] = 2; p0[1] = 0; p0[2] = 1; p0[3] = 4;
|
|
||||||
p0[4] = 3;
|
|
||||||
ret.push_back(p0);
|
|
||||||
}
|
|
||||||
return ret;
|
|
||||||
}
|
|
||||||
|
|
||||||
void test_apply_reverse_from_right_to_perm(permutation_matrix<double, double> & l) {
|
|
||||||
permutation_matrix<double, double> p(5);
|
|
||||||
p[0] = 4; p[1] = 2; p[2] = 0; p[3] = 3;
|
|
||||||
p[4] = 1;
|
|
||||||
|
|
||||||
permutation_matrix<double, double> pclone(5);
|
|
||||||
pclone[0] = 4; pclone[1] = 2; pclone[2] = 0; pclone[3] = 3;
|
|
||||||
pclone[4] = 1;
|
|
||||||
|
|
||||||
p.multiply_by_reverse_from_right(l);
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
auto rev = l.get_inverse();
|
|
||||||
auto rs = pclone * rev;
|
|
||||||
lp_assert(p == rs)
|
|
||||||
#endif
|
|
||||||
}
|
|
||||||
|
|
||||||
void test_apply_reverse_from_right() {
|
|
||||||
auto vec = vector_of_permutations();
|
|
||||||
for (unsigned i = 0; i < vec.size(); i++) {
|
|
||||||
test_apply_reverse_from_right_to_perm(vec[i]);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void test_permutations() {
|
|
||||||
std::cout << "test permutations" << std::endl;
|
|
||||||
test_apply_reverse_from_right();
|
|
||||||
vector<double> v; v.resize(5, 0);
|
|
||||||
v[1] = 1;
|
|
||||||
v[3] = 3;
|
|
||||||
permutation_matrix<double, double> p(5);
|
|
||||||
p[0] = 4; p[1] = 2; p[2] = 0; p[3] = 3;
|
|
||||||
p[4] = 1;
|
|
||||||
|
|
||||||
indexed_vector<double> vi(5);
|
|
||||||
vi.set_value(1, 1);
|
|
||||||
vi.set_value(3, 3);
|
|
||||||
|
|
||||||
p.apply_reverse_from_right_to_T(v);
|
|
||||||
p.apply_reverse_from_right_to_T(vi);
|
|
||||||
lp_assert(vectors_are_equal(v, vi.m_data));
|
|
||||||
lp_assert(vi.is_OK());
|
|
||||||
}
|
|
||||||
|
|
||||||
void lp_solver_test() {
|
void lp_solver_test() {
|
||||||
// lp_revised_solver<double> lp_revised;
|
// lp_revised_solver<double> lp_revised;
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue