Skip to content

Commit 0c92b66

Browse files
geo2ageo2a
committed
Don't check initial constraints when "assume-state-defined"
1 parent 5862b70 commit 0c92b66

8 files changed

+453
-2
lines changed

‎booster/library/Booster/JsonRpc.hs

+6-1
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,11 @@ respond stateVar request =
131131
[ req.logSuccessfulRewrites
132132
, req.logFailedRewrites
133133
]
134+
checkConstraintsConsistent =
135+
case req.assumeStateDefined of
136+
Nothing -> ApplyEquations.CheckConstraintsConsistent
137+
Just False -> ApplyEquations.CheckConstraintsConsistent
138+
Just True -> ApplyEquations.NoCheckConstraintsConsistent
134139
-- apply the given substitution before doing anything else
135140
let substPat =
136141
Pattern
@@ -154,7 +159,7 @@ respond stateVar request =
154159
mLlvmLibrary
155160
solver
156161
mempty
157-
ApplyEquations.CheckConstraintsConsistent
162+
checkConstraintsConsistent
158163
substPat
159164

160165
case evaluatedInitialPattern of

‎booster/test/rpc-integration/test-vacuous/params-unchecked-vacuous-rewrite.json

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{ "assume-state-defined": true }

‎booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{ "assume-state-defined": true }

‎booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.json

+221
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,221 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "stuck",
6+
"depth": 0,
7+
"state": {
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "And",
13+
"sort": {
14+
"tag": "SortApp",
15+
"name": "SortGeneratedTopCell",
16+
"args": []
17+
},
18+
"patterns": [
19+
{
20+
"tag": "App",
21+
"name": "Lbl'-LT-'generatedTop'-GT-'",
22+
"sorts": [],
23+
"args": [
24+
{
25+
"tag": "App",
26+
"name": "Lbl'-LT-'k'-GT-'",
27+
"sorts": [],
28+
"args": [
29+
{
30+
"tag": "App",
31+
"name": "kseq",
32+
"sorts": [],
33+
"args": [
34+
{
35+
"tag": "App",
36+
"name": "inj",
37+
"sorts": [
38+
{
39+
"tag": "SortApp",
40+
"name": "SortState",
41+
"args": []
42+
},
43+
{
44+
"tag": "SortApp",
45+
"name": "SortKItem",
46+
"args": []
47+
}
48+
],
49+
"args": [
50+
{
51+
"tag": "DV",
52+
"sort": {
53+
"tag": "SortApp",
54+
"name": "SortState",
55+
"args": []
56+
},
57+
"value": "d"
58+
}
59+
]
60+
},
61+
{
62+
"tag": "App",
63+
"name": "dotk",
64+
"sorts": [],
65+
"args": []
66+
}
67+
]
68+
}
69+
]
70+
},
71+
{
72+
"tag": "App",
73+
"name": "Lbl'-LT-'int'-GT-'",
74+
"sorts": [],
75+
"args": [
76+
{
77+
"tag": "EVar",
78+
"name": "N",
79+
"sort": {
80+
"tag": "SortApp",
81+
"name": "SortInt",
82+
"args": []
83+
}
84+
}
85+
]
86+
},
87+
{
88+
"tag": "App",
89+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
90+
"sorts": [],
91+
"args": [
92+
{
93+
"tag": "DV",
94+
"sort": {
95+
"tag": "SortApp",
96+
"name": "SortInt",
97+
"args": []
98+
},
99+
"value": "0"
100+
}
101+
]
102+
}
103+
]
104+
},
105+
{
106+
"tag": "And",
107+
"sort": {
108+
"tag": "SortApp",
109+
"name": "SortGeneratedTopCell",
110+
"args": []
111+
},
112+
"patterns": [
113+
{
114+
"tag": "Equals",
115+
"argSort": {
116+
"tag": "SortApp",
117+
"name": "SortBool",
118+
"args": []
119+
},
120+
"sort": {
121+
"tag": "SortApp",
122+
"name": "SortGeneratedTopCell",
123+
"args": []
124+
},
125+
"first": {
126+
"tag": "DV",
127+
"sort": {
128+
"tag": "SortApp",
129+
"name": "SortBool",
130+
"args": []
131+
},
132+
"value": "true"
133+
},
134+
"second": {
135+
"tag": "App",
136+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
137+
"sorts": [],
138+
"args": [
139+
{
140+
"tag": "EVar",
141+
"name": "N",
142+
"sort": {
143+
"tag": "SortApp",
144+
"name": "SortInt",
145+
"args": []
146+
}
147+
},
148+
{
149+
"tag": "DV",
150+
"sort": {
151+
"tag": "SortApp",
152+
"name": "SortInt",
153+
"args": []
154+
},
155+
"value": "0"
156+
}
157+
]
158+
}
159+
},
160+
{
161+
"tag": "Equals",
162+
"argSort": {
163+
"tag": "SortApp",
164+
"name": "SortBool",
165+
"args": []
166+
},
167+
"sort": {
168+
"tag": "SortApp",
169+
"name": "SortGeneratedTopCell",
170+
"args": []
171+
},
172+
"first": {
173+
"tag": "DV",
174+
"sort": {
175+
"tag": "SortApp",
176+
"name": "SortBool",
177+
"args": []
178+
},
179+
"value": "true"
180+
},
181+
"second": {
182+
"tag": "App",
183+
"name": "LblnotBool'Unds'",
184+
"sorts": [],
185+
"args": [
186+
{
187+
"tag": "App",
188+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
189+
"sorts": [],
190+
"args": [
191+
{
192+
"tag": "EVar",
193+
"name": "N",
194+
"sort": {
195+
"tag": "SortApp",
196+
"name": "SortInt",
197+
"args": []
198+
}
199+
},
200+
{
201+
"tag": "DV",
202+
"sort": {
203+
"tag": "SortApp",
204+
"name": "SortInt",
205+
"args": []
206+
},
207+
"value": "0"
208+
}
209+
]
210+
}
211+
]
212+
}
213+
}
214+
]
215+
}
216+
]
217+
}
218+
}
219+
}
220+
}
221+
}

0 commit comments

Comments
 (0)