From 98363fbfd1b7d7368171ba90f3cbb6d02beae838 Mon Sep 17 00:00:00 2001 From: Mikolaj Wielgus Date: Sat, 8 Jun 2024 18:07:59 +0200 Subject: [PATCH] drawing: remove unnecessary contracts on `&self` methods --- src/drawing/drawing.rs | 24 ------------------------ 1 file changed, 24 deletions(-) diff --git a/src/drawing/drawing.rs b/src/drawing/drawing.rs index 7625d23..4eb49d8 100644 --- a/src/drawing/drawing.rs +++ b/src/drawing/drawing.rs @@ -729,8 +729,6 @@ impl Drawing { Ok(()) } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] fn detect_infringement_except( &self, node: PrimitiveIndex, @@ -777,8 +775,6 @@ impl Drawing { .and_then(|infringee| Some(Infringement(inflated_shape, infringee))) } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] fn detect_collision(&self, node: PrimitiveIndex) -> Option { let shape = node.primitive(self).shape(); @@ -799,8 +795,6 @@ impl Drawing { .and_then(|collidee| Some(Collision(shape, collidee))) } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] fn are_connectable(&self, node1: PrimitiveIndex, node2: PrimitiveIndex) -> bool { if let (Some(node1_net_id), Some(node2_net_id)) = ( node1.primitive(self).maybe_net(), @@ -814,8 +808,6 @@ impl Drawing { } impl Drawing { - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn geometry( &self, ) -> &Geometry< @@ -832,50 +824,34 @@ impl Drawing { self.geometry_with_rtree.geometry() } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn rtree(&self) -> &RTree>>> { self.geometry_with_rtree.rtree() } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn layer_count(&self) -> u64 { self.geometry_with_rtree.layer_count() } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn rules(&self) -> &R { &self.rules } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn guide(&self) -> Guide { Guide::new(self) } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn collect(&self) -> Collect { Collect::new(self) } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn primitive(&self, index: GenericIndex) -> GenericPrimitive { GenericPrimitive::new(index, self) } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn wraparoundable(&self, index: WraparoundableIndex) -> Wraparoundable { Wraparoundable::new(index, self) } - #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))] - #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))] pub fn loose(&self, index: LooseIndex) -> Loose { Loose::new(index, self) }