From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 11 Jul 2017 16:17:23 +0000 (+0200)
Subject: New: simple backtracking with trail
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec89aa96e6538dd5b566d59c67c7ac9e295e5e25;p=fireball-separation.git

New: simple backtracking with trail

auto_instantiate replaced by choose_step and first
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 95b036c..86194cb 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -12,14 +12,18 @@ let bomb = ref(`Var(-1,-666));;
 *)
 let num_more_args = 2;;
 
+type discriminating_set = (int * nf) list;;
+
 type problem =
  { freshno: int
  ; div: i_var option (* None = bomb *)
  ; conv: i_n_var list (* the inerts that must converge *)
  ; ps: i_n_var list (* the n-th inert must become n *)
  ; sigma: (int * nf) list (* the computed substitution *)
- ; deltas: (int * nf) list ref list (* collection of all branches *)
+ ; deltas: discriminating_set ref list (* collection of all branches *)
  ; initialSpecialK: int
+
+ ; trail: discriminating_set list list
 };;
 
 let all_terms p =
@@ -491,7 +495,7 @@ let compute_special_k tms =
  ) in Listx.max (Listx.map (aux 0) tms)
 ;;
 
-let auto_instantiate (n,p) =
+let choose_step (n,p) =
  let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in
  let x =
   match showstoppers_step, showstoppers_eat with
@@ -546,26 +550,45 @@ in*)
      compute_special_k (Listx.from_list (all_terms p :> nf list) )in
  if special_k < n then
   prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@");
- let p = instantiate p x 1 special_k in
- special_k,p
+ let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in
+ x,arity_of_x,special_k
 
+exception Backtrack
+
+let first bound p var f =
+ let p = {p with trail = (List.map (!) p.deltas)::p.trail} in
+ let rec aux i =
+  if i > bound then
+   (prerr_endline (">>>>>>>>>>>>>>>>>> BACKTRACKING ON "^ string_of_var var ^" J="^ string_of_int i ^" <<<<<<<<<<<<<<<<<<");
+   raise Backtrack)
+  else
+   try
+     f p i
+   with
+    Backtrack ->
+     List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
+     aux (i+1)
+ in
+  aux 1
 
 let rec auto_eat (n,p) =
  prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}";
  let m = problem_measure p in
- let (n,p') = auto_instantiate (n,p) in
- match eat p' with
- | `Finished p -> p
- | `Continue p ->
-     prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}";
-     let delta = problem_measure p - m in
-     (* let delta = m - problem_measure p' in *)
-     if delta >= 0
-      then
-       (failwith
-       ("Measure did not decrease (+=" ^ string_of_int delta ^ ")"))
-      else prerr_endline ("$ Measure decreased of " ^ string_of_int delta);
-     auto_eat (n,p)
+ let x, arity_of, n = choose_step (n,p) in
+ first arity_of p x (fun p j ->
+  let p' = instantiate p x j n in
+  match eat p' with
+  | `Finished p -> p
+  | `Continue p ->
+      prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}";
+      let delta = problem_measure p - m in
+      (* let delta = m - problem_measure p' in *)
+      if delta >= 0
+       then
+        (failwith
+        ("Measure did not decrease (+=" ^ string_of_int delta ^ ")"))
+       else prerr_endline ("$ Measure decreased of " ^ string_of_int delta);
+      auto_eat (n,p))
 ;;
 
 let auto p n =
@@ -681,9 +704,9 @@ let main problems =
      `Step x in
    match cmd with
     | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *)
-    | `Step x ->
-        let x = var_of_string x in
-        aux (instantiate p x 1 n) n l
+    | `Step x -> assert false
+        (* let x = var_of_string x in
+        aux (instantiate p x 1 n) n l *)
     | `Auto -> aux (auto p n) n l
  in
   List.iter
@@ -780,7 +803,7 @@ let magic_conv ~div ~conv ~nums cmds =
  if match div with None -> false | Some div -> List.exists (eta_subterm div) (tms@conv)
  then (
   prerr_endline "--- TEST SKIPPED ---";
-  {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0}, 0, []
+  {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0; trail=[]}, 0, []
  ) else
   let tms = sort_uniq ~compare:eta_compare tms in
   let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *)
@@ -794,8 +817,8 @@ let magic_conv ~div ~conv ~nums cmds =
   let deltas =
    let dummy = `Var (max_int / 2, -666) in
     [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
-
-  {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}, special_k, cmds
+  let trail = [] in
+  {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail}, special_k, cmds
 ;;
 
 let magic strings cmds = magic_conv None [] strings cmds;;