From f1f187103db6fd418b4f7d0935059075cec5e41e Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 4 Dec 2023 17:19:31 +0000 Subject: [PATCH] Test rawTerm support --- include/runtime/header.h | 2 +- runtime/util/ConfigurationSerializer.cpp | 4 +- runtime/util/util.cpp | 4 +- test/python/Inputs/evaluate.kore | 406 ++++++++++++----------- test/python/k-files/evaluate.k | 7 + test/python/test_evaluate.py | 17 +- 6 files changed, 247 insertions(+), 193 deletions(-) diff --git a/include/runtime/header.h b/include/runtime/header.h index 48aebb302..68d9c45bd 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -411,7 +411,7 @@ extern const uint32_t first_inj_tag, last_inj_tag; bool is_injection(block *); block *strip_injection(block *); block *constructKItemInj(void *subject, const char *sort, bool raw_value); -block *constructRawTerm(void *subject, const char *sort); +block *constructRawTerm(void *subject, const char *sort, bool raw_value); } std::string floatToString(const floating *); diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 8699a348c..15361d721 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -453,7 +453,7 @@ void serializeTermToFile( void serializeRawTermToFile( const char *filename, void *subject, const char *sort) { - block *term = constructRawTerm(subject, sort); + block *term = constructRawTerm(subject, sort, true); char *data; size_t size; @@ -467,7 +467,7 @@ void serializeRawTermToFile( std::shared_ptr sortedTermToKorePattern(block *subject, const char *sort) { auto is_kitem = (std::string(sort) == "SortKItem{}"); - block *term = is_kitem ? subject : constructRawTerm(subject, sort); + block *term = is_kitem ? subject : constructRawTerm(subject, sort, false); char *data_out; size_t size_out; diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp index 41535ccae..59cb93b58 100644 --- a/runtime/util/util.cpp +++ b/runtime/util/util.cpp @@ -29,10 +29,10 @@ block *constructKItemInj(void *subject, const char *sort, bool raw_value) { return static_cast(constructCompositePattern(tag, args)); } -block *constructRawTerm(void *subject, const char *sort) { +block *constructRawTerm(void *subject, const char *sort, bool raw_value) { auto tag = getTagForSymbolName("rawTerm{}"); auto args = std::vector{ - static_cast(constructKItemInj(subject, sort, true))}; + static_cast(constructKItemInj(subject, sort, raw_value))}; return static_cast(constructCompositePattern(tag, args)); } diff --git a/test/python/Inputs/evaluate.kore b/test/python/Inputs/evaluate.kore index 8d8c90032..8a24f96d7 100644 --- a/test/python/Inputs/evaluate.kore +++ b/test/python/Inputs/evaluate.kore @@ -70,93 +70,94 @@ module EVALUATE // sorts sort SortKCellOpt{} [] 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(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/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(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'List{}())] sort SortKCell{} [] sort SortGeneratedTopCell{} [] 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(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/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(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Map{}())] sort SortGeneratedCounterCellOpt{} [] - sort SortKConfigVar{} [hasDomainValues{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(40,3,40,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/kast.md)"), token{}()] - hooked-sort SortInt{} [hasDomainValues{}(), hook{}("INT.Int"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1189,3,1189,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)")] - 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(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Set{}())] + sort SortKConfigVar{} [hasDomainValues{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(40,3,40,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/kast.md)"), token{}()] + hooked-sort SortInt{} [hasDomainValues{}(), hook{}("INT.Int"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1189,3,1189,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)")] + 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(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Set{}())] sort SortFoo{} [] - hooked-sort SortBool{} [hasDomainValues{}(), hook{}("BOOL.Bool"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1068,3,1068,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)")] + hooked-sort SortBool{} [hasDomainValues{}(), hook{}("BOOL.Bool"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1068,3,1068,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)")] // symbols - hooked-symbol Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortSort}(SortBool{}, SortSort, SortSort) : SortSort [format{}("%c#if%r %1 %c#then%r %2 %c#else%r %3 %c#fi%r"), function{}(), functional{}(), hook{}("KEQUAL.ite"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2277,26,2277,121)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("ite"), terminals{}("1010101"), total{}()] - hooked-symbol Lbl'Stop'List{}() : SortList{} [format{}("%c.List%r"), function{}(), functional{}(), hook{}("LIST.unit"), klabel{}(".List"), latex{}("\\dotCt{List}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(937,19,937,142)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_nil"), symbol'Kywd'{}(), terminals{}("1"), total{}()] - hooked-symbol Lbl'Stop'Map{}() : SortMap{} [format{}("%c.Map%r"), function{}(), functional{}(), hook{}("MAP.unit"), klabel{}(".Map"), latex{}("\\dotCt{Map}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(248,18,248,124)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1"), total{}()] - hooked-symbol Lbl'Stop'Set{}() : SortSet{} [format{}("%c.Set%r"), function{}(), functional{}(), hook{}("SET.unit"), klabel{}(".Set"), latex{}("\\dotCt{Set}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(729,18,729,118)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1"), total{}()] + hooked-symbol Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortSort}(SortBool{}, SortSort, SortSort) : SortSort [format{}("%c#if%r %1 %c#then%r %2 %c#else%r %3 %c#fi%r"), function{}(), functional{}(), hook{}("KEQUAL.ite"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2277,26,2277,121)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("ite"), terminals{}("1010101"), total{}()] + hooked-symbol Lbl'Stop'List{}() : SortList{} [format{}("%c.List%r"), function{}(), functional{}(), hook{}("LIST.unit"), klabel{}(".List"), latex{}("\\dotCt{List}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(937,19,937,142)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_nil"), symbol'Kywd'{}(), terminals{}("1"), total{}()] + hooked-symbol Lbl'Stop'Map{}() : SortMap{} [format{}("%c.Map%r"), function{}(), functional{}(), hook{}("MAP.unit"), klabel{}(".Map"), latex{}("\\dotCt{Map}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(248,18,248,124)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1"), total{}()] + hooked-symbol Lbl'Stop'Set{}() : SortSet{} [format{}("%c.Set%r"), function{}(), functional{}(), hook{}("SET.unit"), klabel{}(".Set"), latex{}("\\dotCt{Set}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(729,18,729,118)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1"), total{}()] symbol Lbl'-LT-'generatedCounter'-GT-'{}(SortInt{}) : SortGeneratedCounterCell{} [cell{}(), cellName{}("generatedCounter"), constructor{}(), format{}("%c%r%i%n%1%d%n%c%r"), functional{}(), injective{}(), left{}(), priorities{}(), right{}(), terminals{}("101")] symbol Lbl'-LT-'generatedTop'-GT-'{}(SortKCell{}, SortGeneratedCounterCell{}) : SortGeneratedTopCell{} [cell{}(), cellName{}("generatedTop"), constructor{}(), format{}("%1"), functional{}(), injective{}(), left{}(), priorities{}(), right{}(), terminals{}("1001")] symbol Lbl'-LT-'generatedTop'-GT-'-fragment{}(SortKCellOpt{}, SortGeneratedCounterCellOpt{}) : SortGeneratedTopCellFragment{} [cellFragment{}("GeneratedTopCell"), constructor{}(), format{}("%c-fragment%r %1 %2 %c-fragment%r"), functional{}(), injective{}(), left{}(), priorities{}(), right{}(), terminals{}("1001")] - symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [cell{}(), cellName{}("k"), constructor{}(), format{}("%c%r%i%n%1%d%n%c%r"), functional{}(), injective{}(), left{}(), maincell{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(535,17,535,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/kast.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), priorities{}(), right{}(), terminals{}("101")] - hooked-symbol LblList'Coln'get{}(SortList{}, SortInt{}) : SortKItem{} [format{}("%1 %c[%r %2 %c]%r"), function{}(), hook{}("LIST.get"), klabel{}("List:get"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(956,20,956,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("0101")] - hooked-symbol LblList'Coln'range{}(SortList{}, SortInt{}, SortInt{}) : SortList{} [format{}("%crange%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}(), hook{}("LIST.range"), klabel{}("List:range"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1003,19,1003,120)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("11010101")] - hooked-symbol LblListItem{}(SortKItem{}) : SortList{} [format{}("%cListItem%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("LIST.element"), klabel{}("ListItem"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(945,19,945,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_elem"), symbol'Kywd'{}(), terminals{}("1101"), total{}()] - hooked-symbol LblMap'Coln'lookup{}(SortMap{}, SortKItem{}) : SortKItem{} [format{}("%1 %c[%r %2 %c]%r"), function{}(), hook{}("MAP.lookup"), klabel{}("Map:lookup"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(271,20,271,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("0101")] - hooked-symbol LblMap'Coln'update{}(SortMap{}, SortKItem{}, SortKItem{}) : SortMap{} [format{}("%1 %c[%r %2 %c<-%r %3 %c]%r"), function{}(), functional{}(), hook{}("MAP.update"), klabel{}("Map:update"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(290,18,290,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), prefer{}(), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010101"), total{}()] - hooked-symbol LblSet'Coln'difference{}(SortSet{}, SortSet{}) : SortSet{} [format{}("%1 %c-Set%r %2"), function{}(), functional{}(), hook{}("SET.difference"), klabel{}("Set:difference"), latex{}("{#1}-_{\\it Set}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(769,18,769,142)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol LblSet'Coln'in{}(SortKItem{}, SortSet{}) : SortBool{} [format{}("%1 %cin%r %2"), function{}(), functional{}(), hook{}("SET.in"), klabel{}("Set:in"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(777,19,777,102)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol LblSetItem{}(SortKItem{}) : SortSet{} [format{}("%cSetItem%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("SET.element"), injective{}(), klabel{}("SetItem"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(737,18,737,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1101"), total{}()] - hooked-symbol Lbl'UndsPerc'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c%%Int%r %2"), function{}(), hook{}("INT.tmod"), klabel{}("_%Int_"), latex{}("{#1}\\mathrel{\\%_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsStar'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1237,18,1237,171)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("mod"), symbol'Kywd'{}(), terminals{}("010")] - hooked-symbol Lbl'UndsAnd-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c&Int%r %2"), function{}(), functional{}(), hook{}("INT.and"), klabel{}("_&Int_"), latex{}("{#1}\\mathrel{\\&_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsAnd-'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1248,18,1248,184)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smtlib{}("andInt"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'UndsStar'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c*Int%r %2"), function{}(), functional{}(), hook{}("INT.mul"), klabel{}("_*Int_"), latex{}("{#1}\\mathrel{\\ast_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'Unds'modInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsStar'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1233,18,1233,183)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("*"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'UndsPlus'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c+Int%r %2"), function{}(), functional{}(), hook{}("INT.add"), klabel{}("_+Int_"), latex{}("{#1}\\mathrel{+_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1242,18,1242,180)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smt-hook{}("+"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'-Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c-Int%r %2"), function{}(), functional{}(), hook{}("INT.sub"), klabel{}("_-Int_"), latex{}("{#1}\\mathrel{-_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1243,18,1243,174)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smt-hook{}("-"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [format{}("%1 %c-Map%r %2"), function{}(), functional{}(), hook{}("MAP.difference"), latex{}("{#1}-_{\\it Map}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(311,18,311,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'UndsSlsh'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c/Int%r %2"), function{}(), hook{}("INT.tdiv"), klabel{}("_/Int_"), latex{}("{#1}\\mathrel{\\div_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1236,18,1236,173)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("div"), symbol'Kywd'{}(), terminals{}("010")] - hooked-symbol Lbl'Unds-LT--LT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c<=Int%r %2"), function{}(), functional{}(), hook{}("INT.ge"), klabel{}("_>=Int_"), latex{}("{#1}\\mathrel{\\geq_{\\scriptstyle\\it Int}}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1306,19,1306,166)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}(">="), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds-GT--GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c>>Int%r %2"), function{}(), hook{}("INT.shr"), klabel{}("_>>Int_"), latex{}("{#1}\\mathrel{\\gg_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1245,18,1245,173)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smtlib{}("shrInt"), symbol'Kywd'{}(), terminals{}("010")] - hooked-symbol Lbl'Unds-GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortBool{} [format{}("%1 %c>Int%r %2"), function{}(), functional{}(), hook{}("INT.gt"), klabel{}("_>Int_"), latex{}("{#1}\\mathrel{>_{\\scriptstyle\\it Int}}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1307,19,1307,161)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}(">"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'List'Unds'{}(SortList{}, SortList{}) : SortList{} [assoc{}(), element{}(LblListItem{}()), format{}("%1%n%2"), function{}(), functional{}(), hook{}("LIST.concat"), klabel{}("_List_"), left{}(Lbl'Unds'List'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(929,19,929,188)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_concat"), symbol'Kywd'{}(), terminals{}("00"), total{}(), unit{}(Lbl'Stop'List{}())] - hooked-symbol Lbl'Unds'Map'Unds'{}(SortMap{}, SortMap{}) : SortMap{} [assoc{}(), comm{}(), element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), format{}("%1%n%2"), function{}(), hook{}("MAP.concat"), index{}("0"), klabel{}("_Map_"), left{}(Lbl'Unds'Map'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(240,18,240,173)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("00"), unit{}(Lbl'Stop'Map{}())] - hooked-symbol Lbl'Unds'Set'Unds'{}(SortSet{}, SortSet{}) : SortSet{} [assoc{}(), comm{}(), element{}(LblSetItem{}()), format{}("%1%n%2"), function{}(), hook{}("SET.concat"), idem{}(), klabel{}("_Set_"), left{}(Lbl'Unds'Set'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(721,18,721,165)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("00"), unit{}(Lbl'Stop'Set{}())] - hooked-symbol Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortKItem{}) : SortList{} [format{}("%1 %c[%r %2 %c<-%r %3 %c]%r"), function{}(), hook{}("LIST.update"), klabel{}("List:set"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(965,19,965,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010101")] - hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(SortMap{}, SortKItem{}) : SortMap{} [format{}("%1 %c[%r %2 %c<-%r %cundef%r %c]%r"), function{}(), functional{}(), hook{}("MAP.remove"), klabel{}("_[_<-undef]"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(299,18,299,117)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010111"), total{}()] - hooked-symbol Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem{}(SortMap{}, SortKItem{}, SortKItem{}) : SortKItem{} [format{}("%1 %c[%r %2 %c]%r %corDefault%r %3"), function{}(), functional{}(), hook{}("MAP.lookupOrDefault"), klabel{}("Map:lookupOrDefault"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(281,20,281,134)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010110"), total{}()] - hooked-symbol Lbl'UndsXor-Perc'Int'UndsUnds'{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c^%%Int%r %2 %3"), function{}(), hook{}("INT.powmod"), klabel{}("_^%Int__"), left{}(Lbl'UndsXor-Perc'Int'UndsUnds'{}(),Lbl'UndsXor-'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1231,18,1231,139)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("(mod (^ #1 #2) #3)"), symbol'Kywd'{}(), terminals{}("0100")] - hooked-symbol Lbl'UndsXor-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c^Int%r %2"), function{}(), hook{}("INT.pow"), klabel{}("_^Int_"), latex{}("{#1}\\mathrel{{\\char`\\^}_{\\!\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsXor-'Int'Unds'{}(),Lbl'UndsXor-Perc'Int'UndsUnds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1230,18,1230,178)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("^"), symbol'Kywd'{}(), terminals{}("010")] - hooked-symbol Lbl'Unds'andBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %candBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.and"), klabel{}("_andBool_"), latex{}("{#1}\\wedge_{\\scriptstyle\\it Bool}{#2}"), left{}(Lbl'Unds'andBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1101,19,1101,192)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("and"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'andThenBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %candThenBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.andThen"), klabel{}("_andThenBool_"), left{}(Lbl'Unds'andThenBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1102,19,1102,154)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("and"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'divInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %cdivInt%r %2"), function{}(), hook{}("INT.ediv"), klabel{}("_divInt_"), left{}(Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1239,18,1239,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("div"), symbol'Kywd'{}(), terminals{}("010")] - symbol Lbl'Unds'dividesInt'UndsUnds'INT-COMMON'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [format{}("%1 %cdividesInt%r %2"), function{}(), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1318,19,1318,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010")] - hooked-symbol Lbl'Unds'impliesBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %cimpliesBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.implies"), klabel{}("_impliesBool_"), left{}(Lbl'Unds'impliesBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1106,19,1106,153)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("=>"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List{}(SortKItem{}, SortList{}) : SortBool{} [format{}("%1 %cin%r %2"), function{}(), functional{}(), hook{}("LIST.in"), klabel{}("_inList_"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1012,19,1012,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(SortKItem{}, SortMap{}) : SortBool{} [format{}("%1 %cin_keys%r %c(%r %2 %c)%r"), function{}(), functional{}(), hook{}("MAP.in_keys"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(357,19,357,89)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("01101"), total{}()] - hooked-symbol Lbl'Unds'modInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %cmodInt%r %2"), function{}(), hook{}("INT.emod"), klabel{}("_modInt_"), left{}(Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1240,18,1240,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("mod"), symbol'Kywd'{}(), terminals{}("010")] - hooked-symbol Lbl'Unds'orBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %corBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.or"), klabel{}("_orBool_"), latex{}("{#1}\\vee_{\\scriptstyle\\it Bool}{#2}"), left{}(Lbl'Unds'orBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1104,19,1104,187)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("or"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'orElseBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %corElseBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.orElse"), klabel{}("_orElseBool_"), left{}(Lbl'Unds'orElseBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1105,19,1105,151)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("or"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'xorBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %cxorBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.xor"), klabel{}("_xorBool_"), left{}(Lbl'Unds'xorBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1103,19,1103,146)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("xor"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'Unds'xorInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %cxorInt%r %2"), function{}(), functional{}(), hook{}("INT.xor"), klabel{}("_xorInt_"), latex{}("{#1}\\mathrel{\\oplus_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'Unds'xorInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1250,18,1250,190)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPipe'Int'Unds'{}()), right{}(), smtlib{}("xorInt"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(SortKItem{}, SortKItem{}) : SortMap{} [format{}("%1 %c|->%r %2"), function{}(), functional{}(), hook{}("MAP.element"), injective{}(), klabel{}("_|->_"), latex{}("{#1}\\mapsto{#2}"), left{}(Lbl'UndsPipe'-'-GT-Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(257,18,257,151)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Stop'Map{}(),Lbl'Unds'Map'Unds'{}()), right{}(Lbl'UndsPipe'-'-GT-Unds'{}()), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'UndsPipe'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c|Int%r %2"), function{}(), functional{}(), hook{}("INT.or"), klabel{}("_|Int_"), latex{}("{#1}\\mathrel{|_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsPipe'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1252,18,1252,181)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("orInt"), symbol'Kywd'{}(), terminals{}("010"), total{}()] - hooked-symbol Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [comm{}(), format{}("%1 %c|Set%r %2"), function{}(), functional{}(), hook{}("SET.union"), left{}(Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(748,18,748,92)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010"), total{}()] - hooked-symbol LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%cabsInt%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("INT.abs"), klabel{}("absInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1269,18,1269,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("(ite (< #1 0) (- 0 #1) #1)"), terminals{}("1101"), total{}()] - symbol Lblbar{}(SortInt{}) : SortFoo{} [constructor{}(), format{}("%cbar%r %c(%r %1 %c)%r"), functional{}(), injective{}(), klabel{}("bar"), label{}("bar"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(5,18,5,47)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1101")] - hooked-symbol LblbitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [format{}("%cbitRangeInt%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}(), hook{}("INT.bitRange"), klabel{}("bitRangeInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1294,18,1294,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("11010101")] - hooked-symbol Lblchoice'LParUndsRParUnds'MAP'Unds'KItem'Unds'Map{}(SortMap{}) : SortKItem{} [format{}("%cchoice%r %c(%r %1 %c)%r"), function{}(), hook{}("MAP.choice"), klabel{}("Map:choice"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(393,20,393,101)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] - hooked-symbol Lblchoice'LParUndsRParUnds'SET'Unds'KItem'Unds'Set{}(SortSet{}) : SortKItem{} [format{}("%cchoice%r %c(%r %1 %c)%r"), function{}(), hook{}("SET.choice"), klabel{}("Set:choice"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(804,20,804,95)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] - symbol Lblf{}(SortFoo{}, SortFoo{}) : SortFoo{} [format{}("%cf%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), klabel{}("f"), label{}("f"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(7,18,7,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("110101")] - hooked-symbol LblfillList'LParUndsCommUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortInt{}, SortKItem{}) : SortList{} [format{}("%cfillList%r %c(%r %1 %c,%r %2 %c,%r %3 %c,%r %4 %c)%r"), function{}(), hook{}("LIST.fill"), klabel{}("fillList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(993,19,993,100)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101010101")] - symbol Lblfoo{}(SortInt{}) : SortFoo{} [constructor{}(), format{}("%cfoo%r %c(%r %1 %c)%r"), functional{}(), injective{}(), klabel{}("foo"), label{}("foo"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(4,18,4,47)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1101")] - symbol LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%cfreshInt%r %c(%r %1 %c)%r"), freshGenerator{}(), function{}(), functional{}(), klabel{}("freshInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1432,18,1432,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), private{}(), right{}(), terminals{}("1101"), total{}()] + symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [cell{}(), cellName{}("k"), constructor{}(), format{}("%c%r%i%n%1%d%n%c%r"), functional{}(), injective{}(), left{}(), maincell{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(535,17,535,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/kast.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), priorities{}(), right{}(), terminals{}("101")] + hooked-symbol LblList'Coln'get{}(SortList{}, SortInt{}) : SortKItem{} [format{}("%1 %c[%r %2 %c]%r"), function{}(), hook{}("LIST.get"), klabel{}("List:get"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(956,20,956,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("0101")] + hooked-symbol LblList'Coln'range{}(SortList{}, SortInt{}, SortInt{}) : SortList{} [format{}("%crange%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}(), hook{}("LIST.range"), klabel{}("List:range"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1003,19,1003,120)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("11010101")] + hooked-symbol LblListItem{}(SortKItem{}) : SortList{} [format{}("%cListItem%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("LIST.element"), klabel{}("ListItem"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(945,19,945,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_elem"), symbol'Kywd'{}(), terminals{}("1101"), total{}()] + hooked-symbol LblMap'Coln'lookup{}(SortMap{}, SortKItem{}) : SortKItem{} [format{}("%1 %c[%r %2 %c]%r"), function{}(), hook{}("MAP.lookup"), klabel{}("Map:lookup"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(271,20,271,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("0101")] + hooked-symbol LblMap'Coln'update{}(SortMap{}, SortKItem{}, SortKItem{}) : SortMap{} [format{}("%1 %c[%r %2 %c<-%r %3 %c]%r"), function{}(), functional{}(), hook{}("MAP.update"), klabel{}("Map:update"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(290,18,290,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), prefer{}(), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010101"), total{}()] + hooked-symbol LblSet'Coln'difference{}(SortSet{}, SortSet{}) : SortSet{} [format{}("%1 %c-Set%r %2"), function{}(), functional{}(), hook{}("SET.difference"), klabel{}("Set:difference"), latex{}("{#1}-_{\\it Set}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(769,18,769,142)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol LblSet'Coln'in{}(SortKItem{}, SortSet{}) : SortBool{} [format{}("%1 %cin%r %2"), function{}(), functional{}(), hook{}("SET.in"), klabel{}("Set:in"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(777,19,777,102)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol LblSetItem{}(SortKItem{}) : SortSet{} [format{}("%cSetItem%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("SET.element"), injective{}(), klabel{}("SetItem"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(737,18,737,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1101"), total{}()] + hooked-symbol Lbl'UndsPerc'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c%%Int%r %2"), function{}(), hook{}("INT.tmod"), klabel{}("_%Int_"), latex{}("{#1}\\mathrel{\\%_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsStar'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1237,18,1237,171)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("mod"), symbol'Kywd'{}(), terminals{}("010")] + hooked-symbol Lbl'UndsAnd-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c&Int%r %2"), function{}(), functional{}(), hook{}("INT.and"), klabel{}("_&Int_"), latex{}("{#1}\\mathrel{\\&_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsAnd-'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1248,18,1248,184)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smtlib{}("andInt"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'UndsStar'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c*Int%r %2"), function{}(), functional{}(), hook{}("INT.mul"), klabel{}("_*Int_"), latex{}("{#1}\\mathrel{\\ast_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'Unds'modInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsStar'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1233,18,1233,183)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("*"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'UndsPlus'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c+Int%r %2"), function{}(), functional{}(), hook{}("INT.add"), klabel{}("_+Int_"), latex{}("{#1}\\mathrel{+_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1242,18,1242,180)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smt-hook{}("+"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'-Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c-Int%r %2"), function{}(), functional{}(), hook{}("INT.sub"), klabel{}("_-Int_"), latex{}("{#1}\\mathrel{-_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1243,18,1243,174)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smt-hook{}("-"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [format{}("%1 %c-Map%r %2"), function{}(), functional{}(), hook{}("MAP.difference"), latex{}("{#1}-_{\\it Map}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(311,18,311,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'UndsSlsh'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c/Int%r %2"), function{}(), hook{}("INT.tdiv"), klabel{}("_/Int_"), latex{}("{#1}\\mathrel{\\div_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1236,18,1236,173)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("div"), symbol'Kywd'{}(), terminals{}("010")] + hooked-symbol Lbl'Unds-LT--LT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c<=Int%r %2"), function{}(), functional{}(), hook{}("INT.ge"), klabel{}("_>=Int_"), latex{}("{#1}\\mathrel{\\geq_{\\scriptstyle\\it Int}}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1306,19,1306,166)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}(">="), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds-GT--GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c>>Int%r %2"), function{}(), hook{}("INT.shr"), klabel{}("_>>Int_"), latex{}("{#1}\\mathrel{\\gg_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1245,18,1245,173)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}()), right{}(), smtlib{}("shrInt"), symbol'Kywd'{}(), terminals{}("010")] + hooked-symbol Lbl'Unds-GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortBool{} [format{}("%1 %c>Int%r %2"), function{}(), functional{}(), hook{}("INT.gt"), klabel{}("_>Int_"), latex{}("{#1}\\mathrel{>_{\\scriptstyle\\it Int}}{#2}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1307,19,1307,161)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}(">"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'List'Unds'{}(SortList{}, SortList{}) : SortList{} [assoc{}(), element{}(LblListItem{}()), format{}("%1%n%2"), function{}(), functional{}(), hook{}("LIST.concat"), klabel{}("_List_"), left{}(Lbl'Unds'List'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(929,19,929,188)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_concat"), symbol'Kywd'{}(), terminals{}("00"), total{}(), unit{}(Lbl'Stop'List{}())] + hooked-symbol Lbl'Unds'Map'Unds'{}(SortMap{}, SortMap{}) : SortMap{} [assoc{}(), comm{}(), element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), format{}("%1%n%2"), function{}(), hook{}("MAP.concat"), index{}("0"), klabel{}("_Map_"), left{}(Lbl'Unds'Map'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(240,18,240,173)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("00"), unit{}(Lbl'Stop'Map{}())] + hooked-symbol Lbl'Unds'Set'Unds'{}(SortSet{}, SortSet{}) : SortSet{} [assoc{}(), comm{}(), element{}(LblSetItem{}()), format{}("%1%n%2"), function{}(), hook{}("SET.concat"), idem{}(), klabel{}("_Set_"), left{}(Lbl'Unds'Set'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(721,18,721,165)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("00"), unit{}(Lbl'Stop'Set{}())] + hooked-symbol Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortKItem{}) : SortList{} [format{}("%1 %c[%r %2 %c<-%r %3 %c]%r"), function{}(), hook{}("LIST.update"), klabel{}("List:set"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(965,19,965,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010101")] + hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(SortMap{}, SortKItem{}) : SortMap{} [format{}("%1 %c[%r %2 %c<-%r %cundef%r %c]%r"), function{}(), functional{}(), hook{}("MAP.remove"), klabel{}("_[_<-undef]"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(299,18,299,117)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("010111"), total{}()] + hooked-symbol Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem{}(SortMap{}, SortKItem{}, SortKItem{}) : SortKItem{} [format{}("%1 %c[%r %2 %c]%r %corDefault%r %3"), function{}(), functional{}(), hook{}("MAP.lookupOrDefault"), klabel{}("Map:lookupOrDefault"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(281,20,281,134)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010110"), total{}()] + hooked-symbol Lbl'UndsXor-Perc'Int'UndsUnds'{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c^%%Int%r %2 %3"), function{}(), hook{}("INT.powmod"), klabel{}("_^%Int__"), left{}(Lbl'UndsXor-Perc'Int'UndsUnds'{}(),Lbl'UndsXor-'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1231,18,1231,139)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("(mod (^ #1 #2) #3)"), symbol'Kywd'{}(), terminals{}("0100")] + hooked-symbol Lbl'UndsXor-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %c^Int%r %2"), function{}(), hook{}("INT.pow"), klabel{}("_^Int_"), latex{}("{#1}\\mathrel{{\\char`\\^}_{\\!\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsXor-'Int'Unds'{}(),Lbl'UndsXor-Perc'Int'UndsUnds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1230,18,1230,178)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("^"), symbol'Kywd'{}(), terminals{}("010")] + hooked-symbol Lbl'Unds'andBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %candBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.and"), klabel{}("_andBool_"), latex{}("{#1}\\wedge_{\\scriptstyle\\it Bool}{#2}"), left{}(Lbl'Unds'andBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1101,19,1101,192)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("and"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'andThenBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %candThenBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.andThen"), klabel{}("_andThenBool_"), left{}(Lbl'Unds'andThenBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1102,19,1102,154)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("and"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'divInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %cdivInt%r %2"), function{}(), hook{}("INT.ediv"), klabel{}("_divInt_"), left{}(Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1239,18,1239,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("div"), symbol'Kywd'{}(), terminals{}("010")] + symbol Lbl'Unds'dividesInt'UndsUnds'INT-COMMON'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [format{}("%1 %cdividesInt%r %2"), function{}(), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1318,19,1318,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010")] + hooked-symbol Lbl'Unds'impliesBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %cimpliesBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.implies"), klabel{}("_impliesBool_"), left{}(Lbl'Unds'impliesBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1106,19,1106,153)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("=>"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List{}(SortKItem{}, SortList{}) : SortBool{} [format{}("%1 %cin%r %2"), function{}(), functional{}(), hook{}("LIST.in"), klabel{}("_inList_"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1012,19,1012,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(SortKItem{}, SortMap{}) : SortBool{} [format{}("%1 %cin_keys%r %c(%r %2 %c)%r"), function{}(), functional{}(), hook{}("MAP.in_keys"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(357,19,357,89)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("01101"), total{}()] + hooked-symbol Lbl'Unds'modInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%1 %cmodInt%r %2"), function{}(), hook{}("INT.emod"), klabel{}("_modInt_"), left{}(Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1240,18,1240,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smt-hook{}("mod"), symbol'Kywd'{}(), terminals{}("010")] + hooked-symbol Lbl'Unds'orBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %corBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.or"), klabel{}("_orBool_"), latex{}("{#1}\\vee_{\\scriptstyle\\it Bool}{#2}"), left{}(Lbl'Unds'orBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1104,19,1104,187)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("or"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'orElseBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %corElseBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.orElse"), klabel{}("_orElseBool_"), left{}(Lbl'Unds'orElseBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1105,19,1105,151)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("or"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'xorBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [format{}("%1 %cxorBool%r %2"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.xor"), klabel{}("_xorBool_"), left{}(Lbl'Unds'xorBool'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1103,19,1103,146)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}()), right{}(), smt-hook{}("xor"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'Unds'xorInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %cxorInt%r %2"), function{}(), functional{}(), hook{}("INT.xor"), klabel{}("_xorInt_"), latex{}("{#1}\\mathrel{\\oplus_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'Unds'xorInt'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1250,18,1250,190)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPipe'Int'Unds'{}()), right{}(), smtlib{}("xorInt"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(SortKItem{}, SortKItem{}) : SortMap{} [format{}("%1 %c|->%r %2"), function{}(), functional{}(), hook{}("MAP.element"), injective{}(), klabel{}("_|->_"), latex{}("{#1}\\mapsto{#2}"), left{}(Lbl'UndsPipe'-'-GT-Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(257,18,257,151)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Stop'Map{}(),Lbl'Unds'Map'Unds'{}()), right{}(Lbl'UndsPipe'-'-GT-Unds'{}()), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'UndsPipe'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [comm{}(), format{}("%1 %c|Int%r %2"), function{}(), functional{}(), hook{}("INT.or"), klabel{}("_|Int_"), latex{}("{#1}\\mathrel{|_{\\scriptstyle\\it Int}}{#2}"), left{}(Lbl'UndsPipe'Int'Unds'{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1252,18,1252,181)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("orInt"), symbol'Kywd'{}(), terminals{}("010"), total{}()] + hooked-symbol Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [comm{}(), format{}("%1 %c|Set%r %2"), function{}(), functional{}(), hook{}("SET.union"), left{}(Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}()), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(748,18,748,92)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("010"), total{}()] + hooked-symbol LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%cabsInt%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("INT.abs"), klabel{}("absInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1269,18,1269,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("(ite (< #1 0) (- 0 #1) #1)"), terminals{}("1101"), total{}()] + symbol Lblbar{}(SortInt{}) : SortFoo{} [constructor{}(), format{}("%cbar%r %c(%r %1 %c)%r"), functional{}(), injective{}(), klabel{}("bar"), label{}("bar"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,18,6,47)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1101")] + symbol Lblbaz{}() : SortInt{} [format{}("%cbaz%r %c(%r %c)%r"), function{}(), klabel{}("baz"), label{}("baz"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(11,18,11,54)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("111")] + hooked-symbol LblbitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [format{}("%cbitRangeInt%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}(), hook{}("INT.bitRange"), klabel{}("bitRangeInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1294,18,1294,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("11010101")] + hooked-symbol Lblchoice'LParUndsRParUnds'MAP'Unds'KItem'Unds'Map{}(SortMap{}) : SortKItem{} [format{}("%cchoice%r %c(%r %1 %c)%r"), function{}(), hook{}("MAP.choice"), klabel{}("Map:choice"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(393,20,393,101)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] + hooked-symbol Lblchoice'LParUndsRParUnds'SET'Unds'KItem'Unds'Set{}(SortSet{}) : SortKItem{} [format{}("%cchoice%r %c(%r %1 %c)%r"), function{}(), hook{}("SET.choice"), klabel{}("Set:choice"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(804,20,804,95)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] + symbol Lblf{}(SortFoo{}, SortFoo{}) : SortFoo{} [format{}("%cf%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), klabel{}("f"), label{}("f"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,18,8,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("110101")] + hooked-symbol LblfillList'LParUndsCommUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortInt{}, SortKItem{}) : SortList{} [format{}("%cfillList%r %c(%r %1 %c,%r %2 %c,%r %3 %c,%r %4 %c)%r"), function{}(), hook{}("LIST.fill"), klabel{}("fillList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(993,19,993,100)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101010101")] + symbol Lblfoo{}(SortInt{}) : SortFoo{} [constructor{}(), format{}("%cfoo%r %c(%r %1 %c)%r"), functional{}(), injective{}(), klabel{}("foo"), label{}("foo"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(5,18,5,47)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1101")] + symbol LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%cfreshInt%r %c(%r %1 %c)%r"), freshGenerator{}(), function{}(), functional{}(), klabel{}("freshInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1432,18,1432,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), private{}(), right{}(), terminals{}("1101"), total{}()] symbol LblgetGeneratedCounterCell{}(SortGeneratedTopCell{}) : SortGeneratedCounterCell{} [format{}("%cgetGeneratedCounterCell%r %c(%r %1 %c)%r"), function{}(), left{}(), priorities{}(), right{}(), terminals{}("1101")] symbol LblinitGeneratedCounterCell{}() : SortGeneratedCounterCell{} [format{}("%cinitGeneratedCounterCell%r"), function{}(), initializer{}(), left{}(), priorities{}(), right{}(), terminals{}("1")] symbol LblinitGeneratedTopCell{}(SortMap{}) : SortGeneratedTopCell{} [format{}("%cinitGeneratedTopCell%r %c(%r %1 %c)%r"), function{}(), initializer{}(), left{}(), priorities{}(), right{}(), terminals{}("1101")] symbol LblinitKCell{}(SortMap{}) : SortKCell{} [format{}("%cinitKCell%r %c(%r %1 %c)%r"), function{}(), initializer{}(), left{}(), priorities{}(), right{}(), terminals{}("1101")] - hooked-symbol LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [comm{}(), format{}("%cintersectSet%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("SET.intersection"), klabel{}("intersectSet"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(759,18,759,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), total{}()] + hooked-symbol LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [comm{}(), format{}("%cintersectSet%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("SET.intersection"), klabel{}("intersectSet"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(759,18,759,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), total{}()] symbol LblisBool{}(SortK{}) : SortBool{} [format{}("%cisBool%r %c(%r %1 %c)%r"), function{}(), functional{}(), left{}(), predicate{}("Bool"), priorities{}(), right{}(), terminals{}("1101"), total{}()] symbol LblisFoo{}(SortK{}) : SortBool{} [format{}("%cisFoo%r %c(%r %1 %c)%r"), function{}(), functional{}(), left{}(), predicate{}("Foo"), priorities{}(), right{}(), terminals{}("1101"), total{}()] symbol LblisGeneratedCounterCell{}(SortK{}) : SortBool{} [format{}("%cisGeneratedCounterCell%r %c(%r %1 %c)%r"), function{}(), functional{}(), left{}(), predicate{}("GeneratedCounterCell"), priorities{}(), right{}(), terminals{}("1101"), total{}()] @@ -172,15 +173,15 @@ module EVALUATE symbol LblisList{}(SortK{}) : SortBool{} [format{}("%cisList%r %c(%r %1 %c)%r"), function{}(), functional{}(), left{}(), predicate{}("List"), priorities{}(), right{}(), terminals{}("1101"), total{}()] symbol LblisMap{}(SortK{}) : SortBool{} [format{}("%cisMap%r %c(%r %1 %c)%r"), function{}(), functional{}(), left{}(), predicate{}("Map"), priorities{}(), right{}(), terminals{}("1101"), total{}()] symbol LblisSet{}(SortK{}) : SortBool{} [format{}("%cisSet%r %c(%r %1 %c)%r"), function{}(), functional{}(), left{}(), predicate{}("Set"), priorities{}(), right{}(), terminals{}("1101"), total{}()] - hooked-symbol Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(SortMap{}) : SortSet{} [format{}("%ckeys%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("MAP.keys"), klabel{}("keys"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(341,18,341,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), total{}()] - hooked-symbol Lblkeys'Unds'list'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [format{}("%ckeys_list%r %c(%r %1 %c)%r"), function{}(), hook{}("MAP.keys_list"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(349,19,349,80)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] - hooked-symbol Lbllog2Int'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%clog2Int%r %c(%r %1 %c)%r"), function{}(), hook{}("INT.log2"), klabel{}("log2Int"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1280,18,1280,75)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] - hooked-symbol LblmakeList'LParUndsCommUndsRParUnds'LIST'Unds'List'Unds'Int'Unds'KItem{}(SortInt{}, SortKItem{}) : SortList{} [format{}("%cmakeList%r %c(... %r length: %1 %c,%r value: %2 %c)%r"), function{}(), hook{}("LIST.make"), klabel{}("makeList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(974,19,974,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101")] - hooked-symbol LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%cmaxInt%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("INT.max"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1261,18,1261,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("(ite (< #1 #2) #2 #1)"), terminals{}("110101"), total{}()] - hooked-symbol LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%cminInt%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("INT.min"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1260,18,1260,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("(ite (< #1 #2) #1 #2)"), terminals{}("110101"), total{}()] + hooked-symbol Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(SortMap{}) : SortSet{} [format{}("%ckeys%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("MAP.keys"), klabel{}("keys"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(341,18,341,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), total{}()] + hooked-symbol Lblkeys'Unds'list'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [format{}("%ckeys_list%r %c(%r %1 %c)%r"), function{}(), hook{}("MAP.keys_list"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(349,19,349,80)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] + hooked-symbol Lbllog2Int'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%clog2Int%r %c(%r %1 %c)%r"), function{}(), hook{}("INT.log2"), klabel{}("log2Int"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1280,18,1280,75)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] + hooked-symbol LblmakeList'LParUndsCommUndsRParUnds'LIST'Unds'List'Unds'Int'Unds'KItem{}(SortInt{}, SortKItem{}) : SortList{} [format{}("%cmakeList%r %c(... %r length: %1 %c,%r value: %2 %c)%r"), function{}(), hook{}("LIST.make"), klabel{}("makeList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(974,19,974,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101")] + hooked-symbol LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%cmaxInt%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("INT.max"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1261,18,1261,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("(ite (< #1 #2) #2 #1)"), terminals{}("110101"), total{}()] + hooked-symbol LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [format{}("%cminInt%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("INT.min"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1260,18,1260,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smt-hook{}("(ite (< #1 #2) #1 #2)"), terminals{}("110101"), total{}()] symbol LblnoGeneratedCounterCell{}() : SortGeneratedCounterCellOpt{} [cellOptAbsent{}("GeneratedCounterCell"), constructor{}(), format{}("%cnoGeneratedCounterCell%r"), functional{}(), injective{}(), left{}(), priorities{}(), right{}(), terminals{}("1")] symbol LblnoKCell{}() : SortKCellOpt{} [cellOptAbsent{}("KCell"), constructor{}(), format{}("%cnoKCell%r"), functional{}(), injective{}(), left{}(), priorities{}(), right{}(), terminals{}("1")] - hooked-symbol LblnotBool'Unds'{}(SortBool{}) : SortBool{} [format{}("%cnotBool%r %1"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.not"), klabel{}("notBool_"), latex{}("\\neg_{\\scriptstyle\\it Bool}{#1}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1100,19,1100,179)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds'orElseBool'Unds'{}(),Lbl'Unds'orBool'Unds'{}(),Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'Unds'andThenBool'Unds'{}(),Lbl'Unds'impliesBool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}(),Lbl'Unds'andBool'Unds'{}(),Lbl'Unds'xorBool'Unds'{}()), right{}(), smt-hook{}("not"), symbol'Kywd'{}(), terminals{}("10"), total{}()] + hooked-symbol LblnotBool'Unds'{}(SortBool{}) : SortBool{} [format{}("%cnotBool%r %1"), function{}(), functional{}(), group{}("boolOperation"), hook{}("BOOL.not"), klabel{}("notBool_"), latex{}("\\neg_{\\scriptstyle\\it Bool}{#1}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1100,19,1100,179)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'Unds'orElseBool'Unds'{}(),Lbl'Unds'orBool'Unds'{}(),Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(),Lbl'Unds'andThenBool'Unds'{}(),Lbl'Unds'impliesBool'Unds'{}(),Lbl'UndsEqlsEqls'Bool'Unds'{}(),Lbl'Unds'andBool'Unds'{}(),Lbl'Unds'xorBool'Unds'{}()), right{}(), smt-hook{}("not"), symbol'Kywd'{}(), terminals{}("10"), total{}()] symbol Lblproject'Coln'Bool{}(SortK{}) : SortBool{} [format{}("%cproject:Bool%r %c(%r %1 %c)%r"), function{}(), left{}(), priorities{}(), projection{}(), right{}(), terminals{}("1101")] symbol Lblproject'Coln'Foo{}(SortK{}) : SortFoo{} [format{}("%cproject:Foo%r %c(%r %1 %c)%r"), function{}(), left{}(), priorities{}(), projection{}(), right{}(), terminals{}("1101")] symbol Lblproject'Coln'GeneratedCounterCell{}(SortK{}) : SortGeneratedCounterCell{} [format{}("%cproject:GeneratedCounterCell%r %c(%r %1 %c)%r"), function{}(), left{}(), priorities{}(), projection{}(), right{}(), terminals{}("1101")] @@ -195,17 +196,18 @@ module EVALUATE symbol Lblproject'Coln'List{}(SortK{}) : SortList{} [format{}("%cproject:List%r %c(%r %1 %c)%r"), function{}(), left{}(), priorities{}(), projection{}(), right{}(), terminals{}("1101")] symbol Lblproject'Coln'Map{}(SortK{}) : SortMap{} [format{}("%cproject:Map%r %c(%r %1 %c)%r"), function{}(), left{}(), priorities{}(), projection{}(), right{}(), terminals{}("1101")] symbol Lblproject'Coln'Set{}(SortK{}) : SortSet{} [format{}("%cproject:Set%r %c(%r %1 %c)%r"), function{}(), left{}(), priorities{}(), projection{}(), right{}(), terminals{}("1101")] - hooked-symbol LblrandInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%crandInt%r %c(%r %1 %c)%r"), function{}(), hook{}("INT.rand"), impure{}(), klabel{}("randInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1328,18,1328,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] - hooked-symbol LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(SortMap{}, SortSet{}) : SortMap{} [format{}("%cremoveAll%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("MAP.removeAll"), klabel{}("removeAll"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(333,18,333,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), total{}()] - hooked-symbol LblsignExtendBitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [format{}("%csignExtendBitRangeInt%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}(), hook{}("INT.signExtendBitRange"), klabel{}("signExtendBitRangeInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1295,18,1295,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("11010101")] - hooked-symbol Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}(SortList{}) : SortInt{} [format{}("%csize%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("LIST.size"), klabel{}("sizeList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1020,18,1020,117)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_len"), terminals{}("1101"), total{}()] - hooked-symbol Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map{}(SortMap{}) : SortInt{} [format{}("%csize%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("MAP.size"), klabel{}("sizeMap"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(373,18,373,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), total{}()] - hooked-symbol Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(SortSet{}) : SortInt{} [format{}("%csize%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("SET.size"), klabel{}("size"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(794,18,794,76)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), total{}()] - hooked-symbol LblsrandInt'LParUndsRParUnds'INT-COMMON'Unds'K'Unds'Int{}(SortInt{}) : SortK{} [format{}("%csrandInt%r %c(%r %1 %c)%r"), function{}(), hook{}("INT.srand"), impure{}(), klabel{}("srandInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1329,16,1329,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] - hooked-symbol LblupdateList'LParUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'List{}(SortList{}, SortInt{}, SortList{}) : SortList{} [format{}("%cupdateList%r %c(... %r dest: %1 %c,%r index: %2 %c,%r src: %3 %c)%r"), function{}(), hook{}("LIST.updateAll"), klabel{}("updateList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(984,19,984,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("11010101")] - hooked-symbol LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [format{}("%cupdateMap%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("MAP.updateAll"), klabel{}("updateMap"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(324,18,324,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), total{}()] - hooked-symbol Lblvalues'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [format{}("%cvalues%r %c(%r %1 %c)%r"), function{}(), hook{}("MAP.values"), klabel{}("values"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(365,19,365,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] - hooked-symbol Lbl'Tild'Int'Unds'{}(SortInt{}) : SortInt{} [format{}("%c~Int%r %1"), function{}(), functional{}(), hook{}("INT.not"), klabel{}("~Int_"), latex{}("\\mathop{\\sim_{\\scriptstyle\\it Int}}{#1}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1228,18,1228,168)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'UndsXor-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'UndsXor-Perc'Int'UndsUnds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smtlib{}("notInt"), symbol'Kywd'{}(), terminals{}("10"), total{}()] + symbol Lblqux{}(SortInt{}) : SortBool{} [format{}("%cqux%r %c(%r %1 %c)%r"), function{}(), klabel{}("qux"), label{}("qux"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(12,19,12,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), priorities{}(), right{}(), symbol'Kywd'{}(), terminals{}("1101")] + hooked-symbol LblrandInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [format{}("%crandInt%r %c(%r %1 %c)%r"), function{}(), hook{}("INT.rand"), impure{}(), klabel{}("randInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1328,18,1328,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] + hooked-symbol LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(SortMap{}, SortSet{}) : SortMap{} [format{}("%cremoveAll%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("MAP.removeAll"), klabel{}("removeAll"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(333,18,333,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), total{}()] + hooked-symbol LblsignExtendBitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [format{}("%csignExtendBitRangeInt%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), function{}(), hook{}("INT.signExtendBitRange"), klabel{}("signExtendBitRangeInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1295,18,1295,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("11010101")] + hooked-symbol Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}(SortList{}) : SortInt{} [format{}("%csize%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("LIST.size"), klabel{}("sizeList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1020,18,1020,117)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), smtlib{}("smt_seq_len"), terminals{}("1101"), total{}()] + hooked-symbol Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map{}(SortMap{}) : SortInt{} [format{}("%csize%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("MAP.size"), klabel{}("sizeMap"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(373,18,373,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), total{}()] + hooked-symbol Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(SortSet{}) : SortInt{} [format{}("%csize%r %c(%r %1 %c)%r"), function{}(), functional{}(), hook{}("SET.size"), klabel{}("size"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(794,18,794,76)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), total{}()] + hooked-symbol LblsrandInt'LParUndsRParUnds'INT-COMMON'Unds'K'Unds'Int{}(SortInt{}) : SortK{} [format{}("%csrandInt%r %c(%r %1 %c)%r"), function{}(), hook{}("INT.srand"), impure{}(), klabel{}("srandInt"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1329,16,1329,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] + hooked-symbol LblupdateList'LParUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'List{}(SortList{}, SortInt{}, SortList{}) : SortList{} [format{}("%cupdateList%r %c(... %r dest: %1 %c,%r index: %2 %c,%r src: %3 %c)%r"), function{}(), hook{}("LIST.updateAll"), klabel{}("updateList"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(984,19,984,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("11010101")] + hooked-symbol LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [format{}("%cupdateMap%r %c(%r %1 %c,%r %2 %c)%r"), function{}(), functional{}(), hook{}("MAP.updateAll"), klabel{}("updateMap"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(324,18,324,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), total{}()] + hooked-symbol Lblvalues'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [format{}("%cvalues%r %c(%r %1 %c)%r"), function{}(), hook{}("MAP.values"), klabel{}("values"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(365,19,365,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101")] + hooked-symbol Lbl'Tild'Int'Unds'{}(SortInt{}) : SortInt{} [format{}("%c~Int%r %1"), function{}(), functional{}(), hook{}("INT.not"), klabel{}("~Int_"), latex{}("\\mathop{\\sim_{\\scriptstyle\\it Int}}{#1}"), left{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1228,18,1228,168)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), priorities{}(Lbl'UndsPlus'Int'Unds'{}(),Lbl'Unds'divInt'Unds'{}(),Lbl'UndsPerc'Int'Unds'{}(),Lbl'Unds-GT--GT-'Int'Unds'{}(),Lbl'Unds'xorInt'Unds'{}(),Lbl'UndsSlsh'Int'Unds'{}(),Lbl'UndsAnd-'Int'Unds'{}(),Lbl'UndsXor-'Int'Unds'{}(),Lbl'Unds-LT--LT-'Int'Unds'{}(),Lbl'UndsStar'Int'Unds'{}(),Lbl'UndsPipe'Int'Unds'{}(),Lbl'Unds'modInt'Unds'{}(),Lbl'UndsXor-Perc'Int'UndsUnds'{}(),Lbl'Unds'-Int'Unds'{}()), right{}(), smtlib{}("notInt"), symbol'Kywd'{}(), terminals{}("10"), total{}()] // generated axioms axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKCellOpt{}, SortKItem{}} (From:SortKCellOpt{}))) [subsort{SortKCellOpt{}, SortKItem{}}()] // subsort @@ -330,7 +332,7 @@ module EVALUATE axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortGeneratedCounterCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortGeneratedCounterCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk // rules -// rule `#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort`{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(2b32069ac3f589174502fa507ebc88fab7c902854c0a9baa8ab09beb551232e2), org.kframework.attributes.Location(Location(2304,8,2304,59)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] +// rule `#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort`{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(2b32069ac3f589174502fa507ebc88fab7c902854c0a9baa8ab09beb551232e2), org.kframework.attributes.Location(Location(2304,8,2304,59)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -356,9 +358,9 @@ module EVALUATE \and{SortK{}} ( VarB1:SortK{}, \top{SortK{}}()))) - [UNIQUE'Unds'ID{}("2b32069ac3f589174502fa507ebc88fab7c902854c0a9baa8ab09beb551232e2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2304,8,2304,59)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] + [UNIQUE'Unds'ID{}("2b32069ac3f589174502fa507ebc88fab7c902854c0a9baa8ab09beb551232e2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2304,8,2304,59)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] -// rule `#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort`{K}(C,_Gen0,B2)=>B2 requires `notBool_`(C) ensures #token("true","Bool") [UNIQUE_ID(651bff3fa53d464ac7dd7aa77e1ef6071e14c959eb6df97baa325e2ad300daaa), org.kframework.attributes.Location(Location(2305,8,2305,67)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] +// rule `#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort`{K}(C,_Gen0,B2)=>B2 requires `notBool_`(C) ensures #token("true","Bool") [UNIQUE_ID(651bff3fa53d464ac7dd7aa77e1ef6071e14c959eb6df97baa325e2ad300daaa), org.kframework.attributes.Location(Location(2305,8,2305,67)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -384,9 +386,9 @@ module EVALUATE \and{SortK{}} ( VarB2:SortK{}, \top{SortK{}}()))) - [UNIQUE'Unds'ID{}("651bff3fa53d464ac7dd7aa77e1ef6071e14c959eb6df97baa325e2ad300daaa"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2305,8,2305,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] + [UNIQUE'Unds'ID{}("651bff3fa53d464ac7dd7aa77e1ef6071e14c959eb6df97baa325e2ad300daaa"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2305,8,2305,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] -// rule `_=/=Bool_`(B1,B2)=>`notBool_`(`_==Bool_`(B1,B2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f), org.kframework.attributes.Location(Location(1150,8,1150,57)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_=/=Bool_`(B1,B2)=>`notBool_`(`_==Bool_`(B1,B2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f), org.kframework.attributes.Location(Location(1150,8,1150,57)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -406,9 +408,9 @@ module EVALUATE \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(1150,8,1150,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1150,8,1150,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_=/=Int_`(I1,I2)=>`notBool_`(`_==Int_`(I1,I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3), org.kframework.attributes.Location(Location(1429,8,1429,53)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_=/=Int_`(I1,I2)=>`notBool_`(`_==Int_`(I1,I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3), org.kframework.attributes.Location(Location(1429,8,1429,53)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -428,9 +430,9 @@ module EVALUATE \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(1429,8,1429,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1429,8,1429,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_=/=K_`(K1,K2)=>`notBool_`(`_==K_`(K1,K2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c), org.kframework.attributes.Location(Location(2302,8,2302,45)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_=/=K_`(K1,K2)=>`notBool_`(`_==K_`(K1,K2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c), org.kframework.attributes.Location(Location(2302,8,2302,45)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -450,9 +452,9 @@ module EVALUATE \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(2302,8,2302,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2302,8,2302,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// 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(1123,8,1123,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// 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(1123,8,1123,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -472,9 +474,9 @@ module EVALUATE \and{SortBool{}} ( Var'Unds'Gen1:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1123,8,1123,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1123,8,1123,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_andBool_`(B,#token("true","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e8d4ca75a690151f99f8904b068db555782f5599b11230a9d0b97a71afb6fc98), org.kframework.attributes.Location(Location(1122,8,1122,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_andBool_`(B,#token("true","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e8d4ca75a690151f99f8904b068db555782f5599b11230a9d0b97a71afb6fc98), org.kframework.attributes.Location(Location(1122,8,1122,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -482,9 +484,9 @@ module EVALUATE \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("e8d4ca75a690151f99f8904b068db555782f5599b11230a9d0b97a71afb6fc98"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1122,8,1122,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("e8d4ca75a690151f99f8904b068db555782f5599b11230a9d0b97a71afb6fc98"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1122,8,1122,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_andBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9c183fae7de06f560180386d14d29c609cadf0c98266ce2adbecb50100a1daca), org.kframework.attributes.Location(Location(1124,8,1124,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_andBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9c183fae7de06f560180386d14d29c609cadf0c98266ce2adbecb50100a1daca), org.kframework.attributes.Location(Location(1124,8,1124,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -492,9 +494,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("9c183fae7de06f560180386d14d29c609cadf0c98266ce2adbecb50100a1daca"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1124,8,1124,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("9c183fae7de06f560180386d14d29c609cadf0c98266ce2adbecb50100a1daca"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1124,8,1124,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_andBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f), org.kframework.attributes.Location(Location(1121,8,1121,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_andBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f), org.kframework.attributes.Location(Location(1121,8,1121,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -514,9 +516,9 @@ module EVALUATE \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1121,8,1121,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1121,8,1121,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// 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(1128,8,1128,36)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// 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(1128,8,1128,36)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -536,9 +538,9 @@ module EVALUATE \and{SortBool{}} ( Var'Unds'Gen1:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1128,8,1128,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1128,8,1128,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_andThenBool_`(K,#token("true","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(82ac30b094be9b12206773d87b60274e929a41ca595f4674be1d37eeff873d7c), org.kframework.attributes.Location(Location(1127,8,1127,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_andThenBool_`(K,#token("true","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(82ac30b094be9b12206773d87b60274e929a41ca595f4674be1d37eeff873d7c), org.kframework.attributes.Location(Location(1127,8,1127,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -546,9 +548,9 @@ module EVALUATE \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("82ac30b094be9b12206773d87b60274e929a41ca595f4674be1d37eeff873d7c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1127,8,1127,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("82ac30b094be9b12206773d87b60274e929a41ca595f4674be1d37eeff873d7c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1127,8,1127,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_andThenBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(0508592878b546cbc6eeda6ec7b322584eea5c6d6eea3f72be8418fe4f7149b2), org.kframework.attributes.Location(Location(1129,8,1129,36)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_andThenBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(0508592878b546cbc6eeda6ec7b322584eea5c6d6eea3f72be8418fe4f7149b2), org.kframework.attributes.Location(Location(1129,8,1129,36)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -556,9 +558,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("0508592878b546cbc6eeda6ec7b322584eea5c6d6eea3f72be8418fe4f7149b2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1129,8,1129,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("0508592878b546cbc6eeda6ec7b322584eea5c6d6eea3f72be8418fe4f7149b2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1129,8,1129,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_andThenBool_`(#token("true","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689), org.kframework.attributes.Location(Location(1126,8,1126,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_andThenBool_`(#token("true","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689), org.kframework.attributes.Location(Location(1126,8,1126,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -578,9 +580,9 @@ module EVALUATE \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1126,8,1126,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1126,8,1126,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// 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(1418,8,1419,23)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] +// 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(1418,8,1419,23)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -602,9 +604,9 @@ module EVALUATE \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(1418,8,1419,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] + [UNIQUE'Unds'ID{}("83dcf9bc8c69f131715bc7a92d06c99b9a2b5f4c4fdafb69e6fdb2f1822712d4"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1418,8,1419,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] -// 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(1430,8,1430,58)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// 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(1430,8,1430,58)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -624,9 +626,9 @@ module EVALUATE \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(1430,8,1430,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("fd8facae0061fe5bc5c406f7ad2ed5d8d21960bf1118c9b240451253064dadb5"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1430,8,1430,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_impliesBool_`(B,#token("false","Bool"))=>`notBool_`(B) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(022c562a21d72cedfb795607d2249b8ad14b66399b720b3b2f4a05a1da08df96), org.kframework.attributes.Location(Location(1148,8,1148,45)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_impliesBool_`(B,#token("false","Bool"))=>`notBool_`(B) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(022c562a21d72cedfb795607d2249b8ad14b66399b720b3b2f4a05a1da08df96), org.kframework.attributes.Location(Location(1148,8,1148,45)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -634,9 +636,9 @@ module EVALUATE \and{SortBool{}} ( LblnotBool'Unds'{}(VarB:SortBool{}), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("022c562a21d72cedfb795607d2249b8ad14b66399b720b3b2f4a05a1da08df96"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1148,8,1148,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("022c562a21d72cedfb795607d2249b8ad14b66399b720b3b2f4a05a1da08df96"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1148,8,1148,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_impliesBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(99ba64afc26a739953df142ccd4b486bba68107fce8c9aa356d40afa7a988712), org.kframework.attributes.Location(Location(1147,8,1147,39)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_impliesBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(99ba64afc26a739953df142ccd4b486bba68107fce8c9aa356d40afa7a988712), org.kframework.attributes.Location(Location(1147,8,1147,39)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -644,9 +646,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("99ba64afc26a739953df142ccd4b486bba68107fce8c9aa356d40afa7a988712"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1147,8,1147,39)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("99ba64afc26a739953df142ccd4b486bba68107fce8c9aa356d40afa7a988712"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1147,8,1147,39)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), 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(1146,8,1146,40)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// 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(1146,8,1146,40)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -666,9 +668,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1146,8,1146,40)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1146,8,1146,40)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_impliesBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d), org.kframework.attributes.Location(Location(1145,8,1145,36)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_impliesBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d), org.kframework.attributes.Location(Location(1145,8,1145,36)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -688,9 +690,9 @@ module EVALUATE \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1145,8,1145,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1145,8,1145,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// 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(adfacb58b0678a49f66186954229939a953c9849d5b08edc8f887c0d7514b2c6), concrete, org.kframework.attributes.Location(Location(1421,5,1424,23)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol]), 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(adfacb58b0678a49f66186954229939a953c9849d5b08edc8f887c0d7514b2c6), concrete, org.kframework.attributes.Location(Location(1421,5,1424,23)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol]), simplification] axiom{R} \implies{R} ( \equals{SortBool{},R}( Lbl'UndsEqlsSlshEqls'Int'Unds'{}(VarI2:SortInt{},\dv{SortInt{}}("0")), @@ -700,9 +702,9 @@ module EVALUATE \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{}("adfacb58b0678a49f66186954229939a953c9849d5b08edc8f887c0d7514b2c6"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1421,5,1424,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("adfacb58b0678a49f66186954229939a953c9849d5b08edc8f887c0d7514b2c6"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1421,5,1424,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]"), simplification{}()] -// rule `_orBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d7245713da157cf997438091f92bb78eb51a6cefa568bb0d30560ce08d647f26), org.kframework.attributes.Location(Location(1138,8,1138,32)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_orBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d7245713da157cf997438091f92bb78eb51a6cefa568bb0d30560ce08d647f26), org.kframework.attributes.Location(Location(1138,8,1138,32)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -710,9 +712,9 @@ module EVALUATE \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("d7245713da157cf997438091f92bb78eb51a6cefa568bb0d30560ce08d647f26"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1138,8,1138,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("d7245713da157cf997438091f92bb78eb51a6cefa568bb0d30560ce08d647f26"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1138,8,1138,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_orBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(47860d52c18a441b229449cd89d5464256137dc32deb5551effbac0482c883f3), org.kframework.attributes.Location(Location(1136,8,1136,34)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_orBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(47860d52c18a441b229449cd89d5464256137dc32deb5551effbac0482c883f3), org.kframework.attributes.Location(Location(1136,8,1136,34)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -720,9 +722,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("47860d52c18a441b229449cd89d5464256137dc32deb5551effbac0482c883f3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1136,8,1136,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("47860d52c18a441b229449cd89d5464256137dc32deb5551effbac0482c883f3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1136,8,1136,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_orBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b), org.kframework.attributes.Location(Location(1137,8,1137,32)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_orBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b), org.kframework.attributes.Location(Location(1137,8,1137,32)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -742,9 +744,9 @@ module EVALUATE \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1137,8,1137,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1137,8,1137,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// 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(1135,8,1135,34)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// 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(1135,8,1135,34)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -764,9 +766,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1135,8,1135,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1135,8,1135,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_orElseBool_`(K,#token("false","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(684b0444a1f711d49ff1502423a3346fb26958697423db488b05d25081fc0480), org.kframework.attributes.Location(Location(1143,8,1143,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_orElseBool_`(K,#token("false","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(684b0444a1f711d49ff1502423a3346fb26958697423db488b05d25081fc0480), org.kframework.attributes.Location(Location(1143,8,1143,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -774,9 +776,9 @@ module EVALUATE \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("684b0444a1f711d49ff1502423a3346fb26958697423db488b05d25081fc0480"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1143,8,1143,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("684b0444a1f711d49ff1502423a3346fb26958697423db488b05d25081fc0480"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1143,8,1143,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_orElseBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(c9eccff94ecf6e810c600d4536bf1701485c13c3456c6b98c0cdab0fe7c5af14), org.kframework.attributes.Location(Location(1141,8,1141,33)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_orElseBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(c9eccff94ecf6e810c600d4536bf1701485c13c3456c6b98c0cdab0fe7c5af14), org.kframework.attributes.Location(Location(1141,8,1141,33)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -784,9 +786,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("c9eccff94ecf6e810c600d4536bf1701485c13c3456c6b98c0cdab0fe7c5af14"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1141,8,1141,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("c9eccff94ecf6e810c600d4536bf1701485c13c3456c6b98c0cdab0fe7c5af14"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1141,8,1141,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_orElseBool_`(#token("false","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf), org.kframework.attributes.Location(Location(1142,8,1142,37)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_orElseBool_`(#token("false","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf), org.kframework.attributes.Location(Location(1142,8,1142,37)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -806,9 +808,9 @@ module EVALUATE \and{SortBool{}} ( VarK:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1142,8,1142,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1142,8,1142,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// 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(1140,8,1140,33)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// 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(1140,8,1140,33)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -828,9 +830,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1140,8,1140,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1140,8,1140,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_xorBool_`(B,B)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f), org.kframework.attributes.Location(Location(1133,8,1133,38)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_xorBool_`(B,B)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f), org.kframework.attributes.Location(Location(1133,8,1133,38)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -850,9 +852,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1133,8,1133,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1133,8,1133,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_xorBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7a2851f9d4ea4bd3f35070ee029fc3bdca36e361f7ee54addeff9d10ddeb7c75), org.kframework.attributes.Location(Location(1132,8,1132,38)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] +// rule `_xorBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7a2851f9d4ea4bd3f35070ee029fc3bdca36e361f7ee54addeff9d10ddeb7c75), org.kframework.attributes.Location(Location(1132,8,1132,38)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] axiom{R} \implies{R} ( \top{R}(), \equals{SortBool{},R} ( @@ -860,9 +862,9 @@ module EVALUATE \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("7a2851f9d4ea4bd3f35070ee029fc3bdca36e361f7ee54addeff9d10ddeb7c75"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1132,8,1132,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] + [UNIQUE'Unds'ID{}("7a2851f9d4ea4bd3f35070ee029fc3bdca36e361f7ee54addeff9d10ddeb7c75"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1132,8,1132,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), simplification{}()] -// rule `_xorBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf), org.kframework.attributes.Location(Location(1131,8,1131,38)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_xorBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf), org.kframework.attributes.Location(Location(1131,8,1131,38)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -882,9 +884,9 @@ module EVALUATE \and{SortBool{}} ( VarB:SortBool{}, \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1131,8,1131,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1131,8,1131,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `_|Set__SET_Set_Set_Set`(S1,S2)=>`_Set_`(S1,`Set:difference`(S2,S1)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e9a710d8d1ca5c799420161879cbbff926de45a5bddd820d646f51d43eb67e62), concrete, org.kframework.attributes.Location(Location(749,8,749,45)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `_|Set__SET_Set_Set_Set`(S1,S2)=>`_Set_`(S1,`Set:difference`(S2,S1)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e9a710d8d1ca5c799420161879cbbff926de45a5bddd820d646f51d43eb67e62), concrete, org.kframework.attributes.Location(Location(749,8,749,45)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -904,9 +906,23 @@ module EVALUATE \and{SortSet{}} ( Lbl'Unds'Set'Unds'{}(VarS1:SortSet{},LblSet'Coln'difference{}(VarS2:SortSet{},VarS1:SortSet{})), \top{SortSet{}}()))) - [UNIQUE'Unds'ID{}("e9a710d8d1ca5c799420161879cbbff926de45a5bddd820d646f51d43eb67e62"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(749,8,749,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("e9a710d8d1ca5c799420161879cbbff926de45a5bddd820d646f51d43eb67e62"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(749,8,749,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN)=>`_modInt_`(`_>>Int_`(I,IDX),`_<#token("78","Int") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(32821e175e0297326fd933c8aee0e9b427f8ad86e60ab28b24ae0b3bf5e30814), org.kframework.attributes.Location(Location(14,8,14,19)), org.kframework.attributes.Source(Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortInt{},R} ( + Lblbaz{}(), + \and{SortInt{}} ( + \dv{SortInt{}}("78"), + \top{SortInt{}}()))) + [UNIQUE'Unds'ID{}("32821e175e0297326fd933c8aee0e9b427f8ad86e60ab28b24ae0b3bf5e30814"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(14,8,14,19)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + +// rule `bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN)=>`_modInt_`(`_>>Int_`(I,IDX),`_<foo(`_+Int_`(A,B)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(1aa48edc07745c1c026ba564bb2c869de998868ddda8de280e3dcdbfe89d85f0), org.kframework.attributes.Location(Location(8,8,8,42)), org.kframework.attributes.Source(Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule f(foo(A),bar(B))=>foo(`_+Int_`(A,B)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(1aa48edc07745c1c026ba564bb2c869de998868ddda8de280e3dcdbfe89d85f0), org.kframework.attributes.Location(Location(9,8,9,42)), org.kframework.attributes.Source(Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -952,9 +968,9 @@ module EVALUATE \and{SortFoo{}} ( Lblfoo{}(Lbl'UndsPlus'Int'Unds'{}(VarA:SortInt{},VarB:SortInt{})), \top{SortFoo{}}()))) - [UNIQUE'Unds'ID{}("1aa48edc07745c1c026ba564bb2c869de998868ddda8de280e3dcdbfe89d85f0"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,8,8,42)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("1aa48edc07745c1c026ba564bb2c869de998868ddda8de280e3dcdbfe89d85f0"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(9,8,9,42)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `freshInt(_)_INT_Int_Int`(I)=>I requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b), org.kframework.attributes.Location(Location(1433,8,1433,28)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `freshInt(_)_INT_Int_Int`(I)=>I requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b), org.kframework.attributes.Location(Location(1433,8,1433,28)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -970,7 +986,7 @@ module EVALUATE \and{SortInt{}} ( VarI:SortInt{}, \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1433,8,1433,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1433,8,1433,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] // rule getGeneratedCounterCell(``(_DotVar0,Cell))=>Cell requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9ef5eb9b9e6bbd7436911fad20615821f61e06e742dd27773001ab0664bd1de3)] axiom{R} \implies{R} ( @@ -1045,13 +1061,13 @@ module EVALUATE \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:SortBool{}, + \exists{R} (Var'Unds'Gen0:SortBool{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortBool{}, SortKItem{}}(Var'Unds'Gen1:SortBool{}),dotk{}()) + kseq{}(inj{SortBool{}, SortKItem{}}(Var'Unds'Gen0:SortBool{}),dotk{}()) ), \top{R} () ) @@ -1153,13 +1169,13 @@ module EVALUATE \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:SortGeneratedCounterCell{}, + \exists{R} (Var'Unds'Gen0:SortGeneratedCounterCell{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(Var'Unds'Gen1:SortGeneratedCounterCell{}),dotk{}()) + kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(Var'Unds'Gen0:SortGeneratedCounterCell{}),dotk{}()) ), \top{R} () ) @@ -1207,13 +1223,13 @@ module EVALUATE \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen0:SortGeneratedCounterCellOpt{}, + \exists{R} (Var'Unds'Gen1:SortGeneratedCounterCellOpt{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortGeneratedCounterCellOpt{}, SortKItem{}}(Var'Unds'Gen0:SortGeneratedCounterCellOpt{}),dotk{}()) + kseq{}(inj{SortGeneratedCounterCellOpt{}, SortKItem{}}(Var'Unds'Gen1:SortGeneratedCounterCellOpt{}),dotk{}()) ), \top{R} () ) @@ -1261,13 +1277,13 @@ module EVALUATE \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:SortGeneratedTopCell{}, + \exists{R} (Var'Unds'Gen0:SortGeneratedTopCell{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(Var'Unds'Gen1:SortGeneratedTopCell{}),dotk{}()) + kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(Var'Unds'Gen0:SortGeneratedTopCell{}),dotk{}()) ), \top{R} () ) @@ -1441,13 +1457,13 @@ module EVALUATE \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen0:SortKCell{}, + \exists{R} (Var'Unds'Gen1:SortKCell{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortKCell{}, SortKItem{}}(Var'Unds'Gen0:SortKCell{}),dotk{}()) + kseq{}(inj{SortKCell{}, SortKItem{}}(Var'Unds'Gen1:SortKCell{}),dotk{}()) ), \top{R} () ) @@ -1657,13 +1673,13 @@ module EVALUATE \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen1:SortList{}, + \exists{R} (Var'Unds'Gen0:SortList{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortList{}, SortKItem{}}(Var'Unds'Gen1:SortList{}),dotk{}()) + kseq{}(inj{SortList{}, SortKItem{}}(Var'Unds'Gen0:SortList{}),dotk{}()) ), \top{R} () ) @@ -1711,13 +1727,13 @@ module EVALUATE \and{R} ( \not{R} ( \or{R} ( - \exists{R} (Var'Unds'Gen0:SortMap{}, + \exists{R} (Var'Unds'Gen1:SortMap{}, \and{R} ( \top{R}(), \and{R} ( \in{SortK{}, R} ( X0:SortK{}, - kseq{}(inj{SortMap{}, SortKItem{}}(Var'Unds'Gen0:SortMap{}),dotk{}()) + kseq{}(inj{SortMap{}, SortKItem{}}(Var'Unds'Gen1:SortMap{}),dotk{}()) ), \top{R} () ) @@ -1814,7 +1830,7 @@ module EVALUATE \top{SortBool{}}()))) [UNIQUE'Unds'ID{}("f205bc460bdb728b4c3458643699be30d519db4d8b13e80e2c27082b9e846e80")] -// rule `minInt(_,_)_INT-COMMON_Int_Int_Int`(I1,I2)=>I1 requires `_<=Int_`(I1,I2) ensures #token("true","Bool") [UNIQUE_ID(fb09b6acc4366cb77203e07c4efe8a9cf304e1bac9fb0664deea05d3eb9a80c6), org.kframework.attributes.Location(Location(1426,8,1426,57)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] +// rule `minInt(_,_)_INT-COMMON_Int_Int_Int`(I1,I2)=>I1 requires `_<=Int_`(I1,I2) ensures #token("true","Bool") [UNIQUE_ID(fb09b6acc4366cb77203e07c4efe8a9cf304e1bac9fb0664deea05d3eb9a80c6), org.kframework.attributes.Location(Location(1426,8,1426,57)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -1836,9 +1852,9 @@ module EVALUATE \and{SortInt{}} ( VarI1:SortInt{}, \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("fb09b6acc4366cb77203e07c4efe8a9cf304e1bac9fb0664deea05d3eb9a80c6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1426,8,1426,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] + [UNIQUE'Unds'ID{}("fb09b6acc4366cb77203e07c4efe8a9cf304e1bac9fb0664deea05d3eb9a80c6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1426,8,1426,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] -// 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(1427,8,1427,57)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] +// 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(1427,8,1427,57)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] axiom{R} \implies{R} ( \and{R}( \equals{SortBool{},R}( @@ -1860,9 +1876,9 @@ module EVALUATE \and{SortInt{}} ( VarI2:SortInt{}, \top{SortInt{}}()))) - [UNIQUE'Unds'ID{}("e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1427,8,1427,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] + [UNIQUE'Unds'ID{}("e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1427,8,1427,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")] -// rule `notBool_`(#token("false","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415), org.kframework.attributes.Location(Location(1119,8,1119,29)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `notBool_`(#token("false","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415), org.kframework.attributes.Location(Location(1119,8,1119,29)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -1878,9 +1894,9 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("true"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1119,8,1119,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1119,8,1119,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] -// rule `notBool_`(#token("true","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c), org.kframework.attributes.Location(Location(1118,8,1118,29)), org.kframework.attributes.Source(Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] +// rule `notBool_`(#token("true","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c), org.kframework.attributes.Location(Location(1118,8,1118,29)), org.kframework.attributes.Source(Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] axiom{R} \implies{R} ( \and{R}( \top{R}(), @@ -1896,7 +1912,7 @@ module EVALUATE \and{SortBool{}} ( \dv{SortBool{}}("false"), \top{SortBool{}}()))) - [UNIQUE'Unds'ID{}("53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1118,8,1118,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/hsyjdwwx88f1d6ap53lv6zdm1b9r8y03-k-6.1.25-41dfa2474fea88b1313e8ac2b12c25dd3e722f9e/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + [UNIQUE'Unds'ID{}("53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1118,8,1118,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/fg6ksmcv4ddxgn27xnrp38sxf2gad9wi-k-6.1.36-ddb98f2d97e1460f73140ff3693b6f5fb9a84d73/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] // rule `project:Bool`(inj{Bool,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5872f0d5b8131216db7bc41e2c3a423e55f4b8581589fcbd1bf93b2ca6862d54), projection] axiom{R} \implies{R} ( @@ -2150,7 +2166,25 @@ module EVALUATE \top{SortSet{}}()))) [UNIQUE'Unds'ID{}("0e7f5070c993161786e314f7199d985afebac9e07b5c784f6f623780c60ce9d0"), projection{}()] -// 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_`(I,#token("34","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(31023a7a43cbf6fcaa550c42d3d6e6f271aa5a0cf1d2c4938800c57418e5af7f), org.kframework.attributes.Location(Location(15,8,15,28)), org.kframework.attributes.Source(Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortInt{}, R} ( + X0:SortInt{}, + VarI:SortInt{} + ), + \top{R} () + )), + \equals{SortBool{},R} ( + Lblqux{}(X0:SortInt{}), + \and{SortBool{}} ( + Lbl'UndsEqlsEqls'Int'Unds'{}(VarI:SortInt{},\dv{SortInt{}}("34")), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("31023a7a43cbf6fcaa550c42d3d6e6f271aa5a0cf1d2c4938800c57418e5af7f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(15,8,15,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/brucecollie/code/llvm-backend/test/python/k-files/evaluate.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]")] + +// rule `signExtendBitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN)=>`_-Int_`(`_modInt_`(`_+Int_`(`bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN),`_< foo(A +Int B) + + syntax Int ::= baz() [function, label(baz), symbol] + syntax Bool ::= qux(Int) [function, label(qux), symbol] + + rule baz() => 78 + rule qux(I) => I ==Int 34 endmodule diff --git a/test/python/test_evaluate.py b/test/python/test_evaluate.py index 08225249d..91fa97f76 100644 --- a/test/python/test_evaluate.py +++ b/test/python/test_evaluate.py @@ -10,12 +10,25 @@ class TestEvaluate(unittest.TestCase): - def test_eval(self): + def test_ctor(self): left = kllvm.parser.Parser.from_string('Lblfoo{}(\\dv{SortInt{}}("23"))').pattern() right = kllvm.parser.Parser.from_string('Lblbar{}(\\dv{SortInt{}}("56"))').pattern() result = kllvm.runtime.evaluate_function('Lblf{}', [left, right]) - print(result) + self.assertEqual(str(result), 'Lblfoo{}(\dv{SortInt{}}("79"))') + + def test_int_function(self): + result = kllvm.runtime.evaluate_function('Lblbaz{}', []) + self.assertEqual(str(result), '\dv{SortInt{}}("78")') + + def test_bool_function(self): + arg_t = kllvm.parser.Parser.from_string('\\dv{SortInt{}}("34")').pattern() + result_t = kllvm.runtime.evaluate_function('Lblqux{}', [arg_t]) + self.assertEqual(str(result_t), '\dv{SortBool{}}("true")') + + arg_f = kllvm.parser.Parser.from_string('\\dv{SortInt{}}("98")').pattern() + result_f = kllvm.runtime.evaluate_function('Lblqux{}', [arg_f]) + self.assertEqual(str(result_f), '\dv{SortBool{}}("false")') if __name__ == "__main__":