berkus
/
topola
mirror of https://codeberg.org/topola/topola.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

layout: Add contracts for node and edge counts

This commit is contained in:
Mikolaj Wielgus 2023-09-16 18:24:57 +02:00
parent 7d2cff9004
commit 394510de8d
1 changed files with 21 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/layout.rs
View File

@ -1,4 +1,4 @@
use contracts::debug_invariant; use contracts::{debug_ensures, debug_invariant};
use geo::Point; use geo::Point;
use petgraph::stable_graph::StableDiGraph; use petgraph::stable_graph::StableDiGraph;
use petgraph::visit::EdgeRef; use petgraph::visit::EdgeRef;
@ -32,6 +32,7 @@ impl Layout {
} }
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count() - path.interior().len()))]
pub fn remove_interior(&mut self, path: &impl Interior<TaggedIndex>) { pub fn remove_interior(&mut self, path: &impl Interior<TaggedIndex>) {
for index in path.interior().iter().filter(|index| !index.is_dot()) { for index in path.interior().iter().filter(|index| !index.is_dot()) {
untag!(index, self.remove(*index)); untag!(index, self.remove(*index));
@ -45,6 +46,7 @@ impl Layout {
} }
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count() - 1))]
pub fn remove<Weight: std::marker::Copy>(&mut self, index: Index<Weight>) { pub fn remove<Weight: std::marker::Copy>(&mut self, index: Index<Weight>) {
// Unnecessary retag. It should be possible to elide it. // Unnecessary retag. It should be possible to elide it.
let weight = *self.graph.node_weight(index.index).unwrap(); let weight = *self.graph.node_weight(index.index).unwrap();
@ -53,6 +55,7 @@ impl Layout {
self.graph.remove_node(index.index); self.graph.remove_node(index.index);
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count() + 1))]
pub fn add_dot(&mut self, weight: DotWeight) -> Result<DotIndex, ()> { pub fn add_dot(&mut self, weight: DotWeight) -> Result<DotIndex, ()> {
let dot = DotIndex::new(self.graph.add_node(TaggedWeight::Dot(weight))); let dot = DotIndex::new(self.graph.add_node(TaggedWeight::Dot(weight)));
@ -62,6 +65,8 @@ impl Layout {
Ok(dot) Ok(dot)
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count() + 1))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count() + 2))]
pub fn add_seg( pub fn add_seg(
&mut self, &mut self,
from: DotIndex, from: DotIndex,
@ -92,6 +97,7 @@ impl Layout {
Ok(seg) Ok(seg)
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count() + 1))]
pub fn add_bend( pub fn add_bend(
&mut self, &mut self,
from: DotIndex, from: DotIndex,
@ -106,6 +112,8 @@ impl Layout {
} }
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count() + 1))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count() + 3))]
pub fn add_core_bend( pub fn add_core_bend(
&mut self, &mut self,
from: DotIndex, from: DotIndex,
@ -124,6 +132,8 @@ impl Layout {
Ok(bend) Ok(bend)
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count() + 1))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count() + 2))]
pub fn add_outer_bend( pub fn add_outer_bend(
&mut self, &mut self,
from: DotIndex, from: DotIndex,
@ -149,6 +159,8 @@ impl Layout {
Ok(bend) Ok(bend)
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
pub fn reattach_bend(&mut self, bend: BendIndex, inner: BendIndex) { pub fn reattach_bend(&mut self, bend: BendIndex, inner: BendIndex) {
if let Some(old_inner_edge) = self if let Some(old_inner_edge) = self
.graph .graph
@ -161,6 +173,8 @@ impl Layout {
self.graph.add_edge(inner.index, bend.index, Label::Outer); self.graph.add_edge(inner.index, bend.index, Label::Outer);
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
pub fn extend_bend(&mut self, bend: BendIndex, dot: DotIndex, to: Point) -> Result<(), ()> { pub fn extend_bend(&mut self, bend: BendIndex, dot: DotIndex, to: Point) -> Result<(), ()> {
self.remove_from_rtree(bend.tag()); self.remove_from_rtree(bend.tag());
let result = self.move_dot(dot, to); let result = self.move_dot(dot, to);
@ -211,6 +225,8 @@ impl Layout {
} }
impl Layout { impl Layout {
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
pub fn move_dot(&mut self, dot: DotIndex, to: Point) -> Result<(), ()> { pub fn move_dot(&mut self, dot: DotIndex, to: Point) -> Result<(), ()> {
let mut cur_bend = self.primitive(dot).outer(); let mut cur_bend = self.primitive(dot).outer();
loop { loop {
@ -277,11 +293,15 @@ impl Layout {
.next() .next()
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
fn insert_into_rtree(&mut self, index: TaggedIndex) { fn insert_into_rtree(&mut self, index: TaggedIndex) {
let shape = untag!(index, self.primitive(index).shape()); let shape = untag!(index, self.primitive(index).shape());
self.rtree.insert(RTreeWrapper::new(shape, index)); self.rtree.insert(RTreeWrapper::new(shape, index));
} }
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
fn remove_from_rtree(&mut self, index: TaggedIndex) { fn remove_from_rtree(&mut self, index: TaggedIndex) {
let shape = untag!(index, self.primitive(index).shape()); let shape = untag!(index, self.primitive(index).shape());
debug_assert!(self debug_assert!(self