Skip to content

Commit

Permalink
use explicit potential function
Browse files Browse the repository at this point in the history 
Signed-off-by: Elazar Gershuni <[email protected]>
  • Loading branch information
@elazarg
elazarg committed Dec 2, 2024
1 parent bc91973 commit a1331aa
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 37 deletions.
17 changes: 9 additions & 8 deletions src/crab/split_dbm.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -281,7 +281,7 @@ bool SplitDBM::add_linear_leq(const linear_expression_t& exp) {
}
GraphOps::close_over_edge(g, src, dest);
}
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, potential, 0));
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, [&](vert_id v){ return potential[v]; }, 0));
normalize();
return true;
}
Expand Down Expand Up @@ -504,7 +504,7 @@ SplitDBM SplitDBM::operator|(const SplitDBM& o) const& {
bool is_closed;
graph_t g_rx(GraphOps::meet(gx, g_ix_ry, is_closed));
if (!is_closed) {
GraphOps::apply_delta(g_rx, GraphOps::close_after_meet(SubGraph(g_rx, 0), pot_rx, gx, g_ix_ry));
GraphOps::apply_delta(g_rx, GraphOps::close_after_meet(SubGraph(g_rx, 0), [&](vert_id v) { return pot_rx[v]; }, gx, g_ix_ry));
}

graph_t g_rx_iy;
Expand All @@ -525,7 +525,7 @@ SplitDBM SplitDBM::operator|(const SplitDBM& o) const& {
// Similarly, should use a SubGraph view.
graph_t g_ry(GraphOps::meet(gy, g_rx_iy, is_closed));
if (!is_closed) {
GraphOps::apply_delta(g_ry, GraphOps::close_after_meet(SubGraph(g_ry, 0), pot_ry, gy, g_rx_iy));
GraphOps::apply_delta(g_ry, GraphOps::close_after_meet(SubGraph(g_ry, 0), [&](vert_id v) { return pot_ry[v]; }, gy, g_rx_iy));
}

// We now have the relevant set of relations. Because g_rx and g_ry are closed,
Expand Down Expand Up @@ -730,11 +730,12 @@ std::optional<SplitDBM> SplitDBM::meet(const SplitDBM& o) const {
}

if (!is_closed) {
GraphOps::apply_delta(meet_g, GraphOps::close_after_meet(SubGraph(meet_g, 0), meet_pi, gx, gy));
auto potential_func = [&](vert_id v) -> Weight { return meet_pi[v]; };
GraphOps::apply_delta(meet_g, GraphOps::close_after_meet(SubGraph(meet_g, 0), potential_func, gx, gy));

// Recover updated LBs and UBs.<

GraphOps::apply_delta(meet_g, GraphOps::close_after_assign(meet_g, meet_pi, 0));
GraphOps::apply_delta(meet_g, GraphOps::close_after_assign(meet_g, potential_func, 0));
}
SplitDBM res(std::move(meet_verts), std::move(meet_rev), std::move(meet_g), std::move(meet_pi), vert_set_t());
CRAB_LOG("zones-split", std::cout << "Result meet:\n" << res << "\n");
Expand Down Expand Up @@ -891,7 +892,7 @@ void SplitDBM::assign(variable_t lhs, const linear_expression_t& e) {
// apply_delta should be safe here, as x has no edges in G.
GraphOps::apply_delta(g, delta);
}
GraphOps::apply_delta(g, GraphOps::close_after_assign(SubGraph(g, 0), potential, vert));
GraphOps::apply_delta(g, GraphOps::close_after_assign(SubGraph(g, 0), [&](vert_id v){ return potential[v]; }, vert));

if (lb_w) {
g.update_edge(vert, *lb_w, 0);
Expand Down Expand Up @@ -946,9 +947,9 @@ void SplitDBM::normalize() {
GraphOps::edge_vector delta;
// GraphOps::close_after_widen(g, potential, vert_set_wrap_t(unstable), delta);
// GKG: Check
GraphOps::apply_delta(g, GraphOps::close_after_widen(SubGraph(g, 0), potential, vert_set_wrap_t(unstable)));
GraphOps::apply_delta(g, GraphOps::close_after_widen(SubGraph(g, 0), [&](vert_id v){ return potential[v]; }, vert_set_wrap_t(unstable)));
// Retrieve variable bounds
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, potential, 0));
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, [&](vert_id v){ return potential[v]; }, 0));

unstable.clear();
}
Expand Down
48 changes: 19 additions & 29 deletions src/crab_utils/graph_ops.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -484,13 +484,6 @@ class GraphRev {
G& g;
};

// temporary concept: indexable
// TODO: replace everywhere with simple callable
template <typename T>
concept WeightIndexable = requires(T t, AdaptGraph::vert_id v) {
{ t[v] } -> std::convertible_to<typename AdaptGraph::Weight>;
};

// GKG - What's the best way to split this out?
class GraphOps {
public:
Expand All @@ -499,6 +492,8 @@ class GraphOps {
using Weight = typename graph_t::Weight;
using vert_id = typename graph_t::vert_id;
using WeightVector = std::vector<Weight>;

using PotentialFunction = std::function<Weight(vert_id)>;
using mut_val_ref_t = typename graph_t::mut_val_ref_t;

using edge_vector = std::vector<std::tuple<vert_id, vert_id, Weight>>;
Expand Down Expand Up @@ -786,7 +781,7 @@ class GraphOps {
}

template <class G, class G1, class G2>
static edge_vector close_after_meet(const G& g, const WeightIndexable auto& pots, const G1& l, const G2& r) {
static edge_vector close_after_meet(const G& g, const PotentialFunction& pots, const G1& l, const G2& r) {
// We assume the syntactic meet has already been computed, and potentials have been initialized.
// We just want to restore closure.
assert(l.size() == r.size());
Expand Down Expand Up @@ -850,7 +845,7 @@ class GraphOps {
// P is some vector-alike holding a valid system of potentials.
// Don't need to clear/initialize
template <class G>
static void chrome_dijkstra(const G& g, const WeightIndexable auto& p,
static void chrome_dijkstra(const G& g, const PotentialFunction& p,
std::vector<std::vector<vert_id>>& colour_succs, vert_id src,
std::vector<std::tuple<vert_id, Weight>>& out) {
const size_t sz = g.size();
Expand All @@ -870,7 +865,7 @@ class GraphOps {

for (const auto e : g.e_succs(src)) {
const vert_id dest = e.vert;
dists->at(dest) = p[src] + e.val - p[dest];
dists->at(dest) = p(src) + e.val - p(dest);
dist_ts->at(dest) = ts;

vert_marks->at(dest) = edge_marks->at(sz * src + dest);
Expand All @@ -879,9 +874,9 @@ class GraphOps {

while (!heap.empty()) {
const int es = heap.removeMin();
const Weight es_cost = dists->at(es) + p[es]; // If it's on the queue, distance is not infinite.
const Weight es_cost = dists->at(es) + p(es); // If it's on the queue, distance is not infinite.
{
const Weight es_val = es_cost - p[src];
const Weight es_val = es_cost - p(src);
const auto w = g.lookup(src, es);
if (!w || *w > es_val) {
out.emplace_back(es, es_val);
Expand All @@ -896,7 +891,7 @@ class GraphOps {
const std::vector<vert_id>& es_succs =
(vert_marks->at(es) == E_LEFT) ? colour_succs[2 * es + 1] : colour_succs[2 * es];
for (vert_id ed : es_succs) {
const Weight v = es_cost + g.edge_val(es, ed) - p[ed];
const Weight v = es_cost + g.edge_val(es, ed) - p(ed);
if (dist_ts->at(ed) != ts || v < dists->at(ed)) {
dists->at(ed) = v;
dist_ts->at(ed) = ts;
Expand All @@ -917,7 +912,7 @@ class GraphOps {
// Run Dijkstra's algorithm, but similar to the chromatic algorithm, avoid expanding anything that _was_ stable.
// GKG: Factor out common elements of this & the previous algorithm.
template <class G, class S>
static void dijkstra_recover(const G& g, const WeightIndexable auto& p, const S& is_stable, vert_id src,
static void dijkstra_recover(const G& g, const PotentialFunction& p, const S& is_stable, vert_id src,
std::vector<std::tuple<vert_id, Weight>>& out) {
const size_t sz = g.size();
if (sz == 0) {
Expand All @@ -940,7 +935,7 @@ class GraphOps {

for (const auto e : g.e_succs(src)) {
const vert_id dest = e.vert;
dists->at(dest) = p[src] + e.val - p[dest];
dists->at(dest) = p(src) + e.val - p(dest);
dist_ts->at(dest) = ts;

vert_marks->at(dest) = V_UNSTABLE;
Expand All @@ -949,9 +944,9 @@ class GraphOps {

while (!heap.empty()) {
const int es = heap.removeMin();
const Weight es_cost = dists->at(es) + p[es]; // If it's on the queue, distance is not infinite.
const Weight es_cost = dists->at(es) + p(es); // If it's on the queue, distance is not infinite.
{
Weight es_val = es_cost - p[src];
Weight es_val = es_cost - p(src);
auto w = g.lookup(src, es);
if (!w || *w > es_val) {
out.emplace_back(es, es_val);
Expand All @@ -966,7 +961,7 @@ class GraphOps {
// Pick the appropriate set of successors
for (const auto e : g.e_succs(es)) {
const vert_id ed = e.vert;
const Weight v = es_cost + e.val - p[ed];
const Weight v = es_cost + e.val - p(ed);
if (dist_ts->at(ed) != ts || v < dists->at(ed)) {
dists->at(ed) = v;
dist_ts->at(ed) = ts;
Expand Down Expand Up @@ -1037,7 +1032,7 @@ class GraphOps {
}

template <class G, class V>
static edge_vector close_after_widen(const G& g, const WeightIndexable auto& p, const V& is_stable) {
static edge_vector close_after_widen(const G& g, const PotentialFunction& p, const V& is_stable) {
const size_t sz = g.size();
grow_scratch(sz);
// assert(orig.size() == sz);
Expand All @@ -1064,7 +1059,7 @@ class GraphOps {
// Compute the transitive closure of edges reachable from v, assuming
// (1) the subgraph G \ {v} is closed, and
// (2) P is a valid model of G.
static void close_after_assign_fwd(const auto& g, const WeightIndexable auto& p, vert_id v,
static void close_after_assign_fwd(const auto& g, const PotentialFunction& p, vert_id v,
std::vector<std::tuple<vert_id, Weight>>& aux) {
// Initialize the queue and distances.
for (vert_id u : g.verts()) {
Expand All @@ -1079,14 +1074,14 @@ class GraphOps {
vert_id d = e.vert;
vert_marks->at(d) = BF_QUEUED;
dists->at(d) = e.val;
// assert(p[v] + dists->at(d) - p[d] >= Weight(0));
// assert(p(v) + dists->at(d) - p(d) >= Weight(0));
*adj_tail = d;
++adj_tail;
}

// Sort the immediate edges by increasing slack.
std::sort(adj_head, adj_tail,
[&p](vert_id d1, vert_id d2) { return dists->at(d1) - p[d1] < dists->at(d2) - p[d2]; });
[&p](vert_id d1, vert_id d2) { return dists->at(d1) - p(d1) < dists->at(d2) - p(d2); });

auto reach_tail = adj_tail;
for (; adj_head < adj_tail; ++adj_head) {
Expand Down Expand Up @@ -1178,8 +1173,7 @@ class GraphOps {
// Closure is now updated.
}

template <WeightIndexable P>
static edge_vector close_after_assign(const auto& g, const P& p, vert_id v) {
static edge_vector close_after_assign(const auto& g, const PotentialFunction& p, vert_id v) {
const size_t sz = g.size();
grow_scratch(sz);
edge_vector delta;
Expand All @@ -1194,11 +1188,7 @@ class GraphOps {
std::vector<std::tuple<vert_id, Weight>> aux;
GraphRev g_rev{g};

struct NegP {
Weight operator[](vert_id v) const { return -(p[v]); }
const P& p;
};
close_after_assign_fwd(g_rev, NegP{p}, v, aux);
close_after_assign_fwd(g_rev, [&](vert_id v) { return -(p(v)); }, v, aux);
for (const auto& [vid, wt] : aux) {
delta.emplace_back(vid, v, wt);
}
Expand Down

0 comments on commit a1331aa

Please sign in to comment.