From f6b18d41a401a4e076f1a589248af26816442bbe Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 23 Oct 2024 10:28:37 -0300 Subject: [PATCH] Adding support for MInt{128} (#1160) This PR extends our Machine Integers support to also support 128 bits for k hashing and for equality function `==K`. This is necessary for one of our light semantics in Pi2. --- runtime/collections/hash.cpp | 6 + runtime/collections/kelemle.cpp | 10 + test/defn/hash-mint.kore | 670 +++++++++++++++++++------------- test/defn/k-files/hash-mint.k | 9 +- test/input/hash-mint.in | 2 +- test/output/hash-mint.out.diff | 2 +- 6 files changed, 432 insertions(+), 267 deletions(-) diff --git a/runtime/collections/hash.cpp b/runtime/collections/hash.cpp index 453fcd113..8f1e99f7f 100644 --- a/runtime/collections/hash.cpp +++ b/runtime/collections/hash.cpp @@ -134,6 +134,12 @@ void k_hash(block *arg, void *h) { add_hash64(h, *intptr); break; } + case MINT_LAYOUT + 128: { + auto *intptr = (uint64_t *)(argintptr + offset); + add_hash64(h, intptr[0]); + add_hash64(h, intptr[1]); + break; + } case MINT_LAYOUT + 160: { auto *intptr = (uint64_t *)(argintptr + offset); add_hash64(h, intptr[0]); diff --git a/runtime/collections/kelemle.cpp b/runtime/collections/kelemle.cpp index 6656d24a8..06d12d569 100644 --- a/runtime/collections/kelemle.cpp +++ b/runtime/collections/kelemle.cpp @@ -143,6 +143,16 @@ bool hook_KEQUAL_eq(block *arg1, block *arg2) { } break; } + case MINT_LAYOUT + 128: { + auto *child1ptr = (int64_t *)(child1intptr); + auto *child2ptr = (int64_t *)(child2intptr); + bool cmp + = child1ptr[0] == child2ptr[0] && child1ptr[1] == child2ptr[1]; + if (!cmp) { + return false; + } + break; + } case MINT_LAYOUT + 160: { auto *child1ptr = (int64_t *)(child1intptr); auto *child2ptr = (int64_t *)(child2intptr); diff --git a/test/defn/hash-mint.kore b/test/defn/hash-mint.kore index 6df49afc9..7f90754de 100644 --- a/test/defn/hash-mint.kore +++ b/test/defn/hash-mint.kore @@ -1,8 +1,7 @@ // RUN: %interpreter -// RUN: %run | diff - %test-diff-out -// RUN: %run-binary | diff - %test-diff-out +// RUN: %run | grep -oP "(?=Lbl'-LT-'k'-GT-'{}).*(dotk{}\(\)\)\)\)\))" | diff - %test-diff-out // RUN: %run-binary-out | diff - <(echo -n) -[topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] +[topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] module BASIC-K sort SortK{} [] @@ -66,132 +65,135 @@ module K endmodule [] -module TEST +module HASH-MINT // imports import K [] // sorts + sort Sort128{} [nat{}("128")] sort SortKCellOpt{} [] sort SortKCell{} [] sort Sort256{} [nat{}("256")] - sort SortKConfigVar{} [hasDomainValues{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(40,3,40,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/kast.md)"), token{}()] - hooked-sort SortSet{} [concat{}(Lbl'Unds'Set'Unds'{}()), element{}(LblSetItem{}()), hook{}("SET.Set"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(700,3,700,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Set{}())] - hooked-sort SortBool{} [hasDomainValues{}(), hook{}("BOOL.Bool"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1077,3,1077,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + sort SortKConfigVar{} [hasDomainValues{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(40,3,40,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/kast.md)"), token{}()] + hooked-sort SortSet{} [concat{}(Lbl'Unds'Set'Unds'{}()), element{}(LblSetItem{}()), hook{}("SET.Set"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(700,3,700,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Set{}())] + hooked-sort SortBool{} [hasDomainValues{}(), hook{}("BOOL.Bool"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1077,3,1077,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] hooked-sort SortMInt{SortS0} [hasDomainValues{}(), hook{}("MINT.MInt")] sort SortGeneratedTopCellFragment{} [] - hooked-sort SortList{} [concat{}(Lbl'Unds'List'Unds'{}()), element{}(LblListItem{}()), hook{}("LIST.List"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(913,3,913,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'List{}())] + hooked-sort SortList{} [concat{}(Lbl'Unds'List'Unds'{}()), element{}(LblListItem{}()), hook{}("LIST.List"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(913,3,913,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'List{}()), update{}(LblList'Coln'set{}())] sort SortGeneratedTopCell{} [] sort SortStateCell{} [] sort SortGeneratedCounterCell{} [] - hooked-sort SortMap{} [concat{}(Lbl'Unds'Map'Unds'{}()), element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), hook{}("MAP.Map"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(218,3,218,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Map{}())] + hooked-sort SortMap{} [concat{}(Lbl'Unds'Map'Unds'{}()), element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), hook{}("MAP.Map"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(218,3,218,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Map{}())] sort Sort160{} [nat{}("160")] - hooked-sort SortInt{} [hasDomainValues{}(), hook{}("INT.Int"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1198,3,1198,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-sort SortInt{} [hasDomainValues{}(), hook{}("INT.Int"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1198,3,1198,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] sort SortStateCellOpt{} [] // symbols - hooked-symbol Lbl--MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.neg"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2953,34,2953,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvuminus"), total{}()] - hooked-symbol Lbl'Stop'List{}() : SortList{} [function{}(), functional{}(), hook{}("LIST.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(937,19,937,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_nil"), symbol'Kywd'{}(".List"), total{}()] - hooked-symbol Lbl'Stop'Map{}() : SortMap{} [function{}(), functional{}(), hook{}("MAP.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(248,18,248,96)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(".Map"), total{}()] - hooked-symbol Lbl'Stop'Set{}() : SortSet{} [function{}(), functional{}(), hook{}("SET.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(729,18,729,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(".Set"), total{}()] + hooked-symbol Lbl--MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.neg"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2957,34,2957,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvuminus"), total{}()] + hooked-symbol Lbl'Stop'List{}() : SortList{} [function{}(), functional{}(), hook{}("LIST.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(937,19,937,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_nil"), symbol'Kywd'{}(".List"), total{}()] + hooked-symbol Lbl'Stop'Map{}() : SortMap{} [function{}(), functional{}(), hook{}("MAP.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(248,18,248,96)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(".Map"), total{}()] + hooked-symbol Lbl'Stop'Set{}() : SortSet{} [function{}(), functional{}(), hook{}("SET.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(729,18,729,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(".Set"), total{}()] symbol Lbl'-LT-'generatedCounter'-GT-'{}(SortInt{}) : SortGeneratedCounterCell{} [cell{}(), constructor{}(), functional{}(), injective{}()] - symbol Lbl'-LT-'generatedTop'-GT-'{}(SortKCell{}, SortStateCell{}, SortGeneratedCounterCell{}) : SortGeneratedTopCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(7,17,8,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + symbol Lbl'-LT-'generatedTop'-GT-'{}(SortKCell{}, SortStateCell{}, SortGeneratedCounterCell{}) : SortGeneratedTopCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,17,9,81)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] symbol Lbl'-LT-'generatedTop'-GT-'-fragment{}(SortKCellOpt{}, SortStateCellOpt{}) : SortGeneratedTopCellFragment{} [constructor{}(), functional{}(), injective{}()] - symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(7,17,7,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] - symbol Lbl'-LT-'state'-GT-'{}(SortMap{}) : SortStateCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,17,8,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] - hooked-symbol LblInt2MInt'LParUndsRParUnds'MINT'Unds'MInt'Unds'Int{SortWidth}(SortInt{}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.integer"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2888,34,2888,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("int2bv"), total{}()] - hooked-symbol LblList'Coln'get{}(SortList{}, SortInt{}) : SortKItem{} [function{}(), hook{}("LIST.get"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(965,20,965,91)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:get")] - hooked-symbol LblList'Coln'range{}(SortList{}, SortInt{}, SortInt{}) : SortList{} [function{}(), hook{}("LIST.range"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1012,19,1012,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:range")] - hooked-symbol LblList'Coln'set{}(SortList{}, SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(974,19,974,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:set")] - hooked-symbol LblListItem{}(SortKItem{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.element"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(945,19,945,124)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_elem"), symbol'Kywd'{}("ListItem"), total{}()] - hooked-symbol LblMInt2Signed'LParUndsRParUnds'MINT'Unds'Int'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortInt{} [function{}(), functional{}(), hook{}("MINT.svalue"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2885,26,2885,91)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol LblMInt2Unsigned'LParUndsRParUnds'MINT'Unds'Int'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortInt{} [function{}(), functional{}(), hook{}("MINT.uvalue"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2886,26,2886,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bv2int"), total{}()] - hooked-symbol LblMap'Coln'choice{}(SortMap{}) : SortKItem{} [function{}(), hook{}("MAP.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(393,20,393,101)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:choice")] - hooked-symbol LblMap'Coln'lookup{}(SortMap{}, SortKItem{}) : SortKItem{} [function{}(), hook{}("MAP.lookup"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(271,20,271,105)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:lookup")] - hooked-symbol LblMap'Coln'lookupOrDefault{}(SortMap{}, SortKItem{}, SortKItem{}) : SortKItem{} [function{}(), functional{}(), hook{}("MAP.lookupOrDefault"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(281,20,281,134)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:lookupOrDefault"), total{}()] - hooked-symbol LblMap'Coln'update{}(SortMap{}, SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(290,18,290,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:update"), total{}()] - hooked-symbol LblSet'Coln'choice{}(SortSet{}) : SortKItem{} [function{}(), hook{}("SET.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(804,20,804,95)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:choice")] - hooked-symbol LblSet'Coln'difference{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(769,18,769,106)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:difference"), total{}()] - hooked-symbol LblSet'Coln'in{}(SortKItem{}, SortSet{}) : SortBool{} [function{}(), functional{}(), hook{}("SET.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(777,19,777,94)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:in"), total{}()] - hooked-symbol LblSetItem{}(SortKItem{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.element"), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(737,18,737,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("SetItem"), total{}()] - hooked-symbol Lbl'UndsPerc'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tmod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1246,18,1246,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("mod"), symbol'Kywd'{}("_%Int_")] - hooked-symbol Lbl'UndsPerc'sMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.srem"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2957,34,2957,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsrem")] - hooked-symbol Lbl'UndsPerc'uMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.urem"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2959,34,2959,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvurem")] - hooked-symbol Lbl'UndsAnd-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1257,18,1257,125)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("andInt"), symbol'Kywd'{}("_&Int_"), total{}()] - hooked-symbol Lbl'UndsAnd-'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2968,34,2968,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvand"), total{}()] - hooked-symbol Lbl'UndsStar'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.mul"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1242,18,1242,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("*"), symbol'Kywd'{}("_*Int_"), total{}()] - hooked-symbol Lbl'UndsStar'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.mul"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2955,34,2955,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvmul"), total{}()] - hooked-symbol Lbl'UndsPlus'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.add"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1251,18,1251,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("+"), symbol'Kywd'{}("_+Int_"), total{}()] - hooked-symbol Lbl'UndsPlus'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.add"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2961,34,2961,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvadd"), total{}()] - hooked-symbol Lbl'Unds'-Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.sub"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1252,18,1252,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("-"), symbol'Kywd'{}("_-Int_"), total{}()] - hooked-symbol Lbl'Unds'-MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.sub"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2962,34,2962,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsub"), total{}()] - hooked-symbol Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(311,18,311,88)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol Lbl'UndsSlsh'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tdiv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1245,18,1245,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("div"), symbol'Kywd'{}("_/Int_")] - hooked-symbol Lbl'UndsSlsh'sMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.sdiv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2956,34,2956,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsdiv")] - hooked-symbol Lbl'UndsSlsh'uMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.udiv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2958,34,2958,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvudiv")] - hooked-symbol Lbl'Unds-LT--LT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shl"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1255,18,1255,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("shlInt"), symbol'Kywd'{}("_<="), symbol'Kywd'{}("_>=Int_"), total{}()] - hooked-symbol Lbl'Unds-GT-Eqls'sMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.sge"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2989,27,2989,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsge"), total{}()] - hooked-symbol Lbl'Unds-GT-Eqls'uMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.uge"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2990,27,2990,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvuge"), total{}()] - hooked-symbol Lbl'Unds-GT--GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shr"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1254,18,1254,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("shrInt"), symbol'Kywd'{}("_>>Int_")] - hooked-symbol Lbl'Unds-GT--GT-'aMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.ashr"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2965,34,2965,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvashr")] - hooked-symbol Lbl'Unds-GT--GT-'lMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.lshr"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2966,34,2966,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvlshr")] - hooked-symbol Lbl'Unds-GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), functional{}(), hook{}("INT.gt"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1316,19,1316,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}(">"), symbol'Kywd'{}("_>Int_"), total{}()] - hooked-symbol Lbl'Unds-GT-'sMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.sgt"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2987,27,2987,110)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsgt"), total{}()] - hooked-symbol Lbl'Unds-GT-'uMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.ugt"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2988,27,2988,110)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvugt"), total{}()] - hooked-symbol Lbl'Unds'List'Unds'{}(SortList{}, SortList{}) : SortList{} [element{}(LblListItem{}()), function{}(), functional{}(), hook{}("LIST.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(929,19,929,180)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_concat"), symbol'Kywd'{}("_List_"), total{}(), unit{}(Lbl'Stop'List{}())] - hooked-symbol Lbl'Unds'Map'Unds'{}(SortMap{}, SortMap{}) : SortMap{} [element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), function{}(), hook{}("MAP.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(240,18,240,165)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_Map_"), unit{}(Lbl'Stop'Map{}())] - hooked-symbol Lbl'Unds'Set'Unds'{}(SortSet{}, SortSet{}) : SortSet{} [element{}(LblSetItem{}()), function{}(), hook{}("SET.concat"), idem{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(721,18,721,157)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_Set_"), unit{}(Lbl'Stop'Set{}())] - hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(SortMap{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.remove"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(299,18,299,109)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_[_<-undef]"), total{}()] - hooked-symbol Lbl'UndsXor-Perc'Int'UndsUnds'{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.powmod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1240,18,1240,131)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(mod (^ #1 #2) #3)"), symbol'Kywd'{}("_^%Int__")] - hooked-symbol Lbl'UndsXor-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.pow"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1239,18,1239,109)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("^"), symbol'Kywd'{}("_^Int_")] - hooked-symbol Lbl'Unds'andBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1110,19,1110,138)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}("_andBool_"), total{}()] - hooked-symbol Lbl'Unds'andThenBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.andThen"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1111,19,1111,146)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}("_andThenBool_"), total{}()] - hooked-symbol Lbl'Unds'divInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.ediv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1248,18,1248,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("div"), symbol'Kywd'{}("_divInt_")] - symbol Lbl'Unds'dividesInt'UndsUnds'INT-COMMON'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1327,19,1327,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol Lbl'Unds'impliesBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.implies"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1115,19,1115,145)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("=>"), symbol'Kywd'{}("_impliesBool_"), total{}()] - hooked-symbol Lbl'Unds'inList'Unds'{}(SortKItem{}, SortList{}) : SortBool{} [function{}(), functional{}(), hook{}("LIST.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1021,19,1021,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_inList_"), total{}()] - hooked-symbol Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(SortKItem{}, SortMap{}) : SortBool{} [function{}(), functional{}(), hook{}("MAP.in_keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(357,19,357,89)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol Lbl'Unds'modInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.emod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1249,18,1249,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("mod"), symbol'Kywd'{}("_modInt_")] - hooked-symbol Lbl'Unds'orBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.or"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1113,19,1113,135)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}("_orBool_"), total{}()] - hooked-symbol Lbl'Unds'orElseBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.orElse"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1114,19,1114,143)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}("_orElseBool_"), total{}()] - hooked-symbol Lbl'Unds'xorBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1112,19,1112,138)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("xor"), symbol'Kywd'{}("_xorBool_"), total{}()] - hooked-symbol Lbl'Unds'xorInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1259,18,1259,127)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("xorInt"), symbol'Kywd'{}("_xorInt_"), total{}()] - hooked-symbol Lbl'Unds'xorMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2970,34,2970,118)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvxor"), total{}()] - hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.element"), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(257,18,257,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_|->_"), total{}()] - hooked-symbol Lbl'UndsPipe'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.or"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1261,18,1261,123)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("orInt"), symbol'Kywd'{}("_|Int_"), total{}()] - hooked-symbol Lbl'UndsPipe'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.or"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2972,34,2972,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvor"), total{}()] - hooked-symbol Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.union"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(748,18,748,92)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.abs"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1278,18,1278,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 0) (- 0 #1) #1)"), total{}()] - symbol Lblbar'LParRParUnds'TEST'Unds'KItem{}() : SortKItem{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(10,28,10,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] - hooked-symbol LblbitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.bitRange"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1303,18,1303,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblbitwidthMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortInt{} [function{}(), functional{}(), hook{}("MINT.bitwidth"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2868,26,2868,92)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol LblfillList'LParUndsCommUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.fill"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1002,19,1002,100)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - symbol Lblfoo'LParRParUnds'TEST'Unds'KItem{}() : SortKItem{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(10,20,10,25)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] - symbol LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [freshGenerator{}(), function{}(), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1441,18,1441,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,17,8,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] + symbol Lbl'-LT-'state'-GT-'{}(SortMap{}) : SortStateCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(9,17,9,81)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] + hooked-symbol LblInt2MInt'LParUndsRParUnds'MINT'Unds'MInt'Unds'Int{SortWidth}(SortInt{}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.integer"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2892,34,2892,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("int2bv"), total{}()] + hooked-symbol LblList'Coln'get{}(SortList{}, SortInt{}) : SortKItem{} [function{}(), hook{}("LIST.get"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(965,20,965,91)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:get")] + hooked-symbol LblList'Coln'range{}(SortList{}, SortInt{}, SortInt{}) : SortList{} [function{}(), hook{}("LIST.range"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1012,19,1012,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:range")] + hooked-symbol LblList'Coln'set{}(SortList{}, SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(974,19,974,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:set")] + hooked-symbol LblListItem{}(SortKItem{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.element"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(945,19,945,124)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_elem"), symbol'Kywd'{}("ListItem"), total{}()] + hooked-symbol LblMInt2Signed'LParUndsRParUnds'MINT'Unds'Int'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortInt{} [function{}(), functional{}(), hook{}("MINT.svalue"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2889,26,2889,91)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblMInt2Unsigned'LParUndsRParUnds'MINT'Unds'Int'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortInt{} [function{}(), functional{}(), hook{}("MINT.uvalue"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2890,26,2890,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bv2int"), total{}()] + hooked-symbol LblMap'Coln'choice{}(SortMap{}) : SortKItem{} [function{}(), hook{}("MAP.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(393,20,393,101)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:choice")] + hooked-symbol LblMap'Coln'lookup{}(SortMap{}, SortKItem{}) : SortKItem{} [function{}(), hook{}("MAP.lookup"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(271,20,271,105)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:lookup")] + hooked-symbol LblMap'Coln'lookupOrDefault{}(SortMap{}, SortKItem{}, SortKItem{}) : SortKItem{} [function{}(), functional{}(), hook{}("MAP.lookupOrDefault"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(281,20,281,134)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:lookupOrDefault"), total{}()] + hooked-symbol LblMap'Coln'update{}(SortMap{}, SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(290,18,290,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:update"), total{}()] + hooked-symbol LblSet'Coln'choice{}(SortSet{}) : SortKItem{} [function{}(), hook{}("SET.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(804,20,804,95)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:choice")] + hooked-symbol LblSet'Coln'difference{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(769,18,769,106)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:difference"), total{}()] + hooked-symbol LblSet'Coln'in{}(SortKItem{}, SortSet{}) : SortBool{} [function{}(), functional{}(), hook{}("SET.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(777,19,777,94)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:in"), total{}()] + hooked-symbol LblSetItem{}(SortKItem{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.element"), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(737,18,737,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("SetItem"), total{}()] + hooked-symbol Lbl'UndsPerc'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tmod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1248,18,1250,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))"), symbol'Kywd'{}("_%Int_")] + hooked-symbol Lbl'UndsPerc'sMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.srem"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2961,34,2961,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsrem")] + hooked-symbol Lbl'UndsPerc'uMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.urem"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2963,34,2963,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvurem")] + hooked-symbol Lbl'UndsAnd-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1261,18,1261,125)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("andInt"), symbol'Kywd'{}("_&Int_"), total{}()] + hooked-symbol Lbl'UndsAnd-'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2972,34,2972,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvand"), total{}()] + hooked-symbol Lbl'UndsStar'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.mul"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1242,18,1242,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("*"), symbol'Kywd'{}("_*Int_"), total{}()] + hooked-symbol Lbl'UndsStar'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.mul"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2959,34,2959,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvmul"), total{}()] + hooked-symbol Lbl'UndsPlus'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.add"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1255,18,1255,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("+"), symbol'Kywd'{}("_+Int_"), total{}()] + hooked-symbol Lbl'UndsPlus'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.add"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2965,34,2965,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvadd"), total{}()] + hooked-symbol Lbl'Unds'-Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.sub"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1256,18,1256,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("-"), symbol'Kywd'{}("_-Int_"), total{}()] + hooked-symbol Lbl'Unds'-MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.sub"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2966,34,2966,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsub"), total{}()] + hooked-symbol Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(311,18,311,88)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'UndsSlsh'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tdiv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1245,18,1247,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))"), symbol'Kywd'{}("_/Int_")] + hooked-symbol Lbl'UndsSlsh'sMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.sdiv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2960,34,2960,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsdiv")] + hooked-symbol Lbl'UndsSlsh'uMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.udiv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2962,34,2962,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvudiv")] + hooked-symbol Lbl'Unds-LT--LT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shl"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1259,18,1259,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("shlInt"), symbol'Kywd'{}("_<="), symbol'Kywd'{}("_>=Int_"), total{}()] + hooked-symbol Lbl'Unds-GT-Eqls'sMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.sge"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2993,27,2993,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsge"), total{}()] + hooked-symbol Lbl'Unds-GT-Eqls'uMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.uge"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2994,27,2994,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvuge"), total{}()] + hooked-symbol Lbl'Unds-GT--GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shr"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1258,18,1258,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("shrInt"), symbol'Kywd'{}("_>>Int_")] + hooked-symbol Lbl'Unds-GT--GT-'aMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.ashr"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2969,34,2969,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvashr")] + hooked-symbol Lbl'Unds-GT--GT-'lMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), hook{}("MINT.lshr"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2970,34,2970,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvlshr")] + hooked-symbol Lbl'Unds-GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), functional{}(), hook{}("INT.gt"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1320,19,1320,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}(">"), symbol'Kywd'{}("_>Int_"), total{}()] + hooked-symbol Lbl'Unds-GT-'sMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.sgt"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2991,27,2991,110)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvsgt"), total{}()] + hooked-symbol Lbl'Unds-GT-'uMInt'UndsUnds'MINT'Unds'Bool'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortBool{} [function{}(), functional{}(), hook{}("MINT.ugt"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2992,27,2992,110)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvugt"), total{}()] + hooked-symbol Lbl'Unds'List'Unds'{}(SortList{}, SortList{}) : SortList{} [element{}(LblListItem{}()), function{}(), functional{}(), hook{}("LIST.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(929,19,929,198)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_concat"), symbol'Kywd'{}("_List_"), total{}(), unit{}(Lbl'Stop'List{}()), update{}(LblList'Coln'set{}())] + hooked-symbol Lbl'Unds'Map'Unds'{}(SortMap{}, SortMap{}) : SortMap{} [element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), function{}(), hook{}("MAP.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(240,18,240,165)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_Map_"), unit{}(Lbl'Stop'Map{}())] + hooked-symbol Lbl'Unds'Set'Unds'{}(SortSet{}, SortSet{}) : SortSet{} [element{}(LblSetItem{}()), function{}(), hook{}("SET.concat"), idem{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(721,18,721,157)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_Set_"), unit{}(Lbl'Stop'Set{}())] + hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(SortMap{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.remove"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(299,18,299,109)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_[_<-undef]"), total{}()] + hooked-symbol Lbl'UndsXor-Perc'Int'UndsUnds'{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.powmod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1240,18,1240,131)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(mod (^ #1 #2) #3)"), symbol'Kywd'{}("_^%Int__")] + hooked-symbol Lbl'UndsXor-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.pow"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1239,18,1239,109)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("^"), symbol'Kywd'{}("_^Int_")] + hooked-symbol Lbl'Unds'andBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1110,19,1110,138)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}("_andBool_"), total{}()] + hooked-symbol Lbl'Unds'andThenBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.andThen"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1111,19,1111,146)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}("_andThenBool_"), total{}()] + hooked-symbol Lbl'Unds'divInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.ediv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1252,18,1252,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("div"), symbol'Kywd'{}("_divInt_")] + symbol Lbl'Unds'dividesInt'UndsUnds'INT-COMMON'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1331,19,1331,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbl'Unds'impliesBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.implies"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1115,19,1115,145)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("=>"), symbol'Kywd'{}("_impliesBool_"), total{}()] + hooked-symbol Lbl'Unds'inList'Unds'{}(SortKItem{}, SortList{}) : SortBool{} [function{}(), functional{}(), hook{}("LIST.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1021,19,1021,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_inList_"), total{}()] + hooked-symbol Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(SortKItem{}, SortMap{}) : SortBool{} [function{}(), functional{}(), hook{}("MAP.in_keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(357,19,357,89)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'Unds'modInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.emod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1253,18,1253,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("mod"), symbol'Kywd'{}("_modInt_")] + hooked-symbol Lbl'Unds'orBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.or"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1113,19,1113,135)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}("_orBool_"), total{}()] + hooked-symbol Lbl'Unds'orElseBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.orElse"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1114,19,1114,143)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}("_orElseBool_"), total{}()] + hooked-symbol Lbl'Unds'xorBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1112,19,1112,138)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("xor"), symbol'Kywd'{}("_xorBool_"), total{}()] + hooked-symbol Lbl'Unds'xorInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1263,18,1263,127)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("xorInt"), symbol'Kywd'{}("_xorInt_"), total{}()] + hooked-symbol Lbl'Unds'xorMInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2974,34,2974,118)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvxor"), total{}()] + hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.element"), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(257,18,257,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_|->_"), total{}()] + hooked-symbol Lbl'UndsPipe'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.or"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1265,18,1265,123)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("orInt"), symbol'Kywd'{}("_|Int_"), total{}()] + hooked-symbol Lbl'UndsPipe'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.or"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2976,34,2976,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvor"), total{}()] + hooked-symbol Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.union"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(748,18,748,92)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.abs"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1282,18,1282,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 0) (- 0 #1) #1)"), total{}()] + symbol Lblbar'LParRParUnds'HASH-MINT'Unds'KItem{}() : SortKItem{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(11,28,11,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] + symbol Lblbaz'LParRParUnds'HASH-MINT'Unds'KItem{}() : SortKItem{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(11,36,11,41)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] + hooked-symbol LblbitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.bitRange"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1307,18,1307,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblbitwidthMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortInt{} [function{}(), functional{}(), hook{}("MINT.bitwidth"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2872,26,2872,92)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblfillList'LParUndsCommUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.fill"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1002,19,1002,100)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + symbol Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}() : SortKItem{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(11,20,11,25)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] + symbol LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [freshGenerator{}(), function{}(), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1445,18,1445,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] symbol LblgetGeneratedCounterCell{}(SortGeneratedTopCell{}) : SortGeneratedCounterCell{} [function{}()] symbol LblinitGeneratedCounterCell{}() : SortGeneratedCounterCell{} [function{}(), functional{}(), total{}()] symbol LblinitGeneratedTopCell{}(SortMap{}) : SortGeneratedTopCell{} [function{}()] symbol LblinitKCell{}(SortMap{}) : SortKCell{} [function{}()] symbol LblinitStateCell{}() : SortStateCell{} [function{}(), functional{}(), total{}()] - hooked-symbol LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.intersection"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(759,18,759,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.intersection"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(759,18,759,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + symbol Lblis128{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol Lblis160{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol Lblis256{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisBool{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] @@ -205,22 +207,23 @@ module TEST symbol LblisKConfigVar{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisKItem{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisList{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisMInt'LBra'128'RBra'{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisMInt'LBra'160'RBra'{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisMInt'LBra'256'RBra'{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisMap{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisSet{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisStateCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] symbol LblisStateCellOpt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] - hooked-symbol Lblite{SortSort}(SortBool{}, SortSort, SortSort) : SortSort [function{}(), functional{}(), hook{}("KEQUAL.ite"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2293,26,2293,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("ite"), symbol'Kywd'{}("ite"), total{}()] - hooked-symbol Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(SortMap{}) : SortSet{} [function{}(), functional{}(), hook{}("MAP.keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(341,18,341,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol Lblkeys'Unds'list'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [function{}(), hook{}("MAP.keys_list"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(349,19,349,80)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol Lbllog2Int'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), hook{}("INT.log2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1289,18,1289,75)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblmakeList'LParUndsCommUndsRParUnds'LIST'Unds'List'Unds'Int'Unds'KItem{}(SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.make"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(983,19,983,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.max"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1270,18,1270,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 #2) #2 #1)"), total{}()] - hooked-symbol LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.min"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1269,18,1269,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 #2) #1 #2)"), total{}()] + hooked-symbol Lblite{SortSort}(SortBool{}, SortSort, SortSort) : SortSort [function{}(), functional{}(), hook{}("KEQUAL.ite"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2297,26,2297,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("ite"), symbol'Kywd'{}("ite"), total{}()] + hooked-symbol Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(SortMap{}) : SortSet{} [function{}(), functional{}(), hook{}("MAP.keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(341,18,341,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lblkeys'Unds'list'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [function{}(), hook{}("MAP.keys_list"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(349,19,349,80)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbllog2Int'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), hook{}("INT.log2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1293,18,1293,75)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblmakeList'LParUndsCommUndsRParUnds'LIST'Unds'List'Unds'Int'Unds'KItem{}(SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.make"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(983,19,983,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.max"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1274,18,1274,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 #2) #2 #1)"), total{}()] + hooked-symbol LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.min"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1273,18,1273,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 #2) #1 #2)"), total{}()] symbol LblnoKCell{}() : SortKCellOpt{} [constructor{}(), functional{}(), injective{}()] symbol LblnoStateCell{}() : SortStateCellOpt{} [constructor{}(), functional{}(), injective{}()] - hooked-symbol LblnotBool'Unds'{}(SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1109,19,1109,131)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("not"), symbol'Kywd'{}("notBool_"), total{}()] + hooked-symbol LblnotBool'Unds'{}(SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1109,19,1109,131)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("not"), symbol'Kywd'{}("notBool_"), total{}()] symbol Lblproject'Coln'Bool{}(SortK{}) : SortBool{} [function{}()] symbol Lblproject'Coln'GeneratedCounterCell{}(SortK{}) : SortGeneratedCounterCell{} [function{}()] symbol Lblproject'Coln'GeneratedTopCell{}(SortK{}) : SortGeneratedTopCell{} [function{}()] @@ -231,37 +234,38 @@ module TEST symbol Lblproject'Coln'KCellOpt{}(SortK{}) : SortKCellOpt{} [function{}()] symbol Lblproject'Coln'KItem{}(SortK{}) : SortKItem{} [function{}()] symbol Lblproject'Coln'List{}(SortK{}) : SortList{} [function{}()] + symbol Lblproject'Coln'MInt'LBra'128'RBra'{}(SortK{}) : SortMInt{Sort128{}} [function{}()] symbol Lblproject'Coln'MInt'LBra'160'RBra'{}(SortK{}) : SortMInt{Sort160{}} [function{}()] symbol Lblproject'Coln'MInt'LBra'256'RBra'{}(SortK{}) : SortMInt{Sort256{}} [function{}()] symbol Lblproject'Coln'Map{}(SortK{}) : SortMap{} [function{}()] symbol Lblproject'Coln'Set{}(SortK{}) : SortSet{} [function{}()] symbol Lblproject'Coln'StateCell{}(SortK{}) : SortStateCell{} [function{}()] symbol Lblproject'Coln'StateCellOpt{}(SortK{}) : SortStateCellOpt{} [function{}()] - hooked-symbol LblpushList{}(SortKItem{}, SortList{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.push"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(953,19,953,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("pushList"), total{}()] - hooked-symbol LblrandInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), hook{}("INT.rand"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1337,18,1337,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(SortMap{}, SortSet{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.removeAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(333,18,333,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol LblroundMInt'LParUndsRParUnds'MINT'Unds'MInt'Unds'MInt{SortWidth1, SortWidth2}(SortMInt{SortWidth2}) : SortMInt{SortWidth1} [function{}(), functional{}(), hook{}("MINT.round"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3017,44,3017,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol LblsMaxMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.smax"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3002,34,3002,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvslt #1 #2) #2 #1)"), total{}()] - hooked-symbol LblsMinMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.smin"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3003,34,3003,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvslt #1 #2) #1 #2)"), total{}()] - hooked-symbol LblsignExtendBitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.signExtendBitRange"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1304,18,1304,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblsignExtendMInt'LParUndsRParUnds'MINT'Unds'MInt'Unds'MInt{SortWidth1, SortWidth2}(SortMInt{SortWidth2}) : SortMInt{SortWidth1} [function{}(), functional{}(), hook{}("MINT.sext"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3018,44,3018,107)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(SortSet{}) : SortInt{} [function{}(), functional{}(), hook{}("SET.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(794,18,794,76)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol LblsizeList{}(SortList{}) : SortInt{} [function{}(), functional{}(), hook{}("LIST.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1029,18,1029,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_len"), symbol'Kywd'{}("sizeList"), total{}()] - hooked-symbol LblsizeMap{}(SortMap{}) : SortInt{} [function{}(), functional{}(), hook{}("MAP.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(373,18,373,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("sizeMap"), total{}()] - symbol LblsmaxMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2899,18,2899,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - symbol LblsminMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2898,18,2898,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - symbol LblsoverflowMInt'LParUndsCommUndsRParUnds'MINT'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2915,19,2915,62)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblsrandInt'LParUndsRParUnds'INT-COMMON'Unds'K'Unds'Int{}(SortInt{}) : SortK{} [function{}(), hook{}("INT.srand"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1338,16,1338,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LbluMaxMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.umax"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3004,34,3004,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvult #1 #2) #2 #1)"), total{}()] - hooked-symbol LbluMinMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.umin"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3005,34,3005,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvult #1 #2) #1 #2)"), total{}()] - symbol LblumaxMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2901,18,2901,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - symbol LbluminMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2900,18,2900,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - symbol LbluoverflowMInt'LParUndsCommUndsRParUnds'MINT'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2916,19,2916,62)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblupdateList'LParUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'List{}(SortList{}, SortInt{}, SortList{}) : SortList{} [function{}(), hook{}("LIST.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(993,19,993,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(324,18,324,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] - hooked-symbol Lblvalues'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [function{}(), hook{}("MAP.values"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(365,19,365,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] - hooked-symbol Lbl'Tild'Int'Unds'{}(SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1237,18,1237,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("notInt"), symbol'Kywd'{}("~Int_"), total{}()] - hooked-symbol Lbl'Tild'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2952,34,2952,104)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvnot"), total{}()] + hooked-symbol LblpushList{}(SortKItem{}, SortList{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.push"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(953,19,953,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("pushList"), total{}()] + hooked-symbol LblrandInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), hook{}("INT.rand"), impure{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1341,18,1341,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(SortMap{}, SortSet{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.removeAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(333,18,333,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblroundMInt'LParUndsRParUnds'MINT'Unds'MInt'Unds'MInt{SortWidth1, SortWidth2}(SortMInt{SortWidth2}) : SortMInt{SortWidth1} [function{}(), functional{}(), hook{}("MINT.round"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3021,44,3021,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblsMaxMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.smax"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3006,34,3006,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvslt #1 #2) #2 #1)"), total{}()] + hooked-symbol LblsMinMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.smin"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3007,34,3007,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvslt #1 #2) #1 #2)"), total{}()] + hooked-symbol LblsignExtendBitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.signExtendBitRange"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1308,18,1308,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblsignExtendMInt'LParUndsRParUnds'MINT'Unds'MInt'Unds'MInt{SortWidth1, SortWidth2}(SortMInt{SortWidth2}) : SortMInt{SortWidth1} [function{}(), functional{}(), hook{}("MINT.sext"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3022,44,3022,107)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(SortSet{}) : SortInt{} [function{}(), functional{}(), hook{}("SET.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(794,18,794,76)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblsizeList{}(SortList{}) : SortInt{} [function{}(), functional{}(), hook{}("LIST.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1029,18,1029,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_len"), symbol'Kywd'{}("sizeList"), total{}()] + hooked-symbol LblsizeMap{}(SortMap{}) : SortInt{} [function{}(), functional{}(), hook{}("MAP.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(373,18,373,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("sizeMap"), total{}()] + symbol LblsmaxMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2903,18,2903,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + symbol LblsminMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2902,18,2902,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + symbol LblsoverflowMInt'LParUndsCommUndsRParUnds'MINT'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2919,19,2919,62)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblsrandInt'LParUndsRParUnds'INT-COMMON'Unds'K'Unds'Int{}(SortInt{}) : SortK{} [function{}(), hook{}("INT.srand"), impure{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1342,16,1342,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LbluMaxMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.umax"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3008,34,3008,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvult #1 #2) #2 #1)"), total{}()] + hooked-symbol LbluMinMInt'LParUndsCommUndsRParUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}, SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.umin"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3009,34,3009,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (bvult #1 #2) #1 #2)"), total{}()] + symbol LblumaxMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2905,18,2905,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + symbol LbluminMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2904,18,2904,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + symbol LbluoverflowMInt'LParUndsCommUndsRParUnds'MINT'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2920,19,2920,62)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblupdateList'LParUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'List{}(SortList{}, SortInt{}, SortList{}) : SortList{} [function{}(), hook{}("LIST.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(993,19,993,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(324,18,324,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lblvalues'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [function{}(), hook{}("MAP.values"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(365,19,365,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbl'Tild'Int'Unds'{}(SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1237,18,1237,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("notInt"), symbol'Kywd'{}("~Int_"), total{}()] + hooked-symbol Lbl'Tild'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt{SortWidth}(SortMInt{SortWidth}) : SortMInt{SortWidth} [function{}(), functional{}(), hook{}("MINT.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2956,34,2956,104)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("bvnot"), total{}()] // generated axioms axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKCellOpt{}, SortKItem{}} (From:SortKCellOpt{}))) [subsort{SortKCellOpt{}, SortKItem{}}()] // subsort @@ -273,6 +277,7 @@ module TEST axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortList{}, SortKItem{}} (From:SortList{}))) [subsort{SortList{}, SortKItem{}}()] // subsort axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedTopCell{}, SortKItem{}} (From:SortGeneratedTopCell{}))) [subsort{SortGeneratedTopCell{}, SortKItem{}}()] // subsort axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (From:SortGeneratedCounterCell{}))) [subsort{SortGeneratedCounterCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortMInt{Sort128{}}, SortKItem{}} (From:SortMInt{Sort128{}}))) [subsort{SortMInt{Sort128{}}, SortKItem{}}()] // subsort axiom{R} \exists{R} (Val:SortStateCellOpt{}, \equals{SortStateCellOpt{}, R} (Val:SortStateCellOpt{}, inj{SortStateCell{}, SortStateCellOpt{}} (From:SortStateCell{}))) [subsort{SortStateCell{}, SortStateCellOpt{}}()] // subsort axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortBool{}, SortKItem{}} (From:SortBool{}))) [subsort{SortBool{}, SortKItem{}}()] // subsort axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortMInt{Sort160{}}, SortKItem{}} (From:SortMInt{Sort160{}}))) [subsort{SortMInt{Sort160{}}, SortKItem{}}()] // subsort @@ -362,14 +367,18 @@ module TEST axiom{R, SortWidth} \exists{R} (Val:SortMInt{SortWidth}, \equals{SortMInt{SortWidth}, R} (Val:SortMInt{SortWidth}, Lbl'UndsPipe'MInt'UndsUnds'MINT'Unds'MInt'Unds'MInt'Unds'MInt{SortWidth}(K0:SortMInt{SortWidth}, K1:SortMInt{SortWidth}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(K0:SortInt{}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lblbar'LParRParUnds'TEST'Unds'KItem{}())) [functional{}()] // functional - axiom{}\not{SortKItem{}} (\and{SortKItem{}} (Lblbar'LParRParUnds'TEST'Unds'KItem{}(), Lblfoo'LParRParUnds'TEST'Unds'KItem{}())) [constructor{}()] // no confusion different constructors + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lblbar'LParRParUnds'HASH-MINT'Unds'KItem{}())) [functional{}()] // functional + axiom{}\not{SortKItem{}} (\and{SortKItem{}} (Lblbar'LParRParUnds'HASH-MINT'Unds'KItem{}(), Lblbaz'LParRParUnds'HASH-MINT'Unds'KItem{}())) [constructor{}()] // no confusion different constructors + axiom{}\not{SortKItem{}} (\and{SortKItem{}} (Lblbar'LParRParUnds'HASH-MINT'Unds'KItem{}(), Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}())) [constructor{}()] // no confusion different constructors + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lblbaz'LParRParUnds'HASH-MINT'Unds'KItem{}())) [functional{}()] // functional + axiom{}\not{SortKItem{}} (\and{SortKItem{}} (Lblbaz'LParRParUnds'HASH-MINT'Unds'KItem{}(), Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}())) [constructor{}()] // no confusion different constructors axiom{R, SortWidth} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblbitwidthMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'MInt{SortWidth}(K0:SortMInt{SortWidth}))) [functional{}()] // functional - axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lblfoo'LParRParUnds'TEST'Unds'KItem{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}())) [functional{}()] // functional axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(K0:SortInt{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortGeneratedCounterCell{}, \equals{SortGeneratedCounterCell{}, R} (Val:SortGeneratedCounterCell{}, LblinitGeneratedCounterCell{}())) [functional{}()] // functional axiom{R} \exists{R} (Val:SortStateCell{}, \equals{SortStateCell{}, R} (Val:SortStateCell{}, LblinitStateCell{}())) [functional{}()] // functional axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lblis128{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lblis160{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lblis256{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisBool{}(K0:SortK{}))) [functional{}()] // functional @@ -383,6 +392,7 @@ module TEST axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKConfigVar{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKItem{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisList{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisMInt'LBra'128'RBra'{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisMInt'LBra'160'RBra'{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisMInt'LBra'256'RBra'{}(K0:SortK{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisMap{}(K0:SortK{}))) [functional{}()] // functional @@ -418,32 +428,42 @@ module TEST axiom{} \or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}()) [constructor{}()] // no junk axiom{} \or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}()) [constructor{}()] // no junk axiom{} \or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \or{SortKItem{}} (Lblbar'LParRParUnds'TEST'Unds'KItem{}(), Lblfoo'LParRParUnds'TEST'Unds'KItem{}(), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortMInt{Sort160{}}, inj{SortMInt{Sort160{}}, SortKItem{}} (Val:SortMInt{Sort160{}})), \exists{SortKItem{}} (Val:SortMInt{Sort256{}}, inj{SortMInt{Sort256{}}, SortKItem{}} (Val:SortMInt{Sort256{}})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortStateCell{}, inj{SortStateCell{}, SortKItem{}} (Val:SortStateCell{})), \exists{SortKItem{}} (Val:SortStateCellOpt{}, inj{SortStateCellOpt{}, SortKItem{}} (Val:SortStateCellOpt{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk + axiom{} \or{SortKItem{}} (Lblbar'LParRParUnds'HASH-MINT'Unds'KItem{}(), Lblbaz'LParRParUnds'HASH-MINT'Unds'KItem{}(), Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}(), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortMInt{Sort128{}}, inj{SortMInt{Sort128{}}, SortKItem{}} (Val:SortMInt{Sort128{}})), \exists{SortKItem{}} (Val:SortMInt{Sort160{}}, inj{SortMInt{Sort160{}}, SortKItem{}} (Val:SortMInt{Sort160{}})), \exists{SortKItem{}} (Val:SortMInt{Sort256{}}, inj{SortMInt{Sort256{}}, SortKItem{}} (Val:SortMInt{Sort256{}})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortStateCell{}, inj{SortStateCell{}, SortKItem{}} (Val:SortStateCell{})), \exists{SortKItem{}} (Val:SortStateCellOpt{}, inj{SortStateCellOpt{}, SortKItem{}} (Val:SortStateCellOpt{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk + axiom{} \or{SortMInt{Sort128{}}} (\top{SortMInt{Sort128{}}}(), \bottom{SortMInt{Sort128{}}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) axiom{} \or{SortMInt{Sort160{}}} (\top{SortMInt{Sort160{}}}(), \bottom{SortMInt{Sort160{}}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) axiom{} \or{SortMInt{Sort256{}}} (\top{SortMInt{Sort256{}}}(), \bottom{SortMInt{Sort256{}}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) axiom{} \or{SortStateCell{}} (\exists{SortStateCell{}} (X0:SortMap{}, Lbl'-LT-'state'-GT-'{}(X0:SortMap{})), \bottom{SortStateCell{}}()) [constructor{}()] // no junk axiom{} \or{SortStateCellOpt{}} (LblnoStateCell{}(), \exists{SortStateCellOpt{}} (Val:SortStateCell{}, inj{SortStateCell{}, SortStateCellOpt{}} (Val:SortStateCell{})), \bottom{SortStateCellOpt{}}()) [constructor{}()] // no junk // rules -// rule ``(``(`bar()_TEST_KItem`(.KList)~>_DotVar1),``(State) #as _Gen3,_DotVar0)=>``(``(`Map:lookup`(State,inj{MInt,KItem}(#token("0p160","MInt{160}")))~>_DotVar1),_Gen3,_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4dcc2d1a5e3970091468ef270cb216543eae4f844d74fc1767804d6b53952890), org.kframework.attributes.Location(Location(14,8,15,30)), org.kframework.attributes.Source(Source(/home/dwightguth/test/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule ``(``(`bar()_HASH-MINT_KItem`(.KList)~>_DotVar1),``(State) #as _Gen3,_DotVar0)=>``(``(`baz()_HASH-MINT_KItem`(.KList)~>`Map:lookup`(State,inj{MInt,KItem}(#token("0p160","MInt{160}")))~>_DotVar1),_Gen3,_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e8f2128d41c445ac543ec534571d8d77898b99cb0913c6a8f3f8c555914932f0), org.kframework.attributes.Location(Location(15,8,16,30)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{} \rewrites{SortGeneratedTopCell{}} ( \and{SortGeneratedTopCell{}} ( - Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'LParRParUnds'TEST'Unds'KItem{}(),Var'Unds'DotVar1:SortK{})),\and{SortStateCell{}}(Lbl'-LT-'state'-GT-'{}(VarState:SortMap{}),Var'Unds'Gen3:SortStateCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'LParRParUnds'HASH-MINT'Unds'KItem{}(),Var'Unds'DotVar1:SortK{})),\and{SortStateCell{}}(Lbl'-LT-'state'-GT-'{}(VarState:SortMap{}),Var'Unds'Gen3:SortStateCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()), \and{SortGeneratedTopCell{}} ( - Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(LblMap'Coln'lookup{}(VarState:SortMap{},inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("0p160"))),Var'Unds'DotVar1:SortK{})),Var'Unds'Gen3:SortStateCell{},Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) - [UNIQUE'Unds'ID{}("4dcc2d1a5e3970091468ef270cb216543eae4f844d74fc1767804d6b53952890"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(14,8,15,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbaz'LParRParUnds'HASH-MINT'Unds'KItem{}(),kseq{}(LblMap'Coln'lookup{}(VarState:SortMap{},inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("0p160"))),Var'Unds'DotVar1:SortK{}))),Var'Unds'Gen3:SortStateCell{},Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("e8f2128d41c445ac543ec534571d8d77898b99cb0913c6a8f3f8c555914932f0"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(15,8,16,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] -// rule ``(``(`foo()_TEST_KItem`(.KList)~>_DotVar1),``(State) #as _Gen3,_DotVar0)=>``(``(`bar()_TEST_KItem`(.KList)~>`Map:lookup`(State,inj{MInt,KItem}(#token("0p256","MInt{256}")))~>_DotVar1),_Gen3,_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7e25f55341359a29cf521671396ee862c8a684f2bb54b113e596955a9849b723), org.kframework.attributes.Location(Location(12,8,13,30)), org.kframework.attributes.Source(Source(/home/dwightguth/test/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule ``(``(`baz()_HASH-MINT_KItem`(.KList)~>_DotVar1),``(State) #as _Gen3,_DotVar0)=>``(``(`Map:lookup`(State,inj{MInt,KItem}(#token("0p128","MInt{128}")))~>_DotVar1),_Gen3,_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ee96bef5e01540a16fcce8f178445e20fc2039752f47671739394f43f2be7f59), org.kframework.attributes.Location(Location(17,8,18,30)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{} \rewrites{SortGeneratedTopCell{}} ( \and{SortGeneratedTopCell{}} ( - Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'LParRParUnds'TEST'Unds'KItem{}(),Var'Unds'DotVar1:SortK{})),\and{SortStateCell{}}(Lbl'-LT-'state'-GT-'{}(VarState:SortMap{}),Var'Unds'Gen3:SortStateCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbaz'LParRParUnds'HASH-MINT'Unds'KItem{}(),Var'Unds'DotVar1:SortK{})),\and{SortStateCell{}}(Lbl'-LT-'state'-GT-'{}(VarState:SortMap{}),Var'Unds'Gen3:SortStateCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()), \and{SortGeneratedTopCell{}} ( - Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'LParRParUnds'TEST'Unds'KItem{}(),kseq{}(LblMap'Coln'lookup{}(VarState:SortMap{},inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("0p256"))),Var'Unds'DotVar1:SortK{}))),Var'Unds'Gen3:SortStateCell{},Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) - [UNIQUE'Unds'ID{}("7e25f55341359a29cf521671396ee862c8a684f2bb54b113e596955a9849b723"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(12,8,13,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(LblMap'Coln'lookup{}(VarState:SortMap{},inj{SortMInt{Sort128{}}, SortKItem{}}(\dv{SortMInt{Sort128{}}}("0p128"))),Var'Unds'DotVar1:SortK{})),Var'Unds'Gen3:SortStateCell{},Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("ee96bef5e01540a16fcce8f178445e20fc2039752f47671739394f43f2be7f59"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(17,8,18,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] -// rule `_=/=Bool_`(B1,B2)=>`notBool_`(`_==Bool_`(B1,B2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f), org.kframework.attributes.Location(Location(1159,8,1159,57)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule ``(``(`foo()_HASH-MINT_KItem`(.KList)~>_DotVar1),``(State) #as _Gen3,_DotVar0)=>``(``(`bar()_HASH-MINT_KItem`(.KList)~>`Map:lookup`(State,inj{MInt,KItem}(#token("0p256","MInt{256}")))~>_DotVar1),_Gen3,_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(8da016c95f3e4ee150c57031fe817f8ea95848f5c90caa763573987d51837378), org.kframework.attributes.Location(Location(13,8,14,30)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + axiom{} \rewrites{SortGeneratedTopCell{}} ( + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}(),Var'Unds'DotVar1:SortK{})),\and{SortStateCell{}}(Lbl'-LT-'state'-GT-'{}(VarState:SortMap{}),Var'Unds'Gen3:SortStateCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + \top{SortGeneratedTopCell{}}()), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblbar'LParRParUnds'HASH-MINT'Unds'KItem{}(),kseq{}(LblMap'Coln'lookup{}(VarState:SortMap{},inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("0p256"))),Var'Unds'DotVar1:SortK{}))),Var'Unds'Gen3:SortStateCell{},Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("8da016c95f3e4ee150c57031fe817f8ea95848f5c90caa763573987d51837378"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(13,8,14,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] + +// rule `_=/=Bool_`(B1,B2)=>`notBool_`(`_==Bool_`(B1,B2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f), org.kframework.attributes.Location(Location(1159,8,1159,57)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -463,9 +483,9 @@ module TEST \and{SortBool{}} ( LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Bool'Unds'{}(VarB1:SortBool{},VarB2:SortBool{})), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1159,8,1159,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1159,8,1159,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_=/=Int_`(I1,I2)=>`notBool_`(`_==Int_`(I1,I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3), org.kframework.attributes.Location(Location(1438,8,1438,53)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_=/=Int_`(I1,I2)=>`notBool_`(`_==Int_`(I1,I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3), org.kframework.attributes.Location(Location(1442,8,1442,53)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -485,9 +505,9 @@ module TEST \and{SortBool{}} ( LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Int'Unds'{}(VarI1:SortInt{},VarI2:SortInt{})), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1438,8,1438,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1442,8,1442,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_=/=K_`(K1,K2)=>`notBool_`(`_==K_`(K1,K2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c), org.kframework.attributes.Location(Location(2318,8,2318,45)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_=/=K_`(K1,K2)=>`notBool_`(`_==K_`(K1,K2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c), org.kframework.attributes.Location(Location(2322,8,2322,45)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -507,9 +527,9 @@ module TEST \and{SortBool{}} ( LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'K'Unds'{}(VarK1:SortK{},VarK2:SortK{})), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2318,8,2318,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2322,8,2322,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_andBool_`(#token("false","Bool") #as _Gen1,_Gen0)=>_Gen1 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497), org.kframework.attributes.Location(Location(1132,8,1132,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_andBool_`(#token("false","Bool") #as _Gen1,_Gen0)=>_Gen1 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497), org.kframework.attributes.Location(Location(1132,8,1132,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -529,9 +549,9 @@ module TEST \and{SortBool{}} ( Var'Unds'Gen1:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1132,8,1132,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1132,8,1132,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_andBool_`(B,#token("true","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(72139ee1f2b9362a47514de6503329ccf3c27e74e3ebfa0c0fe26321ec13f281), org.kframework.attributes.Location(Location(1131,8,1131,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_andBool_`(B,#token("true","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(72139ee1f2b9362a47514de6503329ccf3c27e74e3ebfa0c0fe26321ec13f281), org.kframework.attributes.Location(Location(1131,8,1131,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -539,9 +559,9 @@ module TEST \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("72139ee1f2b9362a47514de6503329ccf3c27e74e3ebfa0c0fe26321ec13f281"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1131,8,1131,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("72139ee1f2b9362a47514de6503329ccf3c27e74e3ebfa0c0fe26321ec13f281"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1131,8,1131,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_andBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fd61c826168aab115cd7f528702e8187ca16195bdcf29f42f33a32c83afebb12), org.kframework.attributes.Location(Location(1133,8,1133,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_andBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fd61c826168aab115cd7f528702e8187ca16195bdcf29f42f33a32c83afebb12), org.kframework.attributes.Location(Location(1133,8,1133,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -549,9 +569,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("fd61c826168aab115cd7f528702e8187ca16195bdcf29f42f33a32c83afebb12"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1133,8,1133,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("fd61c826168aab115cd7f528702e8187ca16195bdcf29f42f33a32c83afebb12"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1133,8,1133,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_andBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f), org.kframework.attributes.Location(Location(1130,8,1130,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_andBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f), org.kframework.attributes.Location(Location(1130,8,1130,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -571,9 +591,9 @@ module TEST \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1130,8,1130,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1130,8,1130,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_andThenBool_`(#token("false","Bool") #as _Gen1,_Gen0)=>_Gen1 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d), org.kframework.attributes.Location(Location(1137,8,1137,36)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_andThenBool_`(#token("false","Bool") #as _Gen1,_Gen0)=>_Gen1 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d), org.kframework.attributes.Location(Location(1137,8,1137,36)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -593,9 +613,9 @@ module TEST \and{SortBool{}} ( Var'Unds'Gen1:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1137,8,1137,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1137,8,1137,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_andThenBool_`(K,#token("true","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2cfb33affb9c668d39a4a7267156085e1dbd3584fc7925b1aa9a1672bb9eab9f), org.kframework.attributes.Location(Location(1136,8,1136,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_andThenBool_`(K,#token("true","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2cfb33affb9c668d39a4a7267156085e1dbd3584fc7925b1aa9a1672bb9eab9f), org.kframework.attributes.Location(Location(1136,8,1136,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -603,9 +623,9 @@ module TEST \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("2cfb33affb9c668d39a4a7267156085e1dbd3584fc7925b1aa9a1672bb9eab9f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1136,8,1136,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("2cfb33affb9c668d39a4a7267156085e1dbd3584fc7925b1aa9a1672bb9eab9f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1136,8,1136,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_andThenBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(198861009d03d8f5220000f16342962720be289ca0d49b12953fb2693e2fea01), org.kframework.attributes.Location(Location(1138,8,1138,36)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_andThenBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(198861009d03d8f5220000f16342962720be289ca0d49b12953fb2693e2fea01), org.kframework.attributes.Location(Location(1138,8,1138,36)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -613,9 +633,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("198861009d03d8f5220000f16342962720be289ca0d49b12953fb2693e2fea01"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1138,8,1138,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("198861009d03d8f5220000f16342962720be289ca0d49b12953fb2693e2fea01"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1138,8,1138,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_andThenBool_`(#token("true","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689), org.kframework.attributes.Location(Location(1135,8,1135,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_andThenBool_`(#token("true","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689), org.kframework.attributes.Location(Location(1135,8,1135,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -635,9 +655,9 @@ module TEST \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1135,8,1135,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1135,8,1135,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_divInt_`(I1,I2)=>`_/Int_`(`_-Int_`(I1,`_modInt_`(I1,I2)),I2) requires `_=/=Int_`(I2,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(83dcf9bc8c69f131715bc7a92d06c99b9a2b5f4c4fdafb69e6fdb2f1822712d4), org.kframework.attributes.Location(Location(1427,8,1428,23)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] +// rule `_divInt_`(I1,I2)=>`_/Int_`(`_-Int_`(I1,`_modInt_`(I1,I2)),I2) requires `_=/=Int_`(I2,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(83dcf9bc8c69f131715bc7a92d06c99b9a2b5f4c4fdafb69e6fdb2f1822712d4), org.kframework.attributes.Location(Location(1431,8,1432,23)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -659,9 +679,9 @@ module TEST \and{SortInt{}} ( Lbl'UndsSlsh'Int'Unds'{}(Lbl'Unds'-Int'Unds'{}(VarI1:SortInt{},Lbl'Unds'modInt'Unds'{}(VarI1:SortInt{},VarI2:SortInt{})),VarI2:SortInt{}), \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("83dcf9bc8c69f131715bc7a92d06c99b9a2b5f4c4fdafb69e6fdb2f1822712d4"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1427,8,1428,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("83dcf9bc8c69f131715bc7a92d06c99b9a2b5f4c4fdafb69e6fdb2f1822712d4"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1431,8,1432,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_dividesInt__INT-COMMON_Bool_Int_Int`(I1,I2)=>`_==Int_`(`_%Int_`(I2,I1),#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fd8facae0061fe5bc5c406f7ad2ed5d8d21960bf1118c9b240451253064dadb5), org.kframework.attributes.Location(Location(1439,8,1439,58)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_dividesInt__INT-COMMON_Bool_Int_Int`(I1,I2)=>`_==Int_`(`_%Int_`(I2,I1),#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fd8facae0061fe5bc5c406f7ad2ed5d8d21960bf1118c9b240451253064dadb5), org.kframework.attributes.Location(Location(1443,8,1443,58)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -681,9 +701,9 @@ module TEST \and{SortBool{}} ( Lbl'UndsEqlsEqls'Int'Unds'{}(Lbl'UndsPerc'Int'Unds'{}(VarI2:SortInt{},VarI1:SortInt{}),\dv{SortInt{}}("0")), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("fd8facae0061fe5bc5c406f7ad2ed5d8d21960bf1118c9b240451253064dadb5"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1439,8,1439,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("fd8facae0061fe5bc5c406f7ad2ed5d8d21960bf1118c9b240451253064dadb5"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1443,8,1443,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_impliesBool_`(B,#token("false","Bool"))=>`notBool_`(B) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(93b8d798abd6d9999e0e733384ad161e9a0bd2f074623a742afdc63964380aba), org.kframework.attributes.Location(Location(1157,8,1157,45)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_impliesBool_`(B,#token("false","Bool"))=>`notBool_`(B) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(93b8d798abd6d9999e0e733384ad161e9a0bd2f074623a742afdc63964380aba), org.kframework.attributes.Location(Location(1157,8,1157,45)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -691,9 +711,9 @@ module TEST \and{SortBool{}} ( LblnotBool'Unds'{}(VarB:SortBool{}), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("93b8d798abd6d9999e0e733384ad161e9a0bd2f074623a742afdc63964380aba"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1157,8,1157,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("93b8d798abd6d9999e0e733384ad161e9a0bd2f074623a742afdc63964380aba"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1157,8,1157,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_impliesBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2b4994db7b40b72dc09ac8d5d036263b215c37d45f45d764251d8b607a7592ba), org.kframework.attributes.Location(Location(1156,8,1156,39)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_impliesBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2b4994db7b40b72dc09ac8d5d036263b215c37d45f45d764251d8b607a7592ba), org.kframework.attributes.Location(Location(1156,8,1156,39)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -701,9 +721,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("2b4994db7b40b72dc09ac8d5d036263b215c37d45f45d764251d8b607a7592ba"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1156,8,1156,39)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("2b4994db7b40b72dc09ac8d5d036263b215c37d45f45d764251d8b607a7592ba"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1156,8,1156,39)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_impliesBool_`(#token("false","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e), org.kframework.attributes.Location(Location(1155,8,1155,40)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_impliesBool_`(#token("false","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e), org.kframework.attributes.Location(Location(1155,8,1155,40)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -723,9 +743,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1155,8,1155,40)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1155,8,1155,40)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_impliesBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d), org.kframework.attributes.Location(Location(1154,8,1154,36)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_impliesBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d), org.kframework.attributes.Location(Location(1154,8,1154,36)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -745,9 +765,9 @@ module TEST \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1154,8,1154,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1154,8,1154,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_modInt_`(I1,I2)=>`_%Int_`(`_+Int_`(`_%Int_`(I1,`absInt(_)_INT-COMMON_Int_Int`(I2)),`absInt(_)_INT-COMMON_Int_Int`(I2)),`absInt(_)_INT-COMMON_Int_Int`(I2)) requires `_=/=Int_`(I2,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(44257f63a99a0583c2d10058edbff90118966e30914b3a637b8315212c681bc4), concrete, org.kframework.attributes.Location(Location(1430,5,1433,23)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)]), simplification] +// rule `_modInt_`(I1,I2)=>`_%Int_`(`_+Int_`(`_%Int_`(I1,`absInt(_)_INT-COMMON_Int_Int`(I2)),`absInt(_)_INT-COMMON_Int_Int`(I2)),`absInt(_)_INT-COMMON_Int_Int`(I2)) requires `_=/=Int_`(I2,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(44257f63a99a0583c2d10058edbff90118966e30914b3a637b8315212c681bc4), concrete, org.kframework.attributes.Location(Location(1434,5,1437,23)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)]), simplification] axiom{R} \implies{R} ( \equals{SortBool{},R}( Lbl'UndsEqlsSlshEqls'Int'Unds'{}(VarI2:SortInt{},\dv{SortInt{}}("0")), @@ -757,9 +777,9 @@ module TEST \and{SortInt{}} ( Lbl'UndsPerc'Int'Unds'{}(Lbl'UndsPlus'Int'Unds'{}(Lbl'UndsPerc'Int'Unds'{}(VarI1:SortInt{},LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(VarI2:SortInt{})),LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(VarI2:SortInt{})),LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(VarI2:SortInt{})), \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("44257f63a99a0583c2d10058edbff90118966e30914b3a637b8315212c681bc4"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1430,5,1433,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("44257f63a99a0583c2d10058edbff90118966e30914b3a637b8315212c681bc4"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1434,5,1437,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_orBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(a5bb27ab54700cb845d17b12e0b0a4cbd5c8944272bcbe0d15ccc0b44d0049ff), org.kframework.attributes.Location(Location(1147,8,1147,32)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_orBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(a5bb27ab54700cb845d17b12e0b0a4cbd5c8944272bcbe0d15ccc0b44d0049ff), org.kframework.attributes.Location(Location(1147,8,1147,32)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -767,9 +787,9 @@ module TEST \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("a5bb27ab54700cb845d17b12e0b0a4cbd5c8944272bcbe0d15ccc0b44d0049ff"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1147,8,1147,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("a5bb27ab54700cb845d17b12e0b0a4cbd5c8944272bcbe0d15ccc0b44d0049ff"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1147,8,1147,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_orBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(942af273100b5a3c1fb3d0c8cc92b0bf845a7b34444c5a6c35b7d3fe72bef48e), org.kframework.attributes.Location(Location(1145,8,1145,34)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_orBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(942af273100b5a3c1fb3d0c8cc92b0bf845a7b34444c5a6c35b7d3fe72bef48e), org.kframework.attributes.Location(Location(1145,8,1145,34)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -777,9 +797,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("942af273100b5a3c1fb3d0c8cc92b0bf845a7b34444c5a6c35b7d3fe72bef48e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1145,8,1145,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("942af273100b5a3c1fb3d0c8cc92b0bf845a7b34444c5a6c35b7d3fe72bef48e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1145,8,1145,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_orBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b), org.kframework.attributes.Location(Location(1146,8,1146,32)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_orBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b), org.kframework.attributes.Location(Location(1146,8,1146,32)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -799,9 +819,9 @@ module TEST \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1146,8,1146,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1146,8,1146,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_orBool_`(#token("true","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2), org.kframework.attributes.Location(Location(1144,8,1144,34)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_orBool_`(#token("true","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2), org.kframework.attributes.Location(Location(1144,8,1144,34)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -821,9 +841,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1144,8,1144,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1144,8,1144,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_orElseBool_`(K,#token("false","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(13cf42d440f9a7a360a8136ee4b35ae7b99501f515322d214c3b866691f4713b), org.kframework.attributes.Location(Location(1152,8,1152,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_orElseBool_`(K,#token("false","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(13cf42d440f9a7a360a8136ee4b35ae7b99501f515322d214c3b866691f4713b), org.kframework.attributes.Location(Location(1152,8,1152,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -831,9 +851,9 @@ module TEST \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("13cf42d440f9a7a360a8136ee4b35ae7b99501f515322d214c3b866691f4713b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1152,8,1152,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("13cf42d440f9a7a360a8136ee4b35ae7b99501f515322d214c3b866691f4713b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1152,8,1152,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_orElseBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2459cad4fbb946a5c7f71565601afeeec79f05f41497b1f7ef547578c88f3158), org.kframework.attributes.Location(Location(1150,8,1150,33)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_orElseBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2459cad4fbb946a5c7f71565601afeeec79f05f41497b1f7ef547578c88f3158), org.kframework.attributes.Location(Location(1150,8,1150,33)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -841,9 +861,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("2459cad4fbb946a5c7f71565601afeeec79f05f41497b1f7ef547578c88f3158"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1150,8,1150,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("2459cad4fbb946a5c7f71565601afeeec79f05f41497b1f7ef547578c88f3158"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1150,8,1150,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_orElseBool_`(#token("false","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf), org.kframework.attributes.Location(Location(1151,8,1151,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_orElseBool_`(#token("false","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf), org.kframework.attributes.Location(Location(1151,8,1151,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -863,9 +883,9 @@ module TEST \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1151,8,1151,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1151,8,1151,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_orElseBool_`(#token("true","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6), org.kframework.attributes.Location(Location(1149,8,1149,33)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_orElseBool_`(#token("true","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6), org.kframework.attributes.Location(Location(1149,8,1149,33)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -885,9 +905,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1149,8,1149,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1149,8,1149,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_xorBool_`(B,B)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f), org.kframework.attributes.Location(Location(1142,8,1142,38)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_xorBool_`(B,B)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f), org.kframework.attributes.Location(Location(1142,8,1142,38)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -907,9 +927,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1142,8,1142,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1142,8,1142,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_xorBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(69f518203376930fb76ce51df5dd0c6c81d19f71eba3a1852afa5301d02eb4fa), org.kframework.attributes.Location(Location(1141,8,1141,38)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] +// rule `_xorBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(69f518203376930fb76ce51df5dd0c6c81d19f71eba3a1852afa5301d02eb4fa), org.kframework.attributes.Location(Location(1141,8,1141,38)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -917,9 +937,9 @@ module TEST \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("69f518203376930fb76ce51df5dd0c6c81d19f71eba3a1852afa5301d02eb4fa"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1141,8,1141,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + [UNIQUE'Unds'ID{}("69f518203376930fb76ce51df5dd0c6c81d19f71eba3a1852afa5301d02eb4fa"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1141,8,1141,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] -// rule `_xorBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf), org.kframework.attributes.Location(Location(1140,8,1140,38)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_xorBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf), org.kframework.attributes.Location(Location(1140,8,1140,38)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -939,9 +959,9 @@ module TEST \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1140,8,1140,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1140,8,1140,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `_|Set__SET_Set_Set_Set`(S1,S2)=>`_Set_`(S1,`Set:difference`(S2,S1)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(c384edb8f3875244a593dda6163c3dee1bce5485e4e1848892aebc2bab67d2e9), concrete, org.kframework.attributes.Location(Location(749,8,749,45)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `_|Set__SET_Set_Set_Set`(S1,S2)=>`_Set_`(S1,`Set:difference`(S2,S1)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(c384edb8f3875244a593dda6163c3dee1bce5485e4e1848892aebc2bab67d2e9), concrete, org.kframework.attributes.Location(Location(749,8,749,45)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -961,9 +981,9 @@ module TEST \and{SortSet{}} ( Lbl'Unds'Set'Unds'{}(VarS1:SortSet{},LblSet'Coln'difference{}(VarS2:SortSet{},VarS1:SortSet{})), \top{SortSet{}}()))) - [UNIQUE'Unds'ID{}("c384edb8f3875244a593dda6163c3dee1bce5485e4e1848892aebc2bab67d2e9"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(749,8,749,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("c384edb8f3875244a593dda6163c3dee1bce5485e4e1848892aebc2bab67d2e9"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(749,8,749,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN)=>`_modInt_`(`_>>Int_`(I,IDX),`_<`_modInt_`(`_>>Int_`(I,IDX),`_<I requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b), org.kframework.attributes.Location(Location(1442,8,1442,28)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `freshInt(_)_INT_Int_Int`(I)=>I requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b), org.kframework.attributes.Location(Location(1446,8,1446,28)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -1005,7 +1025,7 @@ module TEST \and{SortInt{}} ( VarI:SortInt{}, \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1442,8,1442,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1446,8,1446,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] // rule getGeneratedCounterCell(``(_Gen0,_Gen1,Cell))=>Cell requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(6aaa6e2dcc27f3f1c36a11a988ed5674f7b6892c35cde7937bcb682488aaf8e1)] axiom{R} \implies{R} ( @@ -1075,7 +1095,7 @@ module TEST \top{SortKCell{}}()))) [UNIQUE'Unds'ID{}("888ac40929773fd17d5b9fd1e9d0be94791665a663f07907d894c31dccc871a5")] -// rule initStateCell(.KList)=>``(`_Map_`(`_|->_`(inj{MInt,KItem}(#token("0p256","MInt{256}")),inj{MInt,KItem}(#token("1p256","MInt{256}"))),`_|->_`(inj{MInt,KItem}(#token("0p160","MInt{160}")),inj{MInt,KItem}(#token("1p160","MInt{160}"))))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(70b1649b1bedd0ab5fec5e656f8bf448702454500c67f5a97835552511377501), initializer] +// rule initStateCell(.KList)=>``(`_Map_`(`_Map_`(`_|->_`(inj{MInt,KItem}(#token("0p256","MInt{256}")),inj{MInt,KItem}(#token("1p256","MInt{256}"))),`_|->_`(inj{MInt,KItem}(#token("0p160","MInt{160}")),inj{MInt,KItem}(#token("1p160","MInt{160}")))),`_|->_`(inj{MInt,KItem}(#token("0p128","MInt{128}")),inj{MInt,KItem}(#token("1p128","MInt{128}"))))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(afb9707c007f5578878b8e55c27528966bafe0fbf7047baf623b5501613dcf02), initializer] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -1085,22 +1105,76 @@ module TEST \equals{SortStateCell{},R} ( LblinitStateCell{}(), \and{SortStateCell{}} ( - Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("0p256")),inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("0p160")),inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160"))))), + Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("0p256")),inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("0p160")),inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort128{}}, SortKItem{}}(\dv{SortMInt{Sort128{}}}("0p128")),inj{SortMInt{Sort128{}}, SortKItem{}}(\dv{SortMInt{Sort128{}}}("1p128"))))), \top{SortStateCell{}}()))) - [UNIQUE'Unds'ID{}("70b1649b1bedd0ab5fec5e656f8bf448702454500c67f5a97835552511377501")] + [UNIQUE'Unds'ID{}("afb9707c007f5578878b8e55c27528966bafe0fbf7047baf623b5501613dcf02")] + +// rule is128(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ed30b6d387415a2fd25e7dd9cdf1134305182152d6fc0f17dfb0e7e8470db19e), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:Sort128{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{Sort128{}, SortKItem{}}(Var'Unds'Gen1:Sort128{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + Lblis128{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("ed30b6d387415a2fd25e7dd9cdf1134305182152d6fc0f17dfb0e7e8470db19e"), owise{}()] + +// rule is128(inj{128,KItem}(128))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5ac512ae7b5a4834f889b26e92e88909be476b024c47c382c396e35ff459cf15)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{Sort128{}, SortKItem{}}(Var128:Sort128{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + Lblis128{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("5ac512ae7b5a4834f889b26e92e88909be476b024c47c382c396e35ff459cf15")] // rule is160(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(aa3f00cb9a02ba98f022164716991c7b0359fee8a7542d52899563654190f19d), owise] axiom{R} \implies{R} ( \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:Sort160{}, + \exists{R} (Var'Unds'Gen0:Sort160{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{Sort160{}, SortKItem{}}(Var'Unds'Gen1:Sort160{}),dotk{}()) + kseq{}(inj{Sort160{}, SortKItem{}}(Var'Unds'Gen0:Sort160{}),dotk{}()) ), \top{R} () ) @@ -1148,13 +1222,13 @@ module TEST \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:Sort256{}, + \exists{R} (Var'Unds'Gen0:Sort256{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{Sort256{}, SortKItem{}}(Var'Unds'Gen1:Sort256{}),dotk{}()) + kseq{}(inj{Sort256{}, SortKItem{}}(Var'Unds'Gen0:Sort256{}),dotk{}()) ), \top{R} () ) @@ -1418,13 +1492,13 @@ module TEST \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen0:SortInt{}, + \exists{R} (Var'Unds'Gen1:SortInt{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortInt{}, SortKItem{}}(Var'Unds'Gen0:SortInt{}),dotk{}()) + kseq{}(inj{SortInt{}, SortKItem{}}(Var'Unds'Gen1:SortInt{}),dotk{}()) ), \top{R} () ) @@ -1598,13 +1672,13 @@ module TEST \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:SortKConfigVar{}, + \exists{R} (Var'Unds'Gen0:SortKConfigVar{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortKConfigVar{}, SortKItem{}}(Var'Unds'Gen1:SortKConfigVar{}),dotk{}()) + kseq{}(inj{SortKConfigVar{}, SortKItem{}}(Var'Unds'Gen0:SortKConfigVar{}),dotk{}()) ), \top{R} () ) @@ -1652,13 +1726,13 @@ module TEST \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen0:SortKItem{}, + \exists{R} (Var'Unds'Gen1:SortKItem{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(Var'Unds'Gen0:SortKItem{},dotk{}()) + kseq{}(Var'Unds'Gen1:SortKItem{},dotk{}()) ), \top{R} () ) @@ -1706,13 +1780,13 @@ module TEST \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen0:SortList{}, + \exists{R} (Var'Unds'Gen1:SortList{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortList{}, SortKItem{}}(Var'Unds'Gen0:SortList{}),dotk{}()) + kseq{}(inj{SortList{}, SortKItem{}}(Var'Unds'Gen1:SortList{}),dotk{}()) ), \top{R} () ) @@ -1755,6 +1829,60 @@ module TEST \top{SortBool{}}()))) [UNIQUE'Unds'ID{}("7d4dddf5bbdb61cfd11fb9be1071be7bd551cf186607cf6f493cfade3221c446")] +// rule `isMInt{128}`(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(dc188a31b206a41038341299d0ea46a88bb305e193b1826405aa6d319e2f07fb), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortMInt{Sort128{}}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortMInt{Sort128{}}, SortKItem{}}(Var'Unds'Gen1:SortMInt{Sort128{}}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisMInt'LBra'128'RBra'{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("dc188a31b206a41038341299d0ea46a88bb305e193b1826405aa6d319e2f07fb"), owise{}()] + +// rule `isMInt{128}`(inj{MInt,KItem}(MInt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(b45946757c7ad7c8674f192e32a3da904d0ef02903159bb3a00e70c4ffa91172)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortMInt{Sort128{}}, SortKItem{}}(VarMInt:SortMInt{Sort128{}}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisMInt'LBra'128'RBra'{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("b45946757c7ad7c8674f192e32a3da904d0ef02903159bb3a00e70c4ffa91172")] + // rule `isMInt{160}`(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(42372f41a4d487dbdae4c035e45ef87b517a47c8260ec37573301b50e64a4b1a), owise] axiom{R} \implies{R} ( \and{R} ( @@ -1922,13 +2050,13 @@ module TEST \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:SortSet{}, + \exists{R} (Var'Unds'Gen0:SortSet{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortSet{}, SortKItem{}}(Var'Unds'Gen1:SortSet{}),dotk{}()) + kseq{}(inj{SortSet{}, SortKItem{}}(Var'Unds'Gen0:SortSet{}),dotk{}()) ), \top{R} () ) @@ -2030,13 +2158,13 @@ module TEST \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:SortStateCellOpt{}, + \exists{R} (Var'Unds'Gen0:SortStateCellOpt{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortStateCellOpt{}, SortKItem{}}(Var'Unds'Gen1:SortStateCellOpt{}),dotk{}()) + kseq{}(inj{SortStateCellOpt{}, SortKItem{}}(Var'Unds'Gen0:SortStateCellOpt{}),dotk{}()) ), \top{R} () ) @@ -2079,7 +2207,7 @@ module TEST \top{SortBool{}}()))) [UNIQUE'Unds'ID{}("b5285b2b23133d428fcb21af02d523dec10d3660f0f43d59933927d0ee79471e")] -// rule ite{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(1ff8f4d71e4c13084eed473b08740da83c4cc7f1875d340d86dc72124c48b4a0), org.kframework.attributes.Location(Location(2320,8,2320,59)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] +// rule ite{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(1ff8f4d71e4c13084eed473b08740da83c4cc7f1875d340d86dc72124c48b4a0), org.kframework.attributes.Location(Location(2324,8,2324,59)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -2105,9 +2233,9 @@ module TEST \and{SortK{}} ( VarB1:SortK{}, \top{SortK{}}()))) - [UNIQUE'Unds'ID{}("1ff8f4d71e4c13084eed473b08740da83c4cc7f1875d340d86dc72124c48b4a0"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2320,8,2320,59)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("1ff8f4d71e4c13084eed473b08740da83c4cc7f1875d340d86dc72124c48b4a0"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2324,8,2324,59)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule ite{K}(C,_Gen0,B2)=>B2 requires `notBool_`(C) ensures #token("true","Bool") [UNIQUE_ID(2f3f58a93926913fc5ca147dfd8d3d612508bc8ff67412ef10935df7c09554d5), org.kframework.attributes.Location(Location(2321,8,2321,67)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] +// rule ite{K}(C,_Gen0,B2)=>B2 requires `notBool_`(C) ensures #token("true","Bool") [UNIQUE_ID(2f3f58a93926913fc5ca147dfd8d3d612508bc8ff67412ef10935df7c09554d5), org.kframework.attributes.Location(Location(2325,8,2325,67)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -2133,9 +2261,9 @@ module TEST \and{SortK{}} ( VarB2:SortK{}, \top{SortK{}}()))) - [UNIQUE'Unds'ID{}("2f3f58a93926913fc5ca147dfd8d3d612508bc8ff67412ef10935df7c09554d5"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2321,8,2321,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("2f3f58a93926913fc5ca147dfd8d3d612508bc8ff67412ef10935df7c09554d5"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2325,8,2325,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `minInt(_,_)_INT-COMMON_Int_Int_Int`(I1,I2)=>I1 requires `_I1 requires `_I2 requires `_>=Int_`(I1,I2) ensures #token("true","Bool") [UNIQUE_ID(e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3), org.kframework.attributes.Location(Location(1436,8,1436,57)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] +// rule `minInt(_,_)_INT-COMMON_Int_Int_Int`(I1,I2)=>I2 requires `_>=Int_`(I1,I2) ensures #token("true","Bool") [UNIQUE_ID(e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3), org.kframework.attributes.Location(Location(1440,8,1440,57)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -2181,9 +2309,9 @@ module TEST \and{SortInt{}} ( VarI2:SortInt{}, \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1436,8,1436,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1440,8,1440,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `notBool_`(#token("false","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415), org.kframework.attributes.Location(Location(1128,8,1128,29)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `notBool_`(#token("false","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415), org.kframework.attributes.Location(Location(1128,8,1128,29)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -2199,9 +2327,9 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1128,8,1128,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1128,8,1128,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `notBool_`(#token("true","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c), org.kframework.attributes.Location(Location(1127,8,1127,29)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `notBool_`(#token("true","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c), org.kframework.attributes.Location(Location(1127,8,1127,29)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -2217,7 +2345,7 @@ module TEST \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1127,8,1127,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1127,8,1127,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] // rule `project:Bool`(inj{Bool,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5872f0d5b8131216db7bc41e2c3a423e55f4b8581589fcbd1bf93b2ca6862d54), projection] axiom{R} \implies{R} ( @@ -2399,6 +2527,24 @@ module TEST \top{SortList{}}()))) [UNIQUE'Unds'ID{}("2b75eac5a59779d336e6cf9632bf9ba7d67286f322e753108b34e62f2443efe5")] +// rule `project:MInt{128}`(inj{MInt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(250308c1ea628de6748f15212dc6e789392aa9efa195dc1ffa2855b7ab8940a4), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortMInt{Sort128{}}, SortKItem{}}(VarK:SortMInt{Sort128{}}),dotk{}()) + ), + \top{R} () + )), + \equals{SortMInt{Sort128{}},R} ( + Lblproject'Coln'MInt'LBra'128'RBra'{}(X0:SortK{}), + \and{SortMInt{Sort128{}}} ( + VarK:SortMInt{Sort128{}}, + \top{SortMInt{Sort128{}}}()))) + [UNIQUE'Unds'ID{}("250308c1ea628de6748f15212dc6e789392aa9efa195dc1ffa2855b7ab8940a4")] + // rule `project:MInt{160}`(inj{MInt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e7ba7fd34b4205d4632fc16d50d52a48d062fd4bcdf0eac660ea7f27d2d43213), projection] axiom{R} \implies{R} ( \and{R}( @@ -2507,7 +2653,7 @@ module TEST \top{SortStateCellOpt{}}()))) [UNIQUE'Unds'ID{}("e9c7307bada1aa928bd077216781fb45fe226c28e19ec950318b7cfa9e6ae9be")] -// rule pushList(K,L1)=>`_List_`(`ListItem`(K),L1) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f6967050cc4ec32c2d34d52f5577e09120f730420d2c5dc838cba81d04c57adf), org.kframework.attributes.Location(Location(954,8,954,54)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule pushList(K,L1)=>`_List_`(`ListItem`(K),L1) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f6967050cc4ec32c2d34d52f5577e09120f730420d2c5dc838cba81d04c57adf), org.kframework.attributes.Location(Location(954,8,954,54)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -2527,9 +2673,9 @@ module TEST \and{SortList{}} ( Lbl'Unds'List'Unds'{}(LblListItem{}(VarK:SortKItem{}),VarL1:SortList{}), \top{SortList{}}()))) - [UNIQUE'Unds'ID{}("f6967050cc4ec32c2d34d52f5577e09120f730420d2c5dc838cba81d04c57adf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(954,8,954,54)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("f6967050cc4ec32c2d34d52f5577e09120f730420d2c5dc838cba81d04c57adf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(954,8,954,54)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `signExtendBitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN)=>`_-Int_`(`_modInt_`(`_+Int_`(`bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN),`_<`_-Int_`(`_modInt_`(`_+Int_`(`bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN),`_<`_-Int_`(`_<`_-Int_`(`_<`_-Int_`(#token("0","Int"),`_<`_-Int_`(#token("0","Int"),`_<`_orBool_`(`_Int_`(I,`smaxMInt(_)_MINT_Int_Int`(N))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(451ca26671f46f6bc7874beade344389ec2cd222fb83b97a9eedd324b8353629), org.kframework.attributes.Location(Location(2918,5,2920,49)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `soverflowMInt(_,_)_MINT_Bool_Int_Int`(N,I)=>`_orBool_`(`_Int_`(I,`smaxMInt(_)_MINT_Int_Int`(N))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(451ca26671f46f6bc7874beade344389ec2cd222fb83b97a9eedd324b8353629), org.kframework.attributes.Location(Location(2922,5,2924,49)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -2611,9 +2757,9 @@ module TEST \and{SortBool{}} ( Lbl'Unds'orBool'Unds'{}(Lbl'Unds-LT-'Int'Unds'{}(VarI:SortInt{},LblsminMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(VarN:SortInt{})),Lbl'Unds-GT-'Int'Unds'{}(VarI:SortInt{},LblsmaxMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(VarN:SortInt{}))), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("451ca26671f46f6bc7874beade344389ec2cd222fb83b97a9eedd324b8353629"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2918,5,2920,49)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("451ca26671f46f6bc7874beade344389ec2cd222fb83b97a9eedd324b8353629"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2922,5,2924,49)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `umaxMInt(_)_MINT_Int_Int`(N)=>`_-Int_`(`_<`_-Int_`(`_<#token("0","Int") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(340a658083b6c1ac8b55d4c7c643de32cf560bb8b733ed8f9b139aee7c8c838b), org.kframework.attributes.Location(Location(2904,8,2904,28)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `uminMInt(_)_MINT_Int_Int`(_Gen0)=>#token("0","Int") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(340a658083b6c1ac8b55d4c7c643de32cf560bb8b733ed8f9b139aee7c8c838b), org.kframework.attributes.Location(Location(2908,8,2908,28)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -2647,9 +2793,9 @@ module TEST \and{SortInt{}} ( \dv{SortInt{}}("0"), \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("340a658083b6c1ac8b55d4c7c643de32cf560bb8b733ed8f9b139aee7c8c838b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2904,8,2904,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("340a658083b6c1ac8b55d4c7c643de32cf560bb8b733ed8f9b139aee7c8c838b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2908,8,2908,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -// rule `uoverflowMInt(_,_)_MINT_Bool_Int_Int`(N,I)=>`_orBool_`(`_Int_`(I,`umaxMInt(_)_MINT_Int_Int`(N))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(669772aa6f72077d244868ca7dc07771189bb331b0347f2384101ba036d78ab2), org.kframework.attributes.Location(Location(2922,5,2924,49)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] +// rule `uoverflowMInt(_,_)_MINT_Bool_Int_Int`(N,I)=>`_orBool_`(`_Int_`(I,`umaxMInt(_)_MINT_Int_Int`(N))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(669772aa6f72077d244868ca7dc07771189bb331b0347f2384101ba036d78ab2), org.kframework.attributes.Location(Location(2926,5,2928,49)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -2669,6 +2815,6 @@ module TEST \and{SortBool{}} ( Lbl'Unds'orBool'Unds'{}(Lbl'Unds-LT-'Int'Unds'{}(VarI:SortInt{},LbluminMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(VarN:SortInt{})),Lbl'Unds-GT-'Int'Unds'{}(VarI:SortInt{},LblumaxMInt'LParUndsRParUnds'MINT'Unds'Int'Unds'Int{}(VarN:SortInt{}))), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("669772aa6f72077d244868ca7dc07771189bb331b0347f2384101ba036d78ab2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2922,5,2924,49)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + [UNIQUE'Unds'ID{}("669772aa6f72077d244868ca7dc07771189bb331b0347f2384101ba036d78ab2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2926,5,2928,49)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] -endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1,1,17,10)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] +endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1,1,20,10)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/hash-mint.k)")] diff --git a/test/defn/k-files/hash-mint.k b/test/defn/k-files/hash-mint.k index b087d3914..31fd9f035 100644 --- a/test/defn/k-files/hash-mint.k +++ b/test/defn/k-files/hash-mint.k @@ -3,15 +3,18 @@ module HASH-MINT syntax MInt{160} syntax MInt{256} + syntax MInt{128} configuration $PGM:K - 0p256 |-> 1p256 0p160 |-> 1p160 + 0p256 |-> 1p256 0p160 |-> 1p160 0p128 |-> 1p128 - syntax KItem ::= foo() | bar() + syntax KItem ::= foo() | bar() | baz() rule foo() => bar() ~> State [ 0p256 ] ... State - rule bar() => State [ 0p160 ] ... + rule bar() => baz() ~> State [ 0p160 ] ... + State + rule baz() => State [ 0p128 ] ... State endmodule diff --git a/test/input/hash-mint.in b/test/input/hash-mint.in index 10f45cbe0..113cb72c1 100644 --- a/test/input/hash-mint.in +++ b/test/input/hash-mint.in @@ -1 +1 @@ -LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lblfoo'LParRParUnds'TEST'Unds'KItem{}()))) +LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lblfoo'LParRParUnds'HASH-MINT'Unds'KItem{}()))) diff --git a/test/output/hash-mint.out.diff b/test/output/hash-mint.out.diff index 724245d69..05b16262c 100644 --- a/test/output/hash-mint.out.diff +++ b/test/output/hash-mint.out.diff @@ -1 +1 @@ -Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")),kseq{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256")),dotk{}()))),Lbl'-LT-'state'-GT-'{}(\left-assoc{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("0p256")),inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("0p160")),inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))) \ No newline at end of file +Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortMInt{Sort128{}}, SortKItem{}}(\dv{SortMInt{Sort128{}}}("1p128")),kseq{}(inj{SortMInt{Sort160{}}, SortKItem{}}(\dv{SortMInt{Sort160{}}}("1p160")),kseq{}(inj{SortMInt{Sort256{}}, SortKItem{}}(\dv{SortMInt{Sort256{}}}("1p256")),dotk{}()))))