search

runtimeverification / pyk

Python tools for the K Framework
BSD 3-Clause "New" or "Revised" License
13 stars 2 forks source link

Generate associativity axioms #971

Closed tothtamas28 closed 7 months ago

tothtamas28 commented 7 months ago

Negative testing:

diff --git a/src/pyk/konvert/_module_to_kore.py b/src/pyk/konvert/_module_to_kore.py
index 386829af..112ad960 100644
--- a/src/pyk/konvert/_module_to_kore.py
+++ b/src/pyk/konvert/_module_to_kore.py
@@ -286,7 +286,7 @@ def _assoc_axioms(defn: KDefinition) -> list[Axiom]:
         symbol = _label_name(production.klabel.name)
         sort_params = tuple(SortVar(param.name) for param in production.klabel.params)
         sort = sort_to_kore(production.sort)
-        R = SortVar('R')  # noqa: N806
+        R = SortVar('S')  # noqa: N806
         K1, K2, K3 = (EVar(name, sort) for name in ['K1', 'K2', 'K3'])  # noqa: N806

         def app(left: Pattern, right: Pattern) -> App:
$ make test-integration TEST_ARGS='-n0 -k test_module_to_kore'
...
E               Failed: Invalid sentence: axiom{S} \equals{SortMap{}, S}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(K1 : SortMap{}, K2 : SortMap{}), K3 : SortMap{}), Lbl'Unds'Map'Unds'{}(K1 : SortMap{}, Lbl'Unds'Map'Unds'{}(K2 : SortMap{}, K3 : SortMap{}))) [assoc{}()]