diff --git a/lib/BddUtil.ml b/lib/BddUtil.ml
index ce18d69..b0bdeef 100644
--- a/lib/BddUtil.ml
+++ b/lib/BddUtil.ml
@@ -35,8 +35,8 @@ let dump_dot (m: name_map) (b:Bdd.dt) =
       name in
   Format.printf "digraph D {\n";
   let _ : String.t = dump_dot_h m b (Hashtbl.Poly.create ()) in
-  Format.printf "}"
-
+  Format.printf "}";
+  Format.print_flush ()
 
 
 (** prints a dotfile to the console *)
@@ -76,4 +76,4 @@ let dump_dot_multiroot (m: name_map) (b: Bdd.dt VarState.btree) : String.t =
       let l_s = print_h s (Format.sprintf "%sl" curlbl) l in
       print_h l_s (Format.sprintf "%sr" curlbl) r
   in
-  Format.sprintf "digraph D { %s } " (print_h "" "" b)
+  Format.sprintf "digraph D { %s } " (print_h "" "" b)
\ No newline at end of file
diff --git a/lib/Compiler.ml b/lib/Compiler.ml
index db0a08e..cea423e 100644
--- a/lib/Compiler.ml
+++ b/lib/Compiler.ml
@@ -2,19 +2,27 @@ open Core
 open Cudd
 open Wmc
 open VarState
-open CoreGrammar
 
-let flip_id = ref 1
+module CG = CoreGrammar
+module VO = VarOrder
+
+(* let flip_id = ref 1 *)
+
+type subst = (Bdd.dt * Bdd.dt) List.t
 
 (** Result of compiling an expression *)
 type compiled_expr = {
   state: Bdd.dt btree;
   z: Bdd.dt;
-  flips: Bdd.dt List.t}
+  subst: subst;
+  flips: Bdd.dt List.t;
+}
 
 type compiled_func = {
   args: (Bdd.dt btree) List.t;
   body: compiled_expr;
+  local_bools: int List.t;
+  arg_bools: int List.t;
 }
 
 type compile_context = {
@@ -33,10 +41,8 @@ type compiled_program = {
 
 type env = (String.t, Bdd.dt btree) Map.Poly.t (* map from variable identifiers to BDDs*)
 
-let ctx_man = Man.make_d ()
-
-let new_context ~lazy_eval () =
-  let man = ctx_man in
+let new_context ~lazy_eval count () =
+  let man = Man.make_d ~numVars:count () in
   (* Man.enable_autodyn man Man.REORDER_LINEAR; *)
   Man.disable_autodyn man;
   let weights = Hashtbl.Poly.create () in
@@ -49,26 +55,29 @@ let new_context ~lazy_eval () =
    lazy_eval = lazy_eval}
 
 (** generates a symbolic representation for a variable of the given type *)
-let rec gen_sym_type ctx (t:typ) : Bdd.dt btree =
+(* let rec gen_sym_type ctx (t:CG.typ) : Bdd.dt btree =
   match t with
   | TBool ->
     let bdd = Bdd.newvar ctx in Leaf(bdd)
   | TTuple(t1, t2) ->
     let s1 = gen_sym_type ctx t1 and s2 = gen_sym_type ctx t2 in
-    Node(s1, s2)
+    Node(s1, s2) *)
 
 let rec is_const (st: Bdd.dt btree) =
   match st with
   | Leaf(v) -> Bdd.is_cst v
   | Node(l, r) -> (is_const l) && (is_const r)
 
-let rec compile_expr (ctx: compile_context) (tenv: tenv) (env: env) e : compiled_expr =
+type state = Bdd.dt btree
+
+let rec compile_expr (ctx: compile_context) (tenv: CG.tenv)
+    (env: env) (subst: subst) (z: Bdd.dt) (e: VO.texpr) : compiled_expr =
   let binop_helper f e1 e2 =
-    let c1 = compile_expr ctx tenv env e1 in
-    let c2 = compile_expr ctx tenv env e2 in
+    let c1 = compile_expr ctx tenv env subst z e1 in
+    let c2 = compile_expr ctx tenv env c1.subst c1.z e2 in
     let v = Leaf(f (extract_leaf c1.state) (extract_leaf c2.state)) in
     let z = Bdd.dand c1.z c2.z in
-    {state=v; z=z; flips=List.append c1.flips c2.flips} in
+    {state=v; z=z; subst=c2.subst; flips=List.append c1.flips c2.flips} in
 
   let r = match e with
   | And(e1, e2) -> binop_helper Bdd.dand e1 e2
@@ -76,139 +85,142 @@ let rec compile_expr (ctx: compile_context) (tenv: tenv) (env: env) e : compiled
   | Xor(e1, e2) -> binop_helper Bdd.xor e1 e2
   | Eq(e1, e2) -> binop_helper Bdd.eq e1 e2
   | Not(e) ->
-    let c = compile_expr ctx tenv env e in
+    let c = compile_expr ctx tenv env subst z e in
     let v = Bdd.dnot (extract_leaf c.state) in
-    {state=Leaf(v); z=c.z; flips=c.flips}
+    {state=Leaf(v); subst=c.subst; z=c.z; flips=c.flips}
 
-  | True -> {state=Leaf(Bdd.dtrue ctx.man); z=Bdd.dtrue ctx.man; flips=[]}
+  | True -> {state=Leaf(Bdd.dtrue ctx.man); subst=subst; z=Bdd.dtrue ctx.man; flips=[]}
 
-  | False -> {state=Leaf(Bdd.dfalse ctx.man); z=Bdd.dtrue ctx.man; flips=[]}
+  | False -> {state=Leaf(Bdd.dfalse ctx.man); subst=subst; z=Bdd.dtrue ctx.man; flips=[]}
 
   | Ident(s) ->
     (match Map.Poly.find env s with
-     | Some(r) -> {state=r; z=Bdd.dtrue ctx.man; flips=[]}
+     | Some(r) -> {state=r; z=Bdd.dtrue ctx.man; flips=[]; subst=subst}
      | _ -> failwith (sprintf "Could not find variable '%s'" s))
 
   | Tup(e1, e2) ->
-    let c1 = compile_expr ctx tenv env e1 in
-    let c2 = compile_expr ctx tenv env e2 in
-    {state=Node(c1.state, c2.state); z=Bdd.dand c1.z c2.z; flips=List.append c1.flips c2.flips}
+    let c1 = compile_expr ctx tenv env subst z e1 in
+    let c2 = compile_expr ctx tenv env c1.subst c1.z e2 in
+    {state=Node(c1.state, c2.state); z=c2.z; subst=c2.subst; flips=List.append c1.flips c2.flips}
 
   | Ite(g, thn, els) ->
-    let cg = compile_expr ctx tenv env g in
+    let cg = compile_expr ctx tenv env subst z g in
     if is_const cg.state then
       let v = extract_leaf cg.state in
-      let r = compile_expr ctx tenv env (if Bdd.is_true v then thn else els) in
-      {state=r.state; z=Bdd.dand cg.z r.z; flips = cg.flips @ r.flips}
+      let r = compile_expr ctx tenv env cg.subst cg.z (if Bdd.is_true v then thn else els) in
+      {state=r.state; z=Bdd.dand cg.z r.z; subst=r.subst; flips = cg.flips @ r.flips}
     else
-      let cthn = compile_expr ctx tenv env thn in
-      let cels = compile_expr ctx tenv env els in
+      let cthn = compile_expr ctx tenv env cg.subst cg.z thn in
+      let cels = compile_expr ctx tenv env cthn.subst cthn.z els in
       let gbdd = extract_leaf cg.state in
       let zipped = zip_tree cthn.state cels.state in
       let v' = map_tree zipped (fun (thn_state, els_state) ->
           Bdd.ite gbdd thn_state els_state
         ) in
       let z' = Bdd.dand cg.z (Bdd.ite gbdd cthn.z cels.z) in
-      {state=v'; z=z'; flips = List.append cg.flips (List.append cthn.flips cels.flips)}
+      {state=v'; z=z'; flips = List.append cg.flips (List.append cthn.flips cels.flips); subst=cels.subst}
 
   | Fst(e) ->
-    let c = compile_expr ctx tenv env e in
+    let c = compile_expr ctx tenv env subst z e in
     let v' = (match c.state with
      | Node(l, _) -> l
-     | _ -> failwith (Format.sprintf "Internal Failure: calling `fst` on non-tuple at %s" (string_of_expr e))) in
-    {state=v'; z=c.z; flips=c.flips}
+     | _ -> failwith (Format.sprintf "Internal Failure: calling `fst` on non-tuple at %s" (VO.string_of_texpr e))) in
+    {state=v'; z=c.z; flips=c.flips; subst=c.subst}
 
   | Snd(e) ->
-    let c = compile_expr ctx tenv env e in
+    let c = compile_expr ctx tenv env subst z e in
     let v' = (match c.state with
      | Node(_, r) -> r
-     | _ -> failwith (Format.sprintf "Internal Failure: calling `snd` on non-tuple at %s" (string_of_expr e))) in
-    {state=v'; z=c.z; flips=c.flips}
+     | _ -> failwith (Format.sprintf "Internal Failure: calling `snd` on non-tuple at %s" (VO.string_of_texpr e))) in
+    {state=v'; z=c.z; flips=c.flips; subst=c.subst}
 
-  | Flip(f) ->
-    let new_f = Bdd.newvar ctx.man in
+  | Flip(f, idx) ->
+    let new_f = Bdd.ithvar ctx.man idx in
     let var_lbl = Bdd.topvar new_f in
-    let var_name = (Format.sprintf "f%d" !flip_id) in
-    Hashtbl.add_exn ctx.name_map ~key:var_lbl ~data:var_name;
-    flip_id := !flip_id + 1;
+    let var_name = (Format.sprintf "f%d" idx) in
     Hashtbl.Poly.add_exn ctx.weights ~key:var_lbl ~data:(1.0-.f, f);
-    {state=Leaf(new_f); z=Bdd.dtrue ctx.man; flips=[new_f]}
+    Hashtbl.add_exn ctx.name_map ~key:var_lbl ~data:var_name;
+    {state=Leaf(new_f); z=Bdd.dtrue ctx.man; flips=[new_f]; subst=subst}
 
   | Observe(g) ->
-    let c = compile_expr ctx tenv env g in
-    {state=Leaf(Bdd.dtrue ctx.man); z=Bdd.dand (extract_leaf c.state) c.z; flips=c.flips}
+    let c = compile_expr ctx tenv env subst z g in
+    {state=Leaf(Bdd.dtrue ctx.man); z=Bdd.dand (extract_leaf c.state) c.z; flips=c.flips; subst=c.subst}
 
-  | Let(x, e1, e2) ->
-    let c1 = compile_expr ctx tenv env e1 in
-    let t = (type_of tenv e1) in
+  | Let(x, e1, e2, tree) ->
+    let c1 = compile_expr ctx tenv env subst z e1 in
+    let t = (VO.type_of tenv e1) in
     let tenv' = Map.Poly.set tenv ~key:x ~data:t in
-    (* if true then (\* this value is a heuristic *\) *)
     if is_const c1.state then (* this value is a heuristic *)
       let env' = Map.Poly.set env ~key:x ~data:c1.state in
-      let c2 = compile_expr ctx tenv' env' e2 in
-      {state=c2.state; z=Bdd.dand c1.z c2.z; flips=List.append c1.flips c2.flips}
+      let c2 = compile_expr ctx tenv' env' c1.subst c1.z e2 in
+      {state=c2.state; z=Bdd.dand c1.z c2.z; flips=List.append c1.flips c2.flips; subst=c2.subst}
     else
       (* create a temp variable *)
-      let tmp = gen_sym_type ctx.man t in
+      let tmp = VarState.map_tree tree (fun idx -> Bdd.ithvar ctx.man idx) in
       let env' = Map.Poly.set env ~key:x ~data:tmp in
-      let c2 = compile_expr ctx tenv' env' e2 in
       let newsubst = List.zip_exn (collect_leaves tmp) (collect_leaves c1.state) in
-
+      let c2 = compile_expr ctx tenv' env' (newsubst @ subst) c1.z e2 in
       (* do substitution *)
       let swap_idx = List.to_array (List.map (collect_leaves tmp) ~f:(Bdd.topvar)) in
       let swap_bdd = List.to_array (collect_leaves c1.state) in
-      (* Format.printf "Composing BDD of size %d into %d, num vars: %d\n" (VarState.state_size [c1.state]) (VarState.state_size [c2.state]) ();
-       * flush_all (); *)
       let final_state = map_tree c2.state (fun bdd ->
           List.fold ~init:bdd newsubst ~f:(fun acc (tmp, e1c) ->
               Bdd.compose (Bdd.topvar tmp) e1c acc
             )
-          (* Bdd.labeled_vector_compose bdd swap_bdd swap_idx *)
         ) in
-
       let final_z = Bdd.labeled_vector_compose c2.z swap_bdd swap_idx in
-      {state=final_state; z=Bdd.dand c1.z final_z; flips=List.append c1.flips c2.flips}
+      {state=final_state; z=Bdd.dand c1.z final_z; flips=List.append c1.flips c2.flips; subst = c2.subst}
 
   | Sample(e) ->
-    let sube = compile_expr ctx tenv env e in
-    (* perform sequential sampling *)
+    let c = compile_expr ctx tenv env subst z e in
+    (* substitute *)
+    let comp = List.fold ~init:c.state c.subst ~f:(fun acc (arg, subst) ->
+        VarState.map_tree acc (fun treebdd -> Bdd.compose (Bdd.topvar arg) subst treebdd)
+      ) in
+    let z' = List.fold ~init:(Bdd.dand z c.z) c.subst ~f:(fun acc (arg, subst) ->
+        Bdd.compose (Bdd.topvar arg) subst acc
+      ) in
     let rec sequential_sample cur_obs state =
       (match state with
        | Leaf(bdd) ->
-         let t = Wmc.wmc (Bdd.dand (Bdd.dand cur_obs bdd) sube.z) ctx.weights in
-         let curz = Wmc.wmc (Bdd.dand sube.z cur_obs) ctx.weights in
+         let t = Wmc.wmc (Bdd.dand (Bdd.dand cur_obs bdd) z') ctx.weights in
+         let curz = Wmc.wmc (Bdd.dand z' cur_obs) ctx.weights in
          let rndvalue = Random.float 1.0 in
+         Format.printf "z: %f, v: %f, accepted: %s\n" curz t
+           (if compare_float rndvalue (t /. curz) < 0 then "yes" else "no");
          if compare_float rndvalue (t /. curz) < 0 then (bdd, Leaf(Bdd.dtrue ctx.man)) else (Bdd.dnot bdd, Leaf(Bdd.dfalse ctx.man))
        | Node(l, r) ->
          let lbdd, lres = sequential_sample cur_obs l in
          let rbdd, rres = sequential_sample lbdd r in
          (rbdd, Node(lres, rres))
       ) in
-    let _, r = sequential_sample (Bdd.dtrue ctx.man) sube.state in
-    {state=r; z=Bdd.dtrue ctx.man; flips=[]}
-
-  | FuncCall(name, args) ->
+    let _, r = sequential_sample (Bdd.dtrue ctx.man) comp in
+    let obs = List.fold ~init:(Bdd.dtrue ctx.man) (List.zip_exn (collect_leaves comp) (collect_leaves r))
+        ~f:(fun acc (st, obs) ->
+            if Bdd.is_true obs then Bdd.dand acc st
+            else if Bdd.is_false obs then Bdd.dand acc (Bdd.dnot st)
+            else failwith "unreachable"
+          ) in
+    {state=r; z=Bdd.dand obs z; subst = subst; flips=[]}
+    (* {state=r; z=z; subst = subst; flips=[]} *)
+
+  | FuncCall(name, args, order_map) ->
     let func = try Hashtbl.Poly.find_exn ctx.funcs name
       with _ -> failwith (Format.sprintf "Could not find function '%s'." name) in
 
-    let cargs = List.map args ~f:(compile_expr ctx tenv env) in
-    let new_flips = List.map func.body.flips ~f:(fun f ->
-        let cur_name = Hashtbl.find_exn ctx.name_map (Bdd.topvar f) in
-        let var_name = (Format.sprintf "%s_%d" cur_name !flip_id) in
-        flip_id := !flip_id + 1;
-
-        let newv = Bdd.newvar ctx.man in
-        let lvl = Bdd.topvar newv in
-        Hashtbl.add_exn ctx.name_map ~key:lvl ~data:var_name;
-        (match Hashtbl.Poly.find ctx.weights (Bdd.topvar f) with
-         | Some(v) -> Hashtbl.Poly.add_exn ctx.weights ~key:lvl ~data:v
-         | None -> ());
-        newv) in
-    let swapA = List.to_array (List.map new_flips ~f:(fun cur -> Bdd.topvar cur)) in
+    let curz = ref z in
+    let cursubst = ref subst in
+    let cargs = List.map args ~f:(fun i ->
+        let r = compile_expr ctx tenv env !cursubst !curz i in
+        curz := r.z;
+        cursubst := r.subst;
+        r) in
+    let argflips = List.fold cargs ~init:[] ~f:(fun acc i -> acc @ i.flips) in
+    let new_flips = List.map func.body.flips ~f:(fun v -> Bdd.ithvar ctx.man (Map.Poly.find_exn order_map (Bdd.topvar v))) in
+    (* let swapA = List.to_array (List.map new_flips ~f:(fun cur -> Bdd.topvar cur)) in
     let swapB = List.to_array (List.map func.body.flips ~f:(fun cur -> Bdd.topvar cur)) in
     let refreshed_state = map_tree func.body.state (fun bdd -> Bdd.swapvariables bdd swapA swapB) in
     let refreshed_z = Bdd.swapvariables func.body.z swapA swapB in
-
     let swap_idx =
       List.map func.args ~f:(fun arg ->
           List.to_array (List.map (collect_leaves arg) ~f:(Bdd.topvar)))
@@ -217,41 +229,98 @@ let rec compile_expr (ctx: compile_context) (tenv: tenv) (env: env) e : compiled
       List.map cargs ~f:(fun arg ->
           List.to_array (collect_leaves arg.state))
       |> Array.concat in
-    let argz = List.fold cargs ~init:(Bdd.dtrue ctx.man) ~f:(fun acc i -> Bdd.dand i.z acc) in
-    let argflips = List.fold cargs ~init:[] ~f:(fun acc i -> acc @ i.flips) in
     let final_state = map_tree refreshed_state (fun bdd ->
         Bdd.labeled_vector_compose bdd swap_bdd swap_idx) in
-    let final_z = Bdd.labeled_vector_compose refreshed_z swap_bdd swap_idx in
-    {state=final_state; z=Bdd.dand argz final_z; flips=new_flips @ argflips} in
- r
+    let final_z = Bdd.labeled_vector_compose refreshed_z swap_bdd swap_idx in *)
+    let order_pairs = Map.Poly.to_alist order_map in
+    (* print_endline "state = <<";
+    BddUtil.dump_dot (Hashtbl.Poly.create ()) (extract_leaf func.body.state);
+    print_endline "\n>>"; *)
+    (* print_endline ""; *)
+    (* Map.Poly.sexp_of_t sexp_of_int sexp_of_int order_map |> Sexp.to_string_hum |> print_endline; *)
+    (* [%sexp_of: (int, float*float) Hashtbl.Poly.t] ctx.weights |> Sexp.to_string_hum |> print_endline; *)
+    List.iter order_pairs (fun (old_id, new_id) ->
+      let wts_option = Hashtbl.Poly.find ctx.weights old_id in
+      match wts_option with
+      | Some wts -> Hashtbl.Poly.add_exn ctx.weights ~key:new_id ~data: wts
+      | None -> ();
+      let var_name_option = Hashtbl.Poly.find ctx.name_map old_id in
+      match var_name_option with
+      | Some var_name -> Hashtbl.add_exn ctx.name_map ~key:new_id ~data:var_name
+      | None -> ()
+      (* let wts = Hashtbl.Poly.find_exn ctx.weights old_id in
+      Hashtbl.Poly.add_exn ctx.weights ~key:new_id ~data: wts *)
+    ) ;
+    let old_ids = List.map order_pairs (fun (x,y) -> x) |> List.to_array in
+    (* let new_ids = List.map order_pairs (fun (x,y) -> y) |> List.to_array in *)
+    (* let (arg_start, arg_end) = arg_range in *)
+    let (arg_start, arg_end) =
+      if (List.length func.arg_bools) > 0 then
+        (List.nth_exn func.arg_bools 0, List.last_exn func.arg_bools)
+      else
+        (0, -1)
+      in
+    let arg_leaves = List.map cargs ~f:(fun carg ->
+          List.to_array (collect_leaves carg.state))
+      |> Array.concat in
+    let new_bdds = List.map order_pairs (fun (x,y) ->
+      if x >= arg_start && x <= arg_end then Array.get arg_leaves (x - arg_start)
+      else 
+      Bdd.ithvar ctx.man y
+    ) |> List.to_array in
+    let final_state = map_tree func.body.state (fun bdd ->
+        Bdd.labeled_vector_compose bdd new_bdds old_ids
+      ) in
+(*     print_endline "final state = <<";
+    BddUtil.dump_dot (Hashtbl.Poly.create ()) (extract_leaf final_state);
+    print_endline "\n>>"; *)
+    let final_z = Bdd.labeled_vector_compose func.body.z new_bdds old_ids in
+    {state=final_state; z=Bdd.dand !curz final_z; flips=new_flips @ argflips; subst= !cursubst}
+  in r
+
 
-let compile_func (ctx: compile_context) tenv (f: func) : compiled_func =
+let compile_func (ctx: compile_context) tenv (f: VO.func) : compiled_func =
   (* set up the context; need both a list and a map, so build both together *)
   let new_tenv = List.fold ~init:tenv f.args ~f:(fun acc (name, typ) ->
       Map.Poly.add_exn acc ~key:name ~data:typ
     ) in
+  let count = ref 0 in
   let (args, env) = List.fold f.args ~init:([], Map.Poly.empty)
       ~f:(fun (lst, map) (name, typ) ->
-          let placeholder_arg = gen_sym_type ctx.man typ in
+          let iarg = VO.mk_tree count typ in
+          let placeholder_arg = map_tree iarg (fun i ->
+            let i' = List.nth_exn f.arg_bools i in
+            Bdd.ithvar ctx.man i'
+          ) in
           (List.append lst [placeholder_arg], Map.Poly.set map ~key:name ~data:placeholder_arg)
         ) in
   (* now compile the function body with these arguments *)
-  let body = compile_expr ctx new_tenv env f.body in
-  {args = args; body = body}
+  let body = compile_expr ctx new_tenv env [] (Bdd.dtrue ctx.man) f.body in
+  {args = args; body = body; arg_bools = f.arg_bools; local_bools = f.local_bools}
 
-let compile_program (p:program) : compiled_program =
+let compile_program (p:CG.program) : compiled_program =
   (* first compile the functions in topological order *)
-  let ctx = new_context ~lazy_eval:true () in
+  let (count, vp) = VO.from_cg_prog VO.DFS p in
+  let ctx = new_context count ~lazy_eval:true () in
   let tenv = ref Map.Poly.empty in
-  List.iter p.functions ~f:(fun func ->
+  List.iter p.functions ~f:(fun cg_func ->
+      let func = Map.Poly.find_exn vp.functions cg_func.name in
       let c = compile_func ctx !tenv func in
-      tenv := Map.Poly.add_exn !tenv ~key:func.name ~data:(type_of_fun !tenv func);
+      tenv := Map.Poly.add_exn !tenv ~key:func.name ~data:(VO.type_of_fun !tenv func);
       try Hashtbl.Poly.add_exn ctx.funcs ~key:func.name ~data:c
       with _ -> failwith (Format.sprintf "Function names must be unique: %s found twice" func.name)
     );
   (* now compile the main body, which is the result of the program *)
   let env = Map.Poly.empty in
-  {ctx = ctx; body = compile_expr ctx !tenv env p.body}
+  let c = compile_expr ctx !tenv env [] (Bdd.dtrue ctx.man) vp.body in
+  (* do substitutions *)
+  let subst = List.fold ~init:c.state c.subst ~f:(fun acc (arg, subst) ->
+      VarState.map_tree acc (fun treebdd -> Bdd.compose (Bdd.topvar arg) subst treebdd)
+    ) in
+  let z' = List.fold ~init:c.z c.subst ~f:(fun acc (arg, subst) ->
+      Bdd.compose (Bdd.topvar arg) subst acc
+    ) in
+  {ctx = ctx; body = {state = subst; z = z'; flips=c.flips; subst=[]}}
 
 
 let get_prob p =
@@ -290,7 +359,7 @@ let parse_and_prob ?debug txt =
   (match debug with
    | Some(true)->
      Format.printf "Program: %s\n" (ExternalGrammar.string_of_prog parsed);
-     Format.printf "After passes: %s\n" (CoreGrammar.string_of_prog (transformed));
+     Format.printf "After passes: %s\n" (CG.string_of_prog (transformed));
    | _ -> ());
   get_prob transformed
 
@@ -307,7 +376,7 @@ let parse_optimize_and_prob ?debug txt =
   (match debug with
    | Some(true)->
      Format.printf "Program: %s\n" (ExternalGrammar.string_of_prog parsed);
-     Format.printf "After passes: %s\n" (CoreGrammar.string_of_prog (transformed));
+     Format.printf "After passes: %s\n" (CG.string_of_prog (transformed));
    | _ -> ());
   get_prob transformed
 
diff --git a/lib/Compiler.mli b/lib/Compiler.mli
index f284d28..79b9829 100644
--- a/lib/Compiler.mli
+++ b/lib/Compiler.mli
@@ -3,24 +3,29 @@ open Cudd
 open Core
 open Wmc
 
+type subst = (Bdd.dt * Bdd.dt) List.t
+
 (** Result of compiling an expression *)
 type compiled_expr = {
   state: Bdd.dt btree;
   z: Bdd.dt;
-  flips: Bdd.dt List.t}
+  subst: subst;
+  flips: Bdd.dt List.t;
+}
 
 type compiled_func = {
   args: (Bdd.dt btree) List.t;
   body: compiled_expr;
+  local_bools: int List.t;
+  arg_bools: int List.t;
 }
 
-
 type compile_context = {
   man: Man.dt;
   name_map: (int, String.t) Hashtbl.Poly.t; (* map from variable identifiers to names, for debugging *)
   weights: weight; (* map from variables to weights *)
   lazy_eval: bool; (* true if lazy let evaluation *)
-  free_stack: Bdd.dt Stack.t; (* a stack of unallocated BDD variables, for reuse *)
+  free_stack: Bdd.dt Stack.t;
   funcs: (String.t, compiled_func) Hashtbl.Poly.t;
 }
 
diff --git a/lib/VarOrder.ml b/lib/VarOrder.ml
new file mode 100644
index 0000000..f6983ad
--- /dev/null
+++ b/lib/VarOrder.ml
@@ -0,0 +1,391 @@
+(** Defines an intermediate AST that tags each new variable production source
+    with an index. This AST is used by the compiler to generate variables in a
+    particular order. *)
+
+open Core
+open Cudd
+open VarState
+
+module CG = CoreGrammar
+
+type strategy =
+    Default
+  | DFS
+
+(** A tagged expression where, each time a new logical variable is introduced,
+    it is tagged with its order *)
+type texpr =
+  | And of texpr * texpr
+  | Or of texpr * texpr
+  | Eq of texpr * texpr
+  | Xor of texpr * texpr
+  | Not of texpr
+  | Ident of String.t
+  | Sample of texpr
+  | Fst of texpr
+  | Snd of texpr
+  | Tup of texpr * texpr
+  | Ite of texpr * texpr * texpr
+  | True
+  | False
+  | Flip of float * int (** the int is order of the flip *)
+  | Let of String.t * texpr * texpr * (int btree) (** the int btree is the order of the argument *)
+  | FuncCall of String.t * texpr List.t * (int, int) Map.Poly.t 
+  | Observe of texpr
+[@@deriving sexp_of]
+and fcall = {
+  fname: String.t;
+  args: texpr
+}
+
+let string_of_texpr e =
+  Sexp.to_string_hum (sexp_of_texpr e)
+
+let rec type_of env e : CG.typ =
+  match e with
+  | And(_, _) | Xor(_, _) | Eq(_, _) | Or(_, _) | Not(_) | True | False | Flip(_) | Observe(_) -> TBool
+  | Ident(s) -> (try Map.Poly.find_exn env s
+    with _ -> failwith (Format.sprintf "Could not find variable %s during typechecking" s))
+  | Sample(e) -> type_of env e
+  | Fst(e1) ->
+    (match type_of env e1 with
+     | TTuple(l, _) -> l
+     | _ -> failwith "Type error: expected tuple")
+  | Snd(e1) ->
+    (match type_of env e1 with
+     | TTuple(_, r) -> r
+     | _ -> failwith "Type error: expected tuple")
+  | Tup(e1, e2) ->
+    let t1 = type_of env e1 in
+    let t2 = type_of env e2 in
+    TTuple(t1 ,t2)
+  | Let(x, e1, e2, _) ->
+    let te1 = type_of env e1 in
+    type_of (Map.Poly.set env ~key:x ~data:te1) e2
+  | Ite(_, thn, _) ->
+    let t1 = type_of env thn in
+    (* let t2 = type_of env els in *)
+    (* assert (t1 == t2); *)
+    t1
+  | FuncCall(id, _, _) ->
+    (try Map.Poly.find_exn env id
+    with _ -> failwith (Format.sprintf "Could not find function '%s' during typechecking" id))
+
+
+(** Core function grammar *)
+type func = {
+  name: String.t;
+  args: CG.arg List.t;
+  body: texpr;
+
+  local_bools: int List.t;
+  arg_bools: int List.t;
+}
+[@@deriving sexp_of]
+
+type fenv = (String.t, func) Map.Poly.t
+[@@deriving sexp_of]
+
+
+let type_of_fun env f : CG.typ =
+  (* set up the type environment and then type the body *)
+  let new_env = List.fold ~init:env f.args ~f:(fun acc (name, typ) ->
+      Map.Poly.add_exn acc ~key:name ~data:typ
+    ) in
+  type_of new_env f.body
+
+type program = {
+  functions: fenv;
+  body: texpr;
+}
+[@@deriving sexp_of]
+
+let string_of_prog e =
+  Sexp.to_string_hum (sexp_of_program e)
+
+
+(** create a new variable tree
+   `c` is a counter that tracks that tracks which variable is currently the last
+   in the order *)
+let rec mk_tree (c: int ref) (t:CG.typ) : int VarState.btree =
+  match t with
+  | TBool ->
+    let v = !c in
+    c := !c + 1;
+    Leaf(v)
+  | TTuple(l, r) ->
+    let l = mk_tree c l in
+    let r = mk_tree c r in
+    Node(l, r)
+
+(** Updates the order of a tagged AST `e` according to `map` *)
+let rec update_order map e =
+  match e with
+  | And(e1, e2) -> And(update_order map e1, update_order map e2)
+  | Or(e1, e2) -> Or(update_order map e1, update_order map e2)
+  | Xor(e1, e2) -> Xor(update_order map e1, update_order map e2)
+  | Eq(e1, e2) -> Eq(update_order map e1, update_order map e2)
+  | Not(e1) -> Not(update_order map e1)
+  | Observe(e1) -> Observe(update_order map e1)
+  | Sample(e1) -> Sample(update_order map e1)
+  | True -> True
+  | False -> False
+  | Ident(x) -> Ident(x)
+  | Fst(e) -> Fst(update_order map e)
+  | Snd(e) -> Snd(update_order map e)
+  | Tup(e1, e2) ->
+    Tup(update_order map e1, update_order map e2)
+  | Flip(f, v) -> Flip(f, Hashtbl.Poly.find_exn map v)
+  | Ite(g, thn, els) -> Ite(update_order map g,
+                            update_order map thn,
+                            update_order map els)
+  | Let(x, e1, e2, v) ->
+    Let(x, update_order map e1, update_order map e2, map_tree v (Hashtbl.Poly.find_exn map))
+  | FuncCall(name, targs, order_map) ->
+    FuncCall(
+      name,
+      List.map targs (update_order map),
+      Map.Poly.map order_map (Hashtbl.Poly.find_exn map)
+      (* arg_range *)
+    )
+
+
+(** creates a tagged AST from a core grammar AST. The goal here is simply to associate each
+    created logical variable with a unique identifier.
+
+    By default, this should be the same as the depth-first order used by the compiler.
+
+    TOOD: Make sure that this is the case. I suspect right now that these orders
+    are different, and that using the default ordering from this module will
+    cause a serious performance regression.
+*)
+let rec from_cg_h (count: int ref) (t: CG.tenv) (f:fenv) (e: CG.expr) : texpr =
+  match e with
+  | And(l, r) ->
+    let l = from_cg_h count t f l in
+    let r = from_cg_h count t f r in
+    And(l, r)
+  | Or(l, r) ->
+    let l = from_cg_h count t f l in
+    let r = from_cg_h count t f r in
+    Or(l, r)
+  | Eq(l, r) ->
+    let l = from_cg_h count t f l in
+    let r = from_cg_h count t f r in
+    Eq(l, r)
+  | Xor(l, r) ->
+    let l = from_cg_h count t f l in
+    let r = from_cg_h count t f r in
+    Xor(l, r)
+  | Tup(l, r) ->
+    let l = from_cg_h count t f l in
+    let r = from_cg_h count t f r in
+    Tup(l, r)
+  | Not(e) -> Not(from_cg_h count t f e)
+  | Ident(s) -> Ident(s)
+  | Sample(e) -> Sample(from_cg_h count t f e)
+  | Fst(e) -> Fst(from_cg_h count t f e)
+  | Snd(e) -> Snd(from_cg_h count t f e)
+  | True -> True
+  | False -> False
+  | Flip(x) ->
+    let i = !count in
+    count := !count + 1;
+    Flip(x, i)
+  | Ite(g, thn, els) ->
+    let g = from_cg_h count t f g in
+    let thn = from_cg_h count t f thn in
+    let els = from_cg_h count t f els in
+    Ite(g, thn, els)
+  | Let(x, e1, e2) ->
+    let te1 = CG.type_of t e1 in
+    let rece1 = from_cg_h count t f e1 in
+    let tree = mk_tree count te1 in
+    let t' = Map.Poly.set t ~key:x ~data:te1 in
+    let rece2 = from_cg_h count t' f e2 in
+    Let(x, rece1, rece2, tree)
+  | Observe(e) -> Observe(from_cg_h count t f e)
+  | FuncCall(name, args) ->
+    let targs = List.map args (from_cg_h count t f) in
+    let func = Map.Poly.find_exn f name in
+    let bool_count = (List.length func.arg_bools) + (List.length func.local_bools) in
+    let init_count = !count in
+    let order_map_args = List.fold ~init:Map.Poly.empty ~f:(fun map i ->
+      let map' = Map.Poly.set map ~key:i ~data:!count in
+      count := !count +1;
+      map'
+    ) func.arg_bools in
+    (* let arg_range = (init_count, !count) in *)
+    let order_map = List.fold ~init:order_map_args ~f:(fun map i ->
+      let map' = Map.Poly.set map ~key:i ~data:!count in
+      count := !count +1;
+      map'
+    ) func.local_bools in
+    FuncCall(name, targs, order_map)
+
+
+let from_cg_func count (tenv: CG.tenv) (fenv: fenv) (f: CG.func) : func =
+  (* add the arguments to the type environment *)
+  let init_count = !count in
+  let tenvwithargs = List.fold f.args ~init:tenv ~f:(fun acc (name, typ) ->
+      let _tree = mk_tree count typ in
+      Map.Poly.set acc ~key:name ~data:typ
+    ) in
+  let count_with_args = !count in
+  let conv = from_cg_h count tenvwithargs fenv f.body in
+  (* convert arguments *)
+  {name = f.name;
+   args = f.args;
+   body = conv;
+
+   arg_bools = List.range init_count count_with_args;
+   local_bools = List.range count_with_args !count;
+   }
+
+(** a map from each variable to its parents. This encodes a dependency graph. *)
+type cdfg = (int, int Set.Poly.t) Hashtbl.Poly.t
+(** a map from each identifier to the variables that it depends on *)
+type env = (String.t, (int Set.Poly.t) btree) Map.Poly.t
+
+let build_cdfg (p: program) (f: fenv) =
+  (** construct a CDFG for an expression. Returns a `btree` of sets of integers
+      for handling tuples. *)
+  let rec cdfg_e (cdfg: cdfg) (env: env) e =
+    match e with
+    | And(e1, e2)
+    | Or(e1, e2)
+    | Eq(e1, e2)
+    | Xor(e1, e2) ->
+      (* for binary expressions, simply take the union of whichever dependencies are
+         present in the two children *)
+      let s1 = extract_leaf (cdfg_e cdfg env e1) in
+      let s2 = extract_leaf (cdfg_e cdfg env e2) in
+      Leaf(Set.union s1 s2)
+    | Not(e1)
+    | Observe(e1) -> cdfg_e cdfg env e1
+    | Sample(e) -> cdfg_e cdfg env e
+    | True
+    | False -> Leaf(Set.Poly.empty)
+    | Ident(x) ->
+      (* this is why we have the environment map *)
+      Map.Poly.find_exn env x
+    | Fst(e) ->
+      extract_l (cdfg_e cdfg env e)
+    | Snd(e) -> extract_r (cdfg_e cdfg env e)
+    | Tup(e1, e2) ->
+      let s1 = cdfg_e cdfg env e1 in
+      let s2 = cdfg_e cdfg env e2 in
+      Node(s1, s2)
+    | Flip(_, v) ->
+      (* for flips, depend only on the flip's Boolean indicator *)
+      Hashtbl.Poly.add_exn cdfg ~key:v ~data:Set.Poly.empty;
+      Leaf(Set.Poly.of_list [v])
+    | Ite(g, thn, els) ->
+      let gdeps = extract_leaf (cdfg_e cdfg env g) in
+      let thndeps = cdfg_e cdfg env thn in
+      let elsdeps = cdfg_e cdfg env els in
+      (* take the union all the dependencies of the guard, then branch, and else-branch *)
+      map_tree (zip_tree thndeps elsdeps) (fun (l, r) ->
+          Set.Poly.union_list [l; r; gdeps]
+        )
+    | Let(x, e1, e2, v) ->
+      let e1deps = cdfg_e cdfg env e1 in
+      let settree = map_tree v (fun i -> Set.Poly.of_list [i]) in
+      let env' = Map.Poly.set env ~key:x ~data:settree in
+      let e2deps = cdfg_e cdfg env' e2 in
+
+      (* update the dependencies for all the variables in x *)
+      let _a = map_tree (zip_tree v e1deps) (fun (curx, curdep) ->
+          Hashtbl.Poly.add_exn cdfg ~key:curx ~data:curdep;
+        ) in
+      e2deps
+    | FuncCall(name, args, order_map) ->
+      let argdeps = List.map args (cdfg_e cdfg env) in
+      (* let (arg_start, arg_end) = arg_range in *)
+      let func = Map.Poly.find_exn f name in
+      let argtrees = 
+        if (List.length func.arg_bools) > 0 then
+          let count = ref (List.nth_exn func.arg_bools 0) in 
+          List.map func.args ~f:(fun (_, typ) ->
+            map_tree (mk_tree count typ) (fun i -> Set.Poly.of_list [Map.Poly.find_exn order_map i])
+          )
+        else
+          []
+        in
+      List.iter (List.zip_exn argtrees argdeps) ~f:(fun (tree, dep) ->
+        let _a = map_tree (zip_tree tree dep) (fun (curx, curdep) ->
+          Hashtbl.Poly.add_exn cdfg ~key:(Set.Poly.choose_exn curx) ~data:curdep;
+        ) in ()
+      );
+      let argenv = List.fold ~init:Map.Poly.empty ~f:(fun argenv ((name, _), tree) ->
+        Map.Poly.set argenv ~key:name ~data:tree
+      ) (List.zip_exn func.args argtrees) in
+      let order_map_h = Hashtbl.Poly.create () in
+      List.iter (Map.Poly.to_alist order_map) ~f:(fun (k,v) -> Hashtbl.Poly.add_exn order_map_h ~key:k ~data:v);
+      let refreshed_body = update_order order_map_h func.body in
+      cdfg_e cdfg argenv refreshed_body
+    in
+  let tbl : cdfg = Hashtbl.Poly.create () in
+  let r = cdfg_e tbl Map.Poly.empty p.body in
+  (r, tbl)
+
+(** This is a variable ordering function that takes a CDFG as an argument
+    and produces a possible variable ordering. Produces a map from variable
+    identifiers to their new positions in the order.
+
+    It perform a depth-first topological sort.
+    TODO: Test this and make sure that it is correct
+ *)
+let dfs_ts ?start (cdfg: cdfg) =
+  let map = Hashtbl.Poly.create () in
+  let init_count = match start with Some x -> x | None -> 0 in
+  let count = ref init_count in
+  let rec visit (n: int) =
+    if Hashtbl.Poly.mem map n then () else
+      (let parlist : int List.t = Set.Poly.to_list (Hashtbl.Poly.find_exn cdfg n) in
+       List.iter parlist ~f:(fun i ->
+           (* Format.printf "Parent of %d: %d\n" n i; *)
+           visit i
+         );
+       Hashtbl.Poly.set map ~key:n ~data:!count;
+       (* Format.printf "Mapped %d -> %d\n" n !count; *)
+       count := !count + 1;
+      ) in
+  let l = Hashtbl.Poly.keys cdfg |> List.sort ~compare:Int.compare |> List.rev in
+  List.iter l ~f:(fun n ->
+      visit n
+    );
+  map
+
+let from_cg_prog strategy (p: CG.program) =
+  let count = ref 0 in
+  (* TODO right now, functions are not handled by variable reordering. We would
+     add this feature here. *)
+  let (tenv, fenv) = List.fold p.functions ~init:(Map.Poly.empty, Map.Poly.empty) ~f:(fun (tenv, fenv) i ->
+      let tenvwithargs = List.fold i.args ~init:tenv ~f:(fun acc (name, typ) ->
+          Map.Poly.set acc ~key:name ~data:typ
+        ) in
+      let t = CG.type_of tenvwithargs i.body in
+      let conv = from_cg_func count tenv fenv i in
+      (* print_endline i.name; *)
+  (* [%sexp_of: texpr] conv.body |> Sexp.to_string_hum |> print_endline;     *)
+      let tenv' = Map.Poly.set tenv ~key:i.name ~data:t in
+      let fenv' = Map.Poly.set fenv ~key:i.name ~data:conv in
+      (tenv', fenv')
+    ) in
+  let dummy_count = !count in
+  let convbody = from_cg_h count tenv fenv p.body in
+  (* print_endline "* MAIN *"; [%sexp_of: texpr] convbody |> Sexp.to_string_hum |> print_endline; *)
+  match strategy with
+  | Default ->
+    (!count, {functions=fenv; body=convbody})
+  | DFS ->
+    let prog = {functions = fenv; body = convbody} in
+    let (_, cdfg) = build_cdfg prog fenv in
+    (* print_endline "\nBEFORE"; [%sexp_of: texpr] prog.body |> Sexp.to_string_hum |> print_endline; *)
+    (* [%sexp_of: (int, int Set.Poly.t) Hashtbl.Poly.t] cdfg |> Sexp.to_string_hum |> print_endline; *)
+    let order = dfs_ts ~start:dummy_count cdfg in
+    
+    let updated = update_order order prog.body in
+    (* print_endline "\nAFTER"; [%sexp_of: texpr]  updated |> Sexp.to_string_hum |> print_endline; *)
+    (!count, {functions=fenv; body=updated})
diff --git a/lib/VarState.ml b/lib/VarState.ml
index dbb8018..69f88ac 100644
--- a/lib/VarState.ml
+++ b/lib/VarState.ml
@@ -87,3 +87,12 @@ let state_size (states : Bdd.dt btree List.t) =
       let leaves = collect_leaves i in
       List.fold leaves ~init:acc ~f:(fun acc bdd -> acc + (helper bdd)) )
 
+let extract_l a =
+  match a with
+  | Node(l, _) -> l
+  | _ -> failwith "Attempting to extract left non-node"
+
+let extract_r a =
+  match a with
+  | Node(_, r) -> r
+  | _ -> failwith "Attempting to extract right non-node"
\ No newline at end of file
diff --git a/lib/VarState.mli b/lib/VarState.mli
index 6b9e927..4748ab4 100644
--- a/lib/VarState.mli
+++ b/lib/VarState.mli
@@ -22,3 +22,6 @@ val get_table: Bdd.dt btree ->
 (** [state_size] computes the total number of unique nodes in the list of
     varstates [states] *)
 val state_size: Bdd.dt btree Core.List.t -> int
+
+val extract_l : 'a btree -> 'a btree
+val extract_r : 'a btree -> 'a btree
\ No newline at end of file