Commit d8cd18ad authored by ehebrard's avatar ehebrard
Browse files

restart

parent 8ad8db14
......@@ -18,9 +18,9 @@ along with minicsp. If not, see <http://www.gnu.org/licenses/>.
*************************************************************************/
// #include "DistanceVariable.hpp"
#include "SparseDistanceGraph.hpp"
#include "DistanceGraph.hpp"
#include "Schedule.hpp"
// #include "SparseGraph.hpp"
// #include "DistanceGraph.hpp"
#include "BellmanFord.hpp"
#include "osp.hpp"
......@@ -54,16 +54,16 @@ int main(int argc, char *argv[]) {
cout << endl;
Schedule<int> S1;
Schedule<int> S2;
// Schedule<int> S2;
for (auto d : duration) {
S1.addTask("t" + to_string(S1.numTask()), d, d);
S2.addTask("t" + to_string(S2.numTask()), d, d);
// S2.addTask("t" + to_string(S2.numTask()), d, d);
}
auto ub{osp::getUb(duration, resource)};
S1.setUpperBound(ub);
S2.setUpperBound(ub);
// S2.setUpperBound(ub);
for (auto R : resource) {
for (auto x : R) {
......@@ -74,10 +74,10 @@ int main(int argc, char *argv[]) {
S1.addEdge(END(x), START(y));
S1.addEdge(END(x), END(y));
S2.addEdge(START(x), START(y));
S2.addEdge(START(x), END(y));
S2.addEdge(END(x), START(y));
S2.addEdge(END(x), END(y));
// S2.addEdge(START(x), START(y));
// S2.addEdge(START(x), END(y));
// S2.addEdge(END(x), START(y));
// S2.addEdge(END(x), END(y));
}
}
}
......@@ -93,7 +93,7 @@ int main(int argc, char *argv[]) {
// cout << SG << endl;
DistanceGraph<int> G(S2);
// DistanceGraph<int> G(S2);
// cout << G << endl;
......@@ -111,7 +111,7 @@ int main(int argc, char *argv[]) {
// cout << S.label(v) << ": " << shortest_path[v] << endl;
S1.initialise();
S2.initialise();
// S2.initialise();
// cout << S1 << endl;
// cout << S2 << endl;
......@@ -128,26 +128,26 @@ int main(int argc, char *argv[]) {
// cout << S2 << endl;
S1.updateDistances();
S2.updateDistances();
G.FloydWarshall();
// S2.updateDistances();
// G.FloydWarshall();
cout << S1 << endl;
cout << S2 << endl;
for (auto v : S1.variables) {
auto x{v->from};
auto y{v->to};
auto w{v->get()};
// cout << S2 << endl;
auto u{S2.getVariable(x, y)};
if (w != u->get()) {
cout << "d[" << S1.label(x) << "][" << S1.label(y) << "]=" << w << "/"
<< u->get() << endl;
}
}
// for (auto v : S1.variables) {
// auto x{v->from};
// auto y{v->to};
// auto w{v->get()};
//
// // auto u{S2.getVariable(x, y)};
// if (w != u->get()) {
// cout << "d[" << S1.label(x) << "][" << S1.label(y) << "]=" << w << "/"
// << u->get() << endl;
// }
// }
auto u{S1.getVariable(START(1), END(0))};
S1.addConstraint(u, 0);
S1.addConstraint(u, 0, Constant<int>::NoReason);
S1.updateDistances();
cout << S1 << endl;
......@@ -155,14 +155,14 @@ int main(int argc, char *argv[]) {
ReversibleObject::env->save();
cout << S1.graph << endl;
cout << S1.minimal_graph << endl;
// cout << "merge\n";
for (auto i{0}; i < S1.numTask(); ++i)
S1.graph.merge(START(i), END(i), duration[i]);
S1.minimal_graph.merge(START(i), END(i), duration[i]);
cout << S1.graph << endl;
cout << S1.minimal_graph << endl;
cout << "restore to level " << ReversibleObject::env->level() << "\n";
......@@ -170,7 +170,7 @@ int main(int argc, char *argv[]) {
cout << "OK!\n";
// cout << S1.graph << endl;
// cout << S1.minimal_graph << endl;
// auto v2{S2.getVariable(START(1), END(0))};
// v2->set(0);
......
......@@ -16,6 +16,56 @@ event schedcl::END( task x ) {
return 2*x+3;
}
bool schedcl::is_cycle(const long hint) { return static_cast<bool>(hint & 1); }
int schedcl::var(const long hint) {
return static_cast<int>((hint >> 1) & (numeric_limits<int>::max()));
}
int schedcl::lit(const long hint) {
return static_cast<int>(hint >> (1 + 8 * sizeof(int)));
}
long schedcl::make_hint(const long var_id, const long lit_id,
const bool cycle) {
// cout << var_id << " / " << lit_id << " / " << cycle << endl;
//
//
// assert((1 + 8 * sizeof(int)) == 33);
long r = (lit_id << (1 + 8 * sizeof(int))) + (var_id << 1) + cycle;
// auto ec{(lit_id << 33)};
// auto ev{(var_id << 1)};
//
// cout << ev << " (" << (ev >> 1) << ") / " << ec << " (" << (ec >> 33) << ")
// / " << cycle << endl;
//
// cout << r << " (" << (r >> 33) << ") [" << (r >> 1) << " -> " << ((r >> 1)
// & numeric_limits<int>::max()) << "]" << endl;
//
// assert(r == ev + ec + cycle);
//
//
// auto v{var(r)};
// auto l{lit(r)};
// auto c{is_cycle(r)};
//
// cout << v << " / " << l << " / " << c << endl;
//
// assert(v == var_id);
// assert(l == lit_id);
// assert(c == cycle);
//
// exit(1);
//
// // 8589934592
// // 4294967296
return r; //(lit_id << (1 + 8 * sizeof(int))) + (var_id << 1) + is_cycle;
}
// schedcl::ConstraintQueue::ConstraintQueue() {}
//
// int schedcl::ConstraintQueue::add(
......
......@@ -51,13 +51,9 @@ public:
bool debug_flag{false};
#endif
// vector<T> shortest_path;
// SparseSet<> reached;
private:
SparseSet<> changed;
// long unsigned max_num_step{0};
};
template <typename T> BellmanFord<T>::BellmanFord() {}
......@@ -68,44 +64,30 @@ template <typename T> BellmanFord<T>::BellmanFord(const int n) {
template <typename T>
void BellmanFord<T>::initialise(const int n) {
// shortest_path.clear();
// shortest_path.resize(n, INFTY);
changed.reserve(n);
changed.clear();
// reached.reserve(n);
// reached.clear();
negative_cycle = false;
}
template <typename T>
template<class G>
void BellmanFord<T>::allShortestPaths(const int s, const G& neighbors, vector<T>& shortest_path) {
// long unsigned steps{0};
void BellmanFord<T>::allShortestPaths(const int s, const G& neighbors, vector<T>& shortest_path
// , vector<int>& predecessor
) {
shortest_path[s] = 0;
changed.add(s);
// reached.add(s);
while (not changed.empty()) {
auto u{changed.front()};
changed.pop_front();
// ++steps;
// if (steps > max_num_step) {
// max_num_step = steps;
// cout << max_num_step << endl;
// }
// cout << u << ":";
for (auto e : neighbors[u]) {
auto v{e.neighbor()};
auto w{e.length()};
// cout << " (" << v << "|" << w << ")";
if (w != INFTY and shortest_path[u] + w < shortest_path[v]) {
if (v == s) {
......@@ -115,6 +97,7 @@ void BellmanFord<T>::allShortestPaths(const int s, const G& neighbors, vector<T>
}
shortest_path[v] = shortest_path[u] + w;
// predecessor[v] = u;
if (not changed.has(v))
changed.add(v);
......@@ -133,15 +116,14 @@ template <class G
void BellmanFord<T>::allShorterPaths(const int x, const int y, const T wxy,
const G &neighbors,
vector<T> &shortest_path,
SparseSet<> &reached
SparseSet<> &reached//,
// vector<int>& predecessor
#ifdef DEBUG_BELLMANFORD
,
P &printer
#endif
) {
// long unsigned steps{0};
assert(changed.empty());
#ifdef DEBUG_BELLMANFORD
if (debug_flag)
......@@ -172,12 +154,6 @@ void BellmanFord<T>::allShorterPaths(const int x, const int y, const T wxy,
changed.pop_front();
// ++steps;
// if (steps > max_num_step) {
// max_num_step = steps;
// cout << max_num_step << endl;
// }
for (auto e : neighbors[u]) {
auto v{e.neighbor()};
auto w{e.length()};
......@@ -207,11 +183,10 @@ void BellmanFord<T>::allShorterPaths(const int x, const int y, const T wxy,
negative_cycle = true;
changed.clear();
// exit(1);
return;
}
// predecessor[v] = u;
shortest_path[v] = shortest_path[u] + w;
if (not changed.has(v))
changed.add(v);
......
......@@ -16,6 +16,8 @@ template <typename T> class Schedule;
template <typename T> class DistanceVariable;
template <typename T> class Explanation;
template <typename T> class DistanceLiteral {
public:
......@@ -25,11 +27,15 @@ public:
// {static_cast<DistanceVariable<T>*>(NULL),-1}
DistanceVariable<T> *var{NULL};
int lit{-1};
int lit_idx{-1};
Explanation<T> get_explanation() const;
bool operator==(const DistanceLiteral<T> &rhs) const;
ostream &display(ostream &os) const {
os << var->sched.label(var->to) << " - " << var->sched.label(var->from)
<< " <= " << var->get(lit).value;
<< " <= " << var->get(lit_idx).value;
// os << "e" << to << " - e" << from << " <= " << get();
return os;
}
......@@ -48,40 +54,44 @@ The static object "NoReason" is the empty reason
*/
template <typename T> class Explainer {
public:
virtual void xplain(const int hint, vector<DistanceLiteral<T>> &Cl) const {};
virtual void xplain(const DistanceLiteral<T> &l, const long hint,
vector<DistanceLiteral<T>> &Cl) const {};
// virtual void xplain(const int hint, vector<DistanceLiteral>& Cl)
// const {};
virtual ostream &print_reason(ostream &os, const int hint) const { os << "no reason"; return os; }
virtual ostream &print_reason(ostream &os, const long hint) const {
os << "no reason";
return os;
}
};
template<typename T>
class Explanation {
public:
Explainer<T> *expl;
int hint;
void get(vector<DistanceLiteral<T>> &Cl) const { expl->xplain(hint, Cl); }
Explainer<T> *expl{NULL};
long hint{-1};
void get_reason_for(const DistanceLiteral<T> &l,
vector<DistanceLiteral<T>> &Cl) const {
expl->xplain(l, hint, Cl);
}
ostream &display(ostream &os) const {
assert(expl != NULL);
assert(expl != NULL);
// os << "b/c ";
expl->print_reason(os, hint);
expl->print_reason(os, hint);
return os;
}
};
template <typename T> class Constant {
public:
// static Explainer<T> *NoReason;
static DistanceLiteral<T> NoLiteral;
static Explanation<T> NoReason;
static Explanation<T> NoReason;
};
// template <typename T> Explainer<T> *Constant<T>::NoReason = new Explainer<T>();
......@@ -95,7 +105,7 @@ DistanceLiteral<T> Constant<T>::NoLiteral = {
template <typename T> struct Bound {
T value;
const Explanation<T> reason;
const Explanation<T> reason;
};
......@@ -179,22 +189,21 @@ public:
// }
// }
void set(const T d,
const Explanation<T> e){
// const Explainer<T> *e, const int h) {
auto l{d - offset};
if (get() > l) {
ReversibleObject::save();
// literals.push_back({l, e});
literals->push_back({l, e});
// trail.push_back(d);
// reason.push_back(e);
void set(const T d, const Explanation<T> e) {
// const Explainer<T> *e, const int h) {
auto l{d - offset};
if (get() > l) {
ReversibleObject::save();
// literals.push_back({l, e});
literals->push_back({l, e});
// trail.push_back(d);
// reason.push_back(e);
}
}
void set(const T d) {
set(d, Constant<T>::NoReason);
set(d, Constant<T>::NoReason);
// set(d, Constant<T>::NoReason, NoHint);
// if (get() > d) {
// ReversibleObject::save();
......@@ -216,6 +225,7 @@ public:
void clear() { from = -1; }
bool empty() const { return from < 0; }
bool loop() const { return from == to; }
size_t history_size() const { return literals->size(); }
// int latest() const { return literals.size()-1; }
......@@ -253,29 +263,26 @@ public:
ostream &display(ostream &os) const {
os << sched.label(to) << " - " << sched.label(from) << " <= " << get();
// os << "e" << to << " - e" << from << " <= " << get();
return os;
}
// protected:
protected:
// stores the successive values, the explainer, and a hint used to index the
// literals on the explainer's side, or directly encode a hint to allow to
// reconstruct the reason
vector<Bound<T>> *literals;
// vector<T> trail;
//
// // stores the explanations
// vector<const Explainer<T>*> reason;
//
// // data structure used to index the literals on the explainer's side, or
// directly encode a hint to allow to reconstruct the reason
// // e.g., can be used to reconstruct the shortest paths: hint[i][j] gives a
// vertex x that helped decrease the the shortest path between i and j.
// Therefore, SP(i,j) is SP(i,x) + SP(x,j)
// vector<const int> hint;
};
template <typename T>
schedcl::Explanation<T> schedcl::DistanceLiteral<T>::get_explanation() const {
return var->get(lit_idx).reason;
}
template <typename T>
bool DistanceLiteral<T>::operator==(const DistanceLiteral<T> &rhs) const {
return var == rhs.var and lit_idx == rhs.lit_idx;
}
template <typename T>
ostream &operator<<(ostream &os, const Explanation<T> &x) {
return x.display(os);
......
#ifndef _schedcl_GRAPH_HPP
#define _schedcl_GRAPH_HPP
#include <map>
#include <vector>
#include <boost/dynamic_bitset.hpp>
#include "DistanceVariable.hpp"
#include "SparseSet.hpp"
namespace schedcl {
using namespace std;
/*
Implementation of a graph
- It supports [adding new Arcs/not really]; reducing Arcs' weights; and
merging two
vertices
- Reversible
*/
template <typename T>
class Graph : public ReversibleObject {
public:
// // nor really needed, should probably remove
// Schedule<T> &sched;
// currently active vertex
SparseSet<> vertices;
// the adjency matrices (one for successors, and one for predecessors)
vector<vector<int>> neighbor[2];
size_t arcCount() const;
size_t vertexCount() const;
size_t size() const;
Graph();
// void initialise(Schedule<T> &s);
void initialise(const int n);
// restore to the last saved state (restore vertex merging, Arc weights
// are
// restored via variables directly)
void undo() override;
// add the Arc u -> v
void addArc(const int u, const int v);
// remove vertex u
void removeVertex(const int u);
// merge vertex v to vertex u
void merge(const int u, const int v);
ostream &display(ostream &os) const;
protected:
// the rank of vertex v in its neighbor's adjency list
vector<vector<int>> neighbor_rank[2];
// number of arcs
size_t numArc{0};
// // the merge map
// vector<int> representant;
// The removed vertex is the first one out of vertices. The first int in
// trail
// gives the number of new forward Arcs for its representant x, the
// second
// the number of backward Arcs. They must be last in x's neighbor list
vector<int> trail;
// remove i-th neighbor (successor or predecessor depending on n) from u's
void remove(const bool n, const int u, const int i);
// add v as i-th neighbor of u (successor or predecessor depending on n)
void add(const bool n, const int u, const int v, const int i);
// split u from the vertex it was merge to
void split(const int u);
private:
boost::dynamic_bitset<> buffer;
#ifdef DEBUG_SG
void verify(const char *msg);
#endif
};
// declare a new time point in the graph
template <typename T> Graph<T>::Graph() : ReversibleObject() {}
template <typename T> void Graph<T>::addArc(const int u, const int v) {
ReversibleObject::save();
trail.push_back(u);
trail.push_back(v);
neighbor_rank[SUCCESSOR][u].push_back(static_cast<int>(neighbor[PREDECESSOR][v].size()));
neighbor_rank[PREDECESSOR][v].push_back(static_cast<int>(neighbor[SUCCESSOR][u].size()));
neighbor[SUCCESSOR][u].push_back(v);
neighbor[PREDECESSOR][v].push_back(u);
++numArc;
}
template <typename T> void Graph<T>::initialise(const int n) {
if (n > 0) {
buffer.resize(n, 0);
neighbor[PREDECESSOR].resize(n);
neighbor[SUCCESSOR].resize(n);
neighbor_rank[PREDECESSOR].resize(n);
neighbor_rank[SUCCESSOR].resize(n);
vertices.reserve(n);
vertices.fill();
representant.resize(n);
// for (auto i = 0; i < n; ++i) {
// representant[i]
// // = tail[i] = next[i] = prev[i]
// = i;
// }
}
#ifdef DEBUG_SG
cout << *this << endl;
verify("init");
#endif
}
template <typename T> size_t Graph<T>::arcCount() const { return numArc; }
template <typename T> size_t Graph<T>::vertexCount() const {
return vertices.count();
}