diff --git a/NAMESPACE b/NAMESPACE index 42a5697..76446a8 100644 --- a/NAMESPACE +++ b/NAMESPACE @@ -16,21 +16,128 @@ 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_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) +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_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) +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) +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_ite_formula) +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) +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) +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) +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_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) +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_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) 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..f696ee6 --- /dev/null +++ b/R/cudd_bdd_methods.R @@ -0,0 +1,1034 @@ +.cudd_bdd_wrap <- function(ptr, bdd) { + 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)) { + 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,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,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,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. +#' @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_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_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) { + .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) { + 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) { + 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_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) { + 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_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) { + 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)) +} + +#' @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_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) { + 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/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..06931bc --- /dev/null +++ b/man/cudd_bdd_methods.Rd @@ -0,0 +1,385 @@ +% 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_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} +\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} +\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} +\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_correlation} +\alias{cudd_bdd_correlation_weights} +\alias{cudd_bdd_xor_method} +\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_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} +\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} +\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_solve_eqn} +\alias{cudd_bdd_verify_sol} +\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_ite_formula(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) + +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) + +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_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) + +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_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) + +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) + +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_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) + +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{nvars, num_vars, threshold}{Non-negative integer values used by the operation.} + +\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.} + +\item{quality, quality1, quality0}{Numeric scalars controlling approximate operations.} + +\item{limit}{Optional non-negative integer limit passed to CUDD.} + +\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, g_list}{Lists of [`CuddBDD`] instances.} + +\item{minterm, inputs, y_index}{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{n}{Integer size for equation solving.} + +\item{m}{Numeric scalar used by split operations.} + +\item{manager}{A [`CuddManager`] instance.} +} +\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..aeecf8c 100644 --- a/src/cudd_manager.cpp +++ b/src/cudd_manager.cpp @@ -2,7 +2,9 @@ #include #include #include +#include #include +#include #include #include "cuddObj.hh" @@ -94,6 +96,185 @@ 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; +} + +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; +} + +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; +} + +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)) { + bool is_one = regular == Cudd_ReadOne(mgr); + if (complemented) { + is_one = !is_one; + } + return is_one ? "TRUE" : "FALSE"; + } + if (complemented) { + return make_not(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); + 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 = make_xor(var, sub); + } else { + std::string sub = bdd_ite_formula(mgr, t, memo); + 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 = make_or(make_and(var, t_formula), make_and(make_not(var), e_formula)); + } + memo.emplace(regular, formula); + return formula; +} + extern "C" SEXP c_cudd_new() { try { Cudd *mgr = new Cudd(); @@ -1025,6 +1206,942 @@ 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_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_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); + 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()); +} + +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_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"); + 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()); +} + +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_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); + 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_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); + 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..250d893 100644 --- a/src/rcudd.h +++ b/src/rcudd.h @@ -42,6 +42,113 @@ 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_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); +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); +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_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); +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); +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_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); +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_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); +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..827d905 100644 --- a/src/register.cpp +++ b/src/register.cpp @@ -39,6 +39,113 @@ 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_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}, + {"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}, + {"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_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}, + {"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}, + {"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_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}, + {"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_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}, + {"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}, 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 new file mode 100644 index 0000000..e4175d1 --- /dev/null +++ b/tests/testthat/test_cudd_bdd_methods.R @@ -0,0 +1,55 @@ +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")) + + 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) + expect_equal( + cudd_bdd_correlation_weights(vars[[1L]], vars[[1L]], rep(0.5, 3L)), + 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)" + ) + 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") + expect_gte(shortest_length, 0L) + + manager2 <- CuddManager() + transferred <- cudd_bdd_transfer(vars[[1L]], manager2) + expect_true(methods::is(transferred, "CuddBDD")) + expect_silent(transferred + cudd_bdd_var(manager2)) +})