From 6a492f575c65fc4f51cfe28aa8b9727981dea911 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Thu, 2 Sep 2021 20:40:16 +0200 Subject: [PATCH 01/15] WIP: Migrate libcudd to version 3.0.0, built using autotool. --- Cargo.toml | 4 ++ build.rs | 188 ++++++++++++++++------------------------------------- 2 files changed, 61 insertions(+), 131 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 5585de2..1b08927 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,3 +9,7 @@ license = "CC0-1.0" [dependencies] libc = "0.2" + +[build-dependencies] +bindgen = "0.59.1" +autotools = "0.2.3" \ No newline at end of file diff --git a/build.rs b/build.rs index b663fb6..cd61094 100644 --- a/build.rs +++ b/build.rs @@ -1,13 +1,12 @@ // build.rs use std::env; -use std::fs; -use std::fs::File; -use std::io::{BufRead, BufReader, BufWriter, Write}; +use std::io::ErrorKind; use std::path::{Path, PathBuf}; use std::process::Command; +use MD5Status::{Mismatch, Unknown}; -const PACKAGE_URL: &str = "https://github.com/ivmai/cudd/archive/refs/tags/cudd-2.5.1.tar.gz"; -const PACKAGE_MD5: &str = "42283a52ff815c5ca8231b6927318fbf"; +const PACKAGE_URL: &str = "https://github.com/ivmai/cudd/archive/refs/tags/cudd-3.0.0.tar.gz"; +const PACKAGE_MD5: &str = "edca9c69528256ca8ae37be9cedef73f"; #[derive(Debug)] enum FetchError { @@ -47,146 +46,73 @@ fn run_command(cmd: &mut Command) -> Result<(String, String), FetchError> { fn fetch_package(out_dir: &str, url: &str, md5: &str) -> Result<(PathBuf, MD5Status), FetchError> { let out_path = Path::new(&out_dir); let target_path = out_path.join(Path::new(url).file_name().unwrap()); - - let md5_result = { - let target_path_str = target_path.to_str().unwrap(); - let meta = fs::metadata(&target_path); - - match meta { - Ok(m) => { - if m.is_file() { - println!("{} already exists, skipping download", target_path_str) - } else { - return Err(FetchError::PathExists); - } - } - Err(e) => { - if e.kind() == std::io::ErrorKind::NotFound { - println!("Downloading {} to {}", url, target_path_str); - run_command(&mut Command::new("curl").args(&[ - "-L", - url, - "-o", - target_path_str, - ]))?; - } else { - return Err(FetchError::IOError(e)); - } - } + let target_path_str = target_path.clone().into_os_string().into_string().unwrap(); + + match target_path.metadata() { + Err(error) if error.kind() == ErrorKind::NotFound => { + // Path does not exist! Start download... + println!("Downloading {} to {}", url, target_path_str); + let mut command = Command::new("curl"); + command.args(&["-L", url, "-o", target_path_str.as_str()]); + run_command(&mut command)?; } - - run_command(&mut Command::new("md5sum").arg(target_path_str)) - .or_else(|_| run_command(&mut Command::new("md5").arg(target_path_str))) - }; - - Ok(( - target_path, - match md5_result { - Err(_) => MD5Status::Unknown, - Ok((out, _)) => { - // md5sum outputs " ", md5 on OSX outputs "MD5 () = " - if out.contains(md5) { - MD5Status::Match - } else { - MD5Status::Mismatch - } - } - }, - )) -} - -fn replace_lines(path: &Path, replacements: Vec<(&str, &str)>) -> Result { - let mut lines_replaced = 0; - let new_path = path.with_extension(".new"); - - { - let f_in = File::open(&path)?; - let f_out = File::create(&new_path)?; - let reader = BufReader::new(&f_in); - let mut writer = BufWriter::new(&f_out); - - 'read: for line in reader.lines() { - let line = line.unwrap(); - for &(original, replacement) in &replacements { - if line.starts_with(&original) { - writeln!(writer, "{}", replacement)?; - lines_replaced += 1; - continue 'read; - } - } - writeln!(writer, "{}", line)?; + Ok(data) if data.is_file() => { + println!("{} exists. Skipping download.", target_path_str); } + Ok(_) => return Err(FetchError::PathExists), + Err(error) => return Err(FetchError::IOError(error)), } - fs::remove_file(&path)?; - fs::rename(&new_path, &path)?; + // Now run md5 sum check: + let mut command_1 = Command::new("md5sum"); + command_1.arg(target_path.clone()); + let mut command_2 = Command::new("md5"); + command_2.arg(target_path.clone()); + let md5_result = run_command(&mut command_1).or_else(|_| run_command(&mut command_2)); + + let md5_status = match md5_result { + Err(_) => MD5Status::Unknown, + Ok((output, _)) if output.contains(md5) => MD5Status::Match, + _ => MD5Status::Mismatch, + }; - Ok(lines_replaced) + Ok((target_path, md5_status)) } -fn main() { - let out_dir = env::var("OUT_DIR").unwrap(); +fn main() -> Result<(), String> { + let out_dir = env::var("OUT_DIR") + .map_err(|_| format!("Environmental variable `OUT_DIR` not defined."))?; - let (tar_path, md5_status) = fetch_package(&out_dir, PACKAGE_URL, PACKAGE_MD5).unwrap(); + let (tar_path, md5_status) = fetch_package(&out_dir, PACKAGE_URL, PACKAGE_MD5) + .map_err(|e| format!("Error downloading CUDD package: {:?}.", e))?; + let tar_path_str = tar_path.to_str().unwrap().to_string(); match md5_status { - MD5Status::Match => (), - MD5Status::Unknown => println!("No md5 available, skipping package validation"), - MD5Status::Mismatch => panic!("MD5 mismatch on package"), + Unknown => eprintln!("WARNING: MD5 not computed. Package validation skipped."), + Mismatch => return Err(format!("CUDD package MD5 hash mismatch.")), + _ => (), } - let untarred_path = tar_path.with_extension("").with_extension(""); // kill .tar and .gz - if !untarred_path.exists() { + // Get cudd.tar.gz path without extensions. + let cudd_path = tar_path.with_extension("").with_extension(""); + let cudd_path_str = cudd_path.clone().into_os_string().into_string().unwrap(); + + if !cudd_path.exists() { // Create the destination directory. - std::fs::create_dir_all(untarred_path.clone()).unwrap(); + std::fs::create_dir_all(cudd_path.clone()) + .map_err(|e| format!("Cannot create CUDD director: {:?}", e))?; } - // untar package, ignoring the name of the top level folder, dumping into untarred_path instead. - let untarred_path_str = untarred_path - .clone() - .into_os_string() - .into_string() - .unwrap(); - run_command(Command::new("tar").args(&[ - "xf", - tar_path.to_str().unwrap(), - "--strip-components=1", - "-C", - &untarred_path_str, - ])) - .unwrap(); - - // patch Makefile - let lines_replaced = replace_lines( - &untarred_path.join("Makefile"), - vec![ - // need PIC so our rust lib can be dynamically linked - ("ICFLAGS\t= -g -O3", "ICFLAGS\t= -g -O3 -fPIC"), - // remove "nanotrav" from DIRS, it doesn't compile on OSX - ( - "DIRS\t= $(BDIRS)", // (matches prefix) - "DIRS\t= $(BDIRS)", - ), - ], - ) - .unwrap(); - if lines_replaced != 2 { - panic!("Replaced {} lines in Makefile, expected 1", lines_replaced); - } + // un-tar package, ignoring the name of the top level folder, dumping into cudd_path instead. + let mut tar_command = Command::new("tar"); + tar_command.args(&["xf", &tar_path_str, "--strip-components=1", "-C", &cudd_path_str]); + run_command(&mut tar_command) + .map_err(|e| format!("Error decompressing CUDD: {:?}", e))?; + + let build_output = autotools::build(cudd_path); + eprintln!("Output: {}", build_output.display()); + println!("cargo:rustc-link-search=native={}/lib", build_output.display()); + println!("cargo:rustc-link-lib=static=cudd"); - // build libraries (execute make) - run_command(Command::new("make").current_dir(&untarred_path)).unwrap(); - - // Move all libs to output directory so we don't have to specify each directory - run_command( - Command::new("sh") - .current_dir(&out_dir) - .args(&["-c", "cp cudd-*/*/*.a ."]), - ) - .unwrap(); - - println!("cargo:rustc-flags=-L {}", out_dir); - println!( - "cargo:rustc-flags=-l static=cudd -l static=mtr -l static=util -l static=epd -l static=st" - ); + Ok(()) } From c9ccb044dcd62de9286d1fae344359d91cde5b4a Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Fri, 3 Sep 2021 11:41:31 +0200 Subject: [PATCH 02/15] Fix formatting and give up on using bindgen (too much compat. issues). --- Cargo.toml | 3 +-- build.rs | 25 ++++++++++++++++--------- 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 1b08927..c2a7559 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "cudd-sys" -version = "0.1.1" +version = "1.0.0" authors = ["Philip Lewis "] build = "build.rs" description = "Bindings for CU Decision Diagram library (CUDD)" @@ -11,5 +11,4 @@ license = "CC0-1.0" libc = "0.2" [build-dependencies] -bindgen = "0.59.1" autotools = "0.2.3" \ No newline at end of file diff --git a/build.rs b/build.rs index cd61094..bb256a5 100644 --- a/build.rs +++ b/build.rs @@ -37,7 +37,7 @@ fn run_command(cmd: &mut Command) -> Result<(String, String), FetchError> { String::from_utf8(output.stderr).unwrap(), )) } else { - println!("Command {:?} exited with status {}", cmd, output.status); + eprintln!("Command {:?} exited with status {}", cmd, output.status); Err(FetchError::CommandError(output.status)) }; } @@ -60,7 +60,7 @@ fn fetch_package(out_dir: &str, url: &str, md5: &str) -> Result<(PathBuf, MD5Sta println!("{} exists. Skipping download.", target_path_str); } Ok(_) => return Err(FetchError::PathExists), - Err(error) => return Err(FetchError::IOError(error)), + Err(error) => return Err(FetchError::from(error)), } // Now run md5 sum check: @@ -81,7 +81,7 @@ fn fetch_package(out_dir: &str, url: &str, md5: &str) -> Result<(PathBuf, MD5Sta fn main() -> Result<(), String> { let out_dir = env::var("OUT_DIR") - .map_err(|_| format!("Environmental variable `OUT_DIR` not defined."))?; + .map_err(|_| "Environmental variable `OUT_DIR` not defined.".to_string())?; let (tar_path, md5_status) = fetch_package(&out_dir, PACKAGE_URL, PACKAGE_MD5) .map_err(|e| format!("Error downloading CUDD package: {:?}.", e))?; @@ -89,7 +89,7 @@ fn main() -> Result<(), String> { match md5_status { Unknown => eprintln!("WARNING: MD5 not computed. Package validation skipped."), - Mismatch => return Err(format!("CUDD package MD5 hash mismatch.")), + Mismatch => return Err("CUDD package MD5 hash mismatch.".to_string()), _ => (), } @@ -105,13 +105,20 @@ fn main() -> Result<(), String> { // un-tar package, ignoring the name of the top level folder, dumping into cudd_path instead. let mut tar_command = Command::new("tar"); - tar_command.args(&["xf", &tar_path_str, "--strip-components=1", "-C", &cudd_path_str]); - run_command(&mut tar_command) - .map_err(|e| format!("Error decompressing CUDD: {:?}", e))?; + tar_command.args(&[ + "xf", + &tar_path_str, + "--strip-components=1", + "-C", + &cudd_path_str, + ]); + run_command(&mut tar_command).map_err(|e| format!("Error decompressing CUDD: {:?}", e))?; let build_output = autotools::build(cudd_path); - eprintln!("Output: {}", build_output.display()); - println!("cargo:rustc-link-search=native={}/lib", build_output.display()); + println!( + "cargo:rustc-link-search=native={}", + build_output.join("lib").display() + ); println!("cargo:rustc-link-lib=static=cudd"); Ok(()) From 583232b0e1d9f4842bdf36fd84c45c0ac4346a18 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Fri, 3 Sep 2021 16:02:14 +0200 Subject: [PATCH 03/15] WIP: Migrate CUDD API to version 3.0.0. --- src/lib.rs | 364 ++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 317 insertions(+), 47 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 3b6877a..263cf9a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -6,26 +6,37 @@ extern crate libc; #[cfg(test)] mod test; -use libc::{c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void, FILE}; +use libc::{c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void}; +use std::marker::{PhantomData, PhantomPinned}; +use std::ops::Not; -pub static CUDD_TRUE: c_uint = 1; -pub static CUDD_FALSE: c_uint = 0; +/// An integer representation of a Boolean `true` constant. (This is not a DD construct!) +pub const CUDD_TRUE: c_uint = 1; +/// An integer representation of a Boolean `false` constant. (This is not a DD construct!) +pub const CUDD_FALSE: c_uint = 0; -pub type CUDD_VALUE_TYPE = c_double; +/// An special return value indicating an out-of-memory error. +pub const CUDD_OUT_OF_MEM: c_int = -1; -pub static CUDD_OUT_OF_MEM: c_int = -1; +/// Recommended default size of the unique node table. +pub const CUDD_UNIQUE_SLOTS: c_uint = (1 << 8); +/// Recommended default size of the operation cache table. +pub const CUDD_CACHE_SLOTS: c_uint = (1 << 18); -pub static CUDD_UNIQUE_SLOTS: c_uint = 256; -pub static CUDD_CACHE_SLOTS: c_uint = 262144; +/// Default option for `Cudd_addResidue`: specifies that the least-significant-bit is on top, +/// and the number is interpreted as unsigned. +pub const CUDD_RESIDUE_DEFAULT: c_int = 0; -pub static CUDD_RESIDUE_DEFAULT: c_uint = 0; -pub static CUDD_RESIDUE_MSB: c_uint = 1; -pub static CUDD_RESIDUE_TC: c_uint = 2; +/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that +/// the most-significant-bit is on top. +pub const CUDD_RESIDUE_MSB: c_int = 1; -// TODO: pub static CUDD_MAXINDEX +/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that +/// the number should be interpreted as a signed two's complement. +pub const CUDD_RESIDUE_TC: c_int = 2; -#[repr(C)] -#[allow(dead_code)] +/// Types of variable reordering algorithms. +#[repr("C")] pub enum Cudd_ReorderingType { CUDD_REORDER_SAME, CUDD_REORDER_NONE, @@ -51,8 +62,8 @@ pub enum Cudd_ReorderingType { CUDD_REORDER_EXACT, } -#[repr(C)] -#[allow(dead_code)] +/// Type of aggregation method algorithm. +#[repr("C")] pub enum Cudd_AggregationType { CUDD_NO_CHECK, CUDD_GROUP_CHECK, @@ -66,8 +77,8 @@ pub enum Cudd_AggregationType { CUDD_GROUP_CHECK9, } -#[repr(C)] -#[allow(dead_code)] +/// Type of a hook. +#[repr("C")] pub enum Cudd_HookType { CUDD_PRE_GC_HOOK, CUDD_POST_GC_HOOK, @@ -75,8 +86,8 @@ pub enum Cudd_HookType { CUDD_POST_REORDERING_HOOK, } -#[repr(C)] -#[allow(dead_code)] +// Type of an error code. +#[repr("C")] pub enum Cudd_ErrorType { CUDD_NO_ERROR, CUDD_MEMORY_OUT, @@ -88,8 +99,8 @@ pub enum Cudd_ErrorType { CUDD_INTERNAL_ERROR, } -#[repr(C)] -#[allow(dead_code)] +/// Type of grouping used during lazy sifting. +#[repr("C")] pub enum Cudd_LazyGroupType { CUDD_LAZY_NONE, CUDD_LAZY_SOFT_GROUP, @@ -97,34 +108,276 @@ pub enum Cudd_LazyGroupType { CUDD_LAZY_UNGROUP, } -#[repr(C)] -#[allow(dead_code)] +/// Type of variable used during lazy sifting. +#[repr("C")] pub enum Cudd_VariableType { CUDD_VAR_PRIMARY_INPUT, CUDD_VAR_PRESENT_STATE, CUDD_VAR_NEXT_STATE, } -#[cfg(all(target_pointer_width = "32"))] -pub type DdHalfWord = libc::uint16_t; - -#[cfg(all(target_pointer_width = "64"))] -pub type DdHalfWord = u32; +/// Type of the value of a terminal node. +pub type CUDD_VALUE_TYPE = c_double; -#[repr(C)] +/// An opaque C struct used to represent the decision diagram nodes. +#[repr("C")] pub struct DdNode { - index: DdHalfWord, - ref_count: DdHalfWord, - next: *mut DdNode, - union_data: [c_uint; 2], + _data: [u8; 0], + _marker: PhantomData<(*mut u8, PhantomPinned)>, +} + +/// An opaque C struct used to represent the CUDD manager. +#[repr("C")] +pub struct DdManager { + _data: [u8; 0], + _marker: PhantomData<(*mut u8, PhantomPinned)>, } -pub type DdManager = c_void; -pub type DdGen = c_void; -pub type MtrNode = c_void; -pub type DdTlcInfo = c_void; +/// An opaque C struct used to represent the CUDD generator. +#[repr("C")] +pub struct DdGen { + _data: [u8; 0], + _marker: PhantomData<(*mut u8, PhantomPinned)>, +} + +/// The type of an arbitrary precision "digit". +pub type DdApaDigit = u32; + +/// The type of an arbitrary precision integer, corresponding to an array of digits. +pub type DdApaNumber = *mut DdApaDigit; + +/// A const-qualified version of `DdApaNumber`. +pub type DdConstApaNumber = *const DdApaDigit; + +/// An opaque C struct used to represent the result of computation of two-literal clauses. +/// +/// See `Cudd_FindTwoLiteralClauses`. +#[repr("C")] +pub struct DdTlcInfo { + _data: [u8; 0], + _marker: PhantomData<(*mut u8, PhantomPinned)>, +} + +/// Type of the hook function. +pub type DD_HOOK_FUNCTION = extern "C" fn(*mut DdManager, *const c_char, *mut c_void) -> c_int; + +/// Type of the priority function. +pub type DD_PRIORITY_FUNCTION = extern "C" fn( + *mut DdManager, + c_int, + *mut *mut DdNode, + *mut *mut DdNode, + *mut *mut DdNode, +) -> *mut DdNode; + +/// Type of the apply operator function. +pub type DD_APPLY_OPERATOR = + extern "C" fn(*mut DdManager, *mut *mut DdNode, *mut *mut DdNode) -> *mut DdNode; + +/// Type of the monadic apply operator function. +pub type DD_MONADIC_APPLY_OPERATOR = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; + +/// Type of the two-operand cache tag function. +pub type DD_CACHE_TAG_FUNCTION_2 = + extern "C" fn(*mut DdManager, *mut DdNode, *mut DdNode) -> *mut DdNode; + +/// Type of the one-operand cache tag function. +pub type DD_CACHE_TAG_FUNCTION_1 = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; + +/// Type of the out-of-memory function. +pub type DD_OUT_OF_MEMORY_FUNCTION = extern "C" fn(size_t) -> c_void; + +/// Type of the Q-sort comparison function. +pub type DD_Q_SORT_FUNCTION = extern "C" fn(*const c_void, *const c_void) -> c_int; + +/// Type of the termination handler function. +pub type DD_TERMINATION_HANDLER = extern "C" fn(*const c_void) -> c_int; + +/// Type of the time-out handler function. +pub type DD_TIME_OUT_HANDLER = extern "C" fn(*mut DdManager, *mut c_void) -> c_void; + +/// Complements a DD node by flipping the complement attribute of +/// the pointer (the least significant bit). +#[inline] +pub const unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode { + ((node as usize) ^ 01) as *mut DdNode +} + +/// Complements a DD node by flipping the complement attribute +/// of the pointer if a condition is satisfied. The `condition` +/// argument must be always either `1` or `0`. +#[inline] +pub const unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode { + ((node as usize) ^ (condition as usize)) as *mut DdNode +} + +/// Computes the regular version of a node pointer (i.e. without the complement +/// bit set, regardless of its previous value). +pub const unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode { + ((node as usize) & 01.not()) as *mut DdNode +} + +/// Computes the complemented version of a node pointer (i.e. with a complement +/// bit set, regardless of its previous value). +pub const unsafe fn Cudd_Complement(node: *mut DdNode) -> *mut DdNode { + ((node as usize) | 01) as *mut DdNode +} + +/// Returns 1 if a pointer is complemented. +pub const unsafe fn Cudd_IsComplement(node: *mut DdNode) -> c_int { + ((node as usize) & 1) as c_int +} + +/* +/** +@brief Returns the current position in the order of variable +index. + +@details Returns the current position in the order of variable +index. This macro is obsolete and is kept for compatibility. New +applications should use Cudd_ReadPerm instead. + +@sideeffect none + +@see Cudd_ReadPerm + + */ +#define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index)) + + +/** +@brief Iterates over the cubes of a decision diagram. + +@details Iterates over the cubes of a decision diagram f. +
    +
  • DdManager *manager; +
  • DdNode *f; +
  • DdGen *gen; +
  • int *cube; +
  • CUDD_VALUE_TYPE value; +
+Cudd_ForeachCube allocates and frees the generator. Therefore the +application should not try to do that. Also, the cube is freed at the +end of Cudd_ForeachCube and hence is not available outside of the loop.

+CAUTION: It is assumed that dynamic reordering will not occur while +there are open generators. It is the user's responsibility to make sure +that dynamic reordering does not occur. As long as new nodes are not created +during generation, and dynamic reordering is not called explicitly, +dynamic reordering will not occur. Alternatively, it is sufficient to +disable dynamic reordering. It is a mistake to dispose of a diagram +on which generation is ongoing. + +@sideeffect none + +@see Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree +Cudd_IsGenEmpty Cudd_AutodynDisable + + */ +#define Cudd_ForeachCube(manager, f, gen, cube, value)\ +for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\ +Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ +(void) Cudd_NextCube(gen, &cube, &value)) + + +/** +@brief Iterates over the primes of a Boolean function. + +@details Iterates over the primes of a Boolean function producing +a prime, but not necessarily irredundant, cover. +

    +
  • DdManager *manager; +
  • DdNode *l; +
  • DdNode *u; +
  • DdGen *gen; +
  • int *cube; +
+The Boolean function is described by an upper bound and a lower bound. If +the function is completely specified, the two bounds coincide. +Cudd_ForeachPrime allocates and frees the generator. Therefore the +application should not try to do that. Also, the cube is freed at the +end of Cudd_ForeachPrime and hence is not available outside of the loop.

+CAUTION: It is a mistake to change a diagram on which generation is ongoing. + +@sideeffect none + +@see Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree +Cudd_IsGenEmpty + + */ +#define Cudd_ForeachPrime(manager, l, u, gen, cube)\ +for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\ +Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ +(void) Cudd_NextPrime(gen, &cube)) + + +/** +@brief Iterates over the nodes of a decision diagram. + +@details Iterates over the nodes of a decision diagram f. +

    +
  • DdManager *manager; +
  • DdNode *f; +
  • DdGen *gen; +
  • DdNode *node; +
+The nodes are returned in a seemingly random order. +Cudd_ForeachNode allocates and frees the generator. Therefore the +application should not try to do that.

+CAUTION: It is assumed that dynamic reordering will not occur while +there are open generators. It is the user's responsibility to make sure +that dynamic reordering does not occur. As long as new nodes are not created +during generation, and dynamic reordering is not called explicitly, +dynamic reordering will not occur. Alternatively, it is sufficient to +disable dynamic reordering. It is a mistake to dispose of a diagram +on which generation is ongoing. + +@sideeffect none + +@see Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree +Cudd_IsGenEmpty Cudd_AutodynDisable + + */ +#define Cudd_ForeachNode(manager, f, gen, node)\ +for((gen) = Cudd_FirstNode(manager, f, &node);\ +Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ +(void) Cudd_NextNode(gen, &node)) + + +/** +@brief Iterates over the paths of a %ZDD. + +@details Iterates over the paths of a %ZDD f. +

    +
  • DdManager *manager; +
  • DdNode *f; +
  • DdGen *gen; +
  • int *path; +
+Cudd_zddForeachPath allocates and frees the generator. Therefore the +application should not try to do that. Also, the path is freed at the +end of Cudd_zddForeachPath and hence is not available outside of the loop.

+CAUTION: It is assumed that dynamic reordering will not occur while +there are open generators. It is the user's responsibility to make sure +that dynamic reordering does not occur. As long as new nodes are not created +during generation, and dynamic reordering is not called explicitly, +dynamic reordering will not occur. Alternatively, it is sufficient to +disable dynamic reordering. It is a mistake to dispose of a diagram +on which generation is ongoing. + +@sideeffect none + +@see Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree +Cudd_IsGenEmpty Cudd_AutodynDisable + + */ +#define Cudd_zddForeachPath(manager, f, gen, path)\ +for((gen) = Cudd_zddFirstPath(manager, f, &path);\ +Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ +(void) Cudd_zddNextPath(gen, &path)) + + + */ -#[allow(dead_code)] extern "C" { pub fn Cudd_addNewVar(dd: *mut DdManager) -> *mut DdNode; pub fn Cudd_addNewVarAtLevel(dd: *mut DdManager, level: c_int) -> *mut DdNode; @@ -135,20 +388,43 @@ extern "C" { pub fn Cudd_bddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; pub fn Cudd_zddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; pub fn Cudd_zddVarsFromBddVars(dd: *mut DdManager, multiplicity: c_int) -> c_int; + pub fn Cudd_ReadMaxIndex() -> c_uint; pub fn Cudd_addConst(dd: *mut DdManager, c: CUDD_VALUE_TYPE) -> *mut DdNode; + pub fn Cudd_IsConstant(node: *mut DdNode) -> c_int; pub fn Cudd_IsNonConstant(f: *mut DdNode) -> c_int; + pub fn Cudd_T(node: *mut DdNode) -> *mut DdNode; + pub fn Cudd_E(node: *mut DdNode) -> *mut DdNode; + pub fn Cudd_V(node: *mut DdNode) -> CUDD_VALUE_TYPE; pub fn Cudd_ReadStartTime(unique: *mut DdManager) -> c_ulong; pub fn Cudd_ReadElapsedTime(unique: *mut DdManager) -> c_ulong; pub fn Cudd_SetStartTime(unique: *mut DdManager, st: c_ulong) -> c_void; pub fn Cudd_ResetStartTime(unique: *mut DdManager) -> c_void; pub fn Cudd_ReadTimeLimit(unique: *mut DdManager) -> c_ulong; - pub fn Cudd_SetTimeLimit(unique: *mut DdManager, tl: c_ulong) -> c_void; + pub fn Cudd_SetTimeLimit(unique: *mut DdManager, tl: c_ulong) -> c_ulong; pub fn Cudd_UpdateTimeLimit(unique: *mut DdManager) -> c_void; pub fn Cudd_IncreaseTimeLimit(unique: *mut DdManager, increase: c_ulong) -> c_void; pub fn Cudd_UnsetTimeLimit(unique: *mut DdManager) -> c_void; pub fn Cudd_TimeLimited(unique: *mut DdManager) -> c_int; - //pub fn Cudd_RegisterTerminationCallback(unique: *mut DdManager, callback: c_DD_THFP, callback_arg: *mut c_void) -> c_void; + pub fn Cudd_RegisterTerminationCallback( + unique: *mut DdManager, + callback: DD_TERMINATION_HANDLER, + callback_arg: *mut c_void, + ) -> c_void; pub fn Cudd_UnregisterTerminationCallback(unique: *mut DdManager) -> c_void; + pub fn Cudd_RegisterOutOfMemoryCallback( + unique: *mut DdManager, + callback: DD_OUT_OF_MEMORY_FUNCTION, + ) -> DD_OUT_OF_MEMORY_FUNCTION; + pub fn Cudd_UnregisterOutOfMemoryCallback(unique: *mut DdManager) -> c_void; + pub fn Cudd_RegisterTimeoutHandler( + unique: *mut DdManager, + handler: DD_TIME_OUT_HANDLER, + arg: *mut c_void, + ) -> c_void; + pub fn Cudd_ReadTimeoutHandler( + unique: *mut DdManager, + argp: *mut *mut c_void, + ) -> DD_TIME_OUT_HANDLER; pub fn Cudd_AutodynEnable(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void; pub fn Cudd_AutodynDisable(unique: *mut DdManager) -> c_void; pub fn Cudd_ReorderingStatus(unique: *mut DdManager, method: *mut Cudd_ReorderingType) @@ -213,13 +489,7 @@ extern "C" { pub fn Cudd_SetMaxGrowthAlternate(dd: *mut DdManager, mg: c_double) -> c_void; pub fn Cudd_ReadReorderingCycle(dd: *mut DdManager) -> c_int; pub fn Cudd_SetReorderingCycle(dd: *mut DdManager, cycle: c_int) -> c_void; - pub fn Cudd_ReadTree(dd: *mut DdManager) -> *mut MtrNode; - pub fn Cudd_SetTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; - pub fn Cudd_FreeTree(dd: *mut DdManager) -> c_void; - pub fn Cudd_ReadZddTree(dd: *mut DdManager) -> *mut MtrNode; - pub fn Cudd_SetZddTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; - pub fn Cudd_FreeZddTree(dd: *mut DdManager) -> c_void; - pub fn Cudd_NodeReadIndex(node: *mut DdNode) -> c_uint; + pub fn Cudd_NodeReadIndex(dd: *mut DdNode) -> c_uint; pub fn Cudd_ReadPerm(dd: *mut DdManager, i: c_int) -> c_int; pub fn Cudd_ReadPermZdd(dd: *mut DdManager, i: c_int) -> c_int; pub fn Cudd_ReadInvPerm(dd: *mut DdManager, i: c_int) -> c_int; From f8c05fd9480f47efa6c5ff4fa17af6564a9d6a85 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Fri, 3 Sep 2021 18:30:58 +0200 Subject: [PATCH 04/15] Fix minor issues in new code. --- src/lib.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 263cf9a..e9d02e3 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -6,7 +6,7 @@ extern crate libc; #[cfg(test)] mod test; -use libc::{c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void}; +use libc::{c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void, size_t, FILE}; use std::marker::{PhantomData, PhantomPinned}; use std::ops::Not; @@ -19,9 +19,9 @@ pub const CUDD_FALSE: c_uint = 0; pub const CUDD_OUT_OF_MEM: c_int = -1; /// Recommended default size of the unique node table. -pub const CUDD_UNIQUE_SLOTS: c_uint = (1 << 8); +pub const CUDD_UNIQUE_SLOTS: c_uint = 1 << 8; /// Recommended default size of the operation cache table. -pub const CUDD_CACHE_SLOTS: c_uint = (1 << 18); +pub const CUDD_CACHE_SLOTS: c_uint = 1 << 18; /// Default option for `Cudd_addResidue`: specifies that the least-significant-bit is on top, /// and the number is interpreted as unsigned. @@ -36,7 +36,7 @@ pub const CUDD_RESIDUE_MSB: c_int = 1; pub const CUDD_RESIDUE_TC: c_int = 2; /// Types of variable reordering algorithms. -#[repr("C")] +#[repr(C)] pub enum Cudd_ReorderingType { CUDD_REORDER_SAME, CUDD_REORDER_NONE, @@ -63,7 +63,7 @@ pub enum Cudd_ReorderingType { } /// Type of aggregation method algorithm. -#[repr("C")] +#[repr(C)] pub enum Cudd_AggregationType { CUDD_NO_CHECK, CUDD_GROUP_CHECK, @@ -78,7 +78,7 @@ pub enum Cudd_AggregationType { } /// Type of a hook. -#[repr("C")] +#[repr(C)] pub enum Cudd_HookType { CUDD_PRE_GC_HOOK, CUDD_POST_GC_HOOK, @@ -87,7 +87,7 @@ pub enum Cudd_HookType { } // Type of an error code. -#[repr("C")] +#[repr(C)] pub enum Cudd_ErrorType { CUDD_NO_ERROR, CUDD_MEMORY_OUT, @@ -100,7 +100,7 @@ pub enum Cudd_ErrorType { } /// Type of grouping used during lazy sifting. -#[repr("C")] +#[repr(C)] pub enum Cudd_LazyGroupType { CUDD_LAZY_NONE, CUDD_LAZY_SOFT_GROUP, @@ -109,7 +109,7 @@ pub enum Cudd_LazyGroupType { } /// Type of variable used during lazy sifting. -#[repr("C")] +#[repr(C)] pub enum Cudd_VariableType { CUDD_VAR_PRIMARY_INPUT, CUDD_VAR_PRESENT_STATE, @@ -120,21 +120,21 @@ pub enum Cudd_VariableType { pub type CUDD_VALUE_TYPE = c_double; /// An opaque C struct used to represent the decision diagram nodes. -#[repr("C")] +#[repr(C)] pub struct DdNode { _data: [u8; 0], _marker: PhantomData<(*mut u8, PhantomPinned)>, } /// An opaque C struct used to represent the CUDD manager. -#[repr("C")] +#[repr(C)] pub struct DdManager { _data: [u8; 0], _marker: PhantomData<(*mut u8, PhantomPinned)>, } /// An opaque C struct used to represent the CUDD generator. -#[repr("C")] +#[repr(C)] pub struct DdGen { _data: [u8; 0], _marker: PhantomData<(*mut u8, PhantomPinned)>, @@ -152,7 +152,7 @@ pub type DdConstApaNumber = *const DdApaDigit; /// An opaque C struct used to represent the result of computation of two-literal clauses. /// /// See `Cudd_FindTwoLiteralClauses`. -#[repr("C")] +#[repr(C)] pub struct DdTlcInfo { _data: [u8; 0], _marker: PhantomData<(*mut u8, PhantomPinned)>, @@ -214,7 +214,7 @@ pub const unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut Dd /// Computes the regular version of a node pointer (i.e. without the complement /// bit set, regardless of its previous value). pub const unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode { - ((node as usize) & 01.not()) as *mut DdNode + ((node as usize) & (01 as usize).not()) as *mut DdNode } /// Computes the complemented version of a node pointer (i.e. with a complement From dc0ad8437dd0e7cb30d6ff6d7abdfc7b229d07a2 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 12:11:00 +0200 Subject: [PATCH 05/15] Add new symbols from version 3 and enable older functions which were disabled. --- src/lib.rs | 273 +++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 213 insertions(+), 60 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index e9d02e3..15b4572 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -158,6 +158,20 @@ pub struct DdTlcInfo { _marker: PhantomData<(*mut u8, PhantomPinned)>, } +/// An opaque C struct representing an extended double precision floating point number. +#[repr(C)] +pub struct EpDouble { + _data: [u8; 0], + _marker: PhantomData<(*mut u8, PhantomPinned)>, +} + +/// An opaque C struct representing a multi-way branch tree node. +#[repr(C)] +pub struct MtrNode { + _data: [u8; 0], + _marker: PhantomData<(*mut u8, PhantomPinned)>, +} + /// Type of the hook function. pub type DD_HOOK_FUNCTION = extern "C" fn(*mut DdManager, *const c_char, *mut c_void) -> c_int; @@ -199,7 +213,7 @@ pub type DD_TIME_OUT_HANDLER = extern "C" fn(*mut DdManager, *mut c_void) -> c_v /// Complements a DD node by flipping the complement attribute of /// the pointer (the least significant bit). #[inline] -pub const unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode { +pub unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode { ((node as usize) ^ 01) as *mut DdNode } @@ -207,24 +221,27 @@ pub const unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode { /// of the pointer if a condition is satisfied. The `condition` /// argument must be always either `1` or `0`. #[inline] -pub const unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode { +pub unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode { ((node as usize) ^ (condition as usize)) as *mut DdNode } /// Computes the regular version of a node pointer (i.e. without the complement /// bit set, regardless of its previous value). -pub const unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode { +#[inline] +pub unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode { ((node as usize) & (01 as usize).not()) as *mut DdNode } /// Computes the complemented version of a node pointer (i.e. with a complement /// bit set, regardless of its previous value). -pub const unsafe fn Cudd_Complement(node: *mut DdNode) -> *mut DdNode { +#[inline] +pub unsafe fn Cudd_Complement(node: *mut DdNode) -> *mut DdNode { ((node as usize) | 01) as *mut DdNode } /// Returns 1 if a pointer is complemented. -pub const unsafe fn Cudd_IsComplement(node: *mut DdNode) -> c_int { +#[inline] +pub unsafe fn Cudd_IsComplement(node: *mut DdNode) -> c_int { ((node as usize) & 1) as c_int } @@ -517,22 +534,39 @@ extern "C" { pub fn Cudd_SetNumberXovers(dd: *mut DdManager, numberXovers: c_int) -> c_void; pub fn Cudd_ReadOrderRandomization(dd: *mut DdManager) -> c_uint; pub fn Cudd_SetOrderRandomization(dd: *mut DdManager, factor: c_uint) -> c_void; - pub fn Cudd_ReadMemoryInUse(dd: *mut DdManager) -> c_ulong; + pub fn Cudd_ReadMemoryInUse(dd: *mut DdManager) -> size_t; pub fn Cudd_PrintInfo(dd: *mut DdManager, fp: *mut FILE) -> c_int; pub fn Cudd_ReadPeakNodeCount(dd: *mut DdManager) -> c_long; pub fn Cudd_ReadPeakLiveNodeCount(dd: *mut DdManager) -> c_int; pub fn Cudd_ReadNodeCount(dd: *mut DdManager) -> c_long; pub fn Cudd_zddReadNodeCount(dd: *mut DdManager) -> c_long; - //pub fn Cudd_AddHook(dd: *mut DdManager, f: c_DD_HFP, where: Cudd_HookType ) -> c_int; - //pub fn Cudd_RemoveHook(dd: *mut DdManager, f: c_DD_HFP, where: Cudd_HookType ) -> c_int; - //pub fn Cudd_IsInHook(dd: *mut DdManager, f: c_DD_HFP, where: Cudd_HookType ) -> c_int; - pub fn Cudd_StdPreReordHook(dd: *mut DdManager, str: *mut c_char, data: *mut c_void) -> c_int; - pub fn Cudd_StdPostReordHook(dd: *mut DdManager, str: *mut c_char, data: *mut c_void) -> c_int; + pub fn Cudd_AddHook(dd: *mut DdManager, f: DD_HOOK_FUNCTION, hook_type: Cudd_HookType) + -> c_int; + pub fn Cudd_RemoveHook( + dd: *mut DdManager, + f: DD_HOOK_FUNCTION, + hook_type: Cudd_HookType, + ) -> c_int; + pub fn Cudd_IsInHook( + dd: *mut DdManager, + f: DD_HOOK_FUNCTION, + hook_type: Cudd_HookType, + ) -> c_int; + pub fn Cudd_StdPreReordHook(dd: *mut DdManager, str: *const c_char, data: *mut c_void) + -> c_int; + pub fn Cudd_StdPostReordHook( + dd: *mut DdManager, + str: *const c_char, + data: *mut c_void, + ) -> c_int; pub fn Cudd_EnableReorderingReporting(dd: *mut DdManager) -> c_int; pub fn Cudd_DisableReorderingReporting(dd: *mut DdManager) -> c_int; pub fn Cudd_ReorderingReporting(dd: *mut DdManager) -> c_int; - pub fn Cudd_PrintGroupedOrder(dd: *mut DdManager, str: *mut c_char, data: *mut c_void) - -> c_int; + pub fn Cudd_PrintGroupedOrder( + dd: *mut DdManager, + str: *const c_char, + data: *mut c_void, + ) -> c_int; pub fn Cudd_EnableOrderingMonitoring(dd: *mut DdManager) -> c_int; pub fn Cudd_DisableOrderingMonitoring(dd: *mut DdManager) -> c_int; pub fn Cudd_OrderingMonitoring(dd: *mut DdManager) -> c_int; @@ -540,6 +574,9 @@ extern "C" { pub fn Cudd_ReadApplicationHook(dd: *mut DdManager) -> *mut c_void; pub fn Cudd_ReadErrorCode(dd: *mut DdManager) -> Cudd_ErrorType; pub fn Cudd_ClearErrorCode(dd: *mut DdManager) -> c_void; + pub fn Cudd_InstallOutOfMemoryHandler( + newHandler: DD_OUT_OF_MEMORY_FUNCTION, + ) -> DD_OUT_OF_MEMORY_FUNCTION; pub fn Cudd_ReadStdout(dd: *mut DdManager) -> *mut FILE; pub fn Cudd_SetStdout(dd: *mut DdManager, fp: *mut FILE) -> c_void; pub fn Cudd_ReadStderr(dd: *mut DdManager) -> *mut FILE; @@ -549,8 +586,8 @@ extern "C" { pub fn Cudd_ReadSwapSteps(dd: *mut DdManager) -> c_double; pub fn Cudd_ReadMaxLive(dd: *mut DdManager) -> c_uint; pub fn Cudd_SetMaxLive(dd: *mut DdManager, maxLive: c_uint) -> c_void; - pub fn Cudd_ReadMaxMemory(dd: *mut DdManager) -> c_ulong; - pub fn Cudd_SetMaxMemory(dd: *mut DdManager, maxMemory: c_ulong) -> c_void; + pub fn Cudd_ReadMaxMemory(dd: *mut DdManager) -> size_t; + pub fn Cudd_SetMaxMemory(dd: *mut DdManager, maxMemory: size_t) -> size_t; pub fn Cudd_bddBindVar(dd: *mut DdManager, index: c_int) -> c_int; pub fn Cudd_bddUnbindVar(dd: *mut DdManager, index: c_int) -> c_int; pub fn Cudd_bddVarIsBound(dd: *mut DdManager, index: c_int) -> c_int; @@ -569,8 +606,12 @@ extern "C" { f: *mut DdNode, cube: *mut DdNode, ) -> *mut DdNode; - //M1: extern DdNode * Cudd_addApply (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g); - + pub fn Cudd_addApply( + dd: *mut DdManager, + op: DD_APPLY_OPERATOR, + f: *mut DdNode, + g: *mut DdNode, + ) -> *mut DdNode; pub fn Cudd_addPlus( dd: *mut DdManager, f: *mut *mut DdNode, @@ -641,8 +682,11 @@ extern "C" { f: *mut *mut DdNode, g: *mut *mut DdNode, ) -> *mut DdNode; - //M1: extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f); - + pub fn Cudd_addMonadicApply( + dd: *mut DdManager, + op: DD_MONADIC_APPLY_OPERATOR, + f: *mut DdNode, + ) -> *mut DdNode; pub fn Cudd_addLog(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; pub fn Cudd_addFindMax(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; pub fn Cudd_addFindMin(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; @@ -696,26 +740,89 @@ extern "C" { limit: c_uint, ) -> *mut DdNode; pub fn Cudd_ApaNumberOfDigits(binaryDigits: c_int) -> c_int; - /* - pub fn Cudd_NewApaNumber(digits: c_int) -> c_DdApaNumber; - pub fn Cudd_ApaCopy(digits: c_int, source: c_DdApaNumber, dest: c_DdApaNumber) -> c_void; - pub fn Cudd_ApaAdd(digits: c_int, a: c_DdApaNumber, b: c_DdApaNumber, sum: c_DdApaNumber) -> c_DdApaDigit; - pub fn Cudd_ApaSubtract(digits: c_int, a: c_DdApaNumber, b: c_DdApaNumber, diff: c_DdApaNumber) -> c_DdApaDigit; - pub fn Cudd_ApaShortDivision(digits: c_int, dividend: c_DdApaNumber, divisor: c_DdApaDigit, quotient: c_DdApaNumber) -> c_DdApaDigit; - pub fn Cudd_ApaIntDivision(digits: c_int, dividend: c_DdApaNumber, divisor: c_uint, quotient: c_DdApaNumber) -> c_uint; - pub fn Cudd_ApaShiftRight(digits: c_int, in: c_DdApaDigit, a: c_DdApaNumber, b: c_DdApaNumber) -> c_void; - pub fn Cudd_ApaSetToLiteral(digits: c_int, number: c_DdApaNumber, literal: c_DdApaDigit) -> c_void; - pub fn Cudd_ApaPowerOfTwo(digits: c_int, number: c_DdApaNumber, power: c_int) -> c_void; - pub fn Cudd_ApaCompare(digitsFirst: c_int, first: c_DdApaNumber, digitsSecond: c_int, second: c_DdApaNumber) -> c_int; - pub fn Cudd_ApaCompareRatios(digitsFirst: c_int, firstNum: c_DdApaNumber, firstDen: c_uint, digitsSecond: c_int, secondNum: c_DdApaNumber, secondDen: c_uint) -> c_int; - pub fn Cudd_ApaPrintHex(fp: *mut FILE, digits: c_int, number: c_DdApaNumber) -> c_int; - pub fn Cudd_ApaPrintDecimal(fp: *mut FILE, digits: c_int, number: c_DdApaNumber) -> c_int; - pub fn Cudd_ApaPrintExponential(fp: *mut FILE, digits: c_int, number: c_DdApaNumber, precision: c_int) -> c_int; - pub fn Cudd_ApaCountMinterm(manager: *mut DdManager, node: *mut DdNode, nvars: c_int, digits: *mut c_int) -> c_DdApaNumber; - pub fn Cudd_ApaPrintMinterm(fp: *mut FILE, dd: *mut DdManager, node: *mut DdNode, nvars: c_int) -> c_int; - pub fn Cudd_ApaPrintMintermExp(fp: *mut FILE, dd: *mut DdManager, node: *mut DdNode, nvars: c_int, precision: c_int) -> c_int; - pub fn Cudd_ApaPrintDensity(fp: *mut FILE, dd: *mut DdManager, node: *mut DdNode, nvars: c_int) -> c_int; - */ + pub fn Cudd_NewApaNumber(digits: c_int) -> DdApaNumber; + pub fn Cudd_FreeApaNumber(number: DdApaNumber) -> c_void; + pub fn Cudd_ApaCopy(digits: c_int, source: DdConstApaNumber, dest: DdApaNumber) -> c_void; + pub fn Cudd_ApaAdd( + digits: c_int, + a: DdConstApaNumber, + b: DdConstApaNumber, + sum: DdApaNumber, + ) -> DdApaDigit; + pub fn Cudd_ApaSubtract( + digits: c_int, + a: DdConstApaNumber, + b: DdConstApaNumber, + diff: DdApaNumber, + ) -> DdApaDigit; + pub fn Cudd_ApaShortDivision( + digits: c_int, + dividend: DdConstApaNumber, + divisor: DdApaDigit, + quotient: DdApaNumber, + ) -> DdApaDigit; + pub fn Cudd_ApaIntDivision( + digits: c_int, + dividend: DdConstApaNumber, + divisor: c_uint, + quotient: DdApaNumber, + ) -> c_uint; + pub fn Cudd_ApaShiftRight( + digits: c_int, + input: DdApaDigit, + a: DdConstApaNumber, + b: DdApaNumber, + ) -> c_void; + pub fn Cudd_ApaSetToLiteral(digits: c_int, number: DdApaNumber, literal: DdApaDigit) -> c_void; + pub fn Cudd_ApaPowerOfTwo(digits: c_int, number: DdApaNumber, power: c_int) -> c_void; + pub fn Cudd_ApaCompare( + digitsFirst: c_int, + first: DdConstApaNumber, + digitsSecond: c_int, + second: DdConstApaNumber, + ) -> c_int; + pub fn Cudd_ApaCompareRatios( + digitsFirst: c_int, + firstNum: DdConstApaNumber, + firstDen: c_uint, + digitsSecond: c_int, + secondNum: DdConstApaNumber, + secondDen: c_uint, + ) -> c_int; + pub fn Cudd_ApaPrintHex(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int; + pub fn Cudd_ApaPrintDecimal(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int; + pub fn Cudd_ApaStringDecimal(digits: c_int, number: DdConstApaNumber) -> *mut c_char; + pub fn Cudd_ApaPrintExponential( + fp: *mut FILE, + digits: c_int, + number: DdConstApaNumber, + precision: c_int, + ) -> c_int; + pub fn Cudd_ApaCountMinterm( + manager: *const DdManager, + node: *mut DdNode, + nvars: c_int, + digits: *mut c_int, + ) -> DdApaNumber; + pub fn Cudd_ApaPrintMinterm( + fp: *mut FILE, + dd: *const DdManager, + node: *mut DdNode, + nvars: c_int, + ) -> c_int; + pub fn Cudd_ApaPrintMintermExp( + fp: *mut FILE, + dd: *const DdManager, + node: *mut DdNode, + nvars: c_int, + precision: c_int, + ) -> c_int; + pub fn Cudd_ApaPrintDensity( + fp: *mut FILE, + dd: *mut DdManager, + node: *mut DdNode, + nvars: c_int, + ) -> c_int; pub fn Cudd_UnderApprox( dd: *mut DdManager, f: *mut DdNode, @@ -802,6 +909,13 @@ extern "C" { g: *mut DdNode, h: *mut DdNode, ) -> *mut DdNode; + pub fn Cudd_bddIteLimit( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + h: *mut DdNode, + limit: c_uint, + ) -> *mut DdNode; pub fn Cudd_bddIteConstant( dd: *mut DdManager, f: *mut DdNode, @@ -877,6 +991,12 @@ extern "C" { ) -> *mut DdNode; pub fn Cudd_Cofactor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; pub fn Cudd_CheckCube(dd: *mut DdManager, g: *mut DdNode) -> c_int; + pub fn Cudd_VarsAreSymmetric( + dd: *mut DdManager, + f: *mut DdNode, + index1: c_int, + index2: c_int, + ) -> c_int; pub fn Cudd_bddCompose( dd: *mut DdManager, f: *mut DdNode, @@ -1004,8 +1124,8 @@ extern "C" { pub fn Cudd_ReadIthClause( tlc: *mut DdTlcInfo, i: c_int, - var1: *mut DdHalfWord, - var2: *mut DdHalfWord, + var1: *mut c_uint, + var2: *mut c_uint, phase1: *mut c_int, phase2: *mut c_int, ) -> c_int; @@ -1075,6 +1195,7 @@ extern "C" { pub fn Cudd_bddCharToVect(dd: *mut DdManager, f: *mut DdNode) -> *mut *mut DdNode; pub fn Cudd_bddLICompaction(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; pub fn Cudd_bddSqueeze(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddInterpolate(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode; pub fn Cudd_bddMinimize(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; pub fn Cudd_SubsetCompress( dd: *mut DdManager, @@ -1088,12 +1209,6 @@ extern "C" { nvars: c_int, threshold: c_int, ) -> *mut DdNode; - pub fn Cudd_MakeTreeNode( - dd: *mut DdManager, - low: c_uint, - size: c_uint, - ttype: c_uint, - ) -> *mut MtrNode; pub fn Cudd_addHarwell( fp: *mut FILE, dd: *mut DdManager, @@ -1117,7 +1232,7 @@ extern "C" { numVarsZ: c_uint, numSlots: c_uint, cacheSize: c_uint, - maxMemory: c_ulong, + maxMemory: size_t, ) -> *mut DdManager; pub fn Cudd_Quit(unique: *mut DdManager) -> c_void; pub fn Cudd_PrintLinear(table: *mut DdManager) -> c_int; @@ -1154,8 +1269,16 @@ extern "C" { r: *mut DdNode, c: *mut DdNode, ) -> *mut DdNode; - //M1: extern DdNode * Cudd_PrioritySelect (DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DdNode * (*)(DdManager *, int, DdNode **, DdNode **, DdNode **)); - + pub fn Cudd_PrioritySelect( + dd: *mut DdManager, + R: *mut DdNode, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + z: *mut *mut DdNode, + Pi: *mut DdNode, + n: c_int, + PiFunc: DD_PRIORITY_FUNCTION, + ) -> *mut DdNode; pub fn Cudd_Xgty( dd: *mut DdManager, N: c_int, @@ -1380,6 +1503,7 @@ extern "C" { pub fn Cudd_PrintMinterm(manager: *mut DdManager, node: *mut DdNode) -> c_int; pub fn Cudd_bddPrintCover(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> c_int; pub fn Cudd_PrintDebug(dd: *mut DdManager, f: *mut DdNode, n: c_int, pr: c_int) -> c_int; + pub fn Cudd_PrintSummary(dd: *mut DdManager, f: *mut DdNode, n: c_int, mode: c_int) -> c_int; pub fn Cudd_DagSize(node: *mut DdNode) -> c_int; pub fn Cudd_EstimateCofactor( dd: *mut DdManager, @@ -1390,7 +1514,23 @@ extern "C" { pub fn Cudd_EstimateCofactorSimple(node: *mut DdNode, i: c_int) -> c_int; pub fn Cudd_SharingSize(nodeArray: *mut *mut DdNode, n: c_int) -> c_int; pub fn Cudd_CountMinterm(manager: *mut DdManager, node: *mut DdNode, nvars: c_int) -> c_double; - //pub fn Cudd_EpdCountMinterm(manager: *mut DdManager, node: *mut DdNode, nvars: c_int, epd: *mut c_EpDouble) -> c_int; + pub fn Cudd_EpdCountMinterm( + manager: *const DdManager, + node: *mut DdNode, + nvars: c_int, + epd: *mut EpDouble, + ) -> c_int; + /* + Type f128 cannot be safely represented in Rust at the moment, and 128-bit bytes don't have + a stable ABI format anyway. + + pub fn Cudd_LdblCountMinterm( + manager: *const DdManager, + node: *mut DdNode, + nvars: c_int, + ) -> f128; + */ + pub fn Cudd_EpdPrintMinterm(dd: *const DdManager, node: *mut DdNode, nvars: c_int) -> c_int; pub fn Cudd_CountPath(node: *mut DdNode) -> c_double; pub fn Cudd_CountPathsToNonZero(node: *mut DdNode) -> c_double; pub fn Cudd_SupportIndices( @@ -1486,10 +1626,11 @@ extern "C" { pub fn Cudd_IndicesToCube(dd: *mut DdManager, array: *mut c_int, n: c_int) -> *mut DdNode; pub fn Cudd_PrintVersion(fp: *mut FILE) -> c_void; pub fn Cudd_AverageDistance(dd: *mut DdManager) -> c_double; - //No match: extern long Cudd_Random (void); - pub fn Cudd_Srandom(seed: c_long) -> c_void; + pub fn Cudd_Random(dd: *mut DdManager) -> i32; + pub fn Cudd_Srandom(dd: *mut DdManager, seed: i32) -> c_void; pub fn Cudd_Density(dd: *mut DdManager, f: *mut DdNode, nvars: c_int) -> c_double; - pub fn Cudd_OutOfMem(size: c_long) -> c_void; + pub fn Cudd_OutOfMem(size: size_t) -> c_void; + pub fn Cudd_OutOfMemSilent(size: size_t) -> c_void; pub fn Cudd_zddCount(zdd: *mut DdManager, P: *mut DdNode) -> c_int; pub fn Cudd_zddCountDouble(zdd: *mut DdManager, P: *mut DdNode) -> c_double; pub fn Cudd_zddProduct(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; @@ -1499,12 +1640,6 @@ extern "C" { pub fn Cudd_zddWeakDivF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; pub fn Cudd_zddDivideF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; pub fn Cudd_zddComplement(dd: *mut DdManager, node: *mut DdNode) -> *mut DdNode; - pub fn Cudd_MakeZddTreeNode( - dd: *mut DdManager, - low: c_uint, - size: c_uint, - ttype: c_uint, - ) -> *mut MtrNode; pub fn Cudd_zddIsop( dd: *mut DdManager, L: *mut DdNode, @@ -1576,4 +1711,22 @@ extern "C" { pub fn Cudd_bddSetVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int; pub fn Cudd_bddIsVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int; pub fn Cudd_bddIsVarHardGroup(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_ReadTree(dd: *mut DdManager) -> *mut MtrNode; + pub fn Cudd_SetTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; + pub fn Cudd_FreeTree(dd: *mut DdManager) -> c_void; + pub fn Cudd_ReadZddTree(dd: *mut DdManager) -> *mut MtrNode; + pub fn Cudd_SetZddTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; + pub fn Cudd_FreeZddTree(dd: *mut DdManager) -> c_void; + pub fn Cudd_MakeTreeNode( + dd: *mut DdManager, + low: c_uint, + size: c_uint, + mtr_type: c_uint, + ) -> *mut MtrNode; + pub fn Cudd_MakeZddTreeNode( + dd: *mut DdManager, + low: c_uint, + size: c_uint, + mtr_type: c_uint, + ) -> *mut MtrNode; } From 5aaec71d5985d8a0820b9d8d11014b26071d0ebc Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 12:49:27 +0200 Subject: [PATCH 06/15] Convert iteration macros to inline functions. --- src/lib.rs | 297 +++++++++++++++++++++++++++-------------------------- 1 file changed, 149 insertions(+), 148 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 15b4572..610e759 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -9,6 +9,7 @@ mod test; use libc::{c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void, size_t, FILE}; use std::marker::{PhantomData, PhantomPinned}; use std::ops::Not; +use std::ptr::null_mut; /// An integer representation of a Boolean `true` constant. (This is not a DD construct!) pub const CUDD_TRUE: c_uint = 1; @@ -212,14 +213,22 @@ pub type DD_TIME_OUT_HANDLER = extern "C" fn(*mut DdManager, *mut c_void) -> c_v /// Complements a DD node by flipping the complement attribute of /// the pointer (the least significant bit). +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. #[inline] pub unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode { - ((node as usize) ^ 01) as *mut DdNode + ((node as usize) ^ 1) as *mut DdNode } /// Complements a DD node by flipping the complement attribute /// of the pointer if a condition is satisfied. The `condition` /// argument must be always either `1` or `0`. +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. #[inline] pub unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode { ((node as usize) ^ (condition as usize)) as *mut DdNode @@ -227,173 +236,165 @@ pub unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode { /// Computes the regular version of a node pointer (i.e. without the complement /// bit set, regardless of its previous value). +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. #[inline] pub unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode { - ((node as usize) & (01 as usize).not()) as *mut DdNode + ((node as usize) & (1_usize).not()) as *mut DdNode } /// Computes the complemented version of a node pointer (i.e. with a complement /// bit set, regardless of its previous value). +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. #[inline] pub unsafe fn Cudd_Complement(node: *mut DdNode) -> *mut DdNode { - ((node as usize) | 01) as *mut DdNode + ((node as usize) | 1) as *mut DdNode } /// Returns 1 if a pointer is complemented. +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. #[inline] pub unsafe fn Cudd_IsComplement(node: *mut DdNode) -> c_int { ((node as usize) & 1) as c_int } -/* -/** -@brief Returns the current position in the order of variable -index. - -@details Returns the current position in the order of variable -index. This macro is obsolete and is kept for compatibility. New -applications should use Cudd_ReadPerm instead. - -@sideeffect none - -@see Cudd_ReadPerm - - */ -#define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index)) - - -/** -@brief Iterates over the cubes of a decision diagram. - -@details Iterates over the cubes of a decision diagram f. -

    -
  • DdManager *manager; -
  • DdNode *f; -
  • DdGen *gen; -
  • int *cube; -
  • CUDD_VALUE_TYPE value; -
-Cudd_ForeachCube allocates and frees the generator. Therefore the -application should not try to do that. Also, the cube is freed at the -end of Cudd_ForeachCube and hence is not available outside of the loop.

-CAUTION: It is assumed that dynamic reordering will not occur while -there are open generators. It is the user's responsibility to make sure -that dynamic reordering does not occur. As long as new nodes are not created -during generation, and dynamic reordering is not called explicitly, -dynamic reordering will not occur. Alternatively, it is sufficient to -disable dynamic reordering. It is a mistake to dispose of a diagram -on which generation is ongoing. - -@sideeffect none - -@see Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree -Cudd_IsGenEmpty Cudd_AutodynDisable - - */ -#define Cudd_ForeachCube(manager, f, gen, cube, value)\ -for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\ -Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ -(void) Cudd_NextCube(gen, &cube, &value)) - - -/** -@brief Iterates over the primes of a Boolean function. - -@details Iterates over the primes of a Boolean function producing -a prime, but not necessarily irredundant, cover. -

    -
  • DdManager *manager; -
  • DdNode *l; -
  • DdNode *u; -
  • DdGen *gen; -
  • int *cube; -
-The Boolean function is described by an upper bound and a lower bound. If -the function is completely specified, the two bounds coincide. -Cudd_ForeachPrime allocates and frees the generator. Therefore the -application should not try to do that. Also, the cube is freed at the -end of Cudd_ForeachPrime and hence is not available outside of the loop.

-CAUTION: It is a mistake to change a diagram on which generation is ongoing. - -@sideeffect none - -@see Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree -Cudd_IsGenEmpty - - */ -#define Cudd_ForeachPrime(manager, l, u, gen, cube)\ -for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\ -Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ -(void) Cudd_NextPrime(gen, &cube)) - - -/** -@brief Iterates over the nodes of a decision diagram. - -@details Iterates over the nodes of a decision diagram f. -

    -
  • DdManager *manager; -
  • DdNode *f; -
  • DdGen *gen; -
  • DdNode *node; -
-The nodes are returned in a seemingly random order. -Cudd_ForeachNode allocates and frees the generator. Therefore the -application should not try to do that.

-CAUTION: It is assumed that dynamic reordering will not occur while -there are open generators. It is the user's responsibility to make sure -that dynamic reordering does not occur. As long as new nodes are not created -during generation, and dynamic reordering is not called explicitly, -dynamic reordering will not occur. Alternatively, it is sufficient to -disable dynamic reordering. It is a mistake to dispose of a diagram -on which generation is ongoing. - -@sideeffect none - -@see Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree -Cudd_IsGenEmpty Cudd_AutodynDisable - - */ -#define Cudd_ForeachNode(manager, f, gen, node)\ -for((gen) = Cudd_FirstNode(manager, f, &node);\ -Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ -(void) Cudd_NextNode(gen, &node)) - - -/** -@brief Iterates over the paths of a %ZDD. - -@details Iterates over the paths of a %ZDD f. -

    -
  • DdManager *manager; -
  • DdNode *f; -
  • DdGen *gen; -
  • int *path; -
-Cudd_zddForeachPath allocates and frees the generator. Therefore the -application should not try to do that. Also, the path is freed at the -end of Cudd_zddForeachPath and hence is not available outside of the loop.

-CAUTION: It is assumed that dynamic reordering will not occur while -there are open generators. It is the user's responsibility to make sure -that dynamic reordering does not occur. As long as new nodes are not created -during generation, and dynamic reordering is not called explicitly, -dynamic reordering will not occur. Alternatively, it is sufficient to -disable dynamic reordering. It is a mistake to dispose of a diagram -on which generation is ongoing. - -@sideeffect none +/// Returns the current position in the order of variable +/// index. This macro is obsolete and is kept for compatibility. New +/// applications should use `Cudd_ReadPerm` instead. +/// +/// # Safety +/// +/// Follows the same invariants as `Cudd_ReadPerm`. +#[inline] +pub unsafe fn Cudd_ReadIndex(dd: *mut DdManager, index: c_int) -> c_int { + Cudd_ReadPerm(dd, index) +} -@see Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree -Cudd_IsGenEmpty Cudd_AutodynDisable +/// Iterates over the cubes of a decision diagram f. The length of the cube is the number +/// of variables in the CUDD manager when the iteration is started. +/// +/// See `Cudd_FirstCube` for more info. +/// +/// # Safety +/// +/// The cube is freed at the end of Cudd_ForeachCube and hence is not available +/// outside of the loop. +/// +/// CAUTION: It is assumed that dynamic reordering will not occur while +/// there are open generators. It is the user's responsibility to make sure +/// that dynamic reordering does not occur. As long as new nodes are not created +/// during generation, and dynamic reordering is not called explicitly, +/// dynamic reordering will not occur. Alternatively, it is sufficient to +/// disable dynamic reordering. It is a mistake to dispose of a diagram +/// on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_ForeachCube( + manager: *mut DdManager, + f: *mut DdNode, + mut action: F, +) { + let mut cube = null_mut(); + let mut value = 0.0; + let gen = Cudd_FirstCube(manager, f, &mut cube, &mut value); + while Cudd_IsGenEmpty(gen) != 1 { + action(cube, value); + Cudd_NextCube(gen, &mut cube, &mut value); + } + Cudd_GenFree(gen); +} - */ -#define Cudd_zddForeachPath(manager, f, gen, path)\ -for((gen) = Cudd_zddFirstPath(manager, f, &path);\ -Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : CUDD_TRUE;\ -(void) Cudd_zddNextPath(gen, &path)) +/// Iterates over the primes of a Boolean function producing +/// a prime (but not necessarily irredundant) cover. +/// For more information, see `Cudd_FirstPrime`. +/// +/// # Safety +/// +/// The Boolean function is described by an upper bound and a lower bound. If +/// the function is completely specified, the two bounds coincide. +/// Cudd_ForeachPrime allocates and frees the generator. Therefore the +/// application should not try to do that. Also, the cube is freed at the +/// end of Cudd_ForeachPrime and hence is not available outside of the loop.

+/// CAUTION: It is a mistake to change a diagram on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_ForeachPrime( + manager: *mut DdManager, + l: *mut DdNode, + u: *mut DdNode, + mut action: F, +) { + let mut cube = null_mut(); + let gen = Cudd_FirstPrime(manager, l, u, &mut cube); + while Cudd_IsGenEmpty(gen) != 1 { + action(cube); + Cudd_NextPrime(gen, &mut cube); + } + Cudd_GenFree(gen); +} +/// Iterates over the nodes of a decision diagram `f`. See also `Cudd_FirstNode`. +/// +/// # Safety +/// +/// The nodes are returned in a seemingly random order. +/// +/// CAUTION: It is assumed that dynamic reordering will not occur while +/// there are open generators. It is the user's responsibility to make sure +/// that dynamic reordering does not occur. As long as new nodes are not created +/// during generation, and dynamic reordering is not called explicitly, +/// dynamic reordering will not occur. Alternatively, it is sufficient to +/// disable dynamic reordering. It is a mistake to dispose of a diagram +/// on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_ForeachNode( + manager: *mut DdManager, + f: *mut DdNode, + mut action: F, +) { + let mut node = null_mut(); + let gen = Cudd_FirstNode(manager, f, &mut node); + while Cudd_IsGenEmpty(gen) != 1 { + action(node); + Cudd_NextNode(gen, &mut node); + } + Cudd_GenFree(gen); +} - */ +/// Iterates over the paths of a ZDD `f`. +/// +/// # Safety +/// +/// The path is freed at the end of Cudd_zddForeachPath and hence is not available outside +/// of the loop. +/// +/// CAUTION: It is assumed that dynamic reordering will not occur while +/// there are open generators. It is the user's responsibility to make sure +/// that dynamic reordering does not occur. As long as new nodes are not created +/// during generation, and dynamic reordering is not called explicitly, +/// dynamic reordering will not occur. Alternatively, it is sufficient to +/// disable dynamic reordering. It is a mistake to dispose of a diagram +/// on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_zddForeachPath( + manager: *mut DdManager, + f: *mut DdNode, + mut action: F, +) { + let mut path = null_mut(); + let gen = Cudd_zddFirstPath(manager, f, &mut path); + while Cudd_IsGenEmpty(gen) != 1 { + action(path); + Cudd_zddNextPath(gen, &mut path); + } + Cudd_GenFree(gen); +} extern "C" { pub fn Cudd_addNewVar(dd: *mut DdManager) -> *mut DdNode; From 670251bd0c6a79e10aa151fe94653072fb088b0e Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 13:37:04 +0200 Subject: [PATCH 07/15] Update library structure to enable inclusion of other CUDD modules. --- README.md | 26 +- src/cudd.rs | 1675 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 1706 +-------------------------------------------------- src/test.rs | 6 +- 4 files changed, 1729 insertions(+), 1684 deletions(-) create mode 100644 src/cudd.rs diff --git a/README.md b/README.md index 755906a..e8ff0cf 100644 --- a/README.md +++ b/README.md @@ -4,11 +4,25 @@ # Rust Bindings for the CUDD library -Allows usage of the CUDD decision diagram library from Rust (tested on Linux and macOS). Uses version `2.5.1` of CUDD available from the unofficial [Github mirror](https://github.com/ivmai/cudd). +This crate provides unsafe Rust bindings for the University of Colorado decision diagram package (CUDD). It uses version `3.0.0` of CUDD available from the unofficial [Github mirror](https://github.com/ivmai/cudd) and compiles on Linux and MacOS (you should be also able to build CUDD on Windows using cygwin, but the project is not set-up to do it automatically). -To learn more about CUDD, check out the [manual](https://add-lib.scce.info/assets/documents/cudd-manual.pdf) or [API documentation](https://add-lib.scce.info/assets/doxygen-cudd-documentation/cudd_8h.html). +In the root module, you will find declarations of the C structs and types used +throughout CUDD. The main API of the CUDD package is then exported in `::cudd`. However, +CUDD also includes other "public" functionality (multiway-branching trees, extended +double precision numbers, serialisation, ...) which can be found in the remaining modules. -At the moment, the bindings are functional, but there are some TODOs that need to be addressed: - - Support for latest CUDD (3.0.0). - - CUDD uses C macros for some basic functionality. Port these to Rust. - - Everything is provided as raw C bindings. It would be nice to have *some* type-safe wrappers, at least for basic stuff. \ No newline at end of file +In some cases, there are macro and constant definitions which cannot be directly exported +to Rust. These have been re-implemented and should have their own documentation. +For the functions which are re-exported without change, please refer to the original +[CUDD doxygen](https://add-lib.scce.info/assets/doxygen-cudd-documentation/) and +[manual](https://add-lib.scce.info/assets/documents/cudd-manual.pdf). + +**Completeness:** The main CUDD API should be fully reproduced here (except for one small +issue with `f128` numbers). The remaining modules may still be incomplete: if you need +a function that isn't exported yet, let us know in the issues. + +**Correctness:** Unfortunately, CUDD cannot be processed using `bindgen`, so the API was +reproduced using a semi-automated method with a manual validation step (bunch of regexes +that a human makes sure didn't break anything ;)). As such, it is possible that there +are some minor problems that need to be sorted out. Please file an issue if you see any +unexpected behaviour or segfaults. \ No newline at end of file diff --git a/src/cudd.rs b/src/cudd.rs new file mode 100644 index 0000000..3b3d0e4 --- /dev/null +++ b/src/cudd.rs @@ -0,0 +1,1675 @@ +use libc::{c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void, size_t, FILE}; +use std::ops::Not; +use std::ptr::null_mut; +use { + DdApaDigit, DdApaNumber, DdConstApaNumber, DdGen, DdManager, DdNode, DdTlcInfo, EpDouble, + MtrNode, +}; + +/// Type of the value of a terminal node. +pub type CUDD_VALUE_TYPE = c_double; + +/// Type of the hook function. +pub type DD_HOOK_FUNCTION = extern "C" fn(*mut DdManager, *const c_char, *mut c_void) -> c_int; + +/// Type of the priority function. +pub type DD_PRIORITY_FUNCTION = extern "C" fn( + *mut DdManager, + c_int, + *mut *mut DdNode, + *mut *mut DdNode, + *mut *mut DdNode, +) -> *mut DdNode; + +/// Type of the apply operator function. +pub type DD_APPLY_OPERATOR = + extern "C" fn(*mut DdManager, *mut *mut DdNode, *mut *mut DdNode) -> *mut DdNode; + +/// Type of the monadic apply operator function. +pub type DD_MONADIC_APPLY_OPERATOR = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; + +/// Type of the two-operand cache tag function. +pub type DD_CACHE_TAG_FUNCTION_2 = + extern "C" fn(*mut DdManager, *mut DdNode, *mut DdNode) -> *mut DdNode; + +/// Type of the one-operand cache tag function. +pub type DD_CACHE_TAG_FUNCTION_1 = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; + +/// Type of the out-of-memory function. +pub type DD_OUT_OF_MEMORY_FUNCTION = extern "C" fn(size_t) -> c_void; + +/// Type of the Q-sort comparison function. +pub type DD_Q_SORT_FUNCTION = extern "C" fn(*const c_void, *const c_void) -> c_int; + +/// Type of the termination handler function. +pub type DD_TERMINATION_HANDLER = extern "C" fn(*const c_void) -> c_int; + +/// Type of the time-out handler function. +pub type DD_TIME_OUT_HANDLER = extern "C" fn(*mut DdManager, *mut c_void) -> c_void; + +/// An integer representation of a Boolean `true` constant. (This is not a DD construct!) +pub const CUDD_TRUE: c_uint = 1; +/// An integer representation of a Boolean `false` constant. (This is not a DD construct!) +pub const CUDD_FALSE: c_uint = 0; + +/// An special return value indicating an out-of-memory error. +pub const CUDD_OUT_OF_MEM: c_int = -1; + +/// Recommended default size of the unique node table. +pub const CUDD_UNIQUE_SLOTS: c_uint = 1 << 8; +/// Recommended default size of the operation cache table. +pub const CUDD_CACHE_SLOTS: c_uint = 1 << 18; + +/// Default option for `Cudd_addResidue`: specifies that the least-significant-bit is on top, +/// and the number is interpreted as unsigned. +pub const CUDD_RESIDUE_DEFAULT: c_int = 0; + +/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that +/// the most-significant-bit is on top. +pub const CUDD_RESIDUE_MSB: c_int = 1; + +/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that +/// the number should be interpreted as a signed two's complement. +pub const CUDD_RESIDUE_TC: c_int = 2; + +/// Types of variable reordering algorithms. +#[repr(C)] +pub enum Cudd_ReorderingType { + CUDD_REORDER_SAME, + CUDD_REORDER_NONE, + CUDD_REORDER_RANDOM, + CUDD_REORDER_RANDOM_PIVOT, + CUDD_REORDER_SIFT, + CUDD_REORDER_SIFT_CONVERGE, + CUDD_REORDER_SYMM_SIFT, + CUDD_REORDER_SYMM_SIFT_CONV, + CUDD_REORDER_WINDOW2, + CUDD_REORDER_WINDOW3, + CUDD_REORDER_WINDOW4, + CUDD_REORDER_WINDOW2_CONV, + CUDD_REORDER_WINDOW3_CONV, + CUDD_REORDER_WINDOW4_CONV, + CUDD_REORDER_GROUP_SIFT, + CUDD_REORDER_GROUP_SIFT_CONV, + CUDD_REORDER_ANNEALING, + CUDD_REORDER_GENETIC, + CUDD_REORDER_LINEAR, + CUDD_REORDER_LINEAR_CONVERGE, + CUDD_REORDER_LAZY_SIFT, + CUDD_REORDER_EXACT, +} + +/// Type of aggregation method algorithm. +#[repr(C)] +pub enum Cudd_AggregationType { + CUDD_NO_CHECK, + CUDD_GROUP_CHECK, + CUDD_GROUP_CHECK2, + CUDD_GROUP_CHECK3, + CUDD_GROUP_CHECK4, + CUDD_GROUP_CHECK5, + CUDD_GROUP_CHECK6, + CUDD_GROUP_CHECK7, + CUDD_GROUP_CHECK8, + CUDD_GROUP_CHECK9, +} + +/// Type of a hook. +#[repr(C)] +pub enum Cudd_HookType { + CUDD_PRE_GC_HOOK, + CUDD_POST_GC_HOOK, + CUDD_PRE_REORDERING_HOOK, + CUDD_POST_REORDERING_HOOK, +} + +// Type of an error code. +#[repr(C)] +pub enum Cudd_ErrorType { + CUDD_NO_ERROR, + CUDD_MEMORY_OUT, + CUDD_TOO_MANY_NODES, + CUDD_MAX_MEM_EXCEEDED, + CUDD_TIMEOUT_EXPIRED, + CUDD_TERMINATION, + CUDD_INVALID_ARG, + CUDD_INTERNAL_ERROR, +} + +/// Type of grouping used during lazy sifting. +#[repr(C)] +pub enum Cudd_LazyGroupType { + CUDD_LAZY_NONE, + CUDD_LAZY_SOFT_GROUP, + CUDD_LAZY_HARD_GROUP, + CUDD_LAZY_UNGROUP, +} + +/// Type of variable used during lazy sifting. +#[repr(C)] +pub enum Cudd_VariableType { + CUDD_VAR_PRIMARY_INPUT, + CUDD_VAR_PRESENT_STATE, + CUDD_VAR_NEXT_STATE, +} + +/// Complements a DD node by flipping the complement attribute of +/// the pointer (the least significant bit). +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. +#[inline] +pub unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode { + ((node as usize) ^ 1) as *mut DdNode +} + +/// Complements a DD node by flipping the complement attribute +/// of the pointer if a condition is satisfied. The `condition` +/// argument must be always either `1` or `0`. +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. +#[inline] +pub unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode { + ((node as usize) ^ (condition as usize)) as *mut DdNode +} + +/// Computes the regular version of a node pointer (i.e. without the complement +/// bit set, regardless of its previous value). +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. +#[inline] +pub unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode { + ((node as usize) & (1_usize).not()) as *mut DdNode +} + +/// Computes the complemented version of a node pointer (i.e. with a complement +/// bit set, regardless of its previous value). +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. +#[inline] +pub unsafe fn Cudd_Complement(node: *mut DdNode) -> *mut DdNode { + ((node as usize) | 1) as *mut DdNode +} + +/// Returns 1 if a pointer is complemented. +/// +/// # Safety +/// +/// This function should only be called on a valid `DdNode` pointer. +#[inline] +pub unsafe fn Cudd_IsComplement(node: *mut DdNode) -> c_int { + ((node as usize) & 1) as c_int +} + +/// Returns the current position in the order of variable +/// index. This macro is obsolete and is kept for compatibility. New +/// applications should use `Cudd_ReadPerm` instead. +/// +/// # Safety +/// +/// Follows the same invariants as `Cudd_ReadPerm`. +#[inline] +pub unsafe fn Cudd_ReadIndex(dd: *mut DdManager, index: c_int) -> c_int { + Cudd_ReadPerm(dd, index) +} + +/// Iterates over the cubes of a decision diagram f. The length of the cube is the number +/// of variables in the CUDD manager when the iteration is started. +/// +/// See `Cudd_FirstCube` for more info. +/// +/// # Safety +/// +/// The cube is freed at the end of Cudd_ForeachCube and hence is not available +/// outside of the loop. +/// +/// CAUTION: It is assumed that dynamic reordering will not occur while +/// there are open generators. It is the user's responsibility to make sure +/// that dynamic reordering does not occur. As long as new nodes are not created +/// during generation, and dynamic reordering is not called explicitly, +/// dynamic reordering will not occur. Alternatively, it is sufficient to +/// disable dynamic reordering. It is a mistake to dispose of a diagram +/// on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_ForeachCube( + manager: *mut DdManager, + f: *mut DdNode, + mut action: F, +) { + let mut cube = null_mut(); + let mut value = 0.0; + let gen = Cudd_FirstCube(manager, f, &mut cube, &mut value); + while Cudd_IsGenEmpty(gen) != 1 { + action(cube, value); + Cudd_NextCube(gen, &mut cube, &mut value); + } + Cudd_GenFree(gen); +} + +/// Iterates over the primes of a Boolean function producing +/// a prime (but not necessarily irredundant) cover. +/// For more information, see `Cudd_FirstPrime`. +/// +/// # Safety +/// +/// The Boolean function is described by an upper bound and a lower bound. If +/// the function is completely specified, the two bounds coincide. +/// Cudd_ForeachPrime allocates and frees the generator. Therefore the +/// application should not try to do that. Also, the cube is freed at the +/// end of Cudd_ForeachPrime and hence is not available outside of the loop.

+/// CAUTION: It is a mistake to change a diagram on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_ForeachPrime( + manager: *mut DdManager, + l: *mut DdNode, + u: *mut DdNode, + mut action: F, +) { + let mut cube = null_mut(); + let gen = Cudd_FirstPrime(manager, l, u, &mut cube); + while Cudd_IsGenEmpty(gen) != 1 { + action(cube); + Cudd_NextPrime(gen, &mut cube); + } + Cudd_GenFree(gen); +} + +/// Iterates over the nodes of a decision diagram `f`. See also `Cudd_FirstNode`. +/// +/// # Safety +/// +/// The nodes are returned in a seemingly random order. +/// +/// CAUTION: It is assumed that dynamic reordering will not occur while +/// there are open generators. It is the user's responsibility to make sure +/// that dynamic reordering does not occur. As long as new nodes are not created +/// during generation, and dynamic reordering is not called explicitly, +/// dynamic reordering will not occur. Alternatively, it is sufficient to +/// disable dynamic reordering. It is a mistake to dispose of a diagram +/// on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_ForeachNode( + manager: *mut DdManager, + f: *mut DdNode, + mut action: F, +) { + let mut node = null_mut(); + let gen = Cudd_FirstNode(manager, f, &mut node); + while Cudd_IsGenEmpty(gen) != 1 { + action(node); + Cudd_NextNode(gen, &mut node); + } + Cudd_GenFree(gen); +} + +/// Iterates over the paths of a ZDD `f`. +/// +/// # Safety +/// +/// The path is freed at the end of Cudd_zddForeachPath and hence is not available outside +/// of the loop. +/// +/// CAUTION: It is assumed that dynamic reordering will not occur while +/// there are open generators. It is the user's responsibility to make sure +/// that dynamic reordering does not occur. As long as new nodes are not created +/// during generation, and dynamic reordering is not called explicitly, +/// dynamic reordering will not occur. Alternatively, it is sufficient to +/// disable dynamic reordering. It is a mistake to dispose of a diagram +/// on which generation is ongoing. +#[inline] +pub unsafe fn Cudd_zddForeachPath( + manager: *mut DdManager, + f: *mut DdNode, + mut action: F, +) { + let mut path = null_mut(); + let gen = Cudd_zddFirstPath(manager, f, &mut path); + while Cudd_IsGenEmpty(gen) != 1 { + action(path); + Cudd_zddNextPath(gen, &mut path); + } + Cudd_GenFree(gen); +} + +extern "C" { + pub fn Cudd_addNewVar(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_addNewVarAtLevel(dd: *mut DdManager, level: c_int) -> *mut DdNode; + pub fn Cudd_bddNewVar(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_bddNewVarAtLevel(dd: *mut DdManager, level: c_int) -> *mut DdNode; + pub fn Cudd_bddIsVar(dd: *mut DdManager, f: *mut DdNode) -> c_int; + pub fn Cudd_addIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; + pub fn Cudd_bddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; + pub fn Cudd_zddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; + pub fn Cudd_zddVarsFromBddVars(dd: *mut DdManager, multiplicity: c_int) -> c_int; + pub fn Cudd_ReadMaxIndex() -> c_uint; + pub fn Cudd_addConst(dd: *mut DdManager, c: CUDD_VALUE_TYPE) -> *mut DdNode; + pub fn Cudd_IsConstant(node: *mut DdNode) -> c_int; + pub fn Cudd_IsNonConstant(f: *mut DdNode) -> c_int; + pub fn Cudd_T(node: *mut DdNode) -> *mut DdNode; + pub fn Cudd_E(node: *mut DdNode) -> *mut DdNode; + pub fn Cudd_V(node: *mut DdNode) -> CUDD_VALUE_TYPE; + pub fn Cudd_ReadStartTime(unique: *mut DdManager) -> c_ulong; + pub fn Cudd_ReadElapsedTime(unique: *mut DdManager) -> c_ulong; + pub fn Cudd_SetStartTime(unique: *mut DdManager, st: c_ulong) -> c_void; + pub fn Cudd_ResetStartTime(unique: *mut DdManager) -> c_void; + pub fn Cudd_ReadTimeLimit(unique: *mut DdManager) -> c_ulong; + pub fn Cudd_SetTimeLimit(unique: *mut DdManager, tl: c_ulong) -> c_ulong; + pub fn Cudd_UpdateTimeLimit(unique: *mut DdManager) -> c_void; + pub fn Cudd_IncreaseTimeLimit(unique: *mut DdManager, increase: c_ulong) -> c_void; + pub fn Cudd_UnsetTimeLimit(unique: *mut DdManager) -> c_void; + pub fn Cudd_TimeLimited(unique: *mut DdManager) -> c_int; + pub fn Cudd_RegisterTerminationCallback( + unique: *mut DdManager, + callback: DD_TERMINATION_HANDLER, + callback_arg: *mut c_void, + ) -> c_void; + pub fn Cudd_UnregisterTerminationCallback(unique: *mut DdManager) -> c_void; + pub fn Cudd_RegisterOutOfMemoryCallback( + unique: *mut DdManager, + callback: DD_OUT_OF_MEMORY_FUNCTION, + ) -> DD_OUT_OF_MEMORY_FUNCTION; + pub fn Cudd_UnregisterOutOfMemoryCallback(unique: *mut DdManager) -> c_void; + pub fn Cudd_RegisterTimeoutHandler( + unique: *mut DdManager, + handler: DD_TIME_OUT_HANDLER, + arg: *mut c_void, + ) -> c_void; + pub fn Cudd_ReadTimeoutHandler( + unique: *mut DdManager, + argp: *mut *mut c_void, + ) -> DD_TIME_OUT_HANDLER; + pub fn Cudd_AutodynEnable(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void; + pub fn Cudd_AutodynDisable(unique: *mut DdManager) -> c_void; + pub fn Cudd_ReorderingStatus(unique: *mut DdManager, method: *mut Cudd_ReorderingType) + -> c_int; + pub fn Cudd_AutodynEnableZdd(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void; + pub fn Cudd_AutodynDisableZdd(unique: *mut DdManager) -> c_void; + pub fn Cudd_ReorderingStatusZdd( + unique: *mut DdManager, + method: *mut Cudd_ReorderingType, + ) -> c_int; + pub fn Cudd_zddRealignmentEnabled(unique: *mut DdManager) -> c_int; + pub fn Cudd_zddRealignEnable(unique: *mut DdManager) -> c_void; + pub fn Cudd_zddRealignDisable(unique: *mut DdManager) -> c_void; + pub fn Cudd_bddRealignmentEnabled(unique: *mut DdManager) -> c_int; + pub fn Cudd_bddRealignEnable(unique: *mut DdManager) -> c_void; + pub fn Cudd_bddRealignDisable(unique: *mut DdManager) -> c_void; + pub fn Cudd_ReadOne(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_ReadZddOne(dd: *mut DdManager, i: c_int) -> *mut DdNode; + pub fn Cudd_ReadZero(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_ReadLogicZero(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_ReadPlusInfinity(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_ReadMinusInfinity(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_ReadBackground(dd: *mut DdManager) -> *mut DdNode; + pub fn Cudd_SetBackground(dd: *mut DdManager, bck: *mut DdNode) -> c_void; + pub fn Cudd_ReadCacheSlots(dd: *mut DdManager) -> c_uint; + pub fn Cudd_ReadCacheUsedSlots(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadCacheLookUps(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadCacheHits(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadRecursiveCalls(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadMinHit(dd: *mut DdManager) -> c_uint; + pub fn Cudd_SetMinHit(dd: *mut DdManager, hr: c_uint) -> c_void; + pub fn Cudd_ReadLooseUpTo(dd: *mut DdManager) -> c_uint; + pub fn Cudd_SetLooseUpTo(dd: *mut DdManager, lut: c_uint) -> c_void; + pub fn Cudd_ReadMaxCache(dd: *mut DdManager) -> c_uint; + pub fn Cudd_ReadMaxCacheHard(dd: *mut DdManager) -> c_uint; + pub fn Cudd_SetMaxCacheHard(dd: *mut DdManager, mc: c_uint) -> c_void; + pub fn Cudd_ReadSize(dd: *mut DdManager) -> c_int; + pub fn Cudd_ReadZddSize(dd: *mut DdManager) -> c_int; + pub fn Cudd_ReadSlots(dd: *mut DdManager) -> c_uint; + pub fn Cudd_ReadUsedSlots(dd: *mut DdManager) -> c_double; + pub fn Cudd_ExpectedUsedSlots(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadKeys(dd: *mut DdManager) -> c_uint; + pub fn Cudd_ReadDead(dd: *mut DdManager) -> c_uint; + pub fn Cudd_ReadMinDead(dd: *mut DdManager) -> c_uint; + pub fn Cudd_ReadReorderings(dd: *mut DdManager) -> c_uint; + pub fn Cudd_ReadMaxReorderings(dd: *mut DdManager) -> c_uint; + pub fn Cudd_SetMaxReorderings(dd: *mut DdManager, mr: c_uint) -> c_void; + pub fn Cudd_ReadReorderingTime(dd: *mut DdManager) -> c_long; + pub fn Cudd_ReadGarbageCollections(dd: *mut DdManager) -> c_int; + pub fn Cudd_ReadGarbageCollectionTime(dd: *mut DdManager) -> c_long; + pub fn Cudd_ReadNodesFreed(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadNodesDropped(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadUniqueLookUps(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadUniqueLinks(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadSiftMaxVar(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetSiftMaxVar(dd: *mut DdManager, smv: c_int) -> c_void; + pub fn Cudd_ReadSiftMaxSwap(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetSiftMaxSwap(dd: *mut DdManager, sms: c_int) -> c_void; + pub fn Cudd_ReadMaxGrowth(dd: *mut DdManager) -> c_double; + pub fn Cudd_SetMaxGrowth(dd: *mut DdManager, mg: c_double) -> c_void; + pub fn Cudd_ReadMaxGrowthAlternate(dd: *mut DdManager) -> c_double; + pub fn Cudd_SetMaxGrowthAlternate(dd: *mut DdManager, mg: c_double) -> c_void; + pub fn Cudd_ReadReorderingCycle(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetReorderingCycle(dd: *mut DdManager, cycle: c_int) -> c_void; + pub fn Cudd_NodeReadIndex(dd: *mut DdNode) -> c_uint; + pub fn Cudd_ReadPerm(dd: *mut DdManager, i: c_int) -> c_int; + pub fn Cudd_ReadPermZdd(dd: *mut DdManager, i: c_int) -> c_int; + pub fn Cudd_ReadInvPerm(dd: *mut DdManager, i: c_int) -> c_int; + pub fn Cudd_ReadInvPermZdd(dd: *mut DdManager, i: c_int) -> c_int; + pub fn Cudd_ReadVars(dd: *mut DdManager, i: c_int) -> *mut DdNode; + pub fn Cudd_ReadEpsilon(dd: *mut DdManager) -> CUDD_VALUE_TYPE; + pub fn Cudd_SetEpsilon(dd: *mut DdManager, ep: CUDD_VALUE_TYPE) -> c_void; + pub fn Cudd_ReadGroupcheck(dd: *mut DdManager) -> Cudd_AggregationType; + pub fn Cudd_SetGroupcheck(dd: *mut DdManager, gc: Cudd_AggregationType) -> c_void; + pub fn Cudd_GarbageCollectionEnabled(dd: *mut DdManager) -> c_int; + pub fn Cudd_EnableGarbageCollection(dd: *mut DdManager) -> c_void; + pub fn Cudd_DisableGarbageCollection(dd: *mut DdManager) -> c_void; + pub fn Cudd_DeadAreCounted(dd: *mut DdManager) -> c_int; + pub fn Cudd_TurnOnCountDead(dd: *mut DdManager) -> c_void; + pub fn Cudd_TurnOffCountDead(dd: *mut DdManager) -> c_void; + pub fn Cudd_ReadRecomb(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetRecomb(dd: *mut DdManager, recomb: c_int) -> c_void; + pub fn Cudd_ReadSymmviolation(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetSymmviolation(dd: *mut DdManager, symmviolation: c_int) -> c_void; + pub fn Cudd_ReadArcviolation(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetArcviolation(dd: *mut DdManager, arcviolation: c_int) -> c_void; + pub fn Cudd_ReadPopulationSize(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetPopulationSize(dd: *mut DdManager, populationSize: c_int) -> c_void; + pub fn Cudd_ReadNumberXovers(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetNumberXovers(dd: *mut DdManager, numberXovers: c_int) -> c_void; + pub fn Cudd_ReadOrderRandomization(dd: *mut DdManager) -> c_uint; + pub fn Cudd_SetOrderRandomization(dd: *mut DdManager, factor: c_uint) -> c_void; + pub fn Cudd_ReadMemoryInUse(dd: *mut DdManager) -> size_t; + pub fn Cudd_PrintInfo(dd: *mut DdManager, fp: *mut FILE) -> c_int; + pub fn Cudd_ReadPeakNodeCount(dd: *mut DdManager) -> c_long; + pub fn Cudd_ReadPeakLiveNodeCount(dd: *mut DdManager) -> c_int; + pub fn Cudd_ReadNodeCount(dd: *mut DdManager) -> c_long; + pub fn Cudd_zddReadNodeCount(dd: *mut DdManager) -> c_long; + pub fn Cudd_AddHook(dd: *mut DdManager, f: DD_HOOK_FUNCTION, hook_type: Cudd_HookType) + -> c_int; + pub fn Cudd_RemoveHook( + dd: *mut DdManager, + f: DD_HOOK_FUNCTION, + hook_type: Cudd_HookType, + ) -> c_int; + pub fn Cudd_IsInHook( + dd: *mut DdManager, + f: DD_HOOK_FUNCTION, + hook_type: Cudd_HookType, + ) -> c_int; + pub fn Cudd_StdPreReordHook(dd: *mut DdManager, str: *const c_char, data: *mut c_void) + -> c_int; + pub fn Cudd_StdPostReordHook( + dd: *mut DdManager, + str: *const c_char, + data: *mut c_void, + ) -> c_int; + pub fn Cudd_EnableReorderingReporting(dd: *mut DdManager) -> c_int; + pub fn Cudd_DisableReorderingReporting(dd: *mut DdManager) -> c_int; + pub fn Cudd_ReorderingReporting(dd: *mut DdManager) -> c_int; + pub fn Cudd_PrintGroupedOrder( + dd: *mut DdManager, + str: *const c_char, + data: *mut c_void, + ) -> c_int; + pub fn Cudd_EnableOrderingMonitoring(dd: *mut DdManager) -> c_int; + pub fn Cudd_DisableOrderingMonitoring(dd: *mut DdManager) -> c_int; + pub fn Cudd_OrderingMonitoring(dd: *mut DdManager) -> c_int; + pub fn Cudd_SetApplicationHook(dd: *mut DdManager, value: *mut c_void) -> c_void; + pub fn Cudd_ReadApplicationHook(dd: *mut DdManager) -> *mut c_void; + pub fn Cudd_ReadErrorCode(dd: *mut DdManager) -> Cudd_ErrorType; + pub fn Cudd_ClearErrorCode(dd: *mut DdManager) -> c_void; + pub fn Cudd_InstallOutOfMemoryHandler( + newHandler: DD_OUT_OF_MEMORY_FUNCTION, + ) -> DD_OUT_OF_MEMORY_FUNCTION; + pub fn Cudd_ReadStdout(dd: *mut DdManager) -> *mut FILE; + pub fn Cudd_SetStdout(dd: *mut DdManager, fp: *mut FILE) -> c_void; + pub fn Cudd_ReadStderr(dd: *mut DdManager) -> *mut FILE; + pub fn Cudd_SetStderr(dd: *mut DdManager, fp: *mut FILE) -> c_void; + pub fn Cudd_ReadNextReordering(dd: *mut DdManager) -> c_uint; + pub fn Cudd_SetNextReordering(dd: *mut DdManager, next: c_uint) -> c_void; + pub fn Cudd_ReadSwapSteps(dd: *mut DdManager) -> c_double; + pub fn Cudd_ReadMaxLive(dd: *mut DdManager) -> c_uint; + pub fn Cudd_SetMaxLive(dd: *mut DdManager, maxLive: c_uint) -> c_void; + pub fn Cudd_ReadMaxMemory(dd: *mut DdManager) -> size_t; + pub fn Cudd_SetMaxMemory(dd: *mut DdManager, maxMemory: size_t) -> size_t; + pub fn Cudd_bddBindVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddUnbindVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddVarIsBound(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_addExistAbstract( + manager: *mut DdManager, + f: *mut DdNode, + cube: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addUnivAbstract( + manager: *mut DdManager, + f: *mut DdNode, + cube: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addOrAbstract( + manager: *mut DdManager, + f: *mut DdNode, + cube: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addApply( + dd: *mut DdManager, + op: DD_APPLY_OPERATOR, + f: *mut DdNode, + g: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addPlus( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addTimes( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addThreshold( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addSetNZ( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addDivide( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addMinus( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addMinimum( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addMaximum( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addOneZeroMaximum( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addDiff( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addAgreement( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addOr(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode) -> *mut DdNode; + pub fn Cudd_addNand( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addNor(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode) + -> *mut DdNode; + pub fn Cudd_addXor(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode) + -> *mut DdNode; + pub fn Cudd_addXnor( + dd: *mut DdManager, + f: *mut *mut DdNode, + g: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addMonadicApply( + dd: *mut DdManager, + op: DD_MONADIC_APPLY_OPERATOR, + f: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addLog(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addFindMax(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addFindMin(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addIthBit(dd: *mut DdManager, f: *mut DdNode, bit: c_int) -> *mut DdNode; + pub fn Cudd_addScalarInverse( + dd: *mut DdManager, + f: *mut DdNode, + epsilon: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addIte( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + h: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addIteConstant( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + h: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addEvalConst(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addLeq(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> c_int; + pub fn Cudd_addCmpl(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addNegate(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addRoundOff(dd: *mut DdManager, f: *mut DdNode, N: c_int) -> *mut DdNode; + pub fn Cudd_addWalsh( + dd: *mut DdManager, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_addResidue( + dd: *mut DdManager, + n: c_int, + m: c_int, + options: c_int, + top: c_int, + ) -> *mut DdNode; + pub fn Cudd_bddAndAbstract( + manager: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + cube: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddAndAbstractLimit( + manager: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + cube: *mut DdNode, + limit: c_uint, + ) -> *mut DdNode; + pub fn Cudd_ApaNumberOfDigits(binaryDigits: c_int) -> c_int; + pub fn Cudd_NewApaNumber(digits: c_int) -> DdApaNumber; + pub fn Cudd_FreeApaNumber(number: DdApaNumber) -> c_void; + pub fn Cudd_ApaCopy(digits: c_int, source: DdConstApaNumber, dest: DdApaNumber) -> c_void; + pub fn Cudd_ApaAdd( + digits: c_int, + a: DdConstApaNumber, + b: DdConstApaNumber, + sum: DdApaNumber, + ) -> DdApaDigit; + pub fn Cudd_ApaSubtract( + digits: c_int, + a: DdConstApaNumber, + b: DdConstApaNumber, + diff: DdApaNumber, + ) -> DdApaDigit; + pub fn Cudd_ApaShortDivision( + digits: c_int, + dividend: DdConstApaNumber, + divisor: DdApaDigit, + quotient: DdApaNumber, + ) -> DdApaDigit; + pub fn Cudd_ApaIntDivision( + digits: c_int, + dividend: DdConstApaNumber, + divisor: c_uint, + quotient: DdApaNumber, + ) -> c_uint; + pub fn Cudd_ApaShiftRight( + digits: c_int, + input: DdApaDigit, + a: DdConstApaNumber, + b: DdApaNumber, + ) -> c_void; + pub fn Cudd_ApaSetToLiteral(digits: c_int, number: DdApaNumber, literal: DdApaDigit) -> c_void; + pub fn Cudd_ApaPowerOfTwo(digits: c_int, number: DdApaNumber, power: c_int) -> c_void; + pub fn Cudd_ApaCompare( + digitsFirst: c_int, + first: DdConstApaNumber, + digitsSecond: c_int, + second: DdConstApaNumber, + ) -> c_int; + pub fn Cudd_ApaCompareRatios( + digitsFirst: c_int, + firstNum: DdConstApaNumber, + firstDen: c_uint, + digitsSecond: c_int, + secondNum: DdConstApaNumber, + secondDen: c_uint, + ) -> c_int; + pub fn Cudd_ApaPrintHex(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int; + pub fn Cudd_ApaPrintDecimal(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int; + pub fn Cudd_ApaStringDecimal(digits: c_int, number: DdConstApaNumber) -> *mut c_char; + pub fn Cudd_ApaPrintExponential( + fp: *mut FILE, + digits: c_int, + number: DdConstApaNumber, + precision: c_int, + ) -> c_int; + pub fn Cudd_ApaCountMinterm( + manager: *const DdManager, + node: *mut DdNode, + nvars: c_int, + digits: *mut c_int, + ) -> DdApaNumber; + pub fn Cudd_ApaPrintMinterm( + fp: *mut FILE, + dd: *const DdManager, + node: *mut DdNode, + nvars: c_int, + ) -> c_int; + pub fn Cudd_ApaPrintMintermExp( + fp: *mut FILE, + dd: *const DdManager, + node: *mut DdNode, + nvars: c_int, + precision: c_int, + ) -> c_int; + pub fn Cudd_ApaPrintDensity( + fp: *mut FILE, + dd: *mut DdManager, + node: *mut DdNode, + nvars: c_int, + ) -> c_int; + pub fn Cudd_UnderApprox( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + safe: c_int, + quality: c_double, + ) -> *mut DdNode; + pub fn Cudd_OverApprox( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + safe: c_int, + quality: c_double, + ) -> *mut DdNode; + pub fn Cudd_RemapUnderApprox( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + quality: c_double, + ) -> *mut DdNode; + pub fn Cudd_RemapOverApprox( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + quality: c_double, + ) -> *mut DdNode; + pub fn Cudd_BiasedUnderApprox( + dd: *mut DdManager, + f: *mut DdNode, + b: *mut DdNode, + numVars: c_int, + threshold: c_int, + quality1: c_double, + quality0: c_double, + ) -> *mut DdNode; + pub fn Cudd_BiasedOverApprox( + dd: *mut DdManager, + f: *mut DdNode, + b: *mut DdNode, + numVars: c_int, + threshold: c_int, + quality1: c_double, + quality0: c_double, + ) -> *mut DdNode; + pub fn Cudd_bddExistAbstract( + manager: *mut DdManager, + f: *mut DdNode, + cube: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddExistAbstractLimit( + manager: *mut DdManager, + f: *mut DdNode, + cube: *mut DdNode, + limit: c_uint, + ) -> *mut DdNode; + pub fn Cudd_bddXorExistAbstract( + manager: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + cube: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddUnivAbstract( + manager: *mut DdManager, + f: *mut DdNode, + cube: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddBooleanDiff(manager: *mut DdManager, f: *mut DdNode, x: c_int) -> *mut DdNode; + pub fn Cudd_bddVarIsDependent(dd: *mut DdManager, f: *mut DdNode, var: *mut DdNode) -> c_int; + pub fn Cudd_bddCorrelation(manager: *mut DdManager, f: *mut DdNode, g: *mut DdNode) + -> c_double; + pub fn Cudd_bddCorrelationWeights( + manager: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + prob: *mut c_double, + ) -> c_double; + pub fn Cudd_bddIte( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + h: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddIteLimit( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + h: *mut DdNode, + limit: c_uint, + ) -> *mut DdNode; + pub fn Cudd_bddIteConstant( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + h: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddIntersect(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddAnd(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddAndLimit( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + limit: c_uint, + ) -> *mut DdNode; + pub fn Cudd_bddOr(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddOrLimit( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + limit: c_uint, + ) -> *mut DdNode; + pub fn Cudd_bddNand(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddNor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddXor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddXnor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddXnorLimit( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + limit: c_uint, + ) -> *mut DdNode; + pub fn Cudd_bddLeq(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> c_int; + pub fn Cudd_addBddThreshold( + dd: *mut DdManager, + f: *mut DdNode, + value: CUDD_VALUE_TYPE, + ) -> *mut DdNode; + pub fn Cudd_addBddStrictThreshold( + dd: *mut DdManager, + f: *mut DdNode, + value: CUDD_VALUE_TYPE, + ) -> *mut DdNode; + pub fn Cudd_addBddInterval( + dd: *mut DdManager, + f: *mut DdNode, + lower: CUDD_VALUE_TYPE, + upper: CUDD_VALUE_TYPE, + ) -> *mut DdNode; + pub fn Cudd_addBddIthBit(dd: *mut DdManager, f: *mut DdNode, bit: c_int) -> *mut DdNode; + pub fn Cudd_BddToAdd(dd: *mut DdManager, B: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addBddPattern(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddTransfer( + ddSource: *mut DdManager, + ddDestination: *mut DdManager, + f: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_DebugCheck(table: *mut DdManager) -> c_int; + pub fn Cudd_CheckKeys(table: *mut DdManager) -> c_int; + pub fn Cudd_bddClippingAnd( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + maxDepth: c_int, + direction: c_int, + ) -> *mut DdNode; + pub fn Cudd_bddClippingAndAbstract( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + cube: *mut DdNode, + maxDepth: c_int, + direction: c_int, + ) -> *mut DdNode; + pub fn Cudd_Cofactor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_CheckCube(dd: *mut DdManager, g: *mut DdNode) -> c_int; + pub fn Cudd_VarsAreSymmetric( + dd: *mut DdManager, + f: *mut DdNode, + index1: c_int, + index2: c_int, + ) -> c_int; + pub fn Cudd_bddCompose( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + v: c_int, + ) -> *mut DdNode; + pub fn Cudd_addCompose( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + v: c_int, + ) -> *mut DdNode; + pub fn Cudd_addPermute( + manager: *mut DdManager, + node: *mut DdNode, + permut: *mut c_int, + ) -> *mut DdNode; + pub fn Cudd_addSwapVariables( + dd: *mut DdManager, + f: *mut DdNode, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_bddPermute( + manager: *mut DdManager, + node: *mut DdNode, + permut: *mut c_int, + ) -> *mut DdNode; + pub fn Cudd_bddVarMap(manager: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_SetVarMap( + manager: *mut DdManager, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + n: c_int, + ) -> c_int; + pub fn Cudd_bddSwapVariables( + dd: *mut DdManager, + f: *mut DdNode, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_bddAdjPermuteX( + dd: *mut DdManager, + B: *mut DdNode, + x: *mut *mut DdNode, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_addVectorCompose( + dd: *mut DdManager, + f: *mut DdNode, + vector: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addGeneralVectorCompose( + dd: *mut DdManager, + f: *mut DdNode, + vectorOn: *mut *mut DdNode, + vectorOff: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addNonSimCompose( + dd: *mut DdManager, + f: *mut DdNode, + vector: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddVectorCompose( + dd: *mut DdManager, + f: *mut DdNode, + vector: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddApproxConjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + conjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_bddApproxDisjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + disjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_bddIterConjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + conjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_bddIterDisjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + disjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_bddGenConjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + conjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_bddGenDisjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + disjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_bddVarConjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + conjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_bddVarDisjDecomp( + dd: *mut DdManager, + f: *mut DdNode, + disjuncts: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_FindEssential(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddIsVarEssential( + manager: *mut DdManager, + f: *mut DdNode, + id: c_int, + phase: c_int, + ) -> c_int; + pub fn Cudd_FindTwoLiteralClauses(dd: *mut DdManager, f: *mut DdNode) -> *mut DdTlcInfo; + pub fn Cudd_PrintTwoLiteralClauses( + dd: *mut DdManager, + f: *mut DdNode, + names: *mut *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Cudd_ReadIthClause( + tlc: *mut DdTlcInfo, + i: c_int, + var1: *mut c_uint, + var2: *mut c_uint, + phase1: *mut c_int, + phase2: *mut c_int, + ) -> c_int; + pub fn Cudd_tlcInfoFree(t: *mut DdTlcInfo) -> c_void; + pub fn Cudd_DumpBlif( + dd: *mut DdManager, + n: c_int, + f: *mut *mut DdNode, + inames: *const *const c_char, + onames: *const *const c_char, + mname: *mut c_char, + fp: *mut FILE, + mv: c_int, + ) -> c_int; + pub fn Cudd_DumpBlifBody( + dd: *mut DdManager, + n: c_int, + f: *mut *mut DdNode, + inames: *const *const c_char, + onames: *const *const c_char, + fp: *mut FILE, + mv: c_int, + ) -> c_int; + pub fn Cudd_DumpDot( + dd: *mut DdManager, + n: c_int, + f: *mut *mut DdNode, + inames: *const *const c_char, + onames: *const *const c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Cudd_DumpDaVinci( + dd: *mut DdManager, + n: c_int, + f: *mut *mut DdNode, + inames: *const *const c_char, + onames: *const *const c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Cudd_DumpDDcal( + dd: *mut DdManager, + n: c_int, + f: *mut *mut DdNode, + inames: *const *const c_char, + onames: *const *const c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Cudd_DumpFactoredForm( + dd: *mut DdManager, + n: c_int, + f: *mut *mut DdNode, + inames: *const *const c_char, + onames: *const *const c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Cudd_FactoredFormString( + dd: *mut DdManager, + f: *mut DdNode, + inames: *const *const c_char, + ) -> *mut c_char; + pub fn Cudd_bddConstrain(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddRestrict(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddNPAnd(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addConstrain(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddConstrainDecomp(dd: *mut DdManager, f: *mut DdNode) -> *mut *mut DdNode; + pub fn Cudd_addRestrict(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddCharToVect(dd: *mut DdManager, f: *mut DdNode) -> *mut *mut DdNode; + pub fn Cudd_bddLICompaction(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddSqueeze(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddInterpolate(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddMinimize(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; + pub fn Cudd_SubsetCompress( + dd: *mut DdManager, + f: *mut DdNode, + nvars: c_int, + threshold: c_int, + ) -> *mut DdNode; + pub fn Cudd_SupersetCompress( + dd: *mut DdManager, + f: *mut DdNode, + nvars: c_int, + threshold: c_int, + ) -> *mut DdNode; + pub fn Cudd_addHarwell( + fp: *mut FILE, + dd: *mut DdManager, + E: *mut *mut DdNode, + x: *mut *mut *mut DdNode, + y: *mut *mut *mut DdNode, + xn: *mut *mut *mut DdNode, + yn_: *mut *mut *mut DdNode, + nx: *mut c_int, + ny: *mut c_int, + m: *mut c_int, + n: *mut c_int, + bx: c_int, + sx: c_int, + by: c_int, + sy: c_int, + pr: c_int, + ) -> c_int; + pub fn Cudd_Init( + numVars: c_uint, + numVarsZ: c_uint, + numSlots: c_uint, + cacheSize: c_uint, + maxMemory: size_t, + ) -> *mut DdManager; + pub fn Cudd_Quit(unique: *mut DdManager) -> c_void; + pub fn Cudd_PrintLinear(table: *mut DdManager) -> c_int; + pub fn Cudd_ReadLinear(table: *mut DdManager, x: c_int, y: c_int) -> c_int; + pub fn Cudd_bddLiteralSetIntersection( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addMatrixMultiply( + dd: *mut DdManager, + A: *mut DdNode, + B: *mut DdNode, + z: *mut *mut DdNode, + nz: c_int, + ) -> *mut DdNode; + pub fn Cudd_addTimesPlus( + dd: *mut DdManager, + A: *mut DdNode, + B: *mut DdNode, + z: *mut *mut DdNode, + nz: c_int, + ) -> *mut DdNode; + pub fn Cudd_addTriangle( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + z: *mut *mut DdNode, + nz: c_int, + ) -> *mut DdNode; + pub fn Cudd_addOuterSum( + dd: *mut DdManager, + M: *mut DdNode, + r: *mut DdNode, + c: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_PrioritySelect( + dd: *mut DdManager, + R: *mut DdNode, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + z: *mut *mut DdNode, + Pi: *mut DdNode, + n: c_int, + PiFunc: DD_PRIORITY_FUNCTION, + ) -> *mut DdNode; + pub fn Cudd_Xgty( + dd: *mut DdManager, + N: c_int, + z: *mut *mut DdNode, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_Xeqy( + dd: *mut DdManager, + N: c_int, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_addXeqy( + dd: *mut DdManager, + N: c_int, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_Dxygtdxz( + dd: *mut DdManager, + N: c_int, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + z: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_Dxygtdyz( + dd: *mut DdManager, + N: c_int, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + z: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_Inequality( + dd: *mut DdManager, + N: c_int, + c: c_int, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_Disequality( + dd: *mut DdManager, + N: c_int, + c: c_int, + x: *mut *mut DdNode, + y: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddInterval( + dd: *mut DdManager, + N: c_int, + x: *mut *mut DdNode, + lowerB: c_uint, + upperB: c_uint, + ) -> *mut DdNode; + pub fn Cudd_CProjection(dd: *mut DdManager, R: *mut DdNode, Y: *mut DdNode) -> *mut DdNode; + pub fn Cudd_addHamming( + dd: *mut DdManager, + xVars: *mut *mut DdNode, + yVars: *mut *mut DdNode, + nVars: c_int, + ) -> *mut DdNode; + pub fn Cudd_MinHammingDist( + dd: *mut DdManager, + f: *mut DdNode, + minterm: *mut c_int, + upperBound: c_int, + ) -> c_int; + pub fn Cudd_bddClosestCube( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + distance: *mut c_int, + ) -> *mut DdNode; + pub fn Cudd_addRead( + fp: *mut FILE, + dd: *mut DdManager, + E: *mut *mut DdNode, + x: *mut *mut *mut DdNode, + y: *mut *mut *mut DdNode, + xn: *mut *mut *mut DdNode, + yn_: *mut *mut *mut DdNode, + nx: *mut c_int, + ny: *mut c_int, + m: *mut c_int, + n: *mut c_int, + bx: c_int, + sx: c_int, + by: c_int, + sy: c_int, + ) -> c_int; + pub fn Cudd_bddRead( + fp: *mut FILE, + dd: *mut DdManager, + E: *mut *mut DdNode, + x: *mut *mut *mut DdNode, + y: *mut *mut *mut DdNode, + nx: *mut c_int, + ny: *mut c_int, + m: *mut c_int, + n: *mut c_int, + bx: c_int, + sx: c_int, + by: c_int, + sy: c_int, + ) -> c_int; + pub fn Cudd_Ref(n: *mut DdNode) -> c_void; + pub fn Cudd_RecursiveDeref(table: *mut DdManager, n: *mut DdNode) -> c_void; + pub fn Cudd_IterDerefBdd(table: *mut DdManager, n: *mut DdNode) -> c_void; + pub fn Cudd_DelayedDerefBdd(table: *mut DdManager, n: *mut DdNode) -> c_void; + pub fn Cudd_RecursiveDerefZdd(table: *mut DdManager, n: *mut DdNode) -> c_void; + pub fn Cudd_Deref(node: *mut DdNode) -> c_void; + pub fn Cudd_CheckZeroRef(manager: *mut DdManager) -> c_int; + pub fn Cudd_ReduceHeap( + table: *mut DdManager, + heuristic: Cudd_ReorderingType, + minsize: c_int, + ) -> c_int; + pub fn Cudd_ShuffleHeap(table: *mut DdManager, permutation: *mut c_int) -> c_int; + pub fn Cudd_Eval(dd: *mut DdManager, f: *mut DdNode, inputs: *mut c_int) -> *mut DdNode; + pub fn Cudd_ShortestPath( + manager: *mut DdManager, + f: *mut DdNode, + weight: *mut c_int, + support: *mut c_int, + length: *mut c_int, + ) -> *mut DdNode; + pub fn Cudd_LargestCube( + manager: *mut DdManager, + f: *mut DdNode, + length: *mut c_int, + ) -> *mut DdNode; + pub fn Cudd_ShortestLength( + manager: *mut DdManager, + f: *mut DdNode, + weight: *mut c_int, + ) -> c_int; + pub fn Cudd_Decreasing(dd: *mut DdManager, f: *mut DdNode, i: c_int) -> *mut DdNode; + pub fn Cudd_Increasing(dd: *mut DdManager, f: *mut DdNode, i: c_int) -> *mut DdNode; + pub fn Cudd_EquivDC( + dd: *mut DdManager, + F: *mut DdNode, + G: *mut DdNode, + D: *mut DdNode, + ) -> c_int; + pub fn Cudd_bddLeqUnless( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + D: *mut DdNode, + ) -> c_int; + pub fn Cudd_EqualSupNorm( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + tolerance: CUDD_VALUE_TYPE, + pr: c_int, + ) -> c_int; + pub fn Cudd_bddMakePrime(dd: *mut DdManager, cube: *mut DdNode, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_bddMaximallyExpand( + dd: *mut DdManager, + lb: *mut DdNode, + ub: *mut DdNode, + f: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddLargestPrimeUnate( + dd: *mut DdManager, + f: *mut DdNode, + phaseBdd: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_CofMinterm(dd: *mut DdManager, node: *mut DdNode) -> *mut c_double; + pub fn Cudd_SolveEqn( + bdd: *mut DdManager, + F: *mut DdNode, + Y: *mut DdNode, + G: *mut *mut DdNode, + yIndex: *mut *mut c_int, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_VerifySol( + bdd: *mut DdManager, + F: *mut DdNode, + G: *mut *mut DdNode, + yIndex: *mut c_int, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_SplitSet( + manager: *mut DdManager, + S: *mut DdNode, + xVars: *mut *mut DdNode, + n: c_int, + m: c_double, + ) -> *mut DdNode; + pub fn Cudd_SubsetHeavyBranch( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + ) -> *mut DdNode; + pub fn Cudd_SupersetHeavyBranch( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + ) -> *mut DdNode; + pub fn Cudd_SubsetShortPaths( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + hardlimit: c_int, + ) -> *mut DdNode; + pub fn Cudd_SupersetShortPaths( + dd: *mut DdManager, + f: *mut DdNode, + numVars: c_int, + threshold: c_int, + hardlimit: c_int, + ) -> *mut DdNode; + pub fn Cudd_SymmProfile(table: *mut DdManager, lower: c_int, upper: c_int) -> c_void; + pub fn Cudd_Prime(p: c_uint) -> c_uint; + pub fn Cudd_Reserve(manager: *mut DdManager, amount: c_int) -> c_int; + pub fn Cudd_PrintMinterm(manager: *mut DdManager, node: *mut DdNode) -> c_int; + pub fn Cudd_bddPrintCover(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> c_int; + pub fn Cudd_PrintDebug(dd: *mut DdManager, f: *mut DdNode, n: c_int, pr: c_int) -> c_int; + pub fn Cudd_PrintSummary(dd: *mut DdManager, f: *mut DdNode, n: c_int, mode: c_int) -> c_int; + pub fn Cudd_DagSize(node: *mut DdNode) -> c_int; + pub fn Cudd_EstimateCofactor( + dd: *mut DdManager, + node: *mut DdNode, + i: c_int, + phase: c_int, + ) -> c_int; + pub fn Cudd_EstimateCofactorSimple(node: *mut DdNode, i: c_int) -> c_int; + pub fn Cudd_SharingSize(nodeArray: *mut *mut DdNode, n: c_int) -> c_int; + pub fn Cudd_CountMinterm(manager: *mut DdManager, node: *mut DdNode, nvars: c_int) -> c_double; + pub fn Cudd_EpdCountMinterm( + manager: *const DdManager, + node: *mut DdNode, + nvars: c_int, + epd: *mut EpDouble, + ) -> c_int; + /* + Type f128 cannot be safely represented in Rust at the moment, and 128-bit bytes don't have + a stable ABI format anyway. + + pub fn Cudd_LdblCountMinterm( + manager: *const DdManager, + node: *mut DdNode, + nvars: c_int, + ) -> f128; + */ + pub fn Cudd_EpdPrintMinterm(dd: *const DdManager, node: *mut DdNode, nvars: c_int) -> c_int; + pub fn Cudd_CountPath(node: *mut DdNode) -> c_double; + pub fn Cudd_CountPathsToNonZero(node: *mut DdNode) -> c_double; + pub fn Cudd_SupportIndices( + dd: *mut DdManager, + f: *mut DdNode, + indices: *mut *mut c_int, + ) -> c_int; + pub fn Cudd_Support(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_SupportIndex(dd: *mut DdManager, f: *mut DdNode) -> *mut c_int; + pub fn Cudd_SupportSize(dd: *mut DdManager, f: *mut DdNode) -> c_int; + pub fn Cudd_VectorSupportIndices( + dd: *mut DdManager, + F: *mut *mut DdNode, + n: c_int, + indices: *mut *mut c_int, + ) -> c_int; + pub fn Cudd_VectorSupport(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) -> *mut DdNode; + pub fn Cudd_VectorSupportIndex(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) + -> *mut c_int; + pub fn Cudd_VectorSupportSize(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) -> c_int; + pub fn Cudd_ClassifySupport( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + common: *mut *mut DdNode, + onlyF: *mut *mut DdNode, + onlyG: *mut *mut DdNode, + ) -> c_int; + pub fn Cudd_CountLeaves(node: *mut DdNode) -> c_int; + pub fn Cudd_bddPickOneCube( + ddm: *mut DdManager, + node: *mut DdNode, + string: *mut c_char, + ) -> c_int; + pub fn Cudd_bddPickOneMinterm( + dd: *mut DdManager, + f: *mut DdNode, + vars: *mut *mut DdNode, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_bddPickArbitraryMinterms( + dd: *mut DdManager, + f: *mut DdNode, + vars: *mut *mut DdNode, + n: c_int, + k: c_int, + ) -> *mut *mut DdNode; + pub fn Cudd_SubsetWithMaskVars( + dd: *mut DdManager, + f: *mut DdNode, + vars: *mut *mut DdNode, + nvars: c_int, + maskVars: *mut *mut DdNode, + mvars: c_int, + ) -> *mut DdNode; + pub fn Cudd_FirstCube( + dd: *mut DdManager, + f: *mut DdNode, + cube: *mut *mut c_int, + value: *mut CUDD_VALUE_TYPE, + ) -> *mut DdGen; + pub fn Cudd_NextCube( + gen: *mut DdGen, + cube: *mut *mut c_int, + value: *mut CUDD_VALUE_TYPE, + ) -> c_int; + pub fn Cudd_FirstPrime( + dd: *mut DdManager, + l: *mut DdNode, + u: *mut DdNode, + cube: *mut *mut c_int, + ) -> *mut DdGen; + pub fn Cudd_NextPrime(gen: *mut DdGen, cube: *mut *mut c_int) -> c_int; + pub fn Cudd_bddComputeCube( + dd: *mut DdManager, + vars: *mut *mut DdNode, + phase: *mut c_int, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_addComputeCube( + dd: *mut DdManager, + vars: *mut *mut DdNode, + phase: *mut c_int, + n: c_int, + ) -> *mut DdNode; + pub fn Cudd_CubeArrayToBdd(dd: *mut DdManager, array: *mut c_int) -> *mut DdNode; + pub fn Cudd_BddToCubeArray(dd: *mut DdManager, cube: *mut DdNode, array: *mut c_int) -> c_int; + pub fn Cudd_FirstNode(dd: *mut DdManager, f: *mut DdNode, node: *mut *mut DdNode) + -> *mut DdGen; + pub fn Cudd_NextNode(gen: *mut DdGen, node: *mut *mut DdNode) -> c_int; + pub fn Cudd_GenFree(gen: *mut DdGen) -> c_int; + pub fn Cudd_IsGenEmpty(gen: *mut DdGen) -> c_int; + pub fn Cudd_IndicesToCube(dd: *mut DdManager, array: *mut c_int, n: c_int) -> *mut DdNode; + pub fn Cudd_PrintVersion(fp: *mut FILE) -> c_void; + pub fn Cudd_AverageDistance(dd: *mut DdManager) -> c_double; + pub fn Cudd_Random(dd: *mut DdManager) -> i32; + pub fn Cudd_Srandom(dd: *mut DdManager, seed: i32) -> c_void; + pub fn Cudd_Density(dd: *mut DdManager, f: *mut DdNode, nvars: c_int) -> c_double; + pub fn Cudd_OutOfMem(size: size_t) -> c_void; + pub fn Cudd_OutOfMemSilent(size: size_t) -> c_void; + pub fn Cudd_zddCount(zdd: *mut DdManager, P: *mut DdNode) -> c_int; + pub fn Cudd_zddCountDouble(zdd: *mut DdManager, P: *mut DdNode) -> c_double; + pub fn Cudd_zddProduct(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddUnateProduct(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddWeakDiv(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddDivide(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddWeakDivF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddDivideF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddComplement(dd: *mut DdManager, node: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddIsop( + dd: *mut DdManager, + L: *mut DdNode, + U: *mut DdNode, + zdd_I: *mut *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_bddIsop(dd: *mut DdManager, L: *mut DdNode, U: *mut DdNode) -> *mut DdNode; + pub fn Cudd_MakeBddFromZddCover(dd: *mut DdManager, node: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddDagSize(p_node: *mut DdNode) -> c_int; + pub fn Cudd_zddCountMinterm(zdd: *mut DdManager, node: *mut DdNode, path: c_int) -> c_double; + pub fn Cudd_zddPrintSubtable(table: *mut DdManager) -> c_void; + pub fn Cudd_zddPortFromBdd(dd: *mut DdManager, B: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddPortToBdd(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddReduceHeap( + table: *mut DdManager, + heuristic: Cudd_ReorderingType, + minsize: c_int, + ) -> c_int; + pub fn Cudd_zddShuffleHeap(table: *mut DdManager, permutation: *mut c_int) -> c_int; + pub fn Cudd_zddIte( + dd: *mut DdManager, + f: *mut DdNode, + g: *mut DdNode, + h: *mut DdNode, + ) -> *mut DdNode; + pub fn Cudd_zddUnion(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddIntersect(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddDiff(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddDiffConst(zdd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddSubset1(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode; + pub fn Cudd_zddSubset0(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode; + pub fn Cudd_zddChange(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode; + pub fn Cudd_zddSymmProfile(table: *mut DdManager, lower: c_int, upper: c_int) -> c_void; + pub fn Cudd_zddPrintMinterm(zdd: *mut DdManager, node: *mut DdNode) -> c_int; + pub fn Cudd_zddPrintCover(zdd: *mut DdManager, node: *mut DdNode) -> c_int; + pub fn Cudd_zddPrintDebug(zdd: *mut DdManager, f: *mut DdNode, n: c_int, pr: c_int) -> c_int; + pub fn Cudd_zddFirstPath( + zdd: *mut DdManager, + f: *mut DdNode, + path: *mut *mut c_int, + ) -> *mut DdGen; + pub fn Cudd_zddNextPath(gen: *mut DdGen, path: *mut *mut c_int) -> c_int; + pub fn Cudd_zddCoverPathToString( + zdd: *mut DdManager, + path: *mut c_int, + str: *mut c_char, + ) -> *mut c_char; + pub fn Cudd_zddSupport(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; + pub fn Cudd_zddDumpDot( + dd: *mut DdManager, + n: c_int, + f: *mut *mut DdNode, + inames: *const *const c_char, + onames: *const *const c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Cudd_bddSetPiVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddSetPsVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddSetNsVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddIsPiVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddIsPsVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddIsNsVar(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddSetPairIndex(dd: *mut DdManager, index: c_int, pairIndex: c_int) -> c_int; + pub fn Cudd_bddReadPairIndex(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddSetVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddSetVarHardGroup(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddResetVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddIsVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddSetVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddIsVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_bddIsVarHardGroup(dd: *mut DdManager, index: c_int) -> c_int; + pub fn Cudd_ReadTree(dd: *mut DdManager) -> *mut MtrNode; + pub fn Cudd_SetTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; + pub fn Cudd_FreeTree(dd: *mut DdManager) -> c_void; + pub fn Cudd_ReadZddTree(dd: *mut DdManager) -> *mut MtrNode; + pub fn Cudd_SetZddTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; + pub fn Cudd_FreeZddTree(dd: *mut DdManager) -> c_void; + pub fn Cudd_MakeTreeNode( + dd: *mut DdManager, + low: c_uint, + size: c_uint, + mtr_type: c_uint, + ) -> *mut MtrNode; + pub fn Cudd_MakeZddTreeNode( + dd: *mut DdManager, + low: c_uint, + size: c_uint, + mtr_type: c_uint, + ) -> *mut MtrNode; +} diff --git a/src/lib.rs b/src/lib.rs index 610e759..707302d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,3 +1,31 @@ +//! This crate provides unsafe Rust bindings for the University of Colorado decision diagram +//! package (CUDD). It uses version `3.0.0` of CUDD available from the unofficial +//! [Github mirror](https://github.com/ivmai/cudd) and compiles on Linux and MacOS +//! (you should be also able to build CUDD on Windows using cygwin, but the project is not set-up +//! to do it automatically). +//! +//! In the root module, you will find declarations of the C structs and types used +//! throughout CUDD. The main API of the CUDD package is then exported in `::cudd`. However, +//! CUDD also includes other "public" functionality (multiway-branching trees, extended +//! double precision numbers, serialisation, ...) which can be found in the remaining modules. +//! +//! In some cases, there are macro and constant definitions which cannot be directly exported +//! to Rust. These have been re-implemented and should have their own documentation. +//! For the functions which are re-exported without change, please refer to the original +//! [CUDD doxygen](https://add-lib.scce.info/assets/doxygen-cudd-documentation/) and +//! [manual](https://add-lib.scce.info/assets/documents/cudd-manual.pdf). +//! +//! **Completeness:** The main CUDD API should be fully reproduced here (except for one small +//! issue with `f128` numbers). The remaining modules may still be incomplete: if you need +//! a function that isn't exported yet, let us know in the issues. +//! +//! **Correctness:** Unfortunately, CUDD cannot be processed using `bindgen`, so the API was +//! reproduced using a semi-automated method with a manual validation step (bunch of regexes +//! that a human makes sure didn't break anything ;)). As such, it is possible that there +//! are some minor problems that need to be sorted out. Please file an issue if you see any +//! unexpected behaviour or segfaults. +//! + // Allow non-idiomatic names in the whole crate. #![allow(non_camel_case_types)] #![allow(non_snake_case)] @@ -6,121 +34,12 @@ extern crate libc; #[cfg(test)] mod test; -use libc::{c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void, size_t, FILE}; -use std::marker::{PhantomData, PhantomPinned}; -use std::ops::Not; -use std::ptr::null_mut; - -/// An integer representation of a Boolean `true` constant. (This is not a DD construct!) -pub const CUDD_TRUE: c_uint = 1; -/// An integer representation of a Boolean `false` constant. (This is not a DD construct!) -pub const CUDD_FALSE: c_uint = 0; - -/// An special return value indicating an out-of-memory error. -pub const CUDD_OUT_OF_MEM: c_int = -1; - -/// Recommended default size of the unique node table. -pub const CUDD_UNIQUE_SLOTS: c_uint = 1 << 8; -/// Recommended default size of the operation cache table. -pub const CUDD_CACHE_SLOTS: c_uint = 1 << 18; - -/// Default option for `Cudd_addResidue`: specifies that the least-significant-bit is on top, -/// and the number is interpreted as unsigned. -pub const CUDD_RESIDUE_DEFAULT: c_int = 0; - -/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that -/// the most-significant-bit is on top. -pub const CUDD_RESIDUE_MSB: c_int = 1; - -/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that -/// the number should be interpreted as a signed two's complement. -pub const CUDD_RESIDUE_TC: c_int = 2; - -/// Types of variable reordering algorithms. -#[repr(C)] -pub enum Cudd_ReorderingType { - CUDD_REORDER_SAME, - CUDD_REORDER_NONE, - CUDD_REORDER_RANDOM, - CUDD_REORDER_RANDOM_PIVOT, - CUDD_REORDER_SIFT, - CUDD_REORDER_SIFT_CONVERGE, - CUDD_REORDER_SYMM_SIFT, - CUDD_REORDER_SYMM_SIFT_CONV, - CUDD_REORDER_WINDOW2, - CUDD_REORDER_WINDOW3, - CUDD_REORDER_WINDOW4, - CUDD_REORDER_WINDOW2_CONV, - CUDD_REORDER_WINDOW3_CONV, - CUDD_REORDER_WINDOW4_CONV, - CUDD_REORDER_GROUP_SIFT, - CUDD_REORDER_GROUP_SIFT_CONV, - CUDD_REORDER_ANNEALING, - CUDD_REORDER_GENETIC, - CUDD_REORDER_LINEAR, - CUDD_REORDER_LINEAR_CONVERGE, - CUDD_REORDER_LAZY_SIFT, - CUDD_REORDER_EXACT, -} - -/// Type of aggregation method algorithm. -#[repr(C)] -pub enum Cudd_AggregationType { - CUDD_NO_CHECK, - CUDD_GROUP_CHECK, - CUDD_GROUP_CHECK2, - CUDD_GROUP_CHECK3, - CUDD_GROUP_CHECK4, - CUDD_GROUP_CHECK5, - CUDD_GROUP_CHECK6, - CUDD_GROUP_CHECK7, - CUDD_GROUP_CHECK8, - CUDD_GROUP_CHECK9, -} - -/// Type of a hook. -#[repr(C)] -pub enum Cudd_HookType { - CUDD_PRE_GC_HOOK, - CUDD_POST_GC_HOOK, - CUDD_PRE_REORDERING_HOOK, - CUDD_POST_REORDERING_HOOK, -} - -// Type of an error code. -#[repr(C)] -pub enum Cudd_ErrorType { - CUDD_NO_ERROR, - CUDD_MEMORY_OUT, - CUDD_TOO_MANY_NODES, - CUDD_MAX_MEM_EXCEEDED, - CUDD_TIMEOUT_EXPIRED, - CUDD_TERMINATION, - CUDD_INVALID_ARG, - CUDD_INTERNAL_ERROR, -} - -/// Type of grouping used during lazy sifting. -#[repr(C)] -pub enum Cudd_LazyGroupType { - CUDD_LAZY_NONE, - CUDD_LAZY_SOFT_GROUP, - CUDD_LAZY_HARD_GROUP, - CUDD_LAZY_UNGROUP, -} - -/// Type of variable used during lazy sifting. -#[repr(C)] -pub enum Cudd_VariableType { - CUDD_VAR_PRIMARY_INPUT, - CUDD_VAR_PRESENT_STATE, - CUDD_VAR_NEXT_STATE, -} +/// Contains the declarations present in `cudd.h`. +pub mod cudd; -/// Type of the value of a terminal node. -pub type CUDD_VALUE_TYPE = c_double; +use std::marker::{PhantomData, PhantomPinned}; -/// An opaque C struct used to represent the decision diagram nodes. +/// An opaque C struct used to represent the decision diagram node. #[repr(C)] pub struct DdNode { _data: [u8; 0], @@ -150,7 +69,7 @@ pub type DdApaNumber = *mut DdApaDigit; /// A const-qualified version of `DdApaNumber`. pub type DdConstApaNumber = *const DdApaDigit; -/// An opaque C struct used to represent the result of computation of two-literal clauses. +/// An opaque C struct used to represent the result of the computation of two-literal clauses. /// /// See `Cudd_FindTwoLiteralClauses`. #[repr(C)] @@ -172,1562 +91,3 @@ pub struct MtrNode { _data: [u8; 0], _marker: PhantomData<(*mut u8, PhantomPinned)>, } - -/// Type of the hook function. -pub type DD_HOOK_FUNCTION = extern "C" fn(*mut DdManager, *const c_char, *mut c_void) -> c_int; - -/// Type of the priority function. -pub type DD_PRIORITY_FUNCTION = extern "C" fn( - *mut DdManager, - c_int, - *mut *mut DdNode, - *mut *mut DdNode, - *mut *mut DdNode, -) -> *mut DdNode; - -/// Type of the apply operator function. -pub type DD_APPLY_OPERATOR = - extern "C" fn(*mut DdManager, *mut *mut DdNode, *mut *mut DdNode) -> *mut DdNode; - -/// Type of the monadic apply operator function. -pub type DD_MONADIC_APPLY_OPERATOR = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; - -/// Type of the two-operand cache tag function. -pub type DD_CACHE_TAG_FUNCTION_2 = - extern "C" fn(*mut DdManager, *mut DdNode, *mut DdNode) -> *mut DdNode; - -/// Type of the one-operand cache tag function. -pub type DD_CACHE_TAG_FUNCTION_1 = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; - -/// Type of the out-of-memory function. -pub type DD_OUT_OF_MEMORY_FUNCTION = extern "C" fn(size_t) -> c_void; - -/// Type of the Q-sort comparison function. -pub type DD_Q_SORT_FUNCTION = extern "C" fn(*const c_void, *const c_void) -> c_int; - -/// Type of the termination handler function. -pub type DD_TERMINATION_HANDLER = extern "C" fn(*const c_void) -> c_int; - -/// Type of the time-out handler function. -pub type DD_TIME_OUT_HANDLER = extern "C" fn(*mut DdManager, *mut c_void) -> c_void; - -/// Complements a DD node by flipping the complement attribute of -/// the pointer (the least significant bit). -/// -/// # Safety -/// -/// This function should only be called on a valid `DdNode` pointer. -#[inline] -pub unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode { - ((node as usize) ^ 1) as *mut DdNode -} - -/// Complements a DD node by flipping the complement attribute -/// of the pointer if a condition is satisfied. The `condition` -/// argument must be always either `1` or `0`. -/// -/// # Safety -/// -/// This function should only be called on a valid `DdNode` pointer. -#[inline] -pub unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode { - ((node as usize) ^ (condition as usize)) as *mut DdNode -} - -/// Computes the regular version of a node pointer (i.e. without the complement -/// bit set, regardless of its previous value). -/// -/// # Safety -/// -/// This function should only be called on a valid `DdNode` pointer. -#[inline] -pub unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode { - ((node as usize) & (1_usize).not()) as *mut DdNode -} - -/// Computes the complemented version of a node pointer (i.e. with a complement -/// bit set, regardless of its previous value). -/// -/// # Safety -/// -/// This function should only be called on a valid `DdNode` pointer. -#[inline] -pub unsafe fn Cudd_Complement(node: *mut DdNode) -> *mut DdNode { - ((node as usize) | 1) as *mut DdNode -} - -/// Returns 1 if a pointer is complemented. -/// -/// # Safety -/// -/// This function should only be called on a valid `DdNode` pointer. -#[inline] -pub unsafe fn Cudd_IsComplement(node: *mut DdNode) -> c_int { - ((node as usize) & 1) as c_int -} - -/// Returns the current position in the order of variable -/// index. This macro is obsolete and is kept for compatibility. New -/// applications should use `Cudd_ReadPerm` instead. -/// -/// # Safety -/// -/// Follows the same invariants as `Cudd_ReadPerm`. -#[inline] -pub unsafe fn Cudd_ReadIndex(dd: *mut DdManager, index: c_int) -> c_int { - Cudd_ReadPerm(dd, index) -} - -/// Iterates over the cubes of a decision diagram f. The length of the cube is the number -/// of variables in the CUDD manager when the iteration is started. -/// -/// See `Cudd_FirstCube` for more info. -/// -/// # Safety -/// -/// The cube is freed at the end of Cudd_ForeachCube and hence is not available -/// outside of the loop. -/// -/// CAUTION: It is assumed that dynamic reordering will not occur while -/// there are open generators. It is the user's responsibility to make sure -/// that dynamic reordering does not occur. As long as new nodes are not created -/// during generation, and dynamic reordering is not called explicitly, -/// dynamic reordering will not occur. Alternatively, it is sufficient to -/// disable dynamic reordering. It is a mistake to dispose of a diagram -/// on which generation is ongoing. -#[inline] -pub unsafe fn Cudd_ForeachCube( - manager: *mut DdManager, - f: *mut DdNode, - mut action: F, -) { - let mut cube = null_mut(); - let mut value = 0.0; - let gen = Cudd_FirstCube(manager, f, &mut cube, &mut value); - while Cudd_IsGenEmpty(gen) != 1 { - action(cube, value); - Cudd_NextCube(gen, &mut cube, &mut value); - } - Cudd_GenFree(gen); -} - -/// Iterates over the primes of a Boolean function producing -/// a prime (but not necessarily irredundant) cover. -/// For more information, see `Cudd_FirstPrime`. -/// -/// # Safety -/// -/// The Boolean function is described by an upper bound and a lower bound. If -/// the function is completely specified, the two bounds coincide. -/// Cudd_ForeachPrime allocates and frees the generator. Therefore the -/// application should not try to do that. Also, the cube is freed at the -/// end of Cudd_ForeachPrime and hence is not available outside of the loop.

-/// CAUTION: It is a mistake to change a diagram on which generation is ongoing. -#[inline] -pub unsafe fn Cudd_ForeachPrime( - manager: *mut DdManager, - l: *mut DdNode, - u: *mut DdNode, - mut action: F, -) { - let mut cube = null_mut(); - let gen = Cudd_FirstPrime(manager, l, u, &mut cube); - while Cudd_IsGenEmpty(gen) != 1 { - action(cube); - Cudd_NextPrime(gen, &mut cube); - } - Cudd_GenFree(gen); -} - -/// Iterates over the nodes of a decision diagram `f`. See also `Cudd_FirstNode`. -/// -/// # Safety -/// -/// The nodes are returned in a seemingly random order. -/// -/// CAUTION: It is assumed that dynamic reordering will not occur while -/// there are open generators. It is the user's responsibility to make sure -/// that dynamic reordering does not occur. As long as new nodes are not created -/// during generation, and dynamic reordering is not called explicitly, -/// dynamic reordering will not occur. Alternatively, it is sufficient to -/// disable dynamic reordering. It is a mistake to dispose of a diagram -/// on which generation is ongoing. -#[inline] -pub unsafe fn Cudd_ForeachNode( - manager: *mut DdManager, - f: *mut DdNode, - mut action: F, -) { - let mut node = null_mut(); - let gen = Cudd_FirstNode(manager, f, &mut node); - while Cudd_IsGenEmpty(gen) != 1 { - action(node); - Cudd_NextNode(gen, &mut node); - } - Cudd_GenFree(gen); -} - -/// Iterates over the paths of a ZDD `f`. -/// -/// # Safety -/// -/// The path is freed at the end of Cudd_zddForeachPath and hence is not available outside -/// of the loop. -/// -/// CAUTION: It is assumed that dynamic reordering will not occur while -/// there are open generators. It is the user's responsibility to make sure -/// that dynamic reordering does not occur. As long as new nodes are not created -/// during generation, and dynamic reordering is not called explicitly, -/// dynamic reordering will not occur. Alternatively, it is sufficient to -/// disable dynamic reordering. It is a mistake to dispose of a diagram -/// on which generation is ongoing. -#[inline] -pub unsafe fn Cudd_zddForeachPath( - manager: *mut DdManager, - f: *mut DdNode, - mut action: F, -) { - let mut path = null_mut(); - let gen = Cudd_zddFirstPath(manager, f, &mut path); - while Cudd_IsGenEmpty(gen) != 1 { - action(path); - Cudd_zddNextPath(gen, &mut path); - } - Cudd_GenFree(gen); -} - -extern "C" { - pub fn Cudd_addNewVar(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_addNewVarAtLevel(dd: *mut DdManager, level: c_int) -> *mut DdNode; - pub fn Cudd_bddNewVar(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_bddNewVarAtLevel(dd: *mut DdManager, level: c_int) -> *mut DdNode; - pub fn Cudd_bddIsVar(dd: *mut DdManager, f: *mut DdNode) -> c_int; - pub fn Cudd_addIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; - pub fn Cudd_bddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; - pub fn Cudd_zddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode; - pub fn Cudd_zddVarsFromBddVars(dd: *mut DdManager, multiplicity: c_int) -> c_int; - pub fn Cudd_ReadMaxIndex() -> c_uint; - pub fn Cudd_addConst(dd: *mut DdManager, c: CUDD_VALUE_TYPE) -> *mut DdNode; - pub fn Cudd_IsConstant(node: *mut DdNode) -> c_int; - pub fn Cudd_IsNonConstant(f: *mut DdNode) -> c_int; - pub fn Cudd_T(node: *mut DdNode) -> *mut DdNode; - pub fn Cudd_E(node: *mut DdNode) -> *mut DdNode; - pub fn Cudd_V(node: *mut DdNode) -> CUDD_VALUE_TYPE; - pub fn Cudd_ReadStartTime(unique: *mut DdManager) -> c_ulong; - pub fn Cudd_ReadElapsedTime(unique: *mut DdManager) -> c_ulong; - pub fn Cudd_SetStartTime(unique: *mut DdManager, st: c_ulong) -> c_void; - pub fn Cudd_ResetStartTime(unique: *mut DdManager) -> c_void; - pub fn Cudd_ReadTimeLimit(unique: *mut DdManager) -> c_ulong; - pub fn Cudd_SetTimeLimit(unique: *mut DdManager, tl: c_ulong) -> c_ulong; - pub fn Cudd_UpdateTimeLimit(unique: *mut DdManager) -> c_void; - pub fn Cudd_IncreaseTimeLimit(unique: *mut DdManager, increase: c_ulong) -> c_void; - pub fn Cudd_UnsetTimeLimit(unique: *mut DdManager) -> c_void; - pub fn Cudd_TimeLimited(unique: *mut DdManager) -> c_int; - pub fn Cudd_RegisterTerminationCallback( - unique: *mut DdManager, - callback: DD_TERMINATION_HANDLER, - callback_arg: *mut c_void, - ) -> c_void; - pub fn Cudd_UnregisterTerminationCallback(unique: *mut DdManager) -> c_void; - pub fn Cudd_RegisterOutOfMemoryCallback( - unique: *mut DdManager, - callback: DD_OUT_OF_MEMORY_FUNCTION, - ) -> DD_OUT_OF_MEMORY_FUNCTION; - pub fn Cudd_UnregisterOutOfMemoryCallback(unique: *mut DdManager) -> c_void; - pub fn Cudd_RegisterTimeoutHandler( - unique: *mut DdManager, - handler: DD_TIME_OUT_HANDLER, - arg: *mut c_void, - ) -> c_void; - pub fn Cudd_ReadTimeoutHandler( - unique: *mut DdManager, - argp: *mut *mut c_void, - ) -> DD_TIME_OUT_HANDLER; - pub fn Cudd_AutodynEnable(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void; - pub fn Cudd_AutodynDisable(unique: *mut DdManager) -> c_void; - pub fn Cudd_ReorderingStatus(unique: *mut DdManager, method: *mut Cudd_ReorderingType) - -> c_int; - pub fn Cudd_AutodynEnableZdd(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void; - pub fn Cudd_AutodynDisableZdd(unique: *mut DdManager) -> c_void; - pub fn Cudd_ReorderingStatusZdd( - unique: *mut DdManager, - method: *mut Cudd_ReorderingType, - ) -> c_int; - pub fn Cudd_zddRealignmentEnabled(unique: *mut DdManager) -> c_int; - pub fn Cudd_zddRealignEnable(unique: *mut DdManager) -> c_void; - pub fn Cudd_zddRealignDisable(unique: *mut DdManager) -> c_void; - pub fn Cudd_bddRealignmentEnabled(unique: *mut DdManager) -> c_int; - pub fn Cudd_bddRealignEnable(unique: *mut DdManager) -> c_void; - pub fn Cudd_bddRealignDisable(unique: *mut DdManager) -> c_void; - pub fn Cudd_ReadOne(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_ReadZddOne(dd: *mut DdManager, i: c_int) -> *mut DdNode; - pub fn Cudd_ReadZero(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_ReadLogicZero(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_ReadPlusInfinity(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_ReadMinusInfinity(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_ReadBackground(dd: *mut DdManager) -> *mut DdNode; - pub fn Cudd_SetBackground(dd: *mut DdManager, bck: *mut DdNode) -> c_void; - pub fn Cudd_ReadCacheSlots(dd: *mut DdManager) -> c_uint; - pub fn Cudd_ReadCacheUsedSlots(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadCacheLookUps(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadCacheHits(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadRecursiveCalls(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadMinHit(dd: *mut DdManager) -> c_uint; - pub fn Cudd_SetMinHit(dd: *mut DdManager, hr: c_uint) -> c_void; - pub fn Cudd_ReadLooseUpTo(dd: *mut DdManager) -> c_uint; - pub fn Cudd_SetLooseUpTo(dd: *mut DdManager, lut: c_uint) -> c_void; - pub fn Cudd_ReadMaxCache(dd: *mut DdManager) -> c_uint; - pub fn Cudd_ReadMaxCacheHard(dd: *mut DdManager) -> c_uint; - pub fn Cudd_SetMaxCacheHard(dd: *mut DdManager, mc: c_uint) -> c_void; - pub fn Cudd_ReadSize(dd: *mut DdManager) -> c_int; - pub fn Cudd_ReadZddSize(dd: *mut DdManager) -> c_int; - pub fn Cudd_ReadSlots(dd: *mut DdManager) -> c_uint; - pub fn Cudd_ReadUsedSlots(dd: *mut DdManager) -> c_double; - pub fn Cudd_ExpectedUsedSlots(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadKeys(dd: *mut DdManager) -> c_uint; - pub fn Cudd_ReadDead(dd: *mut DdManager) -> c_uint; - pub fn Cudd_ReadMinDead(dd: *mut DdManager) -> c_uint; - pub fn Cudd_ReadReorderings(dd: *mut DdManager) -> c_uint; - pub fn Cudd_ReadMaxReorderings(dd: *mut DdManager) -> c_uint; - pub fn Cudd_SetMaxReorderings(dd: *mut DdManager, mr: c_uint) -> c_void; - pub fn Cudd_ReadReorderingTime(dd: *mut DdManager) -> c_long; - pub fn Cudd_ReadGarbageCollections(dd: *mut DdManager) -> c_int; - pub fn Cudd_ReadGarbageCollectionTime(dd: *mut DdManager) -> c_long; - pub fn Cudd_ReadNodesFreed(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadNodesDropped(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadUniqueLookUps(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadUniqueLinks(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadSiftMaxVar(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetSiftMaxVar(dd: *mut DdManager, smv: c_int) -> c_void; - pub fn Cudd_ReadSiftMaxSwap(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetSiftMaxSwap(dd: *mut DdManager, sms: c_int) -> c_void; - pub fn Cudd_ReadMaxGrowth(dd: *mut DdManager) -> c_double; - pub fn Cudd_SetMaxGrowth(dd: *mut DdManager, mg: c_double) -> c_void; - pub fn Cudd_ReadMaxGrowthAlternate(dd: *mut DdManager) -> c_double; - pub fn Cudd_SetMaxGrowthAlternate(dd: *mut DdManager, mg: c_double) -> c_void; - pub fn Cudd_ReadReorderingCycle(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetReorderingCycle(dd: *mut DdManager, cycle: c_int) -> c_void; - pub fn Cudd_NodeReadIndex(dd: *mut DdNode) -> c_uint; - pub fn Cudd_ReadPerm(dd: *mut DdManager, i: c_int) -> c_int; - pub fn Cudd_ReadPermZdd(dd: *mut DdManager, i: c_int) -> c_int; - pub fn Cudd_ReadInvPerm(dd: *mut DdManager, i: c_int) -> c_int; - pub fn Cudd_ReadInvPermZdd(dd: *mut DdManager, i: c_int) -> c_int; - pub fn Cudd_ReadVars(dd: *mut DdManager, i: c_int) -> *mut DdNode; - pub fn Cudd_ReadEpsilon(dd: *mut DdManager) -> CUDD_VALUE_TYPE; - pub fn Cudd_SetEpsilon(dd: *mut DdManager, ep: CUDD_VALUE_TYPE) -> c_void; - pub fn Cudd_ReadGroupcheck(dd: *mut DdManager) -> Cudd_AggregationType; - pub fn Cudd_SetGroupcheck(dd: *mut DdManager, gc: Cudd_AggregationType) -> c_void; - pub fn Cudd_GarbageCollectionEnabled(dd: *mut DdManager) -> c_int; - pub fn Cudd_EnableGarbageCollection(dd: *mut DdManager) -> c_void; - pub fn Cudd_DisableGarbageCollection(dd: *mut DdManager) -> c_void; - pub fn Cudd_DeadAreCounted(dd: *mut DdManager) -> c_int; - pub fn Cudd_TurnOnCountDead(dd: *mut DdManager) -> c_void; - pub fn Cudd_TurnOffCountDead(dd: *mut DdManager) -> c_void; - pub fn Cudd_ReadRecomb(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetRecomb(dd: *mut DdManager, recomb: c_int) -> c_void; - pub fn Cudd_ReadSymmviolation(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetSymmviolation(dd: *mut DdManager, symmviolation: c_int) -> c_void; - pub fn Cudd_ReadArcviolation(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetArcviolation(dd: *mut DdManager, arcviolation: c_int) -> c_void; - pub fn Cudd_ReadPopulationSize(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetPopulationSize(dd: *mut DdManager, populationSize: c_int) -> c_void; - pub fn Cudd_ReadNumberXovers(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetNumberXovers(dd: *mut DdManager, numberXovers: c_int) -> c_void; - pub fn Cudd_ReadOrderRandomization(dd: *mut DdManager) -> c_uint; - pub fn Cudd_SetOrderRandomization(dd: *mut DdManager, factor: c_uint) -> c_void; - pub fn Cudd_ReadMemoryInUse(dd: *mut DdManager) -> size_t; - pub fn Cudd_PrintInfo(dd: *mut DdManager, fp: *mut FILE) -> c_int; - pub fn Cudd_ReadPeakNodeCount(dd: *mut DdManager) -> c_long; - pub fn Cudd_ReadPeakLiveNodeCount(dd: *mut DdManager) -> c_int; - pub fn Cudd_ReadNodeCount(dd: *mut DdManager) -> c_long; - pub fn Cudd_zddReadNodeCount(dd: *mut DdManager) -> c_long; - pub fn Cudd_AddHook(dd: *mut DdManager, f: DD_HOOK_FUNCTION, hook_type: Cudd_HookType) - -> c_int; - pub fn Cudd_RemoveHook( - dd: *mut DdManager, - f: DD_HOOK_FUNCTION, - hook_type: Cudd_HookType, - ) -> c_int; - pub fn Cudd_IsInHook( - dd: *mut DdManager, - f: DD_HOOK_FUNCTION, - hook_type: Cudd_HookType, - ) -> c_int; - pub fn Cudd_StdPreReordHook(dd: *mut DdManager, str: *const c_char, data: *mut c_void) - -> c_int; - pub fn Cudd_StdPostReordHook( - dd: *mut DdManager, - str: *const c_char, - data: *mut c_void, - ) -> c_int; - pub fn Cudd_EnableReorderingReporting(dd: *mut DdManager) -> c_int; - pub fn Cudd_DisableReorderingReporting(dd: *mut DdManager) -> c_int; - pub fn Cudd_ReorderingReporting(dd: *mut DdManager) -> c_int; - pub fn Cudd_PrintGroupedOrder( - dd: *mut DdManager, - str: *const c_char, - data: *mut c_void, - ) -> c_int; - pub fn Cudd_EnableOrderingMonitoring(dd: *mut DdManager) -> c_int; - pub fn Cudd_DisableOrderingMonitoring(dd: *mut DdManager) -> c_int; - pub fn Cudd_OrderingMonitoring(dd: *mut DdManager) -> c_int; - pub fn Cudd_SetApplicationHook(dd: *mut DdManager, value: *mut c_void) -> c_void; - pub fn Cudd_ReadApplicationHook(dd: *mut DdManager) -> *mut c_void; - pub fn Cudd_ReadErrorCode(dd: *mut DdManager) -> Cudd_ErrorType; - pub fn Cudd_ClearErrorCode(dd: *mut DdManager) -> c_void; - pub fn Cudd_InstallOutOfMemoryHandler( - newHandler: DD_OUT_OF_MEMORY_FUNCTION, - ) -> DD_OUT_OF_MEMORY_FUNCTION; - pub fn Cudd_ReadStdout(dd: *mut DdManager) -> *mut FILE; - pub fn Cudd_SetStdout(dd: *mut DdManager, fp: *mut FILE) -> c_void; - pub fn Cudd_ReadStderr(dd: *mut DdManager) -> *mut FILE; - pub fn Cudd_SetStderr(dd: *mut DdManager, fp: *mut FILE) -> c_void; - pub fn Cudd_ReadNextReordering(dd: *mut DdManager) -> c_uint; - pub fn Cudd_SetNextReordering(dd: *mut DdManager, next: c_uint) -> c_void; - pub fn Cudd_ReadSwapSteps(dd: *mut DdManager) -> c_double; - pub fn Cudd_ReadMaxLive(dd: *mut DdManager) -> c_uint; - pub fn Cudd_SetMaxLive(dd: *mut DdManager, maxLive: c_uint) -> c_void; - pub fn Cudd_ReadMaxMemory(dd: *mut DdManager) -> size_t; - pub fn Cudd_SetMaxMemory(dd: *mut DdManager, maxMemory: size_t) -> size_t; - pub fn Cudd_bddBindVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddUnbindVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddVarIsBound(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_addExistAbstract( - manager: *mut DdManager, - f: *mut DdNode, - cube: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addUnivAbstract( - manager: *mut DdManager, - f: *mut DdNode, - cube: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addOrAbstract( - manager: *mut DdManager, - f: *mut DdNode, - cube: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addApply( - dd: *mut DdManager, - op: DD_APPLY_OPERATOR, - f: *mut DdNode, - g: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addPlus( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addTimes( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addThreshold( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addSetNZ( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addDivide( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addMinus( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addMinimum( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addMaximum( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addOneZeroMaximum( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addDiff( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addAgreement( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addOr(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode) -> *mut DdNode; - pub fn Cudd_addNand( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addNor(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode) - -> *mut DdNode; - pub fn Cudd_addXor(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode) - -> *mut DdNode; - pub fn Cudd_addXnor( - dd: *mut DdManager, - f: *mut *mut DdNode, - g: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addMonadicApply( - dd: *mut DdManager, - op: DD_MONADIC_APPLY_OPERATOR, - f: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addLog(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addFindMax(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addFindMin(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addIthBit(dd: *mut DdManager, f: *mut DdNode, bit: c_int) -> *mut DdNode; - pub fn Cudd_addScalarInverse( - dd: *mut DdManager, - f: *mut DdNode, - epsilon: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addIte( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - h: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addIteConstant( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - h: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addEvalConst(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addLeq(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> c_int; - pub fn Cudd_addCmpl(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addNegate(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addRoundOff(dd: *mut DdManager, f: *mut DdNode, N: c_int) -> *mut DdNode; - pub fn Cudd_addWalsh( - dd: *mut DdManager, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_addResidue( - dd: *mut DdManager, - n: c_int, - m: c_int, - options: c_int, - top: c_int, - ) -> *mut DdNode; - pub fn Cudd_bddAndAbstract( - manager: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - cube: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddAndAbstractLimit( - manager: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - cube: *mut DdNode, - limit: c_uint, - ) -> *mut DdNode; - pub fn Cudd_ApaNumberOfDigits(binaryDigits: c_int) -> c_int; - pub fn Cudd_NewApaNumber(digits: c_int) -> DdApaNumber; - pub fn Cudd_FreeApaNumber(number: DdApaNumber) -> c_void; - pub fn Cudd_ApaCopy(digits: c_int, source: DdConstApaNumber, dest: DdApaNumber) -> c_void; - pub fn Cudd_ApaAdd( - digits: c_int, - a: DdConstApaNumber, - b: DdConstApaNumber, - sum: DdApaNumber, - ) -> DdApaDigit; - pub fn Cudd_ApaSubtract( - digits: c_int, - a: DdConstApaNumber, - b: DdConstApaNumber, - diff: DdApaNumber, - ) -> DdApaDigit; - pub fn Cudd_ApaShortDivision( - digits: c_int, - dividend: DdConstApaNumber, - divisor: DdApaDigit, - quotient: DdApaNumber, - ) -> DdApaDigit; - pub fn Cudd_ApaIntDivision( - digits: c_int, - dividend: DdConstApaNumber, - divisor: c_uint, - quotient: DdApaNumber, - ) -> c_uint; - pub fn Cudd_ApaShiftRight( - digits: c_int, - input: DdApaDigit, - a: DdConstApaNumber, - b: DdApaNumber, - ) -> c_void; - pub fn Cudd_ApaSetToLiteral(digits: c_int, number: DdApaNumber, literal: DdApaDigit) -> c_void; - pub fn Cudd_ApaPowerOfTwo(digits: c_int, number: DdApaNumber, power: c_int) -> c_void; - pub fn Cudd_ApaCompare( - digitsFirst: c_int, - first: DdConstApaNumber, - digitsSecond: c_int, - second: DdConstApaNumber, - ) -> c_int; - pub fn Cudd_ApaCompareRatios( - digitsFirst: c_int, - firstNum: DdConstApaNumber, - firstDen: c_uint, - digitsSecond: c_int, - secondNum: DdConstApaNumber, - secondDen: c_uint, - ) -> c_int; - pub fn Cudd_ApaPrintHex(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int; - pub fn Cudd_ApaPrintDecimal(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int; - pub fn Cudd_ApaStringDecimal(digits: c_int, number: DdConstApaNumber) -> *mut c_char; - pub fn Cudd_ApaPrintExponential( - fp: *mut FILE, - digits: c_int, - number: DdConstApaNumber, - precision: c_int, - ) -> c_int; - pub fn Cudd_ApaCountMinterm( - manager: *const DdManager, - node: *mut DdNode, - nvars: c_int, - digits: *mut c_int, - ) -> DdApaNumber; - pub fn Cudd_ApaPrintMinterm( - fp: *mut FILE, - dd: *const DdManager, - node: *mut DdNode, - nvars: c_int, - ) -> c_int; - pub fn Cudd_ApaPrintMintermExp( - fp: *mut FILE, - dd: *const DdManager, - node: *mut DdNode, - nvars: c_int, - precision: c_int, - ) -> c_int; - pub fn Cudd_ApaPrintDensity( - fp: *mut FILE, - dd: *mut DdManager, - node: *mut DdNode, - nvars: c_int, - ) -> c_int; - pub fn Cudd_UnderApprox( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - safe: c_int, - quality: c_double, - ) -> *mut DdNode; - pub fn Cudd_OverApprox( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - safe: c_int, - quality: c_double, - ) -> *mut DdNode; - pub fn Cudd_RemapUnderApprox( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - quality: c_double, - ) -> *mut DdNode; - pub fn Cudd_RemapOverApprox( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - quality: c_double, - ) -> *mut DdNode; - pub fn Cudd_BiasedUnderApprox( - dd: *mut DdManager, - f: *mut DdNode, - b: *mut DdNode, - numVars: c_int, - threshold: c_int, - quality1: c_double, - quality0: c_double, - ) -> *mut DdNode; - pub fn Cudd_BiasedOverApprox( - dd: *mut DdManager, - f: *mut DdNode, - b: *mut DdNode, - numVars: c_int, - threshold: c_int, - quality1: c_double, - quality0: c_double, - ) -> *mut DdNode; - pub fn Cudd_bddExistAbstract( - manager: *mut DdManager, - f: *mut DdNode, - cube: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddExistAbstractLimit( - manager: *mut DdManager, - f: *mut DdNode, - cube: *mut DdNode, - limit: c_uint, - ) -> *mut DdNode; - pub fn Cudd_bddXorExistAbstract( - manager: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - cube: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddUnivAbstract( - manager: *mut DdManager, - f: *mut DdNode, - cube: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddBooleanDiff(manager: *mut DdManager, f: *mut DdNode, x: c_int) -> *mut DdNode; - pub fn Cudd_bddVarIsDependent(dd: *mut DdManager, f: *mut DdNode, var: *mut DdNode) -> c_int; - pub fn Cudd_bddCorrelation(manager: *mut DdManager, f: *mut DdNode, g: *mut DdNode) - -> c_double; - pub fn Cudd_bddCorrelationWeights( - manager: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - prob: *mut c_double, - ) -> c_double; - pub fn Cudd_bddIte( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - h: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddIteLimit( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - h: *mut DdNode, - limit: c_uint, - ) -> *mut DdNode; - pub fn Cudd_bddIteConstant( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - h: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddIntersect(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddAnd(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddAndLimit( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - limit: c_uint, - ) -> *mut DdNode; - pub fn Cudd_bddOr(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddOrLimit( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - limit: c_uint, - ) -> *mut DdNode; - pub fn Cudd_bddNand(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddNor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddXor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddXnor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddXnorLimit( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - limit: c_uint, - ) -> *mut DdNode; - pub fn Cudd_bddLeq(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> c_int; - pub fn Cudd_addBddThreshold( - dd: *mut DdManager, - f: *mut DdNode, - value: CUDD_VALUE_TYPE, - ) -> *mut DdNode; - pub fn Cudd_addBddStrictThreshold( - dd: *mut DdManager, - f: *mut DdNode, - value: CUDD_VALUE_TYPE, - ) -> *mut DdNode; - pub fn Cudd_addBddInterval( - dd: *mut DdManager, - f: *mut DdNode, - lower: CUDD_VALUE_TYPE, - upper: CUDD_VALUE_TYPE, - ) -> *mut DdNode; - pub fn Cudd_addBddIthBit(dd: *mut DdManager, f: *mut DdNode, bit: c_int) -> *mut DdNode; - pub fn Cudd_BddToAdd(dd: *mut DdManager, B: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addBddPattern(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddTransfer( - ddSource: *mut DdManager, - ddDestination: *mut DdManager, - f: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_DebugCheck(table: *mut DdManager) -> c_int; - pub fn Cudd_CheckKeys(table: *mut DdManager) -> c_int; - pub fn Cudd_bddClippingAnd( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - maxDepth: c_int, - direction: c_int, - ) -> *mut DdNode; - pub fn Cudd_bddClippingAndAbstract( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - cube: *mut DdNode, - maxDepth: c_int, - direction: c_int, - ) -> *mut DdNode; - pub fn Cudd_Cofactor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_CheckCube(dd: *mut DdManager, g: *mut DdNode) -> c_int; - pub fn Cudd_VarsAreSymmetric( - dd: *mut DdManager, - f: *mut DdNode, - index1: c_int, - index2: c_int, - ) -> c_int; - pub fn Cudd_bddCompose( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - v: c_int, - ) -> *mut DdNode; - pub fn Cudd_addCompose( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - v: c_int, - ) -> *mut DdNode; - pub fn Cudd_addPermute( - manager: *mut DdManager, - node: *mut DdNode, - permut: *mut c_int, - ) -> *mut DdNode; - pub fn Cudd_addSwapVariables( - dd: *mut DdManager, - f: *mut DdNode, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_bddPermute( - manager: *mut DdManager, - node: *mut DdNode, - permut: *mut c_int, - ) -> *mut DdNode; - pub fn Cudd_bddVarMap(manager: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_SetVarMap( - manager: *mut DdManager, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - n: c_int, - ) -> c_int; - pub fn Cudd_bddSwapVariables( - dd: *mut DdManager, - f: *mut DdNode, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_bddAdjPermuteX( - dd: *mut DdManager, - B: *mut DdNode, - x: *mut *mut DdNode, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_addVectorCompose( - dd: *mut DdManager, - f: *mut DdNode, - vector: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addGeneralVectorCompose( - dd: *mut DdManager, - f: *mut DdNode, - vectorOn: *mut *mut DdNode, - vectorOff: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addNonSimCompose( - dd: *mut DdManager, - f: *mut DdNode, - vector: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddVectorCompose( - dd: *mut DdManager, - f: *mut DdNode, - vector: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddApproxConjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - conjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_bddApproxDisjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - disjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_bddIterConjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - conjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_bddIterDisjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - disjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_bddGenConjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - conjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_bddGenDisjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - disjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_bddVarConjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - conjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_bddVarDisjDecomp( - dd: *mut DdManager, - f: *mut DdNode, - disjuncts: *mut *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_FindEssential(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddIsVarEssential( - manager: *mut DdManager, - f: *mut DdNode, - id: c_int, - phase: c_int, - ) -> c_int; - pub fn Cudd_FindTwoLiteralClauses(dd: *mut DdManager, f: *mut DdNode) -> *mut DdTlcInfo; - pub fn Cudd_PrintTwoLiteralClauses( - dd: *mut DdManager, - f: *mut DdNode, - names: *mut *mut c_char, - fp: *mut FILE, - ) -> c_int; - pub fn Cudd_ReadIthClause( - tlc: *mut DdTlcInfo, - i: c_int, - var1: *mut c_uint, - var2: *mut c_uint, - phase1: *mut c_int, - phase2: *mut c_int, - ) -> c_int; - pub fn Cudd_tlcInfoFree(t: *mut DdTlcInfo) -> c_void; - pub fn Cudd_DumpBlif( - dd: *mut DdManager, - n: c_int, - f: *mut *mut DdNode, - inames: *const *const c_char, - onames: *const *const c_char, - mname: *mut c_char, - fp: *mut FILE, - mv: c_int, - ) -> c_int; - pub fn Cudd_DumpBlifBody( - dd: *mut DdManager, - n: c_int, - f: *mut *mut DdNode, - inames: *const *const c_char, - onames: *const *const c_char, - fp: *mut FILE, - mv: c_int, - ) -> c_int; - pub fn Cudd_DumpDot( - dd: *mut DdManager, - n: c_int, - f: *mut *mut DdNode, - inames: *const *const c_char, - onames: *const *const c_char, - fp: *mut FILE, - ) -> c_int; - pub fn Cudd_DumpDaVinci( - dd: *mut DdManager, - n: c_int, - f: *mut *mut DdNode, - inames: *const *const c_char, - onames: *const *const c_char, - fp: *mut FILE, - ) -> c_int; - pub fn Cudd_DumpDDcal( - dd: *mut DdManager, - n: c_int, - f: *mut *mut DdNode, - inames: *const *const c_char, - onames: *const *const c_char, - fp: *mut FILE, - ) -> c_int; - pub fn Cudd_DumpFactoredForm( - dd: *mut DdManager, - n: c_int, - f: *mut *mut DdNode, - inames: *const *const c_char, - onames: *const *const c_char, - fp: *mut FILE, - ) -> c_int; - pub fn Cudd_FactoredFormString( - dd: *mut DdManager, - f: *mut DdNode, - inames: *const *const c_char, - ) -> *mut c_char; - pub fn Cudd_bddConstrain(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddRestrict(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddNPAnd(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addConstrain(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddConstrainDecomp(dd: *mut DdManager, f: *mut DdNode) -> *mut *mut DdNode; - pub fn Cudd_addRestrict(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddCharToVect(dd: *mut DdManager, f: *mut DdNode) -> *mut *mut DdNode; - pub fn Cudd_bddLICompaction(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddSqueeze(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddInterpolate(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddMinimize(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode; - pub fn Cudd_SubsetCompress( - dd: *mut DdManager, - f: *mut DdNode, - nvars: c_int, - threshold: c_int, - ) -> *mut DdNode; - pub fn Cudd_SupersetCompress( - dd: *mut DdManager, - f: *mut DdNode, - nvars: c_int, - threshold: c_int, - ) -> *mut DdNode; - pub fn Cudd_addHarwell( - fp: *mut FILE, - dd: *mut DdManager, - E: *mut *mut DdNode, - x: *mut *mut *mut DdNode, - y: *mut *mut *mut DdNode, - xn: *mut *mut *mut DdNode, - yn_: *mut *mut *mut DdNode, - nx: *mut c_int, - ny: *mut c_int, - m: *mut c_int, - n: *mut c_int, - bx: c_int, - sx: c_int, - by: c_int, - sy: c_int, - pr: c_int, - ) -> c_int; - pub fn Cudd_Init( - numVars: c_uint, - numVarsZ: c_uint, - numSlots: c_uint, - cacheSize: c_uint, - maxMemory: size_t, - ) -> *mut DdManager; - pub fn Cudd_Quit(unique: *mut DdManager) -> c_void; - pub fn Cudd_PrintLinear(table: *mut DdManager) -> c_int; - pub fn Cudd_ReadLinear(table: *mut DdManager, x: c_int, y: c_int) -> c_int; - pub fn Cudd_bddLiteralSetIntersection( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addMatrixMultiply( - dd: *mut DdManager, - A: *mut DdNode, - B: *mut DdNode, - z: *mut *mut DdNode, - nz: c_int, - ) -> *mut DdNode; - pub fn Cudd_addTimesPlus( - dd: *mut DdManager, - A: *mut DdNode, - B: *mut DdNode, - z: *mut *mut DdNode, - nz: c_int, - ) -> *mut DdNode; - pub fn Cudd_addTriangle( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - z: *mut *mut DdNode, - nz: c_int, - ) -> *mut DdNode; - pub fn Cudd_addOuterSum( - dd: *mut DdManager, - M: *mut DdNode, - r: *mut DdNode, - c: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_PrioritySelect( - dd: *mut DdManager, - R: *mut DdNode, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - z: *mut *mut DdNode, - Pi: *mut DdNode, - n: c_int, - PiFunc: DD_PRIORITY_FUNCTION, - ) -> *mut DdNode; - pub fn Cudd_Xgty( - dd: *mut DdManager, - N: c_int, - z: *mut *mut DdNode, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_Xeqy( - dd: *mut DdManager, - N: c_int, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_addXeqy( - dd: *mut DdManager, - N: c_int, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_Dxygtdxz( - dd: *mut DdManager, - N: c_int, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - z: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_Dxygtdyz( - dd: *mut DdManager, - N: c_int, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - z: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_Inequality( - dd: *mut DdManager, - N: c_int, - c: c_int, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_Disequality( - dd: *mut DdManager, - N: c_int, - c: c_int, - x: *mut *mut DdNode, - y: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddInterval( - dd: *mut DdManager, - N: c_int, - x: *mut *mut DdNode, - lowerB: c_uint, - upperB: c_uint, - ) -> *mut DdNode; - pub fn Cudd_CProjection(dd: *mut DdManager, R: *mut DdNode, Y: *mut DdNode) -> *mut DdNode; - pub fn Cudd_addHamming( - dd: *mut DdManager, - xVars: *mut *mut DdNode, - yVars: *mut *mut DdNode, - nVars: c_int, - ) -> *mut DdNode; - pub fn Cudd_MinHammingDist( - dd: *mut DdManager, - f: *mut DdNode, - minterm: *mut c_int, - upperBound: c_int, - ) -> c_int; - pub fn Cudd_bddClosestCube( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - distance: *mut c_int, - ) -> *mut DdNode; - pub fn Cudd_addRead( - fp: *mut FILE, - dd: *mut DdManager, - E: *mut *mut DdNode, - x: *mut *mut *mut DdNode, - y: *mut *mut *mut DdNode, - xn: *mut *mut *mut DdNode, - yn_: *mut *mut *mut DdNode, - nx: *mut c_int, - ny: *mut c_int, - m: *mut c_int, - n: *mut c_int, - bx: c_int, - sx: c_int, - by: c_int, - sy: c_int, - ) -> c_int; - pub fn Cudd_bddRead( - fp: *mut FILE, - dd: *mut DdManager, - E: *mut *mut DdNode, - x: *mut *mut *mut DdNode, - y: *mut *mut *mut DdNode, - nx: *mut c_int, - ny: *mut c_int, - m: *mut c_int, - n: *mut c_int, - bx: c_int, - sx: c_int, - by: c_int, - sy: c_int, - ) -> c_int; - pub fn Cudd_Ref(n: *mut DdNode) -> c_void; - pub fn Cudd_RecursiveDeref(table: *mut DdManager, n: *mut DdNode) -> c_void; - pub fn Cudd_IterDerefBdd(table: *mut DdManager, n: *mut DdNode) -> c_void; - pub fn Cudd_DelayedDerefBdd(table: *mut DdManager, n: *mut DdNode) -> c_void; - pub fn Cudd_RecursiveDerefZdd(table: *mut DdManager, n: *mut DdNode) -> c_void; - pub fn Cudd_Deref(node: *mut DdNode) -> c_void; - pub fn Cudd_CheckZeroRef(manager: *mut DdManager) -> c_int; - pub fn Cudd_ReduceHeap( - table: *mut DdManager, - heuristic: Cudd_ReorderingType, - minsize: c_int, - ) -> c_int; - pub fn Cudd_ShuffleHeap(table: *mut DdManager, permutation: *mut c_int) -> c_int; - pub fn Cudd_Eval(dd: *mut DdManager, f: *mut DdNode, inputs: *mut c_int) -> *mut DdNode; - pub fn Cudd_ShortestPath( - manager: *mut DdManager, - f: *mut DdNode, - weight: *mut c_int, - support: *mut c_int, - length: *mut c_int, - ) -> *mut DdNode; - pub fn Cudd_LargestCube( - manager: *mut DdManager, - f: *mut DdNode, - length: *mut c_int, - ) -> *mut DdNode; - pub fn Cudd_ShortestLength( - manager: *mut DdManager, - f: *mut DdNode, - weight: *mut c_int, - ) -> c_int; - pub fn Cudd_Decreasing(dd: *mut DdManager, f: *mut DdNode, i: c_int) -> *mut DdNode; - pub fn Cudd_Increasing(dd: *mut DdManager, f: *mut DdNode, i: c_int) -> *mut DdNode; - pub fn Cudd_EquivDC( - dd: *mut DdManager, - F: *mut DdNode, - G: *mut DdNode, - D: *mut DdNode, - ) -> c_int; - pub fn Cudd_bddLeqUnless( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - D: *mut DdNode, - ) -> c_int; - pub fn Cudd_EqualSupNorm( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - tolerance: CUDD_VALUE_TYPE, - pr: c_int, - ) -> c_int; - pub fn Cudd_bddMakePrime(dd: *mut DdManager, cube: *mut DdNode, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_bddMaximallyExpand( - dd: *mut DdManager, - lb: *mut DdNode, - ub: *mut DdNode, - f: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddLargestPrimeUnate( - dd: *mut DdManager, - f: *mut DdNode, - phaseBdd: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_CofMinterm(dd: *mut DdManager, node: *mut DdNode) -> *mut c_double; - pub fn Cudd_SolveEqn( - bdd: *mut DdManager, - F: *mut DdNode, - Y: *mut DdNode, - G: *mut *mut DdNode, - yIndex: *mut *mut c_int, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_VerifySol( - bdd: *mut DdManager, - F: *mut DdNode, - G: *mut *mut DdNode, - yIndex: *mut c_int, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_SplitSet( - manager: *mut DdManager, - S: *mut DdNode, - xVars: *mut *mut DdNode, - n: c_int, - m: c_double, - ) -> *mut DdNode; - pub fn Cudd_SubsetHeavyBranch( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - ) -> *mut DdNode; - pub fn Cudd_SupersetHeavyBranch( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - ) -> *mut DdNode; - pub fn Cudd_SubsetShortPaths( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - hardlimit: c_int, - ) -> *mut DdNode; - pub fn Cudd_SupersetShortPaths( - dd: *mut DdManager, - f: *mut DdNode, - numVars: c_int, - threshold: c_int, - hardlimit: c_int, - ) -> *mut DdNode; - pub fn Cudd_SymmProfile(table: *mut DdManager, lower: c_int, upper: c_int) -> c_void; - pub fn Cudd_Prime(p: c_uint) -> c_uint; - pub fn Cudd_Reserve(manager: *mut DdManager, amount: c_int) -> c_int; - pub fn Cudd_PrintMinterm(manager: *mut DdManager, node: *mut DdNode) -> c_int; - pub fn Cudd_bddPrintCover(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> c_int; - pub fn Cudd_PrintDebug(dd: *mut DdManager, f: *mut DdNode, n: c_int, pr: c_int) -> c_int; - pub fn Cudd_PrintSummary(dd: *mut DdManager, f: *mut DdNode, n: c_int, mode: c_int) -> c_int; - pub fn Cudd_DagSize(node: *mut DdNode) -> c_int; - pub fn Cudd_EstimateCofactor( - dd: *mut DdManager, - node: *mut DdNode, - i: c_int, - phase: c_int, - ) -> c_int; - pub fn Cudd_EstimateCofactorSimple(node: *mut DdNode, i: c_int) -> c_int; - pub fn Cudd_SharingSize(nodeArray: *mut *mut DdNode, n: c_int) -> c_int; - pub fn Cudd_CountMinterm(manager: *mut DdManager, node: *mut DdNode, nvars: c_int) -> c_double; - pub fn Cudd_EpdCountMinterm( - manager: *const DdManager, - node: *mut DdNode, - nvars: c_int, - epd: *mut EpDouble, - ) -> c_int; - /* - Type f128 cannot be safely represented in Rust at the moment, and 128-bit bytes don't have - a stable ABI format anyway. - - pub fn Cudd_LdblCountMinterm( - manager: *const DdManager, - node: *mut DdNode, - nvars: c_int, - ) -> f128; - */ - pub fn Cudd_EpdPrintMinterm(dd: *const DdManager, node: *mut DdNode, nvars: c_int) -> c_int; - pub fn Cudd_CountPath(node: *mut DdNode) -> c_double; - pub fn Cudd_CountPathsToNonZero(node: *mut DdNode) -> c_double; - pub fn Cudd_SupportIndices( - dd: *mut DdManager, - f: *mut DdNode, - indices: *mut *mut c_int, - ) -> c_int; - pub fn Cudd_Support(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_SupportIndex(dd: *mut DdManager, f: *mut DdNode) -> *mut c_int; - pub fn Cudd_SupportSize(dd: *mut DdManager, f: *mut DdNode) -> c_int; - pub fn Cudd_VectorSupportIndices( - dd: *mut DdManager, - F: *mut *mut DdNode, - n: c_int, - indices: *mut *mut c_int, - ) -> c_int; - pub fn Cudd_VectorSupport(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) -> *mut DdNode; - pub fn Cudd_VectorSupportIndex(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) - -> *mut c_int; - pub fn Cudd_VectorSupportSize(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) -> c_int; - pub fn Cudd_ClassifySupport( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - common: *mut *mut DdNode, - onlyF: *mut *mut DdNode, - onlyG: *mut *mut DdNode, - ) -> c_int; - pub fn Cudd_CountLeaves(node: *mut DdNode) -> c_int; - pub fn Cudd_bddPickOneCube( - ddm: *mut DdManager, - node: *mut DdNode, - string: *mut c_char, - ) -> c_int; - pub fn Cudd_bddPickOneMinterm( - dd: *mut DdManager, - f: *mut DdNode, - vars: *mut *mut DdNode, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_bddPickArbitraryMinterms( - dd: *mut DdManager, - f: *mut DdNode, - vars: *mut *mut DdNode, - n: c_int, - k: c_int, - ) -> *mut *mut DdNode; - pub fn Cudd_SubsetWithMaskVars( - dd: *mut DdManager, - f: *mut DdNode, - vars: *mut *mut DdNode, - nvars: c_int, - maskVars: *mut *mut DdNode, - mvars: c_int, - ) -> *mut DdNode; - pub fn Cudd_FirstCube( - dd: *mut DdManager, - f: *mut DdNode, - cube: *mut *mut c_int, - value: *mut CUDD_VALUE_TYPE, - ) -> *mut DdGen; - pub fn Cudd_NextCube( - gen: *mut DdGen, - cube: *mut *mut c_int, - value: *mut CUDD_VALUE_TYPE, - ) -> c_int; - pub fn Cudd_FirstPrime( - dd: *mut DdManager, - l: *mut DdNode, - u: *mut DdNode, - cube: *mut *mut c_int, - ) -> *mut DdGen; - pub fn Cudd_NextPrime(gen: *mut DdGen, cube: *mut *mut c_int) -> c_int; - pub fn Cudd_bddComputeCube( - dd: *mut DdManager, - vars: *mut *mut DdNode, - phase: *mut c_int, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_addComputeCube( - dd: *mut DdManager, - vars: *mut *mut DdNode, - phase: *mut c_int, - n: c_int, - ) -> *mut DdNode; - pub fn Cudd_CubeArrayToBdd(dd: *mut DdManager, array: *mut c_int) -> *mut DdNode; - pub fn Cudd_BddToCubeArray(dd: *mut DdManager, cube: *mut DdNode, array: *mut c_int) -> c_int; - pub fn Cudd_FirstNode(dd: *mut DdManager, f: *mut DdNode, node: *mut *mut DdNode) - -> *mut DdGen; - pub fn Cudd_NextNode(gen: *mut DdGen, node: *mut *mut DdNode) -> c_int; - pub fn Cudd_GenFree(gen: *mut DdGen) -> c_int; - pub fn Cudd_IsGenEmpty(gen: *mut DdGen) -> c_int; - pub fn Cudd_IndicesToCube(dd: *mut DdManager, array: *mut c_int, n: c_int) -> *mut DdNode; - pub fn Cudd_PrintVersion(fp: *mut FILE) -> c_void; - pub fn Cudd_AverageDistance(dd: *mut DdManager) -> c_double; - pub fn Cudd_Random(dd: *mut DdManager) -> i32; - pub fn Cudd_Srandom(dd: *mut DdManager, seed: i32) -> c_void; - pub fn Cudd_Density(dd: *mut DdManager, f: *mut DdNode, nvars: c_int) -> c_double; - pub fn Cudd_OutOfMem(size: size_t) -> c_void; - pub fn Cudd_OutOfMemSilent(size: size_t) -> c_void; - pub fn Cudd_zddCount(zdd: *mut DdManager, P: *mut DdNode) -> c_int; - pub fn Cudd_zddCountDouble(zdd: *mut DdManager, P: *mut DdNode) -> c_double; - pub fn Cudd_zddProduct(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddUnateProduct(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddWeakDiv(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddDivide(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddWeakDivF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddDivideF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddComplement(dd: *mut DdManager, node: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddIsop( - dd: *mut DdManager, - L: *mut DdNode, - U: *mut DdNode, - zdd_I: *mut *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_bddIsop(dd: *mut DdManager, L: *mut DdNode, U: *mut DdNode) -> *mut DdNode; - pub fn Cudd_MakeBddFromZddCover(dd: *mut DdManager, node: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddDagSize(p_node: *mut DdNode) -> c_int; - pub fn Cudd_zddCountMinterm(zdd: *mut DdManager, node: *mut DdNode, path: c_int) -> c_double; - pub fn Cudd_zddPrintSubtable(table: *mut DdManager) -> c_void; - pub fn Cudd_zddPortFromBdd(dd: *mut DdManager, B: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddPortToBdd(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddReduceHeap( - table: *mut DdManager, - heuristic: Cudd_ReorderingType, - minsize: c_int, - ) -> c_int; - pub fn Cudd_zddShuffleHeap(table: *mut DdManager, permutation: *mut c_int) -> c_int; - pub fn Cudd_zddIte( - dd: *mut DdManager, - f: *mut DdNode, - g: *mut DdNode, - h: *mut DdNode, - ) -> *mut DdNode; - pub fn Cudd_zddUnion(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddIntersect(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddDiff(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddDiffConst(zdd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddSubset1(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode; - pub fn Cudd_zddSubset0(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode; - pub fn Cudd_zddChange(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode; - pub fn Cudd_zddSymmProfile(table: *mut DdManager, lower: c_int, upper: c_int) -> c_void; - pub fn Cudd_zddPrintMinterm(zdd: *mut DdManager, node: *mut DdNode) -> c_int; - pub fn Cudd_zddPrintCover(zdd: *mut DdManager, node: *mut DdNode) -> c_int; - pub fn Cudd_zddPrintDebug(zdd: *mut DdManager, f: *mut DdNode, n: c_int, pr: c_int) -> c_int; - pub fn Cudd_zddFirstPath( - zdd: *mut DdManager, - f: *mut DdNode, - path: *mut *mut c_int, - ) -> *mut DdGen; - pub fn Cudd_zddNextPath(gen: *mut DdGen, path: *mut *mut c_int) -> c_int; - pub fn Cudd_zddCoverPathToString( - zdd: *mut DdManager, - path: *mut c_int, - str: *mut c_char, - ) -> *mut c_char; - pub fn Cudd_zddSupport(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode; - pub fn Cudd_zddDumpDot( - dd: *mut DdManager, - n: c_int, - f: *mut *mut DdNode, - inames: *const *const c_char, - onames: *const *const c_char, - fp: *mut FILE, - ) -> c_int; - pub fn Cudd_bddSetPiVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddSetPsVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddSetNsVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddIsPiVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddIsPsVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddIsNsVar(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddSetPairIndex(dd: *mut DdManager, index: c_int, pairIndex: c_int) -> c_int; - pub fn Cudd_bddReadPairIndex(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddSetVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddSetVarHardGroup(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddResetVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddIsVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddSetVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddIsVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_bddIsVarHardGroup(dd: *mut DdManager, index: c_int) -> c_int; - pub fn Cudd_ReadTree(dd: *mut DdManager) -> *mut MtrNode; - pub fn Cudd_SetTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; - pub fn Cudd_FreeTree(dd: *mut DdManager) -> c_void; - pub fn Cudd_ReadZddTree(dd: *mut DdManager) -> *mut MtrNode; - pub fn Cudd_SetZddTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void; - pub fn Cudd_FreeZddTree(dd: *mut DdManager) -> c_void; - pub fn Cudd_MakeTreeNode( - dd: *mut DdManager, - low: c_uint, - size: c_uint, - mtr_type: c_uint, - ) -> *mut MtrNode; - pub fn Cudd_MakeZddTreeNode( - dd: *mut DdManager, - low: c_uint, - size: c_uint, - mtr_type: c_uint, - ) -> *mut MtrNode; -} diff --git a/src/test.rs b/src/test.rs index 4e7b90b..d3aa6a9 100644 --- a/src/test.rs +++ b/src/test.rs @@ -1,8 +1,4 @@ -use Cudd_Quit; -use {Cudd_Init, CUDD_CACHE_SLOTS}; -use {Cudd_Ref, Cudd_bddAnd}; -use {Cudd_bddIthVar, CUDD_UNIQUE_SLOTS}; -use {Cudd_bddNand, Cudd_bddNor}; +use cudd::*; #[test] pub fn basic_functionality_test() { From 5c1e8cd04e095e05331b54c13d5c98b293f93a44 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 16:20:40 +0200 Subject: [PATCH 08/15] Add declarations from `mtr.h`. --- src/lib.rs | 3 +++ src/mtr.rs | 45 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 src/mtr.rs diff --git a/src/lib.rs b/src/lib.rs index 707302d..bd43721 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -37,6 +37,9 @@ mod test; /// Contains the declarations present in `cudd.h`. pub mod cudd; +/// Contains the declarations present in `mtr.h`. +pub mod mtr; + use std::marker::{PhantomData, PhantomPinned}; /// An opaque C struct used to represent the decision diagram node. diff --git a/src/mtr.rs b/src/mtr.rs new file mode 100644 index 0000000..d37e845 --- /dev/null +++ b/src/mtr.rs @@ -0,0 +1,45 @@ +use libc::{c_int, c_uint, c_void, FILE}; +use MtrNode; + +/// Default flag value in `Mtr_MakeGroup`. +pub const MTR_DEFAULT: c_uint = 0; +/// See `Mtr_MakeGroup`. +pub const MTR_TERMINAL: c_uint = 1; +/// See `Mtr_MakeGroup`. +pub const MTR_SOFT: c_uint = 2; +/// See `Mtr_MakeGroup`. +pub const MTR_FIXED: c_uint = 4; +/// See `Mtr_MakeGroup`. +pub const MTR_NEWNODE: c_uint = 8; + +extern "C" { + pub fn Mtr_AllocNode() -> *mut MtrNode; + pub fn Mtr_DeallocNode(node: *mut MtrNode) -> c_void; + pub fn Mtr_InitTree() -> *mut MtrNode; + pub fn Mtr_FreeTree(node: *mut MtrNode) -> c_void; + pub fn Mtr_CopyTree(node: *const MtrNode, expansion: c_int) -> *mut MtrNode; + pub fn Mtr_MakeFirstChild(parent: *mut MtrNode, child: *mut MtrNode) -> c_void; + pub fn Mtr_MakeLastChild(parent: *mut MtrNode, child: *mut MtrNode) -> c_void; + pub fn Mtr_CreateFirstChild(parent: *mut MtrNode) -> *mut MtrNode; + pub fn Mtr_CreateLastChild(parent: *mut MtrNode) -> *mut MtrNode; + pub fn Mtr_MakeNextSibling(first: *mut MtrNode, second: *mut MtrNode) -> c_void; + pub fn Mtr_PrintTree(node: *const MtrNode) -> c_void; + pub fn Mtr_InitGroupTree(lower: c_int, size: c_int) -> *mut MtrNode; + pub fn Mtr_MakeGroup( + root: *mut MtrNode, + low: c_uint, + high: c_uint, + flags: c_uint, + ) -> *mut MtrNode; + pub fn Mtr_DissolveGroup(group: *mut MtrNode) -> *mut MtrNode; + pub fn Mtr_FindGroup(root: *mut MtrNode, low: c_uint, high: c_uint) -> *mut MtrNode; + pub fn Mtr_SwapGroups(first: *mut MtrNode, second: *mut MtrNode) -> c_int; + pub fn Mtr_ReorderGroups(treenode: *mut MtrNode, permutation: *mut c_int) -> c_void; + pub fn Mtr_PrintGroups(root: *const MtrNode, silent: c_int) -> c_void; + pub fn Mtr_PrintGroupedOrder( + root: *const MtrNode, + invperm: *const c_int, + fp: *mut FILE, + ) -> c_int; + pub fn Mtr_ReadGroups(fp: *mut FILE, nleaves: c_int) -> *mut MtrNode; +} From cd61b303126cac760ea3f57cf76625f4fbb12aef Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 16:28:43 +0200 Subject: [PATCH 09/15] Add declarations from `epd.h`. --- src/epd.rs | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 7 +++++-- 2 files changed, 64 insertions(+), 2 deletions(-) create mode 100644 src/epd.rs diff --git a/src/epd.rs b/src/epd.rs new file mode 100644 index 0000000..b72bc47 --- /dev/null +++ b/src/epd.rs @@ -0,0 +1,59 @@ +use libc::{c_int, c_void}; +use std::os::raw::{c_char, c_double}; +use EpDouble; + +extern "C" { + pub fn EpdAlloc() -> *mut EpDouble; + pub fn EpdCmp(key1: *const c_void, key2: *const c_void) -> c_int; + pub fn EpdFree(epd: *mut EpDouble) -> c_void; + pub fn EpdGetString(epd: *const EpDouble, str: *mut c_char) -> c_void; + pub fn EpdConvert(value: c_double, epd: *mut EpDouble) -> c_void; + pub fn EpdMultiply(epd1: *mut EpDouble, value: c_double) -> c_void; + pub fn EpdMultiply2(epd1: *mut EpDouble, epd2: *const EpDouble) -> c_void; + pub fn EpdMultiply2Decimal(epd1: *mut EpDouble, epd2: *const EpDouble) -> c_void; + pub fn EpdMultiply3( + epd1: *const EpDouble, + epd2: *const EpDouble, + epd3: *mut EpDouble, + ) -> c_void; + pub fn EpdMultiply3Decimal( + epd1: *const EpDouble, + epd2: *const EpDouble, + epd3: *mut EpDouble, + ) -> c_void; + pub fn EpdDivide(epd1: *mut EpDouble, value: c_double) -> c_void; + pub fn EpdDivide2(epd1: *mut EpDouble, epd2: *const EpDouble) -> c_void; + pub fn EpdDivide3(epd1: *const EpDouble, epd2: *const EpDouble, epd3: *mut EpDouble) -> c_void; + pub fn EpdAdd(epd1: *mut EpDouble, value: c_double) -> c_void; + pub fn EpdAdd2(epd1: *mut EpDouble, epd2: *const EpDouble) -> c_void; + pub fn EpdAdd3(epd1: *const EpDouble, epd2: *const EpDouble, epd3: *mut EpDouble) -> c_void; + pub fn EpdSubtract(epd1: *mut EpDouble, value: c_double) -> c_void; + pub fn EpdSubtract2(epd1: *mut EpDouble, epd2: *const EpDouble) -> c_void; + pub fn EpdSubtract3( + epd1: *const EpDouble, + epd2: *const EpDouble, + epd3: *mut EpDouble, + ) -> c_void; + pub fn EpdPow2(n: c_int, epd: *mut EpDouble) -> c_void; + pub fn EpdPow2Decimal(n: c_int, epd: *mut EpDouble) -> c_void; + pub fn EpdNormalize(epd: *mut EpDouble) -> c_void; + pub fn EpdNormalizeDecimal(epd: *mut EpDouble) -> c_void; + pub fn EpdGetValueAndDecimalExponent( + epd: *const EpDouble, + value: *mut c_double, + exponent: *mut c_int, + ) -> c_void; + pub fn EpdGetExponent(value: c_double) -> c_int; + pub fn EpdGetExponentDecimal(value: c_double) -> c_int; + pub fn EpdMakeInf(epd: *mut EpDouble, sign: c_int) -> c_void; + pub fn EpdMakeZero(epd: *mut EpDouble, sign: c_int) -> c_void; + pub fn EpdMakeNan(epd: *mut EpDouble) -> c_void; + pub fn EpdCopy(from: *const EpDouble, to: *mut EpDouble) -> c_void; + pub fn EpdIsInf(epd: *const EpDouble) -> c_int; + pub fn EpdIsZero(epd: *const EpDouble) -> c_int; + pub fn EpdIsNan(epd: *const EpDouble) -> c_int; + pub fn EpdIsNanOrInf(epd: *const EpDouble) -> c_int; + pub fn IsInfDouble(value: c_double) -> c_int; + pub fn IsNanDouble(value: c_double) -> c_int; + pub fn IsNanOrInfDouble(value: c_double) -> c_int; +} diff --git a/src/lib.rs b/src/lib.rs index bd43721..f5630ea 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -34,12 +34,15 @@ extern crate libc; #[cfg(test)] mod test; -/// Contains the declarations present in `cudd.h`. +/// Contains the declarations present in `cudd.h` (main CUDD API). pub mod cudd; -/// Contains the declarations present in `mtr.h`. +/// Contains the declarations present in `mtr.h` (multiway-branching trees). pub mod mtr; +/// Contains the declarations present in `epd.h` (extended double precision numbers). +pub mod epd; + use std::marker::{PhantomData, PhantomPinned}; /// An opaque C struct used to represent the decision diagram node. From 744b034a6661c4345cda2fa5d719527477324ded Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 16:56:18 +0200 Subject: [PATCH 10/15] Add DDDMP serialization bindings. --- README.md | 12 +- build.rs | 8 +- src/dddmp.rs | 312 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 17 ++- 4 files changed, 339 insertions(+), 10 deletions(-) create mode 100644 src/dddmp.rs diff --git a/README.md b/README.md index e8ff0cf..a5309d0 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,11 @@ # Rust Bindings for the CUDD library -This crate provides unsafe Rust bindings for the University of Colorado decision diagram package (CUDD). It uses version `3.0.0` of CUDD available from the unofficial [Github mirror](https://github.com/ivmai/cudd) and compiles on Linux and MacOS (you should be also able to build CUDD on Windows using cygwin, but the project is not set-up to do it automatically). +This crate provides unsafe Rust bindings for the University of Colorado decision diagram +package (CUDD), including the DDDMP serialisation library. It uses version `3.0.0` of CUDD +available from the unofficial [Github mirror](https://github.com/ivmai/cudd) and compiles on +Linux and MacOS (you should be also able to build CUDD on Windows using cygwin, but the project +is not set-up to do it automatically). In the root module, you will find declarations of the C structs and types used throughout CUDD. The main API of the CUDD package is then exported in `::cudd`. However, @@ -15,7 +19,9 @@ In some cases, there are macro and constant definitions which cannot be directly to Rust. These have been re-implemented and should have their own documentation. For the functions which are re-exported without change, please refer to the original [CUDD doxygen](https://add-lib.scce.info/assets/doxygen-cudd-documentation/) and -[manual](https://add-lib.scce.info/assets/documents/cudd-manual.pdf). +[manual](https://add-lib.scce.info/assets/documents/cudd-manual.pdf). The documentation +of the DDDMP library is available +[here](https://www.cs.rice.edu/~lm30/RSynth/CUDD/dddmp/doc/dddmpExt.html). **Completeness:** The main CUDD API should be fully reproduced here (except for one small issue with `f128` numbers). The remaining modules may still be incomplete: if you need @@ -25,4 +31,4 @@ a function that isn't exported yet, let us know in the issues. reproduced using a semi-automated method with a manual validation step (bunch of regexes that a human makes sure didn't break anything ;)). As such, it is possible that there are some minor problems that need to be sorted out. Please file an issue if you see any -unexpected behaviour or segfaults. \ No newline at end of file +unexpected behaviour or segfaults. diff --git a/build.rs b/build.rs index bb256a5..d8fe460 100644 --- a/build.rs +++ b/build.rs @@ -1,4 +1,6 @@ -// build.rs +extern crate autotools; + +use autotools::Config; use std::env; use std::io::ErrorKind; use std::path::{Path, PathBuf}; @@ -114,7 +116,9 @@ fn main() -> Result<(), String> { ]); run_command(&mut tar_command).map_err(|e| format!("Error decompressing CUDD: {:?}", e))?; - let build_output = autotools::build(cudd_path); + // Enable dddmp when building. + let build_output = Config::new(cudd_path).enable("dddmp", None).build(); + println!( "cargo:rustc-link-search=native={}", build_output.join("lib").display() diff --git a/src/dddmp.rs b/src/dddmp.rs new file mode 100644 index 0000000..971ae58 --- /dev/null +++ b/src/dddmp.rs @@ -0,0 +1,312 @@ +use libc::{c_char, c_int, FILE}; +use {DdManager, DdNode}; + +/// Version of DDDMP format. +pub const DDDMP_VERSION: &str = "DDDMP-2.0"; + +/// Returned by functions when failed. +pub const DDDMP_FAILURE: c_int = 0; + +/// Returned by functions when succeeded. +pub const DDDMP_SUCCESS: c_int = 1; + +/// Text formatting mode. +pub const DDDMP_MODE_TEXT: c_int = 'A' as c_int; + +/// Binary formatting mode. +pub const DDDMP_MODE_BINARY: c_int = 'B' as c_int; + +/// Default formatting mode. +pub const DDDMP_MODE_DEFAULT: c_int = 'D' as c_int; + +#[repr(C)] +pub enum Dddmp_DecompCnfStoreType { + DDDMP_CNF_MODE_NODE, + DDDMP_CNF_MODE_MAXTERM, + DDDMP_CNF_MODE_BEST, +} + +#[repr(C)] +pub enum Dddmp_DecompCnfLoadType { + DDDMP_CNF_MODE_NO_CONJ, + DDDMP_CNF_MODE_NO_QUANT, + DDDMP_CNF_MODE_CONJ_QUANT, +} + +#[repr(C)] +pub enum Dddmp_DecompType { + DDDMP_BDD, + DDDMP_ADD, + DDDMP_CNF, + DDDMP_NONE, +} + +#[repr(C)] +pub enum Dddmp_VarInfoType { + DDDMP_VARIDS, + DDDMP_VARPERMIDS, + DDDMP_VARAUXIDS, + DDDMP_VARNAMES, + DDDMP_VARDEFAULT, +} + +#[repr(C)] +pub enum Dddmp_VarMatchType { + DDDMP_VAR_MATCHIDS, + DDDMP_VAR_MATCHPERMIDS, + DDDMP_VAR_MATCHAUXIDS, + DDDMP_VAR_MATCHNAMES, + DDDMP_VAR_COMPOSEIDS, +} + +#[repr(C)] +pub enum Dddmp_RootMatchType { + DDDMP_ROOT_MATCHNAMES, + DDDMP_ROOT_MATCHLIST, +} + +extern "C" { + pub fn Dddmp_Text2Bin(filein: *mut c_char, fileout: *mut c_char) -> c_int; + pub fn Dddmp_Bin2Text(filein: *mut c_char, fileout: *mut c_char) -> c_int; + pub fn Dddmp_cuddBddDisplayBinary(fileIn: *mut c_char, fileOut: *mut c_char) -> c_int; + pub fn Dddmp_cuddBddLoad( + ddMgr: *mut DdManager, + varMatchMode: Dddmp_VarMatchType, + varmatchnames: *mut *mut c_char, + varmatchauxids: *mut c_int, + varcomposeids: *mut c_int, + mode: c_int, + file: *mut c_char, + fp: *mut FILE, + ) -> *mut DdNode; + pub fn Dddmp_cuddBddArrayLoad( + ddMgr: *mut DdManager, + rootMatchMode: Dddmp_RootMatchType, + rootmatchnames: *mut *mut c_char, + varMatchMode: Dddmp_VarMatchType, + varmatchnames: *mut *mut c_char, + varmatchauxids: *mut c_int, + varcomposeids: *mut c_int, + mode: c_int, + file: *mut c_char, + fp: *mut FILE, + pproots: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Dddmp_cuddAddLoad( + ddMgr: *mut DdManager, + varMatchMode: Dddmp_VarMatchType, + varmatchnames: *mut *mut c_char, + varmatchauxids: *mut c_int, + varcomposeids: *mut c_int, + mode: c_int, + file: *mut c_char, + fp: *mut FILE, + ) -> *mut DdNode; + pub fn Dddmp_cuddAddArrayLoad( + ddMgr: *mut DdManager, + rootMatchMode: Dddmp_RootMatchType, + rootmatchnames: *mut *mut c_char, + varMatchMode: Dddmp_VarMatchType, + varmatchnames: *mut *mut c_char, + varmatchauxids: *mut c_int, + varcomposeids: *mut c_int, + mode: c_int, + file: *mut c_char, + fp: *mut FILE, + pproots: *mut *mut *mut DdNode, + ) -> c_int; + pub fn Dddmp_cuddHeaderLoad( + ddType: *mut Dddmp_DecompType, + nVars: *mut c_int, + nsuppvars: *mut c_int, + suppVarNames: *mut *mut *mut c_char, + orderedVarNames: *mut *mut *mut c_char, + varIds: *mut *mut c_int, + composeIds: *mut *mut c_int, + auxIds: *mut *mut c_int, + nRoots: *mut c_int, + file: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddLoadCnf( + ddMgr: *mut DdManager, + varmatchmode: Dddmp_VarMatchType, + varmatchnames: *mut *mut c_char, + varmatchauxids: *mut c_int, + varcomposeids: *mut c_int, + mode: c_int, + file: *mut c_char, + fp: *mut FILE, + rootsPtrPtr: *mut *mut *mut DdNode, + nRoots: *mut c_int, + ) -> c_int; + pub fn Dddmp_cuddBddArrayLoadCnf( + ddMgr: *mut DdManager, + rootmatchmode: Dddmp_RootMatchType, + rootmatchnames: *mut *mut c_char, + varmatchmode: Dddmp_VarMatchType, + varmatchnames: *mut *mut c_char, + varmatchauxids: *mut c_int, + varcomposeids: *mut c_int, + mode: c_int, + file: *mut c_char, + fp: *mut FILE, + rootsPtrPtr: *mut *mut *mut DdNode, + nRoots: *mut c_int, + ) -> c_int; + pub fn Dddmp_cuddHeaderLoadCnf( + nVars: *mut c_int, + nsuppvars: *mut c_int, + suppVarNames: *mut *mut *mut c_char, + orderedVarNames: *mut *mut *mut c_char, + varIds: *mut *mut c_int, + composeIds: *mut *mut c_int, + auxIds: *mut *mut c_int, + nRoots: *mut c_int, + file: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddAddStore( + ddMgr: *mut DdManager, + ddname: *mut c_char, + f: *mut DdNode, + varnames: *mut *mut c_char, + auxids: *mut c_int, + mode: c_int, + varinfo: Dddmp_VarInfoType, + fname: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddAddArrayStore( + ddMgr: *mut DdManager, + ddname: *mut c_char, + nRoots: c_int, + f: *mut *mut DdNode, + rootnames: *mut *mut c_char, + varnames: *mut *mut c_char, + auxids: *mut c_int, + mode: c_int, + varinfo: Dddmp_VarInfoType, + fname: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddStore( + ddMgr: *mut DdManager, + ddname: *mut c_char, + f: *mut DdNode, + varnames: *mut *mut c_char, + auxids: *mut c_int, + mode: c_int, + varinfo: Dddmp_VarInfoType, + fname: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddArrayStore( + ddMgr: *mut DdManager, + ddname: *mut c_char, + nRoots: c_int, + f: *mut *mut DdNode, + rootnames: *mut *mut c_char, + varnames: *mut *mut c_char, + auxids: *mut c_int, + mode: c_int, + varinfo: Dddmp_VarInfoType, + fname: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddStoreCnf( + ddMgr: *mut DdManager, + f: *mut DdNode, + mode: Dddmp_DecompCnfStoreType, + noHeader: c_int, + varNames: *mut *mut c_char, + bddIds: *mut c_int, + bddAuxIds: *mut c_int, + cnfIds: *mut c_int, + idInitial: c_int, + edgeInTh: c_int, + pathLengthTh: c_int, + fname: *mut c_char, + fp: *mut FILE, + clauseNPtr: *mut c_int, + varNewNPtr: *mut c_int, + ) -> c_int; + pub fn Dddmp_cuddBddArrayStoreCnf( + ddMgr: *mut DdManager, + f: *mut *mut DdNode, + rootN: c_int, + mode: Dddmp_DecompCnfStoreType, + noHeader: c_int, + varNames: *mut *mut c_char, + bddIds: *mut c_int, + bddAuxIds: *mut c_int, + cnfIds: *mut c_int, + idInitial: c_int, + edgeInTh: c_int, + pathLengthTh: c_int, + fname: *mut c_char, + fp: *mut FILE, + clauseNPtr: *mut c_int, + varNewNPtr: *mut c_int, + ) -> c_int; + pub fn Dddmp_cuddBddStorePrefix( + ddMgr: *mut DdManager, + nRoots: c_int, + f: *mut DdNode, + inputNames: *mut *mut c_char, + outputNames: *mut *mut c_char, + modelName: *mut c_char, + fileName: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddArrayStorePrefix( + ddMgr: *mut DdManager, + nroots: c_int, + f: *mut *mut DdNode, + inputNames: *mut *mut c_char, + outputNames: *mut *mut c_char, + modelName: *mut c_char, + fname: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddStoreBlif( + ddMgr: *mut DdManager, + nRoots: c_int, + f: *mut DdNode, + inputNames: *mut *mut c_char, + outputNames: *mut *mut c_char, + modelName: *mut c_char, + fileName: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddArrayStoreBlif( + ddMgr: *mut DdManager, + nroots: c_int, + f: *mut *mut DdNode, + inputNames: *mut *mut c_char, + outputNames: *mut *mut c_char, + modelName: *mut c_char, + fname: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddStoreSmv( + ddMgr: *mut DdManager, + nRoots: c_int, + f: *mut DdNode, + inputNames: *mut *mut c_char, + outputNames: *mut *mut c_char, + modelName: *mut c_char, + fileName: *mut c_char, + fp: *mut FILE, + ) -> c_int; + pub fn Dddmp_cuddBddArrayStoreSmv( + ddMgr: *mut DdManager, + nroots: c_int, + f: *mut *mut DdNode, + inputNames: *mut *mut c_char, + outputNames: *mut *mut c_char, + modelName: *mut c_char, + fname: *mut c_char, + fp: *mut FILE, + ) -> c_int; +} diff --git a/src/lib.rs b/src/lib.rs index f5630ea..f9b37b2 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,8 +1,8 @@ //! This crate provides unsafe Rust bindings for the University of Colorado decision diagram -//! package (CUDD). It uses version `3.0.0` of CUDD available from the unofficial -//! [Github mirror](https://github.com/ivmai/cudd) and compiles on Linux and MacOS -//! (you should be also able to build CUDD on Windows using cygwin, but the project is not set-up -//! to do it automatically). +//! package (CUDD), including the DDDMP serialisation library. It uses version `3.0.0` of CUDD +//! available from the unofficial [Github mirror](https://github.com/ivmai/cudd) and compiles on +//! Linux and MacOS (you should be also able to build CUDD on Windows using cygwin, but the project +//! is not set-up to do it automatically). //! //! In the root module, you will find declarations of the C structs and types used //! throughout CUDD. The main API of the CUDD package is then exported in `::cudd`. However, @@ -13,7 +13,9 @@ //! to Rust. These have been re-implemented and should have their own documentation. //! For the functions which are re-exported without change, please refer to the original //! [CUDD doxygen](https://add-lib.scce.info/assets/doxygen-cudd-documentation/) and -//! [manual](https://add-lib.scce.info/assets/documents/cudd-manual.pdf). +//! [manual](https://add-lib.scce.info/assets/documents/cudd-manual.pdf). The documentation +//! of the DDDMP library is available +//! [here](https://www.cs.rice.edu/~lm30/RSynth/CUDD/dddmp/doc/dddmpExt.html). //! //! **Completeness:** The main CUDD API should be fully reproduced here (except for one small //! issue with `f128` numbers). The remaining modules may still be incomplete: if you need @@ -43,6 +45,11 @@ pub mod mtr; /// Contains the declarations present in `epd.h` (extended double precision numbers). pub mod epd; +/// Declarations from `dddmp.h` (serialisation of decision diagrams). +/// +/// Currently, the error checking macros are not implemented. +pub mod dddmp; + use std::marker::{PhantomData, PhantomPinned}; /// An opaque C struct used to represent the decision diagram node. From d0864fad9a8024d002af847bcda0c21d0388479d Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 17:40:49 +0200 Subject: [PATCH 11/15] Remove unused function types. --- src/cudd.rs | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/src/cudd.rs b/src/cudd.rs index 3b3d0e4..afa85f9 100644 --- a/src/cudd.rs +++ b/src/cudd.rs @@ -28,19 +28,9 @@ pub type DD_APPLY_OPERATOR = /// Type of the monadic apply operator function. pub type DD_MONADIC_APPLY_OPERATOR = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; -/// Type of the two-operand cache tag function. -pub type DD_CACHE_TAG_FUNCTION_2 = - extern "C" fn(*mut DdManager, *mut DdNode, *mut DdNode) -> *mut DdNode; - -/// Type of the one-operand cache tag function. -pub type DD_CACHE_TAG_FUNCTION_1 = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode; - /// Type of the out-of-memory function. pub type DD_OUT_OF_MEMORY_FUNCTION = extern "C" fn(size_t) -> c_void; -/// Type of the Q-sort comparison function. -pub type DD_Q_SORT_FUNCTION = extern "C" fn(*const c_void, *const c_void) -> c_int; - /// Type of the termination handler function. pub type DD_TERMINATION_HANDLER = extern "C" fn(*const c_void) -> c_int; @@ -373,18 +363,18 @@ extern "C" { pub fn Cudd_UnregisterTerminationCallback(unique: *mut DdManager) -> c_void; pub fn Cudd_RegisterOutOfMemoryCallback( unique: *mut DdManager, - callback: DD_OUT_OF_MEMORY_FUNCTION, - ) -> DD_OUT_OF_MEMORY_FUNCTION; + callback: Option, + ) -> Option; pub fn Cudd_UnregisterOutOfMemoryCallback(unique: *mut DdManager) -> c_void; pub fn Cudd_RegisterTimeoutHandler( unique: *mut DdManager, - handler: DD_TIME_OUT_HANDLER, + handler: Option, arg: *mut c_void, ) -> c_void; pub fn Cudd_ReadTimeoutHandler( unique: *mut DdManager, argp: *mut *mut c_void, - ) -> DD_TIME_OUT_HANDLER; + ) -> Option; pub fn Cudd_AutodynEnable(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void; pub fn Cudd_AutodynDisable(unique: *mut DdManager) -> c_void; pub fn Cudd_ReorderingStatus(unique: *mut DdManager, method: *mut Cudd_ReorderingType) From 258350730e43a05de285ede94b05ba034857dded Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 17:41:08 +0200 Subject: [PATCH 12/15] Improve test to include new "macros" and function callbacks. --- src/test.rs | 43 ++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 40 insertions(+), 3 deletions(-) diff --git a/src/test.rs b/src/test.rs index d3aa6a9..b0f5228 100644 --- a/src/test.rs +++ b/src/test.rs @@ -1,15 +1,29 @@ use cudd::*; +use libc::{c_int, c_void}; +use std::ptr::null_mut; + +static mut CALLED: bool = false; + +extern "C" fn termination_handler(_data: *const c_void) -> c_int { + unsafe { + CALLED = true; + } + 0 +} #[test] pub fn basic_functionality_test() { unsafe { let cudd = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); + Cudd_RegisterTerminationCallback(cudd, termination_handler, null_mut()); + // Check that the basic identity (a & b) <=> !(!a | !b) holds. let a = Cudd_bddIthVar(cudd, 1); let b = Cudd_bddIthVar(cudd, 2); - // There is a Cudd_Not macro, but that is not available through bindings. - let not_a = Cudd_bddNand(cudd, a, a); - let not_b = Cudd_bddNand(cudd, b, b); + + // Check the complement "macros". + let not_a = Cudd_Complement(a); + let not_b = Cudd_Complement(b); Cudd_Ref(not_a); Cudd_Ref(not_b); @@ -20,6 +34,29 @@ pub fn basic_functionality_test() { Cudd_Ref(not_a_or_b); assert_eq!(a_and_b, not_a_or_b); + + // 20 variable pairs should be enough to trigger termination handler at some point. + let mut big_bdd = Cudd_ReadOne(cudd); + for i in 1..20 { + let x = Cudd_bddIthVar(cudd, i); + let y = Cudd_bddIthVar(cudd, 2 * i); + let x_iff_y = Cudd_bddXor(cudd, x, y); + Cudd_Ref(x_iff_y); + big_bdd = Cudd_bddAnd(cudd, big_bdd, x_iff_y); + Cudd_Ref(big_bdd); + + let reported = Cudd_DagSize(big_bdd); + let mut counted = 0; + Cudd_ForeachNode(cudd, big_bdd, |_| { + counted += 1; + }); + assert_eq!(reported, counted); + assert!(reported > 0) + } + + assert!(CALLED); + assert_eq!(4091, Cudd_DagSize(big_bdd)); + Cudd_Quit(cudd); } } From 38ba11ded56f66dd038bbdb2148a0fb92f7c3588 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 18:36:18 +0200 Subject: [PATCH 13/15] Add a default feature flag for cudd build, so that documentation can be built even if offline. --- Cargo.toml | 12 +++++++++++- build.rs | 6 ++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index c2a7559..e418b4f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -11,4 +11,14 @@ license = "CC0-1.0" libc = "0.2" [build-dependencies] -autotools = "0.2.3" \ No newline at end of file +autotools = "0.2.3" + +[features] +default = ["build_cudd"] +# When disabled, the build script will not attempt to build CUDD and will just silently continue. +# This is necessary for building documentation on docs.rs without access to the internet. For other commands +# (aside from `cargo doc`), this will fail to produce a binary during linking. +build_cudd = [] + +[package.metadata.docs.rs] +no-default-features = true \ No newline at end of file diff --git a/build.rs b/build.rs index d8fe460..3b8b577 100644 --- a/build.rs +++ b/build.rs @@ -82,6 +82,12 @@ fn fetch_package(out_dir: &str, url: &str, md5: &str) -> Result<(PathBuf, MD5Sta } fn main() -> Result<(), String> { + let build_cudd = env::var_os("CARGO_FEATURE_BUILD_CUDD").is_some(); + if !build_cudd { + // If silent build is active, don't do anything. + return Ok(()); + } + let out_dir = env::var("OUT_DIR") .map_err(|_| "Environmental variable `OUT_DIR` not defined.".to_string())?; From b1384500f6f60f8b60be5cae9d72e42a9261e91d Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 19:02:10 +0200 Subject: [PATCH 14/15] Add a note about build dependencies. --- README.md | 2 ++ src/lib.rs | 3 +++ 2 files changed, 5 insertions(+) diff --git a/README.md b/README.md index a5309d0..b3fa916 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,8 @@ available from the unofficial [Github mirror](https://github.com/ivmai/cudd) and Linux and MacOS (you should be also able to build CUDD on Windows using cygwin, but the project is not set-up to do it automatically). +> On Linux and macOS, you should ideally have `autoconf`, `automake` and `libtool` installed to build CUDD. And of course, some C/C++ compiler (`clang`, `gcc`, etc.). + In the root module, you will find declarations of the C structs and types used throughout CUDD. The main API of the CUDD package is then exported in `::cudd`. However, CUDD also includes other "public" functionality (multiway-branching trees, extended diff --git a/src/lib.rs b/src/lib.rs index f9b37b2..d3b141d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,6 +4,9 @@ //! Linux and MacOS (you should be also able to build CUDD on Windows using cygwin, but the project //! is not set-up to do it automatically). //! +//! > On Linux and macOS, you should ideally have `autoconf`, `automake` and `libtool` installed +//! to build CUDD. And of course, some C/C++ compiler (`clang`, `gcc`, etc.). +//! //! In the root module, you will find declarations of the C structs and types used //! throughout CUDD. The main API of the CUDD package is then exported in `::cudd`. However, //! CUDD also includes other "public" functionality (multiway-branching trees, extended From ec6052188a56526bd8605abcc0f69bfe1d9e5fb5 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Sat, 4 Sep 2021 19:34:11 +0200 Subject: [PATCH 15/15] Fix typo in error message. --- build.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.rs b/build.rs index 3b8b577..de4664d 100644 --- a/build.rs +++ b/build.rs @@ -108,7 +108,7 @@ fn main() -> Result<(), String> { if !cudd_path.exists() { // Create the destination directory. std::fs::create_dir_all(cudd_path.clone()) - .map_err(|e| format!("Cannot create CUDD director: {:?}", e))?; + .map_err(|e| format!("Cannot create CUDD directory: {:?}", e))?; } // un-tar package, ignoring the name of the top level folder, dumping into cudd_path instead.