Merge pull request #213 from marcoeilers/int_pow

Basic ** operator support for integers
marcoeilers · Nov 29, 2024 · ba8d524 · ba8d524
2 parents 63e6f5f + 5818baf
commit ba8d524
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 0 deletions.
diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
@@ -221,6 +221,24 @@ function int___mul__(self: Int, other: Int): Int
     self * other
 }
 
+function int___pow__(self: Int, other: Int): Int
+    decreases _
+    requires @error("** is currently only supported for non-negative exponents.")(other >= 0)
+{
+    ___pow(self, other)
+}
+
+domain ____pow_helper {
+  function ___pow(Int, Int): Int
+  axiom {
+    forall i1: Int :: { ___pow(i1, 0) } ___pow(i1, 0) == 1
+  }
+
+  axiom {
+    forall i1: Int, i2: Int :: { ___pow(i1, i2) } i2 > 0 ==> ___pow(i1, i2) == i1 * ___pow(i1, i2 - 1)
+  }
+}
+
 function int___floordiv__(self: Int, other: Int): Int
     decreases _
     requires @error("Divisor may be zero.")(other != 0)

diff --git a/src/nagini_translation/resources/builtins.json b/src/nagini_translation/resources/builtins.json
@@ -241,6 +241,10 @@
             "args": ["__prim__int", "__prim__int"],
             "type": "__prim__int"
         },
+        "__pow__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__int"
+        },
         "__truediv__": {
             "args": ["__prim__int", "__prim__int"],
             "type": "float"

diff --git a/src/nagini_translation/translators/expression.py b/src/nagini_translation/translators/expression.py
@@ -994,6 +994,8 @@ def translate_operator(self, left: Expr, right: Expr, left_type: PythonType,
 
         if left_type == right_type or isinstance(right_type, TypeVar):
             call_stmt, call = self.get_func_or_method_call(left_type, LEFT_OPERATOR_FUNCTIONS[type(node.op)], [left, right], [left_type, right_type], node, ctx)
+            if call is None:
+                raise UnsupportedException(node, "Unsupported binary operator")
             return stmt + call_stmt, call
 
         else:

diff --git a/tests/functional/verification/test_builtin_functions.py b/tests/functional/verification/test_builtin_functions.py
@@ -11,6 +11,15 @@ def test_abs(x: int) -> None:
     #:: ExpectedOutput(assert.failed:assertion.false)
     assert abs(x) > 0
 
+def test_pow(x: int) -> None:
+    a = -2
+    b = a ** 0
+    assert b == 1
+    c = x ** 4
+    assert c == x * x * x * x
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    assert 3 ** 2 == 8
+
 def test_max() -> None:
     assert max(1,max(-3, 6)) == 6
     c = max(2, -5) + max(-3, -2)