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

fix(contracts,drawing): geometry_with_rtree -> recording_geometry_with_rtree 

Fixes #105.
This commit is contained in:
Alain Emilia Anna Zscheile 2024-11-20 15:41:22 +01:00
parent fd22413057
commit 9dad83d221
1 changed files with 75 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

150
src/drawing/drawing.rs
View File

@ -176,9 +176,9 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(()) Ok(())
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn add_fixed_dot( pub fn add_fixed_dot(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -187,15 +187,15 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
self.add_dot_with_infringables(recorder, weight, Some(&[])) self.add_dot_with_infringables(recorder, weight, Some(&[]))
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() - 1))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() - 1))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn remove_fixed_dot(&mut self, recorder: &mut DrawingEdit<CW>, dot: FixedDotIndex) { pub fn remove_fixed_dot(&mut self, recorder: &mut DrawingEdit<CW>, dot: FixedDotIndex) {
self.recording_geometry_with_rtree self.recording_geometry_with_rtree
.remove_dot(recorder, dot.into()); .remove_dot(recorder, dot.into());
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn add_fixed_dot_infringably( pub fn add_fixed_dot_infringably(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -204,8 +204,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
self.add_dot_infringably(recorder, weight) self.add_dot_infringably(recorder, weight)
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
fn add_dot_with_infringables<W: AccessDotWeight<PrimitiveWeight> + GetLayer>( fn add_dot_with_infringables<W: AccessDotWeight<PrimitiveWeight> + GetLayer>(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -221,9 +221,9 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(dot) Ok(dot)
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn add_fixed_seg( pub fn add_fixed_seg(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -234,8 +234,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
self.add_seg_with_infringables(recorder, from.into(), to.into(), weight, Some(&[])) self.add_seg_with_infringables(recorder, from.into(), to.into(), weight, Some(&[]))
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 2))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 2))]
pub fn add_fixed_seg_infringably( pub fn add_fixed_seg_infringably(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -246,10 +246,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
self.add_seg_infringably(recorder, from.into(), to.into(), weight) self.add_seg_infringably(recorder, from.into(), to.into(), weight)
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 2))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn add_lone_loose_seg( pub fn add_lone_loose_seg(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -262,10 +262,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(seg) Ok(seg)
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 2))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn add_seq_loose_seg( pub fn add_seq_loose_seg(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -277,10 +277,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(seg) Ok(seg)
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().edge_count() >= old(self.geometry_with_rtree.graph().edge_count() + 2))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn add_seg_with_infringables<W: AccessSegWeight<PrimitiveWeight> + GetLayer>( fn add_seg_with_infringables<W: AccessSegWeight<PrimitiveWeight> + GetLayer>(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -298,11 +298,11 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(seg) Ok(seg)
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 3) #[debug_ensures(ret.is_ok() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 3)
|| self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 4))] || self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 4))]
#[debug_ensures(ret.is_err() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn add_loose_bend_with_infringables( fn add_loose_bend_with_infringables(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -364,10 +364,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
} }
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 3))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn add_core_bend_with_infringables<W: AccessBendWeight<PrimitiveWeight> + GetLayer>( fn add_core_bend_with_infringables<W: AccessBendWeight<PrimitiveWeight> + GetLayer>(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -388,10 +388,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(bend) Ok(bend)
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 4))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn add_outer_bend_with_infringables( fn add_outer_bend_with_infringables(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -438,17 +438,17 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(bend) Ok(bend)
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn flip_bend(&mut self, recorder: &mut DrawingEdit<CW>, bend: FixedBendIndex) { pub fn flip_bend(&mut self, recorder: &mut DrawingEdit<CW>, bend: FixedBendIndex) {
self.recording_geometry_with_rtree self.recording_geometry_with_rtree
.flip_bend(recorder, bend.into()); .flip_bend(recorder, bend.into());
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()) #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count())
|| self.geometry_with_rtree.graph().edge_count() == old(self.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)
|| self.geometry_with_rtree.graph().edge_count() == old(self.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))]
fn reattach_bend( fn reattach_bend(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -462,10 +462,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
); );
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 4))] #[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.geometry_with_rtree.graph().edge_count() >= old(self.geometry_with_rtree.graph().edge_count() + 5))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn insert_cane( pub fn insert_cane(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -511,8 +511,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
} }
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn update_this_and_outward_bows( fn update_this_and_outward_bows(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -624,10 +624,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(()) Ok(())
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 4))] #[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.geometry_with_rtree.graph().edge_count() >= old(self.geometry_with_rtree.graph().edge_count() + 5))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn add_cane( pub fn add_cane(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -650,10 +650,10 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
) )
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 4))] #[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.geometry_with_rtree.graph().edge_count() >= old(self.geometry_with_rtree.graph().edge_count() + 5))] #[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.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(ret.is_err() -> self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn add_cane_with_infringables( fn add_cane_with_infringables(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -712,7 +712,7 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
}) })
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() - 4))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() - 4))]
pub fn remove_cane( pub fn remove_cane(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -748,8 +748,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Cane::from_dot(dot, self) Cane::from_dot(dot, self)
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn move_dot( pub fn move_dot(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -762,8 +762,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
} }
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn move_dot_with_infringables( fn move_dot_with_infringables(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -798,8 +798,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
Ok(()) Ok(())
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn shift_bend_with_infringables( fn shift_bend_with_infringables(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -845,8 +845,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
} }
impl<CW: Copy, R: AccessRules> Drawing<CW, R> { impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
fn add_dot_infringably<W: AccessDotWeight<PrimitiveWeight> + GetLayer>( fn add_dot_infringably<W: AccessDotWeight<PrimitiveWeight> + GetLayer>(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -858,8 +858,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
self.recording_geometry_with_rtree.add_dot(recorder, weight) self.recording_geometry_with_rtree.add_dot(recorder, weight)
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count() + 1))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 2))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count() + 2))]
fn add_seg_infringably<W: AccessSegWeight<PrimitiveWeight> + GetLayer>( fn add_seg_infringably<W: AccessSegWeight<PrimitiveWeight> + GetLayer>(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -894,9 +894,9 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
.add_to_compound(recorder, primitive, compound); .add_to_compound(recorder, primitive, compound);
} }
#[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_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.geometry_with_rtree.graph().node_count() == old(self.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() - 1))]
fn fail_and_remove_if_infringes_except( fn fail_and_remove_if_infringes_except(
&mut self, &mut self,
recorder: &mut DrawingEdit<CW>, recorder: &mut DrawingEdit<CW>,
@ -1052,8 +1052,8 @@ impl<CW: Copy, R: AccessRules> Drawing<CW, R> {
self.recording_geometry_with_rtree.rtree() self.recording_geometry_with_rtree.rtree()
} }
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().node_count() == old(self.recording_geometry_with_rtree.graph().node_count()))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] #[debug_ensures(self.recording_geometry_with_rtree.graph().edge_count() == old(self.recording_geometry_with_rtree.graph().edge_count()))]
pub fn rules_mut(&mut self) -> &mut R { pub fn rules_mut(&mut self) -> &mut R {
&mut self.rules &mut self.rules
} }