Repository: pysmt/pysmt
Pull request #797 (2025-04-08 09:19:54)

Added Abs shortcut as shorthand for Ite(x > 0, x, -x)
I added `Abs` as a shortcut for Ite(x > 0, x, -x). 

I haven't yet added support for parsing the `abs` SMT-LIB function and simplifying it into Ite(x > 0, x, -x). Let me know if you think this would be a useful addition.

- [ x ] For bugs or new features, make sure there is a test showing the bug or demonstrating the use of the new feature
- [ x ] Are all tests green?
- [ x ] (First contribution only) You accepted the licensing terms by adding name and email to the CONTRIBUTORS file (see https://github.com/pysmt/pysmt/blob/master/docs/development.rst#licensing).



Patch:
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index b41d2f4..596b719 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -1,3 +1,4 @@
+Agustin Martinez Sune <agustin.martinez.sune@cs.ox.ac.uk>
 Ahmed Irfan <ahmed.irfan@alumni.unitn.it>
 Alastair Reid <alastair.d.reid@gmail.com>
 Alberto Griggio <griggio@fbk.eu>
diff --git a/pysmt/shortcuts.py b/pysmt/shortcuts.py
index 942b8da..a1b908c 100644
--- a/pysmt/shortcuts.py
+++ b/pysmt/shortcuts.py
@@ -233,6 +233,31 @@ def Ite(iff, left, right):
     return get_env().formula_manager.Ite(iff, left, right)
 
 
+def Abs(formula):
+    r"""Returns the absolute value of the formula.
+    
+    This is implemented as If(formula > 0, formula, -formula).
+    Works for both integer and real values.
+    
+    :param formula: The formula to compute the absolute value of
+    :returns: The absolute value of the formula
+    :raises: ValueError if the formula type is not integer or real
+    """
+    # Get the type of the formula to determine the appropriate zero value
+    formula_type = get_type(formula)
+    
+    # Create a zero value of the same type as the formula
+    if formula_type == types.INT:
+        zero = Int(0)
+    elif formula_type == types.REAL:
+        zero = Real(0)
+    else:
+        # Raise an error for unsupported types
+        raise ValueError(f"Abs function only supports integer and real types, got {formula_type}")
+    
+    return Ite(GT(formula, zero), formula, Minus(zero, formula))
+
+
 def Symbol(name, typename=types.BOOL):
     """Returns a symbol with the given name and type.
 


Test patch:
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index 25cb4db..f246ec2 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -19,7 +19,7 @@ import pysmt
 
 from pysmt.typing import BOOL, REAL, INT, FunctionType, BV8, BVType
 from pysmt.shortcuts import Symbol, is_sat, Not, Implies, GT, Plus, Int, Real
-from pysmt.shortcuts import Minus, Times, Xor, And, Or, TRUE, Iff, FALSE, Ite
+from pysmt.shortcuts import Minus, Times, Xor, And, Or, TRUE, Iff, FALSE, Ite, Abs
 from pysmt.shortcuts import Equals
 from pysmt.shortcuts import get_env
 from pysmt.environment import Environment
@@ -317,6 +317,38 @@ class TestFormulaManager(TestCase):
         inv = self.mgr.Real(Fraction(1) / self.rconst.constant_value())
         self.assertEqual(n, self.mgr.Times(self.s, inv))
 
+    def test_abs_shortcut(self):
+        # Test with integer
+        abs_int = Abs(self.p)
+        
+        # Verify the structure of the Abs node
+        self.assertTrue(abs_int.is_ite())
+        self.assertTrue(abs_int.arg(0).is_lt())  # GT is converted to LT with inverted args
+        self.assertEqual(abs_int.arg(0).arg(0), Int(0))  # First arg is 0
+        self.assertEqual(abs_int.arg(0).arg(1), self.p)  # Second arg is p
+        self.assertEqual(abs_int.arg(1), self.p)
+        self.assertTrue(abs_int.arg(2).is_minus())
+        self.assertEqual(abs_int.arg(2).arg(0), Int(0))
+        self.assertEqual(abs_int.arg(2).arg(1), self.p)
+        
+        # Test with real
+        abs_real = Abs(self.r)
+        
+        # Verify the structure of the Abs node
+        self.assertTrue(abs_real.is_ite())
+        self.assertTrue(abs_real.arg(0).is_lt())  # GT is converted to LT with inverted args
+        self.assertEqual(abs_real.arg(0).arg(0), Real(0))  # First arg is 0
+        self.assertEqual(abs_real.arg(0).arg(1), self.r)  # Second arg is r
+        self.assertEqual(abs_real.arg(1), self.r)
+        self.assertTrue(abs_real.arg(2).is_minus())
+        self.assertEqual(abs_real.arg(2).arg(0), Real(0))
+        self.assertEqual(abs_real.arg(2).arg(1), self.r)
+        
+        # Test with boolean (should raise ValueError)
+        bool_var = Symbol("z", BOOL)
+        with self.assertRaises(ValueError):
+            Abs(bool_var)
+
     def test_equals(self):
         n = self.mgr.Equals(self.real_expr, self.real_expr)
         self.assertIsNotNone(n)