From c527a8007bf0dedd376a9de586d867325ad6f106 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 19:32:31 +0200 Subject: [PATCH] Delete obsolete booster-dev responses --- ...ponse-mutual-constraints-stuck.booster-dev | 134 ------------------ ...se-mutual-constraints-terminal.booster-dev | 119 ---------------- .../response-circular-equations.booster-dev | 51 ------- ...onse-symbolic-bottom-predicate.booster-dev | 67 --------- 4 files changed, 371 deletions(-) delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev deleted file mode 100644 index 12b421e0d0..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev +++ /dev/null @@ -1,134 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 2, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "No applicable rules found" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "No applicable rules found" - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev deleted file mode 100644 index 92827d7008..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev +++ /dev/null @@ -1,119 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 2, - "rule": "TEST.FG", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index 46bbb4d894..c469de59ab 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -202,57 +202,6 @@ } ] } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "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'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } } } } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev index 09be95cd22..9a01a8013e 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev @@ -145,73 +145,6 @@ } } } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "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'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] - } - } } } }