diff options
| -rw-r--r-- | test/Makefile | 2 | ||||
| -rw-r--r-- | test/Results/bdd.out | 1 | ||||
| -rw-r--r-- | test/bdd.ml | 210 |
3 files changed, 212 insertions, 1 deletions
diff --git a/test/Makefile b/test/Makefile index 0877f021b..10a5601da 100644 --- a/test/Makefile +++ b/test/Makefile @@ -11,7 +11,7 @@ CODERUNPARAMS=CAMLRUNPARAM='o=100' BYTE_EXE=fib.byt takc.byt taku.byt sieve.byt quicksort.byt quicksort.fast.byt \ fft.byt fft.fast.byt soli.byt soli.fast.byt boyer.byt kb.byt \ - nucleic.byt genlex.byt + nucleic.byt genlex.byt bdd.byt CODE_EXE=$(BYTE_EXE:.byt=.out) diff --git a/test/Results/bdd.out b/test/Results/bdd.out new file mode 100644 index 000000000..d86bac9de --- /dev/null +++ b/test/Results/bdd.out @@ -0,0 +1 @@ +OK diff --git a/test/bdd.ml b/test/bdd.ml new file mode 100644 index 000000000..50f1414ef --- /dev/null +++ b/test/bdd.ml @@ -0,0 +1,210 @@ +type bdd = One | Zero | Node of bdd * int * int * bdd + +let rec eval bdd vars = + match bdd with + Zero -> false + | One -> true + | Node(l, v, _, h) -> + if vars.(v) then eval h vars else eval l vars + +let rec getId bdd = + match bdd with + Node(_,_,id,_) -> id + | Zero -> 0 + | One -> 1 + +let initSize_1 = 8*1024 - 1 +let nodeC = ref 1 +let sz_1 = ref initSize_1 +let htab = ref(Array.create (!sz_1+1) []) +let n_items = ref 0 +let hashVal x y v = x lsl 1 + y + v lsl 2 + +let resize newSize = + let arr = !htab in + let newSz_1 = newSize-1 in + let newArr = Array.create newSize [] in + let rec copyBucket bucket = + match bucket with + [] -> () + | n ::ns -> + match n with + Node(l,v,_,h) -> + let ind = hashVal (getId l) (getId h) v land newSz_1 + in + newArr.(ind) <- (n :: newArr.(ind)); + copyBucket ns + in + for n = 0 to !sz_1 do + copyBucket(arr.(n)) + done; + htab := newArr; + sz_1 := newSz_1 + + +let rec insert idl idh v ind bucket newNode = + if !n_items <= !sz_1 + then ( (!htab).(ind) <- (newNode :: bucket); + incr n_items ) + else ( resize(!sz_1 + !sz_1 + 2); + let ind = hashVal idl idh v land (!sz_1) + in + (!htab).(ind) <- newNode :: (!htab).(ind) + ) + + +let resetUnique () = ( + sz_1 := initSize_1; + htab := Array.create (!sz_1+1) []; + n_items := 0; + nodeC := 1 + ) + +let mkNode low v high = + let idl = getId low in + let idh = getId high + in + if idl = idh + then low + else let ind = hashVal idl idh v land (!sz_1) in + let bucket = (!htab).(ind) in + let rec lookup b = + match b with + [] -> let n = Node(low, v, (incr nodeC; !nodeC), high) + in + insert (getId low) (getId high) v ind bucket n; n + | n :: ns -> + match n with + Node(l,v',id,h) -> if v=v' & idl=getId l & idh=getId h + then n else lookup ns + in + lookup bucket + + +type ordering = LESS | EQUAL | GREATER + +let cmpVar x y = if x<y then LESS else if x>y then GREATER else EQUAL + +let zero = Zero +let one = One + +let mkVar x = mkNode zero x one + + +let cacheSize = 1999 +let andslot1 = Array.create cacheSize 0 +let andslot2 = Array.create cacheSize 0 +let andslot3 = Array.create cacheSize zero +let xorslot1 = Array.create cacheSize 0 +let xorslot2 = Array.create cacheSize 0 +let xorslot3 = Array.create cacheSize zero +let notslot1 = Array.create cacheSize 0 +let notslot2 = Array.create cacheSize one +let hash x y = ((x lsl 1)+y) mod cacheSize + +let rec not n = +match n with + Zero -> One +| One -> Zero +| Node(l, v, id, r) -> let h = id mod cacheSize + in + if id=notslot1.(h) then notslot2.(h) + else let f = mkNode (not l) v (not r) + in + notslot1.(h) <- id; notslot2.(h) <- f; f + +let rec and2 n1 n2 = +match n1 with + Node(l1, v1, i1, r1) + -> (match n2 with + Node(l2, v2, i2, r2) + -> let h = hash i1 i2 + in + if i1=andslot1.(h) & i2=andslot2.(h) then andslot3.(h) + else let f = match cmpVar v1 v2 with + EQUAL -> mkNode (and2 l1 l2) v1 (and2 r1 r2) + | LESS -> mkNode (and2 l1 n2) v1 (and2 r1 n2) + | GREATER -> mkNode (and2 n1 l2) v2 (and2 n1 r2) + in + andslot1.(h) <- i1; + andslot2.(h) <- i2; + andslot3.(h) <- f; + f + | Zero -> Zero + | One -> n1) +| Zero -> Zero +| One -> n2 + + +let rec xor n1 n2 = +match n1 with + Node(l1, v1, i1, r1) + -> (match n2 with + Node(l2, v2, i2, r2) + -> let h = hash i1 i2 + in + if i1=andslot1.(h) & i2=andslot2.(h) then andslot3.(h) + else let f = match cmpVar v1 v2 with + EQUAL -> mkNode (xor l1 l2) v1 (xor r1 r2) + | LESS -> mkNode (xor l1 n2) v1 (xor r1 n2) + | GREATER -> mkNode (xor n1 l2) v2 (xor n1 r2) + in + andslot1.(h) <- i1; + andslot2.(h) <- i2; + andslot3.(h) <- f; + f + | Zero -> n1 + | One -> not n1) +| Zero -> n2 +| One -> not n2 + +let hwb n = + let rec h i j = if i=j + then mkVar i + else xor (and2 (not(mkVar j)) (h i (j-1))) + (and2 (mkVar j) (g i (j-1))) + and g i j = if i=j + then mkVar i + else xor (and2 (not(mkVar i)) (h (i+1) j)) + (and2 (mkVar i) (g (i+1) j)) + in + h 1 n + +(* Testing *) +let seed = ref 0 + +let random() = + seed := !seed * 25173 + 17431; !seed land 1 > 0 + +let random_vars n = + let vars = Array.create n false in + for i = 0 to n - 1 do vars.(i) <- random() done; + vars + +let test_hwb bdd vars = + (* We should have + eval bdd vars = vars.(n) if n > 0 + eval bdd vars = 0 if n = 0 + where n is the number of "true" elements in vars. *) + let ntrue = ref 0 in + for i = 0 to Array.length vars - 1 do + if vars.(i) then incr ntrue + done; + eval bdd vars = (if !ntrue > 0 then vars.(!ntrue) else false) + +let main () = + let n = + if Array.length Sys.argv >= 2 then int_of_string Sys.argv.(1) else 20 in + let ntests = + if Array.length Sys.argv >= 3 then int_of_string Sys.argv.(2) else 50 in + let bdd = hwb n in + let succeeded = ref true in + for i = 1 to ntests do + succeeded := !succeeded || test_hwb bdd (random_vars n) + done; + if !succeeded + then print_string "OK\n" + else print_string "FAILED\n"; + exit 0 + +let _ = main() |