Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extended the Python api with node level and exports #21

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions bindings/python/oxidd/bdd.py
Original file line number Diff line number Diff line change
Expand Up @@ -184,6 +184,32 @@ def __le__(self, other: Self) -> bool:
def __ge__(self, other: Self) -> bool:
return (self._func._p, self._func._i) >= (other._func._p, other._func._i)

def export_dddmp(
self,
dd_name: str,
filename: str,
function_name: str,
variables: list[Self],
variable_names: list[str],
as_ascii: bool,
) -> None:
"""Export the decision diagram in to filename in DDDMP format"""
tmp_variables = [var._func for var in variables]
tmp_variable_names = [
_ffi.new("char[]", name.encode()) for name in variable_names
]

_lib.oxidd_bdd_export_dddmp(
self._func,
filename.encode(),
dd_name.encode(),
function_name.encode(),
tmp_variables,
tmp_variable_names,
len(variables),
as_ascii,
)

@override
def __hash__(self) -> int:
return hash((self._func._p, self._func._i))
Expand Down
70 changes: 70 additions & 0 deletions crates/oxidd-ffi/src/bdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -861,6 +861,76 @@ pub unsafe extern "C" fn oxidd_bdd_eval(
})
}

/// Export the decision diagram for function `f` to `filename` in DDDMP format.
///
/// `dd_name` is the name that is output to the `.dd` field, unless it is an
/// empty string.
///
/// `function_name` is the name of the root function that is output to the `.dd`
/// field, unless it is an empty string.
///
/// `vars` are edges representing *all* variables in the decision diagram. The
/// order does not matter. `var_names` are the names of these variables. These
/// must be `vars.len()` names in the same order as in `vars`.
///
/// `ascii` indicates whether to use the ASCII or binary format.
///
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns `true` on success
#[no_mangle]
pub unsafe extern "C" fn oxidd_bdd_export_dddmp(
f: bdd_t,
path: *const c_char,
dd_name: *const c_char,
function_name: *const c_char,
vars: *const bdd_t,
var_names: *const *const c_char,
num_vars: usize,
ascii: bool,
) -> bool {
let Ok(path) = CStr::from_ptr(path).to_str() else {
return false;
};
let Ok(file) = std::fs::File::create(path) else {
return false;
};

let f = f.get().expect("f must be valid");
f.with_manager_shared(|manager, _| {
// Collect the variables.
let vars: Vec<ManuallyDrop<BDDFunction>> = std::slice::from_raw_parts(vars, num_vars)
.iter()
.map(|g| g.get().expect("Invalid variable BDD"))
.collect();

let vars_ref: Vec<&BDDFunction> = vars.iter().map::<&BDDFunction, _>(|v| v).collect();

let var_names: Vec<&str> = std::slice::from_raw_parts(var_names, num_vars)
.iter()
.map(|&name| {
CStr::from_ptr(name)
.to_str()
.expect("the variable name is not a valid UTF-8 string")
})
.collect();

let func: &BDDFunction = &f;
oxidd_dump::dddmp::export(
file,
manager,
ascii,
&c_char_to_str(dd_name),
&vars_ref,
Some(&var_names),
&[func],
Some(&[&c_char_to_str(function_name)]),
|_| false,
)
.is_ok()
})
}

/// Dump the entire decision diagram represented by `manager` as Graphviz DOT
/// code to a file at `path`
///
Expand Down