summaryrefslogtreecommitdiffstats
path: root/core/src/solving.rs
diff options
context:
space:
mode:
Diffstat (limited to 'core/src/solving.rs')
-rw-r--r--core/src/solving.rs19
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 {
116 result 116 result
117 } 117 }
118 118
119 fn float_abs(&mut self, value: Float) -> Float {
120 let result = self.new_free_float();
121
122 let is_negative = self.float_lt(value, Float::Fixed(0.));
123 let is_positive = self.bool_not(is_negative);
124
125 let inverse = self.float_neg(value);
126 let diff_sign = self.float_eq(result, inverse);
127 let same_sign = self.float_eq(result, value);
128
129 let change_sign = self.bool_implies(is_negative, diff_sign);
130 let keep_sign = self.bool_implies(is_positive, same_sign);
131
132 self.constrain(change_sign);
133 self.constrain(keep_sign);
134
135 result
136 }
137
119 // Bools 138 // Bools
120 139
121 fn new_free_bool(&mut self) -> Bool; 140 fn new_free_bool(&mut self) -> Bool;