Skip to content

Commit c643c26

Browse files
tanyongkiamtanyongkiam
authored
Update annotations for some PB frontends (#1282)
* add annotations to subgraph iso * add annotations to mcis/mccis * annot_prob
1 parent 3c7122a commit c643c26

File tree

8 files changed

+209
-144
lines changed

8 files changed

+209
-144
lines changed

‎examples/pseudo_bool/array/compilation/proofs/mccisProofScript.sml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ Theorem machine_code_sound:
7777
get_graph_lad fs (EL 2 cl) = SOME gt ∧
7878
(
7979
(LENGTH cl = 3 ∧
80-
out = concat (print_prob (mk_prob (full_encode_mccis gp gt)))) ∨
80+
out = concat (print_annot_prob (mk_prob (full_encode_mccis gp gt)))) ∨
8181
(LENGTH cl = 4 ∧
8282
(
8383
out = mccis_eq_str (max_ccis_size gp gt) ∨

‎examples/pseudo_bool/array/compilation/proofs/mcisProofScript.sml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ Theorem machine_code_sound:
7777
get_graph_lad fs (EL 2 cl) = SOME gt ∧
7878
(
7979
(LENGTH cl = 3 ∧
80-
out = concat (print_prob (mk_prob (full_encode_mcis gp gt)))) ∨
80+
out = concat (print_annot_prob (mk_prob (full_encode_mcis gp gt)))) ∨
8181
(LENGTH cl = 4 ∧
8282
(
8383
out = mcis_eq_str (max_cis_size gp gt) ∨

‎examples/pseudo_bool/array/compilation/proofs/subgraph_isoProofScript.sml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ Theorem machine_code_sound:
7777
get_graph_lad fs (EL 2 cl) = SOME gt ∧
7878
(
7979
(LENGTH cl = 3 ∧
80-
out = concat (print_prob (mk_prob (full_encode gp gt)))) ∨
80+
out = concat (print_annot_prob (mk_prob (full_encode gp gt)))) ∨
8181
(LENGTH cl = 4 ∧
8282
(
8383
(out = «s VERIFIED NOT SUBGRAPH ISOMORPHIC\n» ∧

‎examples/pseudo_bool/array/mccisProgScript.sml‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,10 @@ Theorem parse_and_enc_spec:
6161
(OPTION_TYPE (PAIR_TYPE
6262
(LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE)))
6363
INT))
64-
(LIST_TYPE (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))
64+
(LIST_TYPE
65+
(PAIR_TYPE
66+
(OPTION_TYPE STRING_TYPE)
67+
(PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))))
6568
)) res v ∧
6669
case res of
6770
INL err =>
@@ -157,7 +160,8 @@ val res = translate map_concl_to_string_def;
157160
Definition mk_prob_def:
158161
mk_prob objf = (NONE,objf):mlstring list option #
159162
((int # mlstring pbc$lit) list # int) option #
160-
(pbop # (int # mlstring pbc$lit) list # int) list
163+
(mlstring option #
164+
(pbop # (int # mlstring pbc$lit) list # int)) list
161165
End
162166

163167
val res = translate mk_prob_def;
@@ -167,10 +171,13 @@ val check_unsat_3 = (append_prog o process_topdecs) `
167171
case parse_and_enc f1 f2 of
168172
Inl err => TextIO.output TextIO.stdErr err
169173
| Inr (n,objf) =>
170-
let val probt = default_prob in
174+
let val probt = default_prob
175+
val prob = mk_prob objf
176+
val prob = strip_annot_prob prob
177+
in
171178
(case
172179
map_concl_to_string n
173-
(check_unsat_top_norm False (mk_prob objf) probt f3) of
180+
(check_unsat_top_norm False prob probt f3) of
174181
Inl err => TextIO.output TextIO.stdErr err
175182
| Inr s => TextIO.print s)
176183
end`
@@ -223,11 +230,12 @@ Proof
223230
>-
224231
(xvar>>xsimpl)>>
225232
xlet_autop>>
233+
xlet_autop>>
226234
xlet`POSTv v. STDIO fs * &BOOL F v`
227235
>-
228236
(xcon>>xsimpl)>>
229237
drule npbc_parseProgTheory.check_unsat_top_norm_spec>>
230-
qpat_x_assum`prob_TYPE (mk_prob _) _`assume_tac>>
238+
qpat_x_assum`prob_TYPE (strip_annot_prob _) _`assume_tac>>
231239
disch_then drule>>
232240
qpat_x_assum`prob_TYPE default_prob _`assume_tac>>
233241
disch_then drule>>
@@ -274,14 +282,17 @@ Proof
274282
qexists_tac`strlit ""`>>
275283
simp[STD_streams_stderr,add_stdo_nil]>>
276284
xsimpl>>
285+
fs[oneline pb_parseTheory.strip_annot_prob_def]>>
286+
every_case_tac>>gvs[]>>
277287
(drule_at Any) full_encode_mccis_sem_concl>>
278288
fs[]>>
279289
Cases_on`x`>> disch_then (drule_at Any)>>
280290
disch_then(qspec_then`gt'` mp_tac)>>
281291
impl_tac>-
282292
fs[get_graph_lad_def,AllCaseEqs(),mk_prob_def]>>
283293
rw[]>>
284-
qexists_tac`(q,r)`>>
294+
rename1`(qq,rr)`>>
295+
qexists_tac`(qq,rr)`>>
285296
simp[mccis_sem_def]>>
286297
metis_tac[])
287298
QED
@@ -294,7 +305,7 @@ Definition check_unsat_2_sem_def:
294305
case get_graph_lad fs f2 of
295306
NONE => out = strlit ""
296307
| SOME gtt =>
297-
out = concat (print_prob
308+
out = concat (print_annot_prob
298309
(mk_prob (full_encode_mccis gpp gtt)))
299310
End
300311

@@ -303,7 +314,7 @@ val check_unsat_2 = (append_prog o process_topdecs) `
303314
case parse_and_enc f1 f2 of
304315
Inl err => TextIO.output TextIO.stdErr err
305316
| Inr (n,objf) =>
306-
TextIO.print_list (print_prob (mk_prob objf))`
317+
TextIO.print_list (print_annot_prob (mk_prob objf))`
307318

308319
Theorem check_unsat_2_spec:
309320
STRING_TYPE f1 f1v ∧ validArg f1 ∧

‎examples/pseudo_bool/array/mcisProgScript.sml‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,10 @@ Theorem parse_and_enc_spec:
5050
(OPTION_TYPE (PAIR_TYPE
5151
(LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE)))
5252
INT))
53-
(LIST_TYPE (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))
53+
(LIST_TYPE
54+
(PAIR_TYPE
55+
(OPTION_TYPE STRING_TYPE)
56+
(PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))))
5457
)) res v ∧
5558
case res of
5659
INL err =>
@@ -146,7 +149,8 @@ val res = translate map_concl_to_string_def;
146149
Definition mk_prob_def:
147150
mk_prob objf = (NONE,objf):mlstring list option #
148151
((int # mlstring pbc$lit) list # int) option #
149-
(pbop # (int # mlstring pbc$lit) list # int) list
152+
(mlstring option #
153+
(pbop # (int # mlstring pbc$lit) list # int)) list
150154
End
151155

152156
val res = translate mk_prob_def;
@@ -156,10 +160,13 @@ val check_unsat_3 = (append_prog o process_topdecs) `
156160
case parse_and_enc f1 f2 of
157161
Inl err => TextIO.output TextIO.stdErr err
158162
| Inr (n,objf) =>
159-
let val probt = default_prob in
163+
let val probt = default_prob
164+
val prob = mk_prob objf
165+
val prob = strip_annot_prob prob
166+
in
160167
(case
161168
map_concl_to_string n
162-
(check_unsat_top_norm False (mk_prob objf) probt f3) of
169+
(check_unsat_top_norm False prob probt f3) of
163170
Inl err => TextIO.output TextIO.stdErr err
164171
| Inr s => TextIO.print s)
165172
end`
@@ -212,11 +219,12 @@ Proof
212219
>-
213220
(xvar>>xsimpl)>>
214221
xlet_autop>>
222+
xlet_autop>>
215223
xlet`POSTv v. STDIO fs * &BOOL F v`
216224
>-
217225
(xcon>>xsimpl)>>
218226
drule npbc_parseProgTheory.check_unsat_top_norm_spec>>
219-
qpat_x_assum`prob_TYPE (mk_prob _) _`assume_tac>>
227+
qpat_x_assum`prob_TYPE (strip_annot_prob _) _`assume_tac>>
220228
disch_then drule>>
221229
qpat_x_assum`prob_TYPE default_prob _`assume_tac>>
222230
disch_then drule>>
@@ -263,14 +271,17 @@ Proof
263271
qexists_tac`strlit ""`>>
264272
rw[]>>simp[STD_streams_stderr,add_stdo_nil]>>
265273
xsimpl>>
274+
fs[oneline pb_parseTheory.strip_annot_prob_def]>>
275+
every_case_tac>>gvs[]>>
266276
(drule_at Any) full_encode_mcis_sem_concl>>
267277
fs[]>>
268278
Cases_on`x`>> disch_then (drule_at Any)>>
269279
disch_then(qspec_then`gt'` mp_tac)>>
270280
impl_tac>-
271281
fs[get_graph_lad_def,AllCaseEqs(),mk_prob_def]>>
272282
rw[]>>
273-
qexists_tac`(q,r)`>>
283+
rename1`(qq,rr)`>>
284+
qexists_tac`(qq,rr)`>>
274285
simp[mcis_sem_def]>>
275286
metis_tac[])
276287
QED
@@ -283,7 +294,7 @@ Definition check_unsat_2_sem_def:
283294
case get_graph_lad fs f2 of
284295
NONE => out = strlit ""
285296
| SOME gtt =>
286-
out = concat (print_prob
297+
out = concat (print_annot_prob
287298
(mk_prob (full_encode_mcis gpp gtt)))
288299
End
289300

@@ -292,7 +303,7 @@ val check_unsat_2 = (append_prog o process_topdecs) `
292303
case parse_and_enc f1 f2 of
293304
Inl err => TextIO.output TextIO.stdErr err
294305
| Inr (n,objf) =>
295-
TextIO.print_list (print_prob (mk_prob objf))`
306+
TextIO.print_list (print_annot_prob (mk_prob objf))`
296307

297308
Theorem check_unsat_2_spec:
298309
STRING_TYPE f1 f1v ∧ validArg f1 ∧

‎examples/pseudo_bool/array/subgraph_isoProgScript.sml‎

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,10 @@ Theorem parse_and_enc_spec:
4545
& ∃res.
4646
SUM_TYPE STRING_TYPE
4747
(LIST_TYPE
48-
(PAIR_TYPE PBC_PBOP_TYPE
49-
(PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))) res v ∧
48+
(PAIR_TYPE
49+
(OPTION_TYPE STRING_TYPE)
50+
(PAIR_TYPE PBC_PBOP_TYPE
51+
(PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))) res v ∧
5052
case res of
5153
INL err =>
5254
get_graph_lad fs f1 = NONE ∨ get_graph_lad fs f2 = NONE
@@ -110,7 +112,8 @@ val res = translate (res_to_string_def |> SIMP_RULE std_ss [UNSAT_string_def,SAT
110112
Definition mk_prob_def:
111113
mk_prob fml = (NONE,NONE,fml):mlstring list option #
112114
((int # mlstring pbc$lit) list # int) option #
113-
(pbop # (int # mlstring pbc$lit) list # int) list
115+
(mlstring option #
116+
(pbop # (int # mlstring pbc$lit) list # int)) list
114117
End
115118

116119
val res = translate mk_prob_def;
@@ -120,9 +123,11 @@ val check_unsat_3 = (append_prog o process_topdecs) `
120123
case parse_and_enc f1 f2 of
121124
Inl err => TextIO.output TextIO.stdErr err
122125
| Inr fml =>
123-
let val probt = default_prob in
126+
let val probt = default_prob
127+
val prob = mk_prob fml
128+
val prob = strip_annot_prob prob in
124129
(case
125-
res_to_string (check_unsat_top_norm False (mk_prob fml) probt f3) of
130+
res_to_string (check_unsat_top_norm False prob probt f3) of
126131
Inl err => TextIO.output TextIO.stdErr err
127132
| Inr s => TextIO.print s)
128133
end`
@@ -174,6 +179,7 @@ Proof
174179
>-
175180
(xvar>>xsimpl)>>
176181
xlet_autop>>
182+
xlet_autop>>
177183
xlet`POSTv v. STDIO fs * &BOOL F v`
178184
>-
179185
(xcon>>xsimpl)>>
@@ -225,6 +231,7 @@ Proof
225231
qexists_tac`strlit ""`>>
226232
simp[STD_streams_stderr,add_stdo_nil]>>
227233
xsimpl>>
234+
fs[pb_parseTheory.strip_annot_prob_def]>>
228235
(drule_at Any) full_encode_sem_concl>>
229236
fs[]>>
230237
impl_tac >-
@@ -239,6 +246,7 @@ Proof
239246
qexists_tac`strlit ""`>>
240247
simp[STD_streams_stderr,add_stdo_nil]>>
241248
xsimpl>>
249+
fs[pb_parseTheory.strip_annot_prob_def]>>
242250
(drule_at Any) full_encode_sem_concl>>
243251
fs[]>>
244252
impl_tac >-
@@ -264,15 +272,15 @@ Definition check_unsat_2_sem_def:
264272
case get_graph_lad fs f2 of
265273
NONE => out = strlit ""
266274
| SOME gtt =>
267-
out = concat (print_prob (mk_prob (full_encode gpp gtt)))
275+
out = concat (print_annot_prob (mk_prob (full_encode gpp gtt)))
268276
End
269277

270278
val check_unsat_2 = (append_prog o process_topdecs) `
271279
fun check_unsat_2 f1 f2 =
272280
case parse_and_enc f1 f2 of
273281
Inl err => TextIO.output TextIO.stdErr err
274282
| Inr fml =>
275-
TextIO.print_list (print_prob (mk_prob fml))`
283+
TextIO.print_list (print_annot_prob (mk_prob fml))`
276284

277285
Theorem check_unsat_2_spec:
278286
STRING_TYPE f1 f1v ∧ validArg f1 ∧

0 commit comments

Comments
 (0)