Skip to content

Commit

Permalink
kint.py: add docstrings
Browse files Browse the repository at this point in the history
  • Loading branch information
@anvacaru
anvacaru committed Jun 25, 2024
1 parent 28e126f commit d4cbfe9
Show file tree
Hide file tree
Showing 2 changed files with 232 additions and 9 deletions.
235 changes: 229 additions & 6 deletions pyk/src/pyk/prelude/kint.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,100 +13,323 @@


def intToken(i: int) -> KToken: # noqa: N802
r"""Instantiate the KAST term ```#token`(i, "Int")``.
Args:
i: The left operand.
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(i1: KInner) -> KApply: # noqa: N802
return KApply('~Int_', i1)
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 operand.
i2: The exponent operand.
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 operand.
i2: The divisior operand.
i3: The modulo divisor operand.
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 operand.
i2: The divisor operand.
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 operand.
i2: The divisor operand.
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 operand.
i2: The divisor operand.
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 operand.
i2: The divisor operand.
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
return KApply('minInt(_,_)_INT-COMMON_Int_Int_Int', i1, i2)
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
return KApply('maxInt(_,_)_INT-COMMON_Int_Int_Int', i1, i2)
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.
def absInt(i1: KInner) -> KApply: # noqa: N802
return KApply('absInt(_)_INT-COMMON_Int_Int', i1)
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 d4cbfe9

Please sign in to comment.