Skip to content

Commit

Permalink
Add missing operators to prelude.kint (#4477)
Browse files Browse the repository at this point in the history 
Adding new functions to the `KInt` module for Integer operations
described in
[domains.md](https://github.com/runtimeverification/k/blob/master/pyk/src/tests/profiling/test-data/domains.md?plain=1#L1173)
for:
 - integer arithmetic
 - integer min and max
 - integer absolute value

Adding docstrings to KInt module.
Adding labels for `minInt`, `maxInt`, and `absInt`.

---------

Co-authored-by: Tamás Tóth <[email protected]>
  • Loading branch information
@anvacaru @tothtamas28
anvacaru and tothtamas28 authored Jun 25, 2024
1 parent 531652d commit 94a069d
Show file tree
Hide file tree
Showing 2 changed files with 302 additions and 3 deletions.
299 changes: 299 additions & 0 deletions pyk/src/pyk/prelude/kint.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
6 changes: 3 additions & 3 deletions pyk/src/tests/profiling/test-data/domains.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 94a069d

Please sign in to comment.