From bbe2c97e876259d08b32a544a8556820338d8314 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Thu, 18 Jan 2024 10:58:13 +0800 Subject: [PATCH] de-duplicate in wcnf_to_pb, better errors --- .../array/npbc_arrayProgScript.sml | 152 +++++++++++------- examples/pseudo_bool/array/wcnfProgScript.sml | 3 +- .../cnf_encoding/wcnf_to_pbScript.sml | 38 +++-- 3 files changed, 125 insertions(+), 68 deletions(-) diff --git a/examples/pseudo_bool/array/npbc_arrayProgScript.sml b/examples/pseudo_bool/array/npbc_arrayProgScript.sml index 1259a32f0b..7f0190bc77 100644 --- a/examples/pseudo_bool/array/npbc_arrayProgScript.sml +++ b/examples/pseudo_bool/array/npbc_arrayProgScript.sml @@ -1481,10 +1481,11 @@ val r = translate splim_def; val every_hs = process_topdecs` fun every_hs hs ls = - case ls of [] => True + case ls of [] => None | l::ls => - in_hashset_arr l hs andalso - every_hs hs ls` |> append_prog + if in_hashset_arr l hs then + every_hs hs ls + else Some (npbc_string l)` |> append_prog Theorem every_hs_spec: ∀ls lsv. @@ -1498,26 +1499,30 @@ Theorem every_hs_spec: (ARRAY hspv hsv) (POSTv resv. ARRAY hspv hsv * - &BOOL (EVERY (λc. in_hashset c hs) ls) resv) + & ∃err. + OPTION_TYPE STRING_TYPE + (if EVERY (λc. in_hashset c hs) ls + then NONE else SOME err) resv) Proof Induct>>rw[]>> fs[LIST_TYPE_def]>> xcf "every_hs" (get_ml_prog_state ())>> xmatch - >- (xcon>>xsimpl)>> + >- (xcon>>xsimpl>>EVAL_TAC)>> xlet_auto>> - xlog>> - xsimpl>>rw[] - >- ( - xapp>>xsimpl>> - pairarg_tac>>fs[])>> - gvs[] + xif + >- + (xapp>>xsimpl)>> + xlet_autop>> + xcon>>xsimpl>> + simp[OPTION_TYPE_def]>> + metis_tac[] QED val hash_check = process_topdecs` fun hash_check fmlls proved lf = case lf of - [] => True + [] => None | _ => let val hs = Array.array splim [] @@ -1544,10 +1549,12 @@ Theorem hash_check_spec: [xv; yv; lsv] emp (POSTv resv. - &BOOL ( - let hs = mk_hashset x + & ∃err. + OPTION_TYPE STRING_TYPE + (let hs = mk_hashset x (mk_hashset y (REPLICATE splim [])) in - EVERY (λc. in_hashset c hs) ls) resv) + if EVERY (λc. in_hashset c hs) ls + then NONE else SOME err) resv) Proof rw[]>> xcf "hash_check" (get_ml_prog_state ())>> @@ -1555,7 +1562,8 @@ Proof >- ( fs[LIST_TYPE_def]>> xmatch>> - xcon>>xsimpl)>> + xcon>>xsimpl>> + EVAL_TAC)>> fs[LIST_TYPE_def]>> xmatch>> xlet_autop>> @@ -1631,7 +1639,7 @@ val res = translate red_cond_check_pure_def; val red_cond_check = process_topdecs` fun red_cond_check indfml extra pfs rsubs goals = case red_cond_check_pure extra pfs rsubs goals of - None => False + None => Some "not all # subgoals present" | Some (x,ls) => hash_check indfml x ls` |> append_prog @@ -1649,18 +1657,22 @@ Theorem red_cond_check_spec: [av; aav; bv; cv; dv] emp (POSTv resv. - &BOOL (red_cond_check a aa b c d) resv) + & ∃err. + OPTION_TYPE STRING_TYPE + (if red_cond_check a aa b c d then NONE + else SOME err) resv) Proof rw[]>> xcf "red_cond_check" (get_ml_prog_state ())>> fs[]>> xlet_autop>> simp[red_cond_check_eq]>> - TOP_CASE_TAC>>fs[OPTION_TYPE_def] + Cases_on`red_cond_check_pure aa b c d`>> + fs[OPTION_TYPE_def] >- ( xmatch>> xcon>>xsimpl)>> - TOP_CASE_TAC>>fs[PAIR_TYPE_def]>> + Cases_on`x`>>fs[PAIR_TYPE_def]>> xmatch>> xapp>> xsimpl>> @@ -1749,10 +1761,10 @@ val check_red_arr = process_topdecs` None => let val u = rollback_arr fml' id id' val goals = subst_indexes_arr s bortcb fml' rinds in - if red_cond_check fmlls nc pfs rsubs goals - then - (fml', (rinds,id')) - else raise Fail (format_failure_2 lno ("Redundancy subproofs did not cover all subgoals.") (print_subproofs_err rsubs goals)) + case red_cond_check fmlls nc pfs rsubs goals + of None => (fml', (rinds,id')) + | Some err => + raise Fail (format_failure_2 lno ("Redundancy subproofs did not cover all subgoals. Info: " ^ err ^ ".") (print_subproofs_err rsubs goals)) end | Some cid => if check_contradiction_fml_arr b fml' cid then @@ -1950,20 +1962,23 @@ Proof >- ( rpt xlet_autop>> fs[do_red_check_def]>> - reverse xif + pop_assum mp_tac>>IF_CASES_TAC>> + strip_tac>>fs[OPTION_TYPE_def]>>xmatch + >- ( + fs[red_cond_check_def]>> + pairarg_tac>>fs[]>> + xlet_autop>> + xcon>>xsimpl>> + simp[PAIR_TYPE_def]>> + xsimpl) >- ( rpt xlet_autop>> fs[red_cond_check_def]>> xraise>> xsimpl>> rw[]>>fs[]>> - metis_tac[ARRAY_refl,NOT_EVERY,Fail_exn_def]) >> - fs[red_cond_check_def]>> - pairarg_tac>>fs[]>> - xlet_autop>> - xcon>>xsimpl>> - simp[PAIR_TYPE_def]>> - xsimpl)>> + metis_tac[ARRAY_refl,NOT_EVERY,Fail_exn_def]) + )>> rpt xlet_autop>> reverse xif >- ( @@ -2303,10 +2318,10 @@ val check_dom_arr = process_topdecs` None => let val u = rollback_arr fml' id id' val goals = core_subgoals s corels in - if red_cond_check fmlls nc pfs dsubs goals - then - (fml',(rinds,id')) - else raise Fail (format_failure_2 lno ("Dominance subproofs did not cover all subgoals") (print_subproofs_err dsubs goals)) + case red_cond_check fmlls nc pfs dsubs goals of + None => (fml',(rinds,id')) + | Some err => + raise Fail (format_failure_2 lno ("Dominance subproofs did not cover all subgoals. Info: " ^ err ^ ".") (print_subproofs_err dsubs goals)) end | Some cid => if check_contradiction_fml_arr False fml' cid then @@ -2446,20 +2461,23 @@ Proof xmatch >- ( rpt xlet_autop>> - reverse xif>>gs[] + pop_assum mp_tac>>IF_CASES_TAC>> + strip_tac>>fs[OPTION_TYPE_def]>>xmatch + >- ( + xlet_autop>> + xcon>>xsimpl>> + pairarg_tac>>fs[red_cond_check_def,core_subgoals_def]>> + fs[PAIR_TYPE_def,OPTION_TYPE_def]>> + xsimpl) >- ( rpt xlet_autop>> fs[red_cond_check_def]>>pairarg_tac>>fs[core_subgoals_def]>> xraise>>xsimpl>> fs[red_cond_check_def]>>rw[]>> - metis_tac[ARRAY_refl,Fail_exn_def,NOT_EVERY])>> - xlet_autop>> - xcon>>xsimpl>> - pairarg_tac>>fs[red_cond_check_def,core_subgoals_def]>> - fs[PAIR_TYPE_def,OPTION_TYPE_def]>> - xsimpl)>> - rpt xlet_autop>> + metis_tac[ARRAY_refl,Fail_exn_def,NOT_EVERY]) + )>> rename1`check_contradiction_fml_list F A B`>> + xlet_autop>> xlet`POSTv v. ARRAY fmlv' fmllsv' * & BOOL (check_contradiction_fml_list F A B) v` @@ -3616,7 +3634,10 @@ Theorem fml_include_arr_spec: [lsv; rsv] (emp) (POSTv v. - &BOOL (fml_include_list ls rs) v) + & ∃err. + OPTION_TYPE STRING_TYPE + (if fml_include_list ls rs + then NONE else SOME err) v) Proof rw[fml_include_list_def]>> xcf"fml_include_arr"(get_ml_prog_state ())>> @@ -3636,24 +3657,33 @@ QED val _ = register_type ``:output`` +Definition print_opt_string_def: + (print_opt_string NONE = strlit"T") ∧ + (print_opt_string (SOME s) = s) +End + +val res = translate print_opt_string_def; + Definition derivable_res_def: - derivable_res (dbound :int option) b2 = + derivable_res (dbound :int option) b2opt = let b1 = (dbound = NONE) in + let b2 = (b2opt = NONE) in if b1 ∧ b2 then NONE else SOME ( strlit "output DERIVABLE check failed:" ^ strlit " [dbound = NONE] " ^ bool_to_string b1 ^ - strlit " [core in output] " ^ bool_to_string b2 - ) + strlit " [core in output] " ^ print_opt_string b2opt) End val res = translate derivable_res_def; Definition equisatisfiable_res_def: equisatisfiable_res - (bound:int option) (dbound:int option) chk b2 b3 = + (bound:int option) (dbound:int option) chk b2opt b3opt = let b11 = (bound = NONE) in let b12 = (dbound = NONE) in + let b2 = (b2opt = NONE) in + let b3 = (b3opt = NONE) in if b11 ∧ b12 ∧ chk ∧ b2 ∧ b3 then NONE else SOME ( @@ -3661,8 +3691,8 @@ Definition equisatisfiable_res_def: strlit " [bound = NONE] " ^ bool_to_string b11 ^ strlit " [dbound = NONE] " ^ bool_to_string b12 ^ strlit " [checked deletion] " ^ bool_to_string chk ^ - strlit " [core in output] " ^ bool_to_string b2 ^ - strlit " [output in core] " ^ bool_to_string b3 + strlit " [core in output] " ^ print_opt_string b2opt ^ + strlit " [output in core] " ^ print_opt_string b3opt ) End @@ -3670,21 +3700,33 @@ val res = translate equisatisfiable_res_def; val res = translate npbc_checkTheory.opt_eq_obj_def; +Definition opt_err_obj_check_string_def: + (opt_err_obj_check_string (SOME fc) (SOME fc') = + err_obj_check_string (SOME fc) fc') ∧ + (opt_err_obj_check_string _ _ = strlit "missing objective") +End + +val res = translate opt_err_obj_check_string_def; + Definition equioptimal_res_def: equioptimal_res (bound:int option) (dbound:int option) chk - obj obj' b2 b3 = + obj obj' b2opt b3opt = let b11 = opt_le bound dbound in let b12 = opt_eq_obj obj obj' in + let b12s = + if b12 then strlit"T" else opt_err_obj_check_string obj obj' in + let b2 = (b2opt = NONE) in + let b3 = (b3opt = NONE) in if b11 ∧ b12 ∧ chk ∧ b2 ∧ b3 then NONE else SOME ( strlit "output EQUIOPTIMAL check failed:" ^ strlit " [bound <= dbound]: " ^ bool_to_string b11 ^ - strlit " [obj = output obj]: " ^ bool_to_string b12 ^ + strlit " [obj = output obj]: " ^ b12s ^ strlit " [checked deletion]: " ^ bool_to_string chk ^ - strlit " [core in output]: " ^ bool_to_string b2 ^ - strlit " [output in core]: " ^ bool_to_string b3 + strlit " [core in output] " ^ print_opt_string b2opt ^ + strlit " [output in core] " ^ print_opt_string b3opt ) End diff --git a/examples/pseudo_bool/array/wcnfProgScript.sml b/examples/pseudo_bool/array/wcnfProgScript.sml index 3de566de04..4d6f59aeb3 100644 --- a/examples/pseudo_bool/array/wcnfProgScript.sml +++ b/examples/pseudo_bool/array/wcnfProgScript.sml @@ -271,12 +271,13 @@ QED val res = translate enc_lit_def; val res = translate enc_clause_def; val res = translate pbcTheory.negate_def; +val res = translate (nub_def |> SIMP_RULE std_ss [MEMBER_INTRO]); val res = translate wclause_to_pbc_def; val wclause_to_pbc_side = Q.prove(` wclause_to_pbc_side x <=> T`, EVAL_TAC>>rw[]>> - fs[quantHeuristicsTheory.LIST_LENGTH_1])|>update_precondition; + CCONTR_TAC>>fs[]) |>update_precondition; val res = translate miscTheory.enumerate_def; val res = translate wfml_to_pbf_def; diff --git a/examples/pseudo_bool/cnf_encoding/wcnf_to_pbScript.sml b/examples/pseudo_bool/cnf_encoding/wcnf_to_pbScript.sml index 26dadf3e50..2c3efdbc75 100644 --- a/examples/pseudo_bool/cnf_encoding/wcnf_to_pbScript.sml +++ b/examples/pseudo_bool/cnf_encoding/wcnf_to_pbScript.sml @@ -83,7 +83,7 @@ End ≤ 1 PB constraints and ≤ 1 terms in the objective *) Definition wclause_to_pbc_def: wclause_to_pbc (i,n,C) = - let C = FILTER (λl. l ≠ 0) C in + let C = nub (FILTER (λl. l ≠ 0) C) in if n = 0 then (* hard clauses *) ([(GreaterEqual,enc_clause C,1:int)],[]) else (* soft clauses *) @@ -239,6 +239,19 @@ Proof metis_tac[interp_cclause_FILTER] QED +Theorem weight_clause_nub: + weight_clause f (q,nub C) = + weight_clause f (q,C) +Proof + rw[weight_clause_def,interp_cclause_def] +QED + +Theorem interp_cclause_nub: + interp_cclause (nub C) = interp_cclause C +Proof + rw[interp_cclause_def] +QED + (* The sum of weights for unsatisfied clauses is upper bounded by the (negated) obj *) Theorem weight_clause_obj_upper: @@ -264,7 +277,7 @@ Proof fs[Abbr`C`,wf_clause_def,MEM_FILTER]>> `weight_clause (λx. w (INL x)) (q,r) = weight_clause (λx. w (INL x)) (q,C)` by - metis_tac[Abbr`C`,weight_clause_FILTER]>> + metis_tac[Abbr`C`,weight_clause_FILTER,weight_clause_nub]>> rw[]>>simp[weight_clause_def,iSUM_def] >- ( Cases_on`C`>>fs[]>> @@ -307,6 +320,7 @@ Proof Cases_on`EL n wfml`>> fs[wclause_to_pbc_def]>> strip_tac>>simp[Once interp_cclause_FILTER]>> + PURE_ONCE_REWRITE_TAC[GSYM interp_cclause_nub]>> match_mp_tac satisfies_pbc_satisfies_clause>> simp[wf_clause_def,MEM_FILTER])>> drule_all weight_clause_obj_upper>> @@ -359,14 +373,15 @@ Proof rw[] >- ( match_mp_tac satisfies_clause_satisfies_pbc>> - simp[GSYM interp_cclause_FILTER]>> - first_x_assum drule>>simp[wf_clause_def,MEM_FILTER])>> + simp[interp_cclause_nub,GSYM interp_cclause_FILTER]>> + first_x_assum drule>> + simp[wf_clause_def,MEM_FILTER])>> (* For the non-hard clauses *) Cases_on`satisfies_clause w (interp_cclause r)`>> simp[satisfies_pbc_def,eval_lin_term_def,iSUM_def]>> simp[GSYM eval_lin_term_def] >- ( - fs[Once interp_cclause_FILTER]>> + fs[Once interp_cclause_FILTER,Once (GSYM interp_cclause_nub)]>> drule_at Any satisfies_clause_satisfies_pbc>> simp[satisfies_pbc_def]>> disch_then match_mp_tac>> @@ -396,15 +411,14 @@ Proof `wf_clause C` by fs[Abbr`C`,wf_clause_def,MEM_FILTER]>> rw[]>>fs[iSUM_def]>> + `satisfies_clause w (interp_cclause r) = + satisfies_clause w (interp_cclause C)` by + metis_tac[Abbr`C`,interp_cclause_nub,interp_cclause_FILTER]>> + gvs[]>> ( Cases_on`C`>>fs[]>> - fs[Once interp_cclause_FILTER]>> gvs[interp_cclause_def,wf_clause_def,interp_lit_def,enc_lit_def]>> - rw[]>>fs[satisfies_clause_def,satisfies_literal_def]>> - IF_CASES_TAC>> - gvs[interp_cclause_def,satisfies_clause_def,wf_clause_def]>> - rw[enc_lit_def]>>fs[interp_lit_def,satisfies_literal_def]>> - intLib.ARITH_TAC))>> + rw[]>>fs[satisfies_clause_def,satisfies_literal_def]))>> pop_assum (qspec_then`k+1` sym_sub_tac)>> AP_TERM_TAC>> rw[MAP_EQ_f,MEM_FLAT,MEM_MAP,PULL_EXISTS]>> @@ -679,7 +693,7 @@ End strlit"h 1 2 3 4 0"; strlit"1 -3 -5 6 7 0"; strlit"6 -1 -2 0"; - strlit"4 1 6 -7 0";]`` + strlit"4 1 6 -7 6 -7 0";]`` val enc = EVAL`` full_encode (THE ^(rconc wcnf))`` *)