diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp index dc449c5b..dbd7e237 100644 --- a/src/crab/split_dbm.cpp +++ b/src/crab/split_dbm.cpp @@ -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> lbs, ubs; std::vector csts; @@ -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, potential, 0)); + GraphOps::apply_delta(g, GraphOps::close_after_assign(g, index_to_call(potential), 0)); normalize(); return true; } @@ -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), pot_rx, 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; @@ -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), pot_ry, 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, @@ -730,11 +734,12 @@ std::optional 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)); + 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.< - 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"); @@ -891,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), potential, 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); @@ -946,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), potential, 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, potential, 0)); + GraphOps::apply_delta(g, GraphOps::close_after_assign(g, p, 0)); unstable.clear(); } diff --git a/src/crab/split_dbm.hpp b/src/crab/split_dbm.hpp index f508dea7..82ef3189 100644 --- a/src/crab/split_dbm.hpp +++ b/src/crab/split_dbm.hpp @@ -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; diff --git a/src/crab_utils/graph_ops.hpp b/src/crab_utils/graph_ops.hpp index 8c26d093..5e2d28ec 100644 --- a/src/crab_utils/graph_ops.hpp +++ b/src/crab_utils/graph_ops.hpp @@ -26,7 +26,6 @@ class GraphPerm { using vert_id = typename G::vert_id; constexpr static vert_id invalid_vert = std::numeric_limits::max(); using Weight = typename G::Weight; - using g_neighbour_const_range = typename G::neighbour_const_range; using mut_val_ref_t = typename G::mut_val_ref_t; GraphPerm(const std::vector& _perm, G& _g) : g{_g}, perm{_perm}, inv(_g.size(), invalid_vert) { @@ -125,7 +124,7 @@ class GraphPerm { } bool operator!=(const adj_const_iterator& other) { - while (v != other.v && inv[*v] == (invalid_vert)) { + while (v != other.v && inv[*v] == invalid_vert) { ++v; } return v != other.v; @@ -151,7 +150,7 @@ class GraphPerm { } bool operator!=(const e_adj_const_iterator& other) { - while (v != other.v && inv[(*v).vert] == (invalid_vert)) { + while (v != other.v && inv[(*v).vert] == invalid_vert) { ++v; } return v != other.v; @@ -189,7 +188,7 @@ class GraphPerm { [[nodiscard]] bool mem(unsigned int v) const { - if (!adj || perm[v] == (invalid_vert)) { + if (!adj || perm[v] == invalid_vert) { return false; } return (*adj).mem(perm[v]); @@ -229,7 +228,7 @@ class GraphPerm { [[nodiscard]] bool mem(unsigned int v) const { - if (!adj || perm[v] == (invalid_vert)) { + if (!adj || perm[v] == invalid_vert) { return false; } return (*adj).mem(perm[v]); @@ -247,26 +246,26 @@ class GraphPerm { e_adj_const_iterator>; neighbour_const_range succs(vert_id v) const { - if (perm[v] == (invalid_vert)) { + if (perm[v] == invalid_vert) { return neighbour_const_range(perm, inv); } return neighbour_const_range(perm, inv, g.succs(perm[v])); } neighbour_const_range preds(vert_id v) const { - if (perm[v] == (invalid_vert)) { + if (perm[v] == invalid_vert) { return neighbour_const_range(perm, inv); } return neighbour_const_range(perm, inv, g.preds(perm[v])); } e_neighbour_const_range e_succs(vert_id v) const { - if (perm[v] == (invalid_vert)) { + if (perm[v] == invalid_vert) { return e_neighbour_const_range(perm, inv); } return e_neighbour_const_range(perm, inv, g.e_succs(perm[v])); } e_neighbour_const_range e_preds(vert_id v) const { - if (perm[v] == (invalid_vert)) { + if (perm[v] == invalid_vert) { return e_neighbour_const_range(perm, inv); } return e_neighbour_const_range(perm, inv, g.e_preds(perm[v])); @@ -407,14 +406,13 @@ class SubGraph { template class adj_list { public: - using g_iter = typename R::iterator; using iterator = It; adj_list(const R& _rG, vert_id _v_ex) : rG(_rG), v_ex(_v_ex) {} 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; }; @@ -446,7 +444,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) {} @@ -469,8 +466,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; @@ -484,13 +479,6 @@ class GraphRev { G& g; }; -// temporary concept: indexable -// TODO: replace everywhere with simple callable -template -concept WeightIndexable = requires(T t, AdaptGraph::vert_id v) { - { t[v] } -> std::convertible_to; -}; - // GKG - What's the best way to split this out? class GraphOps { public: @@ -499,12 +487,12 @@ class GraphOps { using Weight = typename graph_t::Weight; using vert_id = typename graph_t::vert_id; using WeightVector = std::vector; + + using PotentialFunction = std::function; using mut_val_ref_t = typename graph_t::mut_val_ref_t; using edge_vector = std::vector>; - using edge_ref = std::tuple; - //=========================================== // Enums used to mark vertices/edges during algorithms //=========================================== @@ -514,7 +502,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. @@ -535,6 +523,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(); @@ -546,7 +535,7 @@ class GraphOps { ts = 0; ts_idx = 0; } - + private: static void grow_scratch(const size_t sz) { if (sz <= scratch_sz) { return; @@ -574,6 +563,7 @@ class GraphOps { } } + public: // Syntactic join. static graph_t join(auto& l, auto& r) { // For the join, potentials are preserved @@ -643,6 +633,7 @@ class GraphOps { return g; } + private: // Compute the strongly connected components. // Duped pretty much verbatim from Wikipedia. // Abuses 'dual_queue' to store indices. @@ -700,6 +691,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) { @@ -786,7 +778,7 @@ class GraphOps { } template - 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()); @@ -845,14 +837,14 @@ 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. // Don't need to clear/initialize template - static void chrome_dijkstra(const G& g, const WeightIndexable auto& p, - std::vector>& colour_succs, vert_id src, - std::vector>& out) { + static void chrome_dijkstra(const G& g, const PotentialFunction& p, std::vector>& colour_succs, + vert_id src, std::vector>& out) { const size_t sz = g.size(); if (sz == 0) { return; @@ -870,7 +862,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); @@ -879,9 +871,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); @@ -896,7 +888,7 @@ class GraphOps { const std::vector& 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; @@ -917,8 +909,8 @@ 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 - static void dijkstra_recover(const G& g, const WeightIndexable auto& p, const S& is_stable, vert_id src, - std::vector>& out) { + static void dijkstra_recover(const G& g, const PotentialFunction& p, const S& is_stable, vert_id src, + edge_vector& delta) { const size_t sz = g.size(); if (sz == 0) { return; @@ -940,7 +932,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; @@ -949,12 +941,12 @@ 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); + delta.emplace_back(src, es, es_val); } } if (vert_marks->at(es) == V_STABLE) { @@ -966,7 +958,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; @@ -983,7 +975,7 @@ class GraphOps { } } } - + public: template static bool repair_potential(const G& g, WeightVector& p, vert_id ii, vert_id jj) { // Ensure there's enough scratch space. @@ -1037,7 +1029,7 @@ class GraphOps { } template - 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); @@ -1048,23 +1040,18 @@ class GraphOps { edge_marks->at(v) = is_stable[v] ? V_STABLE : V_UNSTABLE; } edge_vector delta; - std::vector> aux; for (vert_id v : g.verts()) { if (!edge_marks->at(v)) { - aux.clear(); - dijkstra_recover(g, p, edge_marks->begin(), v, aux); - for (const auto& [vid, wt] : aux) { - delta.emplace_back(v, vid, wt); - } + dijkstra_recover(g, p, *edge_marks, v, delta); } } 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. - 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>& aux) { // Initialize the queue and distances. for (vert_id u : g.verts()) { @@ -1079,14 +1066,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) { @@ -1114,7 +1101,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 g_excl(g, 0); @@ -1178,8 +1165,7 @@ class GraphOps { // Closure is now updated. } - template - 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; @@ -1194,11 +1180,7 @@ class GraphOps { std::vector> 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); }