From b599d9cf50e0b54a31ae923bed7a5b5919e58afc Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Wed, 31 Dec 2025 13:23:48 +0100 Subject: [PATCH 1/8] Expose more CUDD BDD methods --- NAMESPACE | 49 +++ R/cudd_bdd.R | 16 + R/cudd_bdd_methods.R | 476 +++++++++++++++++++++++++++++ inst/examples/bdd_reduce_example.R | 27 ++ man/cudd_bdd_methods.Rd | 179 +++++++++++ man/cudd_bdd_restrict.Rd | 19 ++ src/cudd_manager.cpp | 420 +++++++++++++++++++++++++ src/rcudd.h | 49 +++ src/register.cpp | 49 +++ 9 files changed, 1284 insertions(+) create mode 100644 R/cudd_bdd_methods.R create mode 100644 inst/examples/bdd_reduce_example.R create mode 100644 man/cudd_bdd_methods.Rd create mode 100644 man/cudd_bdd_restrict.Rd diff --git a/NAMESPACE b/NAMESPACE index 42a5697..759cd09 100644 --- a/NAMESPACE +++ b/NAMESPACE @@ -16,21 +16,70 @@ export(cudd_autodyn_disable_zdd) export(cudd_autodyn_enable) export(cudd_autodyn_enable_zdd) export(cudd_background) +export(cudd_bdd_and_abstract) +export(cudd_bdd_and_limit) export(cudd_bdd_bind_var) +export(cudd_bdd_boolean_diff) +export(cudd_bdd_c_projection) +export(cudd_bdd_cofactor) +export(cudd_bdd_compose) +export(cudd_bdd_constrain) +export(cudd_bdd_decreasing) export(cudd_bdd_dump_dot) export(cudd_bdd_epd_print_minterm) +export(cudd_bdd_eval) +export(cudd_bdd_exist_abstract) +export(cudd_bdd_factored_form_string) +export(cudd_bdd_increasing) +export(cudd_bdd_interpolate) +export(cudd_bdd_intersect) +export(cudd_bdd_is_var) +export(cudd_bdd_is_zero) +export(cudd_bdd_isop) +export(cudd_bdd_ite) +export(cudd_bdd_ite_constant) +export(cudd_bdd_leq) +export(cudd_bdd_li_compaction) +export(cudd_bdd_literal_set_intersection) +export(cudd_bdd_make_prime) +export(cudd_bdd_min_hamming_dist) +export(cudd_bdd_minimize) +export(cudd_bdd_nand) +export(cudd_bdd_nor) export(cudd_bdd_one) +export(cudd_bdd_or_limit) +export(cudd_bdd_permute) +export(cudd_bdd_pick_one_cube) +export(cudd_bdd_pick_one_minterm) +export(cudd_bdd_port_to_zdd) +export(cudd_bdd_print_cover) +export(cudd_bdd_print_cover_with_cube) export(cudd_bdd_print_debug) +export(cudd_bdd_print_factored_form) export(cudd_bdd_print_minterm) export(cudd_bdd_realign_disable) export(cudd_bdd_realign_enable) export(cudd_bdd_realignment_enabled) +export(cudd_bdd_restrict) +export(cudd_bdd_squeeze) +export(cudd_bdd_subset_compress) +export(cudd_bdd_subset_heavy_branch) +export(cudd_bdd_subset_short_paths) +export(cudd_bdd_superset_compress) +export(cudd_bdd_superset_heavy_branch) +export(cudd_bdd_superset_short_paths) +export(cudd_bdd_swap_variables) export(cudd_bdd_to_add) export(cudd_bdd_to_zdd) export(cudd_bdd_truth_table) export(cudd_bdd_unbind_var) +export(cudd_bdd_univ_abstract) export(cudd_bdd_var) export(cudd_bdd_var_is_bound) +export(cudd_bdd_var_is_dependent) +export(cudd_bdd_vector_compose) +export(cudd_bdd_xnor) +export(cudd_bdd_xor_exist_abstract) export(cudd_bdd_zero) export(cudd_clear_error_code) export(cudd_clear_variable_names) diff --git a/R/cudd_bdd.R b/R/cudd_bdd.R index 4044e8b..d19e975 100644 --- a/R/cudd_bdd.R +++ b/R/cudd_bdd.R @@ -135,6 +135,22 @@ setMethod("^", signature(e1 = "CuddBDD", e2 = "CuddBDD"), function(e1, e2) { return(methods::new("CuddBDD", ptr = ptr, manager_ptr = .cudd_bdd_manager_ptr(e1))) }) +#' Restrict a BDD with a constraint +#' +#' Applies the CUDD `Restrict` operator to reduce a BDD given a constraint BDD. +#' +#' @param bdd A [`CuddBDD`] instance to restrict. +#' @param constraint A [`CuddBDD`] instance expressing the restriction. +#' @return A [`CuddBDD`] instance. +#' @export +cudd_bdd_restrict <- function(bdd, constraint) { + if (!.cudd_check_same_manager(bdd, constraint, "Restrict")) { + stop("Cannot restrict BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_restrict, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(constraint)) + return(methods::new("CuddBDD", ptr = ptr, manager_ptr = .cudd_bdd_manager_ptr(bdd))) +} + #' Print an EPD minterm count for a BDD #' #' This uses the CUDD `EpdPrintMinterm` implementation, which writes to R's diff --git a/R/cudd_bdd_methods.R b/R/cudd_bdd_methods.R new file mode 100644 index 0000000..fc82aac --- /dev/null +++ b/R/cudd_bdd_methods.R @@ -0,0 +1,476 @@ +.cudd_bdd_wrap <- function(ptr, bdd) { + return(methods::new("CuddBDD", ptr = ptr, manager_ptr = .cudd_bdd_manager_ptr(bdd))) +} + +.cudd_check_bdd_list_manager <- function(bdd, vars, op) { + for (var in vars) { + if (!.cudd_check_same_manager(bdd, var, op)) { + return(FALSE) + } + } + return(TRUE) +} + +.cudd_zdd_wrap <- function(ptr, bdd) { + return(methods::new("CuddZDD", ptr = ptr, manager_ptr = .cudd_bdd_manager_ptr(bdd))) +} + +#' Additional BDD methods +#' +#' Convenience wrappers for additional methods on CUDD BDD objects. +#' +#' @param bdd A [`CuddBDD`] instance. +#' @param other,cube,var,g,h,upper Additional [`CuddBDD`] instances used by the +#' operation. +#' @param limit Optional non-negative integer limit passed to CUDD. +#' @param index Integer index values used by the operation. +#' @param permut Integer vector describing a variable permutation. +#' @param x,y,vector,vars Lists of [`CuddBDD`] instances. +#' @param nvars,num_vars,threshold Non-negative integer values used by the operation. +#' @param minterm,inputs Integer vectors used by the operation. +#' @param upper_bound Integer upper bound for min hamming distance. +#' @param hardlimit Logical scalar for short path routines. +#' @return A [`CuddBDD`] instance, a logical scalar, numeric scalar, character +#' scalar, or list depending on the operation. +#' @name cudd_bdd_methods +NULL + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_is_zero <- function(bdd) { + return(.Call(c_cudd_bdd_is_zero, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_is_var <- function(bdd) { + return(.Call(c_cudd_bdd_is_var, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_leq <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Leq")) { + stop("Cannot compare BDDs from different CuddManager instances.", call. = FALSE) + } + return(.Call(c_cudd_bdd_leq, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_and_abstract <- function(bdd, other, cube, limit = 0L) { + if (!.cudd_check_same_manager(bdd, other, "AndAbstract") || + !.cudd_check_same_manager(bdd, cube, "AndAbstract")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_and_abstract, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(other), + .cudd_bdd_ptr(cube), + limit + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_exist_abstract <- function(bdd, cube, limit = 0L) { + if (!.cudd_check_same_manager(bdd, cube, "ExistAbstract")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_exist_abstract, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(cube), limit) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_univ_abstract <- function(bdd, cube) { + if (!.cudd_check_same_manager(bdd, cube, "UnivAbstract")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_univ_abstract, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(cube)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_xor_exist_abstract <- function(bdd, other, cube) { + if (!.cudd_check_same_manager(bdd, other, "XorExistAbstract") || + !.cudd_check_same_manager(bdd, cube, "XorExistAbstract")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_xor_exist_abstract, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(other), + .cudd_bdd_ptr(cube) + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_boolean_diff <- function(bdd, index) { + ptr <- .Call(c_cudd_bdd_boolean_diff, .cudd_bdd_ptr(bdd), index) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_var_is_dependent <- function(bdd, var) { + if (!.cudd_check_same_manager(bdd, var, "VarIsDependent")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + return(.Call(c_cudd_bdd_var_is_dependent, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(var))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_ite <- function(bdd, g, h, limit = 0L) { + if (!.cudd_check_same_manager(bdd, g, "Ite") || + !.cudd_check_same_manager(bdd, h, "Ite")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_ite, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(g), + .cudd_bdd_ptr(h), + limit + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_ite_constant <- function(bdd, g, h) { + if (!.cudd_check_same_manager(bdd, g, "IteConstant") || + !.cudd_check_same_manager(bdd, h, "IteConstant")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_ite_constant, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(g), .cudd_bdd_ptr(h)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_intersect <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Intersect")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_intersect, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_and_limit <- function(bdd, other, limit = 0L) { + if (!.cudd_check_same_manager(bdd, other, "And")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_and_limit, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other), limit) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_or_limit <- function(bdd, other, limit = 0L) { + if (!.cudd_check_same_manager(bdd, other, "Or")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_or_limit, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other), limit) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_nand <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Nand")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_nand, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_nor <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Nor")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_nor, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_xnor <- function(bdd, other, limit = 0L) { + if (!.cudd_check_same_manager(bdd, other, "Xnor")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_xnor, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other), limit) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_cofactor <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Cofactor")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_cofactor, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_constrain <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Constrain")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_constrain, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_compose <- function(bdd, other, index) { + if (!.cudd_check_same_manager(bdd, other, "Compose")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_compose, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other), index) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_permute <- function(bdd, permut) { + ptr <- .Call(c_cudd_bdd_permute, .cudd_bdd_ptr(bdd), permut) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_swap_variables <- function(bdd, x, y) { + if (!.cudd_check_bdd_list_manager(bdd, x, "SwapVariables") || + !.cudd_check_bdd_list_manager(bdd, y, "SwapVariables")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_swap_variables, .cudd_bdd_ptr(bdd), lapply(x, .cudd_bdd_ptr), lapply(y, .cudd_bdd_ptr)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_vector_compose <- function(bdd, vector) { + if (!.cudd_check_bdd_list_manager(bdd, vector, "VectorCompose")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_vector_compose, .cudd_bdd_ptr(bdd), lapply(vector, .cudd_bdd_ptr)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_li_compaction <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "LICompaction")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_li_compaction, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_squeeze <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Squeeze")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_squeeze, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_interpolate <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Interpolate")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_interpolate, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_minimize <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Minimize")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_minimize, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_subset_compress <- function(bdd, nvars, threshold) { + ptr <- .Call(c_cudd_bdd_subset_compress, .cudd_bdd_ptr(bdd), nvars, threshold) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_superset_compress <- function(bdd, nvars, threshold) { + ptr <- .Call(c_cudd_bdd_superset_compress, .cudd_bdd_ptr(bdd), nvars, threshold) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_literal_set_intersection <- function(bdd, other) { # nolint: object_length_linter. + if (!.cudd_check_same_manager(bdd, other, "LiteralSetIntersection")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_literal_set_intersection, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_c_projection <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "CProjection")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_c_projection, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_min_hamming_dist <- function(bdd, minterm, upper_bound) { + result <- .Call(c_cudd_bdd_min_hamming_dist, .cudd_bdd_ptr(bdd), minterm, upper_bound) + names(result) <- c("distance", "minterm") + return(result) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_eval <- function(bdd, inputs) { + ptr <- .Call(c_cudd_bdd_eval, .cudd_bdd_ptr(bdd), inputs) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_decreasing <- function(bdd, index) { + ptr <- .Call(c_cudd_bdd_decreasing, .cudd_bdd_ptr(bdd), index) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_increasing <- function(bdd, index) { + ptr <- .Call(c_cudd_bdd_increasing, .cudd_bdd_ptr(bdd), index) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_make_prime <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "MakePrime")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_make_prime, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_subset_heavy_branch <- function(bdd, num_vars, threshold) { + ptr <- .Call(c_cudd_bdd_subset_heavy_branch, .cudd_bdd_ptr(bdd), num_vars, threshold) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_superset_heavy_branch <- function(bdd, num_vars, threshold) { + ptr <- .Call(c_cudd_bdd_superset_heavy_branch, .cudd_bdd_ptr(bdd), num_vars, threshold) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_subset_short_paths <- function(bdd, num_vars, threshold, hardlimit = FALSE) { + ptr <- .Call(c_cudd_bdd_subset_short_paths, .cudd_bdd_ptr(bdd), num_vars, threshold, hardlimit) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_superset_short_paths <- function(bdd, num_vars, threshold, hardlimit = FALSE) { + ptr <- .Call(c_cudd_bdd_superset_short_paths, .cudd_bdd_ptr(bdd), num_vars, threshold, hardlimit) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_print_cover <- function(bdd) { + .Call(c_cudd_bdd_print_cover, .cudd_bdd_ptr(bdd)) + return(invisible(NULL)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_print_cover_with_cube <- function(bdd, cube) { + if (!.cudd_check_same_manager(bdd, cube, "PrintCover")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + .Call(c_cudd_bdd_print_cover_with_cube, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(cube)) + return(invisible(NULL)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_pick_one_cube <- function(bdd) { + return(.Call(c_cudd_bdd_pick_one_cube, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_pick_one_minterm <- function(bdd, vars) { + if (!.cudd_check_bdd_list_manager(bdd, vars, "PickOneMinterm")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_pick_one_minterm, .cudd_bdd_ptr(bdd), lapply(vars, .cudd_bdd_ptr)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_isop <- function(bdd, upper) { + if (!.cudd_check_same_manager(bdd, upper, "Isop")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_isop, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(upper)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_port_to_zdd <- function(bdd) { + ptr <- .Call(c_cudd_bdd_port_to_zdd, .cudd_bdd_ptr(bdd)) + return(.cudd_zdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_factored_form_string <- function(bdd) { + return(.Call(c_cudd_bdd_factored_form_string, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_print_factored_form <- function(bdd) { + .Call(c_cudd_bdd_print_factored_form, .cudd_bdd_ptr(bdd)) + return(invisible(NULL)) +} diff --git a/inst/examples/bdd_reduce_example.R b/inst/examples/bdd_reduce_example.R new file mode 100644 index 0000000..d6519ef --- /dev/null +++ b/inst/examples/bdd_reduce_example.R @@ -0,0 +1,27 @@ +# Beispiel: großen BDD bauen, darstellen, mit Reduce reduzieren, erneut darstellen + +library(Rcudd) + +manager <- CuddManager() + +vars <- lapply(1:10, function(i) cudd_bdd_var(manager)) +names(vars) <- paste0("x", seq_along(vars)) + +clauses <- list( + vars$x1 * vars$x2, + vars$x3 + !vars$x4, + (vars$x5 * !vars$x6) + (vars$x7 * vars$x8), + vars$x9 ^ vars$x10, + (!vars$x1 * vars$x3) + (vars$x2 * !vars$x4) +) + +large_bdd <- Reduce(`+`, clauses) + +cat("Großer BDD (vor Reduce):\n") +cudd_bdd_print_debug(large_bdd, nvars = 10L, verbosity = 2L) + +restriction <- vars$x1 * !vars$x3 * vars$x5 +reduced_bdd <- cudd_bdd_restrict(large_bdd, restriction) + +cat("Reduzierter BDD (nach Reduce):\n") +cudd_bdd_print_debug(reduced_bdd, nvars = 10L, verbosity = 2L) diff --git a/man/cudd_bdd_methods.Rd b/man/cudd_bdd_methods.Rd new file mode 100644 index 0000000..7bf6a96 --- /dev/null +++ b/man/cudd_bdd_methods.Rd @@ -0,0 +1,179 @@ +% Generated by roxygen2: do not edit by hand +% Please edit documentation in R/cudd_bdd_methods.R +\name{cudd_bdd_methods} +\alias{cudd_bdd_methods} +\alias{cudd_bdd_is_zero} +\alias{cudd_bdd_is_var} +\alias{cudd_bdd_leq} +\alias{cudd_bdd_and_abstract} +\alias{cudd_bdd_exist_abstract} +\alias{cudd_bdd_univ_abstract} +\alias{cudd_bdd_xor_exist_abstract} +\alias{cudd_bdd_boolean_diff} +\alias{cudd_bdd_var_is_dependent} +\alias{cudd_bdd_ite} +\alias{cudd_bdd_ite_constant} +\alias{cudd_bdd_intersect} +\alias{cudd_bdd_and_limit} +\alias{cudd_bdd_or_limit} +\alias{cudd_bdd_nand} +\alias{cudd_bdd_nor} +\alias{cudd_bdd_xnor} +\alias{cudd_bdd_cofactor} +\alias{cudd_bdd_constrain} +\alias{cudd_bdd_compose} +\alias{cudd_bdd_permute} +\alias{cudd_bdd_swap_variables} +\alias{cudd_bdd_vector_compose} +\alias{cudd_bdd_li_compaction} +\alias{cudd_bdd_squeeze} +\alias{cudd_bdd_interpolate} +\alias{cudd_bdd_minimize} +\alias{cudd_bdd_subset_compress} +\alias{cudd_bdd_superset_compress} +\alias{cudd_bdd_literal_set_intersection} +\alias{cudd_bdd_c_projection} +\alias{cudd_bdd_min_hamming_dist} +\alias{cudd_bdd_eval} +\alias{cudd_bdd_decreasing} +\alias{cudd_bdd_increasing} +\alias{cudd_bdd_make_prime} +\alias{cudd_bdd_subset_heavy_branch} +\alias{cudd_bdd_superset_heavy_branch} +\alias{cudd_bdd_subset_short_paths} +\alias{cudd_bdd_superset_short_paths} +\alias{cudd_bdd_print_cover} +\alias{cudd_bdd_print_cover_with_cube} +\alias{cudd_bdd_pick_one_cube} +\alias{cudd_bdd_pick_one_minterm} +\alias{cudd_bdd_isop} +\alias{cudd_bdd_port_to_zdd} +\alias{cudd_bdd_factored_form_string} +\alias{cudd_bdd_print_factored_form} +\title{Additional BDD methods} +\usage{ +cudd_bdd_is_zero(bdd) + +cudd_bdd_is_var(bdd) + +cudd_bdd_leq(bdd, other) + +cudd_bdd_and_abstract(bdd, other, cube, limit = 0L) + +cudd_bdd_exist_abstract(bdd, cube, limit = 0L) + +cudd_bdd_univ_abstract(bdd, cube) + +cudd_bdd_xor_exist_abstract(bdd, other, cube) + +cudd_bdd_boolean_diff(bdd, index) + +cudd_bdd_var_is_dependent(bdd, var) + +cudd_bdd_ite(bdd, g, h, limit = 0L) + +cudd_bdd_ite_constant(bdd, g, h) + +cudd_bdd_intersect(bdd, other) + +cudd_bdd_and_limit(bdd, other, limit = 0L) + +cudd_bdd_or_limit(bdd, other, limit = 0L) + +cudd_bdd_nand(bdd, other) + +cudd_bdd_nor(bdd, other) + +cudd_bdd_xnor(bdd, other, limit = 0L) + +cudd_bdd_cofactor(bdd, other) + +cudd_bdd_constrain(bdd, other) + +cudd_bdd_compose(bdd, other, index) + +cudd_bdd_permute(bdd, permut) + +cudd_bdd_swap_variables(bdd, x, y) + +cudd_bdd_vector_compose(bdd, vector) + +cudd_bdd_li_compaction(bdd, other) + +cudd_bdd_squeeze(bdd, other) + +cudd_bdd_interpolate(bdd, other) + +cudd_bdd_minimize(bdd, other) + +cudd_bdd_subset_compress(bdd, nvars, threshold) + +cudd_bdd_superset_compress(bdd, nvars, threshold) + +cudd_bdd_literal_set_intersection(bdd, other) + +cudd_bdd_c_projection(bdd, other) + +cudd_bdd_min_hamming_dist(bdd, minterm, upper_bound) + +cudd_bdd_eval(bdd, inputs) + +cudd_bdd_decreasing(bdd, index) + +cudd_bdd_increasing(bdd, index) + +cudd_bdd_make_prime(bdd, other) + +cudd_bdd_subset_heavy_branch(bdd, num_vars, threshold) + +cudd_bdd_superset_heavy_branch(bdd, num_vars, threshold) + +cudd_bdd_subset_short_paths(bdd, num_vars, threshold, hardlimit = FALSE) + +cudd_bdd_superset_short_paths(bdd, num_vars, threshold, hardlimit = FALSE) + +cudd_bdd_print_cover(bdd) + +cudd_bdd_print_cover_with_cube(bdd, cube) + +cudd_bdd_pick_one_cube(bdd) + +cudd_bdd_pick_one_minterm(bdd, vars) + +cudd_bdd_isop(bdd, upper) + +cudd_bdd_port_to_zdd(bdd) + +cudd_bdd_factored_form_string(bdd) + +cudd_bdd_print_factored_form(bdd) +} +\arguments{ +\item{bdd}{A [`CuddBDD`] instance.} + +\item{other, cube, var, g, h, upper}{Additional [`CuddBDD`] instances used by the +operation.} + +\item{limit}{Optional non-negative integer limit passed to CUDD.} + +\item{index}{Integer index values used by the operation.} + +\item{permut}{Integer vector describing a variable permutation.} + +\item{x, y, vector, vars}{Lists of [`CuddBDD`] instances.} + +\item{nvars, num_vars, threshold}{Non-negative integer values used by the operation.} + +\item{minterm, inputs}{Integer vectors used by the operation.} + +\item{upper_bound}{Integer upper bound for min hamming distance.} + +\item{hardlimit}{Logical scalar for short path routines.} +} +\value{ +A [`CuddBDD`] instance, a logical scalar, numeric scalar, character + scalar, or list depending on the operation. +} +\description{ +Convenience wrappers for additional methods on CUDD BDD objects. +} diff --git a/man/cudd_bdd_restrict.Rd b/man/cudd_bdd_restrict.Rd new file mode 100644 index 0000000..4657efa --- /dev/null +++ b/man/cudd_bdd_restrict.Rd @@ -0,0 +1,19 @@ +% Generated by roxygen2: do not edit by hand +% Please edit documentation in R/cudd_bdd.R +\name{cudd_bdd_restrict} +\alias{cudd_bdd_restrict} +\title{Restrict a BDD with a constraint} +\usage{ +cudd_bdd_restrict(bdd, constraint) +} +\arguments{ +\item{bdd}{A [`CuddBDD`] instance to restrict.} + +\item{constraint}{A [`CuddBDD`] instance expressing the restriction.} +} +\value{ +A [`CuddBDD`] instance. +} +\description{ +Applies the CUDD `Restrict` operator to reduce a BDD given a constraint BDD. +} diff --git a/src/cudd_manager.cpp b/src/cudd_manager.cpp index 1916c14..1b82b0a 100644 --- a/src/cudd_manager.cpp +++ b/src/cudd_manager.cpp @@ -94,6 +94,65 @@ static ZDD *zdd_from_ptr(SEXP ptr) { return static_cast(addr); } +static SEXP bdd_to_xptr(const BDD &bdd) { + BDD *result = new BDD(bdd); + SEXP ptr = PROTECT(R_MakeExternalPtr(result, R_NilValue, R_NilValue)); + R_RegisterCFinalizerEx(ptr, bdd_finalizer, TRUE); + UNPROTECT(1); + return ptr; +} + +static SEXP zdd_to_xptr(const ZDD &zdd) { + ZDD *result = new ZDD(zdd); + SEXP ptr = PROTECT(R_MakeExternalPtr(result, R_NilValue, R_NilValue)); + R_RegisterCFinalizerEx(ptr, zdd_finalizer, TRUE); + UNPROTECT(1); + return ptr; +} + +static std::vector bdd_vector_from_list(SEXP list, const char *name) { + if (!Rf_isNewList(list)) { + Rf_error("'%s' must be a list of CuddBDD objects.", name); + } + R_xlen_t size = Rf_xlength(list); + std::vector result; + result.reserve(static_cast(size)); + for (R_xlen_t i = 0; i < size; ++i) { + SEXP item = VECTOR_ELT(list, i); + BDD *bdd = bdd_from_ptr(item); + result.push_back(*bdd); + } + return result; +} + +static SEXP bdd_list_from_vector(const std::vector &values) { + R_xlen_t size = static_cast(values.size()); + SEXP list = PROTECT(Rf_allocVector(VECSXP, size)); + for (R_xlen_t i = 0; i < size; ++i) { + SEXP ptr = bdd_to_xptr(values[static_cast(i)]); + SET_VECTOR_ELT(list, i, ptr); + } + UNPROTECT(1); + return list; +} + +static std::vector int_vector_from_sexp(SEXP vec, const char *name) { + if (!Rf_isInteger(vec)) { + Rf_error("'%s' must be an integer vector.", name); + } + R_xlen_t size = Rf_xlength(vec); + std::vector result; + result.reserve(static_cast(size)); + for (R_xlen_t i = 0; i < size; ++i) { + int value = INTEGER(vec)[i]; + if (value == NA_INTEGER) { + Rf_error("'%s' must not contain NA.", name); + } + result.push_back(value); + } + return result; +} + extern "C" SEXP c_cudd_new() { try { Cudd *mgr = new Cudd(); @@ -1025,6 +1084,367 @@ extern "C" SEXP c_cudd_bdd_xor(SEXP lhs_ptr, SEXP rhs_ptr) { return ptr; } +extern "C" SEXP c_cudd_bdd_restrict(SEXP bdd_ptr, SEXP constraint_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *constraint = bdd_from_ptr(constraint_ptr); + BDD *result = new BDD(bdd->Restrict(*constraint)); + SEXP ptr = PROTECT(R_MakeExternalPtr(result, R_NilValue, R_NilValue)); + R_RegisterCFinalizerEx(ptr, bdd_finalizer, TRUE); + UNPROTECT(1); + return ptr; +} + +extern "C" SEXP c_cudd_bdd_is_zero(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return Rf_ScalarLogical(bdd->IsZero()); +} + +extern "C" SEXP c_cudd_bdd_is_var(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return Rf_ScalarLogical(bdd->IsVar()); +} + +extern "C" SEXP c_cudd_bdd_leq(SEXP lhs_ptr, SEXP rhs_ptr) { + BDD *lhs = bdd_from_ptr(lhs_ptr); + BDD *rhs = bdd_from_ptr(rhs_ptr); + return Rf_ScalarLogical(lhs->Leq(*rhs)); +} + +extern "C" SEXP c_cudd_bdd_and_abstract(SEXP bdd_ptr, SEXP other_ptr, SEXP cube_ptr, SEXP limit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + BDD *cube = bdd_from_ptr(cube_ptr); + unsigned int lim = static_cast(Rf_asInteger(limit)); + return bdd_to_xptr(bdd->AndAbstract(*other, *cube, lim)); +} + +extern "C" SEXP c_cudd_bdd_exist_abstract(SEXP bdd_ptr, SEXP cube_ptr, SEXP limit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *cube = bdd_from_ptr(cube_ptr); + unsigned int lim = static_cast(Rf_asInteger(limit)); + return bdd_to_xptr(bdd->ExistAbstract(*cube, lim)); +} + +extern "C" SEXP c_cudd_bdd_univ_abstract(SEXP bdd_ptr, SEXP cube_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *cube = bdd_from_ptr(cube_ptr); + return bdd_to_xptr(bdd->UnivAbstract(*cube)); +} + +extern "C" SEXP c_cudd_bdd_xor_exist_abstract(SEXP bdd_ptr, SEXP other_ptr, SEXP cube_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + BDD *cube = bdd_from_ptr(cube_ptr); + return bdd_to_xptr(bdd->XorExistAbstract(*other, *cube)); +} + +extern "C" SEXP c_cudd_bdd_boolean_diff(SEXP bdd_ptr, SEXP index) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int idx = Rf_asInteger(index); + if (idx == NA_INTEGER || idx < 0) { + Rf_error("'index' must be a non-negative integer."); + } + return bdd_to_xptr(bdd->BooleanDiff(idx)); +} + +extern "C" SEXP c_cudd_bdd_var_is_dependent(SEXP bdd_ptr, SEXP var_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *var = bdd_from_ptr(var_ptr); + return Rf_ScalarLogical(bdd->VarIsDependent(*var)); +} + +extern "C" SEXP c_cudd_bdd_ite(SEXP bdd_ptr, SEXP g_ptr, SEXP h_ptr, SEXP limit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *g = bdd_from_ptr(g_ptr); + BDD *h = bdd_from_ptr(h_ptr); + unsigned int lim = static_cast(Rf_asInteger(limit)); + return bdd_to_xptr(bdd->Ite(*g, *h, lim)); +} + +extern "C" SEXP c_cudd_bdd_ite_constant(SEXP bdd_ptr, SEXP g_ptr, SEXP h_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *g = bdd_from_ptr(g_ptr); + BDD *h = bdd_from_ptr(h_ptr); + return bdd_to_xptr(bdd->IteConstant(*g, *h)); +} + +extern "C" SEXP c_cudd_bdd_intersect(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Intersect(*other)); +} + +extern "C" SEXP c_cudd_bdd_and_limit(SEXP bdd_ptr, SEXP other_ptr, SEXP limit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + unsigned int lim = static_cast(Rf_asInteger(limit)); + return bdd_to_xptr(bdd->And(*other, lim)); +} + +extern "C" SEXP c_cudd_bdd_or_limit(SEXP bdd_ptr, SEXP other_ptr, SEXP limit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + unsigned int lim = static_cast(Rf_asInteger(limit)); + return bdd_to_xptr(bdd->Or(*other, lim)); +} + +extern "C" SEXP c_cudd_bdd_nand(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Nand(*other)); +} + +extern "C" SEXP c_cudd_bdd_nor(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Nor(*other)); +} + +extern "C" SEXP c_cudd_bdd_xnor(SEXP bdd_ptr, SEXP other_ptr, SEXP limit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + unsigned int lim = static_cast(Rf_asInteger(limit)); + return bdd_to_xptr(bdd->Xnor(*other, lim)); +} + +extern "C" SEXP c_cudd_bdd_cofactor(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Cofactor(*other)); +} + +extern "C" SEXP c_cudd_bdd_constrain(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Constrain(*other)); +} + +extern "C" SEXP c_cudd_bdd_compose(SEXP bdd_ptr, SEXP other_ptr, SEXP index) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + int idx = Rf_asInteger(index); + if (idx == NA_INTEGER || idx < 0) { + Rf_error("'index' must be a non-negative integer."); + } + return bdd_to_xptr(bdd->Compose(*other, idx)); +} + +extern "C" SEXP c_cudd_bdd_permute(SEXP bdd_ptr, SEXP permut) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector perm = int_vector_from_sexp(permut, "permut"); + return bdd_to_xptr(bdd->Permute(perm.data())); +} + +extern "C" SEXP c_cudd_bdd_swap_variables(SEXP bdd_ptr, SEXP x_list, SEXP y_list) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector x = bdd_vector_from_list(x_list, "x"); + std::vector y = bdd_vector_from_list(y_list, "y"); + return bdd_to_xptr(bdd->SwapVariables(x, y)); +} + +extern "C" SEXP c_cudd_bdd_vector_compose(SEXP bdd_ptr, SEXP vector_list) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector vec = bdd_vector_from_list(vector_list, "vector"); + return bdd_to_xptr(bdd->VectorCompose(vec)); +} + +extern "C" SEXP c_cudd_bdd_li_compaction(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->LICompaction(*other)); +} + +extern "C" SEXP c_cudd_bdd_squeeze(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Squeeze(*other)); +} + +extern "C" SEXP c_cudd_bdd_interpolate(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Interpolate(*other)); +} + +extern "C" SEXP c_cudd_bdd_minimize(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Minimize(*other)); +} + +extern "C" SEXP c_cudd_bdd_subset_compress(SEXP bdd_ptr, SEXP nvars, SEXP threshold) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'nvars' must be non-negative and 'threshold' must be an integer."); + } + return bdd_to_xptr(bdd->SubsetCompress(vars, thresh)); +} + +extern "C" SEXP c_cudd_bdd_superset_compress(SEXP bdd_ptr, SEXP nvars, SEXP threshold) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'nvars' must be non-negative and 'threshold' must be an integer."); + } + return bdd_to_xptr(bdd->SupersetCompress(vars, thresh)); +} + +extern "C" SEXP c_cudd_bdd_literal_set_intersection(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->LiteralSetIntersection(*other)); +} + +extern "C" SEXP c_cudd_bdd_c_projection(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->CProjection(*other)); +} + +extern "C" SEXP c_cudd_bdd_min_hamming_dist(SEXP bdd_ptr, SEXP minterm, SEXP upper_bound) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector minterm_vec = int_vector_from_sexp(minterm, "minterm"); + int bound = Rf_asInteger(upper_bound); + if (bound == NA_INTEGER) { + Rf_error("'upper_bound' must be an integer."); + } + int result = bdd->MinHammingDist(minterm_vec.data(), bound); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, Rf_ScalarInteger(result)); + SEXP minterm_out = PROTECT(Rf_allocVector(INTSXP, minterm_vec.size())); + for (R_xlen_t i = 0; i < static_cast(minterm_vec.size()); ++i) { + INTEGER(minterm_out)[i] = minterm_vec[static_cast(i)]; + } + SET_VECTOR_ELT(output, 1, minterm_out); + UNPROTECT(2); + return output; +} + +extern "C" SEXP c_cudd_bdd_eval(SEXP bdd_ptr, SEXP inputs) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector values = int_vector_from_sexp(inputs, "inputs"); + return bdd_to_xptr(bdd->Eval(values.data())); +} + +extern "C" SEXP c_cudd_bdd_decreasing(SEXP bdd_ptr, SEXP index) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int idx = Rf_asInteger(index); + if (idx == NA_INTEGER || idx < 0) { + Rf_error("'index' must be a non-negative integer."); + } + return bdd_to_xptr(bdd->Decreasing(idx)); +} + +extern "C" SEXP c_cudd_bdd_increasing(SEXP bdd_ptr, SEXP index) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int idx = Rf_asInteger(index); + if (idx == NA_INTEGER || idx < 0) { + Rf_error("'index' must be a non-negative integer."); + } + return bdd_to_xptr(bdd->Increasing(idx)); +} + +extern "C" SEXP c_cudd_bdd_make_prime(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->MakePrime(*other)); +} + +extern "C" SEXP c_cudd_bdd_subset_heavy_branch(SEXP bdd_ptr, SEXP num_vars, SEXP threshold) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + return bdd_to_xptr(bdd->SubsetHeavyBranch(vars, thresh)); +} + +extern "C" SEXP c_cudd_bdd_superset_heavy_branch(SEXP bdd_ptr, SEXP num_vars, SEXP threshold) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + return bdd_to_xptr(bdd->SupersetHeavyBranch(vars, thresh)); +} + +extern "C" SEXP c_cudd_bdd_subset_short_paths(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP hardlimit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + bool hard = Rf_asLogical(hardlimit); + return bdd_to_xptr(bdd->SubsetShortPaths(vars, thresh, hard)); +} + +extern "C" SEXP c_cudd_bdd_superset_short_paths(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP hardlimit) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + bool hard = Rf_asLogical(hardlimit); + return bdd_to_xptr(bdd->SupersetShortPaths(vars, thresh, hard)); +} + +extern "C" SEXP c_cudd_bdd_print_cover(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + bdd->PrintCover(); + return R_NilValue; +} + +extern "C" SEXP c_cudd_bdd_print_cover_with_cube(SEXP bdd_ptr, SEXP cube_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *cube = bdd_from_ptr(cube_ptr); + bdd->PrintCover(*cube); + return R_NilValue; +} + +extern "C" SEXP c_cudd_bdd_pick_one_cube(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int size = Cudd_ReadSize(bdd->manager()); + std::vector buffer(static_cast(size) + 1, '\0'); + bdd->PickOneCube(buffer.data()); + return Rf_mkString(buffer.data()); +} + +extern "C" SEXP c_cudd_bdd_pick_one_minterm(SEXP bdd_ptr, SEXP vars_list) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector vars = bdd_vector_from_list(vars_list, "vars"); + return bdd_to_xptr(bdd->PickOneMinterm(vars)); +} + +extern "C" SEXP c_cudd_bdd_isop(SEXP bdd_ptr, SEXP upper_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *upper = bdd_from_ptr(upper_ptr); + return bdd_to_xptr(bdd->Isop(*upper)); +} + +extern "C" SEXP c_cudd_bdd_port_to_zdd(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return zdd_to_xptr(bdd->PortToZdd()); +} + +extern "C" SEXP c_cudd_bdd_factored_form_string(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::string output = bdd->FactoredFormString(); + return Rf_mkString(output.c_str()); +} + +extern "C" SEXP c_cudd_bdd_print_factored_form(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + bdd->PrintFactoredForm(); + return R_NilValue; +} + extern "C" SEXP c_cudd_add_times(SEXP lhs_ptr, SEXP rhs_ptr) { ADD *lhs = add_from_ptr(lhs_ptr); ADD *rhs = add_from_ptr(rhs_ptr); diff --git a/src/rcudd.h b/src/rcudd.h index bf95791..5cab5df 100644 --- a/src/rcudd.h +++ b/src/rcudd.h @@ -42,6 +42,55 @@ extern "C" SEXP c_cudd_bdd_not(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_and(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_or(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_xor(SEXP lhs_ptr, SEXP rhs_ptr); +extern "C" SEXP c_cudd_bdd_restrict(SEXP bdd_ptr, SEXP constraint_ptr); +extern "C" SEXP c_cudd_bdd_is_zero(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_is_var(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_leq(SEXP lhs_ptr, SEXP rhs_ptr); +extern "C" SEXP c_cudd_bdd_and_abstract(SEXP bdd_ptr, SEXP other_ptr, SEXP cube_ptr, SEXP limit); +extern "C" SEXP c_cudd_bdd_exist_abstract(SEXP bdd_ptr, SEXP cube_ptr, SEXP limit); +extern "C" SEXP c_cudd_bdd_univ_abstract(SEXP bdd_ptr, SEXP cube_ptr); +extern "C" SEXP c_cudd_bdd_xor_exist_abstract(SEXP bdd_ptr, SEXP other_ptr, SEXP cube_ptr); +extern "C" SEXP c_cudd_bdd_boolean_diff(SEXP bdd_ptr, SEXP index); +extern "C" SEXP c_cudd_bdd_var_is_dependent(SEXP bdd_ptr, SEXP var_ptr); +extern "C" SEXP c_cudd_bdd_ite(SEXP bdd_ptr, SEXP g_ptr, SEXP h_ptr, SEXP limit); +extern "C" SEXP c_cudd_bdd_ite_constant(SEXP bdd_ptr, SEXP g_ptr, SEXP h_ptr); +extern "C" SEXP c_cudd_bdd_intersect(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_and_limit(SEXP bdd_ptr, SEXP other_ptr, SEXP limit); +extern "C" SEXP c_cudd_bdd_or_limit(SEXP bdd_ptr, SEXP other_ptr, SEXP limit); +extern "C" SEXP c_cudd_bdd_nand(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_nor(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_xnor(SEXP bdd_ptr, SEXP other_ptr, SEXP limit); +extern "C" SEXP c_cudd_bdd_cofactor(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_constrain(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_compose(SEXP bdd_ptr, SEXP other_ptr, SEXP index); +extern "C" SEXP c_cudd_bdd_permute(SEXP bdd_ptr, SEXP permut); +extern "C" SEXP c_cudd_bdd_swap_variables(SEXP bdd_ptr, SEXP x_list, SEXP y_list); +extern "C" SEXP c_cudd_bdd_vector_compose(SEXP bdd_ptr, SEXP vector_list); +extern "C" SEXP c_cudd_bdd_li_compaction(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_squeeze(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_interpolate(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_minimize(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_subset_compress(SEXP bdd_ptr, SEXP nvars, SEXP threshold); +extern "C" SEXP c_cudd_bdd_superset_compress(SEXP bdd_ptr, SEXP nvars, SEXP threshold); +extern "C" SEXP c_cudd_bdd_literal_set_intersection(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_c_projection(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_min_hamming_dist(SEXP bdd_ptr, SEXP minterm, SEXP upper_bound); +extern "C" SEXP c_cudd_bdd_eval(SEXP bdd_ptr, SEXP inputs); +extern "C" SEXP c_cudd_bdd_decreasing(SEXP bdd_ptr, SEXP index); +extern "C" SEXP c_cudd_bdd_increasing(SEXP bdd_ptr, SEXP index); +extern "C" SEXP c_cudd_bdd_make_prime(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_subset_heavy_branch(SEXP bdd_ptr, SEXP num_vars, SEXP threshold); +extern "C" SEXP c_cudd_bdd_superset_heavy_branch(SEXP bdd_ptr, SEXP num_vars, SEXP threshold); +extern "C" SEXP c_cudd_bdd_subset_short_paths(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP hardlimit); +extern "C" SEXP c_cudd_bdd_superset_short_paths(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP hardlimit); +extern "C" SEXP c_cudd_bdd_print_cover(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_print_cover_with_cube(SEXP bdd_ptr, SEXP cube_ptr); +extern "C" SEXP c_cudd_bdd_pick_one_cube(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_pick_one_minterm(SEXP bdd_ptr, SEXP vars_list); +extern "C" SEXP c_cudd_bdd_isop(SEXP bdd_ptr, SEXP upper_ptr); +extern "C" SEXP c_cudd_bdd_port_to_zdd(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_factored_form_string(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_print_factored_form(SEXP bdd_ptr); extern "C" SEXP c_cudd_add_times(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_add_plus(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_zdd_intersect(SEXP lhs_ptr, SEXP rhs_ptr); diff --git a/src/register.cpp b/src/register.cpp index 3581cd1..6193f39 100644 --- a/src/register.cpp +++ b/src/register.cpp @@ -39,6 +39,55 @@ static const R_CallMethodDef CallEntries[] = { {"c_cudd_bdd_and", (DL_FUNC) &c_cudd_bdd_and, 2}, {"c_cudd_bdd_or", (DL_FUNC) &c_cudd_bdd_or, 2}, {"c_cudd_bdd_xor", (DL_FUNC) &c_cudd_bdd_xor, 2}, + {"c_cudd_bdd_restrict", (DL_FUNC) &c_cudd_bdd_restrict, 2}, + {"c_cudd_bdd_is_zero", (DL_FUNC) &c_cudd_bdd_is_zero, 1}, + {"c_cudd_bdd_is_var", (DL_FUNC) &c_cudd_bdd_is_var, 1}, + {"c_cudd_bdd_leq", (DL_FUNC) &c_cudd_bdd_leq, 2}, + {"c_cudd_bdd_and_abstract", (DL_FUNC) &c_cudd_bdd_and_abstract, 4}, + {"c_cudd_bdd_exist_abstract", (DL_FUNC) &c_cudd_bdd_exist_abstract, 3}, + {"c_cudd_bdd_univ_abstract", (DL_FUNC) &c_cudd_bdd_univ_abstract, 2}, + {"c_cudd_bdd_xor_exist_abstract", (DL_FUNC) &c_cudd_bdd_xor_exist_abstract, 3}, + {"c_cudd_bdd_boolean_diff", (DL_FUNC) &c_cudd_bdd_boolean_diff, 2}, + {"c_cudd_bdd_var_is_dependent", (DL_FUNC) &c_cudd_bdd_var_is_dependent, 2}, + {"c_cudd_bdd_ite", (DL_FUNC) &c_cudd_bdd_ite, 4}, + {"c_cudd_bdd_ite_constant", (DL_FUNC) &c_cudd_bdd_ite_constant, 3}, + {"c_cudd_bdd_intersect", (DL_FUNC) &c_cudd_bdd_intersect, 2}, + {"c_cudd_bdd_and_limit", (DL_FUNC) &c_cudd_bdd_and_limit, 3}, + {"c_cudd_bdd_or_limit", (DL_FUNC) &c_cudd_bdd_or_limit, 3}, + {"c_cudd_bdd_nand", (DL_FUNC) &c_cudd_bdd_nand, 2}, + {"c_cudd_bdd_nor", (DL_FUNC) &c_cudd_bdd_nor, 2}, + {"c_cudd_bdd_xnor", (DL_FUNC) &c_cudd_bdd_xnor, 3}, + {"c_cudd_bdd_cofactor", (DL_FUNC) &c_cudd_bdd_cofactor, 2}, + {"c_cudd_bdd_constrain", (DL_FUNC) &c_cudd_bdd_constrain, 2}, + {"c_cudd_bdd_compose", (DL_FUNC) &c_cudd_bdd_compose, 3}, + {"c_cudd_bdd_permute", (DL_FUNC) &c_cudd_bdd_permute, 2}, + {"c_cudd_bdd_swap_variables", (DL_FUNC) &c_cudd_bdd_swap_variables, 3}, + {"c_cudd_bdd_vector_compose", (DL_FUNC) &c_cudd_bdd_vector_compose, 2}, + {"c_cudd_bdd_li_compaction", (DL_FUNC) &c_cudd_bdd_li_compaction, 2}, + {"c_cudd_bdd_squeeze", (DL_FUNC) &c_cudd_bdd_squeeze, 2}, + {"c_cudd_bdd_interpolate", (DL_FUNC) &c_cudd_bdd_interpolate, 2}, + {"c_cudd_bdd_minimize", (DL_FUNC) &c_cudd_bdd_minimize, 2}, + {"c_cudd_bdd_subset_compress", (DL_FUNC) &c_cudd_bdd_subset_compress, 3}, + {"c_cudd_bdd_superset_compress", (DL_FUNC) &c_cudd_bdd_superset_compress, 3}, + {"c_cudd_bdd_literal_set_intersection", (DL_FUNC) &c_cudd_bdd_literal_set_intersection, 2}, + {"c_cudd_bdd_c_projection", (DL_FUNC) &c_cudd_bdd_c_projection, 2}, + {"c_cudd_bdd_min_hamming_dist", (DL_FUNC) &c_cudd_bdd_min_hamming_dist, 3}, + {"c_cudd_bdd_eval", (DL_FUNC) &c_cudd_bdd_eval, 2}, + {"c_cudd_bdd_decreasing", (DL_FUNC) &c_cudd_bdd_decreasing, 2}, + {"c_cudd_bdd_increasing", (DL_FUNC) &c_cudd_bdd_increasing, 2}, + {"c_cudd_bdd_make_prime", (DL_FUNC) &c_cudd_bdd_make_prime, 2}, + {"c_cudd_bdd_subset_heavy_branch", (DL_FUNC) &c_cudd_bdd_subset_heavy_branch, 3}, + {"c_cudd_bdd_superset_heavy_branch", (DL_FUNC) &c_cudd_bdd_superset_heavy_branch, 3}, + {"c_cudd_bdd_subset_short_paths", (DL_FUNC) &c_cudd_bdd_subset_short_paths, 4}, + {"c_cudd_bdd_superset_short_paths", (DL_FUNC) &c_cudd_bdd_superset_short_paths, 4}, + {"c_cudd_bdd_print_cover", (DL_FUNC) &c_cudd_bdd_print_cover, 1}, + {"c_cudd_bdd_print_cover_with_cube", (DL_FUNC) &c_cudd_bdd_print_cover_with_cube, 2}, + {"c_cudd_bdd_pick_one_cube", (DL_FUNC) &c_cudd_bdd_pick_one_cube, 1}, + {"c_cudd_bdd_pick_one_minterm", (DL_FUNC) &c_cudd_bdd_pick_one_minterm, 2}, + {"c_cudd_bdd_isop", (DL_FUNC) &c_cudd_bdd_isop, 2}, + {"c_cudd_bdd_port_to_zdd", (DL_FUNC) &c_cudd_bdd_port_to_zdd, 1}, + {"c_cudd_bdd_factored_form_string", (DL_FUNC) &c_cudd_bdd_factored_form_string, 1}, + {"c_cudd_bdd_print_factored_form", (DL_FUNC) &c_cudd_bdd_print_factored_form, 1}, {"c_cudd_add_times", (DL_FUNC) &c_cudd_add_times, 2}, {"c_cudd_add_plus", (DL_FUNC) &c_cudd_add_plus, 2}, {"c_cudd_zdd_intersect", (DL_FUNC) &c_cudd_zdd_intersect, 2}, From 53bb6f33ed1dc9651d91aa711c7dc8e81cae392b Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Wed, 31 Dec 2025 22:44:18 +0100 Subject: [PATCH 2/8] Add more BDD helpers and tests --- NAMESPACE | 34 +++ R/cudd_bdd_methods.R | 347 ++++++++++++++++++++++++- man/cudd_bdd_methods.Rd | 138 +++++++++- src/cudd_manager.cpp | 295 +++++++++++++++++++++ src/rcudd.h | 34 +++ src/register.cpp | 34 +++ tests/testthat/test_cudd_bdd_methods.R | 28 ++ 7 files changed, 900 insertions(+), 10 deletions(-) create mode 100644 tests/testthat/test_cudd_bdd_methods.R diff --git a/NAMESPACE b/NAMESPACE index 759cd09..f73de16 100644 --- a/NAMESPACE +++ b/NAMESPACE @@ -16,38 +16,61 @@ export(cudd_autodyn_disable_zdd) export(cudd_autodyn_enable) export(cudd_autodyn_enable_zdd) export(cudd_background) +export(cudd_bdd_adj_permute_x) export(cudd_bdd_and_abstract) export(cudd_bdd_and_limit) +export(cudd_bdd_biased_over_approx) +export(cudd_bdd_biased_under_approx) export(cudd_bdd_bind_var) export(cudd_bdd_boolean_diff) export(cudd_bdd_c_projection) +export(cudd_bdd_char_to_vect) +export(cudd_bdd_classify_support) +export(cudd_bdd_clipping_and) +export(cudd_bdd_clipping_and_abstract) export(cudd_bdd_cofactor) export(cudd_bdd_compose) export(cudd_bdd_constrain) +export(cudd_bdd_constrain_decomp) +export(cudd_bdd_count_leaves) +export(cudd_bdd_count_minterm) +export(cudd_bdd_count_path) export(cudd_bdd_decreasing) +export(cudd_bdd_density) export(cudd_bdd_dump_dot) export(cudd_bdd_epd_print_minterm) +export(cudd_bdd_estimate_cofactor) +export(cudd_bdd_estimate_cofactor_simple) export(cudd_bdd_eval) export(cudd_bdd_exist_abstract) export(cudd_bdd_factored_form_string) +export(cudd_bdd_find_essential) export(cudd_bdd_increasing) export(cudd_bdd_interpolate) export(cudd_bdd_intersect) +export(cudd_bdd_is_cube) +export(cudd_bdd_is_one) export(cudd_bdd_is_var) +export(cudd_bdd_is_var_essential) export(cudd_bdd_is_zero) export(cudd_bdd_isop) export(cudd_bdd_ite) export(cudd_bdd_ite_constant) +export(cudd_bdd_largest_prime_unate) export(cudd_bdd_leq) +export(cudd_bdd_leq_unless) export(cudd_bdd_li_compaction) export(cudd_bdd_literal_set_intersection) export(cudd_bdd_make_prime) +export(cudd_bdd_maximally_expand) export(cudd_bdd_min_hamming_dist) export(cudd_bdd_minimize) export(cudd_bdd_nand) export(cudd_bdd_nor) +export(cudd_bdd_np_and) export(cudd_bdd_one) export(cudd_bdd_or_limit) +export(cudd_bdd_over_approx) export(cudd_bdd_permute) export(cudd_bdd_pick_one_cube) export(cudd_bdd_pick_one_minterm) @@ -57,10 +80,14 @@ export(cudd_bdd_print_cover_with_cube) export(cudd_bdd_print_debug) export(cudd_bdd_print_factored_form) export(cudd_bdd_print_minterm) +export(cudd_bdd_print_two_literal_clauses) export(cudd_bdd_realign_disable) export(cudd_bdd_realign_enable) export(cudd_bdd_realignment_enabled) +export(cudd_bdd_remap_over_approx) +export(cudd_bdd_remap_under_approx) export(cudd_bdd_restrict) +export(cudd_bdd_split_set) export(cudd_bdd_squeeze) export(cudd_bdd_subset_compress) export(cudd_bdd_subset_heavy_branch) @@ -68,18 +95,25 @@ export(cudd_bdd_subset_short_paths) export(cudd_bdd_superset_compress) export(cudd_bdd_superset_heavy_branch) export(cudd_bdd_superset_short_paths) +export(cudd_bdd_support) +export(cudd_bdd_support_indices) +export(cudd_bdd_support_size) export(cudd_bdd_swap_variables) export(cudd_bdd_to_add) export(cudd_bdd_to_zdd) +export(cudd_bdd_transfer) export(cudd_bdd_truth_table) export(cudd_bdd_unbind_var) +export(cudd_bdd_under_approx) export(cudd_bdd_univ_abstract) export(cudd_bdd_var) +export(cudd_bdd_var_are_symmetric) export(cudd_bdd_var_is_bound) export(cudd_bdd_var_is_dependent) export(cudd_bdd_vector_compose) export(cudd_bdd_xnor) export(cudd_bdd_xor_exist_abstract) +export(cudd_bdd_zdd_isop) export(cudd_bdd_zero) export(cudd_clear_error_code) export(cudd_clear_variable_names) diff --git a/R/cudd_bdd_methods.R b/R/cudd_bdd_methods.R index fc82aac..f9ffff1 100644 --- a/R/cudd_bdd_methods.R +++ b/R/cudd_bdd_methods.R @@ -2,6 +2,10 @@ return(methods::new("CuddBDD", ptr = ptr, manager_ptr = .cudd_bdd_manager_ptr(bdd))) } +.cudd_bdd_wrap_list <- function(ptrs, bdd) { + return(lapply(ptrs, .cudd_bdd_wrap, bdd = bdd)) +} + .cudd_check_bdd_list_manager <- function(bdd, vars, op) { for (var in vars) { if (!.cudd_check_same_manager(bdd, var, op)) { @@ -20,16 +24,21 @@ #' Convenience wrappers for additional methods on CUDD BDD objects. #' #' @param bdd A [`CuddBDD`] instance. -#' @param other,cube,var,g,h,upper Additional [`CuddBDD`] instances used by the -#' operation. +#' @param other,cube,var,g,h,upper,bias,phases,ub,f,d Additional [`CuddBDD`] +#' instances used by the operation. +#' @param manager A [`CuddManager`] instance. #' @param limit Optional non-negative integer limit passed to CUDD. -#' @param index Integer index values used by the operation. +#' @param index,index1,index2,phase Integer index values used by the operation. #' @param permut Integer vector describing a variable permutation. -#' @param x,y,vector,vars Lists of [`CuddBDD`] instances. +#' @param x,y,vector,vars,x_vars Lists of [`CuddBDD`] instances. #' @param nvars,num_vars,threshold Non-negative integer values used by the operation. +#' @param max_depth,direction Integer values used by clipping operations. +#' @param safe Logical scalar controlling approximate operations. +#' @param quality,quality1,quality0 Numeric scalars controlling approximate operations. #' @param minterm,inputs Integer vectors used by the operation. #' @param upper_bound Integer upper bound for min hamming distance. #' @param hardlimit Logical scalar for short path routines. +#' @param m Numeric scalar used by split operations. #' @return A [`CuddBDD`] instance, a logical scalar, numeric scalar, character #' scalar, or list depending on the operation. #' @name cudd_bdd_methods @@ -41,12 +50,183 @@ cudd_bdd_is_zero <- function(bdd) { return(.Call(c_cudd_bdd_is_zero, .cudd_bdd_ptr(bdd))) } +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_is_one <- function(bdd) { + return(.Call(c_cudd_bdd_is_one, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_is_cube <- function(bdd) { + return(.Call(c_cudd_bdd_is_cube, .cudd_bdd_ptr(bdd))) +} + #' @rdname cudd_bdd_methods #' @export cudd_bdd_is_var <- function(bdd) { return(.Call(c_cudd_bdd_is_var, .cudd_bdd_ptr(bdd))) } +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_find_essential <- function(bdd) { + ptr <- .Call(c_cudd_bdd_find_essential, .cudd_bdd_ptr(bdd)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_print_two_literal_clauses <- function(bdd) { # nolint: object_length_linter. + .Call(c_cudd_bdd_print_two_literal_clauses, .cudd_bdd_ptr(bdd)) + return(invisible(NULL)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_count_minterm <- function(bdd, nvars) { + return(.Call(c_cudd_bdd_count_minterm, .cudd_bdd_ptr(bdd), nvars)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_count_path <- function(bdd) { + return(.Call(c_cudd_bdd_count_path, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_support <- function(bdd) { + ptr <- .Call(c_cudd_bdd_support, .cudd_bdd_ptr(bdd)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_support_size <- function(bdd) { + return(.Call(c_cudd_bdd_support_size, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_support_indices <- function(bdd) { + return(.Call(c_cudd_bdd_support_indices, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_classify_support <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "ClassifySupport")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + result <- .Call(c_cudd_bdd_classify_support, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("common", "only_bdd", "only_other") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_count_leaves <- function(bdd) { + return(.Call(c_cudd_bdd_count_leaves, .cudd_bdd_ptr(bdd))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_density <- function(bdd, nvars) { + return(.Call(c_cudd_bdd_density, .cudd_bdd_ptr(bdd), nvars)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_under_approx <- function(bdd, num_vars, threshold = 0L, safe = FALSE, quality = 1.0) { + ptr <- .Call( + c_cudd_bdd_under_approx, + .cudd_bdd_ptr(bdd), + num_vars, + threshold, + safe, + quality + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_over_approx <- function(bdd, num_vars, threshold = 0L, safe = FALSE, quality = 1.0) { + ptr <- .Call( + c_cudd_bdd_over_approx, + .cudd_bdd_ptr(bdd), + num_vars, + threshold, + safe, + quality + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_remap_under_approx <- function(bdd, num_vars, threshold = 0L, quality = 1.0) { + ptr <- .Call( + c_cudd_bdd_remap_under_approx, + .cudd_bdd_ptr(bdd), + num_vars, + threshold, + quality + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_remap_over_approx <- function(bdd, num_vars, threshold = 0L, quality = 1.0) { + ptr <- .Call( + c_cudd_bdd_remap_over_approx, + .cudd_bdd_ptr(bdd), + num_vars, + threshold, + quality + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_biased_under_approx <- function(bdd, bias, num_vars, threshold = 0L, quality1 = 1.0, quality0 = 1.0) { + if (!.cudd_check_same_manager(bdd, bias, "BiasedUnderApprox")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_biased_under_approx, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(bias), + num_vars, + threshold, + quality1, + quality0 + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_biased_over_approx <- function(bdd, bias, num_vars, threshold = 0L, quality1 = 1.0, quality0 = 1.0) { + if (!.cudd_check_same_manager(bdd, bias, "BiasedOverApprox")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_biased_over_approx, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(bias), + num_vars, + threshold, + quality1, + quality0 + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + #' @rdname cudd_bdd_methods #' @export cudd_bdd_leq <- function(bdd, other) { @@ -474,3 +654,162 @@ cudd_bdd_print_factored_form <- function(bdd) { .Call(c_cudd_bdd_print_factored_form, .cudd_bdd_ptr(bdd)) return(invisible(NULL)) } + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_clipping_and <- function(bdd, other, max_depth, direction = 0L) { + if (!.cudd_check_same_manager(bdd, other, "ClippingAnd")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_clipping_and, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(other), + max_depth, + direction + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_clipping_and_abstract <- function(bdd, other, cube, max_depth, direction = 0L) { + if (!.cudd_check_same_manager(bdd, other, "ClippingAndAbstract") || + !.cudd_check_same_manager(bdd, cube, "ClippingAndAbstract")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_clipping_and_abstract, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(other), + .cudd_bdd_ptr(cube), + max_depth, + direction + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_var_are_symmetric <- function(bdd, index1, index2) { + return(.Call(c_cudd_bdd_var_are_symmetric, .cudd_bdd_ptr(bdd), index1, index2)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_adj_permute_x <- function(bdd, x) { + if (!.cudd_check_bdd_list_manager(bdd, x, "AdjPermuteX")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_adj_permute_x, .cudd_bdd_ptr(bdd), lapply(x, .cudd_bdd_ptr)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_is_var_essential <- function(bdd, index, phase) { + return(.Call(c_cudd_bdd_is_var_essential, .cudd_bdd_ptr(bdd), index, phase)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_np_and <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "NPAnd")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_np_and, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_constrain_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_constrain_decomp, .cudd_bdd_ptr(bdd)) + return(.cudd_bdd_wrap_list(result, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_char_to_vect <- function(bdd) { + result <- .Call(c_cudd_bdd_char_to_vect, .cudd_bdd_ptr(bdd)) + return(.cudd_bdd_wrap_list(result, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_leq_unless <- function(bdd, g, d) { + if (!.cudd_check_same_manager(bdd, g, "LeqUnless") || + !.cudd_check_same_manager(bdd, d, "LeqUnless")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + return(.Call(c_cudd_bdd_leq_unless, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(g), .cudd_bdd_ptr(d))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_maximally_expand <- function(bdd, ub, f) { + if (!.cudd_check_same_manager(bdd, ub, "MaximallyExpand") || + !.cudd_check_same_manager(bdd, f, "MaximallyExpand")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_maximally_expand, + .cudd_bdd_ptr(bdd), + .cudd_bdd_ptr(ub), + .cudd_bdd_ptr(f) + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_largest_prime_unate <- function(bdd, phases) { + if (!.cudd_check_same_manager(bdd, phases, "LargestPrimeUnate")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_largest_prime_unate, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(phases)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_split_set <- function(bdd, x_vars, m) { + if (!.cudd_check_bdd_list_manager(bdd, x_vars, "SplitSet")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_split_set, .cudd_bdd_ptr(bdd), lapply(x_vars, .cudd_bdd_ptr), m) + return(.cudd_bdd_wrap(ptr, bdd)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_estimate_cofactor <- function(bdd, index, phase) { + return(.Call(c_cudd_bdd_estimate_cofactor, .cudd_bdd_ptr(bdd), index, phase)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_estimate_cofactor_simple <- function(bdd, index) { # nolint: object_length_linter. + return(.Call(c_cudd_bdd_estimate_cofactor_simple, .cudd_bdd_ptr(bdd), index)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_zdd_isop <- function(bdd, upper) { + if (!.cudd_check_same_manager(bdd, upper, "zddIsop")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + result <- .Call(c_cudd_bdd_zdd_isop, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(upper)) + output <- list( + bdd = .cudd_bdd_wrap(result[[1L]], bdd), + zdd = .cudd_zdd_wrap(result[[2L]], bdd) + ) + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_transfer <- function(bdd, manager) { + ptr <- .Call(c_cudd_bdd_transfer, .cudd_bdd_ptr(bdd), .cudd_manager_ptr(manager)) + return(methods::new("CuddBDD", ptr = ptr, manager_ptr = .cudd_manager_ptr(manager))) +} diff --git a/man/cudd_bdd_methods.Rd b/man/cudd_bdd_methods.Rd index 7bf6a96..58bb1a7 100644 --- a/man/cudd_bdd_methods.Rd +++ b/man/cudd_bdd_methods.Rd @@ -3,7 +3,25 @@ \name{cudd_bdd_methods} \alias{cudd_bdd_methods} \alias{cudd_bdd_is_zero} +\alias{cudd_bdd_is_one} +\alias{cudd_bdd_is_cube} \alias{cudd_bdd_is_var} +\alias{cudd_bdd_find_essential} +\alias{cudd_bdd_print_two_literal_clauses} +\alias{cudd_bdd_count_minterm} +\alias{cudd_bdd_count_path} +\alias{cudd_bdd_support} +\alias{cudd_bdd_support_size} +\alias{cudd_bdd_support_indices} +\alias{cudd_bdd_classify_support} +\alias{cudd_bdd_count_leaves} +\alias{cudd_bdd_density} +\alias{cudd_bdd_under_approx} +\alias{cudd_bdd_over_approx} +\alias{cudd_bdd_remap_under_approx} +\alias{cudd_bdd_remap_over_approx} +\alias{cudd_bdd_biased_under_approx} +\alias{cudd_bdd_biased_over_approx} \alias{cudd_bdd_leq} \alias{cudd_bdd_and_abstract} \alias{cudd_bdd_exist_abstract} @@ -50,12 +68,78 @@ \alias{cudd_bdd_port_to_zdd} \alias{cudd_bdd_factored_form_string} \alias{cudd_bdd_print_factored_form} +\alias{cudd_bdd_clipping_and} +\alias{cudd_bdd_clipping_and_abstract} +\alias{cudd_bdd_var_are_symmetric} +\alias{cudd_bdd_adj_permute_x} +\alias{cudd_bdd_is_var_essential} +\alias{cudd_bdd_np_and} +\alias{cudd_bdd_constrain_decomp} +\alias{cudd_bdd_char_to_vect} +\alias{cudd_bdd_leq_unless} +\alias{cudd_bdd_maximally_expand} +\alias{cudd_bdd_largest_prime_unate} +\alias{cudd_bdd_split_set} +\alias{cudd_bdd_estimate_cofactor} +\alias{cudd_bdd_estimate_cofactor_simple} +\alias{cudd_bdd_zdd_isop} +\alias{cudd_bdd_transfer} \title{Additional BDD methods} \usage{ cudd_bdd_is_zero(bdd) +cudd_bdd_is_one(bdd) + +cudd_bdd_is_cube(bdd) + cudd_bdd_is_var(bdd) +cudd_bdd_find_essential(bdd) + +cudd_bdd_print_two_literal_clauses(bdd) + +cudd_bdd_count_minterm(bdd, nvars) + +cudd_bdd_count_path(bdd) + +cudd_bdd_support(bdd) + +cudd_bdd_support_size(bdd) + +cudd_bdd_support_indices(bdd) + +cudd_bdd_classify_support(bdd, other) + +cudd_bdd_count_leaves(bdd) + +cudd_bdd_density(bdd, nvars) + +cudd_bdd_under_approx(bdd, num_vars, threshold = 0L, safe = FALSE, quality = 1) + +cudd_bdd_over_approx(bdd, num_vars, threshold = 0L, safe = FALSE, quality = 1) + +cudd_bdd_remap_under_approx(bdd, num_vars, threshold = 0L, quality = 1) + +cudd_bdd_remap_over_approx(bdd, num_vars, threshold = 0L, quality = 1) + +cudd_bdd_biased_under_approx( + bdd, + bias, + num_vars, + threshold = 0L, + quality1 = 1, + quality0 = 1 +) + +cudd_bdd_biased_over_approx( + bdd, + bias, + num_vars, + threshold = 0L, + quality1 = 1, + quality0 = 1 +) + cudd_bdd_leq(bdd, other) cudd_bdd_and_abstract(bdd, other, cube, limit = 0L) @@ -147,28 +231,70 @@ cudd_bdd_port_to_zdd(bdd) cudd_bdd_factored_form_string(bdd) cudd_bdd_print_factored_form(bdd) + +cudd_bdd_clipping_and(bdd, other, max_depth, direction = 0L) + +cudd_bdd_clipping_and_abstract(bdd, other, cube, max_depth, direction = 0L) + +cudd_bdd_var_are_symmetric(bdd, index1, index2) + +cudd_bdd_adj_permute_x(bdd, x) + +cudd_bdd_is_var_essential(bdd, index, phase) + +cudd_bdd_np_and(bdd, other) + +cudd_bdd_constrain_decomp(bdd) + +cudd_bdd_char_to_vect(bdd) + +cudd_bdd_leq_unless(bdd, g, d) + +cudd_bdd_maximally_expand(bdd, ub, f) + +cudd_bdd_largest_prime_unate(bdd, phases) + +cudd_bdd_split_set(bdd, x_vars, m) + +cudd_bdd_estimate_cofactor(bdd, index, phase) + +cudd_bdd_estimate_cofactor_simple(bdd, index) + +cudd_bdd_zdd_isop(bdd, upper) + +cudd_bdd_transfer(bdd, manager) } \arguments{ \item{bdd}{A [`CuddBDD`] instance.} -\item{other, cube, var, g, h, upper}{Additional [`CuddBDD`] instances used by the -operation.} +\item{nvars, num_vars, threshold}{Non-negative integer values used by the operation.} + +\item{other, cube, var, g, h, upper, bias, phases, ub, f, d}{Additional [`CuddBDD`] +instances used by the operation.} + +\item{safe}{Logical scalar controlling approximate operations.} + +\item{quality, quality1, quality0}{Numeric scalars controlling approximate operations.} \item{limit}{Optional non-negative integer limit passed to CUDD.} -\item{index}{Integer index values used by the operation.} +\item{index, index1, index2, phase}{Integer index values used by the operation.} \item{permut}{Integer vector describing a variable permutation.} -\item{x, y, vector, vars}{Lists of [`CuddBDD`] instances.} - -\item{nvars, num_vars, threshold}{Non-negative integer values used by the operation.} +\item{x, y, vector, vars, x_vars}{Lists of [`CuddBDD`] instances.} \item{minterm, inputs}{Integer vectors used by the operation.} \item{upper_bound}{Integer upper bound for min hamming distance.} \item{hardlimit}{Logical scalar for short path routines.} + +\item{max_depth, direction}{Integer values used by clipping operations.} + +\item{m}{Numeric scalar used by split operations.} + +\item{manager}{A [`CuddManager`] instance.} } \value{ A [`CuddBDD`] instance, a logical scalar, numeric scalar, character diff --git a/src/cudd_manager.cpp b/src/cudd_manager.cpp index 1b82b0a..e70ff45 100644 --- a/src/cudd_manager.cpp +++ b/src/cudd_manager.cpp @@ -153,6 +153,16 @@ static std::vector int_vector_from_sexp(SEXP vec, const char *name) { return result; } +static SEXP int_vector_to_sexp(const std::vector &values) { + R_xlen_t size = static_cast(values.size()); + SEXP vec = PROTECT(Rf_allocVector(INTSXP, size)); + for (R_xlen_t i = 0; i < size; ++i) { + INTEGER(vec)[i] = static_cast(values[static_cast(i)]); + } + UNPROTECT(1); + return vec; +} + extern "C" SEXP c_cudd_new() { try { Cudd *mgr = new Cudd(); @@ -1094,6 +1104,291 @@ extern "C" SEXP c_cudd_bdd_restrict(SEXP bdd_ptr, SEXP constraint_ptr) { return ptr; } +extern "C" SEXP c_cudd_bdd_is_one(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return Rf_ScalarLogical(bdd->IsOne()); +} + +extern "C" SEXP c_cudd_bdd_is_cube(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return Rf_ScalarLogical(bdd->IsCube()); +} + +extern "C" SEXP c_cudd_bdd_find_essential(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return bdd_to_xptr(bdd->FindEssential()); +} + +extern "C" SEXP c_cudd_bdd_print_two_literal_clauses(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + bdd->PrintTwoLiteralClauses(); + return R_NilValue; +} + +extern "C" SEXP c_cudd_bdd_count_minterm(SEXP bdd_ptr, SEXP nvars) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + if (vars == NA_INTEGER || vars < 0) { + Rf_error("'nvars' must be a non-negative integer."); + } + return Rf_ScalarReal(bdd->CountMinterm(vars)); +} + +extern "C" SEXP c_cudd_bdd_count_path(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return Rf_ScalarReal(bdd->CountPath()); +} + +extern "C" SEXP c_cudd_bdd_support(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return bdd_to_xptr(bdd->Support()); +} + +extern "C" SEXP c_cudd_bdd_support_size(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return Rf_ScalarInteger(bdd->SupportSize()); +} + +extern "C" SEXP c_cudd_bdd_support_indices(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector indices = bdd->SupportIndices(); + return int_vector_to_sexp(indices); +} + +extern "C" SEXP c_cudd_bdd_classify_support(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + BDD common; + BDD only_f; + BDD only_g; + bdd->ClassifySupport(*other, &common, &only_f, &only_g); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 3)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(common)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(only_f)); + SET_VECTOR_ELT(output, 2, bdd_to_xptr(only_g)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_count_leaves(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + return Rf_ScalarInteger(bdd->CountLeaves()); +} + +extern "C" SEXP c_cudd_bdd_density(SEXP bdd_ptr, SEXP nvars) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + if (vars == NA_INTEGER || vars < 0) { + Rf_error("'nvars' must be a non-negative integer."); + } + return Rf_ScalarReal(bdd->Density(vars)); +} + +extern "C" SEXP c_cudd_bdd_under_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP safe, SEXP quality) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + bool safe_flag = Rf_asLogical(safe); + double qual = Rf_asReal(quality); + return bdd_to_xptr(bdd->UnderApprox(vars, thresh, safe_flag, qual)); +} + +extern "C" SEXP c_cudd_bdd_over_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP safe, SEXP quality) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + bool safe_flag = Rf_asLogical(safe); + double qual = Rf_asReal(quality); + return bdd_to_xptr(bdd->OverApprox(vars, thresh, safe_flag, qual)); +} + +extern "C" SEXP c_cudd_bdd_remap_under_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP quality) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + double qual = Rf_asReal(quality); + return bdd_to_xptr(bdd->RemapUnderApprox(vars, thresh, qual)); +} + +extern "C" SEXP c_cudd_bdd_remap_over_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP quality) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + double qual = Rf_asReal(quality); + return bdd_to_xptr(bdd->RemapOverApprox(vars, thresh, qual)); +} + +extern "C" SEXP c_cudd_bdd_biased_under_approx(SEXP bdd_ptr, SEXP bias_ptr, SEXP num_vars, SEXP threshold, SEXP quality1, SEXP quality0) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *bias = bdd_from_ptr(bias_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + double qual1 = Rf_asReal(quality1); + double qual0 = Rf_asReal(quality0); + return bdd_to_xptr(bdd->BiasedUnderApprox(*bias, vars, thresh, qual1, qual0)); +} + +extern "C" SEXP c_cudd_bdd_biased_over_approx(SEXP bdd_ptr, SEXP bias_ptr, SEXP num_vars, SEXP threshold, SEXP quality1, SEXP quality0) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *bias = bdd_from_ptr(bias_ptr); + int vars = Rf_asInteger(num_vars); + int thresh = Rf_asInteger(threshold); + if (vars == NA_INTEGER || vars < 0 || thresh == NA_INTEGER) { + Rf_error("'num_vars' must be non-negative and 'threshold' must be an integer."); + } + double qual1 = Rf_asReal(quality1); + double qual0 = Rf_asReal(quality0); + return bdd_to_xptr(bdd->BiasedOverApprox(*bias, vars, thresh, qual1, qual0)); +} + +extern "C" SEXP c_cudd_bdd_clipping_and(SEXP bdd_ptr, SEXP other_ptr, SEXP max_depth, SEXP direction) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + int depth = Rf_asInteger(max_depth); + int dir = Rf_asInteger(direction); + if (depth == NA_INTEGER || dir == NA_INTEGER) { + Rf_error("'max_depth' and 'direction' must be integers."); + } + return bdd_to_xptr(bdd->ClippingAnd(*other, depth, dir)); +} + +extern "C" SEXP c_cudd_bdd_clipping_and_abstract(SEXP bdd_ptr, SEXP other_ptr, SEXP cube_ptr, SEXP max_depth, SEXP direction) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + BDD *cube = bdd_from_ptr(cube_ptr); + int depth = Rf_asInteger(max_depth); + int dir = Rf_asInteger(direction); + if (depth == NA_INTEGER || dir == NA_INTEGER) { + Rf_error("'max_depth' and 'direction' must be integers."); + } + return bdd_to_xptr(bdd->ClippingAndAbstract(*other, *cube, depth, dir)); +} + +extern "C" SEXP c_cudd_bdd_var_are_symmetric(SEXP bdd_ptr, SEXP index1, SEXP index2) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int idx1 = Rf_asInteger(index1); + int idx2 = Rf_asInteger(index2); + if (idx1 == NA_INTEGER || idx1 < 0 || idx2 == NA_INTEGER || idx2 < 0) { + Rf_error("'index1' and 'index2' must be non-negative integers."); + } + return Rf_ScalarLogical(bdd->VarAreSymmetric(idx1, idx2)); +} + +extern "C" SEXP c_cudd_bdd_adj_permute_x(SEXP bdd_ptr, SEXP x_list) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector x = bdd_vector_from_list(x_list, "x"); + return bdd_to_xptr(bdd->AdjPermuteX(x)); +} + +extern "C" SEXP c_cudd_bdd_is_var_essential(SEXP bdd_ptr, SEXP index, SEXP phase) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int idx = Rf_asInteger(index); + int phase_val = Rf_asInteger(phase); + if (idx == NA_INTEGER || idx < 0 || phase_val == NA_INTEGER) { + Rf_error("'index' must be non-negative and 'phase' must be an integer."); + } + return Rf_ScalarLogical(bdd->IsVarEssential(idx, phase_val)); +} + +extern "C" SEXP c_cudd_bdd_np_and(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->NPAnd(*other)); +} + +extern "C" SEXP c_cudd_bdd_constrain_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector parts = bdd->ConstrainDecomp(); + return bdd_list_from_vector(parts); +} + +extern "C" SEXP c_cudd_bdd_char_to_vect(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector parts = bdd->CharToVect(); + return bdd_list_from_vector(parts); +} + +extern "C" SEXP c_cudd_bdd_leq_unless(SEXP bdd_ptr, SEXP g_ptr, SEXP d_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *g = bdd_from_ptr(g_ptr); + BDD *d = bdd_from_ptr(d_ptr); + return Rf_ScalarLogical(bdd->LeqUnless(*g, *d)); +} + +extern "C" SEXP c_cudd_bdd_maximally_expand(SEXP bdd_ptr, SEXP ub_ptr, SEXP f_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *ub = bdd_from_ptr(ub_ptr); + BDD *f = bdd_from_ptr(f_ptr); + return bdd_to_xptr(bdd->MaximallyExpand(*ub, *f)); +} + +extern "C" SEXP c_cudd_bdd_largest_prime_unate(SEXP bdd_ptr, SEXP phases_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *phases = bdd_from_ptr(phases_ptr); + return bdd_to_xptr(bdd->LargestPrimeUnate(*phases)); +} + +extern "C" SEXP c_cudd_bdd_split_set(SEXP bdd_ptr, SEXP x_vars, SEXP m) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector vars = bdd_vector_from_list(x_vars, "x_vars"); + double value = Rf_asReal(m); + return bdd_to_xptr(bdd->SplitSet(vars, value)); +} + +extern "C" SEXP c_cudd_bdd_estimate_cofactor(SEXP bdd_ptr, SEXP index, SEXP phase) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int idx = Rf_asInteger(index); + int phase_val = Rf_asInteger(phase); + if (idx == NA_INTEGER || idx < 0 || phase_val == NA_INTEGER) { + Rf_error("'index' must be non-negative and 'phase' must be an integer."); + } + return Rf_ScalarInteger(bdd->EstimateCofactor(idx, phase_val)); +} + +extern "C" SEXP c_cudd_bdd_estimate_cofactor_simple(SEXP bdd_ptr, SEXP index) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int idx = Rf_asInteger(index); + if (idx == NA_INTEGER || idx < 0) { + Rf_error("'index' must be a non-negative integer."); + } + return Rf_ScalarInteger(bdd->EstimateCofactorSimple(idx)); +} + +extern "C" SEXP c_cudd_bdd_zdd_isop(SEXP bdd_ptr, SEXP upper_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *upper = bdd_from_ptr(upper_ptr); + ZDD *zdd = new ZDD(); + BDD result = bdd->zddIsop(*upper, zdd); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(result)); + SEXP zdd_ptr = PROTECT(R_MakeExternalPtr(zdd, R_NilValue, R_NilValue)); + R_RegisterCFinalizerEx(zdd_ptr, zdd_finalizer, TRUE); + SET_VECTOR_ELT(output, 1, zdd_ptr); + UNPROTECT(2); + return output; +} + +extern "C" SEXP c_cudd_bdd_transfer(SEXP bdd_ptr, SEXP mgr_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + Cudd *mgr = cudd_manager_from_ptr(mgr_ptr); + return bdd_to_xptr(bdd->Transfer(*mgr)); +} + extern "C" SEXP c_cudd_bdd_is_zero(SEXP bdd_ptr) { BDD *bdd = bdd_from_ptr(bdd_ptr); return Rf_ScalarLogical(bdd->IsZero()); diff --git a/src/rcudd.h b/src/rcudd.h index 5cab5df..717f773 100644 --- a/src/rcudd.h +++ b/src/rcudd.h @@ -43,6 +43,40 @@ extern "C" SEXP c_cudd_bdd_and(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_or(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_xor(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_restrict(SEXP bdd_ptr, SEXP constraint_ptr); +extern "C" SEXP c_cudd_bdd_is_one(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_is_cube(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_find_essential(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_print_two_literal_clauses(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_count_minterm(SEXP bdd_ptr, SEXP nvars); +extern "C" SEXP c_cudd_bdd_count_path(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_support(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_support_size(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_support_indices(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_classify_support(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_count_leaves(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_density(SEXP bdd_ptr, SEXP nvars); +extern "C" SEXP c_cudd_bdd_under_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP safe, SEXP quality); +extern "C" SEXP c_cudd_bdd_over_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP safe, SEXP quality); +extern "C" SEXP c_cudd_bdd_remap_under_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP quality); +extern "C" SEXP c_cudd_bdd_remap_over_approx(SEXP bdd_ptr, SEXP num_vars, SEXP threshold, SEXP quality); +extern "C" SEXP c_cudd_bdd_biased_under_approx(SEXP bdd_ptr, SEXP bias_ptr, SEXP num_vars, SEXP threshold, SEXP quality1, SEXP quality0); +extern "C" SEXP c_cudd_bdd_biased_over_approx(SEXP bdd_ptr, SEXP bias_ptr, SEXP num_vars, SEXP threshold, SEXP quality1, SEXP quality0); +extern "C" SEXP c_cudd_bdd_clipping_and(SEXP bdd_ptr, SEXP other_ptr, SEXP max_depth, SEXP direction); +extern "C" SEXP c_cudd_bdd_clipping_and_abstract(SEXP bdd_ptr, SEXP other_ptr, SEXP cube_ptr, SEXP max_depth, SEXP direction); +extern "C" SEXP c_cudd_bdd_var_are_symmetric(SEXP bdd_ptr, SEXP index1, SEXP index2); +extern "C" SEXP c_cudd_bdd_adj_permute_x(SEXP bdd_ptr, SEXP x_list); +extern "C" SEXP c_cudd_bdd_is_var_essential(SEXP bdd_ptr, SEXP index, SEXP phase); +extern "C" SEXP c_cudd_bdd_np_and(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_constrain_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_char_to_vect(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_leq_unless(SEXP bdd_ptr, SEXP g_ptr, SEXP d_ptr); +extern "C" SEXP c_cudd_bdd_maximally_expand(SEXP bdd_ptr, SEXP ub_ptr, SEXP f_ptr); +extern "C" SEXP c_cudd_bdd_largest_prime_unate(SEXP bdd_ptr, SEXP phases_ptr); +extern "C" SEXP c_cudd_bdd_split_set(SEXP bdd_ptr, SEXP x_vars, SEXP m); +extern "C" SEXP c_cudd_bdd_estimate_cofactor(SEXP bdd_ptr, SEXP index, SEXP phase); +extern "C" SEXP c_cudd_bdd_estimate_cofactor_simple(SEXP bdd_ptr, SEXP index); +extern "C" SEXP c_cudd_bdd_zdd_isop(SEXP bdd_ptr, SEXP upper_ptr); +extern "C" SEXP c_cudd_bdd_transfer(SEXP bdd_ptr, SEXP mgr_ptr); extern "C" SEXP c_cudd_bdd_is_zero(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_is_var(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_leq(SEXP lhs_ptr, SEXP rhs_ptr); diff --git a/src/register.cpp b/src/register.cpp index 6193f39..834ffea 100644 --- a/src/register.cpp +++ b/src/register.cpp @@ -40,6 +40,40 @@ static const R_CallMethodDef CallEntries[] = { {"c_cudd_bdd_or", (DL_FUNC) &c_cudd_bdd_or, 2}, {"c_cudd_bdd_xor", (DL_FUNC) &c_cudd_bdd_xor, 2}, {"c_cudd_bdd_restrict", (DL_FUNC) &c_cudd_bdd_restrict, 2}, + {"c_cudd_bdd_is_one", (DL_FUNC) &c_cudd_bdd_is_one, 1}, + {"c_cudd_bdd_is_cube", (DL_FUNC) &c_cudd_bdd_is_cube, 1}, + {"c_cudd_bdd_find_essential", (DL_FUNC) &c_cudd_bdd_find_essential, 1}, + {"c_cudd_bdd_print_two_literal_clauses", (DL_FUNC) &c_cudd_bdd_print_two_literal_clauses, 1}, + {"c_cudd_bdd_count_minterm", (DL_FUNC) &c_cudd_bdd_count_minterm, 2}, + {"c_cudd_bdd_count_path", (DL_FUNC) &c_cudd_bdd_count_path, 1}, + {"c_cudd_bdd_support", (DL_FUNC) &c_cudd_bdd_support, 1}, + {"c_cudd_bdd_support_size", (DL_FUNC) &c_cudd_bdd_support_size, 1}, + {"c_cudd_bdd_support_indices", (DL_FUNC) &c_cudd_bdd_support_indices, 1}, + {"c_cudd_bdd_classify_support", (DL_FUNC) &c_cudd_bdd_classify_support, 2}, + {"c_cudd_bdd_count_leaves", (DL_FUNC) &c_cudd_bdd_count_leaves, 1}, + {"c_cudd_bdd_density", (DL_FUNC) &c_cudd_bdd_density, 2}, + {"c_cudd_bdd_under_approx", (DL_FUNC) &c_cudd_bdd_under_approx, 5}, + {"c_cudd_bdd_over_approx", (DL_FUNC) &c_cudd_bdd_over_approx, 5}, + {"c_cudd_bdd_remap_under_approx", (DL_FUNC) &c_cudd_bdd_remap_under_approx, 4}, + {"c_cudd_bdd_remap_over_approx", (DL_FUNC) &c_cudd_bdd_remap_over_approx, 4}, + {"c_cudd_bdd_biased_under_approx", (DL_FUNC) &c_cudd_bdd_biased_under_approx, 6}, + {"c_cudd_bdd_biased_over_approx", (DL_FUNC) &c_cudd_bdd_biased_over_approx, 6}, + {"c_cudd_bdd_clipping_and", (DL_FUNC) &c_cudd_bdd_clipping_and, 4}, + {"c_cudd_bdd_clipping_and_abstract", (DL_FUNC) &c_cudd_bdd_clipping_and_abstract, 5}, + {"c_cudd_bdd_var_are_symmetric", (DL_FUNC) &c_cudd_bdd_var_are_symmetric, 3}, + {"c_cudd_bdd_adj_permute_x", (DL_FUNC) &c_cudd_bdd_adj_permute_x, 2}, + {"c_cudd_bdd_is_var_essential", (DL_FUNC) &c_cudd_bdd_is_var_essential, 3}, + {"c_cudd_bdd_np_and", (DL_FUNC) &c_cudd_bdd_np_and, 2}, + {"c_cudd_bdd_constrain_decomp", (DL_FUNC) &c_cudd_bdd_constrain_decomp, 1}, + {"c_cudd_bdd_char_to_vect", (DL_FUNC) &c_cudd_bdd_char_to_vect, 1}, + {"c_cudd_bdd_leq_unless", (DL_FUNC) &c_cudd_bdd_leq_unless, 3}, + {"c_cudd_bdd_maximally_expand", (DL_FUNC) &c_cudd_bdd_maximally_expand, 3}, + {"c_cudd_bdd_largest_prime_unate", (DL_FUNC) &c_cudd_bdd_largest_prime_unate, 2}, + {"c_cudd_bdd_split_set", (DL_FUNC) &c_cudd_bdd_split_set, 3}, + {"c_cudd_bdd_estimate_cofactor", (DL_FUNC) &c_cudd_bdd_estimate_cofactor, 3}, + {"c_cudd_bdd_estimate_cofactor_simple", (DL_FUNC) &c_cudd_bdd_estimate_cofactor_simple, 2}, + {"c_cudd_bdd_zdd_isop", (DL_FUNC) &c_cudd_bdd_zdd_isop, 2}, + {"c_cudd_bdd_transfer", (DL_FUNC) &c_cudd_bdd_transfer, 2}, {"c_cudd_bdd_is_zero", (DL_FUNC) &c_cudd_bdd_is_zero, 1}, {"c_cudd_bdd_is_var", (DL_FUNC) &c_cudd_bdd_is_var, 1}, {"c_cudd_bdd_leq", (DL_FUNC) &c_cudd_bdd_leq, 2}, diff --git a/tests/testthat/test_cudd_bdd_methods.R b/tests/testthat/test_cudd_bdd_methods.R new file mode 100644 index 0000000..4544374 --- /dev/null +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -0,0 +1,28 @@ +test_that("additional BDD methods are exposed", { + manager <- CuddManager() + vars <- lapply(1:3, function(i) cudd_bdd_var(manager)) + + bdd_one <- cudd_bdd_one(manager) + bdd_zero <- cudd_bdd_zero(manager) + bdd_or <- vars[[1L]] + vars[[2L]] + bdd_and <- vars[[1L]] * vars[[3L]] + + expect_true(cudd_bdd_is_one(bdd_one)) + expect_true(cudd_bdd_is_zero(bdd_zero)) + expect_true(cudd_bdd_is_var(vars[[1L]])) + expect_true(cudd_bdd_is_cube(vars[[1L]])) + expect_false(cudd_bdd_is_cube(bdd_or)) + + expect_equal(cudd_bdd_count_minterm(vars[[1L]], 3L), 4.0, tolerance = 1e-8) + expect_identical(cudd_bdd_support_size(bdd_and), 2L) + expect_identical(cudd_bdd_support_indices(bdd_and), c(0L, 2L)) + + classified <- cudd_bdd_classify_support(bdd_and, vars[[1L]]) + expect_named(classified, c("common", "only_bdd", "only_other")) + expect_true(methods::is(classified$common, "CuddBDD")) + + manager2 <- CuddManager() + transferred <- cudd_bdd_transfer(vars[[1L]], manager2) + expect_true(methods::is(transferred, "CuddBDD")) + expect_silent(transferred + cudd_bdd_var(manager2)) +}) From 26148a02b4dcb87deb8813e1d07f321fa6a6c246 Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Wed, 31 Dec 2025 22:44:30 +0100 Subject: [PATCH 3/8] Expose remaining BDD methods --- NAMESPACE | 23 ++ R/cudd_bdd_methods.R | 219 +++++++++++++++++- man/cudd_bdd_methods.Rd | 83 ++++++- src/cudd_manager.cpp | 301 +++++++++++++++++++++++++ src/rcudd.h | 23 ++ src/register.cpp | 23 ++ tests/testthat/test_cudd_bdd_methods.R | 13 ++ 7 files changed, 679 insertions(+), 6 deletions(-) diff --git a/NAMESPACE b/NAMESPACE index f73de16..9beee7b 100644 --- a/NAMESPACE +++ b/NAMESPACE @@ -19,6 +19,10 @@ export(cudd_background) export(cudd_bdd_adj_permute_x) export(cudd_bdd_and_abstract) export(cudd_bdd_and_limit) +export(cudd_bdd_apa_print_minterm) +export(cudd_bdd_apa_print_minterm_exp) +export(cudd_bdd_approx_conj_decomp) +export(cudd_bdd_approx_disj_decomp) export(cudd_bdd_biased_over_approx) export(cudd_bdd_biased_under_approx) export(cudd_bdd_bind_var) @@ -28,10 +32,13 @@ export(cudd_bdd_char_to_vect) export(cudd_bdd_classify_support) export(cudd_bdd_clipping_and) export(cudd_bdd_clipping_and_abstract) +export(cudd_bdd_cof_minterm) export(cudd_bdd_cofactor) export(cudd_bdd_compose) export(cudd_bdd_constrain) export(cudd_bdd_constrain_decomp) +export(cudd_bdd_correlation) +export(cudd_bdd_correlation_weights) export(cudd_bdd_count_leaves) export(cudd_bdd_count_minterm) export(cudd_bdd_count_path) @@ -39,12 +46,15 @@ export(cudd_bdd_decreasing) export(cudd_bdd_density) export(cudd_bdd_dump_dot) export(cudd_bdd_epd_print_minterm) +export(cudd_bdd_equiv_dc) export(cudd_bdd_estimate_cofactor) export(cudd_bdd_estimate_cofactor_simple) export(cudd_bdd_eval) export(cudd_bdd_exist_abstract) export(cudd_bdd_factored_form_string) export(cudd_bdd_find_essential) +export(cudd_bdd_gen_conj_decomp) +export(cudd_bdd_gen_disj_decomp) export(cudd_bdd_increasing) export(cudd_bdd_interpolate) export(cudd_bdd_intersect) @@ -56,7 +66,11 @@ export(cudd_bdd_is_zero) export(cudd_bdd_isop) export(cudd_bdd_ite) export(cudd_bdd_ite_constant) +export(cudd_bdd_iter_conj_decomp) +export(cudd_bdd_iter_disj_decomp) +export(cudd_bdd_largest_cube) export(cudd_bdd_largest_prime_unate) +export(cudd_bdd_ldbl_count_minterm) export(cudd_bdd_leq) export(cudd_bdd_leq_unless) export(cudd_bdd_li_compaction) @@ -75,6 +89,7 @@ export(cudd_bdd_permute) export(cudd_bdd_pick_one_cube) export(cudd_bdd_pick_one_minterm) export(cudd_bdd_port_to_zdd) +export(cudd_bdd_print) export(cudd_bdd_print_cover) export(cudd_bdd_print_cover_with_cube) export(cudd_bdd_print_debug) @@ -87,11 +102,15 @@ export(cudd_bdd_realignment_enabled) export(cudd_bdd_remap_over_approx) export(cudd_bdd_remap_under_approx) export(cudd_bdd_restrict) +export(cudd_bdd_shortest_length) +export(cudd_bdd_shortest_path) +export(cudd_bdd_solve_eqn) export(cudd_bdd_split_set) export(cudd_bdd_squeeze) export(cudd_bdd_subset_compress) export(cudd_bdd_subset_heavy_branch) export(cudd_bdd_subset_short_paths) +export(cudd_bdd_summary) export(cudd_bdd_superset_compress) export(cudd_bdd_superset_heavy_branch) export(cudd_bdd_superset_short_paths) @@ -108,11 +127,15 @@ export(cudd_bdd_under_approx) export(cudd_bdd_univ_abstract) export(cudd_bdd_var) export(cudd_bdd_var_are_symmetric) +export(cudd_bdd_var_conj_decomp) +export(cudd_bdd_var_disj_decomp) export(cudd_bdd_var_is_bound) export(cudd_bdd_var_is_dependent) export(cudd_bdd_vector_compose) +export(cudd_bdd_verify_sol) export(cudd_bdd_xnor) export(cudd_bdd_xor_exist_abstract) +export(cudd_bdd_xor_method) export(cudd_bdd_zdd_isop) export(cudd_bdd_zero) export(cudd_clear_error_code) diff --git a/R/cudd_bdd_methods.R b/R/cudd_bdd_methods.R index f9ffff1..8318c14 100644 --- a/R/cudd_bdd_methods.R +++ b/R/cudd_bdd_methods.R @@ -24,18 +24,22 @@ #' Convenience wrappers for additional methods on CUDD BDD objects. #' #' @param bdd A [`CuddBDD`] instance. -#' @param other,cube,var,g,h,upper,bias,phases,ub,f,d Additional [`CuddBDD`] +#' @param other,cube,var,g,h,upper,bias,phases,ub,f,d,y_bdd Additional [`CuddBDD`] #' instances used by the operation. #' @param manager A [`CuddManager`] instance. #' @param limit Optional non-negative integer limit passed to CUDD. #' @param index,index1,index2,phase Integer index values used by the operation. #' @param permut Integer vector describing a variable permutation. -#' @param x,y,vector,vars,x_vars Lists of [`CuddBDD`] instances. +#' @param x,y,vector,vars,x_vars,g_list Lists of [`CuddBDD`] instances. #' @param nvars,num_vars,threshold Non-negative integer values used by the operation. +#' @param weight Optional integer vector used in shortest path calculations. +#' @param mode,verbosity,precision Integer values used for reporting. #' @param max_depth,direction Integer values used by clipping operations. #' @param safe Logical scalar controlling approximate operations. #' @param quality,quality1,quality0 Numeric scalars controlling approximate operations. -#' @param minterm,inputs Integer vectors used by the operation. +#' @param minterm,inputs,y_index Integer vectors used by the operation. +#' @param prob Numeric vector of probabilities for correlation weights. +#' @param n Integer size for equation solving. #' @param upper_bound Integer upper bound for min hamming distance. #' @param hardlimit Logical scalar for short path routines. #' @param m Numeric scalar used by split operations. @@ -68,6 +72,85 @@ cudd_bdd_is_var <- function(bdd) { return(.Call(c_cudd_bdd_is_var, .cudd_bdd_ptr(bdd))) } +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_print <- function(bdd, nvars, verbosity = 1L) { + .Call(c_cudd_bdd_print, .cudd_bdd_ptr(bdd), nvars, verbosity) + return(invisible(NULL)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_summary <- function(bdd, nvars, mode = 0L) { + .Call(c_cudd_bdd_summary, .cudd_bdd_ptr(bdd), nvars, mode) + return(invisible(NULL)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_apa_print_minterm <- function(bdd, nvars) { + .Call(c_cudd_bdd_apa_print_minterm, .cudd_bdd_ptr(bdd), nvars) + return(invisible(NULL)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_apa_print_minterm_exp <- function(bdd, nvars, precision = 6L) { + .Call(c_cudd_bdd_apa_print_minterm_exp, .cudd_bdd_ptr(bdd), nvars, precision) + return(invisible(NULL)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_ldbl_count_minterm <- function(bdd, nvars) { + return(.Call(c_cudd_bdd_ldbl_count_minterm, .cudd_bdd_ptr(bdd), nvars)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_shortest_path <- function(bdd, weight = NULL) { + result <- .Call(c_cudd_bdd_shortest_path, .cudd_bdd_ptr(bdd), weight) + output <- list( + bdd = .cudd_bdd_wrap(result[[1L]], bdd), + support = result[[2L]], + length = result[[3L]] + ) + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_largest_cube <- function(bdd) { + result <- .Call(c_cudd_bdd_largest_cube, .cudd_bdd_ptr(bdd)) + output <- list( + bdd = .cudd_bdd_wrap(result[[1L]], bdd), + length = result[[2L]] + ) + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_shortest_length <- function(bdd, weight = NULL) { + return(.Call(c_cudd_bdd_shortest_length, .cudd_bdd_ptr(bdd), weight)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_equiv_dc <- function(bdd, g, d) { + if (!.cudd_check_same_manager(bdd, g, "EquivDC") || + !.cudd_check_same_manager(bdd, d, "EquivDC")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + return(.Call(c_cudd_bdd_equiv_dc, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(g), .cudd_bdd_ptr(d))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_cof_minterm <- function(bdd) { + return(.Call(c_cudd_bdd_cof_minterm, .cudd_bdd_ptr(bdd))) +} + #' @rdname cudd_bdd_methods #' @export cudd_bdd_find_essential <- function(bdd) { @@ -305,6 +388,34 @@ cudd_bdd_var_is_dependent <- function(bdd, var) { return(.Call(c_cudd_bdd_var_is_dependent, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(var))) } +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_correlation <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Correlation")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + return(.Call(c_cudd_bdd_correlation, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other))) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_correlation_weights <- function(bdd, other, prob) { + if (!.cudd_check_same_manager(bdd, other, "CorrelationWeights")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + return(.Call(c_cudd_bdd_correlation_weights, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other), prob)) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_xor_method <- function(bdd, other) { + if (!.cudd_check_same_manager(bdd, other, "Xor")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call(c_cudd_bdd_xor_method, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(other)) + return(.cudd_bdd_wrap(ptr, bdd)) +} + #' @rdname cudd_bdd_methods #' @export cudd_bdd_ite <- function(bdd, g, h, limit = 0L) { @@ -451,6 +562,78 @@ cudd_bdd_vector_compose <- function(bdd, vector) { return(.cudd_bdd_wrap(ptr, bdd)) } +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_approx_conj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_approx_conj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_approx_disj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_approx_disj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_iter_conj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_iter_conj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_iter_disj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_iter_disj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_gen_conj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_gen_conj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_gen_disj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_gen_disj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_var_conj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_var_conj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_var_disj_decomp <- function(bdd) { + result <- .Call(c_cudd_bdd_var_disj_decomp, .cudd_bdd_ptr(bdd)) + output <- .cudd_bdd_wrap_list(result, bdd) + names(output) <- c("g", "h") + return(output) +} + #' @rdname cudd_bdd_methods #' @export cudd_bdd_li_compaction <- function(bdd, other) { @@ -771,6 +954,36 @@ cudd_bdd_largest_prime_unate <- function(bdd, phases) { return(.cudd_bdd_wrap(ptr, bdd)) } +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_solve_eqn <- function(bdd, y_bdd, n) { + if (!.cudd_check_same_manager(bdd, y_bdd, "SolveEqn")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + result <- .Call(c_cudd_bdd_solve_eqn, .cudd_bdd_ptr(bdd), .cudd_bdd_ptr(y_bdd), n) + output <- list( + bdd = .cudd_bdd_wrap(result[[1L]], bdd), + g = .cudd_bdd_wrap_list(result[[2L]], bdd), + y_index = result[[3L]] + ) + return(output) +} + +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_verify_sol <- function(bdd, g_list, y_index) { + if (!.cudd_check_bdd_list_manager(bdd, g_list, "VerifySol")) { + stop("Cannot combine BDDs from different CuddManager instances.", call. = FALSE) + } + ptr <- .Call( + c_cudd_bdd_verify_sol, + .cudd_bdd_ptr(bdd), + lapply(g_list, .cudd_bdd_ptr), + y_index + ) + return(.cudd_bdd_wrap(ptr, bdd)) +} + #' @rdname cudd_bdd_methods #' @export cudd_bdd_split_set <- function(bdd, x_vars, m) { diff --git a/man/cudd_bdd_methods.Rd b/man/cudd_bdd_methods.Rd index 58bb1a7..09f492c 100644 --- a/man/cudd_bdd_methods.Rd +++ b/man/cudd_bdd_methods.Rd @@ -6,6 +6,16 @@ \alias{cudd_bdd_is_one} \alias{cudd_bdd_is_cube} \alias{cudd_bdd_is_var} +\alias{cudd_bdd_print} +\alias{cudd_bdd_summary} +\alias{cudd_bdd_apa_print_minterm} +\alias{cudd_bdd_apa_print_minterm_exp} +\alias{cudd_bdd_ldbl_count_minterm} +\alias{cudd_bdd_shortest_path} +\alias{cudd_bdd_largest_cube} +\alias{cudd_bdd_shortest_length} +\alias{cudd_bdd_equiv_dc} +\alias{cudd_bdd_cof_minterm} \alias{cudd_bdd_find_essential} \alias{cudd_bdd_print_two_literal_clauses} \alias{cudd_bdd_count_minterm} @@ -29,6 +39,9 @@ \alias{cudd_bdd_xor_exist_abstract} \alias{cudd_bdd_boolean_diff} \alias{cudd_bdd_var_is_dependent} +\alias{cudd_bdd_correlation} +\alias{cudd_bdd_correlation_weights} +\alias{cudd_bdd_xor_method} \alias{cudd_bdd_ite} \alias{cudd_bdd_ite_constant} \alias{cudd_bdd_intersect} @@ -43,6 +56,14 @@ \alias{cudd_bdd_permute} \alias{cudd_bdd_swap_variables} \alias{cudd_bdd_vector_compose} +\alias{cudd_bdd_approx_conj_decomp} +\alias{cudd_bdd_approx_disj_decomp} +\alias{cudd_bdd_iter_conj_decomp} +\alias{cudd_bdd_iter_disj_decomp} +\alias{cudd_bdd_gen_conj_decomp} +\alias{cudd_bdd_gen_disj_decomp} +\alias{cudd_bdd_var_conj_decomp} +\alias{cudd_bdd_var_disj_decomp} \alias{cudd_bdd_li_compaction} \alias{cudd_bdd_squeeze} \alias{cudd_bdd_interpolate} @@ -79,6 +100,8 @@ \alias{cudd_bdd_leq_unless} \alias{cudd_bdd_maximally_expand} \alias{cudd_bdd_largest_prime_unate} +\alias{cudd_bdd_solve_eqn} +\alias{cudd_bdd_verify_sol} \alias{cudd_bdd_split_set} \alias{cudd_bdd_estimate_cofactor} \alias{cudd_bdd_estimate_cofactor_simple} @@ -94,6 +117,26 @@ cudd_bdd_is_cube(bdd) cudd_bdd_is_var(bdd) +cudd_bdd_print(bdd, nvars, verbosity = 1L) + +cudd_bdd_summary(bdd, nvars, mode = 0L) + +cudd_bdd_apa_print_minterm(bdd, nvars) + +cudd_bdd_apa_print_minterm_exp(bdd, nvars, precision = 6L) + +cudd_bdd_ldbl_count_minterm(bdd, nvars) + +cudd_bdd_shortest_path(bdd, weight = NULL) + +cudd_bdd_largest_cube(bdd) + +cudd_bdd_shortest_length(bdd, weight = NULL) + +cudd_bdd_equiv_dc(bdd, g, d) + +cudd_bdd_cof_minterm(bdd) + cudd_bdd_find_essential(bdd) cudd_bdd_print_two_literal_clauses(bdd) @@ -154,6 +197,12 @@ cudd_bdd_boolean_diff(bdd, index) cudd_bdd_var_is_dependent(bdd, var) +cudd_bdd_correlation(bdd, other) + +cudd_bdd_correlation_weights(bdd, other, prob) + +cudd_bdd_xor_method(bdd, other) + cudd_bdd_ite(bdd, g, h, limit = 0L) cudd_bdd_ite_constant(bdd, g, h) @@ -182,6 +231,22 @@ cudd_bdd_swap_variables(bdd, x, y) cudd_bdd_vector_compose(bdd, vector) +cudd_bdd_approx_conj_decomp(bdd) + +cudd_bdd_approx_disj_decomp(bdd) + +cudd_bdd_iter_conj_decomp(bdd) + +cudd_bdd_iter_disj_decomp(bdd) + +cudd_bdd_gen_conj_decomp(bdd) + +cudd_bdd_gen_disj_decomp(bdd) + +cudd_bdd_var_conj_decomp(bdd) + +cudd_bdd_var_disj_decomp(bdd) + cudd_bdd_li_compaction(bdd, other) cudd_bdd_squeeze(bdd, other) @@ -254,6 +319,10 @@ cudd_bdd_maximally_expand(bdd, ub, f) cudd_bdd_largest_prime_unate(bdd, phases) +cudd_bdd_solve_eqn(bdd, y_bdd, n) + +cudd_bdd_verify_sol(bdd, g_list, y_index) + cudd_bdd_split_set(bdd, x_vars, m) cudd_bdd_estimate_cofactor(bdd, index, phase) @@ -269,7 +338,11 @@ cudd_bdd_transfer(bdd, manager) \item{nvars, num_vars, threshold}{Non-negative integer values used by the operation.} -\item{other, cube, var, g, h, upper, bias, phases, ub, f, d}{Additional [`CuddBDD`] +\item{mode, verbosity, precision}{Integer values used for reporting.} + +\item{weight}{Optional integer vector used in shortest path calculations.} + +\item{other, cube, var, g, h, upper, bias, phases, ub, f, d, y_bdd}{Additional [`CuddBDD`] instances used by the operation.} \item{safe}{Logical scalar controlling approximate operations.} @@ -280,11 +353,13 @@ instances used by the operation.} \item{index, index1, index2, phase}{Integer index values used by the operation.} +\item{prob}{Numeric vector of probabilities for correlation weights.} + \item{permut}{Integer vector describing a variable permutation.} -\item{x, y, vector, vars, x_vars}{Lists of [`CuddBDD`] instances.} +\item{x, y, vector, vars, x_vars, g_list}{Lists of [`CuddBDD`] instances.} -\item{minterm, inputs}{Integer vectors used by the operation.} +\item{minterm, inputs, y_index}{Integer vectors used by the operation.} \item{upper_bound}{Integer upper bound for min hamming distance.} @@ -292,6 +367,8 @@ instances used by the operation.} \item{max_depth, direction}{Integer values used by clipping operations.} +\item{n}{Integer size for equation solving.} + \item{m}{Numeric scalar used by split operations.} \item{manager}{A [`CuddManager`] instance.} diff --git a/src/cudd_manager.cpp b/src/cudd_manager.cpp index e70ff45..dbcfdec 100644 --- a/src/cudd_manager.cpp +++ b/src/cudd_manager.cpp @@ -2,6 +2,7 @@ #include #include #include +#include #include #include #include "cuddObj.hh" @@ -163,6 +164,23 @@ static SEXP int_vector_to_sexp(const std::vector &values) { return vec; } +static std::vector double_vector_from_sexp(SEXP vec, const char *name) { + if (!Rf_isReal(vec)) { + Rf_error("'%s' must be a numeric vector.", name); + } + R_xlen_t size = Rf_xlength(vec); + std::vector result; + result.reserve(static_cast(size)); + for (R_xlen_t i = 0; i < size; ++i) { + double value = REAL(vec)[i]; + if (ISNA(value)) { + Rf_error("'%s' must not contain NA.", name); + } + result.push_back(value); + } + return result; +} + extern "C" SEXP c_cudd_new() { try { Cudd *mgr = new Cudd(); @@ -1104,6 +1122,136 @@ extern "C" SEXP c_cudd_bdd_restrict(SEXP bdd_ptr, SEXP constraint_ptr) { return ptr; } +extern "C" SEXP c_cudd_bdd_print(SEXP bdd_ptr, SEXP nvars, SEXP verbosity) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + int verb = Rf_asInteger(verbosity); + if (vars == NA_INTEGER || vars < 0 || verb == NA_INTEGER) { + Rf_error("'nvars' must be non-negative and 'verbosity' must be an integer."); + } + bdd->print(vars, verb); + return R_NilValue; +} + +extern "C" SEXP c_cudd_bdd_summary(SEXP bdd_ptr, SEXP nvars, SEXP mode) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + int summary_mode = Rf_asInteger(mode); + if (vars == NA_INTEGER || vars < 0 || summary_mode == NA_INTEGER) { + Rf_error("'nvars' must be non-negative and 'mode' must be an integer."); + } + bdd->summary(vars, summary_mode); + return R_NilValue; +} + +extern "C" SEXP c_cudd_bdd_apa_print_minterm(SEXP bdd_ptr, SEXP nvars) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + if (vars == NA_INTEGER || vars < 0) { + Rf_error("'nvars' must be a non-negative integer."); + } + bdd->ApaPrintMinterm(vars); + return R_NilValue; +} + +extern "C" SEXP c_cudd_bdd_apa_print_minterm_exp(SEXP bdd_ptr, SEXP nvars, SEXP precision) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + int prec = Rf_asInteger(precision); + if (vars == NA_INTEGER || vars < 0 || prec == NA_INTEGER) { + Rf_error("'nvars' must be non-negative and 'precision' must be an integer."); + } + bdd->ApaPrintMintermExp(vars, prec); + return R_NilValue; +} + +extern "C" SEXP c_cudd_bdd_ldbl_count_minterm(SEXP bdd_ptr, SEXP nvars) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int vars = Rf_asInteger(nvars); + if (vars == NA_INTEGER || vars < 0) { + Rf_error("'nvars' must be a non-negative integer."); + } + long double count = bdd->LdblCountMinterm(vars); + return Rf_ScalarReal(static_cast(count)); +} + +extern "C" SEXP c_cudd_bdd_shortest_path(SEXP bdd_ptr, SEXP weight) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int size = Cudd_ReadSize(bdd->manager()); + std::vector weight_vec; + int *weight_ptr = nullptr; + if (!Rf_isNull(weight)) { + weight_vec = int_vector_from_sexp(weight, "weight"); + if (static_cast(weight_vec.size()) != size) { + Rf_error("'weight' must have length %d.", size); + } + weight_ptr = weight_vec.data(); + } + std::vector support(static_cast(size), 0); + int length = 0; + BDD result = bdd->ShortestPath(weight_ptr, support.data(), &length); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 3)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(result)); + SEXP support_vec = PROTECT(Rf_allocVector(INTSXP, size)); + for (int i = 0; i < size; ++i) { + INTEGER(support_vec)[i] = support[static_cast(i)]; + } + SET_VECTOR_ELT(output, 1, support_vec); + SET_VECTOR_ELT(output, 2, Rf_ScalarInteger(length)); + UNPROTECT(2); + return output; +} + +extern "C" SEXP c_cudd_bdd_largest_cube(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int length = 0; + BDD result = bdd->LargestCube(&length); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(result)); + SET_VECTOR_ELT(output, 1, Rf_ScalarInteger(length)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_shortest_length(SEXP bdd_ptr, SEXP weight) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int size = Cudd_ReadSize(bdd->manager()); + std::vector weight_vec; + int *weight_ptr = nullptr; + if (!Rf_isNull(weight)) { + weight_vec = int_vector_from_sexp(weight, "weight"); + if (static_cast(weight_vec.size()) != size) { + Rf_error("'weight' must have length %d.", size); + } + weight_ptr = weight_vec.data(); + } + int result = bdd->ShortestLength(weight_ptr); + return Rf_ScalarInteger(result); +} + +extern "C" SEXP c_cudd_bdd_equiv_dc(SEXP bdd_ptr, SEXP g_ptr, SEXP d_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *g = bdd_from_ptr(g_ptr); + BDD *d = bdd_from_ptr(d_ptr); + return Rf_ScalarLogical(bdd->EquivDC(*g, *d)); +} + +extern "C" SEXP c_cudd_bdd_cof_minterm(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + int size = Cudd_ReadSize(bdd->manager()); + double *values = bdd->CofMinterm(); + if (values == nullptr) { + Rf_error("Failed to compute cofactor minterms."); + } + SEXP output = PROTECT(Rf_allocVector(REALSXP, size + 1)); + for (int i = 0; i < size + 1; ++i) { + REAL(output)[i] = values[i]; + } + free(values); + UNPROTECT(1); + return output; +} + extern "C" SEXP c_cudd_bdd_is_one(SEXP bdd_ptr) { BDD *bdd = bdd_from_ptr(bdd_ptr); return Rf_ScalarLogical(bdd->IsOne()); @@ -1343,6 +1491,39 @@ extern "C" SEXP c_cudd_bdd_largest_prime_unate(SEXP bdd_ptr, SEXP phases_ptr) { return bdd_to_xptr(bdd->LargestPrimeUnate(*phases)); } +extern "C" SEXP c_cudd_bdd_solve_eqn(SEXP bdd_ptr, SEXP y_ptr, SEXP n) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *y = bdd_from_ptr(y_ptr); + int count = Rf_asInteger(n); + if (count == NA_INTEGER || count < 0) { + Rf_error("'n' must be a non-negative integer."); + } + std::vector g; + int *y_index = nullptr; + BDD result = bdd->SolveEqn(*y, g, &y_index, count); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 3)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(result)); + SET_VECTOR_ELT(output, 1, bdd_list_from_vector(g)); + SEXP y_index_vec = PROTECT(Rf_allocVector(INTSXP, count)); + for (int i = 0; i < count; ++i) { + INTEGER(y_index_vec)[i] = y_index[i]; + } + SET_VECTOR_ELT(output, 2, y_index_vec); + if (y_index != nullptr) { + free(y_index); + } + UNPROTECT(2); + return output; +} + +extern "C" SEXP c_cudd_bdd_verify_sol(SEXP bdd_ptr, SEXP g_list, SEXP y_index) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::vector g = bdd_vector_from_list(g_list, "g"); + std::vector y_index_vec = int_vector_from_sexp(y_index, "y_index"); + BDD result = bdd->VerifySol(g, y_index_vec.data()); + return bdd_to_xptr(result); +} + extern "C" SEXP c_cudd_bdd_split_set(SEXP bdd_ptr, SEXP x_vars, SEXP m) { BDD *bdd = bdd_from_ptr(bdd_ptr); std::vector vars = bdd_vector_from_list(x_vars, "x_vars"); @@ -1448,6 +1629,30 @@ extern "C" SEXP c_cudd_bdd_var_is_dependent(SEXP bdd_ptr, SEXP var_ptr) { return Rf_ScalarLogical(bdd->VarIsDependent(*var)); } +extern "C" SEXP c_cudd_bdd_correlation(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return Rf_ScalarReal(bdd->Correlation(*other)); +} + +extern "C" SEXP c_cudd_bdd_correlation_weights(SEXP bdd_ptr, SEXP other_ptr, SEXP prob) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + std::vector prob_vec = double_vector_from_sexp(prob, "prob"); + int size = Cudd_ReadSize(bdd->manager()); + if (static_cast(prob_vec.size()) != size) { + Rf_error("'prob' must have length %d.", size); + } + double corr = bdd->CorrelationWeights(*other, prob_vec.data()); + return Rf_ScalarReal(corr); +} + +extern "C" SEXP c_cudd_bdd_xor_method(SEXP bdd_ptr, SEXP other_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD *other = bdd_from_ptr(other_ptr); + return bdd_to_xptr(bdd->Xor(*other)); +} + extern "C" SEXP c_cudd_bdd_ite(SEXP bdd_ptr, SEXP g_ptr, SEXP h_ptr, SEXP limit) { BDD *bdd = bdd_from_ptr(bdd_ptr); BDD *g = bdd_from_ptr(g_ptr); @@ -1543,6 +1748,102 @@ extern "C" SEXP c_cudd_bdd_vector_compose(SEXP bdd_ptr, SEXP vector_list) { return bdd_to_xptr(bdd->VectorCompose(vec)); } +extern "C" SEXP c_cudd_bdd_approx_conj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->ApproxConjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_approx_disj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->ApproxDisjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_iter_conj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->IterConjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_iter_disj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->IterDisjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_gen_conj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->GenConjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_gen_disj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->GenDisjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_var_conj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->VarConjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + +extern "C" SEXP c_cudd_bdd_var_disj_decomp(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + BDD g; + BDD h; + bdd->VarDisjDecomp(&g, &h); + SEXP output = PROTECT(Rf_allocVector(VECSXP, 2)); + SET_VECTOR_ELT(output, 0, bdd_to_xptr(g)); + SET_VECTOR_ELT(output, 1, bdd_to_xptr(h)); + UNPROTECT(1); + return output; +} + extern "C" SEXP c_cudd_bdd_li_compaction(SEXP bdd_ptr, SEXP other_ptr) { BDD *bdd = bdd_from_ptr(bdd_ptr); BDD *other = bdd_from_ptr(other_ptr); diff --git a/src/rcudd.h b/src/rcudd.h index 717f773..8e22c53 100644 --- a/src/rcudd.h +++ b/src/rcudd.h @@ -43,6 +43,16 @@ extern "C" SEXP c_cudd_bdd_and(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_or(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_xor(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_restrict(SEXP bdd_ptr, SEXP constraint_ptr); +extern "C" SEXP c_cudd_bdd_print(SEXP bdd_ptr, SEXP nvars, SEXP verbosity); +extern "C" SEXP c_cudd_bdd_summary(SEXP bdd_ptr, SEXP nvars, SEXP mode); +extern "C" SEXP c_cudd_bdd_apa_print_minterm(SEXP bdd_ptr, SEXP nvars); +extern "C" SEXP c_cudd_bdd_apa_print_minterm_exp(SEXP bdd_ptr, SEXP nvars, SEXP precision); +extern "C" SEXP c_cudd_bdd_ldbl_count_minterm(SEXP bdd_ptr, SEXP nvars); +extern "C" SEXP c_cudd_bdd_shortest_path(SEXP bdd_ptr, SEXP weight); +extern "C" SEXP c_cudd_bdd_largest_cube(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_shortest_length(SEXP bdd_ptr, SEXP weight); +extern "C" SEXP c_cudd_bdd_equiv_dc(SEXP bdd_ptr, SEXP g_ptr, SEXP d_ptr); +extern "C" SEXP c_cudd_bdd_cof_minterm(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_is_one(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_is_cube(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_find_essential(SEXP bdd_ptr); @@ -72,6 +82,8 @@ extern "C" SEXP c_cudd_bdd_char_to_vect(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_leq_unless(SEXP bdd_ptr, SEXP g_ptr, SEXP d_ptr); extern "C" SEXP c_cudd_bdd_maximally_expand(SEXP bdd_ptr, SEXP ub_ptr, SEXP f_ptr); extern "C" SEXP c_cudd_bdd_largest_prime_unate(SEXP bdd_ptr, SEXP phases_ptr); +extern "C" SEXP c_cudd_bdd_solve_eqn(SEXP bdd_ptr, SEXP y_ptr, SEXP n); +extern "C" SEXP c_cudd_bdd_verify_sol(SEXP bdd_ptr, SEXP g_list, SEXP y_index); extern "C" SEXP c_cudd_bdd_split_set(SEXP bdd_ptr, SEXP x_vars, SEXP m); extern "C" SEXP c_cudd_bdd_estimate_cofactor(SEXP bdd_ptr, SEXP index, SEXP phase); extern "C" SEXP c_cudd_bdd_estimate_cofactor_simple(SEXP bdd_ptr, SEXP index); @@ -86,6 +98,9 @@ extern "C" SEXP c_cudd_bdd_univ_abstract(SEXP bdd_ptr, SEXP cube_ptr); extern "C" SEXP c_cudd_bdd_xor_exist_abstract(SEXP bdd_ptr, SEXP other_ptr, SEXP cube_ptr); extern "C" SEXP c_cudd_bdd_boolean_diff(SEXP bdd_ptr, SEXP index); extern "C" SEXP c_cudd_bdd_var_is_dependent(SEXP bdd_ptr, SEXP var_ptr); +extern "C" SEXP c_cudd_bdd_correlation(SEXP bdd_ptr, SEXP other_ptr); +extern "C" SEXP c_cudd_bdd_correlation_weights(SEXP bdd_ptr, SEXP other_ptr, SEXP prob); +extern "C" SEXP c_cudd_bdd_xor_method(SEXP bdd_ptr, SEXP other_ptr); extern "C" SEXP c_cudd_bdd_ite(SEXP bdd_ptr, SEXP g_ptr, SEXP h_ptr, SEXP limit); extern "C" SEXP c_cudd_bdd_ite_constant(SEXP bdd_ptr, SEXP g_ptr, SEXP h_ptr); extern "C" SEXP c_cudd_bdd_intersect(SEXP bdd_ptr, SEXP other_ptr); @@ -100,6 +115,14 @@ extern "C" SEXP c_cudd_bdd_compose(SEXP bdd_ptr, SEXP other_ptr, SEXP index); extern "C" SEXP c_cudd_bdd_permute(SEXP bdd_ptr, SEXP permut); extern "C" SEXP c_cudd_bdd_swap_variables(SEXP bdd_ptr, SEXP x_list, SEXP y_list); extern "C" SEXP c_cudd_bdd_vector_compose(SEXP bdd_ptr, SEXP vector_list); +extern "C" SEXP c_cudd_bdd_approx_conj_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_approx_disj_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_iter_conj_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_iter_disj_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_gen_conj_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_gen_disj_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_var_conj_decomp(SEXP bdd_ptr); +extern "C" SEXP c_cudd_bdd_var_disj_decomp(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_li_compaction(SEXP bdd_ptr, SEXP other_ptr); extern "C" SEXP c_cudd_bdd_squeeze(SEXP bdd_ptr, SEXP other_ptr); extern "C" SEXP c_cudd_bdd_interpolate(SEXP bdd_ptr, SEXP other_ptr); diff --git a/src/register.cpp b/src/register.cpp index 834ffea..3d6dbf1 100644 --- a/src/register.cpp +++ b/src/register.cpp @@ -40,6 +40,16 @@ static const R_CallMethodDef CallEntries[] = { {"c_cudd_bdd_or", (DL_FUNC) &c_cudd_bdd_or, 2}, {"c_cudd_bdd_xor", (DL_FUNC) &c_cudd_bdd_xor, 2}, {"c_cudd_bdd_restrict", (DL_FUNC) &c_cudd_bdd_restrict, 2}, + {"c_cudd_bdd_print", (DL_FUNC) &c_cudd_bdd_print, 3}, + {"c_cudd_bdd_summary", (DL_FUNC) &c_cudd_bdd_summary, 3}, + {"c_cudd_bdd_apa_print_minterm", (DL_FUNC) &c_cudd_bdd_apa_print_minterm, 2}, + {"c_cudd_bdd_apa_print_minterm_exp", (DL_FUNC) &c_cudd_bdd_apa_print_minterm_exp, 3}, + {"c_cudd_bdd_ldbl_count_minterm", (DL_FUNC) &c_cudd_bdd_ldbl_count_minterm, 2}, + {"c_cudd_bdd_shortest_path", (DL_FUNC) &c_cudd_bdd_shortest_path, 2}, + {"c_cudd_bdd_largest_cube", (DL_FUNC) &c_cudd_bdd_largest_cube, 1}, + {"c_cudd_bdd_shortest_length", (DL_FUNC) &c_cudd_bdd_shortest_length, 2}, + {"c_cudd_bdd_equiv_dc", (DL_FUNC) &c_cudd_bdd_equiv_dc, 3}, + {"c_cudd_bdd_cof_minterm", (DL_FUNC) &c_cudd_bdd_cof_minterm, 1}, {"c_cudd_bdd_is_one", (DL_FUNC) &c_cudd_bdd_is_one, 1}, {"c_cudd_bdd_is_cube", (DL_FUNC) &c_cudd_bdd_is_cube, 1}, {"c_cudd_bdd_find_essential", (DL_FUNC) &c_cudd_bdd_find_essential, 1}, @@ -69,6 +79,8 @@ static const R_CallMethodDef CallEntries[] = { {"c_cudd_bdd_leq_unless", (DL_FUNC) &c_cudd_bdd_leq_unless, 3}, {"c_cudd_bdd_maximally_expand", (DL_FUNC) &c_cudd_bdd_maximally_expand, 3}, {"c_cudd_bdd_largest_prime_unate", (DL_FUNC) &c_cudd_bdd_largest_prime_unate, 2}, + {"c_cudd_bdd_solve_eqn", (DL_FUNC) &c_cudd_bdd_solve_eqn, 3}, + {"c_cudd_bdd_verify_sol", (DL_FUNC) &c_cudd_bdd_verify_sol, 3}, {"c_cudd_bdd_split_set", (DL_FUNC) &c_cudd_bdd_split_set, 3}, {"c_cudd_bdd_estimate_cofactor", (DL_FUNC) &c_cudd_bdd_estimate_cofactor, 3}, {"c_cudd_bdd_estimate_cofactor_simple", (DL_FUNC) &c_cudd_bdd_estimate_cofactor_simple, 2}, @@ -83,6 +95,9 @@ static const R_CallMethodDef CallEntries[] = { {"c_cudd_bdd_xor_exist_abstract", (DL_FUNC) &c_cudd_bdd_xor_exist_abstract, 3}, {"c_cudd_bdd_boolean_diff", (DL_FUNC) &c_cudd_bdd_boolean_diff, 2}, {"c_cudd_bdd_var_is_dependent", (DL_FUNC) &c_cudd_bdd_var_is_dependent, 2}, + {"c_cudd_bdd_correlation", (DL_FUNC) &c_cudd_bdd_correlation, 2}, + {"c_cudd_bdd_correlation_weights", (DL_FUNC) &c_cudd_bdd_correlation_weights, 3}, + {"c_cudd_bdd_xor_method", (DL_FUNC) &c_cudd_bdd_xor_method, 2}, {"c_cudd_bdd_ite", (DL_FUNC) &c_cudd_bdd_ite, 4}, {"c_cudd_bdd_ite_constant", (DL_FUNC) &c_cudd_bdd_ite_constant, 3}, {"c_cudd_bdd_intersect", (DL_FUNC) &c_cudd_bdd_intersect, 2}, @@ -97,6 +112,14 @@ static const R_CallMethodDef CallEntries[] = { {"c_cudd_bdd_permute", (DL_FUNC) &c_cudd_bdd_permute, 2}, {"c_cudd_bdd_swap_variables", (DL_FUNC) &c_cudd_bdd_swap_variables, 3}, {"c_cudd_bdd_vector_compose", (DL_FUNC) &c_cudd_bdd_vector_compose, 2}, + {"c_cudd_bdd_approx_conj_decomp", (DL_FUNC) &c_cudd_bdd_approx_conj_decomp, 1}, + {"c_cudd_bdd_approx_disj_decomp", (DL_FUNC) &c_cudd_bdd_approx_disj_decomp, 1}, + {"c_cudd_bdd_iter_conj_decomp", (DL_FUNC) &c_cudd_bdd_iter_conj_decomp, 1}, + {"c_cudd_bdd_iter_disj_decomp", (DL_FUNC) &c_cudd_bdd_iter_disj_decomp, 1}, + {"c_cudd_bdd_gen_conj_decomp", (DL_FUNC) &c_cudd_bdd_gen_conj_decomp, 1}, + {"c_cudd_bdd_gen_disj_decomp", (DL_FUNC) &c_cudd_bdd_gen_disj_decomp, 1}, + {"c_cudd_bdd_var_conj_decomp", (DL_FUNC) &c_cudd_bdd_var_conj_decomp, 1}, + {"c_cudd_bdd_var_disj_decomp", (DL_FUNC) &c_cudd_bdd_var_disj_decomp, 1}, {"c_cudd_bdd_li_compaction", (DL_FUNC) &c_cudd_bdd_li_compaction, 2}, {"c_cudd_bdd_squeeze", (DL_FUNC) &c_cudd_bdd_squeeze, 2}, {"c_cudd_bdd_interpolate", (DL_FUNC) &c_cudd_bdd_interpolate, 2}, diff --git a/tests/testthat/test_cudd_bdd_methods.R b/tests/testthat/test_cudd_bdd_methods.R index 4544374..3d4cc84 100644 --- a/tests/testthat/test_cudd_bdd_methods.R +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -21,6 +21,19 @@ test_that("additional BDD methods are exposed", { expect_named(classified, c("common", "only_bdd", "only_other")) expect_true(methods::is(classified$common, "CuddBDD")) + expect_silent(cudd_bdd_print(bdd_or, 3L)) + expect_silent(cudd_bdd_summary(bdd_or, 3L)) + + expect_equal(cudd_bdd_correlation(vars[[1L]], vars[[1L]]), 1.0) + expect_equal( + cudd_bdd_correlation_weights(vars[[1L]], vars[[1L]], rep(0.5, 3L)), + 1.0 + ) + + shortest_length <- cudd_bdd_shortest_length(vars[[1L]]) + expect_type(shortest_length, "integer") + expect_gte(shortest_length, 0L) + manager2 <- CuddManager() transferred <- cudd_bdd_transfer(vars[[1L]], manager2) expect_true(methods::is(transferred, "CuddBDD")) From a7756510ef8bd786202654242b6017dccf28fb22 Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Wed, 31 Dec 2025 22:44:37 +0100 Subject: [PATCH 4/8] Add snapshot for cudd_bdd_print --- tests/testthat/_snaps/cudd_bdd_methods.md | 4 ++++ tests/testthat/test_cudd_bdd_methods.R | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) create mode 100644 tests/testthat/_snaps/cudd_bdd_methods.md diff --git a/tests/testthat/_snaps/cudd_bdd_methods.md b/tests/testthat/_snaps/cudd_bdd_methods.md new file mode 100644 index 0000000..4fee794 --- /dev/null +++ b/tests/testthat/_snaps/cudd_bdd_methods.md @@ -0,0 +1,4 @@ +# additional BDD methods are exposed + + + diff --git a/tests/testthat/test_cudd_bdd_methods.R b/tests/testthat/test_cudd_bdd_methods.R index 3d4cc84..72b2035 100644 --- a/tests/testthat/test_cudd_bdd_methods.R +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -21,7 +21,7 @@ test_that("additional BDD methods are exposed", { expect_named(classified, c("common", "only_bdd", "only_other")) expect_true(methods::is(classified$common, "CuddBDD")) - expect_silent(cudd_bdd_print(bdd_or, 3L)) + expect_snapshot_output(cudd_bdd_print(bdd_or, 3L)) expect_silent(cudd_bdd_summary(bdd_or, 3L)) expect_equal(cudd_bdd_correlation(vars[[1L]], vars[[1L]]), 1.0) From e6a2f69321d63820bd4e248316d594a97b2229bc Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Thu, 1 Jan 2026 17:46:54 +0100 Subject: [PATCH 5/8] Add ITE formula helper for BDDs --- NAMESPACE | 1 + R/cudd_bdd_methods.R | 6 +++ man/cudd_bdd_methods.Rd | 3 ++ src/cudd_manager.cpp | 51 ++++++++++++++++++++++++++ src/rcudd.h | 1 + src/register.cpp | 1 + tests/testthat/test_cudd_bdd_methods.R | 1 + 7 files changed, 64 insertions(+) diff --git a/NAMESPACE b/NAMESPACE index 9beee7b..76446a8 100644 --- a/NAMESPACE +++ b/NAMESPACE @@ -66,6 +66,7 @@ export(cudd_bdd_is_zero) export(cudd_bdd_isop) export(cudd_bdd_ite) export(cudd_bdd_ite_constant) +export(cudd_bdd_ite_formula) export(cudd_bdd_iter_conj_decomp) export(cudd_bdd_iter_disj_decomp) export(cudd_bdd_largest_cube) diff --git a/R/cudd_bdd_methods.R b/R/cudd_bdd_methods.R index 8318c14..f696ee6 100644 --- a/R/cudd_bdd_methods.R +++ b/R/cudd_bdd_methods.R @@ -72,6 +72,12 @@ cudd_bdd_is_var <- function(bdd) { return(.Call(c_cudd_bdd_is_var, .cudd_bdd_ptr(bdd))) } +#' @rdname cudd_bdd_methods +#' @export +cudd_bdd_ite_formula <- function(bdd) { + return(.Call(c_cudd_bdd_ite_formula, .cudd_bdd_ptr(bdd))) +} + #' @rdname cudd_bdd_methods #' @export cudd_bdd_print <- function(bdd, nvars, verbosity = 1L) { diff --git a/man/cudd_bdd_methods.Rd b/man/cudd_bdd_methods.Rd index 09f492c..06931bc 100644 --- a/man/cudd_bdd_methods.Rd +++ b/man/cudd_bdd_methods.Rd @@ -6,6 +6,7 @@ \alias{cudd_bdd_is_one} \alias{cudd_bdd_is_cube} \alias{cudd_bdd_is_var} +\alias{cudd_bdd_ite_formula} \alias{cudd_bdd_print} \alias{cudd_bdd_summary} \alias{cudd_bdd_apa_print_minterm} @@ -117,6 +118,8 @@ cudd_bdd_is_cube(bdd) cudd_bdd_is_var(bdd) +cudd_bdd_ite_formula(bdd) + cudd_bdd_print(bdd, nvars, verbosity = 1L) cudd_bdd_summary(bdd, nvars, mode = 0L) diff --git a/src/cudd_manager.cpp b/src/cudd_manager.cpp index dbcfdec..b03628b 100644 --- a/src/cudd_manager.cpp +++ b/src/cudd_manager.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include #include "cuddObj.hh" @@ -181,6 +182,49 @@ static std::vector double_vector_from_sexp(SEXP vec, const char *name) { return result; } +static std::string bdd_ite_formula(DdManager *mgr, DdNode *node, std::unordered_map &memo) { + bool complemented = Cudd_IsComplement(node); + DdNode *regular = Cudd_Regular(node); + if (Cudd_IsConstant(regular)) { + bool is_one = regular == Cudd_ReadOne(mgr); + if (complemented) { + is_one = !is_one; + } + return is_one ? "TRUE" : "FALSE"; + } + if (complemented) { + return "!(" + bdd_ite_formula(mgr, regular, memo) + ")"; + } + auto found = memo.find(regular); + if (found != memo.end()) { + return found->second; + } + int index = static_cast(Cudd_NodeReadIndex(regular)); + std::string var = "x" + std::to_string(index); + DdNode *t = Cudd_T(regular); + DdNode *e = Cudd_E(regular); + bool t_comp = Cudd_IsComplement(t); + bool e_comp = Cudd_IsComplement(e); + DdNode *t_reg = Cudd_Regular(t); + DdNode *e_reg = Cudd_Regular(e); + std::string formula; + if (t_reg == e_reg && t_comp != e_comp) { + if (t_comp && !e_comp) { + std::string sub = bdd_ite_formula(mgr, e, memo); + formula = "xor(" + var + ", " + sub + ")"; + } else { + std::string sub = bdd_ite_formula(mgr, t, memo); + formula = "!(xor(" + var + ", " + sub + "))"; + } + } else { + std::string t_formula = bdd_ite_formula(mgr, t, memo); + std::string e_formula = bdd_ite_formula(mgr, e, memo); + formula = "ite(" + var + ", " + t_formula + ", " + e_formula + ")"; + } + memo.emplace(regular, formula); + return formula; +} + extern "C" SEXP c_cudd_new() { try { Cudd *mgr = new Cudd(); @@ -1144,6 +1188,13 @@ extern "C" SEXP c_cudd_bdd_summary(SEXP bdd_ptr, SEXP nvars, SEXP mode) { return R_NilValue; } +extern "C" SEXP c_cudd_bdd_ite_formula(SEXP bdd_ptr) { + BDD *bdd = bdd_from_ptr(bdd_ptr); + std::unordered_map memo; + std::string formula = bdd_ite_formula(bdd->manager(), bdd->getNode(), memo); + return Rf_mkString(formula.c_str()); +} + extern "C" SEXP c_cudd_bdd_apa_print_minterm(SEXP bdd_ptr, SEXP nvars) { BDD *bdd = bdd_from_ptr(bdd_ptr); int vars = Rf_asInteger(nvars); diff --git a/src/rcudd.h b/src/rcudd.h index 8e22c53..250d893 100644 --- a/src/rcudd.h +++ b/src/rcudd.h @@ -43,6 +43,7 @@ extern "C" SEXP c_cudd_bdd_and(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_or(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_xor(SEXP lhs_ptr, SEXP rhs_ptr); extern "C" SEXP c_cudd_bdd_restrict(SEXP bdd_ptr, SEXP constraint_ptr); +extern "C" SEXP c_cudd_bdd_ite_formula(SEXP bdd_ptr); extern "C" SEXP c_cudd_bdd_print(SEXP bdd_ptr, SEXP nvars, SEXP verbosity); extern "C" SEXP c_cudd_bdd_summary(SEXP bdd_ptr, SEXP nvars, SEXP mode); extern "C" SEXP c_cudd_bdd_apa_print_minterm(SEXP bdd_ptr, SEXP nvars); diff --git a/src/register.cpp b/src/register.cpp index 3d6dbf1..827d905 100644 --- a/src/register.cpp +++ b/src/register.cpp @@ -40,6 +40,7 @@ static const R_CallMethodDef CallEntries[] = { {"c_cudd_bdd_or", (DL_FUNC) &c_cudd_bdd_or, 2}, {"c_cudd_bdd_xor", (DL_FUNC) &c_cudd_bdd_xor, 2}, {"c_cudd_bdd_restrict", (DL_FUNC) &c_cudd_bdd_restrict, 2}, + {"c_cudd_bdd_ite_formula", (DL_FUNC) &c_cudd_bdd_ite_formula, 1}, {"c_cudd_bdd_print", (DL_FUNC) &c_cudd_bdd_print, 3}, {"c_cudd_bdd_summary", (DL_FUNC) &c_cudd_bdd_summary, 3}, {"c_cudd_bdd_apa_print_minterm", (DL_FUNC) &c_cudd_bdd_apa_print_minterm, 2}, diff --git a/tests/testthat/test_cudd_bdd_methods.R b/tests/testthat/test_cudd_bdd_methods.R index 72b2035..0764548 100644 --- a/tests/testthat/test_cudd_bdd_methods.R +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -29,6 +29,7 @@ test_that("additional BDD methods are exposed", { cudd_bdd_correlation_weights(vars[[1L]], vars[[1L]], rep(0.5, 3L)), 1.0 ) + expect_identical(cudd_bdd_ite_formula(vars[[1L]] + vars[[2L]]), "ite(x0, TRUE, ite(x1, TRUE, FALSE))") shortest_length <- cudd_bdd_shortest_length(vars[[1L]]) expect_type(shortest_length, "integer") From 55e21f6890abd9f82dac867eaa45f92da546c8e6 Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Fri, 2 Jan 2026 12:48:57 +0100 Subject: [PATCH 6/8] Render BDD formulas without ITE --- src/cudd_manager.cpp | 58 ++++++++++++++++++++++++-- tests/testthat/test_cudd_bdd_methods.R | 2 +- 2 files changed, 55 insertions(+), 5 deletions(-) diff --git a/src/cudd_manager.cpp b/src/cudd_manager.cpp index b03628b..aeecf8c 100644 --- a/src/cudd_manager.cpp +++ b/src/cudd_manager.cpp @@ -183,6 +183,30 @@ static std::vector double_vector_from_sexp(SEXP vec, const char *name) { } static std::string bdd_ite_formula(DdManager *mgr, DdNode *node, std::unordered_map &memo) { + auto make_not = [](const std::string &expr) { + return "not(" + expr + ")"; + }; + auto make_and = [](const std::string &lhs, const std::string &rhs) { + return "and(" + lhs + ", " + rhs + ")"; + }; + auto make_or = [](const std::string &lhs, const std::string &rhs) { + return "or(" + lhs + ", " + rhs + ")"; + }; + auto make_xor = [](const std::string &lhs, const std::string &rhs) { + return "xor(" + lhs + ", " + rhs + ")"; + }; + auto is_const = [mgr](DdNode *candidate, bool &value) { + DdNode *regular = Cudd_Regular(candidate); + if (!Cudd_IsConstant(regular)) { + return false; + } + bool is_one = regular == Cudd_ReadOne(mgr); + if (Cudd_IsComplement(candidate)) { + is_one = !is_one; + } + value = is_one; + return true; + }; bool complemented = Cudd_IsComplement(node); DdNode *regular = Cudd_Regular(node); if (Cudd_IsConstant(regular)) { @@ -193,7 +217,7 @@ static std::string bdd_ite_formula(DdManager *mgr, DdNode *node, std::unordered_ return is_one ? "TRUE" : "FALSE"; } if (complemented) { - return "!(" + bdd_ite_formula(mgr, regular, memo) + ")"; + return make_not(bdd_ite_formula(mgr, regular, memo)); } auto found = memo.find(regular); if (found != memo.end()) { @@ -207,19 +231,45 @@ static std::string bdd_ite_formula(DdManager *mgr, DdNode *node, std::unordered_ bool e_comp = Cudd_IsComplement(e); DdNode *t_reg = Cudd_Regular(t); DdNode *e_reg = Cudd_Regular(e); + bool t_const = false; + bool e_const = false; + bool t_value = false; + bool e_value = false; + t_const = is_const(t, t_value); + e_const = is_const(e, e_value); std::string formula; if (t_reg == e_reg && t_comp != e_comp) { if (t_comp && !e_comp) { std::string sub = bdd_ite_formula(mgr, e, memo); - formula = "xor(" + var + ", " + sub + ")"; + formula = make_xor(var, sub); } else { std::string sub = bdd_ite_formula(mgr, t, memo); - formula = "!(xor(" + var + ", " + sub + "))"; + formula = make_not(make_xor(var, sub)); + } + } else if (t_const && e_const) { + if (t_value == e_value) { + formula = t_value ? "TRUE" : "FALSE"; + } else if (t_value) { + formula = var; + } else { + formula = make_not(var); } + } else if (t_const && t_value) { + std::string e_formula = bdd_ite_formula(mgr, e, memo); + formula = make_or(var, e_formula); + } else if (t_const && !t_value) { + std::string e_formula = bdd_ite_formula(mgr, e, memo); + formula = make_and(make_not(var), e_formula); + } else if (e_const && !e_value) { + std::string t_formula = bdd_ite_formula(mgr, t, memo); + formula = make_and(var, t_formula); + } else if (e_const && e_value) { + std::string t_formula = bdd_ite_formula(mgr, t, memo); + formula = make_or(make_not(var), t_formula); } else { std::string t_formula = bdd_ite_formula(mgr, t, memo); std::string e_formula = bdd_ite_formula(mgr, e, memo); - formula = "ite(" + var + ", " + t_formula + ", " + e_formula + ")"; + formula = make_or(make_and(var, t_formula), make_and(make_not(var), e_formula)); } memo.emplace(regular, formula); return formula; diff --git a/tests/testthat/test_cudd_bdd_methods.R b/tests/testthat/test_cudd_bdd_methods.R index 0764548..d100111 100644 --- a/tests/testthat/test_cudd_bdd_methods.R +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -29,7 +29,7 @@ test_that("additional BDD methods are exposed", { cudd_bdd_correlation_weights(vars[[1L]], vars[[1L]], rep(0.5, 3L)), 1.0 ) - expect_identical(cudd_bdd_ite_formula(vars[[1L]] + vars[[2L]]), "ite(x0, TRUE, ite(x1, TRUE, FALSE))") + expect_identical(cudd_bdd_ite_formula(vars[[1L]] + vars[[2L]]), "or(x0, x1)") shortest_length <- cudd_bdd_shortest_length(vars[[1L]]) expect_type(shortest_length, "integer") From 24a430066b1240d172c97ac1b6fe72ec78b0ca1f Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Fri, 2 Jan 2026 16:18:44 +0100 Subject: [PATCH 7/8] Expand tests for BDD formula rendering --- tests/testthat/test_cudd_bdd_methods.R | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tests/testthat/test_cudd_bdd_methods.R b/tests/testthat/test_cudd_bdd_methods.R index d100111..4262d36 100644 --- a/tests/testthat/test_cudd_bdd_methods.R +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -30,6 +30,14 @@ test_that("additional BDD methods are exposed", { 1.0 ) expect_identical(cudd_bdd_ite_formula(vars[[1L]] + vars[[2L]]), "or(x0, x1)") + expect_identical(cudd_bdd_ite_formula(vars[[1L]] * vars[[2L]]), "and(x0, x1)") + expect_identical(cudd_bdd_ite_formula(!vars[[1L]]), "not(x0)") + expect_identical(cudd_bdd_ite_formula(vars[[1L]] ^ vars[[2L]]), "xor(x0, x1)") + expect_identical(cudd_bdd_ite_formula(!(vars[[1L]] ^ vars[[2L]])), "not(xor(x0, x1))") + expect_identical( + cudd_bdd_ite_formula((!vars[[1L]]) * vars[[2L]]), + "and(not(x0), x1)" + ) shortest_length <- cudd_bdd_shortest_length(vars[[1L]]) expect_type(shortest_length, "integer") From 667272bdbada557127be0e5807161fc9b67145d2 Mon Sep 17 00:00:00 2001 From: MEO265 <99362508+MEO265@users.noreply.github.com> Date: Fri, 2 Jan 2026 16:19:08 +0100 Subject: [PATCH 8/8] Add BDD formula test for nested ops --- tests/testthat/test_cudd_bdd_methods.R | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/testthat/test_cudd_bdd_methods.R b/tests/testthat/test_cudd_bdd_methods.R index 4262d36..e4175d1 100644 --- a/tests/testthat/test_cudd_bdd_methods.R +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -38,6 +38,11 @@ test_that("additional BDD methods are exposed", { cudd_bdd_ite_formula((!vars[[1L]]) * vars[[2L]]), "and(not(x0), x1)" ) + complex_bdd <- (vars[[1L]] * vars[[2L]]) + (!vars[[1L]] * (vars[[2L]] ^ vars[[3L]])) + expect_identical( + cudd_bdd_ite_formula(complex_bdd), + "or(and(x0, x1), and(not(x0), xor(x1, x2)))" + ) shortest_length <- cudd_bdd_shortest_length(vars[[1L]]) expect_type(shortest_length, "integer")