Fix abs() on symbolic boolean

pschanely · Jul 23, 2024 · 7394bcd · 7394bcd
1 parent 4ad30d3
commit 7394bcd
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/crosshair/libimpl/builtinslib.py b/crosshair/libimpl/builtinslib.py
@@ -1058,6 +1058,10 @@ def __ch_realize__(self) -> object:
         with NoTracing():
             return context_statespace().choose_possible(self.var)
 
+    def __abs__(self):
+        with NoTracing():
+            return SymbolicInt(z3.If(self.var, 1, 0))
+
     def __neg__(self):
         with NoTracing():
             return SymbolicInt(z3.If(self.var, -1, 0))

diff --git a/crosshair/libimpl/builtinslib_ch_test.py b/crosshair/libimpl/builtinslib_ch_test.py
@@ -30,7 +30,7 @@
 )
 
 
-def check_abs(x: float) -> ResultComparison:
+def check_abs(x: Union[int, bool, float]) -> ResultComparison:
     """post: _"""
     return compare_results(abs, x)
 

diff --git a/doc/source/changelog.rst b/doc/source/changelog.rst
@@ -6,7 +6,8 @@ Changelog
 Next Version
 ------------
 
-  * Nothing yet!
+  * Fix spurious error calling ``abs()`` on a symbolic boolean.
+    (fixes `#283 <https://github.com/pschanely/CrossHair/issues/283>`__)
 
 
 Version 0.0.64