Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Emmanuel Hebrard
SchedCL
Commits
8fc49c33
Commit
8fc49c33
authored
Feb 18, 2022
by
ehebrard
Browse files
cool
parent
d09c3598
Changes
7
Hide whitespace changes
Inline
Side-by-side
src/cpp/Explanation.cpp
View file @
8fc49c33
...
...
@@ -23,25 +23,23 @@ 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
);
}
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
);
assert
(
expl
!=
NULL
);
// os << "b/c ";
expl
->
print_reason
(
os
,
the_hint
);
return
os
;
}
// os << "b/c ";
expl
->
print_reason
(
os
,
the_hint
);
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
&
schedcl
::
operator
<<
(
ostream
&
os
,
const
Explanation
&
x
)
{
return
x
.
display
(
os
);
}
src/header/ConstraintGraph.hpp
View file @
8fc49c33
...
...
@@ -19,9 +19,9 @@ public:
Graph
network
;
ConstraintGraph
();
vector
<
int
>
&
operator
[](
const
int
var_id
)
const
;
// vector<int>& scope(const int cons_id);
const
vector
<
int
>
&
operator
[](
const
int
var_id
)
const
;
// vector<int>& scope(const int cons_id);
// void resize(const size_t n);
...
...
@@ -51,10 +51,9 @@ public:
template
<
typename
T
>
ConstraintGraph
<
T
>::
ConstraintGraph
()
{}
template
<
typename
T
>
vector
<
int
>&
ConstraintGraph
<
T
>::
operator
[](
const
int
var_id
)
const
{
return
network
[
SUCCESSOR
][
var_id
+
numCon
()];
template
<
typename
T
>
const
vector
<
int
>
&
ConstraintGraph
<
T
>::
operator
[](
const
int
var_id
)
const
{
return
network
[
var_id
+
numCon
()];
}
// template<typename T>
...
...
src/header/ConstraintQueue.hpp
View file @
8fc49c33
...
...
@@ -35,6 +35,7 @@ public:
void
clear
();
bool
empty
()
const
;
bool
has
(
const
int
cons_id
)
const
;
ostream
&
display
(
ostream
&
os
)
const
;
};
...
...
@@ -113,6 +114,14 @@ template <typename T, int N> bool ConstraintQueue<T, N>::empty() const {
return
true
;
}
template
<
typename
T
,
int
N
>
bool
ConstraintQueue
<
T
,
N
>::
has
(
const
int
cons_id
)
const
{
for
(
auto
i
{
N
};
i
--
>
0
;)
if
(
active
[
i
].
has
(
cons_id
))
return
true
;
return
false
;
}
template
<
typename
T
,
int
N
>
ostream
&
ConstraintQueue
<
T
,
N
>::
display
(
ostream
&
os
)
const
{
for
(
auto
p
{
N
};
p
-->
0
;)
{
...
...
src/header/DistanceMatrix.hpp
View file @
8fc49c33
...
...
@@ -124,6 +124,8 @@ public:
size_t
numLiterals
()
const
;
bool
closed
()
const
;
// correct with merge
T
operator
()(
const
event
ei
,
const
event
ej
)
const
;
// be careful, does not work with merges
...
...
@@ -156,75 +158,82 @@ public:
void
xplain
(
const
hint
h
,
vector
<
lit
>
&
Cl
)
const
override
;
ostream
&
print_reason
(
ostream
&
os
,
const
hint
h
)
const
override
;
size_t
arcCount
()
{
return
core
.
arcCount
();
}
void
getLiteralInfo
(
const
lit
l
,
event
&
x
,
event
&
y
,
T
&
d
)
const
;
private:
Graph
core
;
ReversibleEdgeSet
core_edges
;
// boost::dynamic_bitset<> core_edges;
// vector<size_t> core_list;
vector
<
T
>
distance
;
vector
<
event
>
from
;
vector
<
event
>
to
;
vector
<
Explanation
>
reason
;
vector
<
vector
<
lit
>>
current_edge
;
vector
<
lit
>
prev_edge
;
// vector<event> representant;
// merge stuff
vector
<
event
>
rmap
;
vector
<
event
>
umap
;
SparseSet
<>
merged
;
// vector<size_t> numMerged;
// tail[i] == last vertex mapped to i
vector
<
event
>
tail
;
// next[i] == next vertex mapped to the same event as i (i, if there is none)
vector
<
event
>
next
;
// prev[i] == prev vertex mapped to the same event as i (i, if there is none)
vector
<
event
>
prev
;
// update stuff
Reversible
<
lit
>
first_edge
;
BellmanFord
<
T
>
algo
;
vector
<
T
>
shortest_path_from_x
;
vector
<
T
>
shortest_path_to_y
;
SparseSet
<>
candidates
[
2
];
void
reserve
(
const
size_t
n
);
event
getRepresentant
(
const
event
i
,
T
&
d
)
const
;
// merge event ej to event ei
void
merge
(
const
event
ei
,
const
event
ej
);
void
doMerge
();
void
undoMerge
();
// just add a new literal on the stack, does not change the distance until the
// next update
// TODO: explanations
void
push
(
const
event
from
,
const
event
to
,
const
T
d
,
const
Explanation
e
=
Constant
::
NoReason
);
event
getRepresentant
(
const
event
i
)
const
;
private:
Graph
core
;
ReversibleEdgeSet
core_edges
;
// boost::dynamic_bitset<> core_edges;
// vector<size_t> core_list;
vector
<
T
>
distance
;
vector
<
event
>
from
;
vector
<
event
>
to
;
vector
<
Explanation
>
reason
;
vector
<
vector
<
lit
>>
current_edge
;
vector
<
lit
>
prev_edge
;
// vector<event> representant;
// merge stuff
vector
<
event
>
rmap
;
vector
<
event
>
umap
;
SparseSet
<>
merged
;
// vector<size_t> numMerged;
// tail[i] == last vertex mapped to i
vector
<
event
>
tail
;
// next[i] == next vertex mapped to the same event as i (i, if there is
// none)
vector
<
event
>
next
;
// prev[i] == prev vertex mapped to the same event as i (i, if there is
// none)
vector
<
event
>
prev
;
// update stuff
Reversible
<
lit
>
first_edge
;
BellmanFord
<
T
>
algo
;
vector
<
T
>
shortest_path_from_x
;
vector
<
T
>
shortest_path_to_y
;
SparseSet
<>
candidates
[
2
];
// actually applies the change corresponding to literal l
void
commit
(
const
lit
l
);
void
reserve
(
const
size_t
n
);
// actually applies the change corresponding to literal l as well as the
// transitive closure
void
transitive_commit
(
const
lit
l
);
event
getRepresentant
(
const
event
i
,
T
&
d
)
const
;
// push and commit
void
set
(
const
event
from
,
const
event
to
,
const
T
d
,
const
Explanation
e
=
Constant
::
NoReason
);
// merge event ej to event ei
void
merge
(
const
event
ei
,
const
event
ej
);
void
doMerge
();
void
undoMerge
();
// bool inCore(const event x, const event y) const;
// just add a new literal on the stack, does not change the distance
// until the
// next update
// TODO: explanations
void
push
(
const
event
from
,
const
event
to
,
const
T
d
,
const
Explanation
e
=
Constant
::
NoReason
);
// void addToCore(const event x, const event y);
// actually applies the change corresponding to literal l
void
commit
(
const
lit
l
);
// actually applies the change corresponding to literal l as well as the
// transitive closure
void
transitive_commit
(
const
lit
l
);
// push and commit
void
set
(
const
event
from
,
const
event
to
,
const
T
d
,
const
Explanation
e
=
Constant
::
NoReason
);
// bool inCore(const event x, const event y) const;
// void addToCore(const event x, const event y);
};
// template <class T> const T &DistanceConstraint<T>::operator()() const {
...
...
@@ -469,6 +478,17 @@ void DistanceMatrix<T>::xplain(const hint h, vector<lit> &Cl) const {
cout
<<
"TODO!
\n
"
;
}
template
<
class
T
>
ostream
&
DistanceMatrix
<
T
>::
print_reason
(
ostream
&
os
,
const
hint
h
)
const
{
event
x
;
event
y
;
T
d
;
getLiteralInfo
(
h
,
x
,
y
,
d
);
os
<<
" shortest path via ("
<<
x
<<
"->"
<<
y
<<
")"
;
return
os
;
}
template
<
class
T
>
size_t
DistanceMatrix
<
T
>::
size
()
const
{
return
current_edge
.
size
();
}
...
...
@@ -477,6 +497,10 @@ template <class T> size_t DistanceMatrix<T>::numLiterals() const {
return
distance
.
size
();
}
template
<
class
T
>
bool
DistanceMatrix
<
T
>::
closed
()
const
{
return
numLiterals
()
==
first_edge
;
}
// template <class T>
// const DistanceFunction<T> &DistanceMatrix<T>::operator[](const event e)
// const
...
...
@@ -496,6 +520,12 @@ event DistanceMatrix<T>::getRepresentant(const event i, T &d) const {
return
p
;
}
template
<
class
T
>
event
DistanceMatrix
<
T
>::
getRepresentant
(
const
event
i
)
const
{
T
d
;
return
getRepresentant
(
i
,
d
);
}
template
<
class
T
>
T
DistanceMatrix
<
T
>::
get
(
const
event
ei
,
const
event
ej
)
const
{
return
distance
[
current_edge
[
ei
][
ej
]];
...
...
@@ -531,70 +561,76 @@ template <class T> void DistanceMatrix<T>::transitive_commit(const lit l) {
// for(auto e : core.vertices)
// assert(events.has(e));
assert
(
core
.
has
(
x
)
and
core
.
has
(
y
));
for
(
auto
z
:
core
.
vertices
)
{
shortest_path_from_x
[
z
]
=
get
(
x
,
z
);
shortest_path_to_y
[
z
]
=
get
(
z
,
x
);
}
candidates
[
SUCCESSOR
].
clear
();
candidates
[
PREDECESSOR
].
clear
();
if
(
bound
<
get
(
x
,
y
))
{
algo
.
initialise
(
size
());
for
(
auto
z
:
core
)
{
shortest_path_from_x
[
z
]
=
get
(
x
,
z
);
shortest_path_to_y
[
z
]
=
get
(
z
,
x
);
}
candidates
[
SUCCESSOR
].
clear
();
candidates
[
PREDECESSOR
].
clear
();
current_edge
[
x
][
y
]
=
l
;
algo
.
initialise
(
size
())
;
algo
.
allShorterPaths
(
x
,
y
,
bound
,
core
.
neighbor
[
SUCCESSOR
],
*
this
,
shortest_path_from_x
,
candidates
[
SUCCESSOR
]);
current_edge
[
x
][
y
]
=
l
;
algo
.
allShorterPaths
(
y
,
x
,
bound
,
core
.
neighbor
[
PREDECESSOR
],
backward
()
,
shortest_path_
to_y
,
candidates
[
PREDE
CESSOR
]);
algo
.
allShorterPaths
(
x
,
y
,
bound
,
core
.
forward
(),
*
this
,
shortest_path_
from_x
,
candidates
[
SUC
CESSOR
]);
// cout << *this << endl;
//
// cout << "from " << x << ":";
// for (auto z : events)
// cout << " " << shortest_path_from_x[z]
// << (candidates[SUCCESSOR].has(z) ? "*" : "");
// cout << endl;
//
// cout << "to " << y << ":";
// for (auto z : events)
// cout << " " << shortest_path_to_y[z]
// << (candidates[PREDECESSOR].has(z) ? "*" : "");
// cout << endl;
for
(
auto
a
:
core
.
vertices
)
{
auto
dax
=
get
(
a
,
x
);
if
(
dax
==
INFTY
)
continue
;
for
(
auto
b
:
candidates
[
SUCCESSOR
])
{
auto
dxb
=
shortest_path_from_x
[
b
];
// get(x,b);
auto
dab
=
get
(
a
,
b
);
if
(
dax
+
dxb
<
dab
)
{
// cout << "d(" << a << "," << b << ") <- " << dax + dxb << " (was " <<
// pretty(dab) << ")\n";
set
(
a
,
b
,
dax
+
dxb
,
{
this
,
l
});
// current_edge[a][b] = numLiterals() - 1;
algo
.
allShorterPaths
(
y
,
x
,
bound
,
core
.
backward
(),
backward
(),
shortest_path_to_y
,
candidates
[
PREDECESSOR
]);
// cout << *this << endl;
//
// cout << "from " << x << ":";
// for (auto z : events)
// cout << " " << shortest_path_from_x[z]
// << (candidates[SUCCESSOR].has(z) ? "*" : "");
// cout << endl;
//
// cout << "to " << y << ":";
// for (auto z : events)
// cout << " " << shortest_path_to_y[z]
// << (candidates[PREDECESSOR].has(z) ? "*" : "");
// cout << endl;
for
(
auto
a
:
core
)
{
auto
dax
=
get
(
a
,
x
);
if
(
dax
==
INFTY
)
continue
;
for
(
auto
b
:
candidates
[
SUCCESSOR
])
{
auto
dxb
=
shortest_path_from_x
[
b
];
// get(x,b);
auto
dab
=
get
(
a
,
b
);
if
(
dax
+
dxb
<
dab
)
{
// cout << "d(" << a << "," << b << ") <- " << dax + dxb << " (was "
// <<
// pretty(dab) << ")\n";
set
(
a
,
b
,
dax
+
dxb
,
{
this
,
l
});
// current_edge[a][b] = numLiterals() - 1;
}
}
}
}
for
(
auto
b
:
core
.
vertices
)
{
auto
dyb
=
get
(
y
,
b
);
if
(
dyb
==
INFTY
)
continue
;
for
(
auto
a
:
candidates
[
PREDECESSOR
])
{
auto
day
=
shortest_path_to_y
[
a
];
// get(x,b);
auto
dab
=
get
(
a
,
b
);
if
(
day
+
dyb
<
dab
)
{
// cout << "d(" << a << "," << b << ") <- " << day + dyb << " (was " <<
// pretty(dab) << ")\n";
set
(
a
,
b
,
day
+
dyb
,
{
this
,
l
});
// current_edge[a][b] = numLiterals() - 1;
// set_and_commit(a, b, day + dyb);
for
(
auto
b
:
core
)
{
auto
dyb
=
get
(
y
,
b
);
if
(
dyb
==
INFTY
)
continue
;
for
(
auto
a
:
candidates
[
PREDECESSOR
])
{
auto
day
=
shortest_path_to_y
[
a
];
// get(x,b);
auto
dab
=
get
(
a
,
b
);
if
(
day
+
dyb
<
dab
)
{
// cout << "d(" << a << "," << b << ") <- " << day + dyb << " (was "
// <<
// pretty(dab) << ")\n";
set
(
a
,
b
,
day
+
dyb
,
{
this
,
l
});
// current_edge[a][b] = numLiterals() - 1;
// set_and_commit(a, b, day + dyb);
}
}
}
}
...
...
@@ -680,7 +716,7 @@ void DistanceMatrix<T>::add(const event ei, const event ej, const T d,
template
<
class
T
>
void
DistanceMatrix
<
T
>::
merge
(
const
event
ei
,
const
event
ej
)
{
assert
(
core
.
vertices
.
has
(
ei
)
&&
core
.
vertices
.
has
(
ej
));
assert
(
core
.
has
(
ei
)
&&
core
.
has
(
ej
));
auto
a
{
ei
};
auto
b
{
ej
};
...
...
@@ -740,7 +776,7 @@ template <class T> void DistanceMatrix<T>::undoMerge() {
int
x
{
0
};
while
(
merged
.
start
()
+
x
--
>
0
)
{
auto
b
{
merged
[
x
]};
if
(
core
.
vertices
.
has
(
b
))
{
if
(
core
.
has
(
b
))
{
assert
(
rmap
[
b
]
==
umap
[
b
]);
...
...
@@ -794,10 +830,10 @@ template <class T> void DistanceMatrix<T>::closure() {
template
<
typename
T
>
bool
DistanceMatrix
<
T
>::
FloydWarshall
()
{
auto
change
{
false
};
T
dik
,
dkj
,
d
;
for
(
auto
k
:
core
.
vertices
)
{
for
(
auto
i
:
core
.
vertices
)
{
for
(
auto
k
:
core
)
{
for
(
auto
i
:
core
)
{
if
(
i
!=
k
)
{
for
(
auto
j
:
core
.
vertices
)
{
for
(
auto
j
:
core
)
{
if
(
i
!=
j
and
j
!=
k
)
{
dik
=
this
->
get
(
i
,
k
);
if
(
dik
!=
INFTY
)
{
...
...
@@ -876,9 +912,9 @@ void DistanceMatrix<T>::printRow(ostream &os, const int i,
const
int
pwidth
)
const
{
T
d
{
0
};
if
(
core
.
vertices
.
has
(
i
))
{
if
(
core
.
has
(
i
))
{
for
(
auto
j
{
0
};
j
<
size
();
++
j
)
{
if
(
core
.
vertices
.
has
(
j
)
or
getRepresentant
(
j
,
d
)
==
i
)
if
(
core
.
has
(
j
)
or
getRepresentant
(
j
,
d
)
==
i
)
os
<<
setw
(
pwidth
)
<<
right
<<
pretty
((
*
this
)(
i
,
j
))
<<
(
core_edges
.
has
(
i
,
j
)
?
"*"
:
" "
);
else
...
...
@@ -920,7 +956,7 @@ template <class T> ostream &DistanceMatrix<T>::display(ostream &os) const {
os
<<
setw
(
esz
)
<<
" "
;
for
(
auto
i
=
0
;
i
<
size
();
++
i
)
{
if
(
core
.
vertices
.
has
(
i
))
if
(
core
.
has
(
i
))
os
<<
setw
(
largest
)
<<
i
<<
" "
;
else
os
<<
setw
(
largest
+
1
)
<<
""
;
...
...
@@ -933,19 +969,22 @@ template <class T> ostream &DistanceMatrix<T>::display(ostream &os) const {
os
<<
endl
;
}
SparseSet
<>
R
;
R
.
reserve
(
size
());
for
(
auto
x
{
core
.
vertices
.
bbegin
()};
x
!=
core
.
vertices
.
bend
();
++
x
)
{
R
.
add
(
rmap
[
*
x
]);
}
// SparseSet<> R;
// R.reserve(size());
// R.fill();
//
// for (auto x : core) {
// R.remove_back(rmap[*x]);
// }
for
(
auto
x
:
R
)
{
cout
<<
x
<<
" stands for"
;
for
(
auto
y
{
begBag
(
x
)};
y
!=
endBag
(
x
);
++
y
)
{
cout
<<
" "
<<
*
y
;
for
(
auto
x
:
core
)
{
if
(
*
(
begBag
(
x
))
!=
x
)
{
cout
<<
x
<<
" stands for"
;
for
(
auto
y
{
begBag
(
x
)};
y
!=
endBag
(
x
);
++
y
)
{
cout
<<
" "
<<
*
y
;
}
cout
<<
endl
;
}
cout
<<
endl
;
}
cout
<<
core
<<
endl
;
...
...
src/header/Graph.hpp
View file @
8fc49c33
...
...
@@ -74,7 +74,7 @@ vertices
*/
class
Graph
:
public
ReversibleObject
{
p
ublic
:
p
rivate
:
// // nor really needed, should probably remove
// Schedule<T> &sched;
...
...
@@ -84,6 +84,23 @@ public:
// the adjency matrices (one for successors, and one for predecessors)
vector
<
vector
<
int
>>
neighbor
[
2
];
public:
const
vector
<
int
>
&
operator
[](
const
int
u
)
const
{
return
neighbor
[
SUCCESSOR
][
u
];
}
// vector<int>::iterator begin() { return vertices.begin(); }
// vector<int>::iterator end() { return vertices.end(); }
vector
<
int
>::
const_iterator
begin
()
const
{
return
vertices
.
begin
();
}
vector
<
int
>::
const_iterator
end
()
const
{
return
vertices
.
end
();
}
const
vector
<
vector
<
int
>>
&
forward
()
const
{
return
neighbor
[
SUCCESSOR
];
}
const
vector
<
vector
<
int
>>
&
backward
()
const
{
return
neighbor
[
PREDECESSOR
];
}
bool
has
(
const
int
x
)
const
{
return
vertices
.
has
(
x
);
}
size_t
arcCount
()
const
;
size_t
vertexCount
()
const
;
size_t
size
()
const
;
...
...
src/header/Scheduler.hpp
View file @
8fc49c33
...
...
@@ -16,6 +16,7 @@
#define PROPAGATION 2
#define UPDATES 4
#define TRACE 7
namespace
schedcl
{
...
...
@@ -72,7 +73,7 @@ public:
int
getUB
()
const
;
size_t
numVar
()
const
;
size_t
numCon
()
const
;
size_t
numCon
()
const
;
size_t
numTask
()
const
;
size_t
numEvent
()
const
;
...
...
@@ -106,6 +107,8 @@ public:
void
propagate
();
void
initialize
();
void
search
();
// void explore(const ChoicePoint &cp, const bool branch,
...
...
@@ -116,9 +119,8 @@ public:
void
fail
(
const
Explanation
e
);
private:
Reversible
<
lit
>
propag_lit
;
Reversible
<
lit
>
propag_lit
;
bool
isGround
(
const
DistanceConstraint
<
T
>
c
)
const
;
bool
isEntailed
(
const
DistanceConstraint
<
T
>
c
)
const
;
...
...
@@ -147,10 +149,9 @@ private:
bool
debug_flag
{
true
};
#endif
int
init_level
{
0
};
ConstraintGraph
<
T
>
network
;
ConstraintGraph
<
T
>
network
;
ConstraintQueue
<
T
,
1
>
queue
;
// nice labels for tasks
...
...
@@ -230,7 +231,7 @@ template <class T> void Scheduler<T>::declareVariable(event x, event y) {
template
<
class
T
>
void
Scheduler
<
T
>::
post
(
ResourceConstraint
<
T
>
*
c
)
{
network
.
add
(
c
);
// c->post(idx);
// c->post(idx);
#ifdef DEBUG_CONSTRAINT
c
->
id
=
idx
;
...
...
@@ -240,9 +241,17 @@ template <class T> void Scheduler<T>::post(ResourceConstraint<T> *c) {
template
<
class
T
>
void
Scheduler
<
T
>::
wake_me_on
(
const
event
x
,
const
event
y
,
const
int
c
)
{
declareVariable
(
x
,
y
);
// this is a variable that a constraint wants in its watch list
network
.
createTrigger
(
varmap
[
x
][
y
],
c
);
auto
rx
{
distance
.
getRepresentant
(
x
)};
auto
ry
{
distance
.
getRepresentant
(
y
)};
if
(
getVariable
(
rx
,
ry
)
==
NoVar
)
{
declareVariable
(
rx
,
ry
);
// this is a variable that a constraint wants in its watch list
}
if
(
network
[
varmap
[
rx
][
ry
]].
empty
()
or
network
[
varmap
[
rx
][
ry
]].
back
()
!=
c
)
network
.
createTrigger
(
varmap
[
rx
][
ry
],
c
);
}
template
<
class
T
>
...
...
@@ -258,8 +267,8 @@ void Scheduler<T>::addMaximumLag(const event x, const event y, const T lag) {
// if (lag != INFTY) {
addConstraint
(
x
,
y
,
lag
,
Constant
::
NoReason
);
// }
propagate
();