Skip to content

Commit

Permalink
Use the pattern sort for rule substitution
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a committed Oct 28, 2024
1 parent 691f19c commit cb22130
Show file tree
Hide file tree
Showing 7 changed files with 144 additions and 144 deletions.
6 changes: 3 additions & 3 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -605,13 +605,13 @@ toExecState pat unsupported muid mrulePredicate mruleSubst =
where
mrulePredExt = externalisePredicate termSort <$> mrulePredicate
mruleSubstExt =
Syntax.KJAnd predicateSort
. map (uncurry (externaliseSubstitution predicateSort) . first (modifyVarName externaliseRuleMarker))
Syntax.KJAnd termSort
. map
(uncurry (externaliseSubstitution termSort) . first (modifyVarName externaliseRuleMarker))
. Map.toList
<$> mruleSubst
(t, p, s) = externalisePattern pat
termSort = externaliseSort $ sortOfPattern pat
predicateSort = externaliseSort Pattern.SortBool
allUnsupported = Syntax.KJAnd termSort unsupported
addUnsupported
| null unsupported = id
Expand Down
134 changes: 67 additions & 67 deletions booster/test/rpc-integration/test-3934-smt/response-008.booster-dev
View file

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions booster/test/rpc-integration/test-a-to-f/response-branching.booster-dev
View file
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
Expand All @@ -212,7 +212,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -250,7 +250,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -391,7 +391,7 @@
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
Expand All @@ -404,7 +404,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -442,7 +442,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down
48 changes: 24 additions & 24 deletions .../test/rpc-integration/test-issue3764-vacuous-branch/response-branch-after-one.booster-dev
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17670,7 +17670,7 @@
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
Expand All @@ -17683,7 +17683,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -18138,7 +18138,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -22762,7 +22762,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -22800,7 +22800,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -22838,7 +22838,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -22869,7 +22869,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -22987,7 +22987,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -23074,7 +23074,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -23196,7 +23196,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -23231,7 +23231,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -23266,7 +23266,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -32167,7 +32167,7 @@
"tag": "And",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
Expand All @@ -32180,7 +32180,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -32635,7 +32635,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37259,7 +37259,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37297,7 +37297,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37335,7 +37335,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37366,7 +37366,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37484,7 +37484,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37571,7 +37571,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37693,7 +37693,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37728,7 +37728,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down Expand Up @@ -37763,7 +37763,7 @@
},
"sort": {
"tag": "SortApp",
"name": "SortBool",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
Expand Down
Loading

0 comments on commit cb22130

Please sign in to comment.