Skip to content

Update annotations for some PB frontends #1282

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tanyongkiam wants to merge 2 commits into
base: master
Choose a base branch
from
+206 −141
Open

Update annotations for some PB frontends #1282

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6375809
add annotations to subgraph iso
tanyongkiam Dec 14, 2025
fcaf66e
add annotations to mcis/mccis
tanyongkiam Dec 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 19 additions & 8 deletions examples/pseudo_bool/array/mccisProgScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,10 @@ Theorem parse_and_enc_spec:
(OPTION_TYPE (PAIR_TYPE
(LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE)))
INT))
(LIST_TYPE (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))
(LIST_TYPE
(PAIR_TYPE
(OPTION_TYPE STRING_TYPE)
(PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))))
)) res v ∧
case res of
INL err =>
Expand Down Expand Up @@ -157,7 +160,8 @@ val res = translate map_concl_to_string_def;
Definition mk_prob_def:
mk_prob objf = (NONE,objf):mlstring list option #
((int # mlstring pbc$lit) list # int) option #
(pbop # (int # mlstring pbc$lit) list # int) list
(mlstring option #
(pbop # (int # mlstring pbc$lit) list # int)) list
End

val res = translate mk_prob_def;
Expand All @@ -167,10 +171,13 @@ val check_unsat_3 = (append_prog o process_topdecs) `
case parse_and_enc f1 f2 of
Inl err => TextIO.output TextIO.stdErr err
| Inr (n,objf) =>
let val probt = default_prob in
let val probt = default_prob
val prob = mk_prob objf
val prob = strip_annot_prob prob
in
(case
map_concl_to_string n
(check_unsat_top_norm False (mk_prob objf) probt f3) of
(check_unsat_top_norm False prob probt f3) of
Inl err => TextIO.output TextIO.stdErr err
| Inr s => TextIO.print s)
end`
Expand Down Expand Up @@ -223,11 +230,12 @@ Proof
>-
(xvar>>xsimpl)>>
xlet_autop>>
xlet_autop>>
xlet`POSTv v. STDIO fs * &BOOL F v`
>-
(xcon>>xsimpl)>>
drule npbc_parseProgTheory.check_unsat_top_norm_spec>>
qpat_x_assum`prob_TYPE (mk_prob _) _`assume_tac>>
qpat_x_assum`prob_TYPE (strip_annot_prob _) _`assume_tac>>
disch_then drule>>
qpat_x_assum`prob_TYPE default_prob _`assume_tac>>
disch_then drule>>
Expand Down Expand Up @@ -274,14 +282,17 @@ Proof
qexists_tac`strlit ""`>>
simp[STD_streams_stderr,add_stdo_nil]>>
xsimpl>>
fs[oneline pb_parseTheory.strip_annot_prob_def]>>
every_case_tac>>gvs[]>>
(drule_at Any) full_encode_mccis_sem_concl>>
fs[]>>
Cases_on`x`>> disch_then (drule_at Any)>>
disch_then(qspec_then`gt'` mp_tac)>>
impl_tac>-
fs[get_graph_lad_def,AllCaseEqs(),mk_prob_def]>>
rw[]>>
qexists_tac`(q,r)`>>
rename1`(qq,rr)`>>
qexists_tac`(qq,rr)`>>
simp[mccis_sem_def]>>
metis_tac[])
QED
Expand All @@ -294,7 +305,7 @@ Definition check_unsat_2_sem_def:
case get_graph_lad fs f2 of
NONE => out = strlit ""
| SOME gtt =>
out = concat (print_prob
out = concat (print_annot_prob
(mk_prob (full_encode_mccis gpp gtt)))
End

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

Theorem check_unsat_2_spec:
STRING_TYPE f1 f1v ∧ validArg f1 ∧
Expand Down
27 changes: 19 additions & 8 deletions examples/pseudo_bool/array/mcisProgScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,10 @@ Theorem parse_and_enc_spec:
(OPTION_TYPE (PAIR_TYPE
(LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE)))
INT))
(LIST_TYPE (PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))
(LIST_TYPE
(PAIR_TYPE
(OPTION_TYPE STRING_TYPE)
(PAIR_TYPE PBC_PBOP_TYPE (PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))))
)) res v ∧
case res of
INL err =>
Expand Down Expand Up @@ -146,7 +149,8 @@ val res = translate map_concl_to_string_def;
Definition mk_prob_def:
mk_prob objf = (NONE,objf):mlstring list option #
((int # mlstring pbc$lit) list # int) option #
(pbop # (int # mlstring pbc$lit) list # int) list
(mlstring option #
(pbop # (int # mlstring pbc$lit) list # int)) list
End

val res = translate mk_prob_def;
Expand All @@ -156,10 +160,13 @@ val check_unsat_3 = (append_prog o process_topdecs) `
case parse_and_enc f1 f2 of
Inl err => TextIO.output TextIO.stdErr err
| Inr (n,objf) =>
let val probt = default_prob in
let val probt = default_prob
val prob = mk_prob objf
val prob = strip_annot_prob prob
in
(case
map_concl_to_string n
(check_unsat_top_norm False (mk_prob objf) probt f3) of
(check_unsat_top_norm False prob probt f3) of
Inl err => TextIO.output TextIO.stdErr err
| Inr s => TextIO.print s)
end`
Expand Down Expand Up @@ -212,11 +219,12 @@ Proof
>-
(xvar>>xsimpl)>>
xlet_autop>>
xlet_autop>>
xlet`POSTv v. STDIO fs * &BOOL F v`
>-
(xcon>>xsimpl)>>
drule npbc_parseProgTheory.check_unsat_top_norm_spec>>
qpat_x_assum`prob_TYPE (mk_prob _) _`assume_tac>>
qpat_x_assum`prob_TYPE (strip_annot_prob _) _`assume_tac>>
disch_then drule>>
qpat_x_assum`prob_TYPE default_prob _`assume_tac>>
disch_then drule>>
Expand Down Expand Up @@ -263,14 +271,17 @@ Proof
qexists_tac`strlit ""`>>
rw[]>>simp[STD_streams_stderr,add_stdo_nil]>>
xsimpl>>
fs[oneline pb_parseTheory.strip_annot_prob_def]>>
every_case_tac>>gvs[]>>
(drule_at Any) full_encode_mcis_sem_concl>>
fs[]>>
Cases_on`x`>> disch_then (drule_at Any)>>
disch_then(qspec_then`gt'` mp_tac)>>
impl_tac>-
fs[get_graph_lad_def,AllCaseEqs(),mk_prob_def]>>
rw[]>>
qexists_tac`(q,r)`>>
rename1`(qq,rr)`>>
qexists_tac`(qq,rr)`>>
simp[mcis_sem_def]>>
metis_tac[])
QED
Expand All @@ -283,7 +294,7 @@ Definition check_unsat_2_sem_def:
case get_graph_lad fs f2 of
NONE => out = strlit ""
| SOME gtt =>
out = concat (print_prob
out = concat (print_annot_prob
(mk_prob (full_encode_mcis gpp gtt)))
End

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

Theorem check_unsat_2_spec:
STRING_TYPE f1 f1v ∧ validArg f1 ∧
Expand Down
22 changes: 15 additions & 7 deletions examples/pseudo_bool/array/subgraph_isoProgScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,10 @@ Theorem parse_and_enc_spec:
& ∃res.
SUM_TYPE STRING_TYPE
(LIST_TYPE
(PAIR_TYPE PBC_PBOP_TYPE
(PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT))) res v ∧
(PAIR_TYPE
(OPTION_TYPE STRING_TYPE)
(PAIR_TYPE PBC_PBOP_TYPE
(PAIR_TYPE (LIST_TYPE (PAIR_TYPE INT (PBC_LIT_TYPE STRING_TYPE))) INT)))) res v ∧
case res of
INL err =>
get_graph_lad fs f1 = NONE ∨ get_graph_lad fs f2 = NONE
Expand Down Expand Up @@ -110,7 +112,8 @@ val res = translate (res_to_string_def |> SIMP_RULE std_ss [UNSAT_string_def,SAT
Definition mk_prob_def:
mk_prob fml = (NONE,NONE,fml):mlstring list option #
((int # mlstring pbc$lit) list # int) option #
(pbop # (int # mlstring pbc$lit) list # int) list
(mlstring option #
(pbop # (int # mlstring pbc$lit) list # int)) list
End

val res = translate mk_prob_def;
Expand All @@ -120,9 +123,11 @@ val check_unsat_3 = (append_prog o process_topdecs) `
case parse_and_enc f1 f2 of
Inl err => TextIO.output TextIO.stdErr err
| Inr fml =>
let val probt = default_prob in
let val probt = default_prob
val prob = mk_prob fml
val prob = strip_annot_prob prob in
(case
res_to_string (check_unsat_top_norm False (mk_prob fml) probt f3) of
res_to_string (check_unsat_top_norm False prob probt f3) of
Inl err => TextIO.output TextIO.stdErr err
| Inr s => TextIO.print s)
end`
Expand Down Expand Up @@ -174,6 +179,7 @@ Proof
>-
(xvar>>xsimpl)>>
xlet_autop>>
xlet_autop>>
xlet`POSTv v. STDIO fs * &BOOL F v`
>-
(xcon>>xsimpl)>>
Expand Down Expand Up @@ -225,6 +231,7 @@ Proof
qexists_tac`strlit ""`>>
simp[STD_streams_stderr,add_stdo_nil]>>
xsimpl>>
fs[pb_parseTheory.strip_annot_prob_def]>>
(drule_at Any) full_encode_sem_concl>>
fs[]>>
impl_tac >-
Expand All @@ -239,6 +246,7 @@ Proof
qexists_tac`strlit ""`>>
simp[STD_streams_stderr,add_stdo_nil]>>
xsimpl>>
fs[pb_parseTheory.strip_annot_prob_def]>>
(drule_at Any) full_encode_sem_concl>>
fs[]>>
impl_tac >-
Expand All @@ -264,15 +272,15 @@ Definition check_unsat_2_sem_def:
case get_graph_lad fs f2 of
NONE => out = strlit ""
| SOME gtt =>
out = concat (print_prob (mk_prob (full_encode gpp gtt)))
out = concat (print_annot_prob (mk_prob (full_encode gpp gtt)))
End

val check_unsat_2 = (append_prog o process_topdecs) `
fun check_unsat_2 f1 f2 =
case parse_and_enc f1 f2 of
Inl err => TextIO.output TextIO.stdErr err
| Inr fml =>
TextIO.print_list (print_prob (mk_prob fml))`
TextIO.print_list (print_annot_prob (mk_prob fml))`

Theorem check_unsat_2_spec:
STRING_TYPE f1 f1v ∧ validArg f1 ∧
Expand Down
Loading