Implement selection of disjunction variables for EDDs.

Next (?) : leaves can store information on evars.

1 files changed, 9 insertions, 2 deletions

diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index cf29edf..bcfa77a 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -17,6 +17,7 @@ type varenv = {
 
     last_vars     : (bool * id * typ) list;
     all_vars      : (bool * id * typ) list;
+    d_vars        : id list;
 
     cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
     forget        : (id * typ) list;          (* s'(x) not specified *)
@@ -228,7 +229,7 @@ let force_ordering vars groups =
   - cycle, forget
 *)
 
-let mk_varenv (rp : rooted_prog) f cl =
+let mk_varenv (rp : rooted_prog) disj_fun f cl =
     (* add variables from LASTs *)
     let last_vars = uniq_sorted 
       (List.sort compare (extract_last_vars f)) in
@@ -311,6 +312,12 @@ let mk_varenv (rp : rooted_prog) f cl =
           not (List.exists (fun (_, b, _) -> b = id) cycle))
         all_vars) in
 
-    { evars = enum_vars; nvars = num_vars; ev_order;
+    (* use specified disjunction variables *)
+    let d_vars = List.filter disj_fun
+        (List.map (fun (id, _) -> id) enum_vars) in
+    Format.printf "Disjunction variables: @[<hov>[%a]@]@."
+      (print_list Formula_printer.print_id ", ") d_vars;
+
+    { evars = enum_vars; nvars = num_vars; ev_order; d_vars;
       last_vars; all_vars; cycle; forget; forget_inv }