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

drawing: add invariant contract for pairwise non-infringement of looses

This commit is contained in:
Mikolaj Wielgus 2024-06-24 16:36:05 +02:00
parent c3fe91aabe
commit 1706d5ae8c
2 changed files with 135 additions and 96 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

205
src/drawing/drawing.rs
View File

@ -1,4 +1,4 @@
use contracts::debug_ensures;
use contracts::{debug_ensures, debug_invariant};
use enum_dispatch::enum_dispatch;
use geo::Point;
@ -77,6 +77,7 @@ pub struct Drawing<CW: Copy, R: RulesTrait> {
rules: R,
}
#[debug_invariant(self.test_if_looses_dont_infringe_each_other())]
impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
pub fn new(rules: R, layer_count: usize) -> Self {
Self {
@ -183,18 +184,6 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
Ok(dot)
}
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))]
fn add_dot_infringably<W: DotWeightTrait<PrimitiveWeight> + GetLayer>(
&mut self,
weight: W,
) -> GenericIndex<W>
where
GenericIndex<W>: Into<PrimitiveIndex> + Copy,
{
self.geometry_with_rtree.add_dot(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_err() -> 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()))]
@ -266,18 +255,6 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
Ok(seg)
}
fn add_seg_infringably<W: SegWeightTrait<PrimitiveWeight> + GetLayer>(
&mut self,
from: DotIndex,
to: DotIndex,
weight: W,
) -> GenericIndex<W>
where
GenericIndex<W>: Into<PrimitiveIndex>,
{
self.geometry_with_rtree.add_seg(from, to, 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.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 3)
|| self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count() + 4))]
@ -658,55 +635,6 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
Cane::from_dot(dot, self)
}
#[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.geometry_with_rtree.graph().edge_count() == old(self.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))]
fn fail_and_remove_if_infringes_except(
&mut self,
node: PrimitiveIndex,
maybe_except: Option<&[PrimitiveIndex]>,
) -> Result<(), Infringement> {
if let Some(infringement) = self.detect_infringement_except(node, maybe_except) {
if let Ok(dot) = node.try_into() {
self.geometry_with_rtree.remove_dot(dot);
} else if let Ok(seg) = node.try_into() {
self.geometry_with_rtree.remove_seg(seg);
} else if let Ok(bend) = node.try_into() {
self.geometry_with_rtree.remove_bend(bend);
}
return Err(infringement);
}
Ok(())
}
pub fn primitive_nodes(&self) -> impl Iterator<Item = PrimitiveIndex> + '_ {
self.geometry_with_rtree
.rtree()
.iter()
.filter_map(|wrapper| {
if let GenericNode::Primitive(primitive_node) = wrapper.data {
Some(primitive_node)
} else {
None
}
})
}
pub fn layer_primitive_nodes(&self, layer: usize) -> impl Iterator<Item = PrimitiveIndex> + '_ {
self.geometry_with_rtree
.rtree()
.locate_in_envelope_intersecting(&AABB::from_corners(
[-f64::INFINITY, -f64::INFINITY, layer as f64],
[f64::INFINITY, f64::INFINITY, layer as f64],
))
.filter_map(|wrapper| {
if let GenericNode::Primitive(primitive_node) = wrapper.data {
Some(primitive_node)
} else {
None
}
})
}
#[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 move_dot(&mut self, dot: DotIndex, to: Point) -> Result<(), Infringement> {
@ -768,6 +696,75 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
Ok(())
}
fn detect_collision(&self, node: PrimitiveIndex) -> Option<Collision> {
let shape = node.primitive(self).shape();
self.geometry_with_rtree
.rtree()
.locate_in_envelope_intersecting(&shape.full_height_envelope_3d(0.0, 2))
.filter_map(|wrapper| {
if let GenericNode::Primitive(primitive_node) = wrapper.data {
Some(primitive_node)
} else {
None
}
})
.filter(|primitive_node| !self.are_connectable(node, *primitive_node))
.filter(|primitive_node| shape.intersects(&primitive_node.primitive(self).shape()))
.map(|primitive_node| primitive_node)
.next()
.and_then(|collidee| Some(Collision(shape, collidee)))
}
}
impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))]
#[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))]
fn add_dot_infringably<W: DotWeightTrait<PrimitiveWeight> + GetLayer>(
&mut self,
weight: W,
) -> GenericIndex<W>
where
GenericIndex<W>: Into<PrimitiveIndex> + Copy,
{
self.geometry_with_rtree.add_dot(weight)
}
#[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.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))]
fn add_seg_infringably<W: SegWeightTrait<PrimitiveWeight> + GetLayer>(
&mut self,
from: DotIndex,
to: DotIndex,
weight: W,
) -> GenericIndex<W>
where
GenericIndex<W>: Into<PrimitiveIndex>,
{
self.geometry_with_rtree.add_seg(from, to, weight)
}
#[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.geometry_with_rtree.graph().edge_count() == old(self.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))]
fn fail_and_remove_if_infringes_except(
&mut self,
node: PrimitiveIndex,
maybe_except: Option<&[PrimitiveIndex]>,
) -> Result<(), Infringement> {
if let Some(infringement) = self.detect_infringement_except(node, maybe_except) {
if let Ok(dot) = node.try_into() {
self.geometry_with_rtree.remove_dot(dot);
} else if let Ok(seg) = node.try_into() {
self.geometry_with_rtree.remove_seg(seg);
} else if let Ok(bend) = node.try_into() {
self.geometry_with_rtree.remove_bend(bend);
}
return Err(infringement);
}
Ok(())
}
fn detect_infringement_except(
&self,
node: PrimitiveIndex,
@ -832,12 +829,26 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
})
}
fn detect_collision(&self, node: PrimitiveIndex) -> Option<Collision> {
let shape = node.primitive(self).shape();
pub fn primitive_nodes(&self) -> impl Iterator<Item = PrimitiveIndex> + '_ {
self.geometry_with_rtree
.rtree()
.locate_in_envelope_intersecting(&shape.full_height_envelope_3d(0.0, 2))
.iter()
.filter_map(|wrapper| {
if let GenericNode::Primitive(primitive_node) = wrapper.data {
Some(primitive_node)
} else {
None
}
})
}
pub fn layer_primitive_nodes(&self, layer: usize) -> impl Iterator<Item = PrimitiveIndex> + '_ {
self.geometry_with_rtree
.rtree()
.locate_in_envelope_intersecting(&AABB::from_corners(
[-f64::INFINITY, -f64::INFINITY, layer as f64],
[f64::INFINITY, f64::INFINITY, layer as f64],
))
.filter_map(|wrapper| {
if let GenericNode::Primitive(primitive_node) = wrapper.data {
Some(primitive_node)
@ -845,11 +856,6 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
None
}
})
.filter(|primitive_node| !self.are_connectable(node, *primitive_node))
.filter(|primitive_node| shape.intersects(&primitive_node.primitive(self).shape()))
.map(|primitive_node| primitive_node)
.next()
.and_then(|collidee| Some(Collision(shape, collidee)))
}
fn are_connectable(&self, node1: PrimitiveIndex, node2: PrimitiveIndex) -> bool {
@ -920,6 +926,39 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
pub fn node_count(&self) -> usize {
self.geometry_with_rtree.graph().node_count()
}
fn test_if_looses_dont_infringe_each_other(&self) -> bool {
!self
.primitive_nodes()
.filter(|node| match node {
PrimitiveIndex::LooseDot(..)
| PrimitiveIndex::LoneLooseSeg(..)
| PrimitiveIndex::SeqLooseSeg(..)
| PrimitiveIndex::LooseBend(..) => true,
_ => false,
})
.any(|node| {
self.find_infringement(
node,
self.locate_possible_infringers(node)
.filter_map(|n| {
if let GenericNode::Primitive(primitive_node) = n {
Some(primitive_node)
} else {
None
}
})
.filter(|primitive_node| match primitive_node {
PrimitiveIndex::LooseDot(..)
| PrimitiveIndex::LoneLooseSeg(..)
| PrimitiveIndex::SeqLooseSeg(..)
| PrimitiveIndex::LooseBend(..) => true,
_ => false,
}),
)
.is_some()
})
}
}
impl<CW: Copy, R: RulesTrait> CompoundManagerTrait<CW, GenericIndex<CW>> for Drawing<CW, R> {

26
src/layout/layout.rs
View File

@ -46,14 +46,6 @@ impl<R: RulesTrait> Layout<R> {
Self { drawing }
}
pub fn remove_band(&mut self, band: BandFirstSegIndex) {
self.drawing.remove_band(band);
}
pub fn remove_cane(&mut self, cane: &Cane, face: LooseDotIndex) {
self.drawing.remove_cane(cane, face)
}
pub fn insert_cane(
&mut self,
from: DotIndex,
@ -67,6 +59,10 @@ impl<R: RulesTrait> Layout<R> {
.insert_cane(from, around, dot_weight, seg_weight, bend_weight, cw)
}
pub fn remove_cane(&mut self, cane: &Cane, face: LooseDotIndex) {
self.drawing.remove_cane(cane, face)
}
#[debug_ensures(ret.is_ok() -> self.drawing.node_count() == old(self.drawing.node_count()) + weight.to_layer - weight.from_layer)]
#[debug_ensures(ret.is_err() -> self.drawing.node_count() == old(self.drawing.node_count()))]
pub fn add_via(&mut self, weight: ViaWeight) -> Result<GenericIndex<ViaWeight>, Infringement> {
@ -208,11 +204,8 @@ impl<R: RulesTrait> Layout<R> {
)
}
pub fn zones<W: 'static>(
&self,
node: GenericIndex<W>,
) -> impl Iterator<Item = GenericIndex<CompoundWeight>> + '_ {
self.drawing.compounds(node)
pub fn remove_band(&mut self, band: BandFirstSegIndex) {
self.drawing.remove_band(band);
}
pub fn band_length(&self, band: BandFirstSegIndex) -> f64 {
@ -247,6 +240,13 @@ impl<R: RulesTrait> Layout<R> {
}
}
pub fn zones<W: 'static>(
&self,
node: GenericIndex<W>,
) -> impl Iterator<Item = GenericIndex<CompoundWeight>> + '_ {
self.drawing.compounds(node)
}
pub fn zone_nodes(&self) -> impl Iterator<Item = GenericIndex<ZoneWeight>> + '_ {
self.drawing.rtree().iter().filter_map(|wrapper| {
if let NodeIndex::Compound(compound) = wrapper.data {