Add a bigIntDiv hook

Pi-Squared-Inc · Aug 28, 2024 · bbf95c3 · bbf95c3
1 parent 186218a
commit bbf95c3
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 0 deletions.
diff --git a/mx-semantics/main/biguint/hooks.md b/mx-semantics/main/biguint/hooks.md
@@ -3,6 +3,7 @@
 module MX-BIGUINT-HOOKS
     imports BOOL
     imports COMMON-K-CELL
+    imports K-EQUAL-SYNTAX
     imports MX-BIGUINT-CONFIGURATION
     imports MX-COMMON-SYNTAX
 
@@ -58,6 +59,23 @@ module MX-BIGUINT-HOOKS
         <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
         requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
             andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntDiv(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        /Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+            andBool Ints[Id2] orDefault 0 =/=K 0
 endmodule
 
 ```
diff --git a/tests/mx/biguint/div.mx b/tests/mx/biguint/div.mx
@@ -0,0 +1,7 @@
+push mxIntValue(40);
+call 1 MX#bigIntNew;
+push mxIntValue(500);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntDiv;
+get_big_int;
+check_eq mxIntValue(12)