add quantifier elimination, together with a textual print function

.gitignore

@@ -1,3 +1,4 @@
 _build
 *merlin
 *.install
+*~

README.md

@@ -24,6 +24,7 @@ Many executables:
 - `test`: tests producing graphical output - you'll need the `graphviz` and `gv` packages from your distribution
 - `tiling`
 - `bdd_sat`: a propositional tautology checker using `bdd`
+- `quant_elim`: simple tests for quantifier elimination
 - `queen`: computes the number of solutions to the n-queens problem, using a propositional formula (this is not an efficient way to solve this problem, simply another way to test the `bdd` library)
 - `path`
 - `check`: a quick check

lib/bdd.ml

@@ -43,6 +43,8 @@ module type BDD = sig
   val mk_or : t -> t -> t
   val mk_imp : t -> t -> t
   val mk_iff : t -> t -> t
+  val mk_exist : (variable -> bool) -> t -> t
+  val mk_forall : (variable -> bool) -> t -> t
   val apply : (bool -> bool -> bool) -> t -> t -> t
   val constrain : t -> t -> t
   val restriction : t -> t -> t
@@ -55,6 +57,7 @@ module type BDD = sig
   val random_sat : t -> (variable * bool) list
   val all_sat : t -> (variable * bool) list list
   val print_var : Format.formatter -> variable -> unit
+  val print : Format.formatter -> t -> unit
   val to_dot : t -> string
   val print_to_dot : t -> file:string -> unit
   val display : t -> unit
@@ -89,6 +92,14 @@ type t = bdd (* export *)
 
 let view b = b.node
 
+let rec print fmt b =
+  match b.node with
+  | Zero -> Format.fprintf fmt "false"
+  | One  -> Format.fprintf fmt "true"
+  | Node(v,l,h) ->
+     Format.fprintf fmt "@[<hv 2>if %a@ then %a@ else %a@]" print_var v print h print l
+
+
 (* unused
 let equal x y = match x, y with
   | Node (v1, l1, h1), Node (v2, l2, h2) ->
@@ -369,6 +380,36 @@ let mk_or = gapply Op_or
 let mk_imp = gapply Op_imp
 let mk_iff = gapply (Op_any (fun b1 b2 -> b1 == b2))
 
+
+
+(** {2 quantifier elimination} *)
+
+let rec quantifier_elim cache op filter b =
+  try
+    H1.find cache b
+  with Not_found ->
+    let res = match b.node with
+      | Zero | One -> b
+      | Node(v,l,h) ->
+         let low = quantifier_elim cache op filter l in
+         let high = quantifier_elim cache op filter h in
+         if filter v then
+           op low high
+         else
+           mk v ~low ~high
+    in
+    H1.add cache b res;
+    res
+
+
+let mk_exist filter b =
+  let cache = H1.create cache_default_size in
+  quantifier_elim cache mk_or filter b
+
+let mk_forall filter b =
+  let cache = H1.create cache_default_size in
+  quantifier_elim cache mk_and filter b
+
 let apply f = gapply (Op_any f)
 
 let constrain b1 b2 =

lib/bdd.mli

@@ -80,6 +80,17 @@ module type BDD = sig
     (** Builds bdds for negation, conjunction, disjunction, implication,
         and logical equivalence. *)
 
+  (** Quantifier elimination *)
+
+  val mk_exist : (variable -> bool) -> t -> t
+  val mk_forall : (variable -> bool) -> t -> t
+  (** [mk_exists f b] (resp. [mk_forall f b]) quantifies bdd [b] over
+     all variables [v] for which [f v] holds. For example: [mk_exists
+     x. x /\ y] produces [y], [mk_exists x. x \/ y] produces [one],
+     [mk_forall x. x /\ y] produces [zero] and [mk_forall x. x \/ y]
+     produces [y]. See [test/quant_elim.ml]. *)
+
+
   (** Generic binary operator constructor *)
 
   val apply : (bool -> bool -> bool) -> t -> t -> t
@@ -142,6 +153,9 @@ module type BDD = sig
 
   val print_var : Format.formatter -> variable -> unit
 
+  val print : Format.formatter -> t -> unit
+  (** prints as compound if-then-else expressions *)
+
   val to_dot : t -> string
 
   val print_to_dot : t -> file:string -> unit

test/dune

@@ -32,6 +32,11 @@
   (modules bdd_sat)
   (libraries prop unix))
 
+(executable
+  (name quant_elim)
+  (modules quant_elim)
+  (libraries bdd))
+
 (executable
   (name bench_prop_cli)
   (modules bench_prop_cli)

test/quant_elim.ml

@@ -0,0 +1,51 @@
+
+
+let x = 1
+let y = 2
+let z = 3
+
+let print_var fmt x =
+  match x with
+  | 1 -> Format.fprintf fmt "x"
+  | 2 -> Format.fprintf fmt "y"
+  | 3 -> Format.fprintf fmt "z"
+  | _ -> Format.fprintf fmt "b%d" x
+
+module B = Bdd.Make(struct
+               let print_var = print_var
+               let size = 7001
+               let max_var = 100
+             end)
+
+open Format
+
+let test () =
+  (* x /\ y *)
+  let andxy = B.mk_and (B.mk_var x) (B.mk_var y) in
+  (* x \/ y *)
+  let orxy = B.mk_or (B.mk_var x) (B.mk_var y) in
+  (* y /\ z *)
+  let andyz = B.mk_and (B.mk_var y) (B.mk_var z) in
+  (* y \/ z *)
+  let oryz = B.mk_or (B.mk_var y) (B.mk_var z) in
+  let b = B.mk_exist ((==) y) andxy in
+  printf "exists y. x /\\ y ===> @[%a@]@." B.print b;
+  let b = B.mk_exist ((==) y) orxy in
+  printf "exists y. x \\/ y ===> @[%a@]@." B.print b;
+  let b = B.mk_exist ((==) y) andyz in
+  printf "exists y. y /\\ z ===> @[%a@]@." B.print b;
+  let b = B.mk_exist ((==) y) oryz in
+  printf "exists y. y \\/ z ===> @[%a@]@." B.print b;
+  let b = B.mk_forall ((==) y) andxy in
+  printf "forall y. x /\\ y ===> @[%a@]@." B.print b;
+  let b = B.mk_forall ((==) y) orxy in
+  printf "forall y. x \\/ y ===> @[%a@]@." B.print b;
+  let b = B.mk_forall ((==) y) andyz in
+  printf "forall y. y /\\ z ===> @[%a@]@." B.print b;
+  let b = B.mk_forall ((==) y) oryz in
+  printf "forall y. y \\/ z ===> @[%a@]@." B.print b;
+  ()
+
+
+
+let () = test ()