From 3f144c5c3b70ccff27b3429d745065578797de8e Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Tue, 26 Nov 2019 02:03:43 +0100 Subject: [PATCH] remove a lot of stuff, clean code --- LICENSE.md | 2 +- README.md | 62 +------ bench/bench.ml | 80 -------- bench/dune | 4 - examples/numlink/dune | 12 -- examples/numlink/lexer.mll | 41 ---- examples/numlink/main.ml | 146 --------------- examples/numlink/numlink.ml | 125 ------------- examples/numlink/parser.mly | 23 --- examples/numlink/test1.numlink | 7 - examples/numlink/test10.numlink | 1 - examples/numlink/test11.numlink | 2 - examples/numlink/test2.numlink | 2 - examples/numlink/test3.numlink | 2 - examples/numlink/test4.numlink | 1 - examples/numlink/test5.numlink | 1 - examples/numlink/test6.numlink | 4 - examples/numlink/test7.numlink | 3 - examples/queen/dune | 4 - examples/queen/queen.ml | 99 ---------- scripts/bench.sh | 9 - scripts/build.sh | 7 - scripts/clean.sh | 7 - scripts/coverage.sh | 13 -- scripts/install.sh | 8 - scripts/landmarks.sh | 8 - scripts/numlink.sh | 9 - scripts/test.sh | 8 - scripts/todo.sh | 6 - src/bdd.ml | 267 +++++++++++++++++++++++++++ src/bdd/common.ml | 318 -------------------------------- src/bdd/dune | 6 - src/bdd/hashconsed.ml | 44 ----- src/bdd/naive.ml | 19 -- src/bdd/utils.ml | 3 - src/dune | 5 + src/expr/cli.ml | 17 -- src/expr/comp.ml | 66 ------- src/expr/dune | 12 -- src/expr/lang.ml | 15 -- src/expr/lexer.mll | 68 ------- src/expr/parser.mly | 38 ---- src/memo/dune | 5 - src/memo/memo.ml | 56 ------ tests/dune | 4 - tests/tests.ml | 140 -------------- 46 files changed, 275 insertions(+), 1504 deletions(-) delete mode 100644 bench/bench.ml delete mode 100644 bench/dune delete mode 100644 examples/numlink/dune delete mode 100644 examples/numlink/lexer.mll delete mode 100644 examples/numlink/main.ml delete mode 100644 examples/numlink/numlink.ml delete mode 100644 examples/numlink/parser.mly delete mode 100644 examples/numlink/test1.numlink delete mode 100644 examples/numlink/test10.numlink delete mode 100644 examples/numlink/test11.numlink delete mode 100644 examples/numlink/test2.numlink delete mode 100644 examples/numlink/test3.numlink delete mode 100644 examples/numlink/test4.numlink delete mode 100644 examples/numlink/test5.numlink delete mode 100644 examples/numlink/test6.numlink delete mode 100644 examples/numlink/test7.numlink delete mode 100644 examples/queen/dune delete mode 100644 examples/queen/queen.ml delete mode 100755 scripts/bench.sh delete mode 100755 scripts/build.sh delete mode 100755 scripts/clean.sh delete mode 100755 scripts/coverage.sh delete mode 100755 scripts/install.sh delete mode 100755 scripts/landmarks.sh delete mode 100755 scripts/numlink.sh delete mode 100755 scripts/test.sh delete mode 100755 scripts/todo.sh create mode 100644 src/bdd.ml delete mode 100644 src/bdd/common.ml delete mode 100644 src/bdd/dune delete mode 100644 src/bdd/hashconsed.ml delete mode 100644 src/bdd/naive.ml delete mode 100644 src/bdd/utils.ml create mode 100644 src/dune delete mode 100644 src/expr/cli.ml delete mode 100644 src/expr/comp.ml delete mode 100644 src/expr/dune delete mode 100644 src/expr/lang.ml delete mode 100644 src/expr/lexer.mll delete mode 100644 src/expr/parser.mly delete mode 100644 src/memo/dune delete mode 100644 src/memo/memo.ml delete mode 100644 tests/dune delete mode 100644 tests/tests.ml diff --git a/LICENSE.md b/LICENSE.md index d9b459b..020701c 100644 --- a/LICENSE.md +++ b/LICENSE.md @@ -1,7 +1,7 @@ The ISC License (ISC) ===================== -Copyright © 2019, Léo Andrès and Jean-Christophe Filliâtre +Copyright © 2019, Léo Andrès Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies. diff --git a/README.md b/README.md index 08c09ee..e7f5326 100644 --- a/README.md +++ b/README.md @@ -1,64 +1,6 @@ -# Binary Decision Diagram library in OCaml +# bdd -This library provides many implementations of BDD with the same interface. We provide the same set of tests and benchmarks for all of them. - -There's two base implementation: - -- `src/bdd_naive.ml`: naïve implementation -- `src/bdd_hashcons.ml`: hash-consing implementation - -They both are functors to which you can either give the module `Memo.Real` or `Memo.Fake` depending on if you want the implementation to use memoïzation or not. - -They all have the same functorial interface, that you can find in `src/bdd.ml`. - -We have our own implementation of boolean expression: - -- `src/lexer.mll`: the lexer -- `src/parser.mly`: the parser -- `src/lang.ml`: the abstract syntax -- `src/comp.ml`: high-level functions to get an AST from a file or a string containing an expression written in the concrete syntax - -Here's what an expression in the concrete-syntax looks like: `((false || true) && z => true) <=> !(x && y || z)`. - -## Build - -You need to have `dune` on your system. Then: - -```sh -scripts/build.sh -``` - -## Test - -You need to have the `alcotest` package. Then: - -```sh -scripts/test.sh -``` - -## Code coverage - -You need to have the `bisect_ppx` package. Then: - -```sh -scripts/coverage.sh -``` - -It should open the coverage report in your browser. - -## Bench - -An expression written in the concrete syntax - don't forget to put double quotes around it: - -```sh -scripts/bench.sh -e -``` - -A file containing an expression: - -```sh -scripts/bench.sh -f -``` +bdd is an OCaml library for Binary Decision Diagram ## Change Log diff --git a/bench/bench.ml b/bench/bench.ml deleted file mode 100644 index 9a5a04f..0000000 --- a/bench/bench.ml +++ /dev/null @@ -1,80 +0,0 @@ -module Make2 (M : Bdd.Common.S) = struct - module M = Bdd.Common.Make (M) - - let rec build l r i = - let v = Bdd.Common.Base.var_of_string (string_of_int i) in - if i = 1 then M.node v l r - else - let b = if i mod 2 = 0 then M.node v l r else M.node v r l in - build r b (i - 1) - - let bench_one s = - let start = Unix.gettimeofday () in - let bdd = build M.false_bdd M.true_bdd 40 in - let bdd' = M.conj bdd bdd in - let stop = Unix.gettimeofday () in - Printf.printf "bench %s %.2f\n" s (stop -. start) ; - Printf.printf "size(bdd) = %d, size(bdd') = %d\n" (M.size bdd) (M.size bdd') ; - flush stdout -end - -module Make (M : Bdd.Common.S) = struct - module M = Bdd.Common.Make (M) - - let bench_one tbl expr = - let start = Unix.gettimeofday () in - let bdd = M.of_expr expr in - ignore (M.compute tbl bdd) ; - let stop = Unix.gettimeofday () in - stop -. start - - let bench_n n tbl expr = - let sum = ref 0. in - for _ = 0 to n do - sum := !sum +. bench_one tbl expr - done ; - !sum - - let bench_n_print n s tbl expr = - Printf.printf "bench %s %.2f\n" s (bench_n n tbl expr) ; - flush stdout -end - -let _ = - let expr = Expr.Cli.get_expr () in - let tbl = Hashtbl.create 512 in - let v = Bdd.Common.Base.var_of_string in - Hashtbl.add tbl (v "x") false ; - Hashtbl.add tbl (v "y") true ; - let module I1 = Bdd.Naive.Make (Memo.Fake) in - let module I2 = Bdd.Naive.Make (Memo.Make) in - let module I3 = Bdd.Hashconsed.Make (Memo.Fake) in - let module I4 = Bdd.Hashconsed.Make (Memo.Make) in - let n = 1 in - let module B1 = Make (I1) in - let module B2 = Make (I2) in - let module B3 = Make (I3) in - let module B4 = Make (I4) in - B1.bench_n_print n "naïve: " tbl expr ; - B2.bench_n_print n "naïve + memo: " tbl expr ; - B3.bench_n_print n "hashcons: " tbl expr ; - B4.bench_n_print n "hashcons + memo:" tbl expr ; - let module B1 = Make2 (I1) in - let module B2 = Make2 (I2) in - let module B3 = Make2 (I3) in - let module B4 = Make2 (I4) in - (*B1.bench_one "naïve: ";*) - B2.bench_one "naïve + memo: " ; - (* B3.bench_one "hashcons: ";*) - B4.bench_one "hashcons + memo:" ; - let module T = Bdd.Common.Make (I4) in - let sat = T.all_sat (T.of_expr expr) in - List.iter - (fun l -> - print_endline "One sat is:" ; - List.iter - (fun (v, b) -> - Printf.printf "%s = %B\n" (Bdd.Common.Base.string_of_var v) b) - l) - sat ; - () diff --git a/bench/dune b/bench/dune deleted file mode 100644 index 479acd7..0000000 --- a/bench/dune +++ /dev/null @@ -1,4 +0,0 @@ -(executable - (name bench) - (libraries unix bdd expr) - (modules bench)) diff --git a/examples/numlink/dune b/examples/numlink/dune deleted file mode 100644 index fa2cb5c..0000000 --- a/examples/numlink/dune +++ /dev/null @@ -1,12 +0,0 @@ -(executable - (name main) - (libraries expr bdd landmarks) - (preprocess (pps landmarks.ppx --auto)) - (modules main parser lexer numlink)) - -(ocamllex - (modules lexer)) - -(menhir - (modules parser) - (flags ("--explain" "--dump"))) diff --git a/examples/numlink/lexer.mll b/examples/numlink/lexer.mll deleted file mode 100644 index 5316931..0000000 --- a/examples/numlink/lexer.mll +++ /dev/null @@ -1,41 +0,0 @@ -{ - open Parser - - exception Error of string - - let current_line = ref 1 - let current_offset = ref 1 - let total_offset = ref 1 - - let mem_new_line = ref [] - - let get_mem_new_line () = List.rev (!mem_new_line) - - let new_line_met () = - total_offset := !total_offset + 1; - mem_new_line := (!total_offset)::(!mem_new_line); - current_line := !current_line + 1; - current_offset := 0 - - let incr_offset x = - total_offset := !total_offset + x; - current_offset := !current_offset + x - - let incr_offset_string x = - incr_offset (String.length x) - - let parser_fail msg = - raise (Error (Printf.sprintf "Line %d, at offset %d: %s." (!current_line) (!current_offset) msg)) - -} - -let newline = ['\n' '\r'] -let digit = ['0'-'9'] - -rule token = parse - | 'x' { incr_offset 1; BLANK } - | digit as i { let i = String.make 1 i in incr_offset_string i; NUM (int_of_string i) } - | newline { new_line_met (); EOL } - | eof { EOF } - | _ { parser_fail "unexpected character" } - diff --git a/examples/numlink/main.ml b/examples/numlink/main.ml deleted file mode 100644 index 5642f0d..0000000 --- a/examples/numlink/main.ml +++ /dev/null @@ -1,146 +0,0 @@ -exception Stop - -let from_lexing buf = - match Parser.file_final Lexer.token buf with - | exception Lexer.Error msg -> - failwith ("lexer: " ^ msg) - | exception _ -> - let err_pos = Lexing.lexeme_start buf in - let err_line, line_offset = (ref 1, ref 0) in - ( try - List.iter - (fun x -> - if x > err_pos then raise Stop ; - incr err_line ; - line_offset := x) - (Lexer.get_mem_new_line ()) - with Stop -> () ) ; - failwith - (Printf.sprintf "parser: On line %d, at offset %d, syntax error." - !err_line (err_pos - !line_offset)) - | res -> - res - -let from_file f = - let chan = open_in f in - let buf = Lexing.from_channel chan in - let res = from_lexing buf in - close_in chan ; res - -let from_string s = - let buf = Lexing.from_string s in - from_lexing buf - -let get_cli () = - let f = ref None in - let e = ref None in - Arg.parse - [ ("-f", Arg.String (fun s -> f := Some s), "file") - ; ("-e", Arg.String (fun s -> e := Some s), "expression") ] - (fun _ -> ()) - "get_expr" ; - match (!e, !f) with - | Some _, Some _ -> - raise (Arg.Bad "file or expression, not both") - | Some e, _ -> - from_string e - | _, Some f -> - from_file f - | None, None -> - raise (Arg.Bad "file or expression needed") - -let print_parsed_list = - Format.printf "parsed grid is:@." ; - List.iter (fun el -> - List.iter - (function None -> Format.printf "x" | Some i -> Format.printf "%d" i) - el ; - Format.printf "@.") - -let assert_correct_size = function - | [] -> - () - | x :: s -> - let len = List.length x in - List.iter (fun el -> assert (List.length el = len)) s - -let assert_correct_num m = - let tbl = Hashtbl.create 256 in - List.iter - (fun el -> - List.iter - (function - | None -> - () - | Some el -> ( - match Hashtbl.find tbl el with - | exception Not_found -> - Hashtbl.add tbl el 1 - | x -> - Hashtbl.replace tbl el (x + 1) )) - el) - m ; - Hashtbl.iter (fun _ v -> assert (v = 2)) tbl - -let _ = - let map = get_cli () in - print_parsed_list map ; - assert_correct_size map ; - assert_correct_num map ; - let height = List.length map in - let width = - match map with [] -> failwith "invalid map size" | x :: _ -> List.length x - in - (* Format.printf "width = %d ; height = %d@." width height; *) - let tbl = Hashtbl.create 256 in - List.iteri - (fun j el -> - List.iteri - (fun i -> function None -> () | Some el -> ( - match Hashtbl.find tbl el with - | exception Not_found -> - Hashtbl.add tbl el [(i, j)] - | x -> - Hashtbl.replace tbl el ([(i, j)] @ x) )) - el) - map ; - let graph = Numlink.empty_graph () in - let pairs = Numlink.empty_set () in - for i = 0 to width - 1 do - for j = 0 to height - 1 do - Numlink.add_vertex graph (i, j) - done - done ; - let is_in_graph (x, y) = x >= 0 && y >= 0 && x < width && y < height in - let add_if_in_graph p p' = - if is_in_graph p' then Numlink.add_edge graph p p' - in - for i = 0 to width - 1 do - for j = 0 to height - 1 do - add_if_in_graph (i, j) (i + 1, j) ; - add_if_in_graph (i, j) (i, j + 1) - done - done ; - Hashtbl.iter - (fun _ -> function [x; y] -> Numlink.set_add pairs (x, y) | _ -> - failwith "not a pair...") - tbl ; - Format.printf "building the expression...@." ; - let to_solve = Numlink.build_expr graph pairs in - let module M = Bdd.Common.Make (Bdd.Hashconsed.Make (Memo.Make)) in - Format.printf "building bdd...@." ; - let bdd = M.of_expr to_solve in - Format.printf "done !@." ; - let max_var = Bdd.Common.Base.max_var () in - Format.printf "size = %d ; max_var = %d@." (M.size bdd) max_var ; - Format.printf "count_sat = %d@." (M.count_sat max_var bdd) ; - let res = M.any_sat bdd in - match res with - | None -> - Format.printf "pas de solution@." - | Some l -> - List.iter - (fun (v, b) -> - if b then Format.printf "%s@." (Bdd.Common.Base.string_of_var v)) - l ; - () diff --git a/examples/numlink/numlink.ml b/examples/numlink/numlink.ml deleted file mode 100644 index 3b562b2..0000000 --- a/examples/numlink/numlink.ml +++ /dev/null @@ -1,125 +0,0 @@ -let empty_set () = Hashtbl.create 512 - -let set_add s el = Hashtbl.add s el () - -let set_iter f = Hashtbl.iter (fun k _ -> f k) - -let set_mem = Hashtbl.mem - -let empty_graph () = (empty_set (), empty_set ()) - -let add_vertex g v = set_add (fst g) v - -let add_edge g v v' = set_add (snd g) (v, v') - -let set_to_list s = List.of_seq (Hashtbl.to_seq_keys s) - -let set_length = Hashtbl.length - -module E = Expr.Lang - -let range_list n = - let res = ref [] in - for i = n - 1 downto 0 do - res := i :: !res - done ; - !res - -let filter_vertex s v = Seq.filter (fun (el, _, _) -> el = v) s - -let var_to_string (v, path, pos) = - let v = - match v with - | None -> - "phantom" - | Some (vx, vy) -> - Printf.sprintf "(%d,%d)" vx vy - in - Printf.sprintf "%s: path %d, pos %d" v path pos - -let for_all e f = E.BigAnd (Seq.map f e) - -let exists e f = E.BigOr (Seq.map f e) - -let exists_unique e f = - E.BigOr - (Seq.map - (fun x -> - E.BigAnd (Seq.map (fun x' -> if x = x' then f x else E.Neg (f x')) e)) - e) - -let without_phantom = Seq.filter (function None -> false | _ -> true) - -let mk vertex path pos = E.Var (var_to_string (vertex, path, pos)) - -let vertex_appears_once vertices paths positions = - for_all (vertices |> without_phantom) (fun vertex -> - exists_unique paths (fun path -> - exists_unique positions (fun pos -> mk vertex path pos))) - -let path_pos_occupied_once vertices paths positions = - for_all paths (fun path -> - for_all positions (fun pos -> - exists_unique vertices (fun vertex -> mk vertex path pos))) - -let are_adjacent edges v v' = - match (v, v') with - | None, _ | _, None -> - false - | Some v, Some v' -> - set_mem edges (v, v') || set_mem edges (v', v) - -let path_finished paths positions n = - for_all paths (fun path -> - for_all positions (fun pos -> - if pos < n - 1 then E.Imp (mk None path pos, mk None path (pos + 1)) - else E.True)) - -let conseq_in_path_imply_adjacent paths positions vertices edges n = - for_all paths (fun path -> - for_all positions (fun pos -> - if pos < n - 1 then - for_all (vertices |> without_phantom) (fun vertex -> - for_all (vertices |> without_phantom) (fun vertex' -> - if are_adjacent edges vertex vertex' then E.True - else - E.Neg - (E.And (mk vertex path pos, mk vertex' path (pos + 1))))) - else E.True)) - -let check_src_dst to_connect positions n paths = - let to_connect = set_to_list to_connect in - for_all paths (fun i -> - let src, dst = List.nth to_connect i in - E.And - ( mk (Some src) i 0 - , exists positions (fun pos -> - let v = mk (Some dst) i pos in - if pos < n - 1 then E.And (v, mk None i (pos + 1)) else v) )) - -let build_expr (vertices, edges) to_connect = - (* adding the phantom vertex as None and making others Some *) - let vertices' = empty_set () in - set_iter (fun x -> set_add vertices' (Some x)) vertices ; - set_add vertices' None ; - let vertices = vertices' in - let k = set_length to_connect in - let n = set_length vertices - 1 in - (* we don't count the phantom vertex ! *) - let vertices = set_to_list vertices in - let paths = range_list k in - let positions = range_list n in - let vertices = List.to_seq vertices in - let paths = List.to_seq paths in - let positions = List.to_seq positions in - let c1 = vertex_appears_once vertices paths positions in - (*Expr.Comp.print (Format.formatter_of_out_channel stdout) c1;*) - let c2 = path_pos_occupied_once vertices paths positions in - (*Expr.Comp.print (Format.formatter_of_out_channel stdout) c2;*) - let c3 = path_finished paths positions n in - (*Expr.Comp.print (Format.formatter_of_out_channel stdout) c3;*) - let c4 = conseq_in_path_imply_adjacent paths positions vertices edges n in - (*Expr.Comp.print (Format.formatter_of_out_channel stdout) c4;*) - let c5 = check_src_dst to_connect positions n paths in - (*Expr.Comp.print (Format.formatter_of_out_channel stdout) c5;*) - Expr.Comp.list_to_conj [c1; c2; c3; c4; c5] diff --git a/examples/numlink/parser.mly b/examples/numlink/parser.mly deleted file mode 100644 index 76ecf1a..0000000 --- a/examples/numlink/parser.mly +++ /dev/null @@ -1,23 +0,0 @@ -%{ -%} - -%token EOF -%token EOL -%token BLANK -%token NUM - -%start < (int option) list list> file_final - -%% -file_final: -| f = file EOF { f } - -file: -| l = list(line) { l } - -line: -| l = list(block) EOL { l } - -block: -| BLANK { None } -| i = NUM { Some i } diff --git a/examples/numlink/test1.numlink b/examples/numlink/test1.numlink deleted file mode 100644 index db8d69c..0000000 --- a/examples/numlink/test1.numlink +++ /dev/null @@ -1,7 +0,0 @@ -xxx4xxx -x3xx25x -xxx31xx -xxx5xxx -xxxxxxx -xx1xxxx -2xxx4xx diff --git a/examples/numlink/test10.numlink b/examples/numlink/test10.numlink deleted file mode 100644 index 3bf2967..0000000 --- a/examples/numlink/test10.numlink +++ /dev/null @@ -1 +0,0 @@ -1xxxxxxxx1 diff --git a/examples/numlink/test11.numlink b/examples/numlink/test11.numlink deleted file mode 100644 index 925e20d..0000000 --- a/examples/numlink/test11.numlink +++ /dev/null @@ -1,2 +0,0 @@ -1x1 -2x2 diff --git a/examples/numlink/test2.numlink b/examples/numlink/test2.numlink deleted file mode 100644 index d5f829e..0000000 --- a/examples/numlink/test2.numlink +++ /dev/null @@ -1,2 +0,0 @@ -1xxxx -xxxx1 diff --git a/examples/numlink/test3.numlink b/examples/numlink/test3.numlink deleted file mode 100644 index b8be7f4..0000000 --- a/examples/numlink/test3.numlink +++ /dev/null @@ -1,2 +0,0 @@ -1xx -xx1 diff --git a/examples/numlink/test4.numlink b/examples/numlink/test4.numlink deleted file mode 100644 index c642bc9..0000000 --- a/examples/numlink/test4.numlink +++ /dev/null @@ -1 +0,0 @@ -1x1 diff --git a/examples/numlink/test5.numlink b/examples/numlink/test5.numlink deleted file mode 100644 index b4de394..0000000 --- a/examples/numlink/test5.numlink +++ /dev/null @@ -1 +0,0 @@ -11 diff --git a/examples/numlink/test6.numlink b/examples/numlink/test6.numlink deleted file mode 100644 index 4866ded..0000000 --- a/examples/numlink/test6.numlink +++ /dev/null @@ -1,4 +0,0 @@ -123 -xx3 -xxx -x12 diff --git a/examples/numlink/test7.numlink b/examples/numlink/test7.numlink deleted file mode 100644 index 173c14b..0000000 --- a/examples/numlink/test7.numlink +++ /dev/null @@ -1,3 +0,0 @@ -1xx -xxx -xx1 diff --git a/examples/queen/dune b/examples/queen/dune deleted file mode 100644 index 3a78579..0000000 --- a/examples/queen/dune +++ /dev/null @@ -1,4 +0,0 @@ -(executable - (name queen) - (libraries expr bdd landmarks) - (preprocess (pps landmarks.ppx --auto))) diff --git a/examples/queen/queen.ml b/examples/queen/queen.ml deleted file mode 100644 index 3dde3e6..0000000 --- a/examples/queen/queen.ml +++ /dev/null @@ -1,99 +0,0 @@ -(**************************************************************************) -(* *) -(* Copyright (C) Jean-Christophe Filliatre *) -(* *) -(* This software is free software; you can redistribute it and/or *) -(* modify it under the terms of the GNU Library General Public *) -(* License version 2, with the special exception on linking *) -(* described in file LICENSE. *) -(* *) -(* This software is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) -(* *) -(**************************************************************************) - -open Format -include Bdd.Common.Make (Bdd.Hashconsed.Make (Memo.Make)) - -(* - N*N variables v i j = une reine dans la case (i,j) - - forall i. - exists j. v i j // une reine sur chaque ligne - - forall i j. v i j -> // si une reine en i j alors - forall k. k = i \/ not (v i k) // pas de reine sur la même ligne - forall k. k = j \/ not (v k j) // pas de reine sur la même colonne - forall k. ... // pas de reine sur la diagonale montante - forall k. ... // pas de reine sur la diagonale descendante - -*) - -let _ = - if Array.length Sys.argv <> 2 then - failwith ("Usage: " ^ Sys.argv.(0) ^ " ") - -let n = try int_of_string Sys.argv.(1) with _ -> eprintf "queen N" ; exit 1 - -let nb_vars = n * n - -(* 0..n-1 x 0..n-1 -> 1..n x n *) -let vars = Array.init n (fun i -> Array.init n (fun j -> var_bdd ((n * i) + j))) - -let var i j = vars.(i).(j) - -let mk_not = neg - -let one = true_bdd - -let zero = false_bdd - -let mk_and = conj - -let mk_or = disj - -let mk_imp = imp - -let fold_and i j f = - let rec mk k = if k > j then one else mk_and (f k) (mk (k + 1)) in - mk i - -let fold_or i j f = - let rec mk k = if k > j then zero else mk_or (f k) (mk (k + 1)) in - mk i - -let fold_for i j f = - let rec fold k acc = if k > j then acc else fold (k + 1) (f k acc) in - fold i - -let constraints i j = - let b1 = - fold_and 0 (n - 1) (fun l -> if l = j then one else mk_not (var i l)) - in - let b2 = - fold_and 0 (n - 1) (fun k -> if k = i then one else mk_not (var k j)) - in - let b3 = - fold_and 0 (n - 1) (fun k -> - let ll = j + k - i in - if ll >= 0 && ll < n && k <> i then mk_not (var k ll) else one) - in - let b4 = - fold_and 0 (n - 1) (fun k -> - let ll = j + i - k in - if ll >= 0 && ll < n && k <> i then mk_not (var k ll) else one) - in - mk_and b1 (mk_and b2 (mk_and b3 b4)) - -let bdd = fold_and 0 (n - 1) (fun i -> fold_or 0 (n - 1) (fun j -> var i j)) - -let bdd = - fold_for 0 (n - 1) - (fun i acc -> - fold_for 0 (n - 1) - (fun j acc -> mk_and acc (mk_imp (var i j) (constraints i j))) - acc) - bdd - -let () = printf "There are %d solutions@." (count_sat nb_vars bdd) diff --git a/scripts/bench.sh b/scripts/bench.sh deleted file mode 100755 index 3cf2166..0000000 --- a/scripts/bench.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -set -eu - - -( cd "$(dirname "$0")/../" - eval "$(opam env)" - dune exec src/bench.exe -- "$@" -) diff --git a/scripts/build.sh b/scripts/build.sh deleted file mode 100755 index b326d72..0000000 --- a/scripts/build.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/sh - -set -eu - -( cd "$(dirname "$0")/../" - eval "$(opam env)" - dune build --profile release @all ) diff --git a/scripts/clean.sh b/scripts/clean.sh deleted file mode 100755 index e3a3432..0000000 --- a/scripts/clean.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/sh - -set -eu - -( cd "$(dirname "$0")/../" - eval "$(opam env)" - dune clean ) diff --git a/scripts/coverage.sh b/scripts/coverage.sh deleted file mode 100755 index bcbd1e0..0000000 --- a/scripts/coverage.sh +++ /dev/null @@ -1,13 +0,0 @@ -#!/bin/sh - -set -eu - -( cd "$(dirname "$0")/../" - scripts/clean.sh - eval "$(opam env)" - coverage=_coverage - rm -f "$(find . -name 'bisect*.out')" || true - rm -rf $coverage - BISECT_ENABLE=YES dune runtest --no-buffer --force - bisect-ppx-report -html $coverage/ "$(find . -name 'bisect*.out')" - xdg-open $coverage/index.html ) diff --git a/scripts/install.sh b/scripts/install.sh deleted file mode 100755 index 664faf0..0000000 --- a/scripts/install.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/bin/sh - -set -eu - -( cd "$(dirname "$0")/../" - eval "$(opam env)" - dune build @install - dune install bdd ) diff --git a/scripts/landmarks.sh b/scripts/landmarks.sh deleted file mode 100755 index 2453c3c..0000000 --- a/scripts/landmarks.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/bin/sh - -set -eu - -( cd "$(dirname "$0")/../" - eval "$(opam env)" - export OCAML_LANDMARKS="output=landmarks.json,format=json,allocation" -) diff --git a/scripts/numlink.sh b/scripts/numlink.sh deleted file mode 100755 index 6cd06dd..0000000 --- a/scripts/numlink.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -set -eu - - -( cd "$(dirname "$0")/../" - eval "$(opam env)" - dune exec src/numlink/numlink.exe --profile release -- "$@" -) diff --git a/scripts/test.sh b/scripts/test.sh deleted file mode 100755 index c4b62c5..0000000 --- a/scripts/test.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/bin/sh - -set -eu - - -( cd "$(dirname "$0")/../" - eval "$(opam env)" - dune runtest --no-buffer ) diff --git a/scripts/todo.sh b/scripts/todo.sh deleted file mode 100755 index 13d67e4..0000000 --- a/scripts/todo.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -set -eu - -( cd "$(dirname "$0")/../" - ( find . -type f -print0 | xargs -0 cat) | grep -r TODO ) diff --git a/src/bdd.ml b/src/bdd.ml new file mode 100644 index 0000000..332e942 --- /dev/null +++ b/src/bdd.ml @@ -0,0 +1,267 @@ +open Hc + +type var = int + +type hidden = view hash_consed + +and view = True | False | Node of var * hidden * hidden + +module HashedT = struct + type t = view + + let equal x y = + match (x, y) with + | True, True | False, False -> + true + | Node (v1, l1, r1), Node (v2, l2, r2) -> + v1 = v2 && l1 == l2 && r1 == r2 + | _ -> + false + + let hash = function + | True -> + 1 + | False -> + 0 + | Node (v, l, r) -> + (19 * ((19 * v) + l.tag)) + r.tag + 2 +end + +module Hbdd = Hc.Make (HashedT) + +module Hash = struct + type t = hidden + + let equal = ( == ) + + let hash b = b.tag +end + +module Hash2 = struct + type t = hidden * hidden + + let equal (x1, y1) (x2, y2) = x1 == x2 && y1 == y2 + + let hash (x, y) = x.tag + (19 * y.tag) +end + +let hc = Hbdd.hashcons + +let view x = x.node + +module Mem = Memo.MakeWeak (Hash) +module Mem2 = Memo.MakeWeak (Hash) + +let true_bdd = hc True + +let false_bdd = hc False + +let get_order bdd = + match view bdd with True | False -> max_int | Node (v, _, _) -> v + +let node v l h = + if v >= get_order l || v >= get_order h then invalid_arg "node" ; + if Hash.equal l h then l else hc (Node (v, l, h)) + +let var_bdd v = node v false_bdd true_bdd + +let rec fprintf fmt bdd = + match view bdd with + | True -> + Format.fprintf fmt "true" + | False -> + Format.fprintf fmt "false" + | Node (v, l, h) -> + Format.fprintf fmt "%d ? (%a) : (%a)" v fprintf l fprintf h + +let of_bool = function true -> true_bdd | false -> false_bdd + +let neg x = + Mem.memo + (fun neg x -> + match view x with + | True -> + false_bdd + | False -> + true_bdd + | Node (var, low, high) -> + node var (neg low) (neg high)) + x + +let comb_comm op x y = + Mem2.memo + (fun comb_comm n1 n2 -> + match (view n1, view n2) with + | Node (v1, l1, h1), Node (v2, l2, h2) when v1 = v2 -> + node v1 (comb_comm l1 l2) (comb_comm h1 h2) + | Node (v1, l1, h1), Node (v2, _, _) when v1 < v2 -> + node v1 (comb_comm l1 n2) (comb_comm h1 n2) + | Node (_, _, _), Node (v2, l2, h2) -> + node v2 (comb_comm n1 l2) (comb_comm n1 h2) + | True, Node (v, l, h) | Node (v, l, h), True -> + node v (comb_comm l true_bdd) (comb_comm h true_bdd) + | False, Node (v, l, h) | Node (v, l, h), False -> + node v (comb_comm l false_bdd) (comb_comm h false_bdd) + | False, False -> + of_bool (op false false) + | False, True | True, False -> + of_bool (op true false) + | True, True -> + of_bool (op true true)) + x y + +let comb op x y = + Mem2.memo + (fun comb n1 n2 -> + match (view n1, view n2) with + | Node (v1, l1, h1), Node (v2, l2, h2) when v1 = v2 -> + node v1 (comb l1 l2) (comb h1 h2) + | Node (v1, l1, h1), Node (v2, _, _) when v1 < v2 -> + node v1 (comb l1 n2) (comb h1 n2) + | Node (_, _, _), Node (v2, l2, h2) -> + node v2 (comb n1 l2) (comb n1 h2) + | True, Node (v, l, h) -> + node v (comb true_bdd l) (comb true_bdd h) + | Node (v, l, h), True -> + node v (comb l true_bdd) (comb h true_bdd) + | False, Node (v, l, h) -> + node v (comb false_bdd l) (comb false_bdd h) + | Node (v, l, h), False -> + node v (comb l false_bdd) (comb h false_bdd) + | False, False -> + of_bool (op false false) + | False, True -> + of_bool (op false true) + | True, False -> + of_bool (op true false) + | True, True -> + of_bool (op true true)) + x y + +let conj = comb_comm (fun x y -> x && y) + +let disj = comb_comm (fun x y -> x || y) + +let imp = comb (fun x y -> (not x) || y) + +let eq = comb_comm (fun x y -> x = y) + +let compute tbl = + let rec compute_aux bdd = + match view bdd with + | False -> + false_bdd + | True -> + true_bdd + | Node (v, l, h) -> ( + match Hashtbl.find tbl v with + | exception Not_found -> + node v (compute_aux h) (compute_aux l) + | true -> + compute_aux h + | false -> + compute_aux l ) + in + compute_aux + +let size = + (* TODO *) + let module H = Hashtbl.Make (struct + type t = Hash.t + + let equal = ( == ) + + let hash = Hashtbl.hash (* TODO *) + end) in + let tbl = H.create 512 in + let rec size bdd = + match view bdd with + | False | True -> + 0 + | _ when H.mem tbl bdd -> + 0 + | Node (_, l, h) -> + H.add tbl bdd () ; + 1 + size l + size h + in + size + +let is_sat bdd = match view bdd with False -> false | _ -> true + +let count_sat maxn = + let get_var bdd = + match view bdd with False | True -> maxn | Node (v, _, _) -> v + in + let count = + Mem.memo (fun count bdd -> + match view bdd with + | False -> + 0 + | True -> + 1 + | Node (v, l, h) -> + assert ((0 <= v && v < maxn) || (Printf.printf "v = %d\n" v ; false)) ; + (count l lsl (get_var l - v - 1)) + (count h lsl (get_var h - v - 1))) + in + fun bdd -> count bdd lsl get_var bdd + +let any_sat = + let rec aux assign bdd = + match view bdd with + | False -> + None + | True -> + Some assign + | Node (v, l, h) -> ( + match aux assign l with + | None -> + aux ((v, true) :: assign) h + | Some assign -> + Some ((v, false) :: assign) ) + in + aux [] + +let all_sat bdd = + let add_assign v b = function + | None -> + None + | Some assign -> + Some ((v, b) :: assign) + in + let rec aux assign bdd = + match view bdd with + | False -> + [None] + | True -> + [Some assign] + | Node (v, l, h) -> + let add_assign = add_assign v in + let aux = aux assign in + List.map (add_assign false) (aux l) @ List.map (add_assign true) (aux h) + in + List.fold_left + (fun acc -> function None -> acc | Some assign -> assign :: acc) + [] (aux [] bdd) + +(* TODO: in each assign, add all the unused vars. ? *) + +let random_sat _ = + (* let _ = count_sat maxn in *) + let rec aux assign bdd = + match view bdd with + | False -> + None + | True -> + Some assign + | Node (v, l, h) -> ( + if is_sat l && is_sat h then + if true (* TODO *) then aux ((v, false) :: assign) h + else aux ((v, true) :: assign) l + else + match aux assign l with + | None -> + aux ((v, true) :: assign) h + | Some assign -> + Some ((v, false) :: assign) ) + in + aux [] diff --git a/src/bdd/common.ml b/src/bdd/common.ml deleted file mode 100644 index 24c970e..0000000 --- a/src/bdd/common.ml +++ /dev/null @@ -1,318 +0,0 @@ -module Base = struct - type var = int - - type expr = Expr.Lang.t - - (* TODO *) - let inv_tbl = Hashtbl.create 512 - - let string_of_var = Hashtbl.find inv_tbl - - let var_of_string, reset, max_var = - let tbl = Hashtbl.create 512 in - let gen, reset = Utils.gen_tag () in - ( (fun x -> - try Hashtbl.find tbl x - with Not_found -> - let v = gen () in - Hashtbl.add inv_tbl v x ; - Hashtbl.add tbl x v ; - (* Printf.printf "added %s -> %d\n" x v; - flush stdout;*) - v) - , (fun () -> reset ()) - , fun () -> Hashtbl.length tbl ) -end - -module type S = sig - type hidden - - type view = True | False | Node of Base.var * hidden * hidden - - module Hash : Hashtbl.HashedType with type t = hidden - - module Mem : Memo.S with type t = hidden - - val hc : view -> hidden - - val view : hidden -> view -end - -module Make (M : S) = struct - include M - - let true_bdd = hc True - - let false_bdd = hc False - - let fview f bdd = view bdd |> f - - let get_order = - fview (function True | False -> max_int | Node (v, _, _) -> v) - - let node v l h = - if v >= get_order l || v >= get_order h then invalid_arg "node" ; - if Hash.equal l h then l else hc (Node (v, l, h)) - - let ite _ _ _ = true_bdd (* TODO *) - - let var_bdd v = node v false_bdd true_bdd - - let to_string bdd = - let b = Buffer.create 512 in - let rec aux bdd = - match view bdd with - | True -> - Buffer.add_string b "true" - | False -> - Buffer.add_string b "false" - | Node (var, low, high) -> - Buffer.add_string b (Base.string_of_var var) ; - Buffer.add_string b ("(" ^ string_of_int var ^ ") ? (") ; - aux high ; - Buffer.add_string b ") : (" ; - aux low ; - Buffer.add_string b ")" - in - aux bdd ; Buffer.contents b - - let of_bool = function true -> true_bdd | false -> false_bdd - - let neg x = - Mem.memo - (fun neg -> - fview (function - | True -> - false_bdd - | False -> - true_bdd - | Node (var, low, high) -> - node var (neg low) (neg high))) - x - - (* let rec comb_comm op n1 n2 = - let comb_comm = comb_comm op in *) - let comb_comm op x y = - Mem.memo2 - (fun comb_comm n1 n2 -> - match (view n1, view n2) with - | Node (v1, l1, h1), Node (v2, l2, h2) when v1 = v2 -> - node v1 (comb_comm l1 l2) (comb_comm h1 h2) - | Node (v1, l1, h1), Node (v2, _, _) when v1 < v2 -> - node v1 (comb_comm l1 n2) (comb_comm h1 n2) - | Node (_, _, _), Node (v2, l2, h2) -> - node v2 (comb_comm n1 l2) (comb_comm n1 h2) - | True, Node (v, l, h) | Node (v, l, h), True -> - node v (comb_comm l true_bdd) (comb_comm h true_bdd) - | False, Node (v, l, h) | Node (v, l, h), False -> - node v (comb_comm l false_bdd) (comb_comm h false_bdd) - | False, False -> - of_bool (op false false) - | False, True | True, False -> - of_bool (op true false) - | True, True -> - of_bool (op true true)) - x y - - let comb op x y = - Mem.memo2 - (fun comb n1 n2 -> - match (view n1, view n2) with - | Node (v1, l1, h1), Node (v2, l2, h2) when v1 = v2 -> - node v1 (comb l1 l2) (comb h1 h2) - | Node (v1, l1, h1), Node (v2, _, _) when v1 < v2 -> - node v1 (comb l1 n2) (comb h1 n2) - | Node (_, _, _), Node (v2, l2, h2) -> - node v2 (comb n1 l2) (comb n1 h2) - | True, Node (v, l, h) -> - node v (comb true_bdd l) (comb true_bdd h) - | Node (v, l, h), True -> - node v (comb l true_bdd) (comb h true_bdd) - | False, Node (v, l, h) -> - node v (comb false_bdd l) (comb false_bdd h) - | Node (v, l, h), False -> - node v (comb l false_bdd) (comb h false_bdd) - | False, False -> - of_bool (op false false) - | False, True -> - of_bool (op false true) - | True, False -> - of_bool (op true false) - | True, True -> - of_bool (op true true)) - x y - - let conj = comb_comm (fun x y -> x && y) - - let disj = comb_comm (fun x y -> x || y) - - let imp = comb (fun x y -> (not x) || y) - - let eq = comb_comm (fun x y -> x = y) - - let compute tbl = - let compute_aux = - Mem.memo (fun compute_aux -> - fview (function - | False -> - false_bdd - | True -> - true_bdd - | Node (v, l, h) -> ( - match Hashtbl.find tbl v with - | exception Not_found -> - failwith - ("truth value of " ^ Base.string_of_var v ^ " is missing") - | true -> - compute_aux h - | false -> - compute_aux l ))) - in - compute_aux - - let to_expr = - Mem.memo (fun to_expr -> - let module E = Expr.Lang in - fview (function - | False -> - E.False - | True -> - E.True - | Node (v, l, h) -> - E.Or - ( E.And (E.Var (Base.string_of_var v), to_expr l) - , E.And (E.Neg (E.Var (Base.string_of_var v)), to_expr h) ))) - - let rec of_expr = - let module E = Expr.Lang in - function - | E.True -> - true_bdd - | E.False -> - false_bdd - | E.Var v -> ( - try var_bdd (int_of_string v) - with _ -> var_bdd (Base.var_of_string (E.var_to_string v)) ) - | E.Neg e -> - neg (of_expr e) - | E.And (e1, e2) -> - conj (of_expr e1) (of_expr e2) - | E.Or (e1, e2) -> - disj (of_expr e1) (of_expr e2) - | E.Imp (e1, e2) -> - imp (of_expr e1) (of_expr e2) - | E.Eq (e1, e2) -> - eq (of_expr e1) (of_expr e2) - | E.BigAnd e -> - Seq.fold_left (fun acc el -> conj (of_expr el) acc) true_bdd e - | E.BigOr e -> - Seq.fold_left (fun acc el -> disj (of_expr el) acc) false_bdd e - - let of_string s = of_expr (Expr.Comp.from_string s) - - let size = - (* TODO *) - let module H = Hashtbl.Make (struct - type t = M.Hash.t - - let equal = ( == ) - - let hash = Hashtbl.hash (* TODO *) - end) in - let tbl = H.create 512 in - let rec size bdd = - match view bdd with - | False | True -> - 0 - | _ when H.mem tbl bdd -> - 0 - | Node (_, l, h) -> - H.add tbl bdd () ; - 1 + size l + size h - in - size - - let is_sat = fview (function False -> false | _ -> true) - - let count_sat maxn = - let get_var = - fview (function False | True -> maxn | Node (v, _, _) -> v) - in - let count = - Mem.memo (fun count -> - fview (function - | False -> - 0 - | True -> - 1 - | Node (v, l, h) -> - assert ( - (0 <= v && v < maxn) || (Printf.printf "v = %d\n" v ; false) - ) ; - (count l lsl (get_var l - v - 1)) - + (count h lsl (get_var h - v - 1)))) - in - fun bdd -> count bdd lsl get_var bdd - - let any_sat = - let rec aux assign = - fview (function - | False -> - None - | True -> - Some assign - | Node (v, l, h) -> ( - match aux assign l with - | None -> - aux ((v, true) :: assign) h - | Some assign -> - Some ((v, false) :: assign) )) - in - aux [] - - let all_sat bdd = - let add_assign v b = function - | None -> - None - | Some assign -> - Some ((v, b) :: assign) - in - let rec aux assign = - fview (function - | False -> - [None] - | True -> - [Some assign] - | Node (v, l, h) -> - let add_assign = add_assign v in - let aux = aux assign in - List.map (add_assign false) (aux l) - @ List.map (add_assign true) (aux h)) - in - List.fold_left - (fun acc -> function None -> acc | Some assign -> assign :: acc) - [] (aux [] bdd) - - (* TODO: in each assign, add all the unused vars. ? *) - - let random_sat _ = - (* let _ = count_sat maxn in *) - let rec aux assign = - fview (function - | False -> - None - | True -> - Some assign - | Node (v, l, h) -> ( - if is_sat l && is_sat h then - if true (* TODO *) then aux ((v, false) :: assign) h - else aux ((v, true) :: assign) l - else - match aux assign l with - | None -> - aux ((v, true) :: assign) h - | Some assign -> - Some ((v, false) :: assign) )) - in - aux [] -end diff --git a/src/bdd/dune b/src/bdd/dune deleted file mode 100644 index baef5f7..0000000 --- a/src/bdd/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name bdd) - (modules common hashconsed naive utils) - (preprocess - (pps bisect_ppx -conditional landmarks.ppx --auto)) - (libraries expr memo hc landmarks)) diff --git a/src/bdd/hashconsed.ml b/src/bdd/hashconsed.ml deleted file mode 100644 index c96cb16..0000000 --- a/src/bdd/hashconsed.ml +++ /dev/null @@ -1,44 +0,0 @@ -open Hc - -module Make (M : Memo.F) = struct - type hidden = view hash_consed - - and view = True | False | Node of Common.Base.var * hidden * hidden - - module HashedT = struct - type t = view - - let equal x y = - match (x, y) with - | True, True | False, False -> - true - | Node (v1, l1, r1), Node (v2, l2, r2) -> - v1 == v2 && l1 == l2 && r1 == r2 - | _ -> - false - - let hash = function - | True -> - 1 - | False -> - 0 - | Node (v, l, r) -> - (19 * ((19 * v) + l.tag)) + r.tag + 2 - end - - module Hbdd = Hc.Make (HashedT) - - module Hash = struct - type t = hidden - - let equal = ( == ) - - let hash b = b.tag - end - - let hc = Hbdd.hashcons - - let view x = x.node - - module Mem = M (Hash) -end diff --git a/src/bdd/naive.ml b/src/bdd/naive.ml deleted file mode 100644 index 4a43884..0000000 --- a/src/bdd/naive.ml +++ /dev/null @@ -1,19 +0,0 @@ -module Make (M : Memo.F) = struct - type hidden = view - - and view = True | False | Node of Common.Base.var * hidden * hidden - - module Hash = struct - type t = hidden - - let equal = ( = ) - - let hash = Hashtbl.hash - end - - let hc x = x - - let view x = x - - module Mem = M (Hash) -end diff --git a/src/bdd/utils.ml b/src/bdd/utils.ml deleted file mode 100644 index 2b38cfd..0000000 --- a/src/bdd/utils.ml +++ /dev/null @@ -1,3 +0,0 @@ -let gen_tag () = - let count = ref (-1) in - ((fun () -> incr count ; !count), fun () -> count := -1) diff --git a/src/dune b/src/dune new file mode 100644 index 0000000..e8f684d --- /dev/null +++ b/src/dune @@ -0,0 +1,5 @@ +(library + (name bdd) + (preprocess + (pps bisect_ppx -conditional)) + (libraries memo hc)) diff --git a/src/expr/cli.ml b/src/expr/cli.ml deleted file mode 100644 index 3c1d04d..0000000 --- a/src/expr/cli.ml +++ /dev/null @@ -1,17 +0,0 @@ -let get_expr () = - let f = ref None in - let e = ref None in - Arg.parse - [ ("-f", Arg.String (fun s -> f := Some s), "file") - ; ("-e", Arg.String (fun s -> e := Some s), "expression") ] - (fun _ -> ()) - "get_expr" ; - match (!e, !f) with - | Some _, Some _ -> - raise (Arg.Bad "file or expression, not both") - | Some e, _ -> - Comp.from_string e - | _, Some f -> - Comp.from_file f - | None, None -> - raise (Arg.Bad "file or expression needed") diff --git a/src/expr/comp.ml b/src/expr/comp.ml deleted file mode 100644 index 995972b..0000000 --- a/src/expr/comp.ml +++ /dev/null @@ -1,66 +0,0 @@ -exception Stop - -open Lang - -let from_lexing buf = - match Parser.expr_final Lexer.token buf with - | exception Lexer.Error msg -> - failwith ("lexer: " ^ msg) - | exception _ -> - let err_pos = Lexing.lexeme_start buf in - let err_line, line_offset = (ref 1, ref 0) in - ( try - List.iter - (fun x -> - if x > err_pos then raise Stop ; - incr err_line ; - line_offset := x) - (Lexer.get_mem_new_line ()) - with Stop -> () ) ; - failwith - (Printf.sprintf "parser: On line %d, at offset %d, syntax error." - !err_line (err_pos - !line_offset)) - | res -> - res - -let from_file f = - let chan = open_in f in - let buf = Lexing.from_channel chan in - let res = from_lexing buf in - close_in chan ; res - -let from_string s = - let buf = Lexing.from_string s in - from_lexing buf - -let list_to_conj l = Lang.BigAnd (List.to_seq l) - -let rec print fmt = function - | True -> - Format.fprintf fmt "true" - | False -> - Format.fprintf fmt "false" - | Var v -> - Format.fprintf fmt "@[%S@]" v - | Neg e -> - Format.fprintf fmt "(@[NOT %a@])" print e - | And (e1, e2) -> - Format.fprintf fmt "(@[%a AND@ %a@])" print e1 print e2 - | Or (e1, e2) -> - Format.fprintf fmt "(@[%a OR@ %a@])" print e1 print e2 - | Imp (e1, e2) -> - Format.fprintf fmt "(@[%a =>@ %a@])" print e1 print e2 - | Eq (e1, e2) -> - Format.fprintf fmt "(@[%a <=>@ %a@])" print e1 print e2 - | BigAnd s -> - Format.fprintf fmt "(@[%a@])" - (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt " AND@ ") - print) - (List.of_seq s) - | BigOr s -> - Format.fprintf fmt "(@[%a@])" - (Format.pp_print_list - ~pp_sep:(fun fmt () -> Format.fprintf fmt " OR@ ") - print) - (List.of_seq s) diff --git a/src/expr/dune b/src/expr/dune deleted file mode 100644 index 0fc021a..0000000 --- a/src/expr/dune +++ /dev/null @@ -1,12 +0,0 @@ -(library - (name expr) - (libraries landmarks) - (preprocess (pps landmarks.ppx --auto)) - (modules lang comp parser lexer cli)) - -(ocamllex - (modules lexer)) - -(menhir - (modules parser) - (flags ("--explain" "--dump"))) diff --git a/src/expr/lang.ml b/src/expr/lang.ml deleted file mode 100644 index 29ac7f3..0000000 --- a/src/expr/lang.ml +++ /dev/null @@ -1,15 +0,0 @@ -type var = string - -type t = - | True - | False - | Var of var - | Neg of t - | And of t * t - | Or of t * t - | Imp of t * t - | Eq of t * t - | BigAnd of t Seq.t - | BigOr of t Seq.t - -let var_to_string v = v diff --git a/src/expr/lexer.mll b/src/expr/lexer.mll deleted file mode 100644 index acc15e5..0000000 --- a/src/expr/lexer.mll +++ /dev/null @@ -1,68 +0,0 @@ -{ - open Parser - - exception Error of string - - let current_line = ref 1 - let current_offset = ref 1 - let total_offset = ref 1 - - let mem_new_line = ref [] - - let get_mem_new_line () = List.rev (!mem_new_line) - - let new_line_met () = - total_offset := !total_offset + 1; - mem_new_line := (!total_offset)::(!mem_new_line); - current_line := !current_line + 1; - current_offset := 0 - - let incr_offset x = - total_offset := !total_offset + x; - current_offset := !current_offset + x - - let incr_offset_string x = - incr_offset (String.length x) - - let parser_fail msg = - raise (Error (Printf.sprintf "Line %d, at offset %d: %s." (!current_line) (!current_offset) msg)) - - let read_kw kw = - incr_offset_string kw; - match kw with - | "false" -> FALSE - | "true" -> TRUE - | "(" -> LPAR - | ")" -> RPAR - | "!" -> NOT - | "&&" -> AND - | "||" -> OR - | "=>" -> IMP - | "<=>" -> EQ - | _ -> parser_fail "unknown keyword" -} - -let alpha = ['a'-'z' 'A'-'Z'] -let newline = ['\n' '\r'] -let blank = [' ' '\t'] -let digit = ['0'-'9'] -let int = digit+ -let ident = alpha (alpha|digit|'_')* - -rule token = parse - | newline { new_line_met (); token lexbuf } - | blank { incr_offset 1; token lexbuf } - | "/*" { incr_offset 2; comment lexbuf; token lexbuf } - | "false" | "true" | "(" | ")" | "!" | "&&" | "||" | "=>" | "<=>" as kw - { read_kw kw } - | int | ident as i { - incr_offset_string i; - VAR i } - | eof { EOF } - | _ { parser_fail "unexpected character" } - -and comment = parse - | "*/" { incr_offset 2; () } - | newline { new_line_met (); comment lexbuf } - | _ { incr_offset 1; comment lexbuf } - | eof { parser_fail "unterminated comment" } diff --git a/src/expr/parser.mly b/src/expr/parser.mly deleted file mode 100644 index 6516952..0000000 --- a/src/expr/parser.mly +++ /dev/null @@ -1,38 +0,0 @@ -%{ - open Lang -%} - -%token EOF -%token TRUE FALSE -%token VAR -%token NOT -%token AND OR -%token IMP EQ - -%token LPAR RPAR - -%left EQ -%left IMP -%left OR -%left AND -%left NOT - -%start expr_final - -%% -expr_final: -| e = expr EOF { e } - -expr: -| e = par(expr) { e } -| TRUE { True } -| FALSE { False } -| id = VAR { Var id } -| NOT e = expr { Neg e } -| e1 = expr AND e2 = expr { And (e1, e2) } -| e1 = expr OR e2 = expr { Or (e1, e2) } -| e1 = expr IMP e2 = expr { Imp (e1, e2) } -| e1 = expr EQ e2 = expr { Eq (e1, e2) } - -par(X): -| x = delimited(LPAR, X, RPAR) { x } diff --git a/src/memo/dune b/src/memo/dune deleted file mode 100644 index 6cfcc28..0000000 --- a/src/memo/dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name memo) - (libraries landmarks) - (preprocess (pps landmarks.ppx --auto)) - (modules memo)) diff --git a/src/memo/memo.ml b/src/memo/memo.ml deleted file mode 100644 index de3a60d..0000000 --- a/src/memo/memo.ml +++ /dev/null @@ -1,56 +0,0 @@ -module type S = sig - type t - - val memo : ((t -> 'a) -> t -> 'a) -> t -> 'a - - val memo2 : ((t -> t -> 'a) -> t -> t -> 'a) -> t -> t -> 'a -end - -module type F = functor (H : Hashtbl.HashedType) -> S with type t = H.t - -module Make (H : Hashtbl.HashedType) = struct - type t = H.t - - module Hash = Hashtbl.Make (H) - - let memo ff = - let tbl = Hash.create 512 in - let rec f k = - try Hash.find tbl k - with Not_found -> - let v = ff f k in - Hash.add tbl k v ; v - in - f - - module Hash2 = Hashtbl.Make (struct - type t = H.t * H.t - - let equal (x1, y1) (x2, y2) = H.equal x1 x2 && H.equal y1 y2 - - let hash (x, y) = (19 * H.hash x) + H.hash y - end) - - let memo2 ff = - let tbl = Hash2.create 512 in - let rec f k1 k2 = - try Hash2.find tbl (k1, k2) - with Not_found -> - let v = ff f k1 k2 in - Hash2.add tbl (k1, k2) v ; - v - in - f -end - -module Fake (H : Hashtbl.HashedType) = struct - type t = H.t - - let memo ff = - let rec f k = ff f k in - f - - let memo2 ff = - let rec f k1 k2 = ff f k1 k2 in - f -end diff --git a/tests/dune b/tests/dune deleted file mode 100644 index b7c78f2..0000000 --- a/tests/dune +++ /dev/null @@ -1,4 +0,0 @@ -(test - (name tests) - (modules tests) - (libraries bdd alcotest)) diff --git a/tests/tests.ml b/tests/tests.ml deleted file mode 100644 index c7e44ce..0000000 --- a/tests/tests.ml +++ /dev/null @@ -1,140 +0,0 @@ -module Make (M : Bdd.Common.S) = struct - module M = Bdd.Common.Make (M) - - let test s = - let tbl = Hashtbl.create 32 in - Hashtbl.add tbl (Bdd.Common.Base.var_of_string "t") true ; - Hashtbl.add tbl (Bdd.Common.Base.var_of_string "f") false ; - let compute x = M.to_string (M.compute tbl (M.of_string x)) in - let check_t x () = - Alcotest.(check string) "same string" "true" (compute x) - in - let check_f x () = - Alcotest.(check string) "same string" "false" (compute x) - in - let check_sat x () = Alcotest.(check bool) "same bool" true (M.is_sat x) in - let check_notsat x () = - Alcotest.(check bool) "same bool" false (M.is_sat x) - in - let check_countsat s n x () = - Alcotest.(check int) "same int" n (M.count_sat s x) - in - let f = - [ "false" - ; "!true" - ; "false && false" - ; "false && true" - ; "true && false" - ; "false || false" - ; "f" - ; "f && f" - ; "f && t" - ; "f || f" - ; "true => false" - ; "t => f" - ; " false <=> true" - ; " true <=> false" - ; " f <=> t" - ; " t <=> f" ] - in - let t = - [ "true" - ; "!false" - ; "true && true" - ; "true || false" - ; "false || true" - ; "true || true" - ; "t" - ; "t && t" - ; "t || f" - ; "f || t" - ; "t || t" - ; "false => false" - ; "false => true" - ; "true => true" - ; "f => f" - ; "f => t" - ; "t => t" - ; "false <=> false" - ; "true <=> true" - ; "f <=> f" - ; "t <=> t" ] - in - let matrix f t = - List.fold_left (fun acc f -> List.map (fun t -> (f, t)) t @ acc) [] f - in - let aux f x = - List.map - (fun x -> - Bdd.Common.Base.reset () ; - (x, `Quick, f x)) - x - in - let aux2 f x = - List.map - (fun (x, y) -> - Bdd.Common.Base.reset () ; - (x ^ " " ^ y, `Quick, f (x, y))) - x - in - let neg el = "!(" ^ el ^ ")" in - let negneg el = neg (neg el) in - let comb op x y = "(" ^ x ^ ") " ^ op ^ " (" ^ y ^ ")" in - let conj = comb "&&" in - let disj = comb "||" in - let set1 = aux check_f f in - let set2 = aux check_t t in - let set3 = aux (fun f -> neg f |> check_t) f in - let set4 = aux (fun t -> neg t |> check_f) t in - let set5 = aux (fun f -> negneg f |> check_f) f in - let set6 = aux (fun t -> negneg t |> check_t) t in - let set7 = aux2 (fun (x, y) -> conj x y |> check_f) (matrix f f) in - let set8 = aux2 (fun (x, y) -> conj x y |> check_f) (matrix f t) in - let set9 = aux2 (fun (x, y) -> conj x y |> check_f) (matrix t f) in - let set10 = aux2 (fun (x, y) -> conj x y |> check_t) (matrix t t) in - let set11 = aux2 (fun (x, y) -> disj x y |> check_f) (matrix f f) in - let set12 = aux2 (fun (x, y) -> disj x y |> check_t) (matrix f t) in - let set13 = aux2 (fun (x, y) -> disj x y |> check_t) (matrix t f) in - let set14 = aux2 (fun (x, y) -> disj x y |> check_t) (matrix t t) in - let sat = ["true"; "x"; "x && y"; "x => y"] in - let not_sat = ["false"; "x && (!x)"; "(x => y) && x && (!y)"] in - let set15 = aux (fun e -> M.of_string e |> check_sat) sat in - let set16 = aux (fun e -> M.of_string e |> check_notsat) not_sat in - let set17 = aux (fun e -> M.of_string e |> check_countsat 2 0) not_sat in - (* TODO: fix - let sat1 = [ "x && y"; "!(x => y)" ] in - let sat2 = [ "x && (y || (!y))"; "(x && y) || ((!x) && (!y))" ] in - let set18 = aux (fun e -> M.of_string e |> check_countsat 2 1) sat1 in - let set19 = aux (fun e -> M.of_string e |> check_countsat 2 2) sat2 in - *) - Alcotest.run ~and_exit:false s - [ ("false", set1) - ; ("true", set2) - ; ("neg false", set3) - ; ("neg true", set4) - ; ("negneg false", set5) - ; ("negneg true", set6) - ; ("conj false false", set7) - ; ("conj false true", set8) - ; ("conj true false", set9) - ; ("conj true true", set10) - ; ("disj false false", set11) - ; ("disj false true", set12) - ; ("disj true false", set13) - ; ("disj true true", set14) - ; ("sat", set15) - ; ("not sat", set16) - ; ("count sat 0", set17) - (* ; ("count sat 1", set18) - ; ("count_sat 2", set19) *) ] -end - -let _ = - let module T1 = Make (Bdd.Naive.Make (Memo.Fake)) in - let module T2 = Make (Bdd.Naive.Make (Memo.Make)) in - let module T3 = Make (Bdd.Hashconsed.Make (Memo.Fake)) in - let module T4 = Make (Bdd.Hashconsed.Make (Memo.Make)) in - T1.test "Naïve" ; - T2.test "Naïve + Memoïzation" ; - T3.test "Hashcons" ; - T4.test "Hashcons + Memoïzation"