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

route: Add contracts for path length

This commit is contained in:
Mikolaj Wielgus 2023-09-15 22:48:51 +02:00
parent c94a4c716a
commit 7d2cff9004
1 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/route.rs
View File

@ -1,3 +1,5 @@
use contracts::debug_ensures;
use crate::{ use crate::{
draw::{Draw, Head}, draw::{Draw, Head},
layout::Layout, layout::Layout,
@ -41,6 +43,7 @@ impl<'a> Route<'a> {
self.draw().finish(trace.head, into_dot, width) self.draw().finish(trace.head, into_dot, width)
} }
#[debug_ensures(ret.is_ok() -> trace.path.len() == path.len())]
pub fn rework_path( pub fn rework_path(
&mut self, &mut self,
trace: &mut Trace, trace: &mut Trace,
@ -59,6 +62,7 @@ impl<'a> Route<'a> {
self.path(trace, &path[prefix_length..], width) self.path(trace, &path[prefix_length..], width)
} }
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() + path.len()))]
pub fn path(&mut self, trace: &mut Trace, path: &[VertexIndex], width: f64) -> Result<(), ()> { pub fn path(&mut self, trace: &mut Trace, path: &[VertexIndex], width: f64) -> Result<(), ()> {
for (i, vertex) in path.iter().enumerate() { for (i, vertex) in path.iter().enumerate() {
if let Err(err) = self.step(trace, *vertex, width) { if let Err(err) = self.step(trace, *vertex, width) {
@ -69,6 +73,7 @@ impl<'a> Route<'a> {
Ok(()) Ok(())
} }
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() - step_count))]
pub fn undo_path(&mut self, trace: &mut Trace, step_count: usize) -> Result<(), ()> { pub fn undo_path(&mut self, trace: &mut Trace, step_count: usize) -> Result<(), ()> {
for _ in 0..step_count { for _ in 0..step_count {
self.undo_step(trace)?; self.undo_step(trace)?;
@ -76,6 +81,8 @@ impl<'a> Route<'a> {
Ok(()) Ok(())
} }
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() + 1))]
#[debug_ensures(ret.is_err() -> trace.path.len() == old(trace.path.len()))]
pub fn step(&mut self, trace: &mut Trace, to: VertexIndex, width: f64) -> Result<(), ()> { pub fn step(&mut self, trace: &mut Trace, to: VertexIndex, width: f64) -> Result<(), ()> {
let to_dot = self.mesh.dot(to); let to_dot = self.mesh.dot(to);
trace.head = self.draw().segbend_around_dot(trace.head, to_dot, width)?; trace.head = self.draw().segbend_around_dot(trace.head, to_dot, width)?;
@ -83,6 +90,8 @@ impl<'a> Route<'a> {
Ok(()) Ok(())
} }
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() - 1))]
#[debug_ensures(ret.is_err() -> trace.path.len() == old(trace.path.len()))]
pub fn undo_step(&mut self, trace: &mut Trace) -> Result<(), ()> { pub fn undo_step(&mut self, trace: &mut Trace) -> Result<(), ()> {
trace.head = self.draw().undo_segbend(trace.head).unwrap(); trace.head = self.draw().undo_segbend(trace.head).unwrap();
trace.path.pop(); trace.path.pop();