remove a lot of stuff, clean code
This commit is contained in:
parent
bdbc5b9a28
commit
3f144c5c3b
@ -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.
|
||||
|
||||
|
62
README.md
62
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 <expression>
|
||||
```
|
||||
|
||||
A file containing an expression:
|
||||
|
||||
```sh
|
||||
scripts/bench.sh -f <file>
|
||||
```
|
||||
bdd is an OCaml library for Binary Decision Diagram
|
||||
|
||||
## Change Log
|
||||
|
||||
|
@ -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 ;
|
||||
()
|
@ -1,4 +0,0 @@
|
||||
(executable
|
||||
(name bench)
|
||||
(libraries unix bdd expr)
|
||||
(modules bench))
|
@ -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")))
|
@ -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" }
|
||||
|
@ -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 ;
|
||||
()
|
@ -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]
|
@ -1,23 +0,0 @@
|
||||
%{
|
||||
%}
|
||||
|
||||
%token EOF
|
||||
%token EOL
|
||||
%token BLANK
|
||||
%token <int> 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 }
|
@ -1,7 +0,0 @@
|
||||
xxx4xxx
|
||||
x3xx25x
|
||||
xxx31xx
|
||||
xxx5xxx
|
||||
xxxxxxx
|
||||
xx1xxxx
|
||||
2xxx4xx
|
@ -1 +0,0 @@
|
||||
1xxxxxxxx1
|
@ -1,2 +0,0 @@
|
||||
1x1
|
||||
2x2
|
@ -1,2 +0,0 @@
|
||||
1xxxx
|
||||
xxxx1
|
@ -1,2 +0,0 @@
|
||||
1xx
|
||||
xx1
|
@ -1 +0,0 @@
|
||||
1x1
|
@ -1 +0,0 @@
|
||||
11
|
@ -1,4 +0,0 @@
|
||||
123
|
||||
xx3
|
||||
xxx
|
||||
x12
|
@ -1,3 +0,0 @@
|
||||
1xx
|
||||
xxx
|
||||
xx1
|
@ -1,4 +0,0 @@
|
||||
(executable
|
||||
(name queen)
|
||||
(libraries expr bdd landmarks)
|
||||
(preprocess (pps landmarks.ppx --auto)))
|
@ -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) ^ " <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)
|
@ -1,9 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
eval "$(opam env)"
|
||||
dune exec src/bench.exe -- "$@"
|
||||
)
|
@ -1,7 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
eval "$(opam env)"
|
||||
dune build --profile release @all )
|
@ -1,7 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
eval "$(opam env)"
|
||||
dune clean )
|
@ -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 )
|
@ -1,8 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
eval "$(opam env)"
|
||||
dune build @install
|
||||
dune install bdd )
|
@ -1,8 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
eval "$(opam env)"
|
||||
export OCAML_LANDMARKS="output=landmarks.json,format=json,allocation"
|
||||
)
|
@ -1,9 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
eval "$(opam env)"
|
||||
dune exec src/numlink/numlink.exe --profile release -- "$@"
|
||||
)
|
@ -1,8 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
eval "$(opam env)"
|
||||
dune runtest --no-buffer )
|
@ -1,6 +0,0 @@
|
||||
#!/bin/sh
|
||||
|
||||
set -eu
|
||||
|
||||
( cd "$(dirname "$0")/../"
|
||||
( find . -type f -print0 | xargs -0 cat) | grep -r TODO )
|
267
src/bdd.ml
Normal file
267
src/bdd.ml
Normal file
@ -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 []
|
@ -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
|
@ -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))
|
@ -1,44 +0,0 @@
|
||||