Skip to content

Commit 24b2151

Browse files
committed
feat: extend cvlr-fixed with div and ceil
also fix nondet(). Previous version generated nondet whole ints, rather than arbitrary fraction.
1 parent 3f847f3 commit 24b2151

File tree

1 file changed

+29
-1
lines changed

1 file changed

+29
-1
lines changed

cvlr-fixed/src/native_fixed.rs

Lines changed: 29 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,11 @@ macro_rules! native_fixed {
5555
Self::from_val(self.val + v.val)
5656
}
5757

58+
pub fn checked_div(&self, v: Self) -> Self {
59+
cvlr_assume!(v.val > 0u64.into());
60+
Self::from_val(self.val * Self::BASE / v.val)
61+
}
62+
5863
pub fn saturating_sub(&self, v: Self) -> Self {
5964
let val = if self.val <= v.val {
6065
0u64.into()
@@ -93,11 +98,26 @@ macro_rules! native_fixed {
9398
pub fn floor(&self) -> Self {
9499
self.to_floor().into()
95100
}
101+
102+
pub fn to_ceil(&self) -> NativeInt {
103+
let floor = self.to_floor();
104+
let rem = *self - Self::new(floor);
105+
106+
if rem.val > 0u64.into() {
107+
floor + 1
108+
} else {
109+
floor
110+
}
111+
}
112+
113+
pub fn ceil(&self) -> Self {
114+
self.to_ceil().into()
115+
}
96116
}
97117

98118
impl<const F: u32> cvlr_nondet::Nondet for $NativeFixed<F> {
99119
fn nondet() -> Self {
100-
Self::new(nondet())
120+
Self::from_val(nondet())
101121
}
102122
}
103123

@@ -147,6 +167,14 @@ macro_rules! native_fixed {
147167
}
148168
}
149169

170+
impl<const F: u32> core::ops::Div<$NativeFixed<F>> for $NativeFixed<F> {
171+
type Output = Self;
172+
173+
fn div(self, v: Self) -> Self::Output {
174+
self.checked_div(v)
175+
}
176+
}
177+
150178
impl<const F: u32, T: Into<NativeInt>> core::ops::Div<T> for $NativeFixed<F> {
151179
type Output = Self;
152180

0 commit comments

Comments
 (0)