more sparse

This commit is contained in:
chriseth 2022-08-13 19:06:38 +02:00
parent b82e1b2b04
commit d308cf8d96
3 changed files with 79 additions and 26 deletions

View File

@ -29,6 +29,7 @@
namespace solidity::util namespace solidity::util
{ {
using rational = boost::rational<bigint>;
using Model = std::map<std::string, rational>; using Model = std::map<std::string, rational>;
using ReasonSet = std::set<size_t>; using ReasonSet = std::set<size_t>;

View File

@ -18,7 +18,8 @@
#include <libsolutil/LinearExpression.h> #include <libsolutil/LinearExpression.h>
using solidity::util; using namespace solidity::util;
using namespace std;
void SparseMatrix::multiplyRowByFactor(size_t _row, rational const& _factor) void SparseMatrix::multiplyRowByFactor(size_t _row, rational const& _factor)
{ {
@ -53,9 +54,9 @@ void SparseMatrix::addMultipleOfRow(size_t _sourceRow, size_t _targetRow, ration
} }
} }
else if (!target) else if (!target)
target = appendToRow(_targetRow, source->col, _factor * source->value); target = appendToRow(_targetRow, source->col, _factor * source->value)->next_in_row;
else if (target->col > source->col) else
target = prependInRow(target, source->col, _factor * source->value); target = prependInRow(*target, source->col, _factor * source->value)->next_in_row;
source = source->next_in_row; source = source->next_in_row;
} }
@ -64,20 +65,17 @@ void SparseMatrix::addMultipleOfRow(size_t _sourceRow, size_t _targetRow, ration
void SparseMatrix::appendRow(LinearExpression const& _entries) void SparseMatrix::appendRow(LinearExpression const& _entries)
{ {
Entry* prev = nullptr; m_row_start.push_back(nullptr);
m_row_start.push(nullptr); m_row_end.push_back(nullptr);
m_row_end.push(nullptr);
size_t row_nr = m_row_start.size() - 1; size_t row_nr = m_row_start.size() - 1;
for (auto&& [i, v]: _entries.enumerate()) { for (auto&& [i, v]: _entries.enumerate()) {
if (!v) if (!v)
continue; continue;
prev = appendToRow(row_nr, i, move(v)); appendToRow(row_nr, i, move(v));
prev = curr;
} }
} }
void SparseMatrix::remove(Entry& _e) void SparseMatrix::remove(SparseMatrix::Entry& _e)
{ {
if (_e.prev_in_row) if (_e.prev_in_row)
_e.prev_in_row->next_in_row = _e.next_in_row; _e.prev_in_row->next_in_row = _e.next_in_row;
@ -97,28 +95,82 @@ void SparseMatrix::remove(Entry& _e)
m_col_end[_e.col] = _e.prev_in_col; m_col_end[_e.col] = _e.prev_in_col;
} }
void SparseMatrix::appendToRow(size_t _row, size_t _column, rational _value) SparseMatrix::Entry* SparseMatrix::appendToRow(size_t _row, size_t _column, rational _value)
{ {
m_elements.emplace(make_unique<Element>( // TODO could be combined with prependInRow
// with successor being nullptr
m_elements.emplace_back(make_unique<Entry>(Entry{
move(_value), move(_value),
_row, _row,
_column, _column,
m_row_end[_row], m_row_end[_row],
nullptr, nullptr,
m_column_end[i], nullptr,
nullptr nullptr
)); }));
Entry const* e = m_elements.back().get(); Entry* e = m_elements.back().get();
if (m_row_end[_row]) if (m_row_end[_row])
m_row_end[_row]->next_in_row = e; m_row_end[_row]->next_in_row = e;
m_row_end[_row] = e;
if (!m_row_start[_row]) if (!m_row_start[_row])
m_row_start[_row] = e; m_row_start[_row] = e;
if (i >= m_col_start.size())
m_col_start.resize(i + 1); adjustColumnProperties(*e);
if (!m_col_start[i]) return e;
m_col_start[i] = e; }
if (i >= m_col_end.size())
m_col_end.resize(i + 1); SparseMatrix::Entry* SparseMatrix::prependInRow(Entry& _successor, size_t _column, rational _value)
if (!m_col_end[i]) {
m_col_end[i] = e; size_t row = _successor.row;
m_elements.emplace_back(make_unique<Entry>(Entry{
move(_value),
row,
_column,
_successor.prev_in_row,
&_successor,
nullptr,
nullptr
}));
Entry* e = m_elements.back().get();
_successor.prev_in_row = e;
if (m_row_start[row] == &_successor)
m_row_start[row] = e;
adjustColumnProperties(*e);
return e;
}
void SparseMatrix::adjustColumnProperties(Entry& _entry)
{
size_t column = _entry.col;
if (column >= m_col_start.size())
{
m_col_start.resize(column + 1);
m_col_end.resize(column + 1);
}
Entry* c = nullptr;
if (m_col_end[column] && m_col_end[column]->row > _entry.row)
{
c = m_col_start[column];
// TODO could choose to search from end
while (c && c->row < _entry.row)
c = c->next_in_col;
}
_entry.next_in_col = c;
if (c)
{
_entry.prev_in_col = c->prev_in_col;
c->prev_in_col = &_entry;
}
else
{
_entry.prev_in_col = m_col_end[column];
m_col_end[column] = &_entry;
}
if (_entry.prev_in_col)
_entry.prev_in_col->next_in_col = &_entry;
else
m_col_start[column] = &_entry;
} }

View File

@ -17,8 +17,6 @@
// SPDX-License-Identifier: GPL-3.0 // SPDX-License-Identifier: GPL-3.0
#pragma once #pragma once
#include <libsolutil/LP.h>
#include <libsolutil/Common.h> #include <libsolutil/Common.h>
#include <libsolutil/CommonData.h> #include <libsolutil/CommonData.h>
#include <libsolutil/StringUtils.h> #include <libsolutil/StringUtils.h>
@ -214,6 +212,8 @@ private:
void remove(Entry& _entry); void remove(Entry& _entry);
Entry* appendToRow(size_t _row, size_t _column, rational _value); Entry* appendToRow(size_t _row, size_t _column, rational _value);
Entry* prependInRow(Entry& _successor, size_t _column, rational _value);
void adjustColumnProperties(Entry& _entry);
std::vector<std::unique_ptr<Entry>> m_elements; std::vector<std::unique_ptr<Entry>> m_elements;
std::vector<Entry*> m_row_start; std::vector<Entry*> m_row_start;