-
Notifications
You must be signed in to change notification settings - Fork 2
/
test.ml
156 lines (139 loc) · 4.27 KB
/
test.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
(**************************************************************************************)
(* Copyright (C) 2009 Pietro Abate <[email protected]> *)
(* *)
(* This library is free software: you can redistribute it and/or modify *)
(* it under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of the *)
(* License, or (at your option) any later version. A special linking *)
(* exception to the GNU Lesser General Public License applies to this *)
(* library, see the COPYING file for more information. *)
(**************************************************************************************)
open OUnit
let reverse = Hashtbl.create 17 ;;
let add_vars =
List.iter (fun v ->
let i = Buddy.bdd_newvar () in
Hashtbl.add reverse v i
)
;;
let builder (vars,clauses) =
add_vars vars;
let bl =
List.map (fun l ->
List.map (function
|(v,true) -> Buddy.bdd_pos (Hashtbl.find reverse v)
|(v,false) -> Buddy.bdd_neg (Hashtbl.find reverse v)
) l
) clauses
in
Buddy.bdd_bigand (List.map Buddy.bdd_bigor bl)
;;
module S = Set.Make(
struct
type t = (Buddy.var * Buddy.value)
let compare = compare
end
)
let bdd_allsat_test () =
Buddy.bdd_init ();
Hashtbl.clear reverse ;
let bdd = builder (["a";"b"],[[("a",true)];[("b",true)]]) in
let tt_test = ref [] in
let f bdd =
let ch l =
tt_test := (List.sort compare l) :: !tt_test ;
(* List.iter (fun (var,value) ->
Printf.printf "%d = %s\n" var (Buddy.string_of_value(value))
) l;
Printf.printf "\n";
*)
in
(* Buddy.bdd_fprintset stdout bdd; *)
Buddy.bdd_allsat ch bdd;
assert_equal true true
in
f bdd;
Buddy.bdd_done ()
;;
let bdd_satoneset_test () =
Buddy.bdd_init ();
Hashtbl.clear reverse ;
let bdd = builder (["a";"b"],[[("a",true)];[("b",true)]]) in
let f bdd =
let b = Buddy.bdd_satoneset bdd [Hashtbl.find reverse "b"] in
(* Buddy.bdd_fprintdot stdout b; *)
assert_equal true true
in
f bdd ;
Buddy.bdd_done ()
;;
let bdd_satone_test () =
Buddy.bdd_init ();
Hashtbl.clear reverse ;
let bdd = builder (["a";"b"],[[("a",true)];[("b",true)]]) in
Buddy.bdd_fprintdot stdout (Buddy.bdd_restrict bdd (Buddy.bdd_pos (Hashtbl.find reverse "b")));
Buddy.bdd_fprintdot stdout (Buddy.bdd_low bdd);
Buddy.bdd_fprintdot stdout (Buddy.bdd_high bdd);
let f bdd =
let b = Buddy.bdd_satone bdd in
(* Buddy.bdd_fprintdot stdout b; *)
assert_equal true true
in
f bdd ;
Buddy.bdd_done ()
;;
let bdd_bigand_test () =
Buddy.bdd_init ();
Hashtbl.clear reverse ;
let vars = ["a";"b"] in
add_vars vars;
let v = List.map (fun v -> Buddy.bdd_pos (Hashtbl.find reverse v)) vars in
let bdd = Buddy.bdd_bigand v in
assert_equal true true;
Buddy.bdd_done ()
;;
let bdd_bigor_test () =
Buddy.bdd_init ();
Hashtbl.clear reverse ;
let vars = ["a";"b"] in
add_vars vars;
let v = List.map (fun v -> Buddy.bdd_pos (Hashtbl.find reverse v)) vars in
let bdd = Buddy.bdd_bigor v in
assert_equal true true;
Buddy.bdd_done ()
;;
let bdd_setvarorder_test () =
Buddy.bdd_init ();
Hashtbl.clear reverse ;
let vars = ["a";"b"] in
let bdd = builder (["a";"b"],[[("a",true)];[("b",true)]]) in
(* add_vars vars; *)
let v = List.map (Hashtbl.find reverse) vars in
(* print_endline "-----------1";
Buddy.bdd_fprintorder stdout ;
Buddy.bdd_fprintdot stdout bdd;
print_endline "-----------2";
ignore(Buddy.bdd_satone bdd);
Buddy.bdd_setvarorder (List.rev v);
print_endline "-----------3";
Buddy.bdd_fprintorder stdout ;
Buddy.bdd_fprintdot stdout bdd;
print_endline "-----------4";
*)
assert_equal true true;
Buddy.bdd_done ()
;;
let all =
"all tests" >::: [
"bdd_bigand" >:: bdd_satone_test;
"bdd_bigor" >:: bdd_bigor_test;
"bdd_makeset" >:: (fun _ -> todo "");
"bdd_satone" >:: bdd_satone_test;
"bdd_satoneset" >:: bdd_satoneset_test;
"bdd_allsat" >:: bdd_allsat_test;
"bdd_setvarorder" >:: bdd_setvarorder_test;
]
let main () =
OUnit.run_test_tt_main all
;;
main ()