add power-modulo operator to UIUC K

kframework · Nov 16, 2017 · c67e049 · c67e049
1 parent 20fe909
commit c67e049
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 0 deletions.
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
@@ -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
@@ -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
@@ -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 */