core/solving: add float_abs method

1 files changed, 19 insertions, 0 deletions

diff --git a/core/src/solving.rs b/core/src/solving.rs
index 016d188..da053e7 100644
--- a/core/src/solving.rs
+++ b/core/src/solving.rs
@@ -116,6 +116,25 @@ pub trait SolverContext {
         result
     }
 
+    fn float_abs(&mut self, value: Float) -> Float {
+        let result = self.new_free_float();
+
+        let is_negative = self.float_lt(value, Float::Fixed(0.));
+        let is_positive = self.bool_not(is_negative);
+
+        let inverse = self.float_neg(value);
+        let diff_sign = self.float_eq(result, inverse);
+        let same_sign = self.float_eq(result, value);
+
+        let change_sign = self.bool_implies(is_negative, diff_sign);
+        let keep_sign = self.bool_implies(is_positive, same_sign);
+
+        self.constrain(change_sign);
+        self.constrain(keep_sign);
+
+        result
+    }
+
     // Bools
 
     fn new_free_bool(&mut self) -> Bool;