From 989ac33ced6210419795c50387a4c42a8e33b40f Mon Sep 17 00:00:00 2001
From: Minijackson <minijackson@riseup.net>
Date: Wed, 4 Jan 2023 09:36:55 +0100
Subject: core/solving: add float_abs method

---
 core/src/solving.rs | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

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;
-- 
cgit v1.2.3