Commit 354c2407 authored by ehebrard's avatar ehebrard
Browse files

ok sched

parent 480127dd
......@@ -18,18 +18,16 @@ DistanceGraph are also explainers, for the transitivity
The static object "NoReason" is the empty reason
*/
void Explainer_::xplain(const hint h, vector<lit> &Cl) const {};
void Explainer::xplain(const hint h, vector<lit> &Cl) const {};
ostream &Explainer_::print_reason(ostream &os, const hint h) const {
os << "no reason";
return os;
ostream &Explainer::print_reason(ostream &os, const hint h) const {
os << "no reason";
return os;
}
void Explanation_::get(vector<lit> &Cl) const {
expl->xplain(the_hint, Cl);
}
void Explanation::get(vector<lit> &Cl) const { expl->xplain(the_hint, Cl); }
ostream &Explanation_::display(ostream &os) const {
ostream &Explanation::display(ostream &os) const {
assert(expl != NULL);
......@@ -38,12 +36,12 @@ ostream &Explainer_::print_reason(ostream &os, const hint h) const {
return os;
}
Explanation_::Explanation_(Explainer_ *e, hint h) : expl(e), the_hint(h) {}
Explanation::Explanation(Explainer *e, hint h) : expl(e), the_hint(h) {}
Explanation_ Constant_::NoReason = Explanation_(new Explainer_(), NoHint);
Explanation Constant::NoReason = Explanation(new Explainer(), NoHint);
ostream &operator<<(ostream &os, const Explanation_ &x) {
return x.display(os);
ostream &operator<<(ostream &os, const Explanation &x) {
return x.display(os);
}
......@@ -19,9 +19,14 @@ void Graph::addArc(const int u, const int v) {
verify("add arc");
#endif
}
// cout << edges << endl;
}
void Graph::add(Arc a) {
// cout << "add (" << a[0] << "," << a[1] << ")\n";
for (auto l{SUCCESSOR}; l <= PREDECESSOR; ++l) {
neighbor_rank[l][a[l]].push_back(
......@@ -39,6 +44,8 @@ void Graph::add(Arc a) {
bool Graph::has(const int u, const int v) const { return edges.has(u, v); }
void Graph::removeVertex(const int u) {
// cout << edges << endl;
ReversibleObject::save();
trail.push_back(u);
......@@ -50,10 +57,12 @@ void Graph::removeVertex(const int u) {
}
}
vertices.remove_back(u);
vertices.remove_front(u);
// cout << "removed " << u << endl << *this << endl;
// cout << edges << endl;
#ifdef DEBUG_SG
// cout << *this << endl;
verify("remove vertex");
......@@ -183,6 +192,8 @@ void Graph::recall(const int u) {
}
vertices.add(u);
// cout << *this << endl;
// exit(1);
......@@ -201,6 +212,9 @@ void Graph::recall(const int u) {
}
void Graph::undo(Arc a) {
// cout << "undo (" << a[0] << "," << a[1] << ")\n" ; //<< *this << endl;
for (auto l{SUCCESSOR}; l <= PREDECESSOR; ++l) {
assert(neighbor[l][a[l]].back() == a[1 - l]);
......@@ -225,9 +239,12 @@ void Graph::resize(const int n) {
neighbor_rank[SUCCESSOR].resize(n);
vertices.reserve(n);
vertices.fill();
vertices.fill_back();
// cout << "before resize " << edges << endl;
edges.resize(this->vertices, this->neighbor[SUCCESSOR]);
// cout << "after resize " << edges << endl;
}
#ifdef DEBUG_SG
......@@ -245,7 +262,9 @@ size_t Graph::size() const { return vertices.capacity(); }
//
void Graph::merge(const int u, const int v) {
// cout << *this << "\nMERGE " << v << " TO " << u << endl;
// cout
// //<< *this << "\n"
// << "merge " << v << " to " << u << endl;
removeVertex(v);
......@@ -309,7 +328,7 @@ void Graph::merge(const int u, const int v) {
}
}
// cout << *this << endl;
// cout << vertices << endl;
}
// restore to the last saved state
......@@ -317,6 +336,9 @@ void Graph::undo() {
auto v{trail.back()};
trail.pop_back();
// cout << "trail.back(): " << v << " " << vertices.has(v) << " " << vertices << endl;
if (vertices.has(v)) {
......@@ -327,11 +349,13 @@ void Graph::undo() {
} else {
// cout << "undo rm " << v << endl << *this << endl;
// cout << "undo rm " << v << endl ; //<< *this << endl;
// undo a removeVertex
recall(v);
}
// cout << edges << endl;
#ifdef DEBUG_SG
// cout << *this << endl;
......@@ -355,6 +379,8 @@ ostream &Graph::display(ostream &os) const {
<< "@" << neighbor_rank[SUCCESSOR][i][k++]
#endif
;
// assert(edges.has(i,v));
}
os << " /";
k = 0;
......@@ -364,11 +390,16 @@ ostream &Graph::display(ostream &os) const {
<< "@" << neighbor_rank[PREDECESSOR][i][k++]
#endif
;
// assert(edges.has(v,i));
}
os << endl;
// }
}
os << edges << endl;
return os;
}
......@@ -387,6 +418,17 @@ void Graph::verify(const char *msg) {
cout << msg << ": error, there is a loop on " << x << endl;
exit(1);
}
if(l==SUCCESSOR)
if(not edges.has(x,y)) {
cout << msg << ": error, edge (" << x << "," << y << ") is not in edge set"
<< endl << *this << endl;
cout << edges << endl;
exit(1);
}
auto jth{neighbor_rank[l][x][ith]};
......@@ -406,6 +448,18 @@ void Graph::verify(const char *msg) {
}
assert(count == arcCount());
// if(count != edges.count()) {
// cout << msg << ": error, too many edges in edgeset"
// << endl << *this << endl;
// for(auto u{0}; u<size(); ++u) {
// for(auto v{0}; v<size(); ++v) {
// if(edges.has(u,v))
// cout << " (" << u << "," << v << ")";
// }
// cout << endl;
// }
// }
}
}
......@@ -449,6 +503,18 @@ void EdgeSet::remove(const Arc a) {
edgeset.reset(a[0] * size_ + a[1]);
}
ostream& EdgeSet::display(ostream& os) const {
for(auto u{0}; u<size_; ++u) {
for(auto v{0}; v<size_; ++v) {
if(has(u,v))
os << " (" << u << "," << v << ")";
}
}
return os;
}
size_t EdgeSet::count() const { return edgeset.count(); }
// void EdgeSet::remove(const int x, const int y) {
// if (x != y) {
// auto e{x * size() + y};
......@@ -460,4 +526,13 @@ void EdgeSet::remove(const Arc a) {
std::ostream &schedcl::operator<<(std::ostream &os, const schedcl::Graph &x) {
return x.display(os);
}
\ No newline at end of file
}
std::ostream &schedcl::operator<<(std::ostream &os, const schedcl::EdgeSet &x) {
return x.display(os);
}
......@@ -3,12 +3,12 @@
#include "Global.hpp"
#include "Scheduler.hpp"
// #include "Scheduler.hpp"
#include "SparseSet.hpp"
namespace schedcl {
template <class T> class Scheduler;
template <typename T> class ResourceConstraint {
public:
......@@ -51,12 +51,14 @@ public:
ConstraintQueue(Scheduler<T> &s);
void resize(const size_t n);
// void initialise_triggers();
// add a new constraint to the queue, returns the index of that constraint in
// the queue
int add(ResourceConstraint<T> *cons);
void createTrigger(DistanceVariable<T> *x, const int c, const int h);
void createTrigger(const var v, const int c, const int h);
// void createEventTrigger(const int evt, const int c, const int h);
// notifies that variable 'id' has changed, activate the corresponding
......@@ -70,11 +72,26 @@ public:
void clear();
bool empty() const;
size_t numVar() const;
size_t numCons() const;
};
template <typename T, int N>
ConstraintQueue<T, N>::ConstraintQueue(Scheduler<T> &s) : scheduler(s) {}
template <typename T, int N>
void ConstraintQueue<T, N>::resize(const size_t n) {
triggers.resize(n);
}
template <typename T, int N> ConstraintQueue<T, N>::ConstraintQueue(Scheduler<T>& s) : Scheduler(s) {}
template <typename T, int N> size_t ConstraintQueue<T, N>::numVar() const {
return triggers.size();
}
template <typename T, int N> size_t ConstraintQueue<T, N>::numCons() const {
return constraints.size();
}
// add a new constraint to the queue, returns the index of that constraint
// in
......@@ -88,13 +105,13 @@ int ConstraintQueue<T, N>::add(ResourceConstraint<T> *cons) {
}
template <typename T, int N>
void ConstraintQueue<T, N>::createTrigger(DistanceVariable<T> *x, const int c, const int h) {
Trigger t{c, h};
int id{x->id};
if (triggers.size() <= id) {
triggers.resize(id + 1);
}
triggers[id].push_back(t);
void ConstraintQueue<T, N>::createTrigger(const var v, const int c,
const int h) {
// Trigger t{c, h};
// if (triggers.size() <= v) {
// triggers.resize(v + 1);
// }
triggers[v].push_back({c, h});
}
// notifies that variable 'id' has changed, activate the corresponding
......@@ -109,7 +126,7 @@ void ConstraintQueue<T, N>::notifyChange(const int id) {
}
#endif
++CONSTRAINT.num_literals;
++scheduler.num_literals;
for (auto &trigger : triggers[id]) {
auto cons_id{trigger.constraint_id};
auto cons{constraints[cons_id]};
......
......@@ -11,6 +11,7 @@
#include "BellmanFord.hpp"
#include "Explanation.hpp"
#include "Global.hpp"
#include "Graph.hpp"
namespace schedcl {
......@@ -108,10 +109,10 @@ set of difference literals x - y <= k (with x,y pointing to vars and k a
constant)
*/
template <class T>
class DistanceMatrix : public ReversibleObject, public Explainer_ {
class DistanceMatrix : public ReversibleObject, public Explainer {
public:
SparseSet<Reversible<size_t>> events;
// SparseSet<Reversible<size_t>> events;
DistanceMatrix<T>();
......@@ -132,10 +133,10 @@ public:
// 'set()'
// TODO: explanations
void add(const event from, const event to, const T d,
Explanation_ e = Constant_::NoReason);
Explanation e = Constant::NoReason);
// do all the changes ('add()' and 'set()') since the last call
void updateDistances();
void closure();
event_iterator begBag(const event e) const;
......@@ -144,6 +145,8 @@ public:
bool FloydWarshall();
ostream &display(ostream &os) const;
int getPrintWidth() const;
void printRow(ostream &os, const int i, const int pwidth) const;
void undo() override;
......@@ -151,6 +154,10 @@ public:
void xplain(const hint h, vector<lit> &Cl) const override;
size_t arcCount() { return core.arcCount(); }
void getLiteralInfo(const lit l, event &x, event &y, T &d) const;
private:
Graph core;
// boost::dynamic_bitset<> core_edges;
......@@ -159,7 +166,7 @@ private:
vector<T> distance;
vector<event> from;
vector<event> to;
vector<Explanation_> reason;
vector<Explanation> reason;
vector<vector<lit>> current_edge;
vector<lit> prev_edge;
......@@ -199,7 +206,7 @@ private:
// next update
// TODO: explanations
void push(const event from, const event to, const T d,
Explanation_ e = Constant_::NoReason);
const Explanation e = Constant::NoReason);
// actually applies the change corresponding to literal l
void commit(const lit l);
......@@ -210,7 +217,7 @@ private:
// push and commit
void set(const event from, const event to, const T d,
Explanation_ e = Constant_::NoReason);
const Explanation e = Constant::NoReason);
// bool inCore(const event x, const event y) const;
......@@ -329,8 +336,12 @@ template <class T> DistanceMatrix<T>::DistanceMatrix() : first_edge(0) {
current_edge[ORIGIN][HORIZON] = NoLit;
current_edge[ORIGIN][ORIGIN] = IdLit;
current_edge[HORIZON][HORIZON] = IdLit;
// ORIGIN is the first event, HORIZON is the last event
current_edge[HORIZON][ORIGIN] = IdLit;
core.addArc(HORIZON, ORIGIN);
first_edge = 2;
// resize(2);
}
......@@ -349,6 +360,13 @@ template <class T> void DistanceMatrix<T>::resize(const size_t n) {
if (i != j) {
current_edge[i][j] = current_edge[j][i] = NoLit;
}
// ORIGIN is the first event
current_edge[i][ORIGIN] = IdLit;
// HORIZON is the last event
current_edge[HORIZON][i] = IdLit;
core.addArc(i, ORIGIN);
core.addArc(HORIZON, i);
}
}
......@@ -379,7 +397,7 @@ template <class T> void DistanceMatrix<T>::reserve(const size_t n) {
next.resize(n);
prev.resize(n);
tail.resize(n);
events.reserve(n);
// events.reserve(n);
merged.reserve(n);
......@@ -402,7 +420,7 @@ template <class T> void DistanceMatrix<T>::reserve(const size_t n) {
// current_edge[i].resize(n);
rmap[i] = umap[i] = prev[i] = next[i] = tail[i] = i;
events.add(i);
// events.add(i);
// set(i, i, 0);
// for (auto j{prev_size}; j < n; ++j) {
......@@ -415,6 +433,13 @@ template <class T> void DistanceMatrix<T>::reserve(const size_t n) {
}
}
template <class T>
void DistanceMatrix<T>::getLiteralInfo(const lit l, event &x, event &y, T &d) const {
x = from[l];
y = to[l];
d = distance[l];
}
template <class T>
void DistanceMatrix<T>::xplain(const hint h, vector<lit> &Cl) const {
cout << "TODO!\n";
......@@ -475,7 +500,15 @@ template <class T> void DistanceMatrix<T>::transitive_commit(const lit l) {
// event a[2] = {rom[l], to[l]};
for (auto z : events) {
// for(auto e : events)
// assert(core.vertices.has(e));
//
//
// for(auto e : core.vertices)
// assert(events.has(e));
for (auto z : core.vertices) {
shortest_path_from_x[z] = get(x, z);
shortest_path_to_y[z] = get(z, x);
}
......@@ -506,7 +539,7 @@ template <class T> void DistanceMatrix<T>::transitive_commit(const lit l) {
// << (candidates[PREDECESSOR].has(z) ? "*" : "");
// cout << endl;
for (auto a : events) {
for (auto a : core.vertices) {
auto dax = get(a, x);
if (dax == INFTY)
continue;
......@@ -523,7 +556,7 @@ template <class T> void DistanceMatrix<T>::transitive_commit(const lit l) {
}
}
for (auto b : events) {
for (auto b : core.vertices) {
auto dyb = get(y, b);
if (dyb == INFTY)
continue;
......@@ -545,7 +578,7 @@ template <class T> void DistanceMatrix<T>::transitive_commit(const lit l) {
template <class T>
void DistanceMatrix<T>::push(const event x, const event y, const T d,
Explanation_ e) {
const Explanation e) {
auto cycle_length{get(y, x)};
......@@ -560,7 +593,7 @@ void DistanceMatrix<T>::push(const event x, const event y, const T d,
exit(0);
} else if (cycle_length == 0) {
cout << "mark " << x << " " << y << " as merged\n";
// cout << "mark " << x << " " << y << " as merged\n";
merge(x, y);
}
......@@ -576,7 +609,7 @@ void DistanceMatrix<T>::push(const event x, const event y, const T d,
template <class T>
void DistanceMatrix<T>::set(const event x, const event y, const T d,
Explanation_ e) {
const Explanation e) {
// assert(first_edge == numLiterals());
......@@ -591,7 +624,7 @@ void DistanceMatrix<T>::set(const event x, const event y, const T d,
template <class T>
void DistanceMatrix<T>::add(const event ei, const event ej, const T d,
Explanation_ e) {
const Explanation e) {
T di{0};
T dj{0};
auto rei{getRepresentant(ei, di)};
......@@ -603,17 +636,25 @@ void DistanceMatrix<T>::add(const event ei, const event ej, const T d,
// addToCore(rei, rej);
core.addArc(rei, rej);
assert(get(rei, rej) > d - di + dj);
push(rei, rej, d - di + dj, e);
// cout << "add (" << ei << "->" << ej << "):" << d << endl;
//
// cout << *this << endl;
//
// cout << rei << "/" << rej << " " << (*this)(rei, rej) << "=" << get(rei, rej)
// << " > " << d << " - " << di << " + " << dj << endl;
//
// assert(get(rei, rej) > d - di + dj);
if(get(rei, rej) > d - di + dj)
push(rei, rej, d - di + dj, e);
}
// signal that events ej and ei should be merged
template <class T>
void DistanceMatrix<T>::merge(const event ei, const event ej) {
assert(events.has(ei) && events.has(ej));
assert(core.vertices.has(ei) && core.vertices.has(ej));
auto a{ei};
auto b{ej};
......@@ -629,10 +670,6 @@ void DistanceMatrix<T>::merge(const event ei, const event ej) {
a = umap[a];
if (umap[b] > a) {
cout << "yes\n";
// assert(not merged.has(b));
if (not merged.has(b))
merged.add(b);
......@@ -654,7 +691,7 @@ template <class T> void DistanceMatrix<T>::doMerge() {
prev[b] = tail[a];
tail[a] = tail[b];
events.remove_back(b);
// events.remove_front(b);
merged.remove_front(b);
core.merge(a, b);
......@@ -663,10 +700,21 @@ template <class T> void DistanceMatrix<T>::doMerge() {
template <class T> void DistanceMatrix<T>::undoMerge() {
// for(auto e : events)
// assert(core.vertices.has(e));
//
//
// for(auto e : core.vertices)
// assert(events.has(e));
int x{0};
while (merged.start() + x-- > 0) {
auto b{merged[x]};
if (events.has(b)) {
if (core.vertices.has(b)) {
assert(rmap[b] == umap[b]);
......@@ -695,7 +743,7 @@ event_iterator DistanceMatrix<T>::endBag(const event e) const {
return event_iterator();
}
template <class T> void DistanceMatrix<T>::updateDistances() {
template <class T> void DistanceMatrix<T>::closure() {
auto last_edge{numLiterals()};
......@@ -720,10 +768,10 @@ template <class T> void DistanceMatrix<T>::updateDistances() {
template <typename T> bool DistanceMatrix<T>::FloydWarshall() {
auto change{false};
T dik, dkj, d;
for (auto k : events) {
for (auto i : events) {
for (auto k : core.vertices) {
for (auto i : core.vertices) {
if (i != k) {
for (auto j : events) {
for (auto j : core.vertices) {
if (i != j and j != k) {
dik = this->get(i, k);
if (dik != INFTY) {
......@@ -770,9 +818,8 @@ template <class T> void DistanceMatrix<T>::undo() {