|
|
|
|
@ -184,7 +184,7 @@ impl<CW, Cel, R> Drawing<CW, Cel, R> {
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
pub fn node_count(&self) -> usize {
|
|
|
|
|
self.recording_geometry_with_rtree.graph().node_count()
|
|
|
|
|
self.recording_geometry_with_rtree.node_count()
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
@ -293,9 +293,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(())
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn add_fixed_dot(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -304,15 +303,13 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
self.add_dot(recorder, weight, &|_drawing, _infringer, _infringee| true)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() - 1))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() - 1))]
|
|
|
|
|
pub fn remove_fixed_dot(&mut self, recorder: &mut DrawingEdit<CW, Cel>, dot: FixedDotIndex) {
|
|
|
|
|
self.recording_geometry_with_rtree
|
|
|
|
|
.remove_dot(recorder, dot.into());
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
pub fn add_fixed_dot_infringably(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -321,8 +318,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
self.add_dot_infringably(recorder, weight)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn add_dot<W: AccessDotWeight + Into<PrimitiveWeight> + GetLayer>(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -338,9 +335,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(dot)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn add_fixed_seg(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -357,8 +353,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 2))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
pub fn add_fixed_seg_infringably(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -369,10 +364,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
self.add_seg_infringably(recorder, from.into(), to.into(), weight)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 2))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn add_lone_loose_seg(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -390,10 +383,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(seg)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 2))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn add_seq_loose_seg(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -412,8 +403,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(seg)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() - 1))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() - 2))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() - 1))]
|
|
|
|
|
pub fn remove_termseg(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -423,10 +413,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
.remove_seg(recorder, termseg.into())
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() >= old(self.recording_geometry_with_rtree.graph().edge_count() + 2))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn add_seg<W: AccessSegWeight + Into<PrimitiveWeight> + GetLayer>(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -484,11 +472,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(seg)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 3)
|
|
|
|
|
|| self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 4))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn add_loose_bend(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -530,10 +515,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 3))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn add_core_bend<W: AccessBendWeight + Into<PrimitiveWeight> + GetLayer>(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -554,10 +537,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(bend)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 4))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn add_outer_bend(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -567,29 +548,10 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
weight: LooseBendWeight,
|
|
|
|
|
filter: &impl Fn(&Self, PrimitiveIndex, PrimitiveIndex) -> bool,
|
|
|
|
|
) -> Result<GenericIndex<LooseBendWeight>, Infringement> {
|
|
|
|
|
let core = *self
|
|
|
|
|
.recording_geometry_with_rtree
|
|
|
|
|
.graph()
|
|
|
|
|
.neighbors(inner.index().into())
|
|
|
|
|
.filter(|ni| {
|
|
|
|
|
matches!(
|
|
|
|
|
self.recording_geometry_with_rtree
|
|
|
|
|
.graph()
|
|
|
|
|
.edge_weight(
|
|
|
|
|
self.recording_geometry_with_rtree
|
|
|
|
|
.graph()
|
|
|
|
|
.find_edge(inner.index().into(), *ni)
|
|
|
|
|
.unwrap()
|
|
|
|
|
)
|
|
|
|
|
.unwrap(),
|
|
|
|
|
GeometryLabel::Core
|
|
|
|
|
)
|
|
|
|
|
})
|
|
|
|
|
.map(|node| FixedDotIndex::new(node.index()))
|
|
|
|
|
.collect::<Vec<FixedDotIndex>>()
|
|
|
|
|
.first()
|
|
|
|
|
.unwrap();
|
|
|
|
|
|
|
|
|
|
let core = match inner {
|
|
|
|
|
BendIndex::Fixed(bend) => self.primitive(bend).core(),
|
|
|
|
|
BendIndex::Loose(bend) => self.primitive(bend).core(),
|
|
|
|
|
};
|
|
|
|
|
let bend = self.recording_geometry_with_rtree.add_bend(
|
|
|
|
|
recorder,
|
|
|
|
|
from.into(),
|
|
|
|
|
@ -604,17 +566,13 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(bend)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn flip_bend(&mut self, recorder: &mut DrawingEdit<CW, Cel>, bend: FixedBendIndex) {
|
|
|
|
|
self.recording_geometry_with_rtree
|
|
|
|
|
.flip_bend(recorder, bend.into());
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count())
|
|
|
|
|
|| self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() - 1)
|
|
|
|
|
|| self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 1))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn reattach_bend(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -628,10 +586,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 4))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() >= old(self.recording_geometry_with_rtree.graph().edge_count() + 5))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 4))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn insert_cane(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -670,8 +626,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(cane)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn update_this_and_outward_bows(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -751,10 +706,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(())
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 4))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() >= old(self.recording_geometry_with_rtree.graph().edge_count() + 5))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 4))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn add_cane(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -820,7 +773,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
})
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() - 4))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() - 4))]
|
|
|
|
|
pub fn remove_cane(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -856,8 +809,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Cane::from_dot(dot, self)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
pub fn move_dot(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -880,8 +832,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn move_dot_with_infringement_filtering(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -916,8 +867,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
Ok(())
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
fn shift_bend_with_infringement_filtering(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -945,8 +895,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
fn add_dot_infringably<W: AccessDotWeight + Into<PrimitiveWeight> + GetLayer>(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -958,8 +907,7 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
self.recording_geometry_with_rtree.add_dot(recorder, weight)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 2))]
|
|
|
|
|
#[debug_ensures(self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() + 1))]
|
|
|
|
|
fn add_seg_infringably<W: AccessSegWeight + Into<PrimitiveWeight> + GetLayer>(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
@ -1007,9 +955,8 @@ impl<CW: Clone, Cel: Copy, R: AccessRules> Drawing<CW, Cel, R> {
|
|
|
|
|
);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() - 1))]
|
|
|
|
|
#[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count()))]
|
|
|
|
|
#[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.total_node_count() == old(self.recording_geometry_with_rtree.total_node_count() - 1))]
|
|
|
|
|
fn fail_and_remove_if_infringes_except(
|
|
|
|
|
&mut self,
|
|
|
|
|
recorder: &mut DrawingEdit<CW, Cel>,
|
|
|
|
|
|