zapashcanon/bdd
1
0
Fork 0
Code Issues Pull Requests Actions Releases Wiki Activity

format, change repo layout, new build manifest

Browse Source
This commit is contained in:
zapashcanon 2019-11-23 14:13:50 +01:00
parent 1bde58afce
commit 3a8adf98e6
Signed by: zapashcanon
GPG Key ID: 8981C3C62D1D28F1
30 changed files with 900 additions and 774 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

83
.build.yml Normal file
View File

@ -0,0 +1,83 @@
image: debian/unstable
packages:
- opam
- ocaml
- curl
sources:
- https://git.zapashcanon.fr/zapashcanon/bdd
environment:
name: bdd
deploy: fs@zapashcanon.fr
sshopts: "-o StrictHostKeyChecking=no -q"
coverage_dst: /var/www/coverage.zapashcanon.fr
doc_dst: /var/www/doc.zapashcanon.fr
archive_dst: /var/www/fs.zapashcanon.fr/archive
secrets:
- ec1f49cd-38dc-41d9-89f4-c3b6ecd7bcad # ssh deploy key
- b5b0e36c-fe52-43c4-9103-0aa918ad175c # github token
- c9e55d80-7b6a-4ad4-81bd-921d2c3247b8 # dune release profile
- ff8575b8-7192-4e0c-9905-6d04142a4ec1 # git config
tasks:
- setup: |
opam init -y
opam update -y
opam install -y dune bisect_ppx odoc ocamlformat
- lint-format: |
cd $name
eval "$(opam env)"
ocamlformat -p ocamlformat --enable-outside-detected-project --check $(find . -name '*.ml')
- build: |
cd $name
eval "$(opam env)"
dune build @all
- test: |
cd $name
eval "$(opam env)"
dune runtest
- deploy-doc: |
cd $name
eval "$(opam env)"
dune build @doc
ssh $sshopts $deploy "mkdir -p $doc_dst/$name/"
scp $sshopts -r _build/default/_doc/_html/* $deploy:$doc_dst/$name/
- deploy-coverage: |
cd $name
eval "$(opam env)"
dune clean
BISECT_ENABLE=YES dune runtest --no-buffer --force > /dev/null
bisect-ppx-report -html _coverage/ "$(find . -name 'bisect*.out')"
ssh $sshopts $deploy "mkdir -p $coverage_dst/$name/"
scp $sshopts -r _coverage/* $deploy:$coverage_dst/$name/
- archive: |
cd $name
eval "$(opam env)"
dune clean
archive_name=${name}-dev.tar.xz
git archive -o $archive_name HEAD
ssh $sshopts $deploy "mkdir -p $archive_dst/$name/"
scp $sshopts $archive_name $deploy:$archive_dst/$name/
rm $archive_name
- release: |
cd $name
eval "$(opam env)"
git describe --exact-match || exit 0
opam install -y dune-release
tag=$(git describe --exact-match)
dune-release distrib || true
archive_name=${name}-${tag}.tbz
ls _build/${archive_name}
scp $sshopts _build/${archive_name} $deploy:$archive_dst/$name/
url="https://fs.zapashcanon.fr/archive/${name}/${archive_name}"
echo $url > _build/${name}-${tag}.url
dune-release opam pkg
opam_file=_build/${name}.${tag}/opam
line_num="$(grep -n -e 'src:' $opam_file | cut -d: -f1)"
sed -i -e "${line_num}s|^.*| src: \"${url}\"|" $opam_file
line_num=$(($line_num + 1))
sed -i -e "${line_num}d" $opam_file
sed -i -e "${line_num}d" $opam_file
cd ..
echo -e "Host github.com\n\tStrictHostKeyChecking no\n" >> ~/.ssh/config
git clone https://github.com/Cameleo/opam-repository.git
cd $name
dune-release opam submit --no-auto-open -y

97
bench/bench.ml
View File

@ -1,16 +1,11 @@
module Make2 (M: Bdd.Common.S) = struct
module M = Bdd.Common.Make(M)
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
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 =
@ -18,78 +13,68 @@ module Make2 (M: Bdd.Common.S) = struct
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');
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)
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);
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 := !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);
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
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
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
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;
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 ;
()

13
build_manifest.yml
View File

@ -1,13 +0,0 @@
image: debian/unstable
packages:
- opam
sources:
- https://git.zapashcanon.fr/zapashcanon/bdd
tasks:
- setup: |
opam init -y -c 4.07.1
opam update -y
opam install -y dune menhir alcotest bisect_ppx
- build: |
cd bdd
scripts/build.sh

6
dune-project
View File

@ -1,3 +1,7 @@
(lang dune 1.6)
(lang dune 1.11)
(name bdd)
(using menhir 2.0)
(explicit_js_mode)

0
src/numlink/dune → examples/numlink/dune
View File

0
src/numlink/lexer.mll → examples/numlink/lexer.mll
View File

146
examples/numlink/main.ml Normal file
View File

@ -0,0 +1,146 @@
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 ;
()

127
src/numlink/numlink.ml → examples/numlink/numlink.ml
View File

@ -1,119 +1,117 @@
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 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 := i :: !res
done ;
!res
let filter_vertex s v =
Seq.filter (fun (el, _, _) -> el = v) s
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
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 for_all e f = E.BigAnd (Seq.map f e)
let exists e f =
E.BigOr (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)
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 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)))
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)))
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 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))
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 begin
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)))))
end
else E.True))
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 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;
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 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
@ -124,11 +122,4 @@ let build_expr (vertices, edges) to_connect =
(*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;
]
Expr.Comp.list_to_conj [c1; c2; c3; c4; c5]

0
src/numlink/parser.mly → examples/numlink/parser.mly
View File

0
test1.numlink → examples/numlink/test1.numlink
View File

0
test10.numlink → examples/numlink/test10.numlink
View File

0
test11.numlink → examples/numlink/test11.numlink
View File

0
test2.numlink → examples/numlink/test2.numlink
View File

0
test3.numlink → examples/numlink/test3.numlink
View File

0
test4.numlink → examples/numlink/test4.numlink
View File

0
test5.numlink → examples/numlink/test5.numlink
View File

0
test6.numlink → examples/numlink/test6.numlink
View File

0
test7.numlink → examples/numlink/test7.numlink
View File

0
src/queen/dune → examples/queen/dune
View File

173
src/queen/queen.ml → examples/queen/queen.ml
View File

@ -1,21 +1,21 @@
(**************************************************************************)
(* *)
(* 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))
(**************************************************************************)
(* *)
(* 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)
@ -28,71 +28,72 @@ include Bdd.Common.Make(Bdd.Hashconsed.Make(Memo.Make))
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) ^ " <size of the grid>")
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)
*)
let _ =
if Array.length Sys.argv <> 2 then
failwith ("Usage: " ^ Sys.argv.(0) ^ " <size of the grid>")
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)

413
src/bdd/common.ml
View File

@ -1,58 +1,57 @@
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;
( (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)
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
type view = True | False | Node of Base.var * hidden * hidden
val hc: view -> hidden
val view: hidden -> view
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
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 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 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 *)
@ -61,191 +60,259 @@ module Make (M: S) = struct
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 ")"
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
aux bdd ; Buffer.contents b
let of_bool = function
| true -> true_bdd
| false -> false_bdd
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 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_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 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 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 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 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
let module H = Hashtbl.Make (struct
type t = M.Hash.t
let equal = (==)
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 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 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 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 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)
| 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))
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)
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 maxn =
let _ = count_sat maxn in
let rec aux assign = fview (function
| False -> None
| True -> Some assign
| Node (v, l, h) -> begin
if is_sat l && is_sat h then begin
if true (* TODO *) then aux ((v, false) :: assign) h
else aux ((v, true) :: assign) l
end else match aux assign l with
| None -> aux ((v, true) :: assign) h
| Some assign -> Some ((v, false) :: assign)
end)
in aux []
(* 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

42
src/bdd/hashconsed.ml
View File

@ -1,34 +1,42 @@
open Hashcons
module Make(M: Memo.F) = struct
module Make (M : Memo.F) = struct
type hidden = view hash_consed
and view =
| True
| False
| Node of Common.Base.var * hidden * hidden
module Hbdd = Hashcons.Make(struct
and view = True | False | Node of Common.Base.var * hidden * hidden
module Hbdd = Hashcons.Make (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 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
| True ->
1
| False ->
0
| Node (v, l, r) ->
(19 * ((19 * v) + l.tag)) + r.tag + 2
end)
module Hash = struct
type t = hidden
let equal = (==)
let equal = ( == )
let hash b = b.tag
end
let hc = Hbdd.hashcons (Hbdd.create 256)
let view x = x.node
module Mem = M(Hash)
module Mem = M (Hash)
end

17
src/bdd/naive.ml
View File

@ -1,20 +1,19 @@
module Make(M: Memo.F) = struct
module Make (M : Memo.F) = struct
type hidden = view
and view =
| True
| False
| Node of Common.Base.var * hidden * hidden
and view = True | False | Node of Common.Base.var * hidden * hidden
module Hash = struct
type t = hidden
let equal = (=)
let equal = ( = )
let hash = Hashtbl.hash
end
let hc x = x
let view x = x
module Mem = M(Hash)
module Mem = M (Hash)
end

3
src/bdd/utils.ml
View File

@ -1,4 +1,3 @@
let gen_tag () =
let count = ref (-1) in
(fun () -> (incr count; !count)),
fun () -> count := -1
((fun () -> incr count ; !count), fun () -> count := -1)

26
src/expr/cli.ml
View File

@ -1,15 +1,17 @@
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")
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")

73
src/expr/comp.ml
View File

@ -1,51 +1,66 @@
exception Stop
open Lang
let from_lexing buf =
match Parser.expr_final Lexer.token buf with
| exception Lexer.Error msg -> failwith ("lexer: " ^ msg)
| 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 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
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 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
| 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 -> fun () -> Format.fprintf fmt " AND@ ")
print)
(List.of_seq s)
(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 -> fun () -> Format.fprintf fmt " OR@ ")
print) (List.of_seq s)
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " OR@ ")
print)
(List.of_seq s)

28
src/hashcons/hashcons.ml
View File

@ -1,34 +1,34 @@
type 'a hash_consed = {
node: 'a;
tag: int;
}
module Make(H: Hashtbl.HashedType) = struct
type 'a hash_consed = {node: 'a; tag: int}
module Make (H : Hashtbl.HashedType) = struct
type key = H.t
type data = key hash_consed
module E = Ephemeron.K1.Make(H)
module E = Ephemeron.K1.Make (H)
type t = data E.t
let create n =
let tbl = E.create n in
at_exit (fun () ->
Format.printf "alive bindings: %d@." (E.stats_alive tbl).num_bindings;
E.clean tbl;
Format.printf "alive bindings: %d@." (E.stats_alive tbl).num_bindings);
Format.printf "alive bindings: %d@." (E.stats_alive tbl).num_bindings ;
E.clean tbl ;
Format.printf "alive bindings: %d@." (E.stats_alive tbl).num_bindings) ;
tbl
let clear = E.clear
let iter = E.iter
let hashcons =
let gen =
let count = ref (-1) in
fun () -> incr count; !count
fun () -> incr count ; !count
in
fun tbl k ->
try E.find tbl k with
| Not_found -> let v = {tag = gen (); node = k} in
E.add tbl k v; v
try E.find tbl k
with Not_found ->
let v = {tag= gen (); node= k} in
E.add tbl k v ; v
end

43
src/memo/memo.ml
View File

@ -1,45 +1,56 @@
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
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 type F = functor (H : Hashtbl.HashedType) -> S with type t = H.t
module Make (H: Hashtbl.HashedType) = struct
module Make (H : Hashtbl.HashedType) = struct
type t = H.t
module Hash = Hashtbl.Make(H)
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
let v = ff f k in
Hash.add tbl k v ; v
in
f
module Hash2 = Hashtbl.Make(struct
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)
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
let v = ff f k1 k2 in
Hash2.add tbl (k1, k2) v ;
v
in
f
end
module Fake (H: Hashtbl.HashedType) = struct
module Fake (H : Hashtbl.HashedType) = struct
type t = H.t
let memo ff =
let rec f k =
ff f k
in f
let rec f k = ff f k in
f
let memo2 ff =
let rec f k1 k2 =
ff f k1 k2
in f
let rec f k1 k2 = ff f k1 k2 in
f
end

149
src/numlink/main.ml
View File

@ -1,149 +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
;
()

235
tests/tests.ml
View File

@ -1,84 +1,87 @@
module Make (M: Bdd.Common.S) = struct
module M = Bdd.Common.Make(M)
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 = fun () -> Alcotest.(check string) "same string" "true" (compute x) in
let check_f x = fun () -> Alcotest.(check string) "same string" "false" (compute x) in
let check_sat x = fun () -> Alcotest.(check bool) "same bool" true (M.is_sat x) in
let check_notsat x = fun () -> Alcotest.(check bool) "same bool" false (M.is_sat x) in
let check_countsat s n x = fun () -> 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
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
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
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
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
@ -93,69 +96,43 @@ module Make (M: Bdd.Common.S) = struct
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
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;
]
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
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";
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"