Add missing operators to prelude.kint

pyk/src/pyk/prelude/kint.py

@@ -13,24 +13,323 @@
 
 
 def intToken(i: int) -> KToken:  # noqa: N802
+    r"""Instantiate the KAST term ``#token(i, "Int")``.
+
+    Args:
+        i: The integer literal.
+
+    Returns:
+        The KAST term ``#token(i, "Int")``.
+    """
     return KToken(str(i), INT)
 
 
 def ltInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_<Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_<Int_`(i1, i2)``.
+    """
     return KApply('_<Int_', i1, i2)
 
 
 def leInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_<=Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_<=Int_`(i1, i2)``.
+    """
     return KApply('_<=Int_', i1, i2)
 
 
 def gtInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_>Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_>Int_`(i1, i2)``.
+    """
     return KApply('_>Int_', i1, i2)
 
 
 def geInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_>=Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_>=Int_`(i1, i2)``.
+    """
     return KApply('_>=Int_', i1, i2)
 
 
 def eqInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_==Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_==Int_`(i1, i2)``.
+    """
     return KApply('_==Int_', i1, i2)
+
+
+def neqInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_=/=Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_=/=Int_`(i1, i2)``.
+    """
+    return KApply('_=/=Int_', i1, i2)
+
+
+def notInt(i: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```~Int_`(i)``.
+
+    Args:
+        i: The integer operand.
+
+    Returns:
+        The KAST term ```Int_`(i)``.
+    """
+    return KApply('~Int_', i)
+
+
+def expInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_^Int_`(i1, i2)``.
+
+    Args:
+        i1: The base.
+        i2: The exponent.
+
+    Returns:
+        The KAST term ```_^Int_`(i1, i2)``.
+    """
+    return KApply('_^Int_', i1, i2)
+
+
+def expModInt(i1: KInner, i2: KInner, i3: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_^%Int__`(i1, i2, i3)``.
+
+    Args:
+        i1: The dividend.
+        i2: The divisior.
+        i3: The modulus.
+
+    Returns:
+        The KAST term ```_^%Int__`(i1, i2, i3)``.
+    """
+    return KApply('_^%Int__', i1, i2, i3)
+
+
+def mulInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_*Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_*Int_`(i1, i2)``.
+    """
+    return KApply('_*Int_', i1, i2)
+
+
+def divInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_/Int_`(i1, i2)``.
+
+    Args:
+        i1: The dividend.
+        i2: The divisor.
+
+    Returns:
+        The KAST term ```_/Int_`(i1, i2)``.
+    """
+    return KApply('_/Int_', i1, i2)
+
+
+def modInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_%Int_`(i1, i2)``.
+
+    Args:
+        i1: The dividend.
+        i2: The divisor.
+
+    Returns:
+        The KAST term ```_%Int_`(i1, i2)``.
+    """
+    return KApply('_%Int_', i1, i2)
+
+
+def euclidDivInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_divInt_`(i1, i2)``.
+
+    Args:
+        i1: The dividend.
+        i2: The divisor.
+
+    Returns:
+        The KAST term ```_divInt_`(i1, i2)``.
+    """
+    return KApply('_divInt_', i1, i2)
+
+
+def euclidModInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_modInt_`(i1, i2)``.
+
+    Args:
+        i1: The dividend.
+        i2: The divisor.
+
+    Returns:
+        The KAST term ```_modInt_`(i1, i2)``.
+    """
+    return KApply('_modInt_', i1, i2)
+
+
+def addInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_+Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_+Int_`(i1, i2)``.
+    """
+    return KApply('_+Int_', i1, i2)
+
+
+def subInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_-Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_-Int_`(i1, i2)``.
+    """
+    return KApply('_-Int_', i1, i2)
+
+
+def rshiftInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_>>Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_>>Int_`(i1, i2)``.
+    """
+    return KApply('_>>Int_', i1, i2)
+
+
+def lshiftInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_<<Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_<<Int_`(i1, i2)``.
+    """
+    return KApply('_<<Int_', i1, i2)
+
+
+def andInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_&Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_&Int_`(i1, i2)``.
+    """
+    return KApply('_&Int_', i1, i2)
+
+
+def xorInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_xorInt_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_xorInt_`(i1, i2)``.
+    """
+    return KApply('_xorInt_', i1, i2)
+
+
+def orInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_|Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_|Int_`(i1, i2)``.
+    """
+    return KApply('_|Int_', i1, i2)
+
+
+def minInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```minInt`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```minInt`(i1, i2)``.
+    """
+    return KApply('minInt', i1, i2)
+
+
+def maxInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```maxInt`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```maxInt`(i1, i2)``.
+    """
+    return KApply('maxInt', i1, i2)
+
+
+def absInt(i: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```absInt`(i)``.
+
+    Args:
+        i: The integer operand.
+
+    Returns:
+        The KAST term ```absInt`(i)``.
+    """
+    return KApply('absInt', i)

pyk/src/tests/profiling/test-data/domains.md

@@ -1257,16 +1257,16 @@ You can:
 You can compute the minimum and maximum `minInt` and `maxInt` of two integers.
 
 ```k
-  syntax Int ::= "minInt" "(" Int "," Int ")"   [function, total, smt-hook((ite (< #1 #2) #1 #2)), hook(INT.min)]
-               | "maxInt" "(" Int "," Int ")"   [function, total, smt-hook((ite (< #1 #2) #2 #1)), hook(INT.max)]
+  syntax Int ::= "minInt" "(" Int "," Int ")"   [function, total, symbol(minInt), smt-hook((ite (< #1 #2) #1 #2)), hook(INT.min)]
+               | "maxInt" "(" Int "," Int ")"   [function, total, symbol(maxInt), smt-hook((ite (< #1 #2) #2 #1)), hook(INT.max)]
 ```
 
 ### Absolute value
 
 You can compute the absolute value `absInt` of an integer.
 
 ```k
-  syntax Int ::= absInt ( Int )                 [function, total, smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)]
+  syntax Int ::= absInt ( Int )                 [function, total, symbol(absInt), smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)]
 ```
 
 ### Log base 2