Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Specialize GraphOps #809

Merged
merged 1 commit into from
Dec 2, 2024
Merged

Specialize GraphOps #809

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 27 additions & 20 deletions src/crab/split_dbm.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@

#include "crab/split_dbm.hpp"
#include "crab_utils/debug.hpp"
#include "crab_utils/graph_ops.hpp"
#include "crab_utils/stats.hpp"
#include "string_constraints.hpp"
#include "type_encoding.hpp"
Expand Down Expand Up @@ -278,9 +279,9 @@ bool SplitDBM::add_linear_leq(const linear_expression_t& exp) {
if (!repair_potential(src, dest)) {
return false;
}
GrOps::close_over_edge(g, src, dest);
GraphOps::close_over_edge(g, src, dest);
}
GrOps::apply_delta(g, GrOps::close_after_assign(g, potential, 0));
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, potential, 0));
normalize();
return true;
}
Expand Down Expand Up @@ -501,9 +502,9 @@ SplitDBM SplitDBM::operator|(const SplitDBM& o) const& {
}
// Apply the deferred relations, and re-close.
bool is_closed;
graph_t g_rx(GrOps::meet(gx, g_ix_ry, is_closed));
graph_t g_rx(GraphOps::meet(gx, g_ix_ry, is_closed));
if (!is_closed) {
GrOps::apply_delta(g_rx, GrOps::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), pot_rx, gx, g_ix_ry));
}

graph_t g_rx_iy;
Expand All @@ -522,14 +523,14 @@ SplitDBM SplitDBM::operator|(const SplitDBM& o) const& {
}
}
// Similarly, should use a SubGraph view.
graph_t g_ry(GrOps::meet(gy, g_rx_iy, is_closed));
graph_t g_ry(GraphOps::meet(gy, g_rx_iy, is_closed));
if (!is_closed) {
GrOps::apply_delta(g_ry, GrOps::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), pot_ry, gy, g_rx_iy));
}

// We now have the relevant set of relations. Because g_rx and g_ry are closed,
// the result is also closed.
graph_t join_g(GrOps::join(g_rx, g_ry));
graph_t join_g(GraphOps::join(g_rx, g_ry));

// Now reapply the missing independent relations.
// Need to derive vert_ids from lb_up/lb_down, and make sure the vertices exist
Expand Down Expand Up @@ -646,7 +647,7 @@ SplitDBM SplitDBM::widen(const SplitDBM& o) const {

// Now perform the widening
vert_set_t widen_unstable(unstable);
graph_t widen_g(GrOps::widen(gx, gy, widen_unstable));
graph_t widen_g(GraphOps::widen(gx, gy, widen_unstable));

SplitDBM res(std::move(out_vmap), std::move(out_revmap), std::move(widen_g), std::move(widen_pot),
std::move(widen_unstable));
Expand Down Expand Up @@ -717,23 +718,23 @@ std::optional<SplitDBM> SplitDBM::meet(const SplitDBM& o) const {
GraphPerm gy(perm_y, o.g);

// Compute the syntactic meet of the permuted graphs.
bool is_closed;
graph_t meet_g(GrOps::meet(gx, gy, is_closed));
bool is_closed{};
graph_t meet_g(GraphOps::meet(gx, gy, is_closed));

// Compute updated potentials on the zero-enriched graph
// vector<Weight> meet_pi(meet_g.size());
// We've warm-started pi with the operand potentials
if (!GrOps::select_potentials(meet_g, meet_pi)) {
if (!GraphOps::select_potentials(meet_g, meet_pi)) {
// Potentials cannot be selected -- state is infeasible.
return {};
}

if (!is_closed) {
GrOps::apply_delta(meet_g, GrOps::close_after_meet(SubGraph(meet_g, 0), meet_pi, gx, gy));
GraphOps::apply_delta(meet_g, GraphOps::close_after_meet(SubGraph(meet_g, 0), meet_pi, gx, gy));

// Recover updated LBs and UBs.<

GrOps::apply_delta(meet_g, GrOps::close_after_assign(meet_g, meet_pi, 0));
GraphOps::apply_delta(meet_g, GraphOps::close_after_assign(meet_g, meet_pi, 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 @@ -878,7 +879,7 @@ void SplitDBM::assign(variable_t lhs, const linear_expression_t& e) {
}

{
edge_vector delta;
GraphOps::edge_vector delta;
for (const auto& [var, n] : diffs_lb) {
delta.emplace_back(vert, get_vert(var), -n);
}
Expand All @@ -888,9 +889,9 @@ void SplitDBM::assign(variable_t lhs, const linear_expression_t& e) {
}

// apply_delta should be safe here, as x has no edges in G.
GrOps::apply_delta(g, delta);
GraphOps::apply_delta(g, delta);
}
GrOps::apply_delta(g, GrOps::close_after_assign(SubGraph(g, 0), potential, vert));
GraphOps::apply_delta(g, GraphOps::close_after_assign(SubGraph(g, 0), potential, vert));

if (lb_w) {
g.update_edge(vert, *lb_w, 0);
Expand Down Expand Up @@ -926,6 +927,12 @@ class vert_set_wrap_t {
const SplitDBM::vert_set_t& vs;
};

bool SplitDBM::repair_potential(vert_id src, vert_id dest) {
return GraphOps::repair_potential(g, potential, src, dest);
}

void SplitDBM::clear_thread_local_state() { GraphOps::clear_thread_local_state(); }

void SplitDBM::normalize() {
CrabStats::count("SplitDBM.count.normalize");
ScopedCrabStats __st__("SplitDBM.normalize");
Expand All @@ -936,12 +943,12 @@ void SplitDBM::normalize() {
return;
}

edge_vector delta;
// GrOps::close_after_widen(g, potential, vert_set_wrap_t(unstable), delta);
GraphOps::edge_vector delta;
// GraphOps::close_after_widen(g, potential, vert_set_wrap_t(unstable), delta);
// GKG: Check
GrOps::apply_delta(g, GrOps::close_after_widen(SubGraph(g, 0), potential, vert_set_wrap_t(unstable)));
GraphOps::apply_delta(g, GraphOps::close_after_widen(SubGraph(g, 0), potential, vert_set_wrap_t(unstable)));
// Retrieve variable bounds
GrOps::apply_delta(g, GrOps::close_after_assign(g, potential, 0));
GraphOps::apply_delta(g, GraphOps::close_after_assign(g, potential, 0));

unstable.clear();
}
Expand Down
7 changes: 2 additions & 5 deletions src/crab/split_dbm.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@
#include "crab/variable.hpp"
#include "crab_utils/adapt_sgraph.hpp"
#include "crab_utils/debug.hpp"
#include "crab_utils/graph_ops.hpp"
#include "crab_utils/num_big.hpp"
#include "crab_utils/num_safeint.hpp"
#include "crab_utils/stats.hpp"
Expand All @@ -57,8 +56,6 @@ class SplitDBM final {
using variable_vector_t = std::vector<variable_t>;

using rev_map_t = std::vector<std::optional<variable_t>>;
using GrOps = GraphOps<graph_t>;
using edge_vector = GrOps::edge_vector;
// < <x, y>, k> == x - y <= k.
using diffcst_t = std::pair<std::pair<variable_t, variable_t>, Weight>;
using vert_set_t = std::unordered_set<vert_id>;
Expand Down Expand Up @@ -129,7 +126,7 @@ class SplitDBM final {
interval_t get_interval(variable_t x, int finite_width) const;

// Restore potential after an edge addition
bool repair_potential(vert_id src, vert_id dest) { return GrOps::repair_potential(g, potential, src, dest); }
bool repair_potential(vert_id src, vert_id dest);

void normalize();

Expand Down Expand Up @@ -304,7 +301,7 @@ class SplitDBM final {
string_invariant to_set() const;

public:
static void clear_thread_local_state() { GraphOps<AdaptGraph>::clear_thread_local_state(); }
static void clear_thread_local_state();
}; // class SplitDBM

} // namespace domains
Expand Down
Loading
Loading