From 516de35a2ea638dfa20a1495a2b357e337b4a355 Mon Sep 17 00:00:00 2001
From: Steffen Juilf Smolka <smolka@cs.cornell.edu>
Date: Tue, 4 Apr 2017 20:11:48 -0400
Subject: [PATCH 01/29] skeleton

---
 _oasis                           |  1 +
 lib/Frenetic_NetKAT_Compiler.mli |  6 +++++-
 lib/frenetic.mldylib             |  3 ++-
 lib/frenetic.mllib               |  3 ++-
 lib/frenetic.odocl               |  3 ++-
 myocamlbuild.ml                  |  9 +++------
 setup.ml                         | 25 ++++++++++++-------------
 7 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/_oasis b/_oasis
index b162bdef4..6a06bb425 100644
--- a/_oasis
+++ b/_oasis
@@ -75,6 +75,7 @@ Library frenetic
     Frenetic_NetKAT_Optimize,
     Frenetic_NetKAT_Json,
     Frenetic_NetKAT_Compiler,
+    Frenetic_NetKAT_Equivalence,
     Frenetic_NetKAT_FabricGen,
     Frenetic_NetKAT_Virtual_Compiler,
     Frenetic_NetKAT_Net,
diff --git a/lib/Frenetic_NetKAT_Compiler.mli b/lib/Frenetic_NetKAT_Compiler.mli
index 745d0559f..1b7f9bfc6 100644
--- a/lib/Frenetic_NetKAT_Compiler.mli
+++ b/lib/Frenetic_NetKAT_Compiler.mli
@@ -18,7 +18,11 @@ val to_dot : t -> string
 
 (** Intermediate representation of global compiler: NetKAT Automata *)
 module Automaton : sig
-  type t
+  type t = private
+    { states : (FDD.t * FDD.t) Int.Table.t;
+      has_state : int FDD.BinTbl.t;
+      mutable source : int;
+      mutable nextState : int }
 
   val fold_reachable: ?order:[< `Post | `Pre > `Pre ]
     -> t
diff --git a/lib/frenetic.mldylib b/lib/frenetic.mldylib
index 956d58c00..9c37f7c15 100644
--- a/lib/frenetic.mldylib
+++ b/lib/frenetic.mldylib
@@ -1,5 +1,5 @@
 # OASIS_START
-# DO NOT EDIT (digest: aa47c387d90c3ea5d993b5e40851f91e)
+# DO NOT EDIT (digest: dac1e5fb1a72b6ef8cd3e272bff307a0)
 Frenetic_Hashcons
 Frenetic_Bits
 Frenetic_Fdd
@@ -11,6 +11,7 @@ Frenetic_NetKAT_Parser
 Frenetic_NetKAT_Optimize
 Frenetic_NetKAT_Json
 Frenetic_NetKAT_Compiler
+Frenetic_NetKAT_Equivalence
 Frenetic_NetKAT_FabricGen
 Frenetic_NetKAT_Virtual_Compiler
 Frenetic_NetKAT_Net
diff --git a/lib/frenetic.mllib b/lib/frenetic.mllib
index 956d58c00..9c37f7c15 100644
--- a/lib/frenetic.mllib
+++ b/lib/frenetic.mllib
@@ -1,5 +1,5 @@
 # OASIS_START
-# DO NOT EDIT (digest: aa47c387d90c3ea5d993b5e40851f91e)
+# DO NOT EDIT (digest: dac1e5fb1a72b6ef8cd3e272bff307a0)
 Frenetic_Hashcons
 Frenetic_Bits
 Frenetic_Fdd
@@ -11,6 +11,7 @@ Frenetic_NetKAT_Parser
 Frenetic_NetKAT_Optimize
 Frenetic_NetKAT_Json
 Frenetic_NetKAT_Compiler
+Frenetic_NetKAT_Equivalence
 Frenetic_NetKAT_FabricGen
 Frenetic_NetKAT_Virtual_Compiler
 Frenetic_NetKAT_Net
diff --git a/lib/frenetic.odocl b/lib/frenetic.odocl
index bbc8a4ed2..c37882fdc 100644
--- a/lib/frenetic.odocl
+++ b/lib/frenetic.odocl
@@ -1,5 +1,5 @@
 # OASIS_START
-# DO NOT EDIT (digest: bd4dfcfd19247c71102a7f3458a16834)
+# DO NOT EDIT (digest: 17e5fb544db46ab709a34ee06e7bc4f7)
 Frenetic_Hashcons
 Frenetic_Bits
 Frenetic_Fdd
@@ -11,6 +11,7 @@ Frenetic_NetKAT_Parser
 Frenetic_NetKAT_Optimize
 Frenetic_NetKAT_Json
 Frenetic_NetKAT_Compiler
+Frenetic_NetKAT_Equivalence
 Frenetic_NetKAT_FabricGen
 Frenetic_NetKAT_Virtual_Compiler
 Frenetic_NetKAT_Net
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 3d03a0f32..672c3f29f 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -1,5 +1,5 @@
 (* OASIS_START *)
-(* DO NOT EDIT (digest: 35df006ca2eac8c1341346e61ce5231a) *)
+(* DO NOT EDIT (digest: 6461dd9639d34b17f1cbbce97fba55a2) *)
 module OASISGettext = struct
 (* # 22 "src/oasis/OASISGettext.ml" *)
 
@@ -746,9 +746,6 @@ module MyOCamlbuildBase = struct
 (* # 110 "src/plugins/ocamlbuild/MyOCamlbuildBase.ml" *)
 
 
-  let env_filename = Pathname.basename BaseEnvLight.default_filename
-
-
   let dispatch_combine lst =
     fun e ->
       List.iter
@@ -881,7 +878,7 @@ module MyOCamlbuildBase = struct
 end
 
 
-# 884 "myocamlbuild.ml"
+# 881 "myocamlbuild.ml"
 open Ocamlbuild_plugin;;
 let package_default =
   {
@@ -910,7 +907,7 @@ let conf = {MyOCamlbuildFindlib.no_automatic_syntax = false}
 
 let dispatch_default = MyOCamlbuildBase.dispatch_default conf package_default;;
 
-# 914 "myocamlbuild.ml"
+# 911 "myocamlbuild.ml"
 (* OASIS_STOP *)
 
 (* SJS: use shared extern token file *)
diff --git a/setup.ml b/setup.ml
index 76fdf5385..61fc06b13 100644
--- a/setup.ml
+++ b/setup.ml
@@ -1,9 +1,9 @@
 (* setup.ml generated for the first time by OASIS v0.4.7 *)
 
 (* OASIS_START *)
-(* DO NOT EDIT (digest: ae04e8316a530295f962b0dc90a6b5f0) *)
+(* DO NOT EDIT (digest: 8354747a8793258042c14c268d3ee451) *)
 (*
-   Regenerated by OASIS v0.4.8
+   Regenerated by OASIS v0.4.7
    Visit http://oasis.forge.ocamlcore.org for more information and
    documentation about functions used in this file.
 *)
@@ -658,7 +658,6 @@ module OASISContext = struct
       ignore_unknown_fields: bool;
       printf:                level -> string -> unit;
       srcfs:                 source OASISFileSystem.fs;
-      load_oasis_plugin:     string -> bool;
     }
 
 
@@ -683,7 +682,6 @@ module OASISContext = struct
         ignore_unknown_fields = false;
         printf                = printf;
         srcfs                 = new OASISFileSystem.host_fs(Sys.getcwd ());
-        load_oasis_plugin     = (fun _ -> false);
       }
 
 
@@ -3162,7 +3160,7 @@ module OASISFileUtil = struct
 end
 
 
-# 3165 "setup.ml"
+# 3163 "setup.ml"
 module BaseEnvLight = struct
 (* # 22 "src/base/BaseEnvLight.ml" *)
 
@@ -3242,7 +3240,7 @@ module BaseEnvLight = struct
 end
 
 
-# 3245 "setup.ml"
+# 3243 "setup.ml"
 module BaseContext = struct
 (* # 22 "src/base/BaseContext.ml" *)
 
@@ -5665,7 +5663,7 @@ module BaseCompat = struct
 end
 
 
-# 5668 "setup.ml"
+# 5666 "setup.ml"
 module InternalConfigurePlugin = struct
 (* # 22 "src/plugins/internal/InternalConfigurePlugin.ml" *)
 
@@ -6471,7 +6469,7 @@ module InternalInstallPlugin = struct
 end
 
 
-# 6474 "setup.ml"
+# 6472 "setup.ml"
 module OCamlbuildCommon = struct
 (* # 22 "src/plugins/ocamlbuild/OCamlbuildCommon.ml" *)
 
@@ -6844,7 +6842,7 @@ module OCamlbuildDocPlugin = struct
 end
 
 
-# 6847 "setup.ml"
+# 6845 "setup.ml"
 module CustomPlugin = struct
 (* # 22 "src/plugins/custom/CustomPlugin.ml" *)
 
@@ -6976,7 +6974,7 @@ module CustomPlugin = struct
 end
 
 
-# 6979 "setup.ml"
+# 6977 "setup.ml"
 open OASISTypes;;
 
 let setup_t =
@@ -7273,6 +7271,7 @@ let setup_t =
                            "Frenetic_NetKAT_Optimize";
                            "Frenetic_NetKAT_Json";
                            "Frenetic_NetKAT_Compiler";
+                           "Frenetic_NetKAT_Equivalence";
                            "Frenetic_NetKAT_FabricGen";
                            "Frenetic_NetKAT_Virtual_Compiler";
                            "Frenetic_NetKAT_Net";
@@ -8951,8 +8950,8 @@ let setup_t =
           plugin_data = []
        };
      oasis_fn = Some "_oasis";
-     oasis_version = "0.4.8";
-     oasis_digest = Some "\020i\211N\209\205\167?\224g\152\189c(\243\021";
+     oasis_version = "0.4.7";
+     oasis_digest = Some "+\213\028tm6\151 \b\226\202!\"\155\026\193";
      oasis_exec = None;
      oasis_setup_args = [];
      setup_update = false
@@ -8960,7 +8959,7 @@ let setup_t =
 
 let setup () = BaseSetup.setup setup_t;;
 
-# 8964 "setup.ml"
+# 8963 "setup.ml"
 let setup_t = BaseCompat.Compat_0_4.adapt_setup_t setup_t
 open BaseCompat.Compat_0_4
 (* OASIS_STOP *)

From 339dbc9a8956d9e73f57953b0a1ab63d7b85cd37 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Tue, 4 Apr 2017 18:56:12 -0700
Subject: [PATCH 02/29] real seleton

---
 lib/Frenetic_NetKAT_Equivalence.ml | 53 ++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 lib/Frenetic_NetKAT_Equivalence.ml

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
new file mode 100644
index 000000000..f5d5e0e13
--- /dev/null
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -0,0 +1,53 @@
+open Core.Std
+
+module A = Frenetic_NetKAT_Compiler.Automaton
+module FDD = struct
+  include Frenetic_NetKAT_Compiler.FDD
+  include (struct include Frenetic_NetKAT_Compiler end : sig
+    val seq : t -> t -> t
+  end)
+
+  let rec strict_equal (x : t) (y : t) =
+    match unget x, unget y with
+    | Branch((vx, lx), tx, fx), Branch((vy, ly), ty, fy) ->
+      begin match Frenetic_Fdd.Field.compare vx vy with
+      |  0 ->
+        begin match Frenetic_Fdd.Value.compare lx ly with
+        |  0 -> strict_equal tx ty && strict_equal fx fy
+        | -1 -> failwith "todo"
+        |  1 -> failwith "todo"
+        |  _ -> assert false
+        end
+      | -1 -> failwith "todo"
+      |  1 -> failwith "todo"
+      |  _ -> assert false
+      end
+end
+
+
+module Naive = struct
+
+  type state = int
+  type mask = FDD.t
+
+  let equiv ?(mask=FDD.id) (a1 : A.t) (a2 : A.t) =
+    let cache = Hash_set.Poly.create () in
+    
+    let rec eq_states (s1 as a, x : mask * state) (s2 as b, y : mask * state) =
+      Hash_set.mem cache (s1,s2) || begin
+        Hash_set.add cache (s1,s2);
+        eq_states' (a, Hashtbl.find_exn a1.states x)
+                   (b, Hashtbl.find_exn a2.states y)
+      end
+
+    and eq_states' (a, (e1,d1) : mask * (FDD.t * FDD.t))
+                   (b, (e2,d2) : mask * (FDD.t * FDD.t)) =
+      FDD.strict_equal (FDD.seq a e1) (FDD.seq b e2) && eq_ds (a, d1) (b,d2)
+
+    and eq_ds (a, d1) (b, d2) =
+      true
+
+    in
+    eq_states (mask, a1.source) (mask, a2.source)
+
+end

From 7fa30fd2d946c2e7f4697e97781cf66f43ab349f Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 6 Apr 2017 11:17:28 -0700
Subject: [PATCH 03/29] more

---
 lib/Frenetic_NetKAT_Equivalence.ml | 62 ++++++++++++++++++++++++------
 1 file changed, 50 insertions(+), 12 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index f5d5e0e13..9e3a84986 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -28,24 +28,62 @@ end
 module Naive = struct
 
   type state = int
-  type mask = FDD.t
 
-  let equiv ?(mask=FDD.id) (a1 : A.t) (a2 : A.t) =
+  module SymPkt = struct
+    include Map.Make(FDD.Field) with type 'a = FDD.Value.t
+    let all = emtpy
+  end
+
+  let equiv ?(pk=SymPkt.all) (a1 : A.t) (a2 : A.t) =
     let cache = Hash_set.Poly.create () in
     
-    let rec eq_states (s1 as a, x : mask * state) (s2 as b, y : mask * state) =
-      Hash_set.mem cache (s1,s2) || begin
-        Hash_set.add cache (s1,s2);
-        eq_states' (a, Hashtbl.find_exn a1.states x)
-                   (b, Hashtbl.find_exn a2.states y)
+    let rec eq_states pk (s1 : state) (s2 : state) =
+      let mask = SymPkt.to_alist pk in
+      let (e1, d1) = Hashtbl.find_exn a1.states s1 in
+      let (e2, d2) = Hashtbl.find_exn a1.states s2 in
+      let (e1, d1) = FDD.(restrict mask e1, restrict mask d1) in
+      let (e2, d2) = FDD.(restrict mask e2, restrict mask d2) in
+      Hash_set.mem cache (e1,d1,e2,d2) || begin
+        Hash_set.add cache (e1,d1,e2,d2);
+        eq_es pk e1 e2 && eq_ds pk d1 d2
       end
 
-    and eq_states' (a, (e1,d1) : mask * (FDD.t * FDD.t))
-                   (b, (e2,d2) : mask * (FDD.t * FDD.t)) =
-      FDD.strict_equal (FDD.seq a e1) (FDD.seq b e2) && eq_ds (a, d1) (b,d2)
+    and eq_es pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
+      let pks1 = Set.Poly.map par1 ~f:(Map.fold ~init:pk ~f:SymPkt.add) in
+      let pks2 = Set.Poly.map par2 ~f:(Map.fold ~init:pk ~f:SymPkt.add) in
+      Set.Poly.equal (SymPkt.equal FDD.Value.equal) pks1 pks2
+    end
+
+    and eq_ds pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
+      failwith "todo"
+    end
 
-    and eq_ds (a, d1) (b, d2) =
-      true
+    and eq_fdd ~leaf_eq pk fdd1 fdd2 =
+      match FDD.(unget fdd1, fdd1, unget fdd2, fdd2) with
+      | Leaf r1,_, Leaf r2,_ ->
+        leaf_eq pk r1 r2
+      | Leaf _,fdd, Leaf ((f,n), tru, fls),_
+      | Leaf ((f,n), tru, fls),_, Leaf _,fdd ->
+        eq_fdd ~leaf_eq pk fdd fls && begin
+          let pk' = SymPkt.add pk ~key:f ~data:n in
+          match SymPkt.find pk f with
+          | None 
+          | Some m when m = n -> eq_fdd ~leaf_eq pk' fdd1 fls
+          | _ -> true
+        end
+      | Branch((vx, lx), tx, fx), Branch((vy, ly), ty, fy) ->
+        begin match V.compare vx vy with
+        |  0 ->
+          begin match L.compare lx ly with
+          |  0 -> mk_branch (vx,lx) (sum tx ty) (sum fx fy)
+          | -1 -> mk_branch (vx,lx) (sum tx (restrict [(vx, lx)] y)) (sum fx y)
+          |  1 -> mk_branch (vy,ly) (sum (restrict [(vy, ly)] x) ty) (sum x fy)
+          |  _ -> assert false
+          end
+        | -1 -> mk_branch (vx,lx) (sum tx y) (sum fx y)
+        |  1 -> mk_branch (vy,ly) (sum x ty) (sum x fy)
+        |  _ -> assert false
+        end
 
     in
     eq_states (mask, a1.source) (mask, a2.source)

From c57db7807294094370e45a8c44204596e7ada596 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 6 Apr 2017 18:07:11 -0400
Subject: [PATCH 04/29] checkpoint that compiles

---
 lib/Frenetic_NetKAT_Equivalence.ml | 83 +++++++++++-------------------
 1 file changed, 31 insertions(+), 52 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 9e3a84986..aaa939b47 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -1,28 +1,7 @@
 open Core.Std
 
 module A = Frenetic_NetKAT_Compiler.Automaton
-module FDD = struct
-  include Frenetic_NetKAT_Compiler.FDD
-  include (struct include Frenetic_NetKAT_Compiler end : sig
-    val seq : t -> t -> t
-  end)
-
-  let rec strict_equal (x : t) (y : t) =
-    match unget x, unget y with
-    | Branch((vx, lx), tx, fx), Branch((vy, ly), ty, fy) ->
-      begin match Frenetic_Fdd.Field.compare vx vy with
-      |  0 ->
-        begin match Frenetic_Fdd.Value.compare lx ly with
-        |  0 -> strict_equal tx ty && strict_equal fx fy
-        | -1 -> failwith "todo"
-        |  1 -> failwith "todo"
-        |  _ -> assert false
-        end
-      | -1 -> failwith "todo"
-      |  1 -> failwith "todo"
-      |  _ -> assert false
-      end
-end
+module FDD = Frenetic_NetKAT_Compiler.FDD
 
 
 module Naive = struct
@@ -30,8 +9,8 @@ module Naive = struct
   type state = int
 
   module SymPkt = struct
-    include Map.Make(FDD.Field) with type 'a = FDD.Value.t
-    let all = emtpy
+    include Map.Make(Frenetic_Fdd.Field)
+    let all = empty
   end
 
   let equiv ?(pk=SymPkt.all) (a1 : A.t) (a2 : A.t) =
@@ -49,43 +28,43 @@ module Naive = struct
       end
 
     and eq_es pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
-      let pks1 = Set.Poly.map par1 ~f:(Map.fold ~init:pk ~f:SymPkt.add) in
-      let pks2 = Set.Poly.map par2 ~f:(Map.fold ~init:pk ~f:SymPkt.add) in
-      Set.Poly.equal (SymPkt.equal FDD.Value.equal) pks1 pks2
+      (* let add ~key ~data m = SymPkt.add m ~key ~data in *)
+      (* let pks1 = Set.Poly.map par1 ~f:(Map.fold ~init:pk ~f:add) in *)
+      (* let pks2 = Set.Poly.map par2 ~f:(Map.fold ~init:pk ~f:add) in *)
+      (* Set.equal pks1 pks2 *)
+      failwith "todo"
     end
 
     and eq_ds pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
       failwith "todo"
     end
 
-    and eq_fdd ~leaf_eq pk fdd1 fdd2 =
-      match FDD.(unget fdd1, fdd1, unget fdd2, fdd2) with
-      | Leaf r1,_, Leaf r2,_ ->
+    and eq_fdd ~leaf_eq pk x y =
+      let check_with pk f n x y =
+        match SymPkt.find pk f with
+        | None ->
+          eq_fdd ~leaf_eq (SymPkt.add pk ~key:f ~data:n) x y
+        | Some m -> 
+          m <> n || eq_fdd ~leaf_eq pk x y
+      in
+      match FDD.(unget x, unget y) with
+      | Leaf r1, Leaf r2 ->
         leaf_eq pk r1 r2
-      | Leaf _,fdd, Leaf ((f,n), tru, fls),_
-      | Leaf ((f,n), tru, fls),_, Leaf _,fdd ->
-        eq_fdd ~leaf_eq pk fdd fls && begin
-          let pk' = SymPkt.add pk ~key:f ~data:n in
-          match SymPkt.find pk f with
-          | None 
-          | Some m when m = n -> eq_fdd ~leaf_eq pk' fdd1 fls
-          | _ -> true
-        end
-      | Branch((vx, lx), tx, fx), Branch((vy, ly), ty, fy) ->
-        begin match V.compare vx vy with
-        |  0 ->
-          begin match L.compare lx ly with
-          |  0 -> mk_branch (vx,lx) (sum tx ty) (sum fx fy)
-          | -1 -> mk_branch (vx,lx) (sum tx (restrict [(vx, lx)] y)) (sum fx y)
-          |  1 -> mk_branch (vy,ly) (sum (restrict [(vy, ly)] x) ty) (sum x fy)
-          |  _ -> assert false
-          end
-        | -1 -> mk_branch (vx,lx) (sum tx y) (sum fx y)
-        |  1 -> mk_branch (vy,ly) (sum x ty) (sum x fy)
-        |  _ -> assert false
+      | Branch ((f,n), xt, xf), Leaf _ ->
+        check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
+      | Leaf _, Branch ((g,m), yt, yf) ->
+        check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
+      | Branch((f, n), xt, xf), Branch((g, m), yt, yf) ->
+        begin match Frenetic_Fdd.(Field.compare f g, Value.compare m n) with
+        |  0,  0 -> check_with pk f n xt yt && eq_fdd ~leaf_eq pk xf yf 
+        | -1,  _
+        |  0, -1 -> check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
+        |  1,  _
+        |  0,  1 -> check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
+        |  _     -> assert false
         end
 
     in
-    eq_states (mask, a1.source) (mask, a2.source)
+    eq_states pk a1.source a2.source
 
 end

From 14d2aa501c5ff63d5ef5a189f60274fd68c491e5 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 6 Apr 2017 18:41:17 -0400
Subject: [PATCH 05/29] eq_es

---
 lib/Frenetic_NetKAT_Equivalence.ml | 28 ++++++++++++++++++++--------
 1 file changed, 20 insertions(+), 8 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index aaa939b47..fa1487831 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -9,10 +9,27 @@ module Naive = struct
   type state = int
 
   module SymPkt = struct
-    include Map.Make(Frenetic_Fdd.Field)
+    module T = Map.Make(Frenetic_Fdd.Field)
+    include T
+
     let all = empty
+
+    module Set = Set.Make(struct
+      type t = Frenetic_Fdd.Value.t T.t [@@deriving sexp]
+      let compare = compare Frenetic_Fdd.Value.compare
+    end)
+
+    let apply_seq pk seq =
+      Frenetic_Fdd.Action.Seq.to_hvs seq
+      |> List.fold ~init:pk ~f:(fun pk (key,data) -> add pk ~key ~data)
+
+    let apply_par pk par : Set.t =
+      Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
+        Set.add pks (apply_seq pk seq))
   end
 
+
+
   let equiv ?(pk=SymPkt.all) (a1 : A.t) (a2 : A.t) =
     let cache = Hash_set.Poly.create () in
     
@@ -27,13 +44,8 @@ module Naive = struct
         eq_es pk e1 e2 && eq_ds pk d1 d2
       end
 
-    and eq_es pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
-      (* let add ~key ~data m = SymPkt.add m ~key ~data in *)
-      (* let pks1 = Set.Poly.map par1 ~f:(Map.fold ~init:pk ~f:add) in *)
-      (* let pks2 = Set.Poly.map par2 ~f:(Map.fold ~init:pk ~f:add) in *)
-      (* Set.equal pks1 pks2 *)
-      failwith "todo"
-    end
+    and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
+      SymPkt.(Set.equal (apply_par pk par1) (apply_par pk par1)))
 
     and eq_ds pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
       failwith "todo"

From 4218adc29c408ebe50d592712e965d5c46dfb520 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 6 Apr 2017 21:14:46 -0400
Subject: [PATCH 06/29] fix

---
 lib/Frenetic_NetKAT_Equivalence.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index fa1487831..1b6dedc95 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -45,7 +45,7 @@ module Naive = struct
       end
 
     and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
-      SymPkt.(Set.equal (apply_par pk par1) (apply_par pk par1)))
+      SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2)
 
     and eq_ds pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
       failwith "todo"

From 5bf392a0a2dce4632abf8a3b33ea7ce423fc98bd Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 6 Apr 2017 21:31:14 -0400
Subject: [PATCH 07/29] factor out upto

---
 lib/Frenetic_NetKAT_Equivalence.ml | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 1b6dedc95..c3c9bdcb1 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -3,10 +3,21 @@ open Core.Std
 module A = Frenetic_NetKAT_Compiler.Automaton
 module FDD = Frenetic_NetKAT_Compiler.FDD
 
+type state = FDD.t * FDD.t
 
-module Naive = struct
+module type UPTO = sig
+  val add_equiv : state -> state -> unit
+  val equiv : state -> state -> bool
+end
+
+module Upto_Sym () : UPTO = struct
+  (* FIXME: avoid polymorphic hash/max/min *)
+  let cache = Hash_set.Poly.create ()
+  let equiv s1 s2 = Hash_set.mem cache (min s1 s2, max s1 s2)
+  let add_equiv s1 s2 = Hash_set.add cache (min s1 s2, max s1 s2)
+end
 
-  type state = int
+module Make_Naive(Upto : UPTO) = struct
 
   module SymPkt = struct
     module T = Map.Make(Frenetic_Fdd.Field)
@@ -31,21 +42,20 @@ module Naive = struct
 
 
   let equiv ?(pk=SymPkt.all) (a1 : A.t) (a2 : A.t) =
-    let cache = Hash_set.Poly.create () in
     
-    let rec eq_states pk (s1 : state) (s2 : state) =
+    let rec eq_states pk (s1 : int) (s2 : int) =
       let mask = SymPkt.to_alist pk in
       let (e1, d1) = Hashtbl.find_exn a1.states s1 in
       let (e2, d2) = Hashtbl.find_exn a1.states s2 in
-      let (e1, d1) = FDD.(restrict mask e1, restrict mask d1) in
-      let (e2, d2) = FDD.(restrict mask e2, restrict mask d2) in
-      Hash_set.mem cache (e1,d1,e2,d2) || begin
-        Hash_set.add cache (e1,d1,e2,d2);
+      let ((e1, d1) as s1) = FDD.(restrict mask e1, restrict mask d1) in
+      let ((e2, d2) as s2) = FDD.(restrict mask e2, restrict mask d2) in
+      Upto.equiv s1 s2 || begin
+        Upto.add_equiv s1 s2;
         eq_es pk e1 e2 && eq_ds pk d1 d2
       end
 
     and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
-      SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2)
+      SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2))
 
     and eq_ds pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
       failwith "todo"

From 1022bf927cda52c72a33462cd89bb573ee6dedb7 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 6 Apr 2017 21:41:54 -0400
Subject: [PATCH 08/29] upto transitivity (Hopcroft Karp)

---
 lib/Frenetic_NetKAT_Equivalence.ml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index c3c9bdcb1..d8bb069d3 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -1,6 +1,6 @@
 open Core.Std
 
-module A = Frenetic_NetKAT_Compiler.Automaton
+module Automaton = Frenetic_NetKAT_Compiler.Automaton
 module FDD = Frenetic_NetKAT_Compiler.FDD
 
 type state = FDD.t * FDD.t
@@ -11,12 +11,20 @@ module type UPTO = sig
 end
 
 module Upto_Sym () : UPTO = struct
-  (* FIXME: avoid polymorphic hash/max/min *)
+  (* FIXME: avoid polymorphic hash/max/min/equality *)
   let cache = Hash_set.Poly.create ()
-  let equiv s1 s2 = Hash_set.mem cache (min s1 s2, max s1 s2)
+  let equiv s1 s2 = (s1 = s2) || Hash_set.mem cache (min s1 s2, max s1 s2)
   let add_equiv s1 s2 = Hash_set.add cache (min s1 s2, max s1 s2)
 end
 
+module Upto_Trans () : UPTO = struct
+  (* FIXME: avoid polymorphic hash/max/min/equality *)
+  let cache = Hashtbl.Poly.create ()
+  let find = Hashtbl.find_or_add cache ~default:Union_find.create
+  let equiv s1 s2 = (s1 = s2) || Union_find.same_class (find s1) (find s2)
+  let add_equiv s1 s2 = Union_find.union (find s1) (find s2)
+end
+
 module Make_Naive(Upto : UPTO) = struct
 
   module SymPkt = struct
@@ -41,7 +49,7 @@ module Make_Naive(Upto : UPTO) = struct
 
 
 
-  let equiv ?(pk=SymPkt.all) (a1 : A.t) (a2 : A.t) =
+  let equiv ?(pk=SymPkt.all) (a1 : Automaton.t) (a2 : Automaton.t) =
     
     let rec eq_states pk (s1 : int) (s2 : int) =
       let mask = SymPkt.to_alist pk in

From 7939576738a007c43cfd73561f0e9bbfc196dc6d Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 14:37:58 -0400
Subject: [PATCH 09/29] transition trees

---
 lib/Frenetic_NetKAT_Equivalence.ml | 34 ++++++++++++++++++++++++++++++
 myocamlbuild.ml                    |  9 +++++---
 setup.ml                           | 22 ++++++++++---------
 3 files changed, 52 insertions(+), 13 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index d8bb069d3..fba2d96eb 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -3,6 +3,11 @@ open Core.Std
 module Automaton = Frenetic_NetKAT_Compiler.Automaton
 module FDD = Frenetic_NetKAT_Compiler.FDD
 
+
+(*===========================================================================*)
+(* UPTO                                                                      *)
+(*===========================================================================*)
+
 type state = FDD.t * FDD.t
 
 module type UPTO = sig
@@ -10,6 +15,7 @@ module type UPTO = sig
   val equiv : state -> state -> bool
 end
 
+(* upto reflexivity & symmetry *)
 module Upto_Sym () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
   let cache = Hash_set.Poly.create ()
@@ -17,6 +23,7 @@ module Upto_Sym () : UPTO = struct
   let add_equiv s1 s2 = Hash_set.add cache (min s1 s2, max s1 s2)
 end
 
+(* upto reflexivity & symmetry & transitivity (Hopcroft-Karp) *)
 module Upto_Trans () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
   let cache = Hashtbl.Poly.create ()
@@ -25,6 +32,33 @@ module Upto_Trans () : UPTO = struct
   let add_equiv s1 s2 = Union_find.union (find s1) (find s2)
 end
 
+
+
+(*===========================================================================*)
+(* Transition Trees                                                          *)
+(*===========================================================================*)
+
+module Trans_Tree = Frenetic_Vlr.Make(Frenetic_Fdd.Field)(Frenetic_Fdd.Value)(struct
+
+  type t = Int.Set.t * Int.Set.t [@@deriving sexp, compare]
+  let hash = Hashtbl.hash
+  let to_string t = sexp_of_t t |> Sexp.to_string
+
+  let zero = (Int.Set.empty, Int.Set.empty)
+  let sum (l1, r1) (l2, r2) = (Set.union l1 l2, Set.union r1 r2)
+
+  (* SJS: no one or product *)
+  let one = zero
+  let prod _ _ = failwith "no product"
+
+end)
+
+
+
+(*===========================================================================*)
+(* Decision Procedure                                                        *)
+(*===========================================================================*)
+
 module Make_Naive(Upto : UPTO) = struct
 
   module SymPkt = struct
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 672c3f29f..3d03a0f32 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -1,5 +1,5 @@
 (* OASIS_START *)
-(* DO NOT EDIT (digest: 6461dd9639d34b17f1cbbce97fba55a2) *)
+(* DO NOT EDIT (digest: 35df006ca2eac8c1341346e61ce5231a) *)
 module OASISGettext = struct
 (* # 22 "src/oasis/OASISGettext.ml" *)
 
@@ -746,6 +746,9 @@ module MyOCamlbuildBase = struct
 (* # 110 "src/plugins/ocamlbuild/MyOCamlbuildBase.ml" *)
 
 
+  let env_filename = Pathname.basename BaseEnvLight.default_filename
+
+
   let dispatch_combine lst =
     fun e ->
       List.iter
@@ -878,7 +881,7 @@ module MyOCamlbuildBase = struct
 end
 
 
-# 881 "myocamlbuild.ml"
+# 884 "myocamlbuild.ml"
 open Ocamlbuild_plugin;;
 let package_default =
   {
@@ -907,7 +910,7 @@ let conf = {MyOCamlbuildFindlib.no_automatic_syntax = false}
 
 let dispatch_default = MyOCamlbuildBase.dispatch_default conf package_default;;
 
-# 911 "myocamlbuild.ml"
+# 914 "myocamlbuild.ml"
 (* OASIS_STOP *)
 
 (* SJS: use shared extern token file *)
diff --git a/setup.ml b/setup.ml
index 61fc06b13..59aa35dff 100644
--- a/setup.ml
+++ b/setup.ml
@@ -1,9 +1,9 @@
 (* setup.ml generated for the first time by OASIS v0.4.7 *)
 
 (* OASIS_START *)
-(* DO NOT EDIT (digest: 8354747a8793258042c14c268d3ee451) *)
+(* DO NOT EDIT (digest: 8d2d24c31edcbfb86f8028e2dd3074e6) *)
 (*
-   Regenerated by OASIS v0.4.7
+   Regenerated by OASIS v0.4.8
    Visit http://oasis.forge.ocamlcore.org for more information and
    documentation about functions used in this file.
 *)
@@ -658,6 +658,7 @@ module OASISContext = struct
       ignore_unknown_fields: bool;
       printf:                level -> string -> unit;
       srcfs:                 source OASISFileSystem.fs;
+      load_oasis_plugin:     string -> bool;
     }
 
 
@@ -682,6 +683,7 @@ module OASISContext = struct
         ignore_unknown_fields = false;
         printf                = printf;
         srcfs                 = new OASISFileSystem.host_fs(Sys.getcwd ());
+        load_oasis_plugin     = (fun _ -> false);
       }
 
 
@@ -3160,7 +3162,7 @@ module OASISFileUtil = struct
 end
 
 
-# 3163 "setup.ml"
+# 3165 "setup.ml"
 module BaseEnvLight = struct
 (* # 22 "src/base/BaseEnvLight.ml" *)
 
@@ -3240,7 +3242,7 @@ module BaseEnvLight = struct
 end
 
 
-# 3243 "setup.ml"
+# 3245 "setup.ml"
 module BaseContext = struct
 (* # 22 "src/base/BaseContext.ml" *)
 
@@ -5663,7 +5665,7 @@ module BaseCompat = struct
 end
 
 
-# 5666 "setup.ml"
+# 5668 "setup.ml"
 module InternalConfigurePlugin = struct
 (* # 22 "src/plugins/internal/InternalConfigurePlugin.ml" *)
 
@@ -6469,7 +6471,7 @@ module InternalInstallPlugin = struct
 end
 
 
-# 6472 "setup.ml"
+# 6474 "setup.ml"
 module OCamlbuildCommon = struct
 (* # 22 "src/plugins/ocamlbuild/OCamlbuildCommon.ml" *)
 
@@ -6842,7 +6844,7 @@ module OCamlbuildDocPlugin = struct
 end
 
 
-# 6845 "setup.ml"
+# 6847 "setup.ml"
 module CustomPlugin = struct
 (* # 22 "src/plugins/custom/CustomPlugin.ml" *)
 
@@ -6974,7 +6976,7 @@ module CustomPlugin = struct
 end
 
 
-# 6977 "setup.ml"
+# 6979 "setup.ml"
 open OASISTypes;;
 
 let setup_t =
@@ -8950,7 +8952,7 @@ let setup_t =
           plugin_data = []
        };
      oasis_fn = Some "_oasis";
-     oasis_version = "0.4.7";
+     oasis_version = "0.4.8";
      oasis_digest = Some "+\213\028tm6\151 \b\226\202!\"\155\026\193";
      oasis_exec = None;
      oasis_setup_args = [];
@@ -8959,7 +8961,7 @@ let setup_t =
 
 let setup () = BaseSetup.setup setup_t;;
 
-# 8963 "setup.ml"
+# 8965 "setup.ml"
 let setup_t = BaseCompat.Compat_0_4.adapt_setup_t setup_t
 open BaseCompat.Compat_0_4
 (* OASIS_STOP *)

From 74eaeb4538c963ab3a46029dd42b3a5fc1f408e4 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 15:09:40 -0400
Subject: [PATCH 10/29] transition trees

---
 lib/Frenetic_NetKAT_Equivalence.ml | 42 +++++++++++++++++++++---------
 1 file changed, 30 insertions(+), 12 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index fba2d96eb..9518a4692 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -38,20 +38,38 @@ end
 (* Transition Trees                                                          *)
 (*===========================================================================*)
 
-module Trans_Tree = Frenetic_Vlr.Make(Frenetic_Fdd.Field)(Frenetic_Fdd.Value)(struct
-
-  type t = Int.Set.t * Int.Set.t [@@deriving sexp, compare]
-  let hash = Hashtbl.hash
-  let to_string t = sexp_of_t t |> Sexp.to_string
-
-  let zero = (Int.Set.empty, Int.Set.empty)
-  let sum (l1, r1) (l2, r2) = (Set.union l1 l2, Set.union r1 r2)
+module Trans_Tree = struct
+  include Frenetic_Vlr.Make(Frenetic_Fdd.Field)(Frenetic_Fdd.Value)(struct
+    type t = Int.Set.t * Int.Set.t [@@deriving sexp, compare]
+    let hash = Hashtbl.hash
+    let to_string t = sexp_of_t t |> Sexp.to_string
+
+    let zero = (Int.Set.empty, Int.Set.empty)
+    let sum (l1, r1) (l2, r2) = (Set.union l1 l2, Set.union r1 r2)
+
+    (* SJS: no one or product *)
+    let one = zero
+    let prod _ _ = failwith "no product"
+  end)
+
+  let of_seq inj seq =
+    let leaf =
+      Frenetic_Fdd.Action.(Seq.find_exn seq K)
+      |> Frenetic_Fdd.Value.to_int_exn
+      |> inj
+      |> const
+    in
+    Frenetic_Fdd.Action.Seq.to_hvs seq
+    |> List.fold ~init:leaf ~f:(fun tree test -> cond test tree drop)
 
-  (* SJS: no one or product *)
-  let one = zero
-  let prod _ _ = failwith "no product"
+  let of_par inj par =
+    Frenetic_Fdd.Action.Par.fold par
+      ~init:drop 
+      ~f:(fun acc seq -> sum acc (of_seq inj seq))
 
-end)
+  let of_left_par = of_par (fun i -> (Int.Set.singleton i, Int.Set.empty))
+  let of_right_par = of_par (fun i -> (Int.Set.empty, Int.Set.singleton i))
+end
 
 
 

From 0b1879a7181c5f5e3d6fb010980f6924fdfc9f0d Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 15:28:04 -0400
Subject: [PATCH 11/29] full decision procedure

---
 lib/Frenetic_NetKAT_Compiler.mli   |  8 +++++++-
 lib/Frenetic_NetKAT_Equivalence.ml | 29 ++++++++++++++++++++++-------
 2 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Compiler.mli b/lib/Frenetic_NetKAT_Compiler.mli
index 1b7f9bfc6..03e945b3a 100644
--- a/lib/Frenetic_NetKAT_Compiler.mli
+++ b/lib/Frenetic_NetKAT_Compiler.mli
@@ -10,7 +10,13 @@ type order
     | `Static of Field.t list
     | `Heuristic ]
 
-module FDD : module type of Frenetic_Fdd.FDD
+module FDD : sig
+  include module type of Frenetic_Fdd.FDD
+  val union : t -> t -> t
+  val seq : t -> t -> t
+  val star : t -> t
+end
+
 type t = FDD.t
 (** The type of the intermediate compiler representation (FDD). *)
 
diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 9518a4692..4aaf067e0 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -102,11 +102,20 @@ module Make_Naive(Upto : UPTO) = struct
 
 
   let equiv ?(pk=SymPkt.all) (a1 : Automaton.t) (a2 : Automaton.t) =
+
+    let rec eq_state_ids pk (s1 : int) (s2 : int) =
+      eq_states pk (Hashtbl.find_exn a1.states s1) (Hashtbl.find_exn a2.states s2)
+
+    and eq_state_id_sets pk (s1s : Int.Set.t) (s2s : Int.Set.t) =
+      let merge (a : Automaton.t) states =
+        Int.Set.fold states ~init:(FDD.drop, FDD.drop) ~f:(fun (e,d) s ->
+          let (e',d') = Hashtbl.find_exn a.states s in
+          FDD.(union e e', union d d'))
+      in
+      eq_states pk (merge a1 s1s) (merge a2 s2s)
     
-    let rec eq_states pk (s1 : int) (s2 : int) =
+    and eq_states pk ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
       let mask = SymPkt.to_alist pk in
-      let (e1, d1) = Hashtbl.find_exn a1.states s1 in
-      let (e2, d2) = Hashtbl.find_exn a1.states s2 in
       let ((e1, d1) as s1) = FDD.(restrict mask e1, restrict mask d1) in
       let ((e2, d2) as s2) = FDD.(restrict mask e2, restrict mask d2) in
       Upto.equiv s1 s2 || begin
@@ -117,9 +126,15 @@ module Make_Naive(Upto : UPTO) = struct
     and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
       SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2))
 
-    and eq_ds pk = eq_fdd pk ~leaf_eq: begin fun pk par1 par2 ->
-      failwith "todo"
-    end
+    and eq_ds pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
+      eq_trans_tree pk (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
+
+    and eq_trans_tree pk tree =
+      match Trans_Tree.unget tree with
+      | Leaf (ksl, ksr) ->
+        eq_state_id_sets pk ksl ksr
+      | Branch ((f,n), tru, fls) ->
+        eq_trans_tree (SymPkt.add pk f n) tru && eq_trans_tree pk fls
 
     and eq_fdd ~leaf_eq pk x y =
       let check_with pk f n x y =
@@ -147,6 +162,6 @@ module Make_Naive(Upto : UPTO) = struct
         end
 
     in
-    eq_states pk a1.source a2.source
+    eq_state_ids pk a1.source a2.source
 
 end

From 3feba03df8080263f518a525e3017b0148e1b692 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 15:29:22 -0400
Subject: [PATCH 12/29] documentation

---
 lib/Frenetic_NetKAT_Equivalence.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 4aaf067e0..0447615f3 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -100,7 +100,7 @@ module Make_Naive(Upto : UPTO) = struct
   end
 
 
-
+  (** decides equivalence of symbolic NetKAT NFAs *)
   let equiv ?(pk=SymPkt.all) (a1 : Automaton.t) (a2 : Automaton.t) =
 
     let rec eq_state_ids pk (s1 : int) (s2 : int) =

From c7318ae2898c178ba41cfd9b65526198c1ba7cf2 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 15:32:03 -0400
Subject: [PATCH 13/29] instantiate decision procedure

---
 lib/Frenetic_NetKAT_Equivalence.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 0447615f3..a05c5b4af 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -165,3 +165,11 @@ module Make_Naive(Upto : UPTO) = struct
     eq_state_ids pk a1.source a2.source
 
 end
+
+
+(*===========================================================================*)
+(* Instantiations                                                            *)
+(*===========================================================================*)
+
+module Hopcroft = Make_Naive(Upto_Trans ())
+module Simple = Make_Naive(Upto_Sym ())

From 0ed3d1b2ec4ff0112c09f865fd5274e98d0193da Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 15:50:38 -0400
Subject: [PATCH 14/29] dumo command for decision procedure

---
 frenetic/Dump.ml                 | 42 +++++++++++++++++++++++++++++---
 lib/Frenetic_NetKAT_Compiler.ml  |  4 +--
 lib/Frenetic_NetKAT_Compiler.mli |  2 +-
 3 files changed, 42 insertions(+), 6 deletions(-)

diff --git a/frenetic/Dump.ml b/frenetic/Dump.ml
index 6e1ded224..e483e517f 100644
--- a/frenetic/Dump.ml
+++ b/frenetic/Dump.ml
@@ -148,7 +148,7 @@ end
 
 
 (*===========================================================================*)
-(* COMMANDS: Local, Global, Virtual, Auto                                    *)
+(* COMMANDS: Local, Global, Virtual, Auto, Decision                          *)
 (*===========================================================================*)
 
 module Local = struct
@@ -277,13 +277,41 @@ module Auto = struct
   let run file json printorder dedup cheap_minimize () =
     let pol = parse_pol ~json file in
     let (t, auto) = time (fun () ->
-      Frenetic_NetKAT_Compiler.Automaton.of_policy pol ~dedup ~cheap_minimize) in
+      Frenetic_NetKAT_Compiler.Automaton.of_pol pol ~dedup ~cheap_minimize) in
     if printorder then print_order ();
     dump_auto auto ~file:(file ^ ".auto.dot");
     print_time t;
 
 end
 
+module Decision = struct
+  let spec = Command.Spec.(
+    empty
+    +> anon ("file-1" %: file)
+    +> anon ("file-2" %: file)
+    +> Flag.dump_auto
+    +> Flag.json
+    +> Flag.print_order
+  )
+
+  let run file1 file2 dumpauto json printorder () =
+    let pol1 = parse_pol ~json file1 in
+    let pol2 = parse_pol ~json file2 in
+    let (a1, a2) = Frenetic_NetKAT_Compiler.Automaton.(of_pol pol1, of_pol pol2) in
+    if printorder then print_order ();
+    if dumpauto then dump_auto a1 ~file:(file1 ^ ".auto.dot");
+    if dumpauto then dump_auto a2 ~file:(file2 ^ ".auto.dot");
+    let module Hopcroft = Frenetic_NetKAT_Equivalence.Hopcroft in
+    let module Simple = Frenetic_NetKAT_Equivalence.Simple in
+    let (th, h) = time (fun () -> Hopcroft.equiv a1 a2) in
+    let(ts, s) = time (fun () -> Simple.equiv a1 a2) in
+    printf "equivalent (Hopcroft): %s" (Bool.to_string h);
+    print_time th;
+    printf "\nequivalent (Simple): %s" (Bool.to_string s);
+    print_time ts
+
+end
+
 
 
 (*===========================================================================*)
@@ -318,8 +346,16 @@ let auto : Command.t =
     Auto.spec
     Auto.run
 
+let decision : Command.t =
+  Command.basic
+    ~summary:"Decides program equivalence."
+    (* ~readme: *)
+    Decision.spec
+    Decision.run
+
 let main : Command.t =
   Command.group
     ~summary:"Runs (local/global/virtual) compiler and dumps resulting tables."
     (* ~readme: *)
-    [("local", local); ("global", global); ("virtual", virt); ("auto", auto)]
+    [("local", local); ("global", global); ("virtual", virt); ("auto", auto);
+     ("decision", decision)]
diff --git a/lib/Frenetic_NetKAT_Compiler.ml b/lib/Frenetic_NetKAT_Compiler.ml
index 366f12201..413558c2c 100644
--- a/lib/Frenetic_NetKAT_Compiler.ml
+++ b/lib/Frenetic_NetKAT_Compiler.ml
@@ -777,7 +777,7 @@ module Automaton = struct
     in
     Tbl.add_exn automaton.states ~key:id ~data:(Lazy.from_fun f)
 
-  let of_policy ?(dedup=true) ?ing ?(cheap_minimize=true) (pol : Frenetic_NetKAT.policy) : t =
+  let of_pol ?(dedup=true) ?ing ?(cheap_minimize=true) (pol : Frenetic_NetKAT.policy) : t =
     let automaton = create_t0 () in
     let pol = Pol.of_pol ing pol in
     let () = add_policy automaton (automaton.source, pol) in
@@ -897,7 +897,7 @@ end
 
 let compile_global ?(options=default_compiler_options) ?(pc=Field.Vlan) pol : FDD.t =
   prepare_compilation ~options pol;
-  Automaton.of_policy pol
+  Automaton.of_pol pol
   |> Automaton.to_local ~pc
 
 
diff --git a/lib/Frenetic_NetKAT_Compiler.mli b/lib/Frenetic_NetKAT_Compiler.mli
index 03e945b3a..14b81c65a 100644
--- a/lib/Frenetic_NetKAT_Compiler.mli
+++ b/lib/Frenetic_NetKAT_Compiler.mli
@@ -36,7 +36,7 @@ module Automaton : sig
     -> f:('a -> int -> (FDD.t * FDD.t) -> 'a)
     -> 'a
 
-  val of_policy: ?dedup:bool -> ?ing:pred -> ?cheap_minimize:bool -> policy -> t
+  val of_pol: ?dedup:bool -> ?ing:pred -> ?cheap_minimize:bool -> policy -> t
   val to_local: pc:Field.t -> t -> FDD.t
 
   val to_dot: t -> string

From 1fd0cbfa9d386e617186dab1f9580d352bdc0c66 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 16:03:26 -0400
Subject: [PATCH 15/29] examples

---
 examples/decision-procedure/README.md       | 17 +++++++++++++++++
 examples/decision-procedure/unrollable1.kat |  7 +++++++
 examples/decision-procedure/unrollable2.kat |  8 ++++++++
 3 files changed, 32 insertions(+)
 create mode 100644 examples/decision-procedure/README.md
 create mode 100644 examples/decision-procedure/unrollable1.kat
 create mode 100644 examples/decision-procedure/unrollable2.kat

diff --git a/examples/decision-procedure/README.md b/examples/decision-procedure/README.md
new file mode 100644
index 000000000..37b6e6b38
--- /dev/null
+++ b/examples/decision-procedure/README.md
@@ -0,0 +1,17 @@
+# Decision Procedure
+This directory contains pairs of NetKAT programs that can be checked for equivalence.
+
+## Requirements
+The frenetic executable must be installed:
+  * run `make && make reinstall` in the frenetic root directory
+
+## Run
+To decide program equivalence, run
+```bash
+frenetic dump decision <file1> <file2>
+```
+
+## Options
+Run `frenetic dump help decision` to see a list of all options. Currently, one flag is supported:
+  * --dump-auto: dump automata representations of the programs
+
diff --git a/examples/decision-procedure/unrollable1.kat b/examples/decision-procedure/unrollable1.kat
new file mode 100644
index 000000000..025a62ef4
--- /dev/null
+++ b/examples/decision-procedure/unrollable1.kat
@@ -0,0 +1,7 @@
+(* NetKAT automata have the strange property that they can sometimes be unrolled
+   into a loop-free automaton. This is an example for such an automaton.
+*)
+
+vlanId:=0;
+(dup; (filter vlanId=0; vlanId:=1 + filter vlanId=1; vlanId:=2))*;
+filter vlanId=1
diff --git a/examples/decision-procedure/unrollable2.kat b/examples/decision-procedure/unrollable2.kat
new file mode 100644
index 000000000..2961935a0
--- /dev/null
+++ b/examples/decision-procedure/unrollable2.kat
@@ -0,0 +1,8 @@
+(* NetKAT automata have the strange property that they can sometimes be unrolled
+   into a loop-free automaton.
+   This is the unrolled version of the "unrollable1.kat" automaton.
+*)
+
+vlanId:=0;
+dup; filter vlanId=0; vlanId:=1;
+filter vlanId=1

From 7c82dbce6a83c0bb27fb79e154e6868b9ab651ff Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 16:10:23 -0400
Subject: [PATCH 16/29] passed first sanity tests :)

---
 examples/decision-procedure/README.md |  2 +-
 examples/decision-procedure/drop.kat  |  1 +
 examples/decision-procedure/id.kat    |  1 +
 frenetic/Dump.ml                      | 16 ++++++++--------
 4 files changed, 11 insertions(+), 9 deletions(-)
 create mode 100644 examples/decision-procedure/drop.kat
 create mode 100644 examples/decision-procedure/id.kat

diff --git a/examples/decision-procedure/README.md b/examples/decision-procedure/README.md
index 37b6e6b38..02a07a8e1 100644
--- a/examples/decision-procedure/README.md
+++ b/examples/decision-procedure/README.md
@@ -1,5 +1,5 @@
 # Decision Procedure
-This directory contains pairs of NetKAT programs that can be checked for equivalence.
+This directory contains (pairs of) NetKAT programs that can be checked for equivalence.
 
 ## Requirements
 The frenetic executable must be installed:
diff --git a/examples/decision-procedure/drop.kat b/examples/decision-procedure/drop.kat
new file mode 100644
index 000000000..41a28c526
--- /dev/null
+++ b/examples/decision-procedure/drop.kat
@@ -0,0 +1 @@
+drop
diff --git a/examples/decision-procedure/id.kat b/examples/decision-procedure/id.kat
new file mode 100644
index 000000000..074d1eeb4
--- /dev/null
+++ b/examples/decision-procedure/id.kat
@@ -0,0 +1 @@
+id
diff --git a/frenetic/Dump.ml b/frenetic/Dump.ml
index e483e517f..7c457efb6 100644
--- a/frenetic/Dump.ml
+++ b/frenetic/Dump.ml
@@ -43,7 +43,7 @@ let time f =
   (t2 -. t1, r)
 
 let print_time ?(prefix="") time =
-  printf "%scompilation time: %.4f\n" prefix time
+  printf "%stime: %.4f\n" prefix time
 
 let print_order () =
   Frenetic_NetKAT_Compiler.Field.(get_order ()
@@ -178,7 +178,7 @@ module Local = struct
       if printfdd then print_fdd fdd;
       if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
       print_all_tables ~no_tables fdd switches;
-      print_time t;
+      print_time ~prefix:"compilation " t;
 end
 
 
@@ -204,7 +204,7 @@ module Global = struct
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
     print_all_tables ~no_tables fdd switches;
-    print_time t;
+    print_time ~prefix:"compilation " t;
 
 end
 
@@ -259,8 +259,8 @@ module Virtual = struct
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(vpol_file ^ ".dot");
     print_all_tables ~no_tables fdd switches;
-    print_time ~prefix:"virtual " t1;
-    print_time ~prefix:"global " t2;
+    print_time ~prefix:"virtual compilation " t1;
+    print_time ~prefix:"global compilation " t2;
 end
 
 
@@ -304,10 +304,10 @@ module Decision = struct
     let module Hopcroft = Frenetic_NetKAT_Equivalence.Hopcroft in
     let module Simple = Frenetic_NetKAT_Equivalence.Simple in
     let (th, h) = time (fun () -> Hopcroft.equiv a1 a2) in
-    let(ts, s) = time (fun () -> Simple.equiv a1 a2) in
-    printf "equivalent (Hopcroft): %s" (Bool.to_string h);
+    let (ts, s) = time (fun () -> Simple.equiv a1 a2) in
+    printf "equivalent (Hopcroft): %s\n" (Bool.to_string h);
     print_time th;
-    printf "\nequivalent (Simple): %s" (Bool.to_string s);
+    printf "\nequivalent (Simple): %s\n" (Bool.to_string s);
     print_time ts
 
 end

From 2831c1ce9c39710812b7a2487087fe6574cb2413 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 17:19:05 -0400
Subject: [PATCH 17/29] steal marks tests

---
 examples/decision-procedure/equalities.txt |  7 ++++++
 frenetic/frenetic.ml                       |  3 ++-
 lib/Frenetic_NetKAT_Equivalence.ml         |  4 ++++
 lib/Frenetic_NetKAT_Lexer.ml               |  4 ++++
 lib/Frenetic_NetKAT_Parser.ml              |  8 ++++++-
 lib/Frenetic_NetKAT_Parser.mli             |  5 ++++-
 lib/Parser.cppo.mly                        | 25 ++++++++++++++++++++++
 7 files changed, 53 insertions(+), 3 deletions(-)
 create mode 100644 examples/decision-procedure/equalities.txt

diff --git a/examples/decision-procedure/equalities.txt b/examples/decision-procedure/equalities.txt
new file mode 100644
index 000000000..4dff9e3e8
--- /dev/null
+++ b/examples/decision-procedure/equalities.txt
@@ -0,0 +1,7 @@
+(* RANDOM CRAP. *)
+(* ASSAGE. *)
+(port := 3; filter port = 3) == (port := 3);;
+(filter port = 3; filter switch = 4) == (filter switch = 4; filter port = 3);;
+(port := 3; switch := 4) == (switch := 4; port := 3);;
+(port := 1; filter switch = 2) == (filter switch = 2; port := 1);;
+(dup; filter port = 3) == (filter port = 3; dup)
diff --git a/frenetic/frenetic.ml b/frenetic/frenetic.ml
index 131040389..3653ce307 100644
--- a/frenetic/frenetic.ml
+++ b/frenetic/frenetic.ml
@@ -153,7 +153,8 @@ let main : Command.t =
     ; ("http-controller", http_controller)
     ; ("openflow13", openflow13_controller)
     ; ("fault-tolerant", openflow13_fault_tolerant_controller)
-    ; ("dump", Dump.main)]
+    ; ("dump", Dump.main)
+    ; ("decide", Decide.main)]
 
 let () =
   Frenetic_Util.pp_exceptions ();
diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index a05c5b4af..8a43492a5 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -13,6 +13,7 @@ type state = FDD.t * FDD.t
 module type UPTO = sig
   val add_equiv : state -> state -> unit
   val equiv : state -> state -> bool
+  val clear : unit -> unit
 end
 
 (* upto reflexivity & symmetry *)
@@ -21,6 +22,7 @@ module Upto_Sym () : UPTO = struct
   let cache = Hash_set.Poly.create ()
   let equiv s1 s2 = (s1 = s2) || Hash_set.mem cache (min s1 s2, max s1 s2)
   let add_equiv s1 s2 = Hash_set.add cache (min s1 s2, max s1 s2)
+  let clear () = Hash_set.clear cache
 end
 
 (* upto reflexivity & symmetry & transitivity (Hopcroft-Karp) *)
@@ -30,6 +32,7 @@ module Upto_Trans () : UPTO = struct
   let find = Hashtbl.find_or_add cache ~default:Union_find.create
   let equiv s1 s2 = (s1 = s2) || Union_find.same_class (find s1) (find s2)
   let add_equiv s1 s2 = Union_find.union (find s1) (find s2)
+  let clear () = Hashtbl.clear cache
 end
 
 
@@ -162,6 +165,7 @@ module Make_Naive(Upto : UPTO) = struct
         end
 
     in
+    Upto.clear ();
     eq_state_ids pk a1.source a2.source
 
 end
diff --git a/lib/Frenetic_NetKAT_Lexer.ml b/lib/Frenetic_NetKAT_Lexer.ml
index ff8463f23..d354b0df5 100644
--- a/lib/Frenetic_NetKAT_Lexer.ml
+++ b/lib/Frenetic_NetKAT_Lexer.ml
@@ -94,6 +94,10 @@ let token ~ppx ~loc_start buf =
       ANTIQ (ascii ~skip:1 buf, loc)
     else
       illegal buf '$'
+  (* equivalence *)
+  | "==" -> EQUIVALENT
+  | "<=" -> LEQ
+  | ";;" -> DOUBLESEMICOLON
   (* predicates *)
   | "true" -> TRUE
   | "false" -> FALSE
diff --git a/lib/Frenetic_NetKAT_Parser.ml b/lib/Frenetic_NetKAT_Parser.ml
index 2503f4ae2..b760f7df8 100644
--- a/lib/Frenetic_NetKAT_Parser.ml
+++ b/lib/Frenetic_NetKAT_Parser.ml
@@ -9,8 +9,14 @@ let pol_of_string ?pos (s : string) =
 let pred_of_string ?pos (s : string) =
   Lexer.parse_string ?pos s Parser.pred_eof
 
+let equalities_of_string ?pos (s : string) =
+  Lexer.parse_string ?pos s Parser.pol_eqs_eof
+
 let pol_of_file (file : string) =
   Lexer.parse_file ~file Parser.pol_eof
 
 let pred_of_file (file : string) =
-  Lexer.parse_file ~file Parser.pred_eof
\ No newline at end of file
+  Lexer.parse_file ~file Parser.pred_eof
+
+let equalities_of_file (file : string) =
+  Lexer.parse_file ~file Parser.pol_eqs_eof
diff --git a/lib/Frenetic_NetKAT_Parser.mli b/lib/Frenetic_NetKAT_Parser.mli
index 6736cfb53..9cd9f3943 100644
--- a/lib/Frenetic_NetKAT_Parser.mli
+++ b/lib/Frenetic_NetKAT_Parser.mli
@@ -2,6 +2,9 @@
 
 val pol_of_string : ?pos: Lexing.position -> string -> Frenetic_NetKAT.policy
 val pred_of_string : ?pos: Lexing.position -> string -> Frenetic_NetKAT.pred
+val equalities_of_string : ?pos: Lexing.position -> string 
+  -> (Frenetic_NetKAT.policy * Frenetic_NetKAT.policy) list
 
 val pol_of_file : string -> Frenetic_NetKAT.policy
-val pred_of_file : string -> Frenetic_NetKAT.pred
\ No newline at end of file
+val pred_of_file : string -> Frenetic_NetKAT.pred
+val equalities_of_file : string -> (Frenetic_NetKAT.policy * Frenetic_NetKAT.policy) list
diff --git a/lib/Parser.cppo.mly b/lib/Parser.cppo.mly
index 4b691b89b..e7c3b3d27 100644
--- a/lib/Parser.cppo.mly
+++ b/lib/Parser.cppo.mly
@@ -29,6 +29,9 @@ let int64 ?loc ?attrs x =
 #endif
 %}
 
+(* equivalence *)
+%token EQUIVALENT LEQ DOUBLESEMICOLON
+
 (* predicates and policies *)
 %token TRUE FALSE AND OR NOT EQUALS
 %token ID DROP FILTER ASSIGN SEMICOLON PLUS STAR LINK VLINK AT SLASH
@@ -69,7 +72,29 @@ let int64 ?loc ?attrs x =
 %start <POLTY> pol_eof
 %start <PREDTY> pred_eof
 
+(* don't support equations in syntax extension for now *)
+#ifndef MAKE_PPX
+%start <(POLTY*POLTY) list> pol_eqs_eof
+#endif
+
 %%
+
+(* don't support equations in syntax extension for now *)
+#ifndef MAKE_PPX
+pol_eqs_eof:
+  | eqs=separated_list(DOUBLESEMICOLON, pol_eq); EOF
+      { eqs }
+  ;
+
+pol_eq:
+  | p=pol; EQUIVALENT; q=pol
+      { (p, q) }
+  | p=pol; LEQ; q=pol
+      { (Union (p, q), q) }
+  ;
+#endif
+
+
 pol_eof:
   | p=pol; EOF
       AST( p )

From 72a618fc3a91ee475e632ba1ec025c1787c6be0b Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 17:29:41 -0400
Subject: [PATCH 18/29] batch decisions; found first bug

---
 examples/decision-procedure/equalities.txt | 74 ++++++++++++++++++++++
 frenetic/Decide.ml                         | 48 ++++++++++++++
 2 files changed, 122 insertions(+)
 create mode 100644 frenetic/Decide.ml

diff --git a/examples/decision-procedure/equalities.txt b/examples/decision-procedure/equalities.txt
index 4dff9e3e8..93bd777f6 100644
--- a/examples/decision-procedure/equalities.txt
+++ b/examples/decision-procedure/equalities.txt
@@ -5,3 +5,77 @@
 (port := 3; switch := 4) == (switch := 4; port := 3);;
 (port := 1; filter switch = 2) == (filter switch = 2; port := 1);;
 (dup; filter port = 3) == (filter port = 3; dup)
+
+(*
+(port = 3; port:= 3) == (port = 3);;
+(port := 3; port:=4 ) == (port := 4);;
+(port = 3; port = 4) == drop;;
+(port = 3 + port != 3) == id;;
+(port != 3) <= port != 4;;
+(port := 3; port :=4; port := 5) == port:=5;;
+(port := 3; port :=4; port := 2; port := 5) == port:=5;;
+(port := 3; port :=4; port := 2; port := 1; port := 5) == port:=5;;
+(port := 3; port :=4; port := 2; port := 1; port := 0; port := 5) == port:=5;;
+(port := 3; port :=4; port := 2; port := 1; port := 0; port := 6; port := 5) == port:=5;;
+(port := 3; port :=4; port := 2; port := 1; port := 0; port := 6; port := 7; port := 5) == port:=5
+(port := 3; switch :=4; port := 2; switch := 1; port := 0; switch := 6; port := 7; port := 5) == port:=5; switch := 6
+(switch := 1; port := 0; switch := 6; port := 5) == port:=5; switch := 6
+port := 0; switch := 6; port := 5 == port := 5; switch := 6
+z := 3; switch := 6; port := 5 <= z := 4; port := 5 switch := 6
+(port = 3 + z = 4) + drop == (port = 3 + z = 4)
+(port = 3 + z = 4) + (port = 3 + z = 4) == (port = 3 + z = 4)
+id; (port = 3 + z = 4) == (port = 3 + z = 4)
+(port = 3 + z = 4); id == (port = 3 + z = 4)
+(switch = 2);(port = 3 + z = 4) == (switch = 2);(port = 3) + (switch = 2);(z = 4)
+(port = 3 + z = 4);(switch = 2) == (port = 3);(switch = 2) + (z = 4);(switch = 2)
+port = 3 <= port = 4
+drop; (port = 3 + z = 4) == drop
+(port = 3 + z = 4); drop == drop
+id + (port = 3 + z = 4); (port = 3 + z = 4)* == (port = 3 + z = 4)*
+
+(*  this is a trolltastic test.  it's true because both sides are equivalent *)
+(*  to the sum of all tests. *)
+(z = 5) + ((port = 3 + z = 4); (port = 3 + z = 4)* ) <= z = 5 + (port = 3 + z = 4)*
+(* BOOLEAN ALGEBRA TIME! *)
+(port = 4) + not (port = 4) == id
+(port = 4); not (port = 4) == drop
+(* DUP-TACULAR! *)
+dup; port = 5 == port = 5; dup
+
+(* PACKET ALGEBRA *)
+port := 4; port = 4 == port:= 4
+port = 4; port := 4 == port = 4
+port = 3; port = 5 == drop
+
+(* from the other project *)
+( switch = 0; (switch := 1))* <= drop
+
+(port := 4; port:= 3; port = 3)* == id + port := 3
+
+(port := 4; port:= 3; port = 3) <= id + port := 3
+
+(port := 4; port:= 3; port = 3) ==  port := 3
+
+
+(* simple hops through the network *)
+
+sw = 0; sw := 1; dup; sw = 1; sw := 2; dup  ==  sw = 0; sw := 1; dup; sw := 2; dup
+
+sw = 0; sw := 1; dup; sw = 1 == sw = 0; sw := 1; dup
+
+(switch = 3 + z = 4;z := 4)*;(switch = 4 + z = 5)*== (switch = 3 + z = 4; z := 4)*;(switch = 4 + z = 5)*
+
+(a=3);(b=4);(c=2;c:=3 + c=3;c:=2)*;(d=1);(e=4);(f=0) <= a = 0
+
+id + (a=1;b:=2);(c=3;drop) + (c=3;drop) <= c=3;drop
+
+id <= drop
+
+port = 1; dup <= dup
+
+(* This eportploits non-canonicity of FDDs, naive implementation gets it wrong *)
+f:=1;g := 2 == f:=1;g:=2 + g=2;f := 1
+
+f=0;g:=0 + f=1;g:=1 + f!=1;g:=0 == f=1;g:=1 + f!=1;g:=0
+
+*)
diff --git a/frenetic/Decide.ml b/frenetic/Decide.ml
new file mode 100644
index 000000000..6419f5388
--- /dev/null
+++ b/frenetic/Decide.ml
@@ -0,0 +1,48 @@
+open Core.Std
+open Dump
+
+
+(*===========================================================================*)
+(* COMMANDS: Local, Global, Virtual, Auto, Decision                          *)
+(*===========================================================================*)
+
+
+module Main = struct
+  let spec = Command.Spec.(
+    empty
+    +> anon ("file" %: file)
+  )
+
+  let run file () =
+    let equalities = Frenetic_NetKAT_Parser.equalities_of_file file in
+    List.iter equalities ~f:(fun (p,q) ->
+      let (ta, (a1, a2)) = Dump.time (fun () -> 
+        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
+      let (th, rh) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
+      let (ts, rs) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
+      let open Frenetic_NetKAT_Pretty in
+      printf "===================================================\n";
+      printf "(%s)  ==  (%s)\n\n" (string_of_policy p) (string_of_policy q);
+      Dump.print_time ~prefix:"automaton construction " ta;
+      printf "\nHopcroft: %s\n" (Bool.to_string rh);
+      Dump.print_time th;
+      printf "\nSimple: %s\n" (Bool.to_string rs);
+      Dump.print_time ts)
+
+end
+
+
+
+(*===========================================================================*)
+(* BASIC SPECIFICATION OF COMMANDS                                           *)
+(*===========================================================================*)
+
+
+let main : Command.t =
+  Command.basic
+    ~summary:"Parses file of NetKAT (in-)equalities and decides them."
+    (* ~readme: *)
+    Main.spec
+    Main.run

From e171b1877d4298067d04d195ecb4cd4024a92b4e Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 7 Apr 2017 17:31:15 -0400
Subject: [PATCH 19/29] typo

---
 frenetic/Decide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/frenetic/Decide.ml b/frenetic/Decide.ml
index 6419f5388..8c89f981e 100644
--- a/frenetic/Decide.ml
+++ b/frenetic/Decide.ml
@@ -25,7 +25,7 @@ module Main = struct
       let open Frenetic_NetKAT_Pretty in
       printf "===================================================\n";
       printf "(%s)  ==  (%s)\n\n" (string_of_policy p) (string_of_policy q);
-      Dump.print_time ~prefix:"automaton construction " ta;
+      Dump.print_time ~prefix:"automata construction " ta;
       printf "\nHopcroft: %s\n" (Bool.to_string rh);
       Dump.print_time th;
       printf "\nSimple: %s\n" (Bool.to_string rs);

From 911368f88a579b0b112b6bb63599e3e16c84a7ef Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Sun, 9 Apr 2017 13:09:46 -0400
Subject: [PATCH 20/29] checkpoint

---
 frenetic/Decide.ml                 | 12 +++++-----
 lib/Frenetic_NetKAT_Equivalence.ml | 35 ++++++++++++++++++++----------
 2 files changed, 29 insertions(+), 18 deletions(-)

diff --git a/frenetic/Decide.ml b/frenetic/Decide.ml
index 8c89f981e..e7332f12f 100644
--- a/frenetic/Decide.ml
+++ b/frenetic/Decide.ml
@@ -16,18 +16,18 @@ module Main = struct
   let run file () =
     let equalities = Frenetic_NetKAT_Parser.equalities_of_file file in
     List.iter equalities ~f:(fun (p,q) ->
-      let (ta, (a1, a2)) = Dump.time (fun () -> 
-        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
-      let (th, rh) = Dump.time (fun () ->
-        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
-      let (ts, rs) = Dump.time (fun () ->
-        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
       let open Frenetic_NetKAT_Pretty in
       printf "===================================================\n";
       printf "(%s)  ==  (%s)\n\n" (string_of_policy p) (string_of_policy q);
+      let (ta, (a1, a2)) = Dump.time (fun () ->
+        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
       Dump.print_time ~prefix:"automata construction " ta;
+      let (th, rh) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
       printf "\nHopcroft: %s\n" (Bool.to_string rh);
       Dump.print_time th;
+      let (ts, rs) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
       printf "\nSimple: %s\n" (Bool.to_string rs);
       Dump.print_time ts)
 
diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 8a43492a5..94a09e198 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -16,23 +16,25 @@ module type UPTO = sig
   val clear : unit -> unit
 end
 
-(* upto reflexivity & symmetry *)
-module Upto_Sym () : UPTO = struct
+(* upto nothing; reflexivity and symmetry DO NOT hold *)
+module Upto_Nada () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
   let cache = Hash_set.Poly.create ()
-  let equiv s1 s2 = (s1 = s2) || Hash_set.mem cache (min s1 s2, max s1 s2)
-  let add_equiv s1 s2 = Hash_set.add cache (min s1 s2, max s1 s2)
+  let equiv s1 s2 = Hash_set.mem cache (s1, s2)
+  let add_equiv s1 s2 = Hash_set.add cache (s1, s2)
   let clear () = Hash_set.clear cache
 end
 
-(* upto reflexivity & symmetry & transitivity (Hopcroft-Karp) *)
+(* upto transitivity (Hopcroft-Karp) *)
 module Upto_Trans () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
-  let cache = Hashtbl.Poly.create ()
-  let find = Hashtbl.find_or_add cache ~default:Union_find.create
-  let equiv s1 s2 = (s1 = s2) || Union_find.same_class (find s1) (find s2)
-  let add_equiv s1 s2 = Union_find.union (find s1) (find s2)
-  let clear () = Hashtbl.clear cache
+  let cache_left = FDD.BinTbl.create ()
+  let cache_right = FDD.BinTbl.create ()
+  let find_left = FDD.BinTbl.find_or_add cache_left ~default:Union_find.create
+  let find_right = FDD.BinTbl.find_or_add cache_right ~default:Union_find.create
+  let equiv s1 s2 = Union_find.same_class (find_left s1) (find_right s2)
+  let add_equiv s1 s2 = Union_find.union (find_left s1) (find_right s2)
+  let clear () = FDD.BinTbl.clear cache_left; FDD.BinTbl.clear cache_right
 end
 
 
@@ -80,7 +82,7 @@ end
 (* Decision Procedure                                                        *)
 (*===========================================================================*)
 
-module Make_Naive(Upto : UPTO) = struct
+module Make_Naive (Upto : UPTO) = struct
 
   module SymPkt = struct
     module T = Map.Make(Frenetic_Fdd.Field)
@@ -100,6 +102,11 @@ module Make_Naive(Upto : UPTO) = struct
     let apply_par pk par : Set.t =
       Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
         Set.add pks (apply_seq pk seq))
+
+    let to_string pk =
+      sprintf "[%s]" (List.to_string (to_alist pk) ~f:(fun (f,v) ->
+        sprintf "%s=%s" (Frenetic_Fdd.Field.to_string f) (Frenetic_Fdd.Value.to_string v)
+      ))
   end
 
 
@@ -133,6 +140,10 @@ module Make_Naive(Upto : UPTO) = struct
       eq_trans_tree pk (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
 
     and eq_trans_tree pk tree =
+      printf "\n[eq_trans_tree] ----------------------------------\n";
+      printf "pk = %s\n" (SymPkt.to_string pk);
+      printf "%s" (Trans_Tree.to_string tree);
+      printf "\n";
       match Trans_Tree.unget tree with
       | Leaf (ksl, ksr) ->
         eq_state_id_sets pk ksl ksr
@@ -176,4 +187,4 @@ end
 (*===========================================================================*)
 
 module Hopcroft = Make_Naive(Upto_Trans ())
-module Simple = Make_Naive(Upto_Sym ())
+module Simple = Make_Naive(Upto_Nada ())

From 7b0281f7cf25a42cb349b876a45467f76ad2bc10 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Mon, 10 Apr 2017 18:00:48 -0400
Subject: [PATCH 21/29] checkpoints

---
 lib/Frenetic_NetKAT_Equivalence.ml | 182 +++++++++++++++++++----------
 1 file changed, 122 insertions(+), 60 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 94a09e198..300264cfa 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -3,7 +3,6 @@ open Core.Std
 module Automaton = Frenetic_NetKAT_Compiler.Automaton
 module FDD = Frenetic_NetKAT_Compiler.FDD
 
-
 (*===========================================================================*)
 (* UPTO                                                                      *)
 (*===========================================================================*)
@@ -76,108 +75,171 @@ module Trans_Tree = struct
   let of_right_par = of_par (fun i -> (Int.Set.empty, Int.Set.singleton i))
 end
 
+module Boolean_Tree = struct
+  include Frenetic_Vlr.Make(Frenetic_Fdd.Field)(Frenetic_Fdd.Value)(struct
+    include Bool
+    let zero = false
+    let one = true
+    let sum = (||)
+    let prod = (&&)
+  end)
+
+  let one = id
+  let zero = drop
+
+end
+
+
+(* IDEA: build product trees *)
+
+module Prod_FDD = struct
+  include Frenetic_Vlr.Make(Frenetic_Fdd.Field)(Frenetic_Fdd.Value)(struct
+    type t = Int.Set.t * Int.Set.t [@@deriving sexp, compare]
+    let hash = Hashtbl.hash
+    let to_string t = sexp_of_t t |> Sexp.to_string
+
+    let zero = (Int.Set.empty, Int.Set.empty)
+    let sum (l1, r1) (l2, r2) = (Set.union l1 l2, Set.union r1 r2)
 
+    (* SJS: no one or product *)
+    let one = zero
+    let prod _ _ = failwith "no product"
+  end)
+
+  let of_seq inj seq =
+    let leaf =
+      Frenetic_Fdd.Action.(Seq.find_exn seq K)
+      |> Frenetic_Fdd.Value.to_int_exn
+      |> inj
+      |> const
+    in
+    Frenetic_Fdd.Action.Seq.to_hvs seq
+    |> List.fold ~init:leaf ~f:(fun tree test -> cond test tree drop)
+
+  let of_par inj par =
+    Frenetic_Fdd.Action.Par.fold par
+      ~init:drop 
+      ~f:(fun acc seq -> sum acc (of_seq inj seq))
+
+  let of_left_par = of_par (fun i -> (Int.Set.singleton i, Int.Set.empty))
+  let of_right_par = of_par (fun i -> (Int.Set.empty, Int.Set.singleton i))
+end
 
 (*===========================================================================*)
 (* Decision Procedure                                                        *)
 (*===========================================================================*)
 
-module Make_Naive (Upto : UPTO) = struct
+module type GUARD = sig
+  type t
+  val one : t
+  val zero : t
+  val set : t -> Frenetic_Fdd.Field.t -> Frenetic_Fdd.Value.t -> t
+  val cases : t -> Frenetic_Fdd.Field.t -> Frenetic_Fdd.Value.t -> t
+  val restrict_fdd : t -> FDD.t -> FDD.t
 
-  module SymPkt = struct
-    module T = Map.Make(Frenetic_Fdd.Field)
-    include T
+  val apply_seq : t -> Frenetic_Fdd.Value.t Frenetic_Fdd.Action.Seq.t -> t
+  val apply_par : t -> Frenetic_Fdd.Action.Par.t -> t
+  val ( && ) : t -> t -> t
+  val ( || ) : t -> t -> t
+  
 
-    let all = empty
+end
 
-    module Set = Set.Make(struct
-      type t = Frenetic_Fdd.Value.t T.t [@@deriving sexp]
-      let compare = compare Frenetic_Fdd.Value.compare
-    end)
+module SymPkt = struct
+  module T = Map.Make(Frenetic_Fdd.Field)
+  include T
 
-    let apply_seq pk seq =
-      Frenetic_Fdd.Action.Seq.to_hvs seq
-      |> List.fold ~init:pk ~f:(fun pk (key,data) -> add pk ~key ~data)
+  let all = empty
 
-    let apply_par pk par : Set.t =
-      Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
-        Set.add pks (apply_seq pk seq))
+  module Set = Set.Make(struct
+    type t = Frenetic_Fdd.Value.t T.t [@@deriving sexp]
+    let compare = compare Frenetic_Fdd.Value.compare
+  end)
 
-    let to_string pk =
-      sprintf "[%s]" (List.to_string (to_alist pk) ~f:(fun (f,v) ->
-        sprintf "%s=%s" (Frenetic_Fdd.Field.to_string f) (Frenetic_Fdd.Value.to_string v)
-      ))
-  end
+  let apply_seq pk seq =
+    Frenetic_Fdd.Action.Seq.to_hvs seq
+    |> List.fold ~init:pk ~f:(fun pk (key,data) -> add pk ~key ~data)
 
+  let apply_par pk par : Set.t =
+    Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
+      Set.add pks (apply_seq pk seq))
+
+  let to_string pk =
+    sprintf "[%s]" (List.to_string (to_alist pk) ~f:(fun (f,v) ->
+      sprintf "%s=%s" (Frenetic_Fdd.Field.to_string f) (Frenetic_Fdd.Value.to_string v)
+    ))
+end
+
+module Make_Naive (Upto : UPTO) (Guard : SYMPKT) = struct
 
   (** decides equivalence of symbolic NetKAT NFAs *)
-  let equiv ?(pk=SymPkt.all) (a1 : Automaton.t) (a2 : Automaton.t) =
+  let equiv ?(guard=Guard.one) (a1 : Automaton.t) (a2 : Automaton.t) =
 
-    let rec eq_state_ids pk (s1 : int) (s2 : int) =
-      eq_states pk (Hashtbl.find_exn a1.states s1) (Hashtbl.find_exn a2.states s2)
+    let rec eq_state_ids guard (s1 : int) (s2 : int) =
+      eq_states guard (Hashtbl.find_exn a1.states s1) (Hashtbl.find_exn a2.states s2)
 
-    and eq_state_id_sets pk (s1s : Int.Set.t) (s2s : Int.Set.t) =
+    and eq_state_id_sets guard (s1s : Int.Set.t) (s2s : Int.Set.t) =
       let merge (a : Automaton.t) states =
         Int.Set.fold states ~init:(FDD.drop, FDD.drop) ~f:(fun (e,d) s ->
           let (e',d') = Hashtbl.find_exn a.states s in
           FDD.(union e e', union d d'))
       in
-      eq_states pk (merge a1 s1s) (merge a2 s2s)
+      eq_states guard (merge a1 s1s) (merge a2 s2s)
     
-    and eq_states pk ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
-      let mask = SymPkt.to_alist pk in
-      let ((e1, d1) as s1) = FDD.(restrict mask e1, restrict mask d1) in
-      let ((e2, d2) as s2) = FDD.(restrict mask e2, restrict mask d2) in
+    and eq_states guard ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
+      let ((e1, d1) as s1) = Guard.(restrict_fdd guard e1, restrict_fdd guard d1) in
+      let ((e2, d2) as s2) = Guard.(restrict_fdd guard e2, restrict_fdd guard d2) in
       Upto.equiv s1 s2 || begin
         Upto.add_equiv s1 s2;
-        eq_es pk e1 e2 && eq_ds pk d1 d2
+        eq_es guard e1 e2 && eq_ds guard d1 d2
       end
 
-    and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
-      SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2))
+    and eq_es guard e1 e2 =
+      FDD.equal e1 e2 || eq_fdd guard ~leaf_eq:(fun guard par1 par2 ->
+        Guard.Set.equal (Guard.apply_par guard par1) (Guard.apply_par guard par2))
 
-    and eq_ds pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
-      eq_trans_tree pk (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
+    and eq_ds guard = eq_fdd guard ~leaf_eq:(fun guard par1 par2 ->
+      eq_trans_tree guard (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
 
-    and eq_trans_tree pk tree =
+    and eq_trans_tree guard tree =
       printf "\n[eq_trans_tree] ----------------------------------\n";
-      printf "pk = %s\n" (SymPkt.to_string pk);
+      printf "guard = %s\n" (Guard.to_string guard);
       printf "%s" (Trans_Tree.to_string tree);
       printf "\n";
       match Trans_Tree.unget tree with
       | Leaf (ksl, ksr) ->
-        eq_state_id_sets pk ksl ksr
+        eq_state_id_sets guard ksl ksr
       | Branch ((f,n), tru, fls) ->
-        eq_trans_tree (SymPkt.add pk f n) tru && eq_trans_tree pk fls
-
-    and eq_fdd ~leaf_eq pk x y =
-      let check_with pk f n x y =
-        match SymPkt.find pk f with
-        | None ->
-          eq_fdd ~leaf_eq (SymPkt.add pk ~key:f ~data:n) x y
-        | Some m -> 
-          m <> n || eq_fdd ~leaf_eq pk x y
-      in
+        eq_trans_tree (Guard.set guard f n) tru && eq_trans_tree guard fls
+
+    and eq_fdd ~leaf_eq guard x y =
       match FDD.(unget x, unget y) with
       | Leaf r1, Leaf r2 ->
-        leaf_eq pk r1 r2
+        leaf_eq guard r1 r2
       | Branch ((f,n), xt, xf), Leaf _ ->
-        check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
+        let (gtrue, gfalse) = Guard.cases guard f n in
+        eq_fdd ~leaf_eq gtrue xt y && eq_fdd ~leaf_eq gfalse xf y
       | Leaf _, Branch ((g,m), yt, yf) ->
-        check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
+        let (gtrue, gfalse) = Guard.cases guard g m in
+        eq_fdd ~leaf_eq gtrue x yt && eq_fdd ~leaf_eq gfalse x yf
       | Branch((f, n), xt, xf), Branch((g, m), yt, yf) ->
         begin match Frenetic_Fdd.(Field.compare f g, Value.compare m n) with
-        |  0,  0 -> check_with pk f n xt yt && eq_fdd ~leaf_eq pk xf yf 
-        | -1,  _
-        |  0, -1 -> check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
-        |  1,  _
-        |  0,  1 -> check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
-        |  _     -> assert false
+        |  0,  0 ->
+          let (gtrue, gfalse) = Guard.cases guard f n in
+          eq_fdd ~leaf_eq gtrue xt yt && eq_fdd ~leaf_eq gfalse xf yf
+        | -1,  _ |  0, -1 ->
+          let (gtrue, gfalse) = Guard.cases guard f n in
+          eq_fdd ~leaf_eq gtrue xt y && eq_fdd ~leaf_eq gfalse xf y
+        |  1,  _ |  0,  1 ->
+          let (gtrue, gfalse) = Guard.cases guard g m in
+          eq_fdd ~leaf_eq gtrue x yt && eq_fdd ~leaf_eq gfalse x yf
+        |  _     -> 
+          assert false
         end
 
     in
     Upto.clear ();
-    eq_state_ids pk a1.source a2.source
+    eq_state_ids guard a1.source a2.source
 
 end
 
@@ -186,5 +248,5 @@ end
 (* Instantiations                                                            *)
 (*===========================================================================*)
 
-module Hopcroft = Make_Naive(Upto_Trans ())
-module Simple = Make_Naive(Upto_Nada ())
+module Hopcroft = Make_Naive(Upto_Trans ())(Guard)
+module Simple = Make_Naive(Upto_Nada ())(Guard)

From 42d94cc98234e571323d4ea8408aed7ed604e1e9 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 13 Apr 2017 15:14:15 -0400
Subject: [PATCH 22/29] Revert "checkpoints"

This reverts commit 7b0281f7cf25a42cb349b876a45467f76ad2bc10.
---
 lib/Frenetic_NetKAT_Equivalence.ml | 182 ++++++++++-------------------
 1 file changed, 60 insertions(+), 122 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 300264cfa..94a09e198 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -3,6 +3,7 @@ open Core.Std
 module Automaton = Frenetic_NetKAT_Compiler.Automaton
 module FDD = Frenetic_NetKAT_Compiler.FDD
 
+
 (*===========================================================================*)
 (* UPTO                                                                      *)
 (*===========================================================================*)
@@ -75,171 +76,108 @@ module Trans_Tree = struct
   let of_right_par = of_par (fun i -> (Int.Set.empty, Int.Set.singleton i))
 end
 
-module Boolean_Tree = struct
-  include Frenetic_Vlr.Make(Frenetic_Fdd.Field)(Frenetic_Fdd.Value)(struct
-    include Bool
-    let zero = false
-    let one = true
-    let sum = (||)
-    let prod = (&&)
-  end)
-
-  let one = id
-  let zero = drop
-
-end
-
-
-(* IDEA: build product trees *)
-
-module Prod_FDD = struct
-  include Frenetic_Vlr.Make(Frenetic_Fdd.Field)(Frenetic_Fdd.Value)(struct
-    type t = Int.Set.t * Int.Set.t [@@deriving sexp, compare]
-    let hash = Hashtbl.hash
-    let to_string t = sexp_of_t t |> Sexp.to_string
-
-    let zero = (Int.Set.empty, Int.Set.empty)
-    let sum (l1, r1) (l2, r2) = (Set.union l1 l2, Set.union r1 r2)
 
-    (* SJS: no one or product *)
-    let one = zero
-    let prod _ _ = failwith "no product"
-  end)
-
-  let of_seq inj seq =
-    let leaf =
-      Frenetic_Fdd.Action.(Seq.find_exn seq K)
-      |> Frenetic_Fdd.Value.to_int_exn
-      |> inj
-      |> const
-    in
-    Frenetic_Fdd.Action.Seq.to_hvs seq
-    |> List.fold ~init:leaf ~f:(fun tree test -> cond test tree drop)
-
-  let of_par inj par =
-    Frenetic_Fdd.Action.Par.fold par
-      ~init:drop 
-      ~f:(fun acc seq -> sum acc (of_seq inj seq))
-
-  let of_left_par = of_par (fun i -> (Int.Set.singleton i, Int.Set.empty))
-  let of_right_par = of_par (fun i -> (Int.Set.empty, Int.Set.singleton i))
-end
 
 (*===========================================================================*)
 (* Decision Procedure                                                        *)
 (*===========================================================================*)
 
-module type GUARD = sig
-  type t
-  val one : t
-  val zero : t
-  val set : t -> Frenetic_Fdd.Field.t -> Frenetic_Fdd.Value.t -> t
-  val cases : t -> Frenetic_Fdd.Field.t -> Frenetic_Fdd.Value.t -> t
-  val restrict_fdd : t -> FDD.t -> FDD.t
+module Make_Naive (Upto : UPTO) = struct
 
-  val apply_seq : t -> Frenetic_Fdd.Value.t Frenetic_Fdd.Action.Seq.t -> t
-  val apply_par : t -> Frenetic_Fdd.Action.Par.t -> t
-  val ( && ) : t -> t -> t
-  val ( || ) : t -> t -> t
-  
+  module SymPkt = struct
+    module T = Map.Make(Frenetic_Fdd.Field)
+    include T
 
-end
+    let all = empty
 
-module SymPkt = struct
-  module T = Map.Make(Frenetic_Fdd.Field)
-  include T
+    module Set = Set.Make(struct
+      type t = Frenetic_Fdd.Value.t T.t [@@deriving sexp]
+      let compare = compare Frenetic_Fdd.Value.compare
+    end)
 
-  let all = empty
+    let apply_seq pk seq =
+      Frenetic_Fdd.Action.Seq.to_hvs seq
+      |> List.fold ~init:pk ~f:(fun pk (key,data) -> add pk ~key ~data)
 
-  module Set = Set.Make(struct
-    type t = Frenetic_Fdd.Value.t T.t [@@deriving sexp]
-    let compare = compare Frenetic_Fdd.Value.compare
-  end)
+    let apply_par pk par : Set.t =
+      Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
+        Set.add pks (apply_seq pk seq))
 
-  let apply_seq pk seq =
-    Frenetic_Fdd.Action.Seq.to_hvs seq
-    |> List.fold ~init:pk ~f:(fun pk (key,data) -> add pk ~key ~data)
+    let to_string pk =
+      sprintf "[%s]" (List.to_string (to_alist pk) ~f:(fun (f,v) ->
+        sprintf "%s=%s" (Frenetic_Fdd.Field.to_string f) (Frenetic_Fdd.Value.to_string v)
+      ))
+  end
 
-  let apply_par pk par : Set.t =
-    Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
-      Set.add pks (apply_seq pk seq))
-
-  let to_string pk =
-    sprintf "[%s]" (List.to_string (to_alist pk) ~f:(fun (f,v) ->
-      sprintf "%s=%s" (Frenetic_Fdd.Field.to_string f) (Frenetic_Fdd.Value.to_string v)
-    ))
-end
-
-module Make_Naive (Upto : UPTO) (Guard : SYMPKT) = struct
 
   (** decides equivalence of symbolic NetKAT NFAs *)
-  let equiv ?(guard=Guard.one) (a1 : Automaton.t) (a2 : Automaton.t) =
+  let equiv ?(pk=SymPkt.all) (a1 : Automaton.t) (a2 : Automaton.t) =
 
-    let rec eq_state_ids guard (s1 : int) (s2 : int) =
-      eq_states guard (Hashtbl.find_exn a1.states s1) (Hashtbl.find_exn a2.states s2)
+    let rec eq_state_ids pk (s1 : int) (s2 : int) =
+      eq_states pk (Hashtbl.find_exn a1.states s1) (Hashtbl.find_exn a2.states s2)
 
-    and eq_state_id_sets guard (s1s : Int.Set.t) (s2s : Int.Set.t) =
+    and eq_state_id_sets pk (s1s : Int.Set.t) (s2s : Int.Set.t) =
       let merge (a : Automaton.t) states =
         Int.Set.fold states ~init:(FDD.drop, FDD.drop) ~f:(fun (e,d) s ->
           let (e',d') = Hashtbl.find_exn a.states s in
           FDD.(union e e', union d d'))
       in
-      eq_states guard (merge a1 s1s) (merge a2 s2s)
+      eq_states pk (merge a1 s1s) (merge a2 s2s)
     
-    and eq_states guard ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
-      let ((e1, d1) as s1) = Guard.(restrict_fdd guard e1, restrict_fdd guard d1) in
-      let ((e2, d2) as s2) = Guard.(restrict_fdd guard e2, restrict_fdd guard d2) in
+    and eq_states pk ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
+      let mask = SymPkt.to_alist pk in
+      let ((e1, d1) as s1) = FDD.(restrict mask e1, restrict mask d1) in
+      let ((e2, d2) as s2) = FDD.(restrict mask e2, restrict mask d2) in
       Upto.equiv s1 s2 || begin
         Upto.add_equiv s1 s2;
-        eq_es guard e1 e2 && eq_ds guard d1 d2
+        eq_es pk e1 e2 && eq_ds pk d1 d2
       end
 
-    and eq_es guard e1 e2 =
-      FDD.equal e1 e2 || eq_fdd guard ~leaf_eq:(fun guard par1 par2 ->
-        Guard.Set.equal (Guard.apply_par guard par1) (Guard.apply_par guard par2))
+    and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
+      SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2))
 
-    and eq_ds guard = eq_fdd guard ~leaf_eq:(fun guard par1 par2 ->
-      eq_trans_tree guard (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
+    and eq_ds pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
+      eq_trans_tree pk (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
 
-    and eq_trans_tree guard tree =
+    and eq_trans_tree pk tree =
       printf "\n[eq_trans_tree] ----------------------------------\n";
-      printf "guard = %s\n" (Guard.to_string guard);
+      printf "pk = %s\n" (SymPkt.to_string pk);
       printf "%s" (Trans_Tree.to_string tree);
       printf "\n";
       match Trans_Tree.unget tree with
       | Leaf (ksl, ksr) ->
-        eq_state_id_sets guard ksl ksr
+        eq_state_id_sets pk ksl ksr
       | Branch ((f,n), tru, fls) ->
-        eq_trans_tree (Guard.set guard f n) tru && eq_trans_tree guard fls
-
-    and eq_fdd ~leaf_eq guard x y =
+        eq_trans_tree (SymPkt.add pk f n) tru && eq_trans_tree pk fls
+
+    and eq_fdd ~leaf_eq pk x y =
+      let check_with pk f n x y =
+        match SymPkt.find pk f with
+        | None ->
+          eq_fdd ~leaf_eq (SymPkt.add pk ~key:f ~data:n) x y
+        | Some m -> 
+          m <> n || eq_fdd ~leaf_eq pk x y
+      in
       match FDD.(unget x, unget y) with
       | Leaf r1, Leaf r2 ->
-        leaf_eq guard r1 r2
+        leaf_eq pk r1 r2
       | Branch ((f,n), xt, xf), Leaf _ ->
-        let (gtrue, gfalse) = Guard.cases guard f n in
-        eq_fdd ~leaf_eq gtrue xt y && eq_fdd ~leaf_eq gfalse xf y
+        check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
       | Leaf _, Branch ((g,m), yt, yf) ->
-        let (gtrue, gfalse) = Guard.cases guard g m in
-        eq_fdd ~leaf_eq gtrue x yt && eq_fdd ~leaf_eq gfalse x yf
+        check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
       | Branch((f, n), xt, xf), Branch((g, m), yt, yf) ->
         begin match Frenetic_Fdd.(Field.compare f g, Value.compare m n) with
-        |  0,  0 ->
-          let (gtrue, gfalse) = Guard.cases guard f n in
-          eq_fdd ~leaf_eq gtrue xt yt && eq_fdd ~leaf_eq gfalse xf yf
-        | -1,  _ |  0, -1 ->
-          let (gtrue, gfalse) = Guard.cases guard f n in
-          eq_fdd ~leaf_eq gtrue xt y && eq_fdd ~leaf_eq gfalse xf y
-        |  1,  _ |  0,  1 ->
-          let (gtrue, gfalse) = Guard.cases guard g m in
-          eq_fdd ~leaf_eq gtrue x yt && eq_fdd ~leaf_eq gfalse x yf
-        |  _     -> 
-          assert false
+        |  0,  0 -> check_with pk f n xt yt && eq_fdd ~leaf_eq pk xf yf 
+        | -1,  _
+        |  0, -1 -> check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
+        |  1,  _
+        |  0,  1 -> check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
+        |  _     -> assert false
         end
 
     in
     Upto.clear ();
-    eq_state_ids guard a1.source a2.source
+    eq_state_ids pk a1.source a2.source
 
 end
 
@@ -248,5 +186,5 @@ end
 (* Instantiations                                                            *)
 (*===========================================================================*)
 
-module Hopcroft = Make_Naive(Upto_Trans ())(Guard)
-module Simple = Make_Naive(Upto_Nada ())(Guard)
+module Hopcroft = Make_Naive(Upto_Trans ())
+module Simple = Make_Naive(Upto_Nada ())

From 8b2d3e38e696a1407e618adec66b0928be6c1de2 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 13 Apr 2017 15:14:46 -0400
Subject: [PATCH 23/29] Revert "checkpoint"

This reverts commit 911368f88a579b0b112b6bb63599e3e16c84a7ef.
---
 frenetic/Decide.ml                 | 12 +++++-----
 lib/Frenetic_NetKAT_Equivalence.ml | 35 ++++++++++--------------------
 2 files changed, 18 insertions(+), 29 deletions(-)

diff --git a/frenetic/Decide.ml b/frenetic/Decide.ml
index e7332f12f..8c89f981e 100644
--- a/frenetic/Decide.ml
+++ b/frenetic/Decide.ml
@@ -16,18 +16,18 @@ module Main = struct
   let run file () =
     let equalities = Frenetic_NetKAT_Parser.equalities_of_file file in
     List.iter equalities ~f:(fun (p,q) ->
+      let (ta, (a1, a2)) = Dump.time (fun () -> 
+        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
+      let (th, rh) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
+      let (ts, rs) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
       let open Frenetic_NetKAT_Pretty in
       printf "===================================================\n";
       printf "(%s)  ==  (%s)\n\n" (string_of_policy p) (string_of_policy q);
-      let (ta, (a1, a2)) = Dump.time (fun () ->
-        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
       Dump.print_time ~prefix:"automata construction " ta;
-      let (th, rh) = Dump.time (fun () ->
-        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
       printf "\nHopcroft: %s\n" (Bool.to_string rh);
       Dump.print_time th;
-      let (ts, rs) = Dump.time (fun () ->
-        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
       printf "\nSimple: %s\n" (Bool.to_string rs);
       Dump.print_time ts)
 
diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 94a09e198..8a43492a5 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -16,25 +16,23 @@ module type UPTO = sig
   val clear : unit -> unit
 end
 
-(* upto nothing; reflexivity and symmetry DO NOT hold *)
-module Upto_Nada () : UPTO = struct
+(* upto reflexivity & symmetry *)
+module Upto_Sym () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
   let cache = Hash_set.Poly.create ()
-  let equiv s1 s2 = Hash_set.mem cache (s1, s2)
-  let add_equiv s1 s2 = Hash_set.add cache (s1, s2)
+  let equiv s1 s2 = (s1 = s2) || Hash_set.mem cache (min s1 s2, max s1 s2)
+  let add_equiv s1 s2 = Hash_set.add cache (min s1 s2, max s1 s2)
   let clear () = Hash_set.clear cache
 end
 
-(* upto transitivity (Hopcroft-Karp) *)
+(* upto reflexivity & symmetry & transitivity (Hopcroft-Karp) *)
 module Upto_Trans () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
-  let cache_left = FDD.BinTbl.create ()
-  let cache_right = FDD.BinTbl.create ()
-  let find_left = FDD.BinTbl.find_or_add cache_left ~default:Union_find.create
-  let find_right = FDD.BinTbl.find_or_add cache_right ~default:Union_find.create
-  let equiv s1 s2 = Union_find.same_class (find_left s1) (find_right s2)
-  let add_equiv s1 s2 = Union_find.union (find_left s1) (find_right s2)
-  let clear () = FDD.BinTbl.clear cache_left; FDD.BinTbl.clear cache_right
+  let cache = Hashtbl.Poly.create ()
+  let find = Hashtbl.find_or_add cache ~default:Union_find.create
+  let equiv s1 s2 = (s1 = s2) || Union_find.same_class (find s1) (find s2)
+  let add_equiv s1 s2 = Union_find.union (find s1) (find s2)
+  let clear () = Hashtbl.clear cache
 end
 
 
@@ -82,7 +80,7 @@ end
 (* Decision Procedure                                                        *)
 (*===========================================================================*)
 
-module Make_Naive (Upto : UPTO) = struct
+module Make_Naive(Upto : UPTO) = struct
 
   module SymPkt = struct
     module T = Map.Make(Frenetic_Fdd.Field)
@@ -102,11 +100,6 @@ module Make_Naive (Upto : UPTO) = struct
     let apply_par pk par : Set.t =
       Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
         Set.add pks (apply_seq pk seq))
-
-    let to_string pk =
-      sprintf "[%s]" (List.to_string (to_alist pk) ~f:(fun (f,v) ->
-        sprintf "%s=%s" (Frenetic_Fdd.Field.to_string f) (Frenetic_Fdd.Value.to_string v)
-      ))
   end
 
 
@@ -140,10 +133,6 @@ module Make_Naive (Upto : UPTO) = struct
       eq_trans_tree pk (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
 
     and eq_trans_tree pk tree =
-      printf "\n[eq_trans_tree] ----------------------------------\n";
-      printf "pk = %s\n" (SymPkt.to_string pk);
-      printf "%s" (Trans_Tree.to_string tree);
-      printf "\n";
       match Trans_Tree.unget tree with
       | Leaf (ksl, ksr) ->
         eq_state_id_sets pk ksl ksr
@@ -187,4 +176,4 @@ end
 (*===========================================================================*)
 
 module Hopcroft = Make_Naive(Upto_Trans ())
-module Simple = Make_Naive(Upto_Nada ())
+module Simple = Make_Naive(Upto_Sym ())

From 9b135d0220a060b8d09c94856790ba699a3271f9 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 13 Apr 2017 15:58:04 -0400
Subject: [PATCH 24/29] fix bug: need to take inequalities into account

---
 lib/Frenetic_NetKAT_Equivalence.ml | 78 +++++++++++++++++++++---------
 1 file changed, 56 insertions(+), 22 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 8a43492a5..c398da986 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -86,20 +86,56 @@ module Make_Naive(Upto : UPTO) = struct
     module T = Map.Make(Frenetic_Fdd.Field)
     include T
 
+    module Value = struct
+      include Frenetic_Fdd.Value
+      module Set = Set.Make(Frenetic_Fdd.Value)
+    end
+
     let all = empty
 
+    type constr =
+      | Eq of Value.t
+      | Neq of Value.Set.t
+      [@@deriving sexp, compare]
+
     module Set = Set.Make(struct
-      type t = Frenetic_Fdd.Value.t T.t [@@deriving sexp]
-      let compare = compare Frenetic_Fdd.Value.compare
+      type t = constr T.t [@@deriving sexp]
+      let compare = T.compare compare_constr
     end)
 
     let apply_seq pk seq =
-      Frenetic_Fdd.Action.Seq.to_hvs seq
-      |> List.fold ~init:pk ~f:(fun pk (key,data) -> add pk ~key ~data)
+      Frenetic_Fdd.Action.Seq.fold seq ~init:pk ~f:(fun ~key ~data pk ->
+        match key with
+        | K -> pk
+        | F f -> T.add pk ~key:f ~data:(Eq data))
 
     let apply_par pk par : Set.t =
       Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
         Set.add pks (apply_seq pk seq))
+
+    let rec restrict_fdd pk fdd =
+      match FDD.unget fdd with
+      | Leaf _ -> fdd
+      | Branch ((f,v), left, right) ->
+        begin match T.find pk f with
+        | Some (Eq v') when v = v'              -> restrict_fdd pk left
+        | Some (Eq v')                          -> restrict_fdd pk right
+        | Some (Neq vs) when Value.Set.mem vs v -> restrict_fdd pk right
+        | Some (Neq _) | None                   ->
+          FDD.unchecked_cond (f,v) (restrict_fdd pk left) (restrict_fdd pk right)
+        end
+
+    let set_eq pk f n =
+      T.add pk f (Eq n)
+
+    let branch pk f n =
+      match T.find pk f with
+      | Some (Eq m) when m = n                -> `Left pk
+      | Some (Eq m)                           -> `Right pk
+      | Some (Neq ms) when Value.Set.mem ms n -> `Right pk
+      | Some (Neq _) | None ->
+        `Both (T.add pk f (Eq n), T.add pk f (Neq (Value.Set.singleton n)))
+
   end
 
 
@@ -118,9 +154,8 @@ module Make_Naive(Upto : UPTO) = struct
       eq_states pk (merge a1 s1s) (merge a2 s2s)
     
     and eq_states pk ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
-      let mask = SymPkt.to_alist pk in
-      let ((e1, d1) as s1) = FDD.(restrict mask e1, restrict mask d1) in
-      let ((e2, d2) as s2) = FDD.(restrict mask e2, restrict mask d2) in
+      let ((e1, d1) as s1) = SymPkt.(restrict_fdd pk e1, restrict_fdd pk d1) in
+      let ((e2, d2) as s2) = SymPkt.(restrict_fdd pk e2, restrict_fdd pk d2) in
       Upto.equiv s1 s2 || begin
         Upto.add_equiv s1 s2;
         eq_es pk e1 e2 && eq_ds pk d1 d2
@@ -137,30 +172,29 @@ module Make_Naive(Upto : UPTO) = struct
       | Leaf (ksl, ksr) ->
         eq_state_id_sets pk ksl ksr
       | Branch ((f,n), tru, fls) ->
-        eq_trans_tree (SymPkt.add pk f n) tru && eq_trans_tree pk fls
+        eq_trans_tree (SymPkt.set_eq pk f n) tru && eq_trans_tree pk fls
 
     and eq_fdd ~leaf_eq pk x y =
-      let check_with pk f n x y =
-        match SymPkt.find pk f with
-        | None ->
-          eq_fdd ~leaf_eq (SymPkt.add pk ~key:f ~data:n) x y
-        | Some m -> 
-          m <> n || eq_fdd ~leaf_eq pk x y
+      let check_branches f n (lx, ly) (rx, ry) =
+        match SymPkt.branch pk f n with
+        | `Left pk -> eq_fdd ~leaf_eq pk lx ly
+        | `Right pk -> eq_fdd ~leaf_eq pk rx ry
+        | `Both (lpk, rpk) -> eq_fdd ~leaf_eq lpk lx ly && eq_fdd ~leaf_eq rpk rx ry
       in
       match FDD.(unget x, unget y) with
       | Leaf r1, Leaf r2 ->
         leaf_eq pk r1 r2
-      | Branch ((f,n), xt, xf), Leaf _ ->
-        check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
-      | Leaf _, Branch ((g,m), yt, yf) ->
-        check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
-      | Branch((f, n), xt, xf), Branch((g, m), yt, yf) ->
+      | Branch ((f,n), lx, rx), Leaf _ ->
+        check_branches f n (lx, y) (rx, y)
+      | Leaf _, Branch ((g,m), ly, ry) ->
+        check_branches g m (x, ly) (x, ly)
+      | Branch((f, n), lx, rx), Branch((g, m), ly, ry) ->
         begin match Frenetic_Fdd.(Field.compare f g, Value.compare m n) with
-        |  0,  0 -> check_with pk f n xt yt && eq_fdd ~leaf_eq pk xf yf 
+        |  0,  0 -> check_branches f n (lx, ly) (rx, ry)
         | -1,  _
-        |  0, -1 -> check_with pk f n xt y && eq_fdd ~leaf_eq pk xf y
+        |  0, -1 -> check_branches f n (lx, y) (rx, y)
         |  1,  _
-        |  0,  1 -> check_with pk g m x yt && eq_fdd ~leaf_eq pk x yf
+        |  0,  1 -> check_branches g m (x, ly) (x, ry)
         |  _     -> assert false
         end
 

From e33089f9c27d830371271790adaeb76cd92f7fae Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 13 Apr 2017 16:37:17 -0400
Subject: [PATCH 25/29] fix

---
 frenetic/Decide.ml                 | 12 ++---
 lib/Frenetic_NetKAT_Equivalence.ml | 72 ++++++++++++++++++++++--------
 2 files changed, 59 insertions(+), 25 deletions(-)

diff --git a/frenetic/Decide.ml b/frenetic/Decide.ml
index 8c89f981e..e7332f12f 100644
--- a/frenetic/Decide.ml
+++ b/frenetic/Decide.ml
@@ -16,18 +16,18 @@ module Main = struct
   let run file () =
     let equalities = Frenetic_NetKAT_Parser.equalities_of_file file in
     List.iter equalities ~f:(fun (p,q) ->
-      let (ta, (a1, a2)) = Dump.time (fun () -> 
-        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
-      let (th, rh) = Dump.time (fun () ->
-        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
-      let (ts, rs) = Dump.time (fun () ->
-        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
       let open Frenetic_NetKAT_Pretty in
       printf "===================================================\n";
       printf "(%s)  ==  (%s)\n\n" (string_of_policy p) (string_of_policy q);
+      let (ta, (a1, a2)) = Dump.time (fun () ->
+        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
       Dump.print_time ~prefix:"automata construction " ta;
+      let (th, rh) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
       printf "\nHopcroft: %s\n" (Bool.to_string rh);
       Dump.print_time th;
+      let (ts, rs) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
       printf "\nSimple: %s\n" (Bool.to_string rs);
       Dump.print_time ts)
 
diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index c398da986..601744203 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -16,23 +16,25 @@ module type UPTO = sig
   val clear : unit -> unit
 end
 
-(* upto reflexivity & symmetry *)
-module Upto_Sym () : UPTO = struct
+(* upto nothing; reflexivity and symmetry DO NOT hold *)
+module Upto_Nada () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
   let cache = Hash_set.Poly.create ()
-  let equiv s1 s2 = (s1 = s2) || Hash_set.mem cache (min s1 s2, max s1 s2)
-  let add_equiv s1 s2 = Hash_set.add cache (min s1 s2, max s1 s2)
+  let equiv s1 s2 = Hash_set.mem cache (s1, s2)
+  let add_equiv s1 s2 = Hash_set.add cache (s1, s2)
   let clear () = Hash_set.clear cache
 end
 
-(* upto reflexivity & symmetry & transitivity (Hopcroft-Karp) *)
+(* upto transitivity (Hopcroft-Karp) *)
 module Upto_Trans () : UPTO = struct
   (* FIXME: avoid polymorphic hash/max/min/equality *)
-  let cache = Hashtbl.Poly.create ()
-  let find = Hashtbl.find_or_add cache ~default:Union_find.create
-  let equiv s1 s2 = (s1 = s2) || Union_find.same_class (find s1) (find s2)
-  let add_equiv s1 s2 = Union_find.union (find s1) (find s2)
-  let clear () = Hashtbl.clear cache
+  let cache_left = FDD.BinTbl.create ()
+  let cache_right = FDD.BinTbl.create ()
+  let find_left = FDD.BinTbl.find_or_add cache_left ~default:Union_find.create
+  let find_right = FDD.BinTbl.find_or_add cache_right ~default:Union_find.create
+  let equiv s1 s2 = Union_find.same_class (find_left s1) (find_right s2)
+  let add_equiv s1 s2 = Union_find.union (find_left s1) (find_right s2)
+  let clear () = FDD.BinTbl.clear cache_left; FDD.BinTbl.clear cache_right
 end
 
 
@@ -80,10 +82,13 @@ end
 (* Decision Procedure                                                        *)
 (*===========================================================================*)
 
-module Make_Naive(Upto : UPTO) = struct
+module Make_Naive (Upto : UPTO) = struct
 
   module SymPkt = struct
-    module T = Map.Make(Frenetic_Fdd.Field)
+
+    module Field = Frenetic_Fdd.Field
+
+    module T = Map.Make(Field)
     include T
 
     module Value = struct
@@ -136,6 +141,16 @@ module Make_Naive(Upto : UPTO) = struct
       | Some (Neq _) | None ->
         `Both (T.add pk f (Eq n), T.add pk f (Neq (Value.Set.singleton n)))
 
+    let to_string pk =
+      List.to_string (to_alist pk) ~f:(function
+        | (f, Eq v) ->
+          sprintf "%s=%s" (Field.to_string f) (Value.to_string v)
+        | (f, Neq vs) ->
+          Value.Set.to_list vs
+          |> List.to_string ~f:Value.to_string
+          |> sprintf "%s!=%s" (Field.to_string f))
+      |>  sprintf "[%s]"
+
   end
 
 
@@ -146,20 +161,33 @@ module Make_Naive(Upto : UPTO) = struct
       eq_states pk (Hashtbl.find_exn a1.states s1) (Hashtbl.find_exn a2.states s2)
 
     and eq_state_id_sets pk (s1s : Int.Set.t) (s2s : Int.Set.t) =
+      let to_s set = List.to_string ~f:Int.to_string (Set.to_list set) in 
+      printf "\n[eq_state_id_sets] ----------------------------------\n";
+      printf "pk = %s\n" (SymPkt.to_string pk);
+      printf "%s = %s?\n" (to_s s1s) (to_s s2s);
       let merge (a : Automaton.t) states =
         Int.Set.fold states ~init:(FDD.drop, FDD.drop) ~f:(fun (e,d) s ->
           let (e',d') = Hashtbl.find_exn a.states s in
           FDD.(union e e', union d d'))
       in
-      eq_states pk (merge a1 s1s) (merge a2 s2s)
+      let eq = eq_states pk (merge a1 s1s) (merge a2 s2s) in
+      printf "-> %s\n" (Bool.to_string eq); eq
     
     and eq_states pk ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
+      printf "\n[eq_states ----------------------------------\n";
+      printf "pk = %s\n" (SymPkt.to_string pk);
+      printf "%s = %s\nand\n%s = %s\n?\n" (FDD.to_string e1) (FDD.to_string e2)
+        (FDD.to_string d1) (FDD.to_string d2);
       let ((e1, d1) as s1) = SymPkt.(restrict_fdd pk e1, restrict_fdd pk d1) in
       let ((e2, d2) as s2) = SymPkt.(restrict_fdd pk e2, restrict_fdd pk d2) in
-      Upto.equiv s1 s2 || begin
+      printf "suffices:\n%s = %s\nand\n%s = %s\n?\n"
+        (FDD.to_string e1) (FDD.to_string e2)
+        (FDD.to_string d1) (FDD.to_string d2);
+      let eq = Upto.equiv s1 s2 || begin
         Upto.add_equiv s1 s2;
         eq_es pk e1 e2 && eq_ds pk d1 d2
-      end
+      end in
+      printf "-> %s\n" (Bool.to_string eq); eq
 
     and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
       SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2))
@@ -168,11 +196,17 @@ module Make_Naive(Upto : UPTO) = struct
       eq_trans_tree pk (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
 
     and eq_trans_tree pk tree =
+      printf "\n[eq_trans_tree] ----------------------------------\n";
+      printf "pk = %s\n" (SymPkt.to_string pk);
+      printf "%s" (Trans_Tree.to_string tree);
+      printf "\n";
       match Trans_Tree.unget tree with
       | Leaf (ksl, ksr) ->
-        eq_state_id_sets pk ksl ksr
+        let eq = eq_state_id_sets pk ksl ksr in
+        printf "-> %s\n" (Bool.to_string eq); eq
       | Branch ((f,n), tru, fls) ->
-        eq_trans_tree (SymPkt.set_eq pk f n) tru && eq_trans_tree pk fls
+        let eq = eq_trans_tree (SymPkt.set_eq pk f n) tru && eq_trans_tree pk fls in
+        printf "-> %s\n" (Bool.to_string eq); eq
 
     and eq_fdd ~leaf_eq pk x y =
       let check_branches f n (lx, ly) (rx, ry) =
@@ -187,7 +221,7 @@ module Make_Naive(Upto : UPTO) = struct
       | Branch ((f,n), lx, rx), Leaf _ ->
         check_branches f n (lx, y) (rx, y)
       | Leaf _, Branch ((g,m), ly, ry) ->
-        check_branches g m (x, ly) (x, ly)
+        check_branches g m (x, ly) (x, ry)
       | Branch((f, n), lx, rx), Branch((g, m), ly, ry) ->
         begin match Frenetic_Fdd.(Field.compare f g, Value.compare m n) with
         |  0,  0 -> check_branches f n (lx, ly) (rx, ry)
@@ -210,4 +244,4 @@ end
 (*===========================================================================*)
 
 module Hopcroft = Make_Naive(Upto_Trans ())
-module Simple = Make_Naive(Upto_Sym ())
+module Simple = Make_Naive(Upto_Nada ())

From 9aa9d88c2a2473a18ee90f240942fd0e05f3b089 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 13 Apr 2017 16:42:08 -0400
Subject: [PATCH 26/29] checkpoint

---
 lib/Frenetic_NetKAT_Equivalence.ml | 34 +++++++++++++++---------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 601744203..78e152c87 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -162,32 +162,32 @@ module Make_Naive (Upto : UPTO) = struct
 
     and eq_state_id_sets pk (s1s : Int.Set.t) (s2s : Int.Set.t) =
       let to_s set = List.to_string ~f:Int.to_string (Set.to_list set) in 
-      printf "\n[eq_state_id_sets] ----------------------------------\n";
-      printf "pk = %s\n" (SymPkt.to_string pk);
-      printf "%s = %s?\n" (to_s s1s) (to_s s2s);
+      (* printf "\n[eq_state_id_sets] ----------------------------------\n"; *)
+      (* printf "pk = %s\n" (SymPkt.to_string pk); *)
+      (* printf "%s = %s?\n" (to_s s1s) (to_s s2s); *)
       let merge (a : Automaton.t) states =
         Int.Set.fold states ~init:(FDD.drop, FDD.drop) ~f:(fun (e,d) s ->
           let (e',d') = Hashtbl.find_exn a.states s in
           FDD.(union e e', union d d'))
       in
       let eq = eq_states pk (merge a1 s1s) (merge a2 s2s) in
-      printf "-> %s\n" (Bool.to_string eq); eq
+      (* printf "-> %s\n" (Bool.to_string eq); *) eq
     
     and eq_states pk ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
-      printf "\n[eq_states ----------------------------------\n";
-      printf "pk = %s\n" (SymPkt.to_string pk);
-      printf "%s = %s\nand\n%s = %s\n?\n" (FDD.to_string e1) (FDD.to_string e2)
-        (FDD.to_string d1) (FDD.to_string d2);
+      (* printf "\n[eq_states ----------------------------------\n"; *)
+      (* printf "pk = %s\n" (SymPkt.to_string pk); *)
+      (* printf "%s = %s\nand\n%s = %s\n?\n" (FDD.to_string e1) (FDD.to_string e2)
+        (FDD.to_string d1) (FDD.to_string d2); *)
       let ((e1, d1) as s1) = SymPkt.(restrict_fdd pk e1, restrict_fdd pk d1) in
       let ((e2, d2) as s2) = SymPkt.(restrict_fdd pk e2, restrict_fdd pk d2) in
-      printf "suffices:\n%s = %s\nand\n%s = %s\n?\n"
+      (* printf "suffices:\n%s = %s\nand\n%s = %s\n?\n"
         (FDD.to_string e1) (FDD.to_string e2)
-        (FDD.to_string d1) (FDD.to_string d2);
+        (FDD.to_string d1) (FDD.to_string d2); *)
       let eq = Upto.equiv s1 s2 || begin
         Upto.add_equiv s1 s2;
         eq_es pk e1 e2 && eq_ds pk d1 d2
       end in
-      printf "-> %s\n" (Bool.to_string eq); eq
+      (* printf "-> %s\n" (Bool.to_string eq); *) eq
 
     and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
       SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2))
@@ -196,17 +196,17 @@ module Make_Naive (Upto : UPTO) = struct
       eq_trans_tree pk (Trans_Tree.(sum (of_left_par par1) (of_right_par par2))))
 
     and eq_trans_tree pk tree =
-      printf "\n[eq_trans_tree] ----------------------------------\n";
-      printf "pk = %s\n" (SymPkt.to_string pk);
-      printf "%s" (Trans_Tree.to_string tree);
-      printf "\n";
+      (* printf "\n[eq_trans_tree] ----------------------------------\n"; *)
+      (* printf "pk = %s\n" (SymPkt.to_string pk); *)
+      (* printf "%s" (Trans_Tree.to_string tree); *)
+      (* printf "\n"; *)
       match Trans_Tree.unget tree with
       | Leaf (ksl, ksr) ->
         let eq = eq_state_id_sets pk ksl ksr in
-        printf "-> %s\n" (Bool.to_string eq); eq
+        (* printf "-> %s\n" (Bool.to_string eq); *) eq
       | Branch ((f,n), tru, fls) ->
         let eq = eq_trans_tree (SymPkt.set_eq pk f n) tru && eq_trans_tree pk fls in
-        printf "-> %s\n" (Bool.to_string eq); eq
+        (* printf "-> %s\n" (Bool.to_string eq); *) eq
 
     and eq_fdd ~leaf_eq pk x y =
       let check_branches f n (lx, ly) (rx, ry) =

From 28ed49754bdb7d5facffbf6ad46ae91eba193221 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 13 Apr 2017 17:25:03 -0400
Subject: [PATCH 27/29] more tests

---
 examples/decision-procedure/equalities.txt | 111 +++++++++++----------
 lib/Frenetic_NetKAT_Lexer.ml               |   1 +
 lib/Parser.cppo.mly                        |   5 +-
 3 files changed, 63 insertions(+), 54 deletions(-)

diff --git a/examples/decision-procedure/equalities.txt b/examples/decision-procedure/equalities.txt
index 93bd777f6..8c381c5fb 100644
--- a/examples/decision-procedure/equalities.txt
+++ b/examples/decision-procedure/equalities.txt
@@ -1,81 +1,86 @@
 (* RANDOM CRAP. *)
 (* ASSAGE. *)
-(port := 3; filter port = 3) == (port := 3);;
-(filter port = 3; filter switch = 4) == (filter switch = 4; filter port = 3);;
-(port := 3; switch := 4) == (switch := 4; port := 3);;
-(port := 1; filter switch = 2) == (filter switch = 2; port := 1);;
-(dup; filter port = 3) == (filter port = 3; dup)
-
-(*
-(port = 3; port:= 3) == (port = 3);;
-(port := 3; port:=4 ) == (port := 4);;
-(port = 3; port = 4) == drop;;
-(port = 3 + port != 3) == id;;
-(port != 3) <= port != 4;;
-(port := 3; port :=4; port := 5) == port:=5;;
-(port := 3; port :=4; port := 2; port := 5) == port:=5;;
-(port := 3; port :=4; port := 2; port := 1; port := 5) == port:=5;;
-(port := 3; port :=4; port := 2; port := 1; port := 0; port := 5) == port:=5;;
-(port := 3; port :=4; port := 2; port := 1; port := 0; port := 6; port := 5) == port:=5;;
-(port := 3; port :=4; port := 2; port := 1; port := 0; port := 6; port := 7; port := 5) == port:=5
-(port := 3; switch :=4; port := 2; switch := 1; port := 0; switch := 6; port := 7; port := 5) == port:=5; switch := 6
-(switch := 1; port := 0; switch := 6; port := 5) == port:=5; switch := 6
-port := 0; switch := 6; port := 5 == port := 5; switch := 6
-z := 3; switch := 6; port := 5 <= z := 4; port := 5 switch := 6
-(port = 3 + z = 4) + drop == (port = 3 + z = 4)
-(port = 3 + z = 4) + (port = 3 + z = 4) == (port = 3 + z = 4)
-id; (port = 3 + z = 4) == (port = 3 + z = 4)
-(port = 3 + z = 4); id == (port = 3 + z = 4)
-(switch = 2);(port = 3 + z = 4) == (switch = 2);(port = 3) + (switch = 2);(z = 4)
-(port = 3 + z = 4);(switch = 2) == (port = 3);(switch = 2) + (z = 4);(switch = 2)
-port = 3 <= port = 4
-drop; (port = 3 + z = 4) == drop
-(port = 3 + z = 4); drop == drop
-id + (port = 3 + z = 4); (port = 3 + z = 4)* == (port = 3 + z = 4)*
+(port:=3; filter port=3) == (port:=3);;
+(filter port=3; filter switch=4) == (filter switch=4; filter port=3);;
+(port:=3; switch:=4) == (switch:=4; port:=3);;
+(port:=1; filter switch=2) == (filter switch=2; port:=1);;
+(dup; filter port=3) == (filter port=3; dup);;
+(filter port=3; port:=3) == (filter port=3);;
+(port:=3; port:=4 ) == (port:=4);;
+(filter port=3; filter port=4) == drop;;
+(filter port=3 + filter port != 3) == id;;
+(* FALSE!! *) (* (filter port != 3) <= filter port != 4;; *)
+(port:=3; port :=4; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=0; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=0; port:=6; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=0; port:=6; port:=7; port:=5) == port:=5;;
+(port:=3; switch :=4; port:=2; switch:=1; port:=0; switch:=6; port:=7; port:=5) == port:=5; switch:=6;;
+(switch:=1; port:=0; switch:=6; port:=5) == port:=5; switch:=6;;
+port:=0; switch:=6; port:=5 == port:=5; switch:=6;;
+(* FALSE!! *) (* vlanId:=3; switch:=6; port:=5 <= vlanId:=4; port:=5; switch:=6;; *)
+(filter port=3 or vlanId=4) + drop == (filter port=3 or vlanId=4);;
+(filter port=3 or vlanId=4) + (filter port=3 or vlanId=4) == (filter port=3 or vlanId=4);;
+id; (filter port=3 or vlanId=4) == (filter port=3 or vlanId=4);;
+(filter port=3 or vlanId=4); id == (filter port=3 or vlanId=4);;
+(filter switch=2);(filter port=3 + filter vlanId=4) == (filter switch=2);(filter port=3) + (filter switch=2);(filter vlanId=4);;
+(filter port=3 + filter vlanId=4);(filter switch=2) == (filter port=3);(filter switch=2) + (filter vlanId=4);(filter switch=2);;
+(* FALSE!! *) (* filter port=3 <= filter port=4;; *)
+drop; (filter port=3 + filter vlanId=4) == drop;;
+(filter port=3 + filter vlanId=4); drop == drop;;
+id + (filter port=3 + filter vlanId=4); (filter port=3 + filter vlanId=4)* == (filter port=3 + filter vlanId=4)*;;
 
 (*  this is a trolltastic test.  it's true because both sides are equivalent *)
 (*  to the sum of all tests. *)
-(z = 5) + ((port = 3 + z = 4); (port = 3 + z = 4)* ) <= z = 5 + (port = 3 + z = 4)*
+(* (vlanId=5) + ((port=3 + vlanId=4); (port=3 + vlanId=4)* ) <= vlanId=5 + (port=3 + vlanId=4)* *)
+
+
 (* BOOLEAN ALGEBRA TIME! *)
-(port = 4) + not (port = 4) == id
-(port = 4); not (port = 4) == drop
+(filter port=4) + (filter port != 4) == id;;
+(filter port=4); (filter port != 4) == drop;;
+
 (* DUP-TACULAR! *)
-dup; port = 5 == port = 5; dup
+dup; filter port=5 == filter port=5; dup;;
 
 (* PACKET ALGEBRA *)
-port := 4; port = 4 == port:= 4
-port = 4; port := 4 == port = 4
-port = 3; port = 5 == drop
+port:=4; filter port=4 == port:=4;;
+filter port=4; port:=4 == filter port=4;;
+filter port=3; filter port=5 == drop;;
+
 
 (* from the other project *)
-( switch = 0; (switch := 1))* <= drop
+(filter switch=0; (switch:=1))* <= id + switch:=1;;
 
-(port := 4; port:= 3; port = 3)* == id + port := 3
+(port:=4; port:=3; filter port=3)* == id + port:=3;;
 
-(port := 4; port:= 3; port = 3) <= id + port := 3
+(port:=4; port:=3; filter port=3) <= id + port:=3;;
 
-(port := 4; port:= 3; port = 3) ==  port := 3
+(port:=4; port:=3; filter port=3) ==  port:=3;;
 
 
 (* simple hops through the network *)
 
-sw = 0; sw := 1; dup; sw = 1; sw := 2; dup  ==  sw = 0; sw := 1; dup; sw := 2; dup
+filter(switch=0); switch:=1; dup; filter(switch=1); switch:=2; dup  ==  filter(switch=0); switch:=1; dup; switch:=2; dup;;
 
-sw = 0; sw := 1; dup; sw = 1 == sw = 0; sw := 1; dup
+filter(switch=0); switch:=1; dup; filter(switch=1) == filter(switch=0); switch:=1; dup;;
 
-(switch = 3 + z = 4;z := 4)*;(switch = 4 + z = 5)*== (switch = 3 + z = 4; z := 4)*;(switch = 4 + z = 5)*
+(filter switch=3 + filter vlanId=4; vlanId:=4)*; (filter switch=4 + filter vlanId=5)* == (filter switch=3 + filter vlanId=4; vlanId:=4)*; (filter switch=4 + filter vlanId=5)*;;
 
-(a=3);(b=4);(c=2;c:=3 + c=3;c:=2)*;(d=1);(e=4);(f=0) <= a = 0
+(filter port=3); (filter switch=4); (filter vlanId=2; vlanId:=3 + filter vlanId=3; vlanId:=2)*; (filter vport=1);
+(filter vswitch=4) <= filter port=0;;
 
-id + (a=1;b:=2);(c=3;drop) + (c=3;drop) <= c=3;drop
+id + (filter port=1; switch:=2);(filter vlanId=3; drop) + (filter vlanId=3;drop) <= filter vlanId=3; drop;;
 
-id <= drop
+(* FALSE !! *) (* id <= drop;; *)
 
-port = 1; dup <= dup
+filter port=1; dup <= dup;;
 
 (* This eportploits non-canonicity of FDDs, naive implementation gets it wrong *)
-f:=1;g := 2 == f:=1;g:=2 + g=2;f := 1
+port:=1; switch:=2 == port:=1; switch:=2 + filter switch=2; port:=1;;
 
-f=0;g:=0 + f=1;g:=1 + f!=1;g:=0 == f=1;g:=1 + f!=1;g:=0
+filter port=0; switch:=0 + filter port=1; switch:=1 + filter port!=1; switch:=0
+  == filter port=1; switch:=1 + filter port!=1; switch:=0;;
 
-*)
+filter port=0; switch:=0 + filter port!=1; switch:=0
+  == filter port!=1; switch:=0
diff --git a/lib/Frenetic_NetKAT_Lexer.ml b/lib/Frenetic_NetKAT_Lexer.ml
index d354b0df5..82b49dd48 100644
--- a/lib/Frenetic_NetKAT_Lexer.ml
+++ b/lib/Frenetic_NetKAT_Lexer.ml
@@ -105,6 +105,7 @@ let token ~ppx ~loc_start buf =
   | "or" -> OR
   | "not" -> NOT
   | '=' -> EQUALS
+  | "!=" -> NEQUALS
   (* policies *)
   | "id" -> ID
   | "drop" -> DROP
diff --git a/lib/Parser.cppo.mly b/lib/Parser.cppo.mly
index e7c3b3d27..a4782ef2a 100644
--- a/lib/Parser.cppo.mly
+++ b/lib/Parser.cppo.mly
@@ -33,7 +33,7 @@ let int64 ?loc ?attrs x =
 %token EQUIVALENT LEQ DOUBLESEMICOLON
 
 (* predicates and policies *)
-%token TRUE FALSE AND OR NOT EQUALS
+%token TRUE FALSE AND OR NOT EQUALS NEQUALS
 %token ID DROP FILTER ASSIGN SEMICOLON PLUS STAR LINK VLINK AT SLASH
 %token IF THEN ELSE WHILE DO
 %token DUP
@@ -171,6 +171,9 @@ pred:
   | hv=header_val(EQUALS)
       AST( Test hv )
       PPX( Test [%e hv] )
+  | hv=header_val(NEQUALS)
+      AST( Neg (Test hv) )
+      PPX( Neg (Test [%e hv]) )
   | NOT; a=pred
       AST( Neg a )
       PPX( Neg [%e a] )

From 1d7d2950f74b10b7bbd24829cb81d1b91c81f051 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Thu, 13 Apr 2017 20:43:19 -0400
Subject: [PATCH 28/29] checkpoint

---
 lib/Frenetic_NetKAT_Equivalence.ml | 195 +++++++++++++++--------------
 1 file changed, 104 insertions(+), 91 deletions(-)

diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index 78e152c87..a7d4b8798 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -77,82 +77,87 @@ module Trans_Tree = struct
 end
 
 
-
 (*===========================================================================*)
-(* Decision Procedure                                                        *)
+(* Symbolic Packets                                                          *)
 (*===========================================================================*)
 
-module Make_Naive (Upto : UPTO) = struct
+module SymPkt = struct
 
-  module SymPkt = struct
-
-    module Field = Frenetic_Fdd.Field
-
-    module T = Map.Make(Field)
-    include T
-
-    module Value = struct
-      include Frenetic_Fdd.Value
-      module Set = Set.Make(Frenetic_Fdd.Value)
-    end
-
-    let all = empty
-
-    type constr =
-      | Eq of Value.t
-      | Neq of Value.Set.t
-      [@@deriving sexp, compare]
-
-    module Set = Set.Make(struct
-      type t = constr T.t [@@deriving sexp]
-      let compare = T.compare compare_constr
-    end)
-
-    let apply_seq pk seq =
-      Frenetic_Fdd.Action.Seq.fold seq ~init:pk ~f:(fun ~key ~data pk ->
-        match key with
-        | K -> pk
-        | F f -> T.add pk ~key:f ~data:(Eq data))
-
-    let apply_par pk par : Set.t =
-      Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
-        Set.add pks (apply_seq pk seq))
-
-    let rec restrict_fdd pk fdd =
-      match FDD.unget fdd with
-      | Leaf _ -> fdd
-      | Branch ((f,v), left, right) ->
-        begin match T.find pk f with
-        | Some (Eq v') when v = v'              -> restrict_fdd pk left
-        | Some (Eq v')                          -> restrict_fdd pk right
-        | Some (Neq vs) when Value.Set.mem vs v -> restrict_fdd pk right
-        | Some (Neq _) | None                   ->
-          FDD.unchecked_cond (f,v) (restrict_fdd pk left) (restrict_fdd pk right)
-        end
-
-    let set_eq pk f n =
-      T.add pk f (Eq n)
-
-    let branch pk f n =
-      match T.find pk f with
-      | Some (Eq m) when m = n                -> `Left pk
-      | Some (Eq m)                           -> `Right pk
-      | Some (Neq ms) when Value.Set.mem ms n -> `Right pk
-      | Some (Neq _) | None ->
-        `Both (T.add pk f (Eq n), T.add pk f (Neq (Value.Set.singleton n)))
-
-    let to_string pk =
-      List.to_string (to_alist pk) ~f:(function
-        | (f, Eq v) ->
-          sprintf "%s=%s" (Field.to_string f) (Value.to_string v)
-        | (f, Neq vs) ->
-          Value.Set.to_list vs
-          |> List.to_string ~f:Value.to_string
-          |> sprintf "%s!=%s" (Field.to_string f))
-      |>  sprintf "[%s]"
+  module Field = Frenetic_Fdd.Field
 
+  module Value = struct
+    include Frenetic_Fdd.Value
+    module Set = Set.Make(Frenetic_Fdd.Value)
   end
 
+  module T = Map.Make(Field)
+  include T
+
+  let all = empty
+
+  type constr =
+    | Eq of Value.t
+    | Neq of Value.Set.t
+    [@@deriving sexp, compare]
+
+  module Set = Set.Make(struct
+    type t = constr T.t [@@deriving sexp]
+    let compare = T.compare compare_constr
+  end)
+
+  let apply_seq pk seq =
+    Frenetic_Fdd.Action.Seq.fold seq ~init:pk ~f:(fun ~key ~data pk ->
+      match key with
+      | K -> pk
+      | F f -> T.add pk ~key:f ~data:(Eq data))
+
+  let apply_par pk par : Set.t =
+    Frenetic_Fdd.Action.Par.fold par ~init:Set.empty ~f:(fun pks seq ->
+      Set.add pks (apply_seq pk seq))
+
+  let rec restrict_fdd pk fdd =
+    match FDD.unget fdd with
+    | Leaf _ -> fdd
+    | Branch ((f,v), left, right) ->
+      begin match T.find pk f with
+      | Some (Eq v') when v = v'              -> restrict_fdd pk left
+      | Some (Eq v')                          -> restrict_fdd pk right
+      | Some (Neq vs) when Value.Set.mem vs v -> restrict_fdd pk right
+      | Some (Neq _) | None                   ->
+        FDD.unchecked_cond (f,v) (restrict_fdd pk left) (restrict_fdd pk right)
+      end
+
+  let set_eq pk f n =
+    T.add pk f (Eq n)
+
+  let branch pk f v =
+    match T.find pk f with
+    | Some (Eq v') when v' = v              -> `Left pk
+    | Some (Eq v')                          -> `Right pk
+    | Some (Neq vs) when Value.Set.mem vs v -> `Right pk
+    | Some (Neq vs) ->
+      `Both (T.add pk f (Eq v), T.add pk f (Neq Value.Set.(add vs v)))
+    | None ->
+      `Both (T.add pk f (Eq v), T.add pk f (Neq Value.Set.(singleton v)))
+
+  let to_string pk =
+    List.to_string (to_alist pk) ~f:(function
+      | (f, Eq v) ->
+        sprintf "%s=%s" (Field.to_string f) (Value.to_string v)
+      | (f, Neq vs) ->
+        Value.Set.to_list vs
+        |> List.to_string ~f:Value.to_string
+        |> sprintf "%s!=%s" (Field.to_string f))
+    |>  sprintf "[%s]"
+
+end
+
+
+(*===========================================================================*)
+(* Decision Procedure                                                        *)
+(*===========================================================================*)
+
+module Make_Naive (Upto : UPTO) = struct
 
   (** decides equivalence of symbolic NetKAT NFAs *)
   let equiv ?(pk=SymPkt.all) (a1 : Automaton.t) (a2 : Automaton.t) =
@@ -176,18 +181,19 @@ module Make_Naive (Upto : UPTO) = struct
     and eq_states pk ((e1, d1) : FDD.t * FDD.t) ((e2, d2) : FDD.t * FDD.t) =
       (* printf "\n[eq_states ----------------------------------\n"; *)
       (* printf "pk = %s\n" (SymPkt.to_string pk); *)
-      (* printf "%s = %s\nand\n%s = %s\n?\n" (FDD.to_string e1) (FDD.to_string e2)
-        (FDD.to_string d1) (FDD.to_string d2); *)
+      (* printf "%s = %s\nand\n%s = %s\n?\n" (FDD.to_string e1) (FDD.to_string e2) *)
+        (* (FDD.to_string d1) (FDD.to_string d2); *)
       let ((e1, d1) as s1) = SymPkt.(restrict_fdd pk e1, restrict_fdd pk d1) in
       let ((e2, d2) as s2) = SymPkt.(restrict_fdd pk e2, restrict_fdd pk d2) in
-      (* printf "suffices:\n%s = %s\nand\n%s = %s\n?\n"
-        (FDD.to_string e1) (FDD.to_string e2)
-        (FDD.to_string d1) (FDD.to_string d2); *)
+      (* printf "suffices:\n%s = %s\nand\n%s = %s\n?\n" *)
+        (* (FDD.to_string e1) (FDD.to_string e2) *)
+        (* (FDD.to_string d1) (FDD.to_string d2); *)
       let eq = Upto.equiv s1 s2 || begin
         Upto.add_equiv s1 s2;
         eq_es pk e1 e2 && eq_ds pk d1 d2
       end in
-      (* printf "-> %s\n" (Bool.to_string eq); *) eq
+      (* printf "-> %s\n" (Bool.to_string eq); *)
+      eq
 
     and eq_es pk = eq_fdd pk ~leaf_eq:(fun pk par1 par2 ->
       SymPkt.Set.equal (SymPkt.apply_par pk par1) (SymPkt.apply_par pk par2))
@@ -209,28 +215,35 @@ module Make_Naive (Upto : UPTO) = struct
         (* printf "-> %s\n" (Bool.to_string eq); *) eq
 
     and eq_fdd ~leaf_eq pk x y =
+      (* printf "\n[eq_fdd ----------------------------------\n"; *)
+      (* printf "pk = %s\n" (SymPkt.to_string pk); *)
+      (* printf "%s = %s\n?\n" (FDD.to_string x) (FDD.to_string y); *)
       let check_branches f n (lx, ly) (rx, ry) =
         match SymPkt.branch pk f n with
         | `Left pk -> eq_fdd ~leaf_eq pk lx ly
         | `Right pk -> eq_fdd ~leaf_eq pk rx ry
         | `Both (lpk, rpk) -> eq_fdd ~leaf_eq lpk lx ly && eq_fdd ~leaf_eq rpk rx ry
       in
-      match FDD.(unget x, unget y) with
-      | Leaf r1, Leaf r2 ->
-        leaf_eq pk r1 r2
-      | Branch ((f,n), lx, rx), Leaf _ ->
-        check_branches f n (lx, y) (rx, y)
-      | Leaf _, Branch ((g,m), ly, ry) ->
-        check_branches g m (x, ly) (x, ry)
-      | Branch((f, n), lx, rx), Branch((g, m), ly, ry) ->
-        begin match Frenetic_Fdd.(Field.compare f g, Value.compare m n) with
-        |  0,  0 -> check_branches f n (lx, ly) (rx, ry)
-        | -1,  _
-        |  0, -1 -> check_branches f n (lx, y) (rx, y)
-        |  1,  _
-        |  0,  1 -> check_branches g m (x, ly) (x, ry)
-        |  _     -> assert false
-        end
+      let eq =
+        match FDD.(unget x, unget y) with
+        | Leaf r1, Leaf r2 ->
+          leaf_eq pk r1 r2
+        | Branch ((f,n), lx, rx), Leaf _ ->
+          check_branches f n (lx, y) (rx, y)
+        | Leaf _, Branch ((g,m), ly, ry) ->
+          check_branches g m (x, ly) (x, ry)
+        | Branch((fx, vx), lx, rx), Branch((fy, vy), ly, ry) ->
+          begin match Frenetic_Fdd.(Field.compare fx fy, Value.compare vx vy) with
+          |  0,  0 -> check_branches fx vx (lx, ly) (rx, ry)
+          | -1,  _
+          |  0, -1 -> check_branches fx vx (lx, y) (rx, y)
+          |  1,  _
+          |  0,  1 -> check_branches fy vy (x, ly) (x, ry)
+          |  _     -> assert false
+          end
+        in
+          (* printf "-> %s\n" (Bool.to_string eq); *)
+          eq
 
     in
     Upto.clear ();

From 613ffc213bf332cf40462341b4e30fb746fb8017 Mon Sep 17 00:00:00 2001
From: Steffen Smolka <smolka@cs.cornell.edu>
Date: Fri, 4 Aug 2017 08:52:47 +0200
Subject: [PATCH 29/29] tweak

---
 frenetic/Decide.ml                 | 4 ++--
 lib/Frenetic_NetKAT_Equivalence.ml | 2 +-
 setup.ml                           | 7 ++++---
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/frenetic/Decide.ml b/frenetic/Decide.ml
index e7332f12f..219126799 100644
--- a/frenetic/Decide.ml
+++ b/frenetic/Decide.ml
@@ -1,9 +1,9 @@
-open Core.Std
+open Core
 open Dump
 
 
 (*===========================================================================*)
-(* COMMANDS: Local, Global, Virtual, Auto, Decision                          *)
+(* COMMANDS                                                                  *)
 (*===========================================================================*)
 
 
diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
index a7d4b8798..7061acf29 100644
--- a/lib/Frenetic_NetKAT_Equivalence.ml
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -1,4 +1,4 @@
-open Core.Std
+open Core
 
 module Automaton = Frenetic_NetKAT_Compiler.Automaton
 module FDD = Frenetic_NetKAT_Compiler.FDD
diff --git a/setup.ml b/setup.ml
index 35e470fd0..d82e7ebf9 100644
--- a/setup.ml
+++ b/setup.ml
@@ -1,7 +1,7 @@
 (* setup.ml generated for the first time by OASIS v0.4.7 *)
 
 (* OASIS_START *)
-(* DO NOT EDIT (digest: 569b2192cca3b4ed39029925f19db2ef) *)
+(* DO NOT EDIT (digest: cfcb4738846318c13ec4b33da20d596c) *)
 (*
    Regenerated by OASIS v0.4.10
    Visit http://oasis.forge.ocamlcore.org for more information and
@@ -7270,6 +7270,7 @@ let setup_t =
                            "Frenetic_NetKAT_Optimize";
                            "Frenetic_NetKAT_Json";
                            "Frenetic_NetKAT_Compiler";
+                           "Frenetic_NetKAT_Equivalence";
                            "Frenetic_NetKAT_FabricGen";
                            "Frenetic_NetKAT_Virtual_Compiler";
                            "Frenetic_NetKAT_Net";
@@ -8950,7 +8951,7 @@ let setup_t =
        };
      oasis_fn = Some "_oasis";
      oasis_version = "0.4.10";
-     oasis_digest = Some "\194\167&\012\015\002\140\215\203\216c\135\141C;M";
+     oasis_digest = Some "?\183z\134\217Gs\240\175\143\129\221?U\031O";
      oasis_exec = None;
      oasis_setup_args = [];
      setup_update = false
@@ -8958,7 +8959,7 @@ let setup_t =
 
 let setup () = BaseSetup.setup setup_t;;
 
-# 8962 "setup.ml"
+# 8963 "setup.ml"
 let setup_t = BaseCompat.Compat_0_4.adapt_setup_t setup_t
 open BaseCompat.Compat_0_4
 (* OASIS_STOP *)