Skip to content

Commit

Permalink
GraphOps: refactor lambda objects, encapsulate private
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 f2bdc93 commit 9f415e8
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 19 deletions.
19 changes: 12 additions & 7 deletions src/crab/split_dbm.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,6 +237,10 @@ void SplitDBM::diffcsts_of_lin_leq(const linear_expression_t& exp,
}
}

static GraphOps::PotentialFunction index_to_call(const GraphOps::WeightVector& p) {
return [&p](GraphOps::vert_id v) -> GraphOps::Weight { return p[v]; };
}

bool SplitDBM::add_linear_leq(const linear_expression_t& exp) {
std::vector<std::pair<variable_t, Weight>> lbs, ubs;
std::vector<diffcst_t> csts;
Expand Down Expand Up @@ -281,7 +285,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, [&](vert_id v){ return potential[v]; }, 0));
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, index_to_call(potential), 0));
normalize();
return true;
}
Expand Down Expand Up @@ -504,7 +508,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), [&](vert_id v) { return pot_rx[v]; }, gx, g_ix_ry));
GraphOps::apply_delta(g_rx, GraphOps::close_after_meet(SubGraph(g_rx, 0),index_to_call(pot_rx), gx, g_ix_ry));
}

graph_t g_rx_iy;
Expand All @@ -525,7 +529,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), [&](vert_id v) { return pot_ry[v]; }, gy, g_rx_iy));
GraphOps::apply_delta(g_ry, GraphOps::close_after_meet(SubGraph(g_ry, 0), index_to_call(pot_ry), 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,7 +734,7 @@ std::optional<SplitDBM> SplitDBM::meet(const SplitDBM& o) const {
}

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

// Recover updated LBs and UBs.<
Expand Down Expand Up @@ -892,7 +896,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), [&](vert_id v){ return potential[v]; }, vert));
GraphOps::apply_delta(g, GraphOps::close_after_assign(SubGraph(g, 0), index_to_call(potential), vert));

if (lb_w) {
g.update_edge(vert, *lb_w, 0);
Expand Down Expand Up @@ -947,9 +951,10 @@ 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), [&](vert_id v){ return potential[v]; }, vert_set_wrap_t(unstable)));
const auto p = index_to_call(potential);
GraphOps::apply_delta(g, GraphOps::close_after_widen(SubGraph(g, 0), p, vert_set_wrap_t(unstable)));
// Retrieve variable bounds
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, [&](vert_id v){ return potential[v]; }, 0));
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, p, 0));

unstable.clear();
}
Expand Down
2 changes: 1 addition & 1 deletion src/crab/split_dbm.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ namespace domains {
class SplitDBM final {
public:
using graph_t = AdaptGraph;
using Weight = AdaptGraph::Weight;
using Weight = graph_t::Weight;
using vert_id = graph_t::vert_id;
using vert_map_t = boost::container::flat_map<variable_t, vert_id>;

Expand Down
22 changes: 11 additions & 11 deletions src/crab_utils/graph_ops.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -414,7 +414,7 @@ class SubGraph {
iterator begin() const { return iterator(rG.begin(), v_ex); }
iterator end() const { return iterator(rG.end(), v_ex); }

protected:
private:
R rG;
vert_id v_ex;
};
Expand Down Expand Up @@ -446,7 +446,6 @@ class GraphRev {
public:
using vert_id = typename G::vert_id;
using Weight = typename G::Weight;
// using g_adj_list = G::adj_list;
using mut_val_ref_t = typename G::mut_val_ref_t;

explicit GraphRev(G& _g) : g(_g) {}
Expand All @@ -469,8 +468,6 @@ class GraphRev {
return g.size();
}

// using adj_list = G::adj_list;

using neighbour_const_range = typename G::neighbour_const_range;
using e_neighbour_const_range = typename G::e_neighbour_const_range;

Expand Down Expand Up @@ -498,8 +495,6 @@ class GraphOps {

using edge_vector = std::vector<std::tuple<vert_id, vert_id, Weight>>;

using edge_ref = std::tuple<vert_id, vert_id, Weight>;

//===========================================
// Enums used to mark vertices/edges during algorithms
//===========================================
Expand All @@ -509,7 +504,7 @@ class GraphOps {
enum SMarkT { V_UNSTABLE = 0, V_STABLE = 1 };
// Whether a vertex is in the current SCC/queue for Bellman-Ford.
enum QMarkT { BF_NONE = 0, BF_SCC = 1, BF_QUEUED = 2 };

private:
// Scratch space needed by the graph algorithms.
// Should really switch to some kind of arena allocator, rather
// than having all these static structures.
Expand All @@ -530,6 +525,7 @@ class GraphOps {
static inline thread_local unsigned int ts;
static inline thread_local unsigned int ts_idx;

public:
static void clear_thread_local_state() {
dists.clear();
dists_alt.clear();
Expand All @@ -541,7 +537,7 @@ class GraphOps {
ts = 0;
ts_idx = 0;
}

private:
static void grow_scratch(const size_t sz) {
if (sz <= scratch_sz) {
return;
Expand Down Expand Up @@ -569,6 +565,7 @@ class GraphOps {
}
}

public:
// Syntactic join.
static graph_t join(auto& l, auto& r) {
// For the join, potentials are preserved
Expand Down Expand Up @@ -638,6 +635,7 @@ class GraphOps {
return g;
}

private:
// Compute the strongly connected components.
// Duped pretty much verbatim from Wikipedia.
// Abuses 'dual_queue' to store indices.
Expand Down Expand Up @@ -695,6 +693,7 @@ class GraphOps {
}
}

public:
// Run Bellman-Ford to compute a valid model of a set of difference constraints.
// Returns false if there is some negative cycle.
static bool select_potentials(const auto& g, WeightVector& potentials) {
Expand Down Expand Up @@ -840,6 +839,7 @@ class GraphOps {
}
}

private:
static bool dists_compare(int x, int y) { return (*dists)[x] < (*dists)[y]; }

// P is some vector-alike holding a valid system of potentials.
Expand Down Expand Up @@ -978,7 +978,7 @@ class GraphOps {
}
}
}

public:
template <class G>
static bool repair_potential(const G& g, WeightVector& p, vert_id ii, vert_id jj) {
// Ensure there's enough scratch space.
Expand Down Expand Up @@ -1055,7 +1055,7 @@ class GraphOps {
}
return delta;
}

private:
// 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.
Expand Down Expand Up @@ -1109,7 +1109,7 @@ class GraphOps {
vert_marks->at(*adj_head) = 0;
}
}

public:
static void close_over_edge(graph_t& g, vert_id ii, vert_id jj) {
assert(ii != 0 && jj != 0);
SubGraph<graph_t> g_excl(g, 0);
Expand Down

0 comments on commit 9f415e8

Please sign in to comment.