From 1642c5f66c302d07a74c583597191005ce032d90 Mon Sep 17 00:00:00 2001 From: david Date: Tue, 30 Apr 2013 10:50:40 +0200 Subject: [PATCH] Added missing functions to CUDDs cpp interface --- CMakeLists.txt | 10 ++-- resources/3rdparty/cudd-2.5.0/cudd/cudd.h | 6 ++ resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc | 60 ++++++++++++++++++++ resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh | 6 ++ 4 files changed, 77 insertions(+), 5 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index bed5cc152..ba522f0e6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -45,9 +45,9 @@ set(GMMXX_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-4.2/include) message(STATUS "GMMXX_INCLUDE_DIR is ${GMMXX_INCLUDE_DIR}") # Set all CUDD references to the version in the repository -set(CUDD_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/include) +set(CUDD_INCLUDE_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/include ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd) set(CUDD_LIBRARY_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/util ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/st ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj) -message(STATUS "CUDD_INCLUDE_DIR is ${CUDD_INCLUDE_DIR}") +message(STATUS "CUDD_INCLUDE_DIRS is ${CUDD_INCLUDE_DIRS}") message(STATUS "CUDD_LIBRARY_DIRS is ${CUDD_LIBRARY_DIRS}") # Now define all available custom options @@ -165,9 +165,9 @@ if (ADDITIONAL_LINK_DIRS) link_directories(${ADDITIONAL_LINK_DIRS}) endif(ADDITIONAL_LINK_DIRS) -if (CUDD_INCLUDE_DIR) - include_directories(${CUDD_INCLUDE_DIR}) -endif(CUDD_INCLUDE_DIR) +if (CUDD_INCLUDE_DIRS) + include_directories(${CUDD_INCLUDE_DIRS}) +endif(CUDD_INCLUDE_DIRS) if (CUDD_LIBRARY_DIRS) link_directories(${CUDD_LIBRARY_DIRS}) endif(CUDD_LIBRARY_DIRS) diff --git a/resources/3rdparty/cudd-2.5.0/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/cudd/cudd.h index 2493cbae0..d60d0c8f8 100644 --- a/resources/3rdparty/cudd-2.5.0/cudd/cudd.h +++ b/resources/3rdparty/cudd-2.5.0/cudd/cudd.h @@ -784,6 +784,12 @@ extern DdNode * Cudd_addNand (DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addNor (DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g); +extern DdNode * Cudd_addEquals (DdManager *dd, DdNode **f, DdNode **g); +extern DdNode * Cudd_addNotEquals (DdManager *dd, DdNode **f, DdNode **g); +extern DdNode * Cudd_addGreaterThan (DdManager *dd, DdNode **f, DdNode **g); +extern DdNode * Cudd_addGreaterThanEquals (DdManager *dd, DdNode **f, DdNode **g); +extern DdNode * Cudd_addLessThan (DdManager *dd, DdNode **f, DdNode **g); +extern DdNode * Cudd_addLessThanEquals (DdManager *dd, DdNode **f, DdNode **g); extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f); extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f); extern DdNode * Cudd_addEquals (DdManager *dd, DdNode **f, DdNode **g); diff --git a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc index 8722ca82f..b8a7f2179 100644 --- a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc @@ -2773,6 +2773,66 @@ Cudd::addResidue( } // Cudd::addResidue +ADD +ADD::Equals(const ADD& g) const +{ + DdManager *mgr = checkSameManager(g); + DdNode *result = Cudd_addApply(mgr, Cudd_addEquals, node, g.node); + checkReturnValue(result); + return ADD(p, result); + +} // ADD::Equals + +ADD +ADD::NotEquals(const ADD& g) const +{ + DdManager *mgr = checkSameManager(g); + DdNode *result = Cudd_addApply(mgr, Cudd_addNotEquals, node, g.node); + checkReturnValue(result); + return ADD(p, result); + +} // ADD::NotEquals + +ADD +ADD::LessThan(const ADD& g) const +{ + DdManager *mgr = checkSameManager(g); + DdNode *result = Cudd_addApply(mgr, Cudd_addLessThan, node, g.node); + checkReturnValue(result); + return ADD(p, result); + +} // ADD::LessThan + +ADD +ADD::LessThanOrEqual(const ADD& g) const +{ + DdManager *mgr = checkSameManager(g); + DdNode *result = Cudd_addApply(mgr, Cudd_addLessThanEquals, node, g.node); + checkReturnValue(result); + return ADD(p, result); + +} // ADD::LessThanOrEqual + +ADD +ADD::GreaterThan(const ADD& g) const +{ + DdManager *mgr = checkSameManager(g); + DdNode *result = Cudd_addApply(mgr, Cudd_addGreaterThan, node, g.node); + checkReturnValue(result); + return ADD(p, result); + +} // ADD::GreaterThan + +ADD +ADD::GreaterThanOrEqual(const ADD& g) const +{ + DdManager *mgr = checkSameManager(g); + DdNode *result = Cudd_addApply(mgr, Cudd_addGreaterThanEquals, node, g.node); + checkReturnValue(result); + return ADD(p, result); + +} // ADD::GreaterThanOrEqual + BDD BDD::AndAbstract( diff --git a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh index 83a0a924a..726476448 100644 --- a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh @@ -401,6 +401,12 @@ public: ADD Cmpl() const; ADD Negate() const; ADD RoundOff(int N) const; + ADD Equals(const ADD& g) const; + ADD NotEquals(const ADD& g) const; + ADD LessThan(const ADD& g) const; + ADD LessThanOrEqual(const ADD& g) const; + ADD GreaterThan(const ADD& g) const; + ADD GreaterThanOrEqual(const ADD& g) const; BDD BddThreshold(CUDD_VALUE_TYPE value) const; BDD BddStrictThreshold(CUDD_VALUE_TYPE value) const; BDD BddInterval(CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper) const;