fix the hint

CakeML · Sep 20, 2020 · 26dcb39 · 26dcb39
1 parent 0a378af
commit 26dcb39
Show file tree

Hide file tree

Showing 3 changed files with 68 additions and 53 deletions.
diff --git a/examples/lpr_checker/array/lpr_arrayProgScript.sml b/examples/lpr_checker/array/lpr_arrayProgScript.sml
@@ -1476,24 +1476,31 @@ Proof
   xapp>>xsimpl
 QED
 
+val _ = translate list_min_aux_def;
+
+val _ = translate list_min_def;
+
 val hint_earliest_arr = process_topdecs`
   fun hint_earliest_arr c w ik fml inds earr =
   case w of
     None =>
-    (case ik of [] => earr
-    | nid::rest =>
+    let val lm = list_min ik in
+    if lm = 0 then earr
+    else
       let val p = safe_hd c
           val ip = index (~p) in
-      if Array.length earr <= ip then earr
-      else
-      (case Unsafe.sub earr ip of
-        None => earr
-      | Some mini =>
-        if check_earliest_arr fml (~p) mini (fst nid) inds
-        then
-          resize_update_arr (Some (fst nid)) ip earr
-        else earr)
-      end)
+          if Array.length earr <= ip then earr
+          else
+          (case Unsafe.sub earr ip of
+            None => earr
+          | Some mini =>
+            if check_earliest_arr fml (~p) mini lm inds
+            then
+              resize_update_arr (Some lm) ip earr
+            else
+              earr)
+      end
+    end
   | Some u => earr` |> append_prog
 
 Theorem hint_earliest_arr_spec:
@@ -1517,17 +1524,15 @@ Proof
   rw[]>>xcf "hint_earliest_arr" (get_ml_prog_state ())>>
   fs[hint_earliest_def]>>
   reverse TOP_CASE_TAC>>fs[OPTION_TYPE_def]>>xmatch
-  >-
-    (xvar>>xsimpl)>>
-  TOP_CASE_TAC>>fs[LIST_TYPE_def]>>xmatch
-  >-
-    (xvar>>xsimpl)>>
+  >- (xvar>>xsimpl)>>
+  rpt xlet_autop>>
+  xif
+  >- (xvar>>xsimpl)>>
   rpt xlet_autop>>
   simp[list_lookup_def]>>
   `LENGTH earliest = LENGTH earliestv` by metis_tac[LIST_REL_LENGTH]>>
   xif>>fs[]
-  >-
-    (xvar>>xsimpl)>>
+  >- (xvar>>xsimpl)>>
   xlet_autop>>
   `OPTION_TYPE NUM (EL (index (-safe_hd c)) earliest) (EL (index (-safe_hd c)) earliestv)` by fs[LIST_REL_EL_EQN]>>
   TOP_CASE_TAC>>fs[OPTION_TYPE_def]>>
@@ -1536,15 +1541,13 @@ Proof
     (xvar>>xsimpl)>>
   rpt xlet_autop>>
   reverse xif>>fs[]
-  >-
-    (xvar>>xsimpl)>>
-  xlet_autop>>
+  >- (xvar>>xsimpl)>>
   xlet_autop>>
   xapp_spec (resize_update_arr_spec |> Q.GEN `vty` |> ISPEC ``NUM``)>>
   xsimpl>>
   asm_exists_tac>>simp[]>>
   asm_exists_tac>>simp[]>>
-  qexists_tac`SOME (FST h)`>>
+  qexists_tac`SOME (list_min ik)`>>
   simp[OPTION_TYPE_def]
 QED
 

diff --git a/examples/lpr_checker/array/lpr_listScript.sml b/examples/lpr_checker/array/lpr_listScript.sml
@@ -334,20 +334,32 @@ val check_earliest_def = Define`
       check_earliest fml x old new is
   else T)`
 
+val list_min_aux_def = Define`
+  (list_min_aux min [] = min) ∧
+  (list_min_aux min ((i,_)::is) =
+      list_min_aux (MIN min i) is)`
+
+(* Note that clauses are 1 indexed *)
+val list_min_def = Define`
+  list_min ls =
+  case ls of [] => 0
+  | (x::xs) => list_min_aux (FST x) xs`
+
 val hint_earliest_def = Define`
   hint_earliest C (w:int list option) (ik:(num # num list) list) fml inds earliest =
   case w of
     NONE =>
-    (case ik of [] => earliest
-    | nid::_ =>
-      (* RAT *)
-      let p = safe_hd C in
-      case list_lookup earliest NONE (index (~p)) of
-        NONE => earliest
-      | SOME mini => (* The current mini index of ~p *)
-        if check_earliest fml (~p) mini (FST nid) inds
-        then resize_update_list earliest NONE (SOME (FST nid)) (index (~p))
-        else earliest)
+    (let lm = list_min ik in
+      if lm = 0 then earliest
+      else
+        (* RAT *)
+        let p = safe_hd C in
+        case list_lookup earliest NONE (index (~p)) of
+          NONE => earliest
+        | SOME mini => (* The current mini index of ~p *)
+          if check_earliest fml (~p) mini lm inds
+          then resize_update_list earliest NONE (SOME lm) (index (~p))
+          else earliest)
   | SOME _ => earliest`
 
 val check_lpr_step_list_def = Define`

diff --git a/examples/lpr_checker/ramseyScript.sml b/examples/lpr_checker/ramseyScript.sml
@@ -847,27 +847,27 @@ QED
 (* Ramsey number 3 is 6 *)
 
 val lpr = ``[
-  Delete []; PR 41 [-12; -14; -15] NONE [39; 38; 40; 17] LN; Delete [17];
-  PR 42 [-9; -14; -15] NONE [35; 36; 40; 14] LN; Delete [14];
-  PR 43 [-5; -14; -15] NONE [30; 29; 40; 8] LN; Delete [40; 8];
-  PR 44 [-14; -15] NONE [43; 42; 4; 41; 13; 7; 21] LN;
-  Delete [43; 42; 41; 21]; PR 45 [9; 5; 14] NONE [15; 4; 9; 22] LN;
-  Delete [22]; PR 46 [12; 5; 14] NONE [18; 7; 9; 25] LN; Delete [25];
-  PR 47 [5; -15] NONE [44; 45; 36; 46; 39; 33; 12] LN; Delete [45; 46; 12];
-  PR 48 [-12; -15] NONE [47; 30; 27; 39; 6] LN; Delete [39; 6];
-  PR 49 [-9; -15] NONE [36; 47; 24; 30; 3] LN; Delete [36; 47; 30; 3];
-  PR 50 [-15] NONE [49; 48; 13; 44; 15; 18; 31] LN;
-  Delete [49; 48; 44; 31]; PR 51 [12; 9] NONE [50; 19; 16; 13; 32] LN;
-  Delete [13; 32]; PR 52 [14; 9] NONE [50; 20; 16; 15; 34] LN;
-  Delete [15; 34]; PR 53 [-5; -12; -14] NONE [27; 29; 38; 5] LN;
-  Delete [5]; PR 54 [9] NONE [50; 51; 52; 16; 53; 10; 23; 4] LN;
+  Delete []; PR 41 [-12; -14; -15] NONE [39; 38; 40; 17] []; Delete [17];
+  PR 42 [-9; -14; -15] NONE [35; 36; 40; 14] []; Delete [14];
+  PR 43 [-5; -14; -15] NONE [30; 29; 40; 8] []; Delete [40; 8];
+  PR 44 [-14; -15] NONE [43; 42; 4; 41; 13; 7; 21] [];
+  Delete [43; 42; 41; 21]; PR 45 [9; 5; 14] NONE [15; 4; 9; 22] [];
+  Delete [22]; PR 46 [12; 5; 14] NONE [18; 7; 9; 25] []; Delete [25];
+  PR 47 [5; -15] NONE [44; 45; 36; 46; 39; 33; 12] []; Delete [45; 46; 12];
+  PR 48 [-12; -15] NONE [47; 30; 27; 39; 6] []; Delete [39; 6];
+  PR 49 [-9; -15] NONE [36; 47; 24; 30; 3] []; Delete [36; 47; 30; 3];
+  PR 50 [-15] NONE [49; 48; 13; 44; 15; 18; 31] [];
+  Delete [49; 48; 44; 31]; PR 51 [12; 9] NONE [50; 19; 16; 13; 32] [];
+  Delete [13; 32]; PR 52 [14; 9] NONE [50; 20; 16; 15; 34] [];
+  Delete [15; 34]; PR 53 [-5; -12; -14] NONE [27; 29; 38; 5] [];
+  Delete [5]; PR 54 [9] NONE [50; 51; 52; 16; 53; 10; 23; 4] [];
   Delete [51; 52; 16; 53; 23; 4];
-  PR 55 [-12; -14] NONE [54; 33; 35; 38; 11] LN; Delete [38; 11];
-  PR 56 [5; 12] NONE [50; 10; 19; 7; 26] LN; Delete [7; 26];
-  PR 57 [-14] NONE [54; 55; 35; 56; 24; 29; 2] LN;
-  Delete [55; 35; 56; 29; 2]; PR 59 [12] NONE [50; 57; 20; 18; 19; 37] LN;
-  Delete [18; 19; 37]; PR 61 [-5] NONE [54; 59; 33; 24; 27; 1] LN;
-  Delete [33; 24; 27; 1]; PR 65 [] NONE [50; 57; 20; 61; 9; 10; 28] LN
+  PR 55 [-12; -14] NONE [54; 33; 35; 38; 11] []; Delete [38; 11];
+  PR 56 [5; 12] NONE [50; 10; 19; 7; 26] []; Delete [7; 26];
+  PR 57 [-14] NONE [54; 55; 35; 56; 24; 29; 2] [];
+  Delete [55; 35; 56; 29; 2]; PR 59 [12] NONE [50; 57; 20; 18; 19; 37] [];
+  Delete [18; 19; 37]; PR 61 [-5] NONE [54; 59; 33; 24; 27; 1] [];
+  Delete [33; 24; 27; 1]; PR 65 [] NONE [50; 57; 20; 61; 9; 10; 28] []
   ]``;
 
 val thm = EVAL ``check_lpr_unsat ^lpr (ramsey_lpr 3 6)``