From e493ab20817cd8261962e532192c58acfc40df3d Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Thu, 20 Jan 2022 15:19:33 +0100 Subject: [PATCH] add quantifier elimination, together with a textual print function --- .gitignore | 1 + README.md | 1 + lib/bdd.ml | 41 +++++++++++++++++++++++++++++++++++++ lib/bdd.mli | 14 +++++++++++++ test/dune | 5 +++++ test/quant_elim.ml | 51 ++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 113 insertions(+) create mode 100644 test/quant_elim.ml diff --git a/.gitignore b/.gitignore index ac1ffb2..a3be6c1 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ _build *merlin *.install +*~ \ No newline at end of file diff --git a/README.md b/README.md index c35ddad..c7a90a2 100644 --- a/README.md +++ b/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 diff --git a/lib/bdd.ml b/lib/bdd.ml index f011e13..81e084a 100644 --- a/lib/bdd.ml +++ b/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 "@[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 = diff --git a/lib/bdd.mli b/lib/bdd.mli index e04a287..88b23ee 100644 --- a/lib/bdd.mli +++ b/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 diff --git a/test/dune b/test/dune index cbf6e1d..fccba8e 100644 --- a/test/dune +++ b/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) diff --git a/test/quant_elim.ml b/test/quant_elim.ml new file mode 100644 index 0000000..0445d3a --- /dev/null +++ b/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 ()