66 lines
2.2 KiB
OCaml
66 lines
2.2 KiB
OCaml
open Bdd
|
|
|
|
let _ =
|
|
let order = get_order true_bdd in
|
|
assert (order = -1) ;
|
|
let order = get_order false_bdd in
|
|
assert (order = -1) ;
|
|
let one_var = var_bdd 0 in
|
|
assert (get_order one_var = 0) ;
|
|
assert (to_string one_var = "0 ? (true) : (false)") ;
|
|
assert (of_bool true == true_bdd) ;
|
|
assert (of_bool false == false_bdd) ;
|
|
assert (neg true_bdd == false_bdd) ;
|
|
assert (neg false_bdd == true_bdd) ;
|
|
assert (to_string (neg one_var) = "0 ? (false) : (true)") ;
|
|
let bdd = conj true_bdd true_bdd in
|
|
assert (bdd == true_bdd) ;
|
|
let bdd = disj false_bdd true_bdd in
|
|
assert (bdd == true_bdd) ;
|
|
let bdd = disj false_bdd one_var in
|
|
assert (bdd == one_var) ;
|
|
let bdd = imp false_bdd true_bdd in
|
|
assert (bdd == true_bdd) ;
|
|
let bdd = imp true_bdd false_bdd in
|
|
assert (bdd == false_bdd) ;
|
|
let bdd = eq false_bdd true_bdd in
|
|
assert (bdd == false_bdd) ;
|
|
let tbl = Hashtbl.create 32 in
|
|
Hashtbl.add tbl 0 true ;
|
|
assert (compute tbl one_var == true_bdd) ;
|
|
Hashtbl.replace tbl 0 false ;
|
|
assert (compute tbl one_var == false_bdd) ;
|
|
Hashtbl.clear tbl ;
|
|
assert (compute tbl one_var == one_var) ;
|
|
assert (size true_bdd = 0) ;
|
|
assert (size false_bdd = 0) ;
|
|
assert (size one_var = 1) ;
|
|
let one_var' = var_bdd 1 in
|
|
let bdd = node 2 one_var' one_var in
|
|
assert (size bdd = 2) ;
|
|
assert (is_sat true_bdd = true) ;
|
|
assert (is_sat false_bdd = false) ;
|
|
assert (is_sat bdd = true) ;
|
|
assert (count_sat 42 false_bdd = 0) ;
|
|
assert (count_sat 0 true_bdd = 1) ;
|
|
assert (count_sat 1 true_bdd = 2) ;
|
|
assert (count_sat 2 true_bdd = 4) ;
|
|
assert (count_sat 1 one_var = 1) ;
|
|
assert (count_sat 2 one_var' = 2) ;
|
|
assert (count_sat 3 bdd = 4) ;
|
|
assert (count_sat 4 bdd = 8) ;
|
|
assert (any_sat false_bdd = None) ;
|
|
assert (any_sat true_bdd = Some []) ;
|
|
assert (any_sat one_var = Some [(0, true)]) ;
|
|
( match any_sat bdd with
|
|
| None ->
|
|
assert false
|
|
| Some assign ->
|
|
assert (
|
|
List.sort compare assign = [(0, true); (2, true)]
|
|
|| List.sort compare assign = [(1, true); (2, false)] ) ) ;
|
|
assert (
|
|
List.sort compare (List.map (fun el -> List.sort compare el) (all_sat bdd))
|
|
= [[(0, true); (2, true)]; [(1, true); (2, false)]] ) ;
|
|
Format.printf "Tests are OK !@."
|