further improvments to the opt of BDD

Author: AnoudAlshnakat

hol/policy_to_table/bdd_end_to_endScript.sml

@@ -773,8 +773,8 @@ End
 
 Definition correct_var_policy_var_tables_exec2_def:
   correct_var_policy_var_tables_exec2 var_policy var_table vars I =
-  let BDD1_opt = mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, var_policy))]) [] vars 1 in
-    let BDD2_opt = mk_BDDPred_opt table_structure_new  (0,[],[(0, non_termn (NONE, var_table ))]) [] vars 1 in
+  let BDD1_opt = mk_BDDPred_opt_new policy_structure (0,[],[(0, non_termn (NONE, var_policy))]) [] vars 1 in
+    let BDD2_opt = mk_BDDPred_opt_new table_structure_new  (0,[],[(0, non_termn (NONE, var_table ))]) [] vars 1 in
       if  ~ IS_SOME(BDD1_opt) \/  ~ IS_SOME (BDD2_opt) then
 	    T
       else let BDD1 = THE BDD1_opt in let BDD2 = THE BDD2_opt in

hol/policy_to_table/bdd_genScript.sml

@@ -602,6 +602,7 @@ Definition has_parent_def:
 End
 
 
+(* TODO: remove lookup *)
 Definition eliminable_def:
   eliminable ((r,edges,labels):('a,'b)BDD) n = 
     case ALOOKUP edges n of
@@ -658,7 +659,15 @@ End
 
 
 
+(*
+Definition edges_project_def:
+  edges_project ((r,edges,labels):('a,'b)BDD) nl = 
+    everything in nl is in the domain od edges'
+End
+*)
 
+
+(* here we use the projection *)
 
 (* eliminate part *) 
 Definition eliminate_BDD_def:
@@ -1099,6 +1108,7 @@ End
 
 (******************* new better optimized definitions ***************************)
 
+val _ = type_abbrev("distrub_st", ``:( (string, (num list) option) alist   # num list # num list)``);
 
 
 Definition update_internals_def:
@@ -1160,7 +1170,6 @@ End
 
 
 
-(* can be improved more *)
 
 (* can be improved more *)
 Definition optimize_node_def:

hol/policy_to_table/fwd_proofLib.sml

@@ -103,7 +103,7 @@ open bdd_utilsLib;
 
 
         (* create BDD of var policy  *)
-        val eval_policy_full_opt = EVAL “mk_BDDPred_opt policy_structure (0,[],[(0, non_termn (NONE, ^var_policy))]) [] ^policy_order 1”;
+        val eval_policy_full_opt = EVAL “mk_BDDPred_opt_new policy_structure (0,[],[(0, non_termn (NONE, ^var_policy))]) [] ^policy_order 1”;
         val eval_policy_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy_full_opt));
 
         val _ = time_stage ("Stage 2 from var policy to BDD", start_cpu_stage2, start_real_stage2);
@@ -124,7 +124,7 @@ open bdd_utilsLib;
         val eval_table_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table_full_opt_auto));
 *)
 
-        val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt table_structure_new (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ^policy_order 1”;
+        val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt_new table_structure_new (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ^policy_order 1”;
         val eval_table_full_opt_auto_rhs = optionSyntax.dest_some (rhs (concl eval_table_full_opt_auto));
 
         val _ = time_stage ("Stage 2 from table to table BDD", start_cpu_stage2_tbl, start_real_stage2_tbl);