Minor updates (bug fix, remove redundant code)

src/cache.ml

@@ -119,7 +119,7 @@ let store_eq_var ctx lr =
 
 let store_eq_vars ctx rls = List.iter (ignore <.> store_eq_var ctx) rls
 
-let rule_var ctx rl = try find_rule rl with Not_found -> store_rule_var ctx rl
+let rule_var ctx rl = try H.find ht_rl_vars rl with Not_found -> store_rule_var ctx rl
 
 let eq_variant (l,r) st = Rule.variant st (l,r) || Rule.variant st (r,l)
 

src/ckb_AC.ml

@@ -60,8 +60,8 @@ let max_constraints s =
 ;;
 
 (* shorthands for settings *)
-let termination_strategy s = 
-  match s.heuristic.strategy with 
+let termination_strategy s =
+  match s.heuristic.strategy with
   | [] -> failwith "no termination strategy found"
   | (s, _, _, _, _) :: _ -> s
 ;;
@@ -112,7 +112,7 @@ let rewrite rr aa =
   L.fold_left rew_nf (NS.empty (), NS.empty ()) (NS.to_list aa)
 ;;
 
-let reduced rr aa = 
+let reduced rr aa =
  let ls_old, ls_new = rewrite rr (NS.of_list aa) in NS.add_all ls_new ls_old
 ;;
 
@@ -193,7 +193,7 @@ let max_k s =
   let ctx, cc = s.context, s.equations in
   let k = s.heuristic.k !(A.iterations) in
   let cc_eq = [ Lit.terms n | n <- NS.to_list cc ] in
-  let cc_symm = [n | n <- NS.to_list (NS.symmetric cc)] in 
+  let cc_symm = [n | n <- NS.to_list (NS.symmetric cc)] in
   let cc_symml = [Lit.terms c | c <- cc_symm] in
   L.iter (fun n -> ignore (C.store_rule_var ctx n)) cc_symml;
   (* lookup is not for free: get these variables only once *)
@@ -273,6 +273,7 @@ let preorient state es =
 ;;
 
 let complete (settings, heuristic) es =
+  A.restart ();
   let es = [Lit.make_axiom (normalize (Lit.terms e)) | e <- es] in
   let ctx = Logic.mk_context () in
   let ss = L.map (fun (ts,_,_,_,_) -> ts) heuristic.strategy in

src/rewriting/rewriting.ml

@@ -13,15 +13,13 @@ let rec rewrite_aux rules = function
   | F (f, ts) ->
       let tpls = [ rewrite_aux rules ti | ti <- ts ] in
       let ls = [ ti | _, ti <- tpls ] in
-      let used_rules = Listx.unique (List.flatten (List.map fst tpls)) in 
+      let used_rules = Listx.unique (List.flatten (List.map fst tpls)) in
       if used_rules <> [] then used_rules, F (f, ls)
       else
        let opt, u = rewrite_at_root (F (f, ls)) rules in
        match opt with
         | None -> used_rules, u
-        | Some lr -> 
-	  if List.mem lr used_rules 
-	  then used_rules, u else (lr :: used_rules), u
+        | Some lr -> [lr], u
 ;;
 
 let step_at_with t p (l,r) =
@@ -32,7 +30,7 @@ let step_at_with t p (l,r) =
 
 let rec nf rules t =
  let used, u = rewrite_aux rules t in
- match used with 
+ match used with
  | [] -> t
  | _ -> nf rules u