diff --git a/_oasis b/_oasis
index 2852a4239..01c5dcd8e 100644
--- a/_oasis
+++ b/_oasis
@@ -80,6 +80,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/examples/decision-procedure/README.md b/examples/decision-procedure/README.md
new file mode 100644
index 000000000..02a07a8e1
--- /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/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/equalities.txt b/examples/decision-procedure/equalities.txt
new file mode 100644
index 000000000..8c381c5fb
--- /dev/null
+++ b/examples/decision-procedure/equalities.txt
@@ -0,0 +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);;
+(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. *)
+(* (vlanId=5) + ((port=3 + vlanId=4); (port=3 + vlanId=4)* ) <= vlanId=5 + (port=3 + vlanId=4)* *)
+
+
+(* BOOLEAN ALGEBRA TIME! *)
+(filter port=4) + (filter port != 4) == id;;
+(filter port=4); (filter port != 4) == drop;;
+
+(* DUP-TACULAR! *)
+dup; filter port=5 == filter port=5; dup;;
+
+(* PACKET ALGEBRA *)
+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 *)
+(filter switch=0; (switch:=1))* <= id + switch:=1;;
+
+(port:=4; port:=3; filter port=3)* == id + port:=3;;
+
+(port:=4; port:=3; filter port=3) <= id + port:=3;;
+
+(port:=4; port:=3; filter port=3) ==  port:=3;;
+
+
+(* simple hops through the network *)
+
+filter(switch=0); switch:=1; dup; filter(switch=1); switch:=2; dup  ==  filter(switch=0); switch:=1; dup; switch:=2; dup;;
+
+filter(switch=0); switch:=1; dup; filter(switch=1) == filter(switch=0); switch:=1; dup;;
+
+(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)*;;
+
+(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 + (filter port=1; switch:=2);(filter vlanId=3; drop) + (filter vlanId=3;drop) <= filter vlanId=3; drop;;
+
+(* FALSE !! *) (* id <= drop;; *)
+
+filter port=1; dup <= dup;;
+
+(* This eportploits non-canonicity of FDDs, naive implementation gets it wrong *)
+port:=1; switch:=2 == port:=1; switch:=2 + filter switch=2; port:=1;;
+
+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/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/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
diff --git a/frenetic/Decide.ml b/frenetic/Decide.ml
new file mode 100644
index 000000000..219126799
--- /dev/null
+++ b/frenetic/Decide.ml
@@ -0,0 +1,48 @@
+open Core
+open Dump
+
+
+(*===========================================================================*)
+(* COMMANDS                                                                  *)
+(*===========================================================================*)
+
+
+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 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)
+
+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
diff --git a/frenetic/Dump.ml b/frenetic/Dump.ml
index eebdc4e1c..fd013ff54 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 ()
@@ -148,7 +148,7 @@ end
 
 
 (*===========================================================================*)
-(* COMMANDS: Local, Global, Virtual, Auto                                    *)
+(* COMMANDS: Local, Global, Virtual, Auto, Decision                          *)
 (*===========================================================================*)
 
 module Local = struct
@@ -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
 
 
@@ -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\n" (Bool.to_string h);
+    print_time th;
+    printf "\nequivalent (Simple): %s\n" (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/frenetic/frenetic.ml b/frenetic/frenetic.ml
index f8325e044..1366a39f3 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_Compiler.ml b/lib/Frenetic_NetKAT_Compiler.ml
index 7f338d85b..c974eee1a 100644
--- a/lib/Frenetic_NetKAT_Compiler.ml
+++ b/lib/Frenetic_NetKAT_Compiler.ml
@@ -851,7 +851,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
@@ -971,7 +971,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 547a345ee..746e2424b 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). *)
 
@@ -18,7 +24,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
@@ -26,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
diff --git a/lib/Frenetic_NetKAT_Equivalence.ml b/lib/Frenetic_NetKAT_Equivalence.ml
new file mode 100644
index 000000000..7061acf29
--- /dev/null
+++ b/lib/Frenetic_NetKAT_Equivalence.ml
@@ -0,0 +1,260 @@
+open Core
+
+module Automaton = Frenetic_NetKAT_Compiler.Automaton
+module FDD = Frenetic_NetKAT_Compiler.FDD
+
+
+(*===========================================================================*)
+(* UPTO                                                                      *)
+(*===========================================================================*)
+
+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 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 = 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 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
+end
+
+
+
+(*===========================================================================*)
+(* Transition Trees                                                          *)
+(*===========================================================================*)
+
+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)
+
+  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
+
+
+(*===========================================================================*)
+(* Symbolic Packets                                                          *)
+(*===========================================================================*)
+
+module SymPkt = struct
+
+  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) =
+
+    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 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
+      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
+      (* 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
+
+    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:(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 =
+      (* 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
+      | 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
+
+    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
+      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 ();
+    eq_state_ids pk a1.source a2.source
+
+end
+
+
+(*===========================================================================*)
+(* Instantiations                                                            *)
+(*===========================================================================*)
+
+module Hopcroft = Make_Naive(Upto_Trans ())
+module Simple = Make_Naive(Upto_Nada ())
diff --git a/lib/Frenetic_NetKAT_Lexer.ml b/lib/Frenetic_NetKAT_Lexer.ml
index 41ce37870..22a3cdeec 100644
--- a/lib/Frenetic_NetKAT_Lexer.ml
+++ b/lib/Frenetic_NetKAT_Lexer.ml
@@ -125,6 +125,10 @@ let token ~ppx ~loc_start buf =
       illegal buf '['
     else
       iverson ~loc_start buf
+  (* equivalence *)
+  | "==" -> EQUIVALENT
+  | "<=" -> LEQ
+  | ";;" -> DOUBLESEMICOLON
   (* predicates *)
   | "true" -> TRUE
   | "false" -> FALSE
@@ -132,6 +136,7 @@ let token ~ppx ~loc_start buf =
   | "or" -> OR
   | "not" -> NOT
   | '=' -> EQUALS
+  | "!=" -> NEQUALS
   (* policies *)
   | "id" -> ID
   | "drop" -> DROP
diff --git a/lib/Frenetic_NetKAT_Parser.ml b/lib/Frenetic_NetKAT_Parser.ml
index ec42a44fa..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
+
+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 87a829f89..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
+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 2159c2279..8f4a42e51 100644
--- a/lib/Parser.cppo.mly
+++ b/lib/Parser.cppo.mly
@@ -34,8 +34,11 @@ let parse_ocaml_expr (s,loc) =
 #endif
 %}
 
+(* equivalence *)
+%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
@@ -76,7 +79,29 @@ let parse_ocaml_expr (s,loc) =
 %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 )
@@ -159,6 +184,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] )
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/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 *)