Skip to content

Commit

Permalink
Add .ocamlformat, run dune fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
mattxwang committed Sep 20, 2023
1 parent 1c9b531 commit 9bb86e3
Show file tree
Hide file tree
Showing 5 changed files with 139 additions and 54 deletions.
2 changes: 2 additions & 0 deletions .ocamlformat
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
profile = default
version = 0.26.0
1 change: 1 addition & 0 deletions dune
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
(dirs :standard \ target)

(data_only_dirs vendor)
88 changes: 65 additions & 23 deletions src/rsdd.ml
Original file line number Diff line number Diff line change
Expand Up @@ -12,26 +12,68 @@ type rsdd_var_label
type rsdd_wmc_params_r
type rsdd_expected_utility
type rsdd_wmc_params_e_u
external mk_bdd_builder_default_order: int64 -> rsdd_bdd_builder = "mk_bdd_builder_default_order"
external bdd_new_var: rsdd_bdd_builder -> bool -> (int64 * rsdd_bdd_ptr) = "bdd_new_var"
external bdd_ite: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_ite"
external bdd_and: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_and"
external bdd_or: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_or"
external bdd_negate: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_negate"
external bdd_true: rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_true"
external bdd_false: rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_false"
external bdd_is_true: rsdd_bdd_ptr -> bool = "bdd_is_true"
external bdd_is_false: rsdd_bdd_ptr -> bool = "bdd_is_false"
external bdd_is_const: rsdd_bdd_ptr -> bool = "bdd_is_const"
external bdd_eq: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> bool = "bdd_eq"
external bdd_topvar: rsdd_bdd_ptr -> int64 = "bdd_topvar"
external bdd_low: rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_low"
external bdd_high: rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_high"
external bdd_wmc: rsdd_bdd_ptr -> rsdd_wmc_params_r -> float = "bdd_wmc"
external new_wmc_params_r: (float * float) list -> rsdd_wmc_params_r = "new_wmc_params_r"
external bdd_bb: rsdd_bdd_ptr -> rsdd_var_label list -> int64 -> rsdd_wmc_params_e_u -> rsdd_expected_utility * rsdd_partial_model = "bdd_bb"
external bdd_meu: rsdd_bdd_ptr -> rsdd_var_label list -> int64 -> rsdd_wmc_params_e_u -> rsdd_expected_utility * rsdd_partial_model = "bdd_meu"
external new_wmc_params_eu: ((float * float) * (float * float)) list -> rsdd_wmc_params_e_u = "new_wmc_params_eu"
external cnf_from_dimacs: string -> rsdd_cnf = "cnf_from_dimacs"
external bdd_builder_compile_cnf: rsdd_bdd_builder -> rsdd_cnf -> rsdd_bdd_ptr = "bdd_builder_compile_cnf"
external bdd_model_count: rsdd_bdd_builder -> rsdd_bdd_ptr -> int64 = "bdd_model_count"

external mk_bdd_builder_default_order : int64 -> rsdd_bdd_builder
= "mk_bdd_builder_default_order"

external bdd_new_var : rsdd_bdd_builder -> bool -> int64 * rsdd_bdd_ptr
= "bdd_new_var"

external bdd_ite :
rsdd_bdd_builder ->
rsdd_bdd_ptr ->
rsdd_bdd_ptr ->
rsdd_bdd_ptr ->
rsdd_bdd_ptr = "bdd_ite"

external bdd_and :
rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_and"

external bdd_or :
rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_or"

external bdd_negate : rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr
= "bdd_negate"

external bdd_true : rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_true"
external bdd_false : rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_false"
external bdd_is_true : rsdd_bdd_ptr -> bool = "bdd_is_true"
external bdd_is_false : rsdd_bdd_ptr -> bool = "bdd_is_false"
external bdd_is_const : rsdd_bdd_ptr -> bool = "bdd_is_const"

external bdd_eq : rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> bool
= "bdd_eq"

external bdd_topvar : rsdd_bdd_ptr -> int64 = "bdd_topvar"
external bdd_low : rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_low"
external bdd_high : rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_high"
external bdd_wmc : rsdd_bdd_ptr -> rsdd_wmc_params_r -> float = "bdd_wmc"

external new_wmc_params_r : (float * float) list -> rsdd_wmc_params_r
= "new_wmc_params_r"

external bdd_bb :
rsdd_bdd_ptr ->
rsdd_var_label list ->
int64 ->
rsdd_wmc_params_e_u ->
rsdd_expected_utility * rsdd_partial_model = "bdd_bb"

external bdd_meu :
rsdd_bdd_ptr ->
rsdd_var_label list ->
int64 ->
rsdd_wmc_params_e_u ->
rsdd_expected_utility * rsdd_partial_model = "bdd_meu"

external new_wmc_params_eu :
((float * float) * (float * float)) list -> rsdd_wmc_params_e_u
= "new_wmc_params_eu"

external cnf_from_dimacs : string -> rsdd_cnf = "cnf_from_dimacs"

external bdd_builder_compile_cnf : rsdd_bdd_builder -> rsdd_cnf -> rsdd_bdd_ptr
= "bdd_builder_compile_cnf"

external bdd_model_count : rsdd_bdd_builder -> rsdd_bdd_ptr -> int64
= "bdd_model_count"
88 changes: 65 additions & 23 deletions src/rsdd.mli
Original file line number Diff line number Diff line change
Expand Up @@ -12,26 +12,68 @@ type rsdd_var_label
type rsdd_wmc_params_r
type rsdd_expected_utility
type rsdd_wmc_params_e_u
external mk_bdd_builder_default_order: int64 -> rsdd_bdd_builder = "mk_bdd_builder_default_order"
external bdd_new_var: rsdd_bdd_builder -> bool -> (int64 * rsdd_bdd_ptr) = "bdd_new_var"
external bdd_ite: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_ite"
external bdd_and: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_and"
external bdd_or: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_or"
external bdd_negate: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_negate"
external bdd_true: rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_true"
external bdd_false: rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_false"
external bdd_is_true: rsdd_bdd_ptr -> bool = "bdd_is_true"
external bdd_is_false: rsdd_bdd_ptr -> bool = "bdd_is_false"
external bdd_is_const: rsdd_bdd_ptr -> bool = "bdd_is_const"
external bdd_eq: rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> bool = "bdd_eq"
external bdd_topvar: rsdd_bdd_ptr -> int64 = "bdd_topvar"
external bdd_low: rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_low"
external bdd_high: rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_high"
external bdd_wmc: rsdd_bdd_ptr -> rsdd_wmc_params_r -> float = "bdd_wmc"
external new_wmc_params_r: (float * float) list -> rsdd_wmc_params_r = "new_wmc_params_r"
external bdd_bb: rsdd_bdd_ptr -> rsdd_var_label list -> int64 -> rsdd_wmc_params_e_u -> rsdd_expected_utility * rsdd_partial_model = "bdd_bb"
external bdd_meu: rsdd_bdd_ptr -> rsdd_var_label list -> int64 -> rsdd_wmc_params_e_u -> rsdd_expected_utility * rsdd_partial_model = "bdd_meu"
external new_wmc_params_eu: ((float * float) * (float * float)) list -> rsdd_wmc_params_e_u = "new_wmc_params_eu"
external cnf_from_dimacs: string -> rsdd_cnf = "cnf_from_dimacs"
external bdd_builder_compile_cnf: rsdd_bdd_builder -> rsdd_cnf -> rsdd_bdd_ptr = "bdd_builder_compile_cnf"
external bdd_model_count: rsdd_bdd_builder -> rsdd_bdd_ptr -> int64 = "bdd_model_count"

external mk_bdd_builder_default_order : int64 -> rsdd_bdd_builder
= "mk_bdd_builder_default_order"

external bdd_new_var : rsdd_bdd_builder -> bool -> int64 * rsdd_bdd_ptr
= "bdd_new_var"

external bdd_ite :
rsdd_bdd_builder ->
rsdd_bdd_ptr ->
rsdd_bdd_ptr ->
rsdd_bdd_ptr ->
rsdd_bdd_ptr = "bdd_ite"

external bdd_and :
rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_and"

external bdd_or :
rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_or"

external bdd_negate : rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr
= "bdd_negate"

external bdd_true : rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_true"
external bdd_false : rsdd_bdd_builder -> rsdd_bdd_ptr = "bdd_false"
external bdd_is_true : rsdd_bdd_ptr -> bool = "bdd_is_true"
external bdd_is_false : rsdd_bdd_ptr -> bool = "bdd_is_false"
external bdd_is_const : rsdd_bdd_ptr -> bool = "bdd_is_const"

external bdd_eq : rsdd_bdd_builder -> rsdd_bdd_ptr -> rsdd_bdd_ptr -> bool
= "bdd_eq"

external bdd_topvar : rsdd_bdd_ptr -> int64 = "bdd_topvar"
external bdd_low : rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_low"
external bdd_high : rsdd_bdd_ptr -> rsdd_bdd_ptr = "bdd_high"
external bdd_wmc : rsdd_bdd_ptr -> rsdd_wmc_params_r -> float = "bdd_wmc"

external new_wmc_params_r : (float * float) list -> rsdd_wmc_params_r
= "new_wmc_params_r"

external bdd_bb :
rsdd_bdd_ptr ->
rsdd_var_label list ->
int64 ->
rsdd_wmc_params_e_u ->
rsdd_expected_utility * rsdd_partial_model = "bdd_bb"

external bdd_meu :
rsdd_bdd_ptr ->
rsdd_var_label list ->
int64 ->
rsdd_wmc_params_e_u ->
rsdd_expected_utility * rsdd_partial_model = "bdd_meu"

external new_wmc_params_eu :
((float * float) * (float * float)) list -> rsdd_wmc_params_e_u
= "new_wmc_params_eu"

external cnf_from_dimacs : string -> rsdd_cnf = "cnf_from_dimacs"

external bdd_builder_compile_cnf : rsdd_bdd_builder -> rsdd_cnf -> rsdd_bdd_ptr
= "bdd_builder_compile_cnf"

external bdd_model_count : rsdd_bdd_builder -> rsdd_bdd_ptr -> int64
= "bdd_model_count"
14 changes: 6 additions & 8 deletions test/test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,9 @@ open Rsdd

let () =
let robdd_builder = mk_bdd_builder_default_order 6L in
let bdd = bdd_builder_compile_cnf robdd_builder (cnf_from_dimacs "
p cnf 6 3\n\
1 2 3 4 0\n\
-2 -3 4 5 0\n\
-4 -5 6 6 0\n\
") in
let model_count = bdd_model_count robdd_builder bdd in
print_endline (Int64.to_string model_count)
let bdd =
bdd_builder_compile_cnf robdd_builder
(cnf_from_dimacs "\n p cnf 6 3\n1 2 3 4 0\n-2 -3 4 5 0\n-4 -5 6 6 0\n")
in
let model_count = bdd_model_count robdd_builder bdd in
print_endline (Int64.to_string model_count)

0 comments on commit 9bb86e3

Please sign in to comment.