mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

more dead code

Browse source
This commit is contained in:
Lev Nachmanson 2023-03-07 17:52:59 -08:00
parent 13549aff66
commit 11eab94321
17 changed files with 10 additions and 1095 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/CMakeLists.txt
View file

@ -1,7 +1,5 @@
z3_add_component(lp
SOURCES
binary_heap_priority_queue.cpp
binary_heap_upair_queue.cpp
core_solver_pretty_printer.cpp
dense_matrix.cpp
emonics.cpp

38
src/math/lp/binary_heap_priority_queue.cpp
View file

@ -1,38 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#include "math/lp/numeric_pair.h"
#include "math/lp/binary_heap_priority_queue_def.h"
namespace lp {
template binary_heap_priority_queue<int>::binary_heap_priority_queue(unsigned int);
template unsigned binary_heap_priority_queue<int>::dequeue();
template void binary_heap_priority_queue<int>::enqueue(unsigned int, int const&);
template void binary_heap_priority_queue<mpq>::enqueue(unsigned int, mpq const&);
template void binary_heap_priority_queue<int>::remove(unsigned int);
template unsigned binary_heap_priority_queue<numeric_pair<mpq> >::dequeue();
template unsigned binary_heap_priority_queue<mpq>::dequeue();
template void binary_heap_priority_queue<numeric_pair<mpq> >::enqueue(unsigned int, numeric_pair<mpq> const&);
template void binary_heap_priority_queue<numeric_pair<mpq> >::resize(unsigned int);
template binary_heap_priority_queue<unsigned int>::binary_heap_priority_queue(unsigned int);
template void binary_heap_priority_queue<unsigned>::resize(unsigned int);
template unsigned binary_heap_priority_queue<unsigned int>::dequeue();
template void binary_heap_priority_queue<unsigned int>::enqueue(unsigned int, unsigned int const&);
template void binary_heap_priority_queue<unsigned int>::remove(unsigned int);
template void lp::binary_heap_priority_queue<mpq>::resize(unsigned int);
}

83
src/math/lp/binary_heap_priority_queue.h
View file

@ -1,83 +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 "math/lp/lp_utils.h"
namespace lp {
// the elements with the smallest priority are dequeued first
template <typename T>
class binary_heap_priority_queue {
vector<T> m_priorities;
// indexing for A starts from 1
vector<unsigned> m_heap; // keeps the elements of the queue
vector<int> m_heap_inverse; // o = m_heap[m_heap_inverse[o]]
unsigned m_heap_size;
// is is the child place in heap
void swap_with_parent(unsigned i);
void put_at(unsigned i, unsigned h);
void decrease_priority(unsigned o, T newPriority);
public:
#ifdef Z3DEBUG
bool is_consistent() const;
#endif
public:
void remove(unsigned o);
unsigned size() const { return m_heap_size; }
binary_heap_priority_queue(): m_heap(1), m_heap_size(0) {} // the empty constructror
// n is the initial queue capacity.
// The capacity will be enlarged each time twice if needed
binary_heap_priority_queue(unsigned n);
void clear() {
for (unsigned i = 0; i < m_heap_size; i++) {
unsigned o = m_heap[i+1];
m_heap_inverse[o] = -1;
}
m_heap_size = 0;
}
void resize(unsigned n);
void put_to_heap(unsigned i, unsigned o);
void enqueue_new(unsigned o, const T& priority);
// This method can work with an element that is already in the queue.
// In this case the priority will be changed and the queue adjusted.
void enqueue(unsigned o, const T & priority);
void change_priority_for_existing(unsigned o, const T & priority);
T get_priority(unsigned o) const { return m_priorities[o]; }
bool is_empty() const { return m_heap_size == 0; }
/// return the first element of the queue and removes it from the queue
unsigned dequeue_and_get_priority(T & priority);
void fix_heap_under(unsigned i);
void put_the_last_at_the_top_and_fix_the_heap();
/// return the first element of the queue and removes it from the queue
unsigned dequeue();
unsigned peek() const {
lp_assert(m_heap_size > 0);
return m_heap[1];
}
void print(std::ostream & out);
};
}

214
src/math/lp/binary_heap_priority_queue_def.h
View file

@ -1,214 +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/binary_heap_priority_queue.h"
namespace lp {
// "i" is the child's place in the heap
template <typename T> void binary_heap_priority_queue<T>::swap_with_parent(unsigned i) {
unsigned parent = m_heap[i >> 1];
put_at(i >> 1, m_heap[i]);
put_at(i, parent);
}
template <typename T> void binary_heap_priority_queue<T>::put_at(unsigned i, unsigned h) {
m_heap[i] = h;
m_heap_inverse[h] = i;
}
template <typename T> void binary_heap_priority_queue<T>::decrease_priority(unsigned o, T newPriority) {
m_priorities[o] = newPriority;
int i = m_heap_inverse[o];
while (i > 1) {
if (m_priorities[m_heap[i]] < m_priorities[m_heap[i >> 1]])
swap_with_parent(i);
else
break;
i >>= 1;
}
}
#ifdef Z3DEBUG
template <typename T> bool binary_heap_priority_queue<T>::is_consistent() const {
for (int i = 0; i < m_heap_inverse.size(); i++) {
int i_index = m_heap_inverse[i];
lp_assert(i_index <= static_cast<int>(m_heap_size));
lp_assert(i_index == -1 || m_heap[i_index] == i);
}
for (unsigned i = 1; i < m_heap_size; i++) {
unsigned ch = i << 1;
for (int k = 0; k < 2; k++) {
if (ch > m_heap_size) break;
if (!(m_priorities[m_heap[i]] <= m_priorities[m_heap[ch]])){
return false;
}
ch++;
}
}
return true;
}
#endif
template <typename T> void binary_heap_priority_queue<T>::remove(unsigned o) {
T priority_of_o = m_priorities[o];
int o_in_heap = m_heap_inverse[o];
if (o_in_heap == -1) {
return; // nothing to do
}
lp_assert(static_cast<unsigned>(o_in_heap) <= m_heap_size);
if (static_cast<unsigned>(o_in_heap) < m_heap_size) {
put_at(o_in_heap, m_heap[m_heap_size--]);
if (m_priorities[m_heap[o_in_heap]] > priority_of_o) {
fix_heap_under(o_in_heap);
} else { // we need to propagate the m_heap[o_in_heap] up
unsigned i = o_in_heap;
while (i > 1) {
unsigned ip = i >> 1;
if (m_priorities[m_heap[i]] < m_priorities[m_heap[ip]])
swap_with_parent(i);
else
break;
i = ip;
}
}
} else {
lp_assert(static_cast<unsigned>(o_in_heap) == m_heap_size);
m_heap_size--;
}
m_heap_inverse[o] = -1;
// lp_assert(is_consistent());
}
// n is the initial queue capacity.
// The capacity will be enlarged two times automatically if needed
template <typename T> binary_heap_priority_queue<T>::binary_heap_priority_queue(unsigned n) :
m_priorities(n),
m_heap(n + 1), // because the indexing for A starts from 1
m_heap_inverse(n, -1),
m_heap_size(0)
{ }
template <typename T> void binary_heap_priority_queue<T>::resize(unsigned n) {
m_priorities.resize(n);
m_heap.resize(n + 1);
m_heap_inverse.resize(n, -1);
}
template <typename T> void binary_heap_priority_queue<T>::put_to_heap(unsigned i, unsigned o) {
m_heap[i] = o;
m_heap_inverse[o] = i;
}
template <typename T> void binary_heap_priority_queue<T>::enqueue_new(unsigned o, const T& priority) {
m_heap_size++;
int i = m_heap_size;
lp_assert(o < m_priorities.size());
m_priorities[o] = priority;
put_at(i, o);
while (i > 1 && m_priorities[m_heap[i >> 1]] > priority) {
swap_with_parent(i);
i >>= 1;
}
}
// This method can work with an element that is already in the queue.
// In this case the priority will be changed and the queue adjusted.
template <typename T> void binary_heap_priority_queue<T>::enqueue(unsigned o, const T & priority) {
if (o >= m_priorities.size()) {
if (o == 0)
resize(2);
else
resize(o << 1); // make the size twice larger
}
if (m_heap_inverse[o] == -1)
enqueue_new(o, priority);
else
change_priority_for_existing(o, priority);
}
template <typename T> void binary_heap_priority_queue<T>::change_priority_for_existing(unsigned o, const T & priority) {
if (m_priorities[o] > priority) {
decrease_priority(o, priority);
} else {
m_priorities[o] = priority;
fix_heap_under(m_heap_inverse[o]);
}
}
/// return the first element of the queue and removes it from the queue
template <typename T> unsigned binary_heap_priority_queue<T>::dequeue_and_get_priority(T & priority) {
lp_assert(m_heap_size != 0);
int ret = m_heap[1];
priority = m_priorities[ret];
put_the_last_at_the_top_and_fix_the_heap();
return ret;
}
template <typename T> void binary_heap_priority_queue<T>::fix_heap_under(unsigned i) {
while (true) {
unsigned smallest = i;
unsigned l = i << 1;
if (l <= m_heap_size && m_priorities[m_heap[l]] < m_priorities[m_heap[i]])
smallest = l;
unsigned r = l + 1;
if (r <= m_heap_size && m_priorities[m_heap[r]] < m_priorities[m_heap[smallest]])
smallest = r;
if (smallest != i)
swap_with_parent(smallest);
else
break;
i = smallest;
}
}
template <typename T> void binary_heap_priority_queue<T>::put_the_last_at_the_top_and_fix_the_heap() {
if (m_heap_size > 1) {
put_at(1, m_heap[m_heap_size--]);
fix_heap_under(1);
} else {
m_heap_size--;
}
}
/// return the first element of the queue and removes it from the queue
template <typename T> unsigned binary_heap_priority_queue<T>::dequeue() {
lp_assert(m_heap_size > 0);
int ret = m_heap[1];
put_the_last_at_the_top_and_fix_the_heap();
m_heap_inverse[ret] = -1;
return ret;
}
template <typename T> void binary_heap_priority_queue<T>::print(std::ostream & out) {
vector<int> index;
vector<T> prs;
while (size()) {
T prior;
int j = dequeue_and_get_priority(prior);
index.push_back(j);
prs.push_back(prior);
out << "(" << j << ", " << prior << ")";
}
out << std::endl;
// restore the queue
for (int i = 0; i < index.size(); i++)
enqueue(index[i], prs[i]);
}
}

32
src/math/lp/binary_heap_upair_queue.cpp
View file

@ -1,32 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#include "math/lp/binary_heap_upair_queue_def.h"
namespace lp {
template binary_heap_upair_queue<int>::binary_heap_upair_queue(unsigned int);
template binary_heap_upair_queue<unsigned int>::binary_heap_upair_queue(unsigned int);
template unsigned binary_heap_upair_queue<int>::dequeue_available_spot();
template unsigned binary_heap_upair_queue<unsigned int>::dequeue_available_spot();
template void binary_heap_upair_queue<int>::enqueue(unsigned int, unsigned int, int const&);
template void binary_heap_upair_queue<int>::remove(unsigned int, unsigned int);
template void binary_heap_upair_queue<unsigned int>::remove(unsigned int, unsigned int);
template void binary_heap_upair_queue<int>::dequeue(unsigned int&, unsigned int&);
template void binary_heap_upair_queue<unsigned int>::enqueue(unsigned int, unsigned int, unsigned int const&);
template void binary_heap_upair_queue<unsigned int>::dequeue(unsigned int&, unsigned int&);
}

65
src/math/lp/binary_heap_upair_queue.h
View file

@ -1,65 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
#include <unordered_set>
#include <unordered_map>
#include <queue>
#include "util/vector.h"
#include <set>
#include <utility>
#include "math/lp/binary_heap_priority_queue.h"
typedef std::pair<unsigned, unsigned> upair;
namespace lp {
template <typename T>
class binary_heap_upair_queue {
binary_heap_priority_queue<T> m_q;
std::unordered_map<upair, unsigned> m_pairs_to_index;
svector<upair> m_pairs; // inverse to index
svector<unsigned> m_available_spots;
public:
binary_heap_upair_queue(unsigned size);
unsigned dequeue_available_spot();
bool is_empty() const { return m_q.is_empty(); }
unsigned size() const {return m_q.size(); }
bool contains(unsigned i, unsigned j) const { return m_pairs_to_index.find(std::make_pair(i, j)) != m_pairs_to_index.end();
}
void remove(unsigned i, unsigned j);
bool ij_index_is_new(unsigned ij_index) const;
void enqueue(unsigned i, unsigned j, const T & priority);
void dequeue(unsigned & i, unsigned &j);
T get_priority(unsigned i, unsigned j) const;
#ifdef Z3DEBUG
bool pair_to_index_is_a_bijection() const;
bool available_spots_are_correct() const;
bool is_correct() const {
return m_q.is_consistent() && pair_to_index_is_a_bijection() && available_spots_are_correct();
}
#endif
void resize(unsigned size) { m_q.resize(size); }
};
}

126
src/math/lp/binary_heap_upair_queue_def.h
View file

@ -1,126 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
#include <set>
#include "math/lp/lp_utils.h"
#include "math/lp/binary_heap_upair_queue.h"
namespace lp {
template <typename T> binary_heap_upair_queue<T>::binary_heap_upair_queue(unsigned size) : m_q(size), m_pairs(size) {
for (unsigned i = 0; i < size; i++)
m_available_spots.push_back(i);
}
template <typename T> unsigned
binary_heap_upair_queue<T>::dequeue_available_spot() {
lp_assert(m_available_spots.empty() == false);
unsigned ret = m_available_spots.back();
m_available_spots.pop_back();
return ret;
}
template <typename T> void binary_heap_upair_queue<T>::remove(unsigned i, unsigned j) {
upair p(i, j);
auto it = m_pairs_to_index.find(p);
if (it == m_pairs_to_index.end())
return; // nothing to do
m_q.remove(it->second);
m_available_spots.push_back(it->second);
m_pairs_to_index.erase(it);
}
template <typename T> bool binary_heap_upair_queue<T>::ij_index_is_new(unsigned ij_index) const {
for (auto it : m_pairs_to_index) {
if (it.second == ij_index)
return false;
}
return true;
}
template <typename T> void binary_heap_upair_queue<T>::enqueue(unsigned i, unsigned j, const T & priority) {
upair p(i, j);
auto it = m_pairs_to_index.find(p);
unsigned ij_index;
if (it == m_pairs_to_index.end()) {
// it is a new pair, let us find a spot for it
if (m_available_spots.empty()) {
// we ran out of empty spots
unsigned size_was = static_cast<unsigned>(m_pairs.size());
unsigned new_size = size_was << 1;
for (unsigned i = size_was; i < new_size; i++)
m_available_spots.push_back(i);
m_pairs.resize(new_size);
}
ij_index = dequeue_available_spot();
// lp_assert(ij_index<m_pairs.size() && ij_index_is_new(ij_index));
m_pairs[ij_index] = p;
m_pairs_to_index[p] = ij_index;
} else {
ij_index = it->second;
}
m_q.enqueue(ij_index, priority);
}
template <typename T> void binary_heap_upair_queue<T>::dequeue(unsigned & i, unsigned &j) {
lp_assert(!m_q.is_empty());
unsigned ij_index = m_q.dequeue();
upair & p = m_pairs[ij_index];
i = p.first;
j = p.second;
m_available_spots.push_back(ij_index);
m_pairs_to_index.erase(p);
}
template <typename T> T binary_heap_upair_queue<T>::get_priority(unsigned i, unsigned j) const {
auto it = m_pairs_to_index.find(std::make_pair(i, j));
if (it == m_pairs_to_index.end())
return T(0xFFFFFF); // big number
return m_q.get_priority(it->second);
}
#ifdef Z3DEBUG
template <typename T> bool binary_heap_upair_queue<T>::pair_to_index_is_a_bijection() const {
std::set<int> tmp;
for (auto p : m_pairs_to_index) {
unsigned j = p.second;
unsigned size = tmp.size();
tmp.insert(j);
if (tmp.size() == size)
return false;
}
return true;
}
template <typename T> bool binary_heap_upair_queue<T>::available_spots_are_correct() const {
std::set<int> tmp;
for (auto p : m_available_spots){
tmp.insert(p);
}
if (tmp.size() != m_available_spots.size())
return false;
for (auto it : m_pairs_to_index)
if (tmp.find(it.second) != tmp.end())
return false;
return true;
}
#endif
}

35
src/math/lp/conversion_helper.h
View file

@ -1,35 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
namespace lp {
template <typename V>
struct conversion_helper {
static V get_lower_bound(const column_info<mpq> & ci) {
return V(ci.get_lower_bound(), ci.lower_bound_is_strict()? 1 : 0);
}
static V get_upper_bound(const column_info<mpq> & ci) {
return V(ci.get_upper_bound(), ci.upper_bound_is_strict()? -1 : 0);
}
};
}

45
src/math/lp/indexer_of_constraints.h
View file

@ -1,45 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
#include "math/lp/binary_heap_priority_queue.h"
namespace lp {
class indexer_of_constraints {
binary_heap_priority_queue<unsigned> m_queue_of_released_indices;
unsigned m_max;
public:
indexer_of_constraints() :m_max(0) {}
unsigned get_new_index() {
unsigned ret;
if (m_queue_of_released_indices.is_empty()) {
ret = m_max++;
}
else {
ret = m_queue_of_released_indices.dequeue();
}
return ret;
};
void release_index(unsigned i) {
m_queue_of_released_indices.enqueue(i, i);
};
unsigned max() const { return m_max; }
};
}

1
src/math/lp/lar_core_solver.h
View file

@ -12,7 +12,6 @@ Author:
#include "math/lp/lp_core_solver_base.h"
#include <algorithm>
#include "math/lp/indexed_vector.h"
#include "math/lp/binary_heap_priority_queue.h"
#include "math/lp/lp_primal_core_solver.h"
#include "math/lp/stacked_vector.h"
#include "math/lp/lar_solution_signature.h"

1
src/math/lp/lar_solver.h
View file

@ -37,7 +37,6 @@
#include "math/lp/stacked_vector.h"
#include "math/lp/implied_bound.h"
#include "math/lp/bound_analyzer_on_row.h"
#include "math/lp/conversion_helper.h"
#include "math/lp/int_solver.h"
#include "math/lp/nra_solver.h"
#include "math/lp/lp_types.h"

1
src/math/lp/lp_primal_core_solver.h
View file

@ -32,7 +32,6 @@ Revision History:
#include "math/lp/static_matrix.h"
#include "math/lp/core_solver_pretty_printer.h"
#include "math/lp/lp_core_solver_base.h"
#include "math/lp/binary_heap_priority_queue.h"
#include "math/lp/u_set.h"
namespace lp {

23
src/math/lp/permutation_matrix.cpp
View file

@ -24,31 +24,8 @@ Revision History:
template void lp::permutation_matrix<lp::mpq, lp::mpq>::init(unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq>>::init(unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_from_right(vector<lp::mpq>&);
template bool lp::permutation_matrix<lp::mpq, lp::mpq>::is_identity() const;
template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_permutation_from_left(lp::permutation_matrix<lp::mpq, lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_permutation_from_right(lp::permutation_matrix<lp::mpq, lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_permutation_reverse_from_left(lp::permutation_matrix<lp::mpq, lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_reverse_from_right(lp::permutation_matrix<lp::mpq, lp::mpq>&);
template lp::permutation_matrix<lp::mpq, lp::mpq>::permutation_matrix(unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::transpose_from_left(unsigned int, unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::transpose_from_right(unsigned int, unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_right(vector<lp::mpq>&);
template bool lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::is_identity() const;
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_permutation_from_left(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_permutation_from_right(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_permutation_reverse_from_left(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_reverse_from_right(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
template lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::permutation_matrix(unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_from_left(unsigned int, unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_from_right(unsigned int, unsigned int);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_left<lp::mpq>(lp::indexed_vector<lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_left_to_T(vector<lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_right_to_T(vector<lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_left<lp::mpq>(lp::indexed_vector<lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_left_to_T(vector<lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_right_to_T(vector<lp::mpq >&);
template void lp::permutation_matrix< lp::mpq, lp::mpq>::apply_reverse_from_left_to_X(vector<lp::mpq> &);
template void lp::permutation_matrix< lp::mpq, lp::numeric_pair< lp::mpq> >::apply_reverse_from_left_to_X(vector<lp::numeric_pair< lp::mpq>> &);
template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_right_to_T(lp::indexed_vector<lp::mpq>&);
template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_right_to_T(lp::indexed_vector<lp::mpq>&);

61
src/math/lp/permutation_matrix.h
View file

@ -25,20 +25,16 @@ Revision History:
#include "math/lp/indexed_vector.h"
#include "math/lp/lp_settings.h"
#include "math/lp/matrix.h"
#include "math/lp/tail_matrix.h"
namespace lp {
#ifdef Z3DEBUG
inline bool is_even(int k) { return (k/2)*2 == k; }
#endif
template <typename T, typename X>
class permutation_matrix : public tail_matrix<T, X> {
template <typename T, typename X>
class permutation_matrix
#ifdef Z3DEBUG
: public matrix<T, X>
#endif
{
vector<unsigned> m_permutation;
vector<unsigned> m_rev;
vector<unsigned> m_work_array;
vector<T> m_T_buffer;
vector<X> m_X_buffer;
class ref {
permutation_matrix & m_p;
@ -63,42 +59,15 @@ class permutation_matrix : public tail_matrix<T, X> {
// create a unit permutation of the given length
void init(unsigned length);
unsigned get_rev(unsigned i) { return m_rev[i]; }
bool is_dense() const override { return false; }
#ifdef Z3DEBUG
permutation_matrix get_inverse() const {
return permutation_matrix(size(), m_rev);
}
#ifdef Z3DEBUG
void print(std::ostream & out) const;
#endif
ref operator[](unsigned i) { return ref(*this, i); }
unsigned operator[](unsigned i) const { return m_permutation[i]; }
void apply_from_left(vector<X> & w, lp_settings &) override;
void apply_from_left_to_T(indexed_vector<T> & w, lp_settings & settings) override;
void apply_from_right(vector<T> & w) override;
void apply_from_right(indexed_vector<T> & w) override;
template <typename L>
void copy_aside(vector<L> & t, vector<unsigned> & tmp_index, indexed_vector<L> & w);
template <typename L>
void clear_data(indexed_vector<L> & w);
template <typename L>
void apply_reverse_from_left(indexed_vector<L> & w);
void apply_reverse_from_left_to_T(vector<T> & w);
void apply_reverse_from_left_to_X(vector<X> & w);
void apply_reverse_from_right_to_T(vector<T> & w);
void apply_reverse_from_right_to_T(indexed_vector<T> & w);
void apply_reverse_from_right_to_X(vector<X> & w);
void set_val(unsigned i, unsigned pi) {
lp_assert(i < size() && pi < size()); m_permutation[i] = pi; m_rev[pi] = i; }
@ -116,18 +85,6 @@ class permutation_matrix : public tail_matrix<T, X> {
void set_number_of_rows(unsigned /*m*/) override { }
void set_number_of_columns(unsigned /*n*/) override { }
#endif
void multiply_by_permutation_from_left(permutation_matrix<T, X> & p);
// this is multiplication in the matrix sense
void multiply_by_permutation_from_right(permutation_matrix<T, X> & p);
void multiply_by_reverse_from_right(permutation_matrix<T, X> & q);
void multiply_by_permutation_reverse_from_left(permutation_matrix<T, X> & r);
void shrink_by_one_identity();
bool is_identity() const;
unsigned size() const { return static_cast<unsigned>(m_rev.size()); }
@ -135,8 +92,6 @@ class permutation_matrix : public tail_matrix<T, X> {
unsigned old_size = m_permutation.size();
m_permutation.resize(size);
m_rev.resize(size);
m_T_buffer.resize(size);
m_X_buffer.resize(size);
for (unsigned i = old_size; i < size; i++) {
m_permutation[i] = m_rev[i] = i;
}

261
src/math/lp/permutation_matrix_def.h
View file

@ -22,13 +22,13 @@ Revision History:
#include "util/vector.h"
#include "math/lp/permutation_matrix.h"
namespace lp {
template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length): m_permutation(length), m_rev(length), m_T_buffer(length), m_X_buffer(length) {
template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length): m_permutation(length), m_rev(length) {
for (unsigned i = 0; i < length; i++) { // do not change the direction of the loop because of the vectorization bug in clang3.3
m_permutation[i] = m_rev[i] = i;
}
}
template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length, vector<unsigned> const & values): m_permutation(length), m_rev(length) , m_T_buffer(length), m_X_buffer(length) {
template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length, vector<unsigned> const & values): m_permutation(length), m_rev(length) {
for (unsigned i = 0; i < length; i++) {
set_val(i, values[i]);
}
@ -37,8 +37,6 @@ template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(u
template <typename T, typename X> void permutation_matrix<T, X>::init(unsigned length) {
m_permutation.resize(length);
m_rev.resize(length);
m_T_buffer.resize(length);
m_X_buffer.resize(length);
for (unsigned i = 0; i < length; i++) {
m_permutation[i] = m_rev[i] = i;
}
@ -59,211 +57,6 @@ template <typename T, typename X> void permutation_matrix<T, X>::print(std::ostr
}
#endif
template <typename T, typename X>
void permutation_matrix<T, X>::apply_from_left(vector<X> & w, lp_settings & ) {
#ifdef Z3DEBUG
// dense_matrix<L, X> deb(*this);
// L * deb_w = clone_vector<L>(w, row_count());
// deb.apply_from_left(deb_w);
#endif
lp_assert(m_X_buffer.size() == w.size());
unsigned i = size();
while (i-- > 0) {
m_X_buffer[i] = w[m_permutation[i]];
}
i = size();
while (i-- > 0) {
w[i] = m_X_buffer[i];
}
#ifdef Z3DEBUG
// lp_assert(vectors_are_equal<L>(deb_w, w, row_count()));
// delete [] deb_w;
#endif
}
template <typename T, typename X>
void permutation_matrix<T, X>::apply_from_left_to_T(indexed_vector<T> & w, lp_settings & ) {
vector<T> t(w.m_index.size());
vector<unsigned> tmp_index(w.m_index.size());
copy_aside(t, tmp_index, w); // todo: is it too much copying
clear_data(w);
// set the new values
for (unsigned i = static_cast<unsigned>(t.size()); i > 0;) {
i--;
unsigned j = m_rev[tmp_index[i]];
w[j] = t[i];
w.m_index[i] = j;
}
}
template <typename T, typename X> void permutation_matrix<T, X>::apply_from_right(vector<T> & w) {
#ifdef Z3DEBUG
// dense_matrix<T, X> deb(*this);
// T * deb_w = clone_vector<T>(w, row_count());
// deb.apply_from_right(deb_w);
#endif
lp_assert(m_T_buffer.size() == w.size());
for (unsigned i = 0; i < size(); i++) {
m_T_buffer[i] = w[m_rev[i]];
}
for (unsigned i = 0; i < size(); i++) {
w[i] = m_T_buffer[i];
}
#ifdef Z3DEBUG
// lp_assert(vectors_are_equal<T>(deb_w, w, row_count()));
// delete [] deb_w;
#endif
}
template <typename T, typename X> void permutation_matrix<T, X>::apply_from_right(indexed_vector<T> & w) {
#ifdef Z3DEBUG
vector<T> wcopy(w.m_data);
apply_from_right(wcopy);
#endif
vector<T> buffer(w.m_index.size());
vector<unsigned> index_copy(w.m_index);
for (unsigned i = 0; i < w.m_index.size(); i++) {
buffer[i] = w.m_data[w.m_index[i]];
}
w.clear();
for (unsigned i = 0; i < index_copy.size(); i++) {
unsigned j = index_copy[i];
unsigned pj = m_permutation[j];
w.set_value(buffer[i], pj);
}
#ifdef Z3DEBUG
lp_assert(vectors_are_equal(wcopy, w.m_data));
#endif
}
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>::copy_aside(vector<L> & t, vector<unsigned> & tmp_index, indexed_vector<L> & w) {
for (unsigned i = static_cast<unsigned>(t.size()); i > 0;) {
i--;
unsigned j = w.m_index[i];
t[i] = w[j]; // copy aside all non-zeroes
tmp_index[i] = j; // and the indices too
}
}
template <typename T, typename X> template <typename L>
void permutation_matrix<T, X>::clear_data(indexed_vector<L> & w) {
// clear old non-zeroes
for (unsigned i = static_cast<unsigned>(w.m_index.size()); i > 0;) {
i--;
unsigned j = w.m_index[i];
w[j] = zero_of_type<L>();
}
}
template <typename T, typename X>template <typename L>
void permutation_matrix<T, X>::apply_reverse_from_left(indexed_vector<L> & w) {
// the result will be w = p(-1) * w
#ifdef Z3DEBUG
// dense_matrix<L, X> deb(get_reverse());
// L * deb_w = clone_vector<L>(w.m_data, row_count());
// deb.apply_from_left(deb_w);
#endif
vector<L> t(w.m_index.size());
vector<unsigned> tmp_index(w.m_index.size());
copy_aside(t, tmp_index, w);
clear_data(w);
// set the new values
for (unsigned i = static_cast<unsigned>(t.size()); i > 0;) {
i--;
unsigned j = m_permutation[tmp_index[i]];
w[j] = t[i];
w.m_index[i] = j;
}
#ifdef Z3DEBUG
// lp_assert(vectors_are_equal<L>(deb_w, w.m_data, row_count()));
// delete [] deb_w;
#endif
}
template <typename T, typename X>
void permutation_matrix<T, X>::apply_reverse_from_left_to_T(vector<T> & w) {
// the result will be w = p(-1) * w
lp_assert(m_T_buffer.size() == w.size());
unsigned i = size();
while (i-- > 0) {
m_T_buffer[m_permutation[i]] = w[i];
}
i = size();
while (i-- > 0) {
w[i] = m_T_buffer[i];
}
}
template <typename T, typename X>
void permutation_matrix<T, X>::apply_reverse_from_left_to_X(vector<X> & w) {
// the result will be w = p(-1) * w
lp_assert(m_X_buffer.size() == w.size());
unsigned i = size();
while (i-- > 0) {
m_X_buffer[m_permutation[i]] = w[i];
}
i = size();
while (i-- > 0) {
w[i] = m_X_buffer[i];
}
}
template <typename T, typename X>
void permutation_matrix<T, X>::apply_reverse_from_right_to_T(vector<T> & w) {
// the result will be w = w * p(-1)
lp_assert(m_T_buffer.size() == w.size());
unsigned i = size();
while (i-- > 0) {
m_T_buffer[i] = w[m_permutation[i]];
}
i = size();
while (i-- > 0) {
w[i] = m_T_buffer[i];
}
}
template <typename T, typename X>
void permutation_matrix<T, X>::apply_reverse_from_right_to_T(indexed_vector<T> & w) {
// the result will be w = w * p(-1)
#ifdef Z3DEBUG
// vector<T> wcopy(w.m_data);
// apply_reverse_from_right_to_T(wcopy);
#endif
vector<T> tmp;
vector<unsigned> tmp_index(w.m_index);
for (auto i : w.m_index) {
tmp.push_back(w[i]);
}
w.clear();
for (unsigned k = 0; k < tmp_index.size(); k++) {
unsigned j = tmp_index[k];
w.set_value(tmp[k], m_rev[j]);
}
}
template <typename T, typename X>
void permutation_matrix<T, X>::apply_reverse_from_right_to_X(vector<X> & w) {
// the result will be w = w * p(-1)
lp_assert(m_X_buffer.size() == w.size());
unsigned i = size();
while (i-- > 0) {
m_X_buffer[i] = w[m_permutation[i]];
}
i = size();
while (i-- > 0) {
w[i] = m_X_buffer[i];
}
}
template <typename T, typename X> void permutation_matrix<T, X>::transpose_from_left(unsigned i, unsigned j) {
// the result will be this = (i,j)*this
@ -283,55 +76,5 @@ template <typename T, typename X> void permutation_matrix<T, X>::transpose_from_
set_val(j, pi);
}
template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_permutation_from_left(permutation_matrix<T, X> & p) {
m_work_array = m_permutation;
lp_assert(p.size() == size());
unsigned i = size();
while (i-- > 0) {
set_val(i, m_work_array[p[i]]); // we have m(P)*m(Q) = m(QP), where m is the matrix of the permutation
}
}
// this is multiplication in the matrix sense
template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_permutation_from_right(permutation_matrix<T, X> & p) {
m_work_array = m_permutation;
lp_assert(p.size() == size());
unsigned i = size();
while (i-- > 0)
set_val(i, p[m_work_array[i]]); // we have m(P)*m(Q) = m(QP), where m is the matrix of the permutation
}
template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_reverse_from_right(permutation_matrix<T, X> & q){ // todo : condensed permutations ?
lp_assert(q.size() == size());
m_work_array = m_permutation;
// the result is this = this*q(-1)
unsigned i = size();
while (i-- > 0) {
set_val(i, q.m_rev[m_work_array[i]]); // we have m(P)*m(Q) = m(QP), where m is the matrix of the permutation
}
}
template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_permutation_reverse_from_left(permutation_matrix<T, X> & r){ // todo : condensed permutations?
// the result is this = r(-1)*this
m_work_array = m_permutation;
// the result is this = this*q(-1)
unsigned i = size();
while (i-- > 0) {
set_val(i, m_work_array[r.m_rev[i]]);
}
}
template <typename T, typename X> bool permutation_matrix<T, X>::is_identity() const {
unsigned i = size();
while (i-- > 0) {
if (m_permutation[i] != i) {
return false;
}
}
return true;
}
}

50
src/math/lp/tail_matrix.h
View file

@ -1,50 +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/indexed_vector.h"
#include "math/lp/matrix.h"
#include "math/lp/lp_settings.h"
// These matrices appear at the end of the list
namespace lp {
template <typename T, typename X>
class tail_matrix
#ifdef Z3DEBUG
: public matrix<T, X>
#endif
{
public:
virtual void apply_from_left_to_T(indexed_vector<T> & w, lp_settings & settings) = 0;
virtual void apply_from_left(vector<X> & w, lp_settings & settings) = 0;
virtual void apply_from_right(vector<T> & w) = 0;
virtual void apply_from_right(indexed_vector<T> & w) = 0;
virtual ~tail_matrix() = default;
virtual bool is_dense() const = 0;
struct ref_row {
const tail_matrix & m_A;
unsigned m_row;
ref_row(const tail_matrix& m, unsigned row): m_A(m), m_row(row) {}
T operator[](unsigned j) const { return m_A.get_elem(m_row, j);}
};
ref_row operator[](unsigned i) const { return ref_row(*this, i);}
};
}

67
src/test/lp/lp.cpp
View file

@ -34,13 +34,11 @@
#include <utility>
#include "math/lp/lp_utils.h"
#include "test/lp/smt_reader.h"
#include "math/lp/binary_heap_priority_queue.h"
#include "test/lp/argument_parser.h"
#include "test/lp/test_file_reader.h"
#include "math/lp/indexed_value.h"
#include "math/lp/lar_solver.h"
#include "math/lp/numeric_pair.h"
#include "math/lp/binary_heap_upair_queue.h"
#include "util/stacked_value.h"
#include "math/lp/u_set.h"
#include "util/stopwatch.h"
@ -458,72 +456,7 @@ void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, uns
void test_upair_queue() {
int n = 10;
binary_heap_upair_queue<int> q(2);
std::unordered_map<upair, int> m;
for (int k = 0; k < 100; k++) {
int i = my_random()%n;
int j = my_random()%n;
q.enqueue(i, j, my_random()%n);
}
q.remove(5, 5);
while (!q.is_empty()) {
unsigned i, j;
q.dequeue(i, j);
}
}
void test_binary_priority_queue() {
std::cout << "testing binary_heap_priority_queue...";
auto q = binary_heap_priority_queue<int>(10);
q.enqueue(2, 2);
q.enqueue(1, 1);
q.enqueue(9, 9);
q.enqueue(8, 8);
q.enqueue(5, 25);
q.enqueue(3, 3);
q.enqueue(4, 4);
q.enqueue(7, 30);
q.enqueue(6, 6);
q.enqueue(0, 0);
q.enqueue(5, 5);
q.enqueue(7, 7);
for (unsigned i = 0; i < 10; i++) {
unsigned de = q.dequeue();
lp_assert(i == de);
std::cout << de << std::endl;
}
q.enqueue(2, 2);
q.enqueue(1, 1);
q.enqueue(9, 9);
q.enqueue(8, 8);
q.enqueue(5, 5);
q.enqueue(3, 3);
q.enqueue(4, 4);
q.enqueue(7, 2);
q.enqueue(0, 1);
q.enqueue(6, 6);
q.enqueue(7, 7);
q.enqueue(33, 1000);
q.enqueue(20, 0);
q.dequeue();
q.remove(33);
q.enqueue(0, 0);
#ifdef Z3DEBUG
unsigned t = 0;
while (q.size() > 0) {
unsigned d =q.dequeue();
lp_assert(t++ == d);
std::cout << d << std::endl;
}
#endif
test_upair_queue();
std::cout << " done" << std::endl;
}
int get_random_rows() {