Commit 480127dd authored by ehebrard's avatar ehebrard
Browse files

menage

parent 7e025138
#include <iostream>
#include "Explanation.hpp"
using namespace std;
using namespace schedcl;
/* Explanation system:
An Explainer is a class with the methods 'xplain(const void* hint, vector<lit> &Cl)' that inserts an explanation for the literal d to the clause Cl
Typically, each constraint is an explainer, and must store the info necessary to access/compute the reason
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 {};
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);
}
ostream &Explanation_::display(ostream &os) const {
assert(expl != NULL);
// os << "b/c ";
expl->print_reason(os, the_hint);
return os;
}
Explanation_::Explanation_(Explainer_ *e, hint h) : expl(e), the_hint(h) {}
Explanation_ Constant_::NoReason = Explanation_(new Explainer_(), NoHint);
ostream &operator<<(ostream &os, const Explanation_ &x) {
return x.display(os);
}
#include "Schedule.hpp"
//
//
// // 0 is for the origin event, 1 is for the completion event
// task schedcl::TASK( event x ) {
// return x/2-1;
// }
//
// event schedcl::START( task x ) {
// return 2*x+2;
// }
//
// 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(
// schedcl::ScheduleConstraint *cons) {
// propagators.push_back(cons);
// active.reserve(propagators.size());
// return propagators.size() - 1;
// }
//
// void schedcl::ConstraintQueue::push(const int cons_idx) {
// active.add(cons_idx);
// }
//
// schedcl::ScheduleConstraint *schedcl::ConstraintQueue::pop() {
// ScheduleConstraint *c = propagators[active.back()];
// active.pop_back();
// return c;
// }
//
// bool schedcl::ConstraintQueue::empty() const { return active.empty(); }
\ No newline at end of file
#include "SparseGraph.hpp"
#ifndef _SCHEDCL_CONSTRAINT_HPP
#define _SCHEDCL_CONSTRAINT_HPP
#include "Global.hpp"
#include "Scheduler.hpp"
namespace schedcl {
template <typename T> class ResourceConstraint {
public:
#ifdef DEBUG_CONSTRAINT
bool debug_flag{false};
int id;
#endif
const int priority{0};
virtual void post(const int idx) = 0;
virtual void propagate() = 0;
virtual void notify(const int hint){};
virtual ostream &display(ostream &os) const = 0;
};
template <typename T, int N> class ConstraintQueue {
class Trigger {
public:
const int constraint_id;
const int variable_id;
};
public:
Scheduler<T> &scheduler;
// all constraints
vector<ResourceConstraint<T> *> constraints;
// which ones need to be propagated
SparseSet<> active[N]; // alows for N levels of priority
// for every variable, its triggers
vector<vector<Trigger>> triggers;
// vector<vector<Trigger>> event_triggers;
ConstraintQueue(Scheduler<T> &s);
// 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 createEventTrigger(const int evt, const int c, const int h);
// notifies that variable 'id' has changed, activate the corresponding
// triggers
void notifyChange(const int id);
// returns the active constraint of highest priority that has been activated
// first, return NULL if there are no active constraint
ResourceConstraint<T> *pop_front();
// bool empty() const;
void clear();
bool empty() const;
};
template <typename T, int N> ConstraintQueue<T, N>::ConstraintQueue(Scheduler<T>& s) : Scheduler(s) {}
// add a new constraint to the queue, returns the index of that constraint
// in
// the queue
template <typename T, int N>
int ConstraintQueue<T, N>::add(ResourceConstraint<T> *cons) {
int id{static_cast<int>(constraints.size())};
constraints.push_back(cons);
active[cons->priority].reserve(id + 1);
return id;
}
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);
}
// notifies that variable 'id' has changed, activate the corresponding
// triggers
template <typename T, int N>
void ConstraintQueue<T, N>::notifyChange(const int id) {
#ifdef TRACE
if (scheduler.debug_flag and (TRACE & PROPAGATION)) {
cout << "new literal: (" << id << ") " << *(scheduler.variables[id])
<< " b/c " << scheduler.variables[id]->back().reason << endl;
}
#endif
++CONSTRAINT.num_literals;
for (auto &trigger : triggers[id]) {
auto cons_id{trigger.constraint_id};
auto cons{constraints[cons_id]};
cons->notify(trigger.variable_id);
if (not active[cons->priority].has(cons_id)) {
active[cons->priority].add(cons_id);
#ifdef TRACE
if (scheduler.debug_flag and (TRACE & PROPAGATION)) {
cout << " triggers " << *cons << endl;
}
#endif
}
}
}
template <typename T, int N>
ResourceConstraint<T> *ConstraintQueue<T, N>::pop_front() {
auto i{N};
ResourceConstraint<T> *cons{NULL};
while (i-- > 0) {
if (not active[i].empty()) {
cons = constraints[active[i].front()];
active[i].pop_front();
break;
}
}
return cons;
}
template <typename T, int N>
void ConstraintQueue<T, N>::clear() {
for (auto i{N}; i-- > 0;)
active[i].clear();
}
template <typename T, int N> bool ConstraintQueue<T, N>::empty() const {
for (auto i{N}; i-- > 0;)
if (not active[i].empty())
return false;
return true;
}
template <class T> ostream &operator<<(ostream &os, const ResourceConstraint<T> &x) {
return x.display(os);
}
} // namespace SCHEDCL
#endif // _SCHEDCL_SCHEDULING_HPP
#ifndef _schedcl_EXPLANATION_HPP
#define _schedcl_EXPLANATION_HPP
#include <vector>
#include "Global.hpp"
namespace schedcl {
using namespace std;
/* Explanation system:
An Explainer is a class with the methods 'xplain(const void* hint, vector<lit> &Cl)' that inserts an explanation for the literal d to the clause Cl
Typically, each constraint is an explainer, and must store the info necessary to access/compute the reason
DistanceGraph are also explainers, for the transitivity
The static object "NoReason" is the empty reason
*/
class Explainer_ {
public:
virtual void xplain(const hint h, vector<lit> &Cl) const;
virtual ostream &print_reason(ostream &os, const hint h) const;
};
class Explanation_ {
public:
Explanation_(Explainer_ *e, hint h);
void get(vector<lit> &Cl) const;
ostream &display(ostream &os) const;
private:
Explainer_ *expl{NULL};
hint the_hint{NoHint};
};
class Constant_ {
public:
static Explanation_ NoReason;
};
ostream &operator<<(ostream &os, const Explanation_ &x);
} // namespace schedcl
#endif
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment