Varorder ok

.vscode/settings.json

@@ -0,0 +1,6 @@
+{
+    "ocaml.sandbox": {
+        "kind": "opam",
+        "switch": "4.09.0"
+    }
+}

bin/dice.ml

@@ -60,11 +60,18 @@ let parse_and_print ~print_parsed ~print_internal ~print_size ~skip_table
   match sample_amount with
   | None ->
     let compiled = Compiler.compile_program internal in
+    (* Format.printf "State:\n";
+    BddUtil.dump_dot compiled.ctx.name_map (VarState.extract_leaf compiled.body.state); Format.print_flush ();
+    Format.printf "\n\nz:\n";
+    BddUtil.dump_dot compiled.ctx.name_map compiled.body.z; Format.print_flush ();
+    Format.printf "\n\n"; *)
     let zbdd = compiled.body.z in
     let z = Wmc.wmc zbdd compiled.ctx.weights in
     let res = if skip_table then res else res @
       (let table = VarState.get_table compiled.body.state t in
        let probs = List.map table ~f:(fun (label, bdd) ->
+        (* BddUtil.dump_dot (Hashtbl.Poly.create ()) bdd;
+        [%sexp_of: (int, float*float) Hashtbl.Poly.t] compiled.ctx.weights |> Sexp.to_string_hum |> print_endline;  *)
            if Util.within_epsilon z 0.0 then (label, 0.0) else
              let prob = (Wmc.wmc (Bdd.dand bdd zbdd) compiled.ctx.weights) /. z in
              (label, prob)) in

lib/BddUtil.ml

@@ -34,5 +34,6 @@ 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 ()
 

lib/Compiler.mli

@@ -3,24 +3,30 @@ 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 *)
   funcs: (String.t, compiled_func) Hashtbl.Poly.t;
 }