diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 520d540eb8..8582453e0b 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -429,14 +429,6 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort Syntax.KJBottom{} -> notSupported Syntax.KJNot{arg} -> do recursion arg >>= \case - [BoolPred (Internal.Predicate (Internal.EqualsInt a b))] -> - pure [BoolPred $ Internal.Predicate $ Internal.NEqualsInt a b] - [BoolPred (Internal.Predicate (Internal.NEqualsInt a b))] -> - pure [BoolPred $ Internal.Predicate $ Internal.EqualsInt a b] - [BoolPred (Internal.Predicate (Internal.EqualsK a b))] -> - pure [BoolPred $ Internal.Predicate $ Internal.NEqualsK a b] - [BoolPred (Internal.Predicate (Internal.NEqualsK a b))] -> - pure [BoolPred $ Internal.Predicate $ Internal.EqualsK a b] [BoolPred (Internal.Predicate p')] -> pure [BoolPred $ Internal.Predicate $ Internal.NotBool p'] [SubstitutionPred k v] -> @@ -444,12 +436,13 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort then notSupported -- @ variables are set variables, the negation of which we do not support internalising else case sortOfTerm v of Internal.SortInt -> - pure [BoolPred $ Internal.Predicate $ Internal.NEqualsInt (Internal.Var k) v] + pure [BoolPred $ Internal.Predicate $ Internal.NotBool $ Internal.EqualsInt (Internal.Var k) v] otherSort -> pure [ BoolPred $ Internal.Predicate $ - Internal.NEqualsK (Internal.KSeq otherSort $ Internal.Var k) (Internal.KSeq otherSort v) + Internal.NotBool $ + Internal.EqualsK (Internal.KSeq otherSort $ Internal.Var k) (Internal.KSeq otherSort v) ] _ -> notSupported Syntax.KJAnd{patterns = []} -> notSupported diff --git a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json index 9084ce597f..adce093c44 100644 --- a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json +++ b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.json @@ -7360,6 +7360,60 @@ ] } }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "LblnotBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'Ques'WORD7", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + }, { "tag": "Equals", "argSort": { @@ -7524,12 +7578,12 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", "sorts": [], "args": [ { "tag": "EVar", - "name": "Var'Ques'WORD7", + "name": "Var'Ques'WORD9", "sort": { "tag": "SortApp", "name": "SortInt", @@ -7537,13 +7591,13 @@ } }, { - "tag": "DV", + "tag": "EVar", + "name": "Var'Ques'WORD7", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "0" + } } ] } @@ -7571,26 +7625,33 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'WORD9", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "Var'Ques'WORD7", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'Ques'WORD8", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] } ] } @@ -7759,12 +7820,12 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "Lbl'Unds-LT-'Int'Unds'", "sorts": [], "args": [ { "tag": "EVar", - "name": "Var'Ques'WORD8", + "name": "Var'Ques'WORD9", "sort": { "tag": "SortApp", "name": "SortInt", @@ -7778,7 +7839,7 @@ "name": "SortInt", "args": [] }, - "value": "0" + "value": "1000000000000000000000000000" } ] } @@ -7825,7 +7886,7 @@ "name": "SortInt", "args": [] }, - "value": "1000000000000000000000000000" + "value": "115792089237316195423570985008687907853269984665640564039457584007913129639936" } ] } @@ -7853,26 +7914,26 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-'Int'Unds'", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'WORD9", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "0" }, { - "tag": "DV", + "tag": "EVar", + "name": "Var'Ques'WORD9", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "115792089237316195423570985008687907853269984665640564039457584007913129639936" + } } ] } @@ -7900,26 +7961,33 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - }, - { - "tag": "EVar", - "name": "Var'Ques'WORD9", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarCALLER'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "645326474426547203313410069153905908525362434349" + } + ] } ] } @@ -8127,73 +8195,33 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarCALLER'Unds'ID", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "645326474426547203313410069153905908525362434349" - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "VarCONTRACT'Unds'ID", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "645326474426547203313410069153905908525362434349" + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarCONTRACT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "645326474426547203313410069153905908525362434349" + } + ] } ] } @@ -8315,26 +8343,33 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - }, - { - "tag": "EVar", - "name": "VarORIGIN'Unds'ID", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarORIGIN'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "645326474426547203313410069153905908525362434349" + } + ] } ] } @@ -8362,26 +8397,26 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "VarORIGIN'Unds'ID", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "0" }, { - "tag": "DV", + "tag": "EVar", + "name": "VarORIGIN'Unds'ID", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "645326474426547203313410069153905908525362434349" + } } ] } diff --git a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json index b48f9573a7..450e95c271 100644 --- a/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json +++ b/booster/test/rpc-integration/test-issue3764-vacuous-branch/response-branch-in-zero.json @@ -7360,6 +7360,60 @@ ] } }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "LblnotBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'Ques'WORD7", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + }, { "tag": "Equals", "argSort": { @@ -7524,12 +7578,12 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", "sorts": [], "args": [ { "tag": "EVar", - "name": "Var'Ques'WORD7", + "name": "Var'Ques'WORD9", "sort": { "tag": "SortApp", "name": "SortInt", @@ -7537,13 +7591,13 @@ } }, { - "tag": "DV", + "tag": "EVar", + "name": "Var'Ques'WORD7", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "0" + } } ] } @@ -7571,26 +7625,33 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'WORD9", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "Var'Ques'WORD7", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "Var'Ques'WORD8", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] } ] } @@ -7759,12 +7820,12 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "Lbl'Unds-LT-'Int'Unds'", "sorts": [], "args": [ { "tag": "EVar", - "name": "Var'Ques'WORD8", + "name": "Var'Ques'WORD9", "sort": { "tag": "SortApp", "name": "SortInt", @@ -7778,7 +7839,7 @@ "name": "SortInt", "args": [] }, - "value": "0" + "value": "1000000000000000000000000000" } ] } @@ -7825,7 +7886,7 @@ "name": "SortInt", "args": [] }, - "value": "1000000000000000000000000000" + "value": "115792089237316195423570985008687907853269984665640564039457584007913129639936" } ] } @@ -7853,26 +7914,26 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-'Int'Unds'", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'WORD9", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "0" }, { - "tag": "DV", + "tag": "EVar", + "name": "Var'Ques'WORD9", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "115792089237316195423570985008687907853269984665640564039457584007913129639936" + } } ] } @@ -7900,26 +7961,33 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - }, - { - "tag": "EVar", - "name": "Var'Ques'WORD9", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarCALLER'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "645326474426547203313410069153905908525362434349" + } + ] } ] } @@ -8127,73 +8195,33 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "VarCALLER'Unds'ID", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "645326474426547203313410069153905908525362434349" - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "VarCONTRACT'Unds'ID", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "645326474426547203313410069153905908525362434349" + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarCONTRACT'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "645326474426547203313410069153905908525362434349" + } + ] } ] } @@ -8315,26 +8343,33 @@ }, "second": { "tag": "App", - "name": "Lbl'Unds-LT-Eqls'Int'Unds'", + "name": "LblnotBool'Unds'", "sorts": [], "args": [ { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - }, - { - "tag": "EVar", - "name": "VarORIGIN'Unds'ID", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "VarORIGIN'Unds'ID", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "645326474426547203313410069153905908525362434349" + } + ] } ] } @@ -8362,26 +8397,26 @@ }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'", + "name": "Lbl'Unds-LT-Eqls'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "VarORIGIN'Unds'ID", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "0" }, { - "tag": "DV", + "tag": "EVar", + "name": "VarORIGIN'Unds'ID", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "645326474426547203313410069153905908525362434349" + } } ] }