From c67e049b68cb53f48349f24004cd0370a2b953f5 Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@runtimeverification.com>
Date: Wed, 15 Nov 2017 15:26:23 -0600
Subject: [PATCH] add power-modulo operator to UIUC K

---
 .../backend/java/builtins/BuiltinIntOperations.java           | 4 ++++
 .../org/kframework/backend/java/symbolic/hooks.properties     | 1 +
 k-distribution/include/builtin/domains.k                      | 1 +
 3 files changed, 6 insertions(+)

diff --git a/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinIntOperations.java b/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinIntOperations.java
index 56d66b38eb..1a0f5a45c6 100644
--- a/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinIntOperations.java
+++ b/java-backend/src/main/java/org/kframework/backend/java/builtins/BuiltinIntOperations.java
@@ -59,6 +59,10 @@ public static IntToken pow(IntToken term1, IntToken term2, TermContext context)
         return IntToken.of(term1.bigIntegerValue().pow(term2.bigIntegerValue().intValue()));
     }
 
+    public static IntToken powmod(IntToken term1, IntToken term2, IntToken term3, TermContext context) {
+        return IntToken.of(term1.bigIntegerValue().modPow(term2.bigIntegerValue(), term3.bigIntegerValue()));
+    }
+
     public static IntToken shl(IntToken term1, IntToken term2, TermContext context) {
         return IntToken.of(term1.bigIntegerValue().shiftLeft(term2.bigIntegerValue().intValue()));
     }
diff --git a/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties b/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties
index 7282011c8c..1cbd526b64 100644
--- a/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties
+++ b/java-backend/src/main/resources/org/kframework/backend/java/symbolic/hooks.properties
@@ -29,6 +29,7 @@ INT.tmod : org.kframework.backend.java.builtins.BuiltinIntOperations.rem
 INT.ediv : org.kframework.backend.java.builtins.BuiltinIntOperations.ediv
 INT.emod : org.kframework.backend.java.builtins.BuiltinIntOperations.mod
 INT.pow : org.kframework.backend.java.builtins.BuiltinIntOperations.pow
+INT.powmod : org.kframework.backend.java.builtins.BuiltinIntOperations.powmod
 INT.shl : org.kframework.backend.java.builtins.BuiltinIntOperations.shl
 INT.shr : org.kframework.backend.java.builtins.BuiltinIntOperations.shr
 INT.not : org.kframework.backend.java.builtins.BuiltinIntOperations.not
diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k
index 315ebb473d..895247109c 100644
--- a/k-distribution/include/builtin/domains.k
+++ b/k-distribution/include/builtin/domains.k
@@ -295,6 +295,7 @@ module INT
   syntax Int ::= "~Int" Int                     [function, latex(\mathop{\sim_{\scriptstyle\it Int}}{#1}), hook(INT.not)]
                > left:
                  Int "^Int" Int                 [function, left, latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)]
+               | Int "^%Int" Int Int            [function, left, hook(INT.powmod)]
                > left:
                  Int "*Int" Int                 [function, left, smtlib(*), latex({#1}\mathrel{\ast_{\scriptstyle\it Int}}{#2}), hook(INT.mul)]
                /* FIXME: translate /Int and %Int into smtlib */