From 0cfb7e1bbe53fb5a017f33303f25825926365539 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Wed, 4 Sep 2024 15:46:34 +0800 Subject: [PATCH] [to delete] move untils into utils.py as #4621 --- pyk/src/tests/unit/test_kcfg.py | 19 +------------------ pyk/src/tests/unit/utils.py | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 18 deletions(-) diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 25faae06f4b..9ba68366a07 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -10,8 +10,7 @@ from pyk.kcfg import KCFG, KCFGShow from pyk.kcfg.kcfg import KCFGNodeAttr from pyk.kcfg.show import NodePrinter -from pyk.prelude.kint import geInt, intToken, ltInt -from pyk.prelude.ml import mlEquals, mlEqualsTrue, mlTop +from pyk.prelude.ml import mlEquals, mlTop from pyk.prelude.utils import token from pyk.utils import not_none, single @@ -25,22 +24,6 @@ from pyk.kast import KInner -def lt(var: str, n: int) -> KApply: - return mlEqualsTrue(ltInt(KVariable(var), intToken(n))) - - -def ge(var: str, n: int) -> KApply: - return mlEqualsTrue(geInt(KVariable(var), intToken(n))) - - -def config(var: str) -> KApply: - return KApply('', KVariable(var)) - - -def config_int(n: int) -> KApply: - return KApply('', intToken(n)) - - def to_csubst_cterm(term_1: CTerm, term_2: CTerm, constraints: Iterable[KInner]) -> CSubst: csubst = term_1.match_with_constraint(term_2) assert csubst is not None diff --git a/pyk/src/tests/unit/utils.py b/pyk/src/tests/unit/utils.py index 73ed9ff8776..bdac4c8d626 100644 --- a/pyk/src/tests/unit/utils.py +++ b/pyk/src/tests/unit/utils.py @@ -4,6 +4,8 @@ from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KLabel, KVariable +from pyk.prelude.kint import geInt, intToken, ltInt +from pyk.prelude.ml import mlEqualsTrue if TYPE_CHECKING: from typing import Final @@ -16,3 +18,19 @@ f, g, h = map(KLabel, ('f', 'g', 'h')) k = KLabel('') + + +def lt(var: str, n: int) -> KApply: + return mlEqualsTrue(ltInt(KVariable(var), intToken(n))) + + +def ge(var: str, n: int) -> KApply: + return mlEqualsTrue(geInt(KVariable(var), intToken(n))) + + +def config(var: str) -> KApply: + return KApply('', KVariable(var)) + + +def config_int(n: int) -> KApply: + return KApply('', intToken(n))