Make constraints optional in CTerm initializer (#493)

Fixes #295

---------

Co-authored-by: devops <[email protected]>

Author: tothtamas28

package/version

@@ -1 +1 @@
-0.1.330
+0.1.331

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.330"
+version = "0.1.331"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/cterm.py

@@ -34,7 +34,7 @@ class CTerm:
     config: KInner  # TODO Optional?
     constraints: tuple[KInner, ...]
 
-    def __init__(self, config: KInner, constraints: Iterable[KInner]) -> None:
+    def __init__(self, config: KInner, constraints: Iterable[KInner] = ()) -> None:
         self._check_config(config)
         constraints = self._normalize_constraints(constraints)
         object.__setattr__(self, 'config', config)

src/tests/integration/kcfg/test_cell_map.py

@@ -85,7 +85,6 @@ def _parse(kt: KToken) -> KInner:
                 KApply('<accounts>', _accounts),
                 KVariable('GENERATED_COUNTER_CELL'),
             ),
-            (),
         )
 
     @pytest.mark.parametrize(

src/tests/integration/kcfg/test_imp.py

@@ -533,7 +533,6 @@ def config(kprint: KPrint, k: str, state: str, constraint: KInner | None = None)
                 ),
                 KVariable('GENERATED_COUNTER_CELL'),
             ),
-            (),
         )
         if constraint is not None:
             _config = _config.add_constraint(constraint)

src/tests/integration/kprove/test_prove_cterm.py

@@ -52,9 +52,7 @@ def test_prove_cterm(
         expected_next_states: Iterable[tuple[str, str]],
     ) -> None:
         def config(k: str, state: str) -> CTerm:
-            return CTerm(
-                KApply('<T>', (KApply('<k>', (KToken(k, 'K'),)), KApply('<state>', (KToken(state, 'Map'),)))), ()
-            )
+            return CTerm(KApply('<T>', (KApply('<k>', (KToken(k, 'K'),)), KApply('<state>', (KToken(state, 'Map'),)))))
 
         # Given
         state = '.Map'

src/tests/unit/test_cterm.py

@@ -35,7 +35,7 @@
 
 
 def _as_cterm(term: KInner) -> CTerm:
-    return CTerm(KApply(KLabel('<generatedTop>', GENERATED_TOP_CELL), term), ())
+    return CTerm(KApply(KLabel('<generatedTop>', GENERATED_TOP_CELL), term))
 
 
 MATCH_TEST_DATA: Final[tuple[tuple[KInner, KInner], ...]] = (

src/tests/unit/test_kcfg.py

@@ -243,8 +243,8 @@ def test_cover_then_remove() -> None:
     cfg = KCFG()
 
     # When
-    node1 = cfg.create_node(CTerm(KApply('<top>', token(1)), ()))
-    node2 = cfg.create_node(CTerm(KApply('<top>', KVariable('X')), ()))
+    node1 = cfg.create_node(CTerm(KApply('<top>', token(1))))
+    node2 = cfg.create_node(CTerm(KApply('<top>', KVariable('X'))))
     cover = cfg.create_cover(node1.id, node2.id)
 
     # Then