diff --git a/.gitignore b/.gitignore
index 0e50990..1eadec4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@
 *.la
 *.lai
 *.swp
+build
\ No newline at end of file
diff --git a/CFLOBDD/assignment.h b/CFLOBDD/assignment.h
index b702b29..ab155c8 100644
--- a/CFLOBDD/assignment.h
+++ b/CFLOBDD/assignment.h
@@ -84,6 +84,8 @@ class Assignment
     bool *binding;                       // bool binding[size];
   public:
 	std::ostream& print(std::ostream & out = std::cout) const;
+  unsigned int get_size() const { return size; }
+  bool *get_data() const { return binding; }
 };
 
 std::ostream& operator<< (std::ostream & out, const Assignment &A);
diff --git a/CFLOBDD/cflobdd_c.cpp b/CFLOBDD/cflobdd_c.cpp
new file mode 100644
index 0000000..9ae87cf
--- /dev/null
+++ b/CFLOBDD/cflobdd_c.cpp
@@ -0,0 +1,296 @@
+#include "cflobdd_c.h"
+#include "cflobdd_t.h"
+#include "cflobdd_int.h"
+#include <utility>
+#include "vector_float_boost.h"
+// #include "vector_complex_float_boost.h"
+#include "quantum_algos.h"
+// #include "matrix1234_fourier.h"
+// #include "Solver/uwr/matrix/HowellMatrix.h"
+// #include "Solver/uwr/matrix/ModularSquareMatrix.h"
+// #include "memory_check.h"
+#include "matmult_map.h"
+// #include "matrix1234_node.h"
+#include "matrix1234_int.h"
+#include "wmatrix1234_fb_mul.h"
+#include "weighted_cross_product.h"
+#include "wvector_fb_mul.h"
+#include "weighted_quantum_algos.h"
+#include "wvector_complex_fb_mul.h"
+#include "wmatrix1234_fourier_mul.h"
+#include "wvector_fourier_mul.h"
+#include "weighted_bdd_node_t.h"
+#include "weighted_cross_product_bdd.h"
+#include "wvector_complex_fb_mul_bdd_node.h"
+static_assert(sizeof(CFL_OBDD::CFLOBDD) == sizeof(CFLOBDD));
+extern "C" {
+
+void CFLOBDD_module_init() {
+    
+	CFL_OBDD::CFLOBDDNodeHandle::InitNoDistinctionTable();
+	// CFLOBDDNodeHandle::InitAdditionInterleavedTable();
+	CFL_OBDD::CFLOBDDNodeHandle::InitReduceCache();
+	CFL_OBDD::InitPairProductCache();
+	CFL_OBDD::InitTripleProductCache();
+	CFL_OBDD::Matrix1234Int::Matrix1234Initializer();
+	CFL_OBDD::VectorFloatBoost::VectorInitializer();
+
+	// typedef double BIG_FLOAT;
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_FLOAT, std::multiplies<CFL_OBDD::BIG_FLOAT>>::InitNoDistinctionTable();
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_FLOAT, std::multiplies<CFL_OBDD::BIG_FLOAT>>::InitNoDistinctionTable_Ann();
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_FLOAT, std::multiplies<CFL_OBDD::BIG_FLOAT>>::InitIdentityNodeTable();		
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_FLOAT, std::multiplies<CFL_OBDD::BIG_FLOAT>>::InitReduceCache();
+	CFL_OBDD::WeightedMatrix1234FloatBoostMul::Matrix1234Initializer();
+	CFL_OBDD::WeightedVectorFloatBoostMul::VectorInitializer();
+	CFL_OBDD::InitWeightedPairProductCache<CFL_OBDD::BIG_FLOAT, std::multiplies<CFL_OBDD::BIG_FLOAT>>();
+
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>::InitNoDistinctionTable();
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>::InitNoDistinctionTable_Ann();
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>::InitIdentityNodeTable();	
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>::InitReduceCache();
+	CFL_OBDD::WeightedMatrix1234ComplexFloatBoostMul::Matrix1234Initializer();
+	CFL_OBDD::WeightedVectorComplexFloatBoostMul::VectorInitializer();
+	CFL_OBDD::InitWeightedPairProductCache<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>();
+
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<fourierSemiring, std::multiplies<fourierSemiring>>::InitNoDistinctionTable();
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<fourierSemiring, std::multiplies<fourierSemiring>>::InitNoDistinctionTable_Ann();
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<fourierSemiring, std::multiplies<fourierSemiring>>::InitIdentityNodeTable();	
+	CFL_OBDD::WeightedCFLOBDDNodeHandleT<fourierSemiring, std::multiplies<fourierSemiring>>::InitReduceCache();
+	CFL_OBDD::WeightedMatrix1234FourierMul::Matrix1234Initializer();
+	CFL_OBDD::WeightedVectorFourierMul::VectorInitializer();
+	CFL_OBDD::InitWeightedPairProductCache<fourierSemiring, std::multiplies<fourierSemiring>>();
+
+	CFL_OBDD::WeightedBDDNodeHandle<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>::InitLeafNodes();
+	CFL_OBDD::InitWeightedBDDPairProductCache<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>();
+}
+
+void CFLOBDD_module_dispose() {
+	CFL_OBDD::DisposeOfTripleProductCache();
+	CFL_OBDD::DisposeOfPairProductCache();
+	CFL_OBDD::CFLOBDDNodeHandle::DisposeOfReduceCache();
+	CFL_OBDD::DisposeOfWeightedPairProductCache<CFL_OBDD::BIG_FLOAT, std::multiplies<CFL_OBDD::BIG_FLOAT>>();
+	CFL_OBDD::DisposeOfWeightedPairProductCache<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>();
+	CFL_OBDD::DisposeOfWeightedPairProductCache<fourierSemiring, std::multiplies<fourierSemiring>>();
+
+	CFL_OBDD::DisposeOfWeightedBDDPairProductCache<CFL_OBDD::BIG_COMPLEX_FLOAT, std::multiplies<CFL_OBDD::BIG_COMPLEX_FLOAT>>();
+}
+
+class CFLOBDD_Nodestruct {
+private:
+    union {
+        CFL_OBDD::CFLOBDD cflobdd;
+    };
+public:
+    CFLOBDD_Nodestruct(CFL_OBDD::CFLOBDD &&cflobdd) : cflobdd(std::move(cflobdd)) {}
+    ~CFLOBDD_Nodestruct() {}
+    CFLOBDD get_value() {
+        return *(CFLOBDD *)&cflobdd;
+    }
+};
+
+CFLOBDD cast(CFL_OBDD::CFLOBDD &&cflobdd) {
+    CFLOBDD_Nodestruct a1(std::move(cflobdd));
+    return a1.get_value();
+}
+CFL_OBDD::CFLOBDD retrieve(CFLOBDD cflobdd) {
+    return CFL_OBDD::CFLOBDD(std::move(*(CFL_OBDD::CFLOBDD *)(&cflobdd)));
+}
+
+void forget(CFL_OBDD::CFLOBDD &&cflobdd) {
+    CFLOBDD_Nodestruct a1(std::move(cflobdd));
+}
+
+CFLOBDD CFLOBDD_createVar(uint32_t i, int level) {
+    return cast(std::move(CFL_OBDD::MkProjection(i, level)));
+}
+CFLOBDD CFLOBDD_createTrue(int level) {
+    return cast(std::move(CFL_OBDD::MkTrue(level)));
+}
+CFLOBDD CFLOBDD_createFalse(int level) {
+    return cast(std::move(CFL_OBDD::MkFalse(level)));
+}
+
+void CFLOBDD_delete(CFLOBDD cflobdd) {
+    auto a1 = retrieve(cflobdd);
+    // a1 will go out of scope and call destructor
+}
+
+// return the root address of CFLOBDD; can be used in hash
+CFLOBDD_C_API void *CFLOBDD_getRoot(const CFLOBDD_Ref cflobdd) {
+    auto a1 = retrieve(cflobdd);
+    void *ans = a1.root.get_ptr();
+    forget(std::move(a1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_copy(const CFLOBDD_Ref cflobdd) {
+    auto a1 = retrieve(cflobdd);
+    auto ans = cast(CFL_OBDD::CFLOBDD(a1));
+    forget(std::move(a1));
+    return ans;
+}
+
+
+
+CFLOBDD CFLOBDD_and(const CFLOBDD_Ref a, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(a);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkAnd(a1, b1));
+    forget(std::move(a1));
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_and_to(CFLOBDD product, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(product);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkAnd(a1, b1));
+    // a1 calls destructor when ans goes out of scope
+    // forget(a1);
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_or(const CFLOBDD_Ref a, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(a);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkOr(a1, b1));
+    forget(std::move(a1));
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_or_to(CFLOBDD sum, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(sum);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkOr(a1, b1));
+    // a1 calls destructor when ans goes out of scope
+    // forget(a1);
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_minus(const CFLOBDD_Ref a, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(a);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkMinus(a1, b1));
+    forget(std::move(a1));
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_not(const CFLOBDD_Ref a) {
+    auto a1 = retrieve(a);
+    auto ans = cast(CFL_OBDD::MkNot(a1));
+    forget(std::move(a1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_xor(const CFLOBDD_Ref a, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(a);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkExclusiveOr(a1, b1));
+    forget(std::move(a1));
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_xor_to(CFLOBDD sum, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(sum);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkExclusiveOr(a1, b1));
+    // a1 calls destructor when ans goes out of scope
+    // forget(a1);
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_implies(const CFLOBDD_Ref a, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(a);
+    auto b1 = retrieve(b);
+    auto ans = cast(CFL_OBDD::MkImplies(a1, b1));
+    forget(std::move(a1));
+    forget(std::move(b1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_exists(const CFLOBDD_Ref a, uint32_t i) {
+    auto a1 = retrieve(a);
+    auto ans = cast(CFL_OBDD::MkExists(a1, i));
+    forget(std::move(a1));
+    return ans;
+}
+
+CFLOBDD CFLOBDD_forall(const CFLOBDD_Ref a, uint32_t i) {
+    auto a1 = retrieve(a);
+    auto ans = cast(CFL_OBDD::MkForall(a1, i));
+    forget(std::move(a1));
+    return ans;
+}
+bool CFLOBDD_isValid(const CFLOBDD_Ref a) {
+    auto a1 = retrieve(a);
+    auto ans = a1.IsValid();
+    forget(std::move(a1));
+    return ans;
+}
+CFLOBDD_C_API uint32_t CFLOBDD_getLevel(const CFLOBDD_Ref cflobdd) {
+    auto a1 = retrieve(cflobdd);
+    auto ans = (*a1.root).level;
+    forget(std::move(a1));
+    return ans;
+}
+#ifdef PATH_COUNTING_ENABLED
+CFLOBDD_C_API uint32_t CFLOBDD_numSatisfyingAssignments(const CFLOBDD_Ref cflobdd) {
+    auto a1 = retrieve(cflobdd);
+    auto ans = a1.NumSatisfyingAssignments();
+    forget(std::move(a1));
+    return ans;
+}
+#endif
+
+CFLOBDD_C_API ssize_t CFLOBDD_getOneSatisfyingAssignment(const CFLOBDD_Ref cflobdd, bool *assignment_buffer, size_t assignment_buffer_size) {
+    auto a1 = retrieve(cflobdd);
+    uint32_t level_size = 1 << ((*a1.root).level);
+    uint32_t level_start = (1 << CFL_OBDD::CFLOBDD::maxLevel) - level_size;
+    SH_OBDD::Assignment *assignment;
+    bool ans = a1.FindOneSatisfyingAssignment(assignment);
+    forget(std::move(a1));
+    if (!ans) {
+        return 0;
+    }
+    size_t copy_size = assignment_buffer_size < level_size ? assignment_buffer_size : level_size;
+    memcpy(assignment_buffer, assignment->get_data() + level_start, copy_size);
+    delete assignment;
+    return copy_size;
+}
+
+bool CFLOBDD_eq(const CFLOBDD_Ref a, const CFLOBDD_Ref b) {
+    auto a1 = retrieve(a);
+    auto b1 = retrieve(b);
+    auto ans = a1 == b1;
+    forget(std::move(a1));
+    forget(std::move(b1));
+    return ans;
+}
+
+uint32_t CFLOBDD_hash(const CFLOBDD_Ref cflobdd) {
+    auto a1 = retrieve(cflobdd);
+    uint32_t ans = a1.Hash(1 << 32);
+    forget(std::move(a1));
+    return ans;
+}
+
+uint32_t CFLOBDD_countNodes(const CFLOBDD_Ref cflobdd) {
+    auto a1 = retrieve(cflobdd);
+    uint32_t ans = 0;
+    a1.CountNodes(ans);
+    forget(std::move(a1));
+    return ans;
+}
+
+void CFLOBDD_print(const CFLOBDD_Ref a) {
+    auto a1 = retrieve(a);
+    CFL_OBDD::PrintCFLOBDD(a1);
+    forget(std::move(a1));
+}
+}
\ No newline at end of file
diff --git a/CFLOBDD/cflobdd_c.h b/CFLOBDD/cflobdd_c.h
new file mode 100644
index 0000000..ebeff5d
--- /dev/null
+++ b/CFLOBDD/cflobdd_c.h
@@ -0,0 +1,70 @@
+#ifndef CFLOBDD_C_H
+#define CFLOBDD_C_H
+#ifdef __cplusplus
+extern "C" {
+#endif
+#include <stdint.h>
+#include <stdlib.h>
+#include <sys/types.h>
+#include <stdbool.h>
+#if defined(_WIN32)
+    #ifdef CFLOBDD_C_EXPORTS
+        #define CFLOBDD_C_API __declspec(dllexport)
+    #else
+        #define CFLOBDD_C_API __declspec(dllimport)
+    #endif
+#else
+    #define CFLOBDD_C_API __attribute__((visibility("default")))
+#endif
+
+// Opaque pointer to the C++ CFLOBDD object
+typedef size_t CFLOBDD;
+// also use ref to indicate that the function will not destroy the input CFLOBDD
+typedef size_t CFLOBDD_Ref;
+
+// C-style functions
+CFLOBDD_C_API void CFLOBDD_module_init();
+CFLOBDD_C_API void CFLOBDD_module_dispose();
+// Another "level" is needed since it do not have a "engine" concept.
+CFLOBDD_C_API CFLOBDD CFLOBDD_createVar(uint32_t i, int level);
+CFLOBDD_C_API CFLOBDD CFLOBDD_createTrue(int level);
+CFLOBDD_C_API CFLOBDD CFLOBDD_createFalse(int level);
+// destroy is not specifically needed since the destruction function is empty]
+// copy constructor
+CFLOBDD_C_API CFLOBDD CFLOBDD_copy(const CFLOBDD_Ref cflobdd);
+// return the root address of CFLOBDD; can be used in hash
+CFLOBDD_C_API void CFLOBDD_delete(CFLOBDD cflobdd);
+CFLOBDD_C_API CFLOBDD CFLOBDD_and(const CFLOBDD_Ref a, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_and_to(CFLOBDD product, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_or(const CFLOBDD_Ref a, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_or_to(CFLOBDD sum, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_minus(const CFLOBDD_Ref a, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_not(const CFLOBDD_Ref a);
+CFLOBDD_C_API CFLOBDD CFLOBDD_xor(const CFLOBDD_Ref a, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_xor_to(CFLOBDD sum, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_implies(const CFLOBDD_Ref a, const CFLOBDD_Ref b);
+CFLOBDD_C_API CFLOBDD CFLOBDD_exists(const CFLOBDD_Ref a, uint32_t i);
+CFLOBDD_C_API CFLOBDD CFLOBDD_forall(const CFLOBDD_Ref a, uint32_t i);
+CFLOBDD_C_API bool CFLOBDD_isValid(const CFLOBDD_Ref a);
+CFLOBDD_C_API uint32_t CFLOBDD_hash(const CFLOBDD_Ref cflobdd);
+CFLOBDD_C_API uint32_t CFLOBDD_countNodes(const CFLOBDD_Ref cflobdd);
+CFLOBDD_C_API uint32_t CFLOBDD_getLevel(const CFLOBDD_Ref cflobdd);
+CFLOBDD_C_API void *CFLOBDD_getRoot(const CFLOBDD_Ref cflobdd);
+#ifdef PATH_COUNTING_ENABLED
+CFLOBDD_C_API uint32_t CFLOBDD_numSatisfyingAssignments(const CFLOBDD_Ref cflobdd);
+#endif
+
+/// Get one satisfying assignment of the CFLOBDD.
+/// @param cflobdd The CFLOBDD.
+/// @param assignment_buffer The buffer to store the satisfying assignment.
+/// @param assignment_buffer_size The size (both in byte and in number of booleans) of the assignment_buffer.
+/// @return 0 if no satisfying assignment is found. If there is a satisfiable assignment,
+/// The size of buffer used to store the satisfying assignment if success, -1 if the assignment_buffer is too small.
+CFLOBDD_C_API ssize_t CFLOBDD_getOneSatisfyingAssignment(const CFLOBDD_Ref cflobdd, bool *assignment_buffer, size_t assignment_buffer_size);
+CFLOBDD_C_API bool CFLOBDD_eq(const CFLOBDD_Ref a, const CFLOBDD_Ref b);
+CFLOBDD_C_API void CFLOBDD_print(const CFLOBDD_Ref a);
+#ifdef __cplusplus
+}
+#endif
+
+#endif // CFLOBDD_C_H
\ No newline at end of file
diff --git a/CFLOBDD/cflobdd_node.cpp b/CFLOBDD/cflobdd_node.cpp
index cbefbcf..f4b4647 100644
--- a/CFLOBDD/cflobdd_node.cpp
+++ b/CFLOBDD/cflobdd_node.cpp
@@ -319,7 +319,7 @@ CFLOBDDNodeHandle::~CFLOBDDNodeHandle()
 }
 
 // Hash
-unsigned int CFLOBDDNodeHandle::Hash(unsigned int modsize)
+unsigned int CFLOBDDNodeHandle::Hash(unsigned long modsize)
 {
   return ((unsigned int) reinterpret_cast<uintptr_t>(handleContents) >> 2) % modsize;
 }
@@ -1277,7 +1277,7 @@ CFLReduceKey::CFLReduceKey(CFLOBDDNodeHandle nodeHandle, ReductionMapHandle redM
 }
 
 // Hash
-unsigned int CFLReduceKey::Hash(unsigned int modsize)
+unsigned int CFLReduceKey::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
   hvalue = (997 * nodeHandle.Hash(modsize) + redMapHandle.Hash(modsize)) % modsize;
@@ -1574,7 +1574,7 @@ CFLOBDDNodeHandle CFLOBDDInternalNode::Reduce(ReductionMapHandle& redMapHandle,
   return CFLOBDDNodeHandle(n);
 } // CFLOBDDInternalNode::Reduce
 
-unsigned int CFLOBDDInternalNode::Hash(unsigned int modsize)
+unsigned int CFLOBDDInternalNode::Hash(unsigned long modsize)
 {
   unsigned int hvalue = AConnection.Hash(modsize);
   for (unsigned int j = 0; j < numBConnections; j++) {
@@ -1909,7 +1909,7 @@ CFLOBDDNodeHandle CFLOBDDForkNode::Reduce(ReductionMapHandle&, unsigned int repl
 	}
 }
 
-unsigned int CFLOBDDForkNode::Hash(unsigned int modsize)
+unsigned int CFLOBDDForkNode::Hash(unsigned long modsize)
 {
   return ((unsigned int)reinterpret_cast<uintptr_t>(this) >> 2) % modsize;
 }
@@ -1983,7 +1983,7 @@ CFLOBDDNodeHandle CFLOBDDDontCareNode::Reduce(ReductionMapHandle&, unsigned int,
   return CFLOBDDNodeHandle::CFLOBDDDontCareNodeHandle;
 }
 
-unsigned int CFLOBDDDontCareNode::Hash(unsigned int modsize)
+unsigned int CFLOBDDDontCareNode::Hash(unsigned long modsize)
 {
   return ((unsigned int) reinterpret_cast<uintptr_t>(this) >> 2) % modsize;
 }
diff --git a/CFLOBDD/cflobdd_node.h b/CFLOBDD/cflobdd_node.h
index 2180210..df9c505 100644
--- a/CFLOBDD/cflobdd_node.h
+++ b/CFLOBDD/cflobdd_node.h
@@ -29,7 +29,7 @@
 
 
 // Configuration flags --------------------------------------------
-//#define PATH_COUNTING_ENABLED 1
+#define PATH_COUNTING_ENABLED 1
 
 namespace CFL_OBDD {
 
@@ -89,7 +89,7 @@ class CFLOBDDNodeHandle {
   CFLOBDDNodeHandle(CFLOBDDNode *n);                          // Constructor
   CFLOBDDNodeHandle(const CFLOBDDNodeHandle &nh);              // Copy constructor
   ~CFLOBDDNodeHandle();                                       // Destructor
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const CFLOBDDNodeHandle &nh);              // Overloaded !=
   bool operator== (const CFLOBDDNodeHandle &nh) const;              // Overloaded ==
   CFLOBDDNodeHandle & operator= (const CFLOBDDNodeHandle &nh); // assignment
@@ -182,7 +182,7 @@ namespace CFL_OBDD {
 
 	public:
 		CFLReduceKey(CFLOBDDNodeHandle nodeHandle, ReductionMapHandle redMap); // Constructor
-		unsigned int Hash(unsigned int modsize);
+		unsigned int Hash(unsigned long modsize);
 		CFLReduceKey& operator= (const CFLReduceKey& p);  // Overloaded assignment
 		bool operator!= (const CFLReduceKey& p);        // Overloaded !=
 		bool operator== (const CFLReduceKey& p);        // Overloaded ==
@@ -229,7 +229,7 @@ class CFLOBDDNode {
   virtual void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index) = 0;
   virtual int Traverse(SH_OBDD::AssignmentIterator &ai) = 0;
   virtual CFLOBDDNodeHandle Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, bool forceReduce = false) = 0;
-  virtual unsigned int Hash(unsigned int modsize) = 0;
+  virtual unsigned int Hash(unsigned long modsize) = 0;
   virtual void DumpConnections(Hashset<CFLOBDDNodeHandle> *visited, std::ostream & out = std::cout) = 0;
   virtual void CountNodesAndEdges(Hashset<CFLOBDDNodeHandle> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
 	  unsigned int &nodeCount, unsigned int &edgeCount, unsigned int &returnEdgesCount) = 0;
@@ -278,7 +278,7 @@ class CFLOBDDInternalNode : public CFLOBDDNode {
   void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index);
   int Traverse(SH_OBDD::AssignmentIterator &ai);
   CFLOBDDNodeHandle Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, bool forceReduce = false);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   void DumpConnections(Hashset<CFLOBDDNodeHandle> *visited, std::ostream & out = std::cout);
   void CountNodesAndEdges(Hashset<CFLOBDDNodeHandle> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
 	  unsigned int &nodeCount, unsigned int &edgeCount, unsigned int& returnEdgesCount);
@@ -322,7 +322,7 @@ class CFLOBDDLeafNode : public CFLOBDDNode {
   virtual void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index) = 0;
   virtual int Traverse(SH_OBDD::AssignmentIterator &ai) = 0;
   virtual CFLOBDDNodeHandle Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, bool forceReduce = false) = 0;
-  virtual unsigned int Hash(unsigned int modsize) = 0;
+  virtual unsigned int Hash(unsigned long modsize) = 0;
   void DumpConnections(Hashset<CFLOBDDNodeHandle> *visited, std::ostream & out = std::cout);
   void CountNodesAndEdges(Hashset<CFLOBDDNodeHandle> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
 	  unsigned int &nodeCount, unsigned int &edgeCount, unsigned int& returnEdgesCount);
@@ -350,7 +350,7 @@ class CFLOBDDForkNode : public CFLOBDDLeafNode {
   void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index);
   int Traverse(SH_OBDD::AssignmentIterator &ai);
   CFLOBDDNodeHandle Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, bool forceReduce = false);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const CFLOBDDNode & n);        // Overloaded !=
   bool operator== (const CFLOBDDNode & n);        // Overloaded ==
 
@@ -375,7 +375,7 @@ class CFLOBDDDontCareNode : public CFLOBDDLeafNode {
   void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index);
   int Traverse(SH_OBDD::AssignmentIterator &ai);
   CFLOBDDNodeHandle Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, bool forceReduce = false);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const CFLOBDDNode & n);        // Overloaded !=
   bool operator== (const CFLOBDDNode & n);        // Overloaded ==
 
diff --git a/CFLOBDD/cflobdd_t.h b/CFLOBDD/cflobdd_t.h
index 2ee673c..d891bef 100644
--- a/CFLOBDD/cflobdd_t.h
+++ b/CFLOBDD/cflobdd_t.h
@@ -1,6 +1,5 @@
 #ifndef CFLOBDD_T_GUARD
 #define CFLOBDD_T_GUARD
-
 //
 //    Copyright (c) 1999, 2017 Thomas W. Reps
 //    All Rights Reserved.
@@ -52,6 +51,7 @@ class CFLOBDD_T {
   CFLOBDD_T();      // Default constructor (rep. of \a.true)
   CFLOBDD_T(typename CFLOBDDTopNodeT<T>::CFLOBDDTopNodeTRefPtr n); // Constructor
   CFLOBDD_T(const CFLOBDD_T &d);                            // Copy constructor
+  CFLOBDD_T(CFLOBDD_T &&d);                            // Move constructor
   ~CFLOBDD_T();                                             // Destructor
   static unsigned int const maxLevel;
   bool Evaluate(SH_OBDD::Assignment &assignment);        // Evaluate a Boolean function
@@ -63,10 +63,11 @@ class CFLOBDD_T {
 #endif
   bool FindOneSatisfyingAssignment(SH_OBDD::Assignment * &assignment);
                                                 // Find a satisfying assignment
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const CFLOBDD_T & C) const;          // Overloaded !=
   bool operator== (const CFLOBDD_T & C) const;          // Overloaded ==
   CFLOBDD_T& operator= (const CFLOBDD_T &c);       // assignment
+  CFLOBDD_T& operator= (CFLOBDD_T &&c);       // Move assignment
   ref_ptr<CFLOBDDTopNodeT<T>> root;
 
   void DumpConnections(std::ostream & out = std::cout);
@@ -112,6 +113,13 @@ CFLOBDD_T<T>::CFLOBDD_T(const CFLOBDD_T<T> &c)
 	root = c.root;
 }
 
+// Move constructor
+template<typename T>
+CFLOBDD_T<T>::CFLOBDD_T(CFLOBDD_T<T> &&c)
+{
+	root = std::move(c.root);
+}
+
 template<typename T>
 CFLOBDD_T<T>::~CFLOBDD_T()
 {
@@ -178,7 +186,7 @@ bool CFLOBDD_T<T>::FindOneSatisfyingAssignment(SH_OBDD::Assignment * &assignment
 
 // Hash
 template<typename T>
-unsigned int CFLOBDD_T<T>::Hash(unsigned int modsize)
+unsigned int CFLOBDD_T<T>::Hash(unsigned long modsize)
 {
 	return root->Hash(modsize);
 }
@@ -241,6 +249,18 @@ CFLOBDD_T<T> & CFLOBDD_T<T>::operator= (const CFLOBDD_T<T> &c)
 	return *this;
 }
 
+// Move assignment
+template<typename T>
+CFLOBDD_T<T> & CFLOBDD_T<T>::operator= (CFLOBDD_T<T> &&c)
+{
+	if (this != &c)      // don't assign to self!
+	{
+		root = std::move(c.root);
+	}
+	return *this;
+}
+
+
 
 // print
 template<typename T>
diff --git a/CFLOBDD/cflobdd_top_node_complex_float_boost.cpp b/CFLOBDD/cflobdd_top_node_complex_float_boost.cpp
index 84d5699..5fa888b 100644
--- a/CFLOBDD/cflobdd_top_node_complex_float_boost.cpp
+++ b/CFLOBDD/cflobdd_top_node_complex_float_boost.cpp
@@ -43,7 +43,7 @@ bool CFLOBDDTopNodeT<BIG_COMPLEX_FLOAT>::FindOneSatisfyingAssignment(SH_OBDD::As
 // Running time: Linear in the size of the CFLOBDDTopNode
 //
 template <>
-unsigned int CFLOBDDTopNodeT<BIG_FLOAT>::NumSatisfyingAssignments()
+unsigned int CFLOBDDTopNodeT<BIG_COMPLEX_FLOAT>::NumSatisfyingAssignments()
 {
 	unsigned int ans = 0;
 
diff --git a/CFLOBDD/cflobdd_top_node_t.cpp b/CFLOBDD/cflobdd_top_node_t.cpp
index 91f5eaa..2dd2fcb 100644
--- a/CFLOBDD/cflobdd_top_node_t.cpp
+++ b/CFLOBDD/cflobdd_top_node_t.cpp
@@ -284,7 +284,7 @@ namespace CFL_OBDD{
 
     // Hash
     template <typename T>
-    unsigned int CFLOBDDTopNodeT<T>::Hash(unsigned int modsize)
+    unsigned int CFLOBDDTopNodeT<T>::Hash(unsigned long modsize)
     {
         return rootConnection.Hash(modsize);
     }
diff --git a/CFLOBDD/cflobdd_top_node_t.h b/CFLOBDD/cflobdd_top_node_t.h
index 53229af..63781be 100644
--- a/CFLOBDD/cflobdd_top_node_t.h
+++ b/CFLOBDD/cflobdd_top_node_t.h
@@ -65,7 +65,7 @@ class CFLOBDDTopNodeT {
   //mpz_class NumSatisfyingAssignments();
 #endif
   bool FindOneSatisfyingAssignment(SH_OBDD::Assignment * &assignment);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   void DumpConnections(Hashset<CFLOBDDNodeHandle> *visited, std::ostream & out = std::cout);
   void CountNodesAndEdges(Hashset<CFLOBDDNodeHandle> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
 	  unsigned int &nodeCount, unsigned int &edgeCount, unsigned int& returnEdgesCount, unsigned int &returnEdgesObjCount);
diff --git a/CFLOBDD/connectionT.cpp b/CFLOBDD/connectionT.cpp
index b59b55a..a9204b6 100644
--- a/CFLOBDD/connectionT.cpp
+++ b/CFLOBDD/connectionT.cpp
@@ -34,7 +34,7 @@ ConnectionT<Handle>::~ConnectionT()
 
 // Hash
 template <typename Handle>
-unsigned int ConnectionT<Handle>::Hash(unsigned int modsize)
+unsigned int ConnectionT<Handle>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 	hvalue = (997 * returnMapHandle.Hash(modsize) + entryPointHandle->Hash(modsize)) % modsize;
diff --git a/CFLOBDD/connectionT.h b/CFLOBDD/connectionT.h
index c4e04c5..0f6d509 100644
--- a/CFLOBDD/connectionT.h
+++ b/CFLOBDD/connectionT.h
@@ -55,7 +55,7 @@ namespace CFL_OBDD {
 		ConnectionT(CFLOBDDNodeHandle &entryPointHandle, Handle &returnMapHandle);
 		~ConnectionT();                                 // Destructor
 
-		unsigned int Hash(unsigned int modsize);
+		unsigned int Hash(unsigned long modsize);
 		ConnectionT& operator= (const ConnectionT &C);   // Overloaded =
 		bool operator!= (const ConnectionT & C);        // Overloaded !=
 		bool operator== (const ConnectionT & C);        // Overloaded ==
diff --git a/CFLOBDD/cross_product.cpp b/CFLOBDD/cross_product.cpp
index 0161d85..ec1e9be 100644
--- a/CFLOBDD/cross_product.cpp
+++ b/CFLOBDD/cross_product.cpp
@@ -71,7 +71,7 @@ void PairProductMapBody::DecrRef()
   }
 }
 
-unsigned int PairProductMapBody::Hash(unsigned int modsize)
+unsigned int PairProductMapBody::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
 
@@ -195,7 +195,7 @@ std::ostream& operator<< (std::ostream & out, const PairProductMapHandle &r)
   return(out);
 }
 
-unsigned int PairProductMapHandle::Hash(unsigned int modsize)
+unsigned int PairProductMapHandle::Hash(unsigned long modsize)
 {
   return ((unsigned int) reinterpret_cast<uintptr_t>(mapContents) >> 2) % modsize;
 }
@@ -309,7 +309,7 @@ PairProductKey::PairProductKey(CFLOBDDNodeHandle nodeHandle1, CFLOBDDNodeHandle
 }
 
 // Hash
-unsigned int PairProductKey::Hash(unsigned int modsize)
+unsigned int PairProductKey::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
   hvalue = (997 * nodeHandle1.Hash(modsize) + nodeHandle2.Hash(modsize)) % modsize;
@@ -626,7 +626,7 @@ void TripleProductMapBody::DecrRef()
   }
 }
 
-unsigned int TripleProductMapBody::Hash(unsigned int modsize)
+unsigned int TripleProductMapBody::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
   TripleProductMapBodyIterator mi(*this);
@@ -702,7 +702,7 @@ std::ostream& operator<< (std::ostream & out, const TripleProductMapHandle &r)
   return(out);
 }
 
-unsigned int TripleProductMapHandle::Hash(unsigned int modsize)
+unsigned int TripleProductMapHandle::Hash(unsigned long modsize)
 {
   return ((unsigned int) reinterpret_cast<uintptr_t>(mapContents) >> 2) % modsize;
 }
@@ -776,7 +776,7 @@ TripleProductKey::TripleProductKey(CFLOBDDNodeHandle nodeHandle1, CFLOBDDNodeHan
 }
 
 // Hash
-unsigned int TripleProductKey::Hash(unsigned int modsize)
+unsigned int TripleProductKey::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
   hvalue = (997 * (997 * nodeHandle1.Hash(modsize) + nodeHandle2.Hash(modsize)) + nodeHandle3.Hash(modsize)) % modsize;
diff --git a/CFLOBDD/cross_product.h b/CFLOBDD/cross_product.h
index 23c9e25..dd0ca65 100644
--- a/CFLOBDD/cross_product.h
+++ b/CFLOBDD/cross_product.h
@@ -59,7 +59,7 @@ class PairProductMapHandle {
   PairProductMapHandle& operator= (const PairProductMapHandle &r); // Overloaded assignment
   bool operator!= (const PairProductMapHandle &r);      // Overloaded !=
   bool operator== (const PairProductMapHandle &r);      // Overloaded ==
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int Size();
   intpair& operator[](unsigned int i);                       // Overloaded []
   void AddToEnd(const intpair& p);
@@ -82,7 +82,7 @@ class PairProductMapBody {//: public List<intpair> {
   PairProductMapBody();    // Constructor
   void IncrRef();
   void DecrRef();
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int refCount;         // reference-count value
   void setHashCheck();
   void AddToEnd(const intpair& y);          // Override AddToEnd
@@ -109,7 +109,7 @@ class PairProductKey {
 
  public:
   PairProductKey(CFLOBDDNodeHandle nodeHandle1, CFLOBDDNodeHandle nodeHandle2); // Constructor
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   PairProductKey& operator= (const PairProductKey& p);  // Overloaded assignment
   bool operator!= (const PairProductKey& p);        // Overloaded !=
   bool operator== (const PairProductKey& p);        // Overloaded ==
@@ -184,7 +184,7 @@ class TripleProductMapHandle {
   TripleProductMapHandle& operator= (const TripleProductMapHandle &r); // Overloaded assignment
   bool operator!= (const TripleProductMapHandle &r);      // Overloaded !=
   bool operator== (const TripleProductMapHandle &r);      // Overloaded ==
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int Size();
   void AddToEnd(inttriple t);
   bool Member(inttriple t);
@@ -205,7 +205,7 @@ class TripleProductMapBody : public List<inttriple> {
   TripleProductMapBody();    // Constructor
   void IncrRef();
   void DecrRef();
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int refCount;         // reference-count value
 
  public:
@@ -226,7 +226,7 @@ class TripleProductKey {
 
  public:
   TripleProductKey(CFLOBDDNodeHandle nodeHandle1, CFLOBDDNodeHandle nodeHandle2, CFLOBDDNodeHandle nodeHandle3); // Constructor
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   TripleProductKey& operator= (const TripleProductKey& p);  // Overloaded assignment
   bool operator!= (const TripleProductKey& p);        // Overloaded !=
   bool operator== (const TripleProductKey& p);        // Overloaded ==
diff --git a/CFLOBDD/java_bindings/.gitignore b/CFLOBDD/java_bindings/.gitignore
new file mode 100644
index 0000000..c41cc9e
--- /dev/null
+++ b/CFLOBDD/java_bindings/.gitignore
@@ -0,0 +1 @@
+/target
\ No newline at end of file
diff --git a/CFLOBDD/java_bindings/README.md b/CFLOBDD/java_bindings/README.md
new file mode 100644
index 0000000..bea02f6
--- /dev/null
+++ b/CFLOBDD/java_bindings/README.md
@@ -0,0 +1,18 @@
+# CFLOBDD Java Bindings
+
+> [!WARNING]
+> The Java binding is still under development; only part of the APIs are available.
+
+## Introduction
+
+This binding is a drop-in replacement of CFLOBDD for JDD. It uses `java.lang.foreign` to interface with the shared library of CFLOBDD, so Java 22 or higher is required.
+
+The binding currently contains two types of APIs:
+- `CFLOBDD.java`: the main class that provides the CFLOBDD APIs. It directly interacts with CFLOBDD shared library.
+- `api/jdd/BDD.java`: is a wrapper around `CFLOBDD.java` that provides the same APIs as `jdd.bdd.BDD`. As it contains optimizations like operation cache, it is more efficient than `CFLOBDD.java`. **We recommend using `api/jdd/BDD.java` instead of `CFLOBDD.java` in most cases.**
+
+## Usage
+
+1. Replace `import jdd.bdd.BDD;` with `import org.trishullab.cflobdd.api.jdd.BDD;`
+2. The constructor of `org.trishullab.cflobdd.api.jdd.BDD` is different from that of `jdd.bdd.BDD`. It takes `int level` instead of `int nodesize` as the first parameter. $n$-level CFLOBDD contains $2^n$ variables.
+3. Make sure that `libcflobdd.so` or `libcflobdd.dylib` is in the `java.library.path`.
\ No newline at end of file
diff --git a/CFLOBDD/java_bindings/pom.xml b/CFLOBDD/java_bindings/pom.xml
new file mode 100644
index 0000000..4ba2944
--- /dev/null
+++ b/CFLOBDD/java_bindings/pom.xml
@@ -0,0 +1,98 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+  xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+  <modelVersion>4.0.0</modelVersion>
+
+  <groupId>org.trishullab.cflobdd</groupId>
+  <artifactId>cflobdd</artifactId>
+  <version>1.0-SNAPSHOT</version>
+
+  <name>cflobdd</name>
+  <!-- FIXME change it to the project's website -->
+  <url>http://www.example.com</url>
+
+  <properties>
+    <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
+    <maven.compiler.release>22</maven.compiler.release>
+  </properties>
+
+  <dependencyManagement>
+    <dependencies>
+      <dependency>
+        <groupId>org.junit</groupId>
+        <artifactId>junit-bom</artifactId>
+        <version>5.11.0</version>
+        <type>pom</type>
+        <scope>import</scope>
+      </dependency>
+    </dependencies>
+  </dependencyManagement>
+
+  <dependencies>
+    <dependency>
+      <groupId>org.junit.jupiter</groupId>
+      <artifactId>junit-jupiter-api</artifactId>
+      <scope>test</scope>
+    </dependency>
+    <!-- Optionally: parameterized tests support -->
+    <dependency>
+      <groupId>org.junit.jupiter</groupId>
+      <artifactId>junit-jupiter-params</artifactId>
+      <scope>test</scope>
+    </dependency>
+    <dependency>
+      <groupId>org.bitbucket.vahidi</groupId>
+      <artifactId>jdd</artifactId>
+      <version>112</version>
+    </dependency>
+  </dependencies>
+
+  <build>
+    <pluginManagement><!-- lock down plugins versions to avoid using Maven defaults (may be moved to parent pom) -->
+      <plugins>
+        <!-- clean lifecycle, see https://maven.apache.org/ref/current/maven-core/lifecycles.html#clean_Lifecycle -->
+        <plugin>
+          <artifactId>maven-clean-plugin</artifactId>
+          <version>3.4.0</version>
+        </plugin>
+        <!-- default lifecycle, jar packaging: see https://maven.apache.org/ref/current/maven-core/default-bindings.html#Plugin_bindings_for_jar_packaging -->
+        <plugin>
+          <artifactId>maven-resources-plugin</artifactId>
+          <version>3.3.1</version>
+        </plugin>
+        <plugin>
+          <artifactId>maven-compiler-plugin</artifactId>
+          <version>3.13.0</version>
+        </plugin>
+        <plugin>
+          <artifactId>maven-surefire-plugin</artifactId>
+          <version>3.3.0</version>
+          <configuration>
+            <argLine>-Djava.library.path=../../build</argLine>
+          </configuration>
+        </plugin>
+        <plugin>
+          <artifactId>maven-jar-plugin</artifactId>
+          <version>3.4.2</version>
+        </plugin>
+        <plugin>
+          <artifactId>maven-install-plugin</artifactId>
+          <version>3.1.2</version>
+        </plugin>
+        <plugin>
+          <artifactId>maven-deploy-plugin</artifactId>
+          <version>3.1.2</version>
+        </plugin>
+        <!-- site lifecycle, see https://maven.apache.org/ref/current/maven-core/lifecycles.html#site_Lifecycle -->
+        <plugin>
+          <artifactId>maven-site-plugin</artifactId>
+          <version>3.12.1</version>
+        </plugin>
+        <plugin>
+          <artifactId>maven-project-info-reports-plugin</artifactId>
+          <version>3.6.1</version>
+        </plugin>
+      </plugins>
+    </pluginManagement>
+  </build>
+</project>
diff --git a/CFLOBDD/java_bindings/src/main/java/org/trishullab/cflobdd/CFLOBDD.java b/CFLOBDD/java_bindings/src/main/java/org/trishullab/cflobdd/CFLOBDD.java
new file mode 100644
index 0000000..edae432
--- /dev/null
+++ b/CFLOBDD/java_bindings/src/main/java/org/trishullab/cflobdd/CFLOBDD.java
@@ -0,0 +1,337 @@
+package org.trishullab.cflobdd;
+import java.lang.foreign.*;
+import java.lang.invoke.MethodHandle;
+import java.util.Arrays;
+
+public class CFLOBDD implements Cloneable {
+    private static final Linker linker;
+    private static final Arena arena = Arena.ofShared();
+    private static final MethodHandle moduleInitHandle, moduleDisposeHandle, createVarHandle, createTrueHandle, createFalseHandle, 
+        deleteHandle, copyHandle, getRootHandle, andHandle, andToHandle, orHandle, orToHandle, minusHandle, notHandle, xorHandle,
+        xorToHandle, impliesHandle, existsHandle, forallHandle, isValidHandle, eqHandle, printHandle, getLevelHandle, hashHandle,
+        countNodesHandle, numSatisfyingAssignmentsHandle, getOneSatisfyingAssignmentHandle;
+    private long bdd_addr;
+
+    static {
+        System.loadLibrary("cflobdd");
+        linker = Linker.nativeLinker();
+        // Use system default library lookup which respects java.library.path and system-specific paths
+        SymbolLookup dylibs = SymbolLookup.loaderLookup();
+        moduleInitHandle = linker.downcallHandle(dylibs.find("CFLOBDD_module_init").orElseThrow(),
+            FunctionDescriptor.ofVoid());
+        moduleDisposeHandle = linker.downcallHandle(dylibs.find("CFLOBDD_module_dispose").orElseThrow(),
+            FunctionDescriptor.ofVoid());
+        try {
+            moduleInitHandle.invokeWithArguments();
+        } catch (Throwable e) {
+            throw new ExceptionInInitializerError(e);
+        }
+        createVarHandle = linker.downcallHandle(dylibs.find("CFLOBDD_createVar").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_INT, ValueLayout.JAVA_INT));
+        createTrueHandle = linker.downcallHandle(dylibs.find("CFLOBDD_createTrue").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_INT));
+        createFalseHandle = linker.downcallHandle(dylibs.find("CFLOBDD_createFalse").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_INT));
+        deleteHandle = linker.downcallHandle(dylibs.find("CFLOBDD_delete").orElseThrow(),
+            FunctionDescriptor.ofVoid(ValueLayout.JAVA_LONG));
+        copyHandle = linker.downcallHandle(dylibs.find("CFLOBDD_copy").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        getRootHandle = linker.downcallHandle(dylibs.find("CFLOBDD_getRoot").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        andHandle = linker.downcallHandle(dylibs.find("CFLOBDD_and").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        andToHandle = linker.downcallHandle(dylibs.find("CFLOBDD_and_to").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        orHandle = linker.downcallHandle(dylibs.find("CFLOBDD_or").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        orToHandle = linker.downcallHandle(dylibs.find("CFLOBDD_or_to").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        minusHandle = linker.downcallHandle(dylibs.find("CFLOBDD_minus").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        notHandle = linker.downcallHandle(dylibs.find("CFLOBDD_not").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        xorHandle = linker.downcallHandle(dylibs.find("CFLOBDD_xor").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        xorToHandle = linker.downcallHandle(dylibs.find("CFLOBDD_xor_to").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        impliesHandle = linker.downcallHandle(dylibs.find("CFLOBDD_implies").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        existsHandle = linker.downcallHandle(dylibs.find("CFLOBDD_exists").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_INT));
+        forallHandle = linker.downcallHandle(dylibs.find("CFLOBDD_forall").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_INT));
+        isValidHandle = linker.downcallHandle(dylibs.find("CFLOBDD_isValid").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_BOOLEAN, ValueLayout.JAVA_LONG));
+        eqHandle = linker.downcallHandle(dylibs.find("CFLOBDD_eq").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_BOOLEAN, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+        printHandle = linker.downcallHandle(dylibs.find("CFLOBDD_print").orElseThrow(),
+            FunctionDescriptor.ofVoid(ValueLayout.JAVA_LONG));
+        getLevelHandle = linker.downcallHandle(dylibs.find("CFLOBDD_getLevel").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_INT, ValueLayout.JAVA_LONG));
+        hashHandle = linker.downcallHandle(dylibs.find("CFLOBDD_hash").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_INT, ValueLayout.JAVA_LONG));
+        countNodesHandle = linker.downcallHandle(dylibs.find("CFLOBDD_countNodes").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_INT, ValueLayout.JAVA_LONG));
+        numSatisfyingAssignmentsHandle = linker.downcallHandle(dylibs.find("CFLOBDD_numSatisfyingAssignments").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_INT, ValueLayout.JAVA_LONG));
+        getOneSatisfyingAssignmentHandle = linker.downcallHandle(dylibs.find("CFLOBDD_getOneSatisfyingAssignment").orElseThrow(),
+            FunctionDescriptor.of(ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG, ValueLayout.JAVA_LONG));
+    }
+
+    private CFLOBDD(long bdd_addr) {
+        this.bdd_addr = bdd_addr;
+    }
+
+    @Override
+    public CFLOBDD clone() {
+        try {
+            long ans = (long) copyHandle.invokeWithArguments(bdd_addr);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public long getRoot() {
+        try {
+            return (long) getRootHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    public static void dispose_module() {
+        try {
+            moduleDisposeHandle.invokeWithArguments();
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+        arena.close();
+    }
+
+    public static CFLOBDD createVar(int varId, int level) {
+        try {
+            long ans = (long) createVarHandle.invokeWithArguments(varId, level);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public void deref() {
+        try {
+            deleteHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD createTrue(int level) {
+        try {
+            long ans = (long) createTrueHandle.invokeWithArguments(level);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD createFalse(int level) {
+        try {
+            long ans = (long) createFalseHandle.invokeWithArguments(level);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD not(CFLOBDD bdd) {
+        try {
+            long ans = (long) notHandle.invokeWithArguments(bdd.bdd_addr);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD or(CFLOBDD bdd1, CFLOBDD bdd2) {
+        try {
+            long ans = (long) orHandle.invokeWithArguments(bdd1.bdd_addr, bdd2.bdd_addr);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public void orWith(CFLOBDD other) {
+        try {
+            long ans = (long) orToHandle.invokeWithArguments(bdd_addr, other.bdd_addr);
+            this.bdd_addr = ans;
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD and(CFLOBDD bdd1, CFLOBDD bdd2) {
+        try {
+            long ans = (long) andHandle.invokeWithArguments(bdd1.bdd_addr, bdd2.bdd_addr);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public void andWith(CFLOBDD other) {
+        try {
+            long ans = (long) andToHandle.invokeWithArguments(bdd_addr, other.bdd_addr);
+            this.bdd_addr = ans;
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD diff(CFLOBDD bdd1, CFLOBDD bdd2) {
+        try {
+            long ans = (long) minusHandle.invokeWithArguments(bdd1.bdd_addr, bdd2.bdd_addr);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    public static CFLOBDD xor(CFLOBDD bdd1, CFLOBDD bdd2) {
+        try {
+            long ans = (long) xorHandle.invokeWithArguments(bdd1.bdd_addr, bdd2.bdd_addr);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    public void xorWith(CFLOBDD other) {
+        try {
+            long ans = (long) xorToHandle.invokeWithArguments(bdd_addr, other.bdd_addr);
+            this.bdd_addr = ans;
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    public static CFLOBDD imp(CFLOBDD bdd1, CFLOBDD bdd2) {
+        try {
+            long ans = (long) impliesHandle.invokeWithArguments(bdd1.bdd_addr, bdd2.bdd_addr);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD exists(CFLOBDD bdd, int varId) {
+        try {
+            long ans = (long) existsHandle.invokeWithArguments(bdd.bdd_addr, varId);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public static CFLOBDD forall(CFLOBDD bdd, int varId) {
+        try {
+            long ans = (long) forallHandle.invokeWithArguments(bdd.bdd_addr, varId);
+            return new CFLOBDD(ans);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public boolean isValid() {
+        try {
+            return (boolean) isValidHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public void print() {
+        try {
+            printHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public int satCount() {
+        try {
+            return (int) numSatisfyingAssignmentsHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public int nodeCount() {
+        try {
+            return (int) countNodesHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+    public int getLevel() {
+        try {
+            return (int) getLevelHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+        
+    public int[] oneSat() {
+        // always return full vector,
+        // collected by system gc.
+        // if unsat, return full -1;
+        int ans_length = 1 << getLevel();
+        int[] ans = new int[ans_length];
+        try (Arena tempArena = Arena.ofConfined()) {
+            MemorySegment c_ans = tempArena.allocate(ans_length);
+            long ret;
+            try {
+                ret = (long) getOneSatisfyingAssignmentHandle.invokeWithArguments(bdd_addr, c_ans.address(), ans_length);
+            } catch (Throwable e) {
+                throw new RuntimeException(e);
+            }
+            if (ret == 0) {
+                Arrays.fill(ans, -1);
+            } else if (ret < 0) {
+                throw new RuntimeException("getOneSatisfyingAssignment failed");
+            } else {
+                for (int i = 0; i < ans_length; i++) {
+                    ans[i] = c_ans.get(ValueLayout.JAVA_BOOLEAN, i) ? 1 : 0;
+                }
+            }
+        }
+        return ans;
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (obj == null) {
+            return false;
+        }
+        if (obj == this) {
+            return true;
+        }
+        if (obj instanceof CFLOBDD) {
+            CFLOBDD other = (CFLOBDD) obj;
+            try {
+                return (boolean) eqHandle.invokeWithArguments(bdd_addr, other.bdd_addr);
+            } catch (Throwable e) {
+                throw new RuntimeException(e);
+            }
+        }
+        return false;
+    }
+
+    @Override
+    public int hashCode() {
+        try {
+            return (int) hashHandle.invokeWithArguments(bdd_addr);
+        } catch (Throwable e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    public static void main(String[] args) {
+        CFLOBDD zero = createFalse(1);
+        CFLOBDD a = createVar(0, 1);
+        CFLOBDD b = createVar(1, 1);
+        System.out.printf("z @ %x: %x\n",zero.bdd_addr, zero.hashCode());
+        System.out.printf("a @ %x: %x\n",a.bdd_addr, a.hashCode());
+        System.out.printf("b @ %x: %x\n",b.bdd_addr, b.hashCode());
+        System.out.println(Arrays.toString(a.oneSat()));
+        zero.deref();
+        a.deref();
+        b.deref();
+        dispose_module();
+    }
+}
\ No newline at end of file
diff --git a/CFLOBDD/java_bindings/src/main/java/org/trishullab/cflobdd/api/jdd/BDD.java b/CFLOBDD/java_bindings/src/main/java/org/trishullab/cflobdd/api/jdd/BDD.java
new file mode 100644
index 0000000..ed0b846
--- /dev/null
+++ b/CFLOBDD/java_bindings/src/main/java/org/trishullab/cflobdd/api/jdd/BDD.java
@@ -0,0 +1,284 @@
+package org.trishullab.cflobdd.api.jdd;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+
+import org.trishullab.cflobdd.CFLOBDD;
+import jdd.bdd.OptimizedCache;
+import jdd.bdd.SimpleCache;
+
+class Configuration {
+   public static int bddOpcacheDiv = 1;
+   public static int bddNegcacheDiv = 2;
+   public static int bddQuantcacheDiv = 3;
+}
+
+public class BDD {
+   protected static final int CACHE_AND = 0;
+   protected static final int CACHE_OR = 1;
+   protected static final int CACHE_XOR = 2;
+   protected static final int CACHE_BIIMP = 3;
+   protected static final int CACHE_IMP = 4;
+   protected static final int CACHE_NAND = 5;
+   protected static final int CACHE_NOR = 6;
+   protected static final int CACHE_RESTRICT = 7;
+   protected static final int CACHE_EXISTS = 0;
+   protected static final int CACHE_FORALL = 1;
+
+    private final int level;
+    private int varCount;
+    private List<CFLOBDD> bddtable;
+    private List<Integer> hashList;
+    private List<Integer> refCount;
+    protected SimpleCache op_cache;
+    protected SimpleCache not_cache;
+    protected SimpleCache quant_cache;
+
+    /// A map from node's hash to node's index in bddtable
+    private HashMap<Integer, Integer> lookup;
+
+    private List<Integer> freeList;
+    
+    public BDD(int level, int cache_size) {
+        this.level = level;
+        bddtable = new ArrayList<>();
+        refCount = new ArrayList<>();
+        freeList = new LinkedList<>();
+        hashList = new ArrayList<>();
+        lookup = new HashMap<>();
+        bddtable.add(CFLOBDD.createFalse(level));
+        bddtable.add(CFLOBDD.createTrue(level));
+        refCount.add(1);
+        refCount.add(1);
+        int hash0 = bddtable.get(0).hashCode();
+        int hash1 = bddtable.get(1).hashCode();
+        hashList.add(hash0);
+        hashList.add(hash1);
+        lookup.put(hash0, 0);
+        lookup.put(hash1, 1);
+
+        // from jdd
+
+        this.op_cache = new OptimizedCache("OP", cache_size / Configuration.bddOpcacheDiv, 3, 2);
+        this.not_cache = new OptimizedCache("NOT", cache_size / Configuration.bddNegcacheDiv, 1, 1);
+        this.quant_cache = new OptimizedCache("QUANT", cache_size / Configuration.bddQuantcacheDiv, 3, 2);
+
+    }
+
+    public final int ref(int bdd) {
+        bddtable.get(bdd).clone();
+        refCount.set(bdd, refCount.get(bdd) + 1);
+        // remove from freelist only if ref count is 1 (0 before)
+        // if (refCount.get(bdd) == 1 && freeList.contains(bdd)) {
+        //     System.err.println("Should not ref bdd in that is alreadly freed");
+        //     // throw new RuntimeException("Should not ref bdd in that is alreadly freed");
+        //     freeList.remove((Integer) bdd);
+        //     lookup.put(hashList.get(bdd), bdd);
+        // }
+        return bdd;
+    }
+    public final int deref(int bdd) {
+        if (bdd == 0 || bdd == 1) {
+            return bdd;
+        }
+        if (refCount.get(bdd) == 0) {
+            System.err.println("Double free");
+            return bdd;
+        }
+        bddtable.get(bdd).deref();
+        refCount.set(bdd, refCount.get(bdd) - 1);
+        // don't free to enable caching.
+        if (refCount.get(bdd) == 0) {
+        // don't free to enable caching.
+        //     freeList.add(bdd);
+            lookup.remove(hashList.get(bdd));
+        //     // table and hashlist are kept and
+        }
+        return bdd;
+    }
+
+    private int putBdd(CFLOBDD val) {
+        int val_hash = val.hashCode();
+        if (lookup.containsKey(val_hash)) {
+            int ans = lookup.get(val_hash);
+            val.deref();
+            bddtable.get(ans).clone();
+            refCount.set(ans, refCount.get(ans) + 1);
+            return ans;
+        }
+        if (freeList.size() > 0) {
+            int bdd = freeList.remove(0);
+            bddtable.set(bdd, val);
+            refCount.set(bdd, 1);
+            lookup.put(val_hash, bdd);
+            hashList.set(bdd, val_hash);
+            return bdd;
+        }
+        bddtable.add(val);
+        refCount.add(1);
+        hashList.add(val_hash);
+        lookup.put(val_hash, bddtable.size() - 1);
+        return bddtable.size() - 1;
+    }
+
+    public int createVar() {
+        CFLOBDD bdd = CFLOBDD.createVar(varCount++, level);
+        return putBdd(bdd);
+    }
+
+    public int not(int bdd) {
+        if (bdd < 2) {
+            return bdd ^ 1; // no need to ref
+        }
+        if (this.not_cache.lookup(bdd)) {
+            if (refCount.get(this.not_cache.answer) > 0) {
+                return ref(this.not_cache.answer);
+            } // otherwise it is invalidated
+        }
+        int hash = this.not_cache.hash_value;
+        CFLOBDD notBdd = CFLOBDD.not(bddtable.get(bdd));
+        int ans = putBdd(notBdd);
+        this.not_cache.insert(hash, bdd, ans);
+        return ans;
+    }
+        
+    public int and(int bdd1, int bdd2) {
+        if (bdd1 == 0 || bdd2 == 0) {
+            return 0;
+        }
+        if (bdd1 == 1) {
+            return ref(bdd2);
+        }
+        if (bdd2 == 1) {
+            return ref(bdd1);
+        }
+        if (this.op_cache.lookup(bdd1, bdd2, CACHE_AND)) {
+            if (refCount.get(this.op_cache.answer) > 0) {
+                return ref(this.op_cache.answer);
+            }
+        }
+        int hash = this.op_cache.hash_value;
+        CFLOBDD andBdd = CFLOBDD.and(bddtable.get(bdd1), bddtable.get(bdd2));
+        int ans = putBdd(andBdd);
+        this.op_cache.insert(hash, bdd1, bdd2, CACHE_AND, ans);
+        return ans;
+    }
+        
+    public int or(int bdd1, int bdd2) {
+        if (bdd1 == 1 || bdd2 == 1) {
+            return 1;
+        }
+        if (bdd1 == 0) {
+            return ref(bdd2);
+        }
+        if (bdd2 == 0) {
+            return ref(bdd1);
+        }
+        if (this.op_cache.lookup(bdd1, bdd2, CACHE_OR)) {
+            if (refCount.get(this.op_cache.answer) > 0) {
+                return ref(this.op_cache.answer);
+            }
+        }
+        int hash = this.op_cache.hash_value;
+        CFLOBDD orBdd = CFLOBDD.or(bddtable.get(bdd1), bddtable.get(bdd2));
+        int ans = putBdd(orBdd);
+        this.op_cache.insert(hash, bdd1, bdd2, CACHE_OR, ans);
+        return ans;
+    }
+
+    public int imp(int bdd1, int bdd2) {
+        if (bdd1 == 0 || bdd2 == 1) {
+            return 1;
+        }
+        if (bdd1 == 1) {
+            return ref(bdd2);
+        }
+        if (bdd2 == 0) {
+            return not(bdd1);
+        }
+        if (this.op_cache.lookup(bdd1, bdd2, CACHE_IMP)) {
+            if (refCount.get(this.op_cache.answer) > 0) {
+                return ref(this.op_cache.answer);
+            }
+        }
+        int hash = this.op_cache.hash_value;
+        CFLOBDD impBdd = CFLOBDD.imp(bddtable.get(bdd1), bddtable.get(bdd2));
+        int ans = putBdd(impBdd);
+        this.op_cache.insert(hash, bdd1, bdd2, CACHE_IMP, ans);
+        return ans;
+    }
+    public int andTo(int bdd1, int bdd2) {
+        int ans = and(bdd1, bdd2);
+        deref(bdd1);
+        return ans;
+    }
+    public int orTo(int bdd1, int bdd2) {
+        int ans = or(bdd1, bdd2);
+        deref(bdd1);
+        return ans;
+    }
+    public int exists(int bdd, int var) {
+        //TODO: exist cache
+        CFLOBDD existsBdd = CFLOBDD.exists(bddtable.get(bdd), var);
+        return putBdd(existsBdd);
+    }
+    public int satCount(int bdd) {
+        return bddtable.get(bdd).satCount();
+    }
+    public long getMemoryUsage() {
+        //TODO: implement
+        System.err.println("not implemented");
+        return 0;
+    }
+    public void oneSat(int bdd, int[] arr) {
+        int[] ans = bddtable.get(bdd).oneSat();
+        if (arr == null) {
+            arr = ans;
+        } else {
+            for (int i = 0; i < arr.length; i++) {
+                arr[i] = ans[i];
+            }
+        }
+    }
+    public boolean isValid(int bdd) {
+        return bddtable.get(bdd).isValid();
+    }
+
+    public void printDot(String name, int bdd) {
+        System.out.println("printDot: " + name);
+        bddtable.get(bdd).print();
+    }
+    public int nodeCount(int bdd) {
+        return bddtable.get(bdd).nodeCount();
+    }
+    public void save(int bdd, String path) {
+        //TODO: implement
+        System.err.println("not implemented");
+    }
+    public void cleanup() {
+        CFLOBDD.dispose_module();
+    }
+
+    public static void main(String[] args) {
+        BDD bdd = new BDD(10, 100000);
+        int a = bdd.createVar();
+        System.out.printf("a: %d, not a: %d\n", a, bdd.bddtable.get(a).hashCode());
+
+
+        int a1 = bdd.createVar();
+        int b1 = bdd.createVar();
+        int c1 = bdd.createVar();
+        int d1 = bdd.ref(bdd.and(a1, b1));
+        int e1 = bdd.ref(bdd.and(d1, c1));
+
+        int d2 = bdd.ref(bdd.and(b1, c1));
+        int e2 = bdd.ref(bdd.and(d2, a1));
+        System.out.printf("e1: %d, e2: %d\n", e1, e2);
+        System.out.printf("e1: %x, e2: %x\n", bdd.bddtable.get(e1).getRoot(), bdd.bddtable.get(e2).getRoot());
+
+        assert e1 == e2;
+        bdd.cleanup();
+    }
+}
diff --git a/CFLOBDD/matmult_map.cpp b/CFLOBDD/matmult_map.cpp
index 6ae81c5..622c6ba 100644
--- a/CFLOBDD/matmult_map.cpp
+++ b/CFLOBDD/matmult_map.cpp
@@ -57,7 +57,7 @@ void MatMultMapBody::DecrRef()
 	}
 }
 
-unsigned int MatMultMapBody::Hash(unsigned int modsize)
+unsigned int MatMultMapBody::Hash(unsigned long modsize)
 {
 	/*if (modsize == HASHSETBASE)
 		return hashCheck;*/
@@ -184,7 +184,7 @@ std::ostream& operator<< (std::ostream & out, const MatMultMapHandle &r)
 	return(out);
 }
 
-unsigned int MatMultMapHandle::Hash(unsigned int modsize)
+unsigned int MatMultMapHandle::Hash(unsigned long modsize)
 {
 	if (!(mapContents->isCanonical)) {
 		std::cout << "Hash of a non-canonical LinearMapHandle occurred" << std::endl;
diff --git a/CFLOBDD/matmult_map.h b/CFLOBDD/matmult_map.h
index 9bb8660..aec716a 100644
--- a/CFLOBDD/matmult_map.h
+++ b/CFLOBDD/matmult_map.h
@@ -58,7 +58,7 @@ class MatMultMapHandle {
 	bool operator!= (const MatMultMapHandle &r) const;      // Overloaded !=
 	bool operator== (const MatMultMapHandle &r) const;      // Overloaded ==
 	VAL_TYPE& operator[](INT_PAIR& p);                        // Overloaded []
-	unsigned int Hash(unsigned int modsize);
+	unsigned int Hash(unsigned long modsize);
 	void Add(const INT_PAIR& p, VAL_TYPE& v);
 	void ForceAdd(const INT_PAIR& p, VAL_TYPE& v);
 	bool Member(INT_PAIR& p);
@@ -85,13 +85,13 @@ extern std::size_t hash_value(const MatMultMapHandle& val);
 class MatMultMapBody {
 
 	friend void MatMultMapHandle::Canonicalize();
-	friend unsigned int MatMultMapHandle::Hash(unsigned int modsize);
+	friend unsigned int MatMultMapHandle::Hash(unsigned long modsize);
 
 public:
 	MatMultMapBody();    // Constructor
 	void IncrRef();
 	void DecrRef();
-	unsigned int Hash(unsigned int modsize);
+	unsigned int Hash(unsigned long modsize);
 	void setHashCheck();
 	unsigned int refCount;         // reference-count value
 	std::map<INT_PAIR, VAL_TYPE> map;
diff --git a/CFLOBDD/reduction_map.cpp b/CFLOBDD/reduction_map.cpp
index adc2063..d47bb2e 100644
--- a/CFLOBDD/reduction_map.cpp
+++ b/CFLOBDD/reduction_map.cpp
@@ -35,6 +35,7 @@
 #include "list_TPtr.h"
 #include "intpair.h"
 #include "hashset.h"
+#include <cstdint>
 
 //***************************************************************
 // ReductionMapBodyIterator
@@ -74,7 +75,7 @@ void ReductionMapBody::DecrRef()
   }
 }
 
-unsigned int ReductionMapBody::Hash(unsigned int modsize)
+unsigned int ReductionMapBody::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
   /*ReductionMapBodyIterator mi(*this);
@@ -212,7 +213,7 @@ std::ostream& operator<< (std::ostream & out, const ReductionMapHandle &r)
   return(out);
 }
 
-unsigned int ReductionMapHandle::Hash(unsigned int modsize)
+unsigned int ReductionMapHandle::Hash(unsigned long modsize)
 {
   return ((unsigned int) reinterpret_cast<uintptr_t>(mapContents) >> 2) % modsize;
 }
diff --git a/CFLOBDD/reduction_map.h b/CFLOBDD/reduction_map.h
index 5804d4e..160e388 100644
--- a/CFLOBDD/reduction_map.h
+++ b/CFLOBDD/reduction_map.h
@@ -52,7 +52,7 @@ class ReductionMapHandle {
   ReductionMapHandle& operator= (const ReductionMapHandle &r); // Overloaded assignment
   bool operator!= (const ReductionMapHandle &r);      // Overloaded !=
   bool operator== (const ReductionMapHandle &r);      // Overloaded ==
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int Size();
   void AddToEnd(int y);
   int& operator[](unsigned int i);                       // Overloaded []
@@ -81,7 +81,7 @@ class ReductionMapBody {//: public List<int> {
   ReductionMapBody(unsigned int capacity);
   void IncrRef();
   void DecrRef();
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   void setHashCheck();
   void AddToEnd(int y);          // Override AddToEnd
   unsigned int refCount;         // reference-count value
diff --git a/CFLOBDD/ref_ptr.h b/CFLOBDD/ref_ptr.h
index 775e683..b07ed77 100644
--- a/CFLOBDD/ref_ptr.h
+++ b/CFLOBDD/ref_ptr.h
@@ -60,6 +60,11 @@ template< typename T > class ref_ptr {
             acquire( rp.ptr );
         }
 
+        ref_ptr(ref_ptr &&rp) : ptr(rp.ptr) {
+            // no acquire, just move the pointer
+            rp.ptr = nullptr;
+        }
+
         ~ref_ptr() {
             release();
         }
@@ -73,6 +78,16 @@ template< typename T > class ref_ptr {
           return *this;
         }
 
+        ref_ptr& operator=( ref_ptr &&rp ) {
+            if (this != &rp) {
+                // no release
+                release(ptr);
+                ptr = rp.ptr;
+                rp.ptr = nullptr;
+            }
+            return *this;
+        }
+
         inline ref_ptr& operator=( const ref_ptr& rp ) {
             return *this = rp.ptr;
         }
@@ -118,7 +133,7 @@ template< typename T > class ref_ptr {
             if( old_ptr ) {
                 --old_ptr->count;
 #ifdef DBGREFPTR
-                std::cout << "Released " << *old_ptr << " with count = "
+                std::cout << "Released " << old_ptr << " with count = "
                     << old_ptr->count << std::endl;
 #endif
                 if( old_ptr->count == 0 ) {
diff --git a/CFLOBDD/return_map_T.h b/CFLOBDD/return_map_T.h
index bad1596..0d284fa 100644
--- a/CFLOBDD/return_map_T.h
+++ b/CFLOBDD/return_map_T.h
@@ -36,6 +36,7 @@
 #include "reduction_map.h"
 #include "intpair.h"
 #include <complex>
+#include <cstdint>
 //#include <boost/multiprecision/cpp_int.hpp>
 //#include "hash_functions.h"
 
@@ -59,7 +60,7 @@ class ReturnMapHandle {
   bool operator!= (const ReturnMapHandle<T> &r);      // Overloaded !=
   bool operator== (const ReturnMapHandle<T> &r);      // Overloaded ==
   T& operator[](unsigned int i);                       // Overloaded []
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int Size();
   void AddToEnd(T y);
   bool Member(T y);
@@ -87,7 +88,7 @@ template <typename T>
 class ReturnMapBody {
 
   friend void ReturnMapHandle<T>::Canonicalize();
-  friend unsigned int ReturnMapHandle<T>::Hash(unsigned int modsize);
+  friend unsigned int ReturnMapHandle<T>::Hash(unsigned long modsize);
 
  public:
   ReturnMapBody();    // Constructor
@@ -95,7 +96,7 @@ class ReturnMapBody {
   //~ReturnMapBody();
   void IncrRef();
   void DecrRef();
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   void setHashCheck();
   unsigned int refCount;         // reference-count value
   std::vector<T> mapArray;
@@ -286,7 +287,7 @@ std::ostream& operator<< (std::ostream & out, const ReturnMapHandle<T> &r)
 }
 
 template <typename T>
-unsigned int ReturnMapHandle<T>::Hash(unsigned int modsize)
+unsigned int ReturnMapHandle<T>::Hash(unsigned long modsize)
 {
 	if (!(mapContents->isCanonical)) {
 		std::cout << "Hash of a non-canonical ReturnMapHandle occurred" << std::endl;
diff --git a/CFLOBDD/return_map_specializations.cpp b/CFLOBDD/return_map_specializations.cpp
index 3658bec..deaedf6 100644
--- a/CFLOBDD/return_map_specializations.cpp
+++ b/CFLOBDD/return_map_specializations.cpp
@@ -46,7 +46,7 @@ typedef boost::multiprecision::cpp_complex_100 BIG_COMPLEX_FLOAT;
 // Instantiation and specialization of class ReturnMapHandle<LinearMapHandle> ----------
 
 // template<>
-// unsigned int ReturnMapBody<LinearMapHandle>::Hash(unsigned int modsize)
+// unsigned int ReturnMapBody<LinearMapHandle>::Hash(unsigned long modsize)
 // {
 // 	unsigned int hvalue = 0;
 
@@ -73,7 +73,7 @@ void ReturnMapBody<MatMultMapHandle>::setHashCheck()
 }
 
 template<>
-unsigned int ReturnMapBody<MatMultMapHandle>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<MatMultMapHandle>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 
@@ -100,7 +100,7 @@ void ReturnMapBody<WeightedMatMultMapHandle<BIG_FLOAT>>::setHashCheck()
 }
 
 template<>
-unsigned int ReturnMapBody<WeightedMatMultMapHandle<BIG_FLOAT>>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<WeightedMatMultMapHandle<BIG_FLOAT>>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 
@@ -127,7 +127,7 @@ void ReturnMapBody<WeightedMatMultMapHandle<BIG_COMPLEX_FLOAT>>::setHashCheck()
 }
 
 template<>
-unsigned int ReturnMapBody<WeightedMatMultMapHandle<BIG_COMPLEX_FLOAT>>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<WeightedMatMultMapHandle<BIG_COMPLEX_FLOAT>>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 
@@ -154,7 +154,7 @@ void ReturnMapBody<WeightedMatMultMapHandle<fourierSemiring>>::setHashCheck()
 }
 
 template<>
-unsigned int ReturnMapBody<WeightedMatMultMapHandle<fourierSemiring>>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<WeightedMatMultMapHandle<fourierSemiring>>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 
@@ -217,7 +217,7 @@ std::ostream& operator<< (std::ostream & out, const ReturnMapBody<LinearMapHandl
 // Instantiation and specialization of class ReturnMapHandle<int> ---------------------
 
 template<>
-unsigned int ReturnMapBody<int>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<int>::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
 
@@ -274,7 +274,7 @@ CFL_OBDD::CFLOBDDReturnMapHandle CFL_OBDD::CFLOBDDReturnMapHandle::Complement()
 // Instantiation and specialization of class ReturnMapHandle<double> ---------------------
 
 template<>
-unsigned int ReturnMapBody<double>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<double>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 	std::hash<double> double_hash;
@@ -312,7 +312,7 @@ ReturnMapHandle<double> ReturnMapHandle<double>::Complement()
 // double_hash needs to be changed
 
 template<>
-unsigned int ReturnMapBody<BIG_FLOAT>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<BIG_FLOAT>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 	std::hash<BIG_FLOAT> big_float_hash;
@@ -350,7 +350,7 @@ ReturnMapHandle<BIG_FLOAT> ReturnMapHandle<BIG_FLOAT>::Complement()
 // double_hash needs to be changed
 
 template<>
-unsigned int ReturnMapBody<BIG_COMPLEX_FLOAT>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<BIG_COMPLEX_FLOAT>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 	std::hash<BIG_COMPLEX_FLOAT> big_float_hash;
@@ -387,7 +387,7 @@ ReturnMapHandle<BIG_COMPLEX_FLOAT> ReturnMapHandle<BIG_COMPLEX_FLOAT>::Complemen
 // double_hash needs to be changed
 
 // template<>
-// unsigned int ReturnMapBody<GeneralMapHandle>::Hash(unsigned int modsize)
+// unsigned int ReturnMapBody<GeneralMapHandle>::Hash(unsigned long modsize)
 // {
 // 	unsigned int hvalue = 0;
 // 	std::hash<double> double_hash;
@@ -424,7 +424,7 @@ ReturnMapHandle<BIG_COMPLEX_FLOAT> ReturnMapHandle<BIG_COMPLEX_FLOAT>::Complemen
 // Instantiation and specialization of class ReturnMapHandle<intPair> ---------------------
 
 template<>
-unsigned int ReturnMapBody<intpair>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<intpair>::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
 
@@ -465,7 +465,7 @@ ReturnMapHandle<intpair> ReturnMapHandle<intpair>::Complement()
 // Instantiation and specialization of class ReturnMapHandle<fourierSemiring> ---------------------
 
 template<>
-unsigned int ReturnMapBody<fourierSemiring>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<fourierSemiring>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 	boost::hash<BIG_INT> boost_hash;
@@ -524,7 +524,7 @@ std::size_t hash_value(std::complex<double> c)
 */
 
 template<>
-unsigned int ReturnMapBody<std::complex<double>>::Hash(unsigned int modsize)
+unsigned int ReturnMapBody<std::complex<double>>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 
diff --git a/CFLOBDD/tests_cfl.cpp b/CFLOBDD/tests_cfl.cpp
index 2c7d6c8..0834b6c 100644
--- a/CFLOBDD/tests_cfl.cpp
+++ b/CFLOBDD/tests_cfl.cpp
@@ -360,7 +360,22 @@ void CFLTests::testTimes(){
 	K2.PrintYield(&std::cout);
 	std::cout << std::endl;
 }
-
+void CFLTests::test0() {
+	CFLOBDD a, b, c, d, e;
+	a = MkProjection(0, 2);
+	b = MkProjection(1, 2);
+	c = MkProjection(2, 2);
+	d = MkProjection(3, 2);
+	e = MkAnd(MkAnd(a, MkNot(b)), MkAnd(c, MkNot(d)));
+	SH_OBDD::Assignment *assignment = nullptr;
+	e.FindOneSatisfyingAssignment(assignment);
+	
+	bool buffer[4];
+	std::memcpy(buffer, &(assignment->get_data())[(1 << 30) - 4], 4);
+	std::cout << "[" << buffer[0] << " " << buffer[1] << " " << buffer[2] << " " << buffer[3] << "]" << std::endl;
+	e.CountPaths();
+	std::cout << "NumSatisfyingAssignments: " << e.NumSatisfyingAssignments() << std::endl;
+}
 void CFLTests::test1(){
   CFLOBDD F, G, H, I;
   F = MkProjection(3);
@@ -1932,6 +1947,8 @@ bool CFLTests::runTests(const char *arg, int size, int seed, int a){
 	// 	CFLTests::test_restrict_exists_and_forall();
 	// } else if (curTest == "Karatsuba") {			
 	// 	CFLTests::testKaratsuba();
+	} else if (curTest == "Test0") {
+		CFLTests::test0();
 	} else if (curTest == "Test1") {
 		CFLTests::test1();
 	} else if (curTest == "Test2") {
diff --git a/CFLOBDD/tests_cfl.h b/CFLOBDD/tests_cfl.h
index 6bf9728..e7d4c5c 100644
--- a/CFLOBDD/tests_cfl.h
+++ b/CFLOBDD/tests_cfl.h
@@ -30,6 +30,7 @@ class CFLTests
         static void testMkIdRelationInterleaved();
         static void testProbability();
         static void testParity();
+        static void test0();
         static void test1();
         static void test2();
         static void testMaxLevelGreaterThan10();
diff --git a/CFLOBDD/weighted_bdd_node_t.cpp b/CFLOBDD/weighted_bdd_node_t.cpp
index 995e381..c4a61de 100644
--- a/CFLOBDD/weighted_bdd_node_t.cpp
+++ b/CFLOBDD/weighted_bdd_node_t.cpp
@@ -50,7 +50,7 @@ WeightedBDDNodeHandle<T,Op>::~WeightedBDDNodeHandle()
 }
 
 template <typename T, typename Op>
-unsigned int WeightedBDDNodeHandle<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedBDDNodeHandle<T,Op>::Hash(unsigned long modsize)
 {
     return ((unsigned int) reinterpret_cast<uintptr_t>(handleContents) >> 2) % modsize;
 }
@@ -194,7 +194,7 @@ void WeightedBDDInternalNode<T,Op>::DecrRef()
 }
 
 template <typename T, typename Op>
-unsigned int WeightedBDDInternalNode<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedBDDInternalNode<T,Op>::Hash(unsigned long modsize)
 {
     unsigned int l_hvalue = leftNode.Hash(modsize);
     unsigned int r_hvalue = rightNode.Hash(modsize);
@@ -312,7 +312,7 @@ void WeightedBDDLeafNode<T,Op>::DecrRef()
 }
 
 template <typename T, typename Op>
-unsigned int WeightedBDDLeafNode<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedBDDLeafNode<T,Op>::Hash(unsigned long modsize)
 {
     boost::hash<T> boost_hash;
     return ((117 * boost_hash(value) + 1) % modsize);
diff --git a/CFLOBDD/weighted_bdd_node_t.h b/CFLOBDD/weighted_bdd_node_t.h
index c1a32da..57b1a28 100644
--- a/CFLOBDD/weighted_bdd_node_t.h
+++ b/CFLOBDD/weighted_bdd_node_t.h
@@ -20,7 +20,7 @@ namespace CFL_OBDD {
             WeightedBDDNodeHandle(WeightedBDDNode<T,Op> *n);
             WeightedBDDNodeHandle(const WeightedBDDNodeHandle<T,Op> &n);
             ~WeightedBDDNodeHandle();
-            unsigned int Hash(unsigned int modsize);
+            unsigned int Hash(unsigned long modsize);
             bool operator!= (const WeightedBDDNodeHandle &nh);
             bool operator== (const WeightedBDDNodeHandle &nh) const;
             WeightedBDDNodeHandle<T,Op>& operator= (const WeightedBDDNodeHandle &nh);
@@ -69,7 +69,7 @@ namespace CFL_OBDD {
             const bool IsCanonical() const { return isCanonical; }
             void SetCanonical() { isCanonical = true;  }
             virtual std::ostream& print(std::ostream &out = std::cout) const = 0;
-            virtual unsigned int Hash(unsigned int modsize) = 0;
+            virtual unsigned int Hash(unsigned long modsize) = 0;
             virtual void ComputeWeightOfPathsAsAmpsToExits(Hashset<WeightedBDDNodeHandle<T,Op>>* visitedNodes);
             long double weightOfPathsAsAmpsToExit;
             protected:
@@ -98,7 +98,7 @@ namespace CFL_OBDD {
             long double leftWeightOfPathsAsAmpsToExit;
             long double rightWeightOfPathsAsAmpsToExit;
 
-            unsigned int Hash(unsigned int modsize);
+            unsigned int Hash(unsigned long modsize);
             void ComputeWeightOfPathsAsAmpsToExits(Hashset<WeightedBDDNodeHandle<T,Op>>* visitedNodes);
 
             private:
@@ -119,7 +119,7 @@ namespace CFL_OBDD {
             BDD_NODEKIND NodeKind() const { return LEAF; }
             std::ostream& print(std::ostream &out = std::cout) const;
             T value;
-            unsigned int Hash(unsigned int modsize);
+            unsigned int Hash(unsigned long modsize);
             void ComputeWeightOfPathsAsAmpsToExits(Hashset<WeightedBDDNodeHandle<T,Op>>* visitedNodes);
     };
 }
diff --git a/CFLOBDD/weighted_cflobdd_node_t.cpp b/CFLOBDD/weighted_cflobdd_node_t.cpp
index 37776ec..61e8aab 100644
--- a/CFLOBDD/weighted_cflobdd_node_t.cpp
+++ b/CFLOBDD/weighted_cflobdd_node_t.cpp
@@ -390,7 +390,7 @@ WeightedCFLOBDDNodeHandleT<T,Op>::~WeightedCFLOBDDNodeHandleT()
 
 // Hash
 template <typename T, typename Op>
-unsigned int WeightedCFLOBDDNodeHandleT<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedCFLOBDDNodeHandleT<T,Op>::Hash(unsigned long modsize)
 {
   return ((unsigned int) reinterpret_cast<uintptr_t>(handleContents) >> 2) % modsize;
 }
@@ -1399,7 +1399,7 @@ WeightedCFLReduceKey<T,Op>::WeightedCFLReduceKey(WeightedCFLOBDDNodeHandleT<T,Op
 
 // Hash
 template <typename T, typename Op>
-unsigned int WeightedCFLReduceKey<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedCFLReduceKey<T,Op>::Hash(unsigned long modsize)
 {
   unsigned int hvalue = 0;
   hvalue = (997 * nodeHandle.Hash(modsize) + 97 * redMapHandle.Hash(modsize) + valList.Hash(modsize)) % modsize;
@@ -1775,7 +1775,7 @@ std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> WeightedCFLOBDDInternalNode<T,Op>:
 } // CFLOBDDInternalNode::Reduce
 
 template <typename T, typename Op>
-unsigned int WeightedCFLOBDDInternalNode<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedCFLOBDDInternalNode<T,Op>::Hash(unsigned long modsize)
 {
   unsigned int hvalue = AConnection.Hash(modsize);
   for (unsigned int j = 0; j < numBConnections; j++) {
@@ -2274,7 +2274,7 @@ std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> WeightedCFLOBDDForkNode<T,Op>::Red
 }
 
 template <typename T, typename Op>
-unsigned int WeightedCFLOBDDForkNode<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedCFLOBDDForkNode<T,Op>::Hash(unsigned long modsize)
 {
     boost::hash<T> boost_hash;
     return (997 * boost_hash(this->lweight) + 97 * boost_hash(this->rweight) + 2) % modsize; 
@@ -2399,7 +2399,7 @@ std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> WeightedCFLOBDDDontCareNode<T,Op>:
 }
 
 template <typename T, typename Op>
-unsigned int WeightedCFLOBDDDontCareNode<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedCFLOBDDDontCareNode<T,Op>::Hash(unsigned long modsize)
 {
     boost::hash<T> boost_hash;
     return (997 * boost_hash(this->lweight) + 97 * boost_hash(this->rweight) + 1) % modsize;
@@ -2620,7 +2620,7 @@ void WeightedBDDTopNode<T,Op>::DecrRef()
 }
 
 template <typename T, typename Op>
-unsigned int WeightedBDDTopNode<T,Op>::Hash(unsigned int modsize)
+unsigned int WeightedBDDTopNode<T,Op>::Hash(unsigned long modsize)
 {
   return (117 * bddContents.Hash(modsize) + 1) % modsize;
 }
diff --git a/CFLOBDD/weighted_cflobdd_node_t.h b/CFLOBDD/weighted_cflobdd_node_t.h
index 3034f92..2a47da2 100644
--- a/CFLOBDD/weighted_cflobdd_node_t.h
+++ b/CFLOBDD/weighted_cflobdd_node_t.h
@@ -73,7 +73,7 @@ class WeightedCFLOBDDNodeHandleT {
   WeightedCFLOBDDNodeHandleT(WeightedCFLOBDDNode<T,Op> *n);                          // Constructor
   WeightedCFLOBDDNodeHandleT(const WeightedCFLOBDDNodeHandleT<T,Op> &nh);              // Copy constructor
   ~WeightedCFLOBDDNodeHandleT();                                       // Destructor
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const WeightedCFLOBDDNodeHandleT &nh);              // Overloaded !=
   bool operator== (const WeightedCFLOBDDNodeHandleT &nh) const;              // Overloaded ==
   WeightedCFLOBDDNodeHandleT<T,Op> & operator= (const WeightedCFLOBDDNodeHandleT<T,Op> &nh); // assignment
@@ -169,7 +169,7 @@ namespace CFL_OBDD {
 
 	public:
 		WeightedCFLReduceKey(WeightedCFLOBDDNodeHandleT<T, Op> nodeHandle, ReductionMapHandle redMap, WeightedValuesListHandle<T> valList ); // Constructor
-		unsigned int Hash(unsigned int modsize);
+		unsigned int Hash(unsigned long modsize);
 		WeightedCFLReduceKey& operator= (const WeightedCFLReduceKey& p);  // Overloaded assignment
 		bool operator!= (const WeightedCFLReduceKey& p);        // Overloaded !=
 		bool operator== (const WeightedCFLReduceKey& p);        // Overloaded ==
@@ -224,7 +224,7 @@ class WeightedCFLOBDDNode {
   virtual void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index) = 0;
   virtual int Traverse(SH_OBDD::AssignmentIterator &ai) = 0;
   virtual std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, WeightedValuesListHandle<T>& valList, bool forceReduce = false) = 0;
-  virtual unsigned int Hash(unsigned int modsize) = 0;
+  virtual unsigned int Hash(unsigned long modsize) = 0;
   virtual void DumpConnections(Hashset<WeightedCFLOBDDNodeHandleT<T,Op>> *visited, std::ostream & out = std::cout) = 0;
   virtual void CountNodesAndEdges(Hashset<WeightedCFLOBDDNodeHandleT<T,Op>> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
         unsigned int &nodeCount, unsigned int &edgeCount, unsigned int &returnEdgesCount) = 0;
@@ -277,7 +277,7 @@ class WeightedCFLOBDDInternalNode : public WeightedCFLOBDDNode<T,Op> {
   void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index);
   int Traverse(SH_OBDD::AssignmentIterator &ai);
   std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, WeightedValuesListHandle<T>& valList, bool forceReduce = false);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   void DumpConnections(Hashset<WeightedCFLOBDDNodeHandleT<T,Op>> *visited, std::ostream & out = std::cout);
   void CountNodesAndEdges(Hashset<WeightedCFLOBDDNodeHandleT<T,Op>> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
 	  unsigned int &nodeCount, unsigned int &edgeCount, unsigned int& returnEdgesCount);
@@ -324,7 +324,7 @@ class WeightedCFLOBDDLeafNode : public WeightedCFLOBDDNode<T,Op> {
   virtual void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index) = 0;
   virtual int Traverse(SH_OBDD::AssignmentIterator &ai) = 0;
   virtual std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, WeightedValuesListHandle<T>& valList, bool forceReduce = false) = 0;
-  virtual unsigned int Hash(unsigned int modsize) = 0;
+  virtual unsigned int Hash(unsigned long modsize) = 0;
   void DumpConnections(Hashset<WeightedCFLOBDDNodeHandleT<T,Op>> *visited, std::ostream & out = std::cout);
   void CountNodesAndEdges(Hashset<WeightedCFLOBDDNodeHandleT<T,Op>> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
 	  unsigned int &nodeCount, unsigned int &edgeCount, unsigned int& returnEdgesCount);
@@ -358,7 +358,7 @@ class WeightedCFLOBDDForkNode : public WeightedCFLOBDDLeafNode<T,Op> {
   void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index);
   int Traverse(SH_OBDD::AssignmentIterator &ai);
   std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, WeightedValuesListHandle<T>& valList, bool forceReduce = false);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const WeightedCFLOBDDNode<T,Op> & n);        // Overloaded !=
   bool operator== (const WeightedCFLOBDDNode<T,Op> & n);        // Overloaded ==
   void InstallWeightsOfPathsAsAmpsToExits(); 
@@ -386,7 +386,7 @@ class WeightedCFLOBDDDontCareNode : public WeightedCFLOBDDLeafNode<T,Op> {
   void FillSatisfyingAssignment(unsigned int i, SH_OBDD::Assignment &assignment, unsigned int &index);
   int Traverse(SH_OBDD::AssignmentIterator &ai);
   std::pair<WeightedCFLOBDDNodeHandleT<T,Op>,T> Reduce(ReductionMapHandle& redMapHandle, unsigned int replacementNumExits, WeightedValuesListHandle<T>& valList, bool forceReduce = false);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const WeightedCFLOBDDNode<T,Op> & n);        // Overloaded !=
   bool operator== (const WeightedCFLOBDDNode<T,Op> & n);        // Overloaded ==
   void InstallWeightsOfPathsAsAmpsToExits();
@@ -408,7 +408,7 @@ class WeightedBDDTopNode : public WeightedCFLOBDDNode<T,Op> {
     WCFLOBDD_NODEKIND NodeKind() const { return W_BDD_TOPNODE; }
     bool operator!= (const WeightedCFLOBDDNode<T,Op> &n);
     bool operator== (const WeightedCFLOBDDNode<T,Op> &n);
-    unsigned int Hash(unsigned int modsize);
+    unsigned int Hash(unsigned long modsize);
     void IncrRef();
     void DecrRef();
     WeightedBDDNodeHandle<T, Op> bddContents;
diff --git a/CFLOBDD/weighted_cflobdd_t.h b/CFLOBDD/weighted_cflobdd_t.h
index 68c91b3..ec58a48 100644
--- a/CFLOBDD/weighted_cflobdd_t.h
+++ b/CFLOBDD/weighted_cflobdd_t.h
@@ -35,12 +35,12 @@ class WEIGHTED_CFLOBDD_T {
 //   void PrintYield(std::ostream * out);               // print the yield of the "tree"
 //   bool IsValid();									// check if the CFLOBDD is valid (satisying all structural invariants)
 #ifdef PATH_COUNTING_ENABLED
-  unsigned int NumSatisfyingAssignments();      // Return number of satisfying assignments
+//   unsigned int NumSatisfyingAssignments();      // Return number of satisfying assignments
  // mpz_class NumSatisfyingAssignments();      // Return number of satisfying assignments
 #endif
   bool FindOneSatisfyingAssignment(SH_OBDD::Assignment * &assignment);
                                                 // Find a satisfying assignment
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   bool operator!= (const WEIGHTED_CFLOBDD_T & C) const;          // Overloaded !=
   bool operator== (const WEIGHTED_CFLOBDD_T & C) const;          // Overloaded ==
   WEIGHTED_CFLOBDD_T& operator= (const WEIGHTED_CFLOBDD_T &c);       // assignment
@@ -133,11 +133,11 @@ bool WEIGHTED_CFLOBDD_T<T, Op>::Evaluate(SH_OBDD::Assignment &assignment)
 //
 // Running time: Linear in the size of the CFLOBDD
 //
-template <typename T, typename Op>
-unsigned int CFLOBDD_T<T, Op>::NumSatisfyingAssignments()
-{
-	return root->NumSatisfyingAssignments();
-}
+// template <typename T, typename Op>
+// unsigned int WEIGHTED_CFLOBDD_T<T, Op>::NumSatisfyingAssignments()
+// {
+// 	return root->NumSatisfyingAssignments();
+// }
 #endif
 
 // FindOneSatisfyingAssignment
@@ -156,7 +156,7 @@ bool WEIGHTED_CFLOBDD_T<T, Op>::FindOneSatisfyingAssignment(SH_OBDD::Assignment
 
 // Hash
 template <typename T, typename Op>
-unsigned int WEIGHTED_CFLOBDD_T<T, Op>::Hash(unsigned int modsize)
+unsigned int WEIGHTED_CFLOBDD_T<T, Op>::Hash(unsigned long modsize)
 {
 	return root->Hash(modsize);
 }
diff --git a/CFLOBDD/weighted_cflobdd_top_node_t.cpp b/CFLOBDD/weighted_cflobdd_top_node_t.cpp
index 963ce81..d40ae57 100644
--- a/CFLOBDD/weighted_cflobdd_top_node_t.cpp
+++ b/CFLOBDD/weighted_cflobdd_top_node_t.cpp
@@ -295,7 +295,7 @@ namespace CFL_OBDD {
 
     // Hash
     template <typename T, typename Op>
-    unsigned int WeightedCFLOBDDTopNodeT<T, Op>::Hash(unsigned int modsize)
+    unsigned int WeightedCFLOBDDTopNodeT<T, Op>::Hash(unsigned long modsize)
     {
         return rootConnection.Hash(modsize);
     }
diff --git a/CFLOBDD/weighted_cflobdd_top_node_t.h b/CFLOBDD/weighted_cflobdd_top_node_t.h
index 54fe104..29259d7 100644
--- a/CFLOBDD/weighted_cflobdd_top_node_t.h
+++ b/CFLOBDD/weighted_cflobdd_top_node_t.h
@@ -34,11 +34,11 @@ class WeightedCFLOBDDTopNodeT {
 //   void PrintYieldSemantic(std::ostream & out);       // print the yield of the "tree"
 //   bool IsValid();				// check if the CFLOBDD is valid (satisfies structural invariants)
 #ifdef PATH_COUNTING_ENABLED
-  unsigned int NumSatisfyingAssignments();
+//   unsigned int NumSatisfyingAssignments();
   //mpz_class NumSatisfyingAssignments();
 #endif
   bool FindOneSatisfyingAssignment(SH_OBDD::Assignment * &assignment);
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   void DumpConnections(Hashset<WeightedCFLOBDDNodeHandleT<T, Op>> *visited, std::ostream & out = std::cout);
   void CountNodesAndEdges(Hashset<WeightedCFLOBDDNodeHandleT<T, Op>> *visitedNodes, Hashset<CFLOBDDReturnMapBody> *visitedEdges, 
 	  unsigned int &nodeCount, unsigned int &edgeCount, unsigned int& returnEdgesCount, unsigned int &returnEdgesObjCount);
diff --git a/CFLOBDD/weighted_connectionT.cpp b/CFLOBDD/weighted_connectionT.cpp
index 2cdbec9..fc9bbd2 100644
--- a/CFLOBDD/weighted_connectionT.cpp
+++ b/CFLOBDD/weighted_connectionT.cpp
@@ -35,7 +35,7 @@ WConnection<T, Op>::~WConnection()
 
 // Hash
 template <typename T, typename Op>
-unsigned int WConnection<T, Op>::Hash(unsigned int modsize)
+unsigned int WConnection<T, Op>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
 	hvalue = (997 * returnMapHandle.Hash(modsize) + entryPointHandle->Hash(modsize)) % modsize;
diff --git a/CFLOBDD/weighted_connectionT.h b/CFLOBDD/weighted_connectionT.h
index c0d8a09..163b64a 100644
--- a/CFLOBDD/weighted_connectionT.h
+++ b/CFLOBDD/weighted_connectionT.h
@@ -35,7 +35,7 @@ namespace CFL_OBDD {
 		WConnection(WeightedCFLOBDDNodeHandleT<T, Op> &entryPointHandle, CFLOBDDReturnMapHandle &returnMapHandle);
 		~WConnection();                                 // Destructor
 
-		unsigned int Hash(unsigned int modsize);
+		unsigned int Hash(unsigned long modsize);
 		WConnection& operator= (const WConnection &C);   // Overloaded =
 		bool operator!= (const WConnection & C);        // Overloaded !=
 		bool operator== (const WConnection & C);        // Overloaded ==
diff --git a/CFLOBDD/weighted_cross_product.cpp b/CFLOBDD/weighted_cross_product.cpp
index 0297531..fdc20bb 100644
--- a/CFLOBDD/weighted_cross_product.cpp
+++ b/CFLOBDD/weighted_cross_product.cpp
@@ -57,7 +57,7 @@ namespace CFL_OBDD {
     }
 
     template <typename T>
-    unsigned int WeightedPairProductMapBody<T>::Hash(unsigned int modsize)
+    unsigned int WeightedPairProductMapBody<T>::Hash(unsigned long modsize)
     {
         unsigned int hvalue = 0;
 
@@ -210,7 +210,7 @@ namespace CFL_OBDD {
     }
 
     template <typename T>
-    unsigned int WeightedPairProductMapHandle<T>::Hash(unsigned int modsize)
+    unsigned int WeightedPairProductMapHandle<T>::Hash(unsigned long modsize)
     {
         return ((unsigned int) reinterpret_cast<uintptr_t>(mapContents) >> 2) % modsize;
     }
@@ -312,7 +312,7 @@ namespace CFL_OBDD {
 
     // Hash
     template <typename T, typename Op>
-    unsigned int WeightedPairProductKey<T,Op>::Hash(unsigned int modsize)
+    unsigned int WeightedPairProductKey<T,Op>::Hash(unsigned long modsize)
     {
         unsigned int hvalue = 0;
         boost::hash<T> boost_hash;
diff --git a/CFLOBDD/weighted_cross_product.h b/CFLOBDD/weighted_cross_product.h
index 24e70c5..5bfabba 100644
--- a/CFLOBDD/weighted_cross_product.h
+++ b/CFLOBDD/weighted_cross_product.h
@@ -34,7 +34,7 @@ class WeightedPairProductMapHandle {
   WeightedPairProductMapHandle& operator= (const WeightedPairProductMapHandle<T> &r); // Overloaded assignment
   bool operator!= (const WeightedPairProductMapHandle<T> &r);      // Overloaded !=
   bool operator== (const WeightedPairProductMapHandle<T> &r);      // Overloaded ==
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int Size();
   std::pair<intpair, Pair_T<T,T>> operator[](unsigned int i);                       // Overloaded []
   void AddToEnd(const intpair& p, const Pair_T<T,T>& v);
@@ -59,7 +59,7 @@ class WeightedPairProductMapBody {//: public List<intpair> {
   WeightedPairProductMapBody();    // Constructor
   void IncrRef();
   void DecrRef();
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int refCount;         // reference-count value
   void setHashCheck();
   void AddToEnd(const intpair& y, const Pair_T<T,T>& v);          // Override AddToEnd
@@ -91,7 +91,7 @@ class WeightedPairProductKey {
  public:
   WeightedPairProductKey(WeightedCFLOBDDNodeHandleT<T,Op> nodeHandle1, WeightedCFLOBDDNodeHandleT<T,Op> nodeHandle2); // Constructor
   WeightedPairProductKey(WeightedCFLOBDDNodeHandleT<T,Op> nodeHandle1, WeightedCFLOBDDNodeHandleT<T,Op> nodeHandle2, T factor1, T factor2); // Constructor
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   WeightedPairProductKey& operator= (const WeightedPairProductKey& p);  // Overloaded assignment
   bool operator!= (const WeightedPairProductKey& p);        // Overloaded !=
   bool operator== (const WeightedPairProductKey& p);        // Overloaded ==
diff --git a/CFLOBDD/weighted_cross_product_bdd.cpp b/CFLOBDD/weighted_cross_product_bdd.cpp
index 93c6a1a..84de325 100644
--- a/CFLOBDD/weighted_cross_product_bdd.cpp
+++ b/CFLOBDD/weighted_cross_product_bdd.cpp
@@ -60,7 +60,7 @@ namespace CFL_OBDD {
     }
 
     template <typename T>
-    unsigned int WeightedBDDPairProductMapBody<T>::Hash(unsigned int modsize)
+    unsigned int WeightedBDDPairProductMapBody<T>::Hash(unsigned long modsize)
     {
         unsigned int hvalue = 0;
         boost::hash<T> boost_hash;
@@ -215,7 +215,7 @@ namespace CFL_OBDD {
     }
 
     template <typename T>
-    unsigned int WeightedBDDPairProductMapHandle<T>::Hash(unsigned int modsize)
+    unsigned int WeightedBDDPairProductMapHandle<T>::Hash(unsigned long modsize)
     {
         return ((unsigned int) reinterpret_cast<uintptr_t>(mapContents) >> 2) % modsize;
     }
@@ -317,7 +317,7 @@ namespace CFL_OBDD {
 
     // Hash
     template <typename T, typename Op>
-    unsigned int WeightedBDDPairProductKey<T,Op>::Hash(unsigned int modsize)
+    unsigned int WeightedBDDPairProductKey<T,Op>::Hash(unsigned long modsize)
     {
         unsigned int hvalue = 0;
         boost::hash<T> boost_hash;
diff --git a/CFLOBDD/weighted_cross_product_bdd.h b/CFLOBDD/weighted_cross_product_bdd.h
index f3346d9..b59514e 100644
--- a/CFLOBDD/weighted_cross_product_bdd.h
+++ b/CFLOBDD/weighted_cross_product_bdd.h
@@ -34,7 +34,7 @@ class WeightedBDDPairProductMapHandle {
   WeightedBDDPairProductMapHandle& operator= (const WeightedBDDPairProductMapHandle<T> &r); // Overloaded assignment
   bool operator!= (const WeightedBDDPairProductMapHandle<T> &r);      // Overloaded !=
   bool operator== (const WeightedBDDPairProductMapHandle<T> &r);      // Overloaded ==
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int Size();
   // std::pair<intpair, Pair_T<T,T>> operator[](unsigned int i);                       // Overloaded []
   void AddToEnd(const std::vector<T>& p, const T v);
@@ -59,7 +59,7 @@ class WeightedBDDPairProductMapBody {//: public List<intpair> {
   WeightedBDDPairProductMapBody();    // Constructor
   void IncrRef();
   void DecrRef();
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int refCount;         // reference-count value
   void setHashCheck();
   void AddToEnd(const std::vector<T>& y, const T v);          // Override AddToEnd
@@ -91,7 +91,7 @@ class WeightedBDDPairProductKey {
  public:
   WeightedBDDPairProductKey(WeightedBDDNodeHandle<T,Op> nodeHandle1, WeightedBDDNodeHandle<T,Op> nodeHandle2); // Constructor
   WeightedBDDPairProductKey(WeightedBDDNodeHandle<T,Op> nodeHandle1, WeightedBDDNodeHandle<T,Op> nodeHandle2, T factor1, T factor2); // Constructor
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   WeightedBDDPairProductKey& operator= (const WeightedBDDPairProductKey& p);  // Overloaded assignment
   bool operator!= (const WeightedBDDPairProductKey& p);        // Overloaded !=
   bool operator== (const WeightedBDDPairProductKey& p);        // Overloaded ==
diff --git a/CFLOBDD/weighted_matmult_map.cpp b/CFLOBDD/weighted_matmult_map.cpp
index 2cb545f..7130c02 100644
--- a/CFLOBDD/weighted_matmult_map.cpp
+++ b/CFLOBDD/weighted_matmult_map.cpp
@@ -37,7 +37,7 @@ void WeightedMatMultMapBody<T>::DecrRef()
 }
 
 template <typename T>
-unsigned int WeightedMatMultMapBody<T>::Hash(unsigned int modsize)
+unsigned int WeightedMatMultMapBody<T>::Hash(unsigned long modsize)
 {
 	/*if (modsize == HASHSETBASE)
 		return hashCheck;*/
@@ -51,7 +51,7 @@ unsigned int WeightedMatMultMapBody<T>::Hash(unsigned int modsize)
 }
 
 template <>
-unsigned int WeightedMatMultMapBody<BIG_COMPLEX_FLOAT>::Hash(unsigned int modsize)
+unsigned int WeightedMatMultMapBody<BIG_COMPLEX_FLOAT>::Hash(unsigned long modsize)
 {
 	/*if (modsize == HASHSETBASE)
 		return hashCheck;*/
@@ -65,7 +65,7 @@ unsigned int WeightedMatMultMapBody<BIG_COMPLEX_FLOAT>::Hash(unsigned int modsiz
 }
 
 template <>
-unsigned int WeightedMatMultMapBody<fourierSemiring>::Hash(unsigned int modsize)
+unsigned int WeightedMatMultMapBody<fourierSemiring>::Hash(unsigned long modsize)
 {
 	/*if (modsize == HASHSETBASE)
 		return hashCheck;*/
@@ -247,7 +247,7 @@ std::ostream& operator<< (std::ostream & out, const WeightedMatMultMapHandle<T>
 }
 
 template <typename T>
-unsigned int WeightedMatMultMapHandle<T>::Hash(unsigned int modsize)
+unsigned int WeightedMatMultMapHandle<T>::Hash(unsigned long modsize)
 {
 	if (!(mapContents->isCanonical)) {
 		std::cout << "Hash of a non-canonical LinearMapHandle occurred" << std::endl;
diff --git a/CFLOBDD/weighted_matmult_map.h b/CFLOBDD/weighted_matmult_map.h
index 204d88f..0fa7a05 100644
--- a/CFLOBDD/weighted_matmult_map.h
+++ b/CFLOBDD/weighted_matmult_map.h
@@ -38,7 +38,7 @@ class WeightedMatMultMapHandle {
 	bool operator!= (const WeightedMatMultMapHandle<T> &r) const;      // Overloaded !=
 	bool operator== (const WeightedMatMultMapHandle<T> &r) const;      // Overloaded ==
 	T& operator[](INT_PAIR& p);                        // Overloaded []
-	unsigned int Hash(unsigned int modsize);
+	unsigned int Hash(unsigned long modsize);
 	void Add(const INT_PAIR& p, T& v);
 	void ForceAdd(const INT_PAIR& p, T& v);
 	bool Member(INT_PAIR& p);
@@ -78,13 +78,13 @@ template <typename T>
 class WeightedMatMultMapBody {
 
 	friend void WeightedMatMultMapHandle<T>::Canonicalize();
-	friend unsigned int WeightedMatMultMapHandle<T>::Hash(unsigned int modsize);
+	friend unsigned int WeightedMatMultMapHandle<T>::Hash(unsigned long modsize);
 
 public:
 	WeightedMatMultMapBody();    // Constructor
 	void IncrRef();
 	void DecrRef();
-	unsigned int Hash(unsigned int modsize);
+	unsigned int Hash(unsigned long modsize);
 	void setHashCheck();
 	unsigned int refCount;         // reference-count value
 	std::map<INT_PAIR, T> map;
diff --git a/CFLOBDD/weighted_rootConnectionT.cpp b/CFLOBDD/weighted_rootConnectionT.cpp
index f63f66d..d1473c5 100644
--- a/CFLOBDD/weighted_rootConnectionT.cpp
+++ b/CFLOBDD/weighted_rootConnectionT.cpp
@@ -35,7 +35,7 @@ WRootConnection<Handle, T, Op>::~WRootConnection()
 
 // Hash
 template <typename Handle, typename T, typename Op>
-unsigned int WRootConnection<Handle, T, Op>::Hash(unsigned int modsize)
+unsigned int WRootConnection<Handle, T, Op>::Hash(unsigned long modsize)
 {
 	unsigned int hvalue = 0;
     boost::hash<T> boost_hash;
diff --git a/CFLOBDD/weighted_rootConnectionT.h b/CFLOBDD/weighted_rootConnectionT.h
index cdffac1..99b25e8 100644
--- a/CFLOBDD/weighted_rootConnectionT.h
+++ b/CFLOBDD/weighted_rootConnectionT.h
@@ -35,7 +35,7 @@ namespace CFL_OBDD {
 		WRootConnection(WeightedCFLOBDDNodeHandleT<T, Op> &entryPointHandle, Handle &returnMapHandle, T factor = 1);
 		~WRootConnection();                                 // Destructor
 
-		unsigned int Hash(unsigned int modsize);
+		unsigned int Hash(unsigned long modsize);
 		WRootConnection& operator= (const WRootConnection &C);   // Overloaded =
 		bool operator!= (const WRootConnection & C);        // Overloaded !=
 		bool operator== (const WRootConnection & C);        // Overloaded ==
diff --git a/CFLOBDD/weighted_values_list.cpp b/CFLOBDD/weighted_values_list.cpp
index d5fa212..a4c8cf8 100644
--- a/CFLOBDD/weighted_values_list.cpp
+++ b/CFLOBDD/weighted_values_list.cpp
@@ -53,7 +53,7 @@ void WeightedValuesListBody<T>::DecrRef()
 }
 
 template <typename T>
-unsigned int WeightedValuesListBody<T>::Hash(unsigned int modsize)
+unsigned int WeightedValuesListBody<T>::Hash(unsigned long modsize)
 {
   boost::hash<T> boost_hash;
   unsigned int hvalue = 0;
@@ -235,7 +235,7 @@ std::ostream& operator<< (std::ostream & out, const WeightedValuesListHandle<T>
 }
 
 template <typename T>
-unsigned int WeightedValuesListHandle<T>::Hash(unsigned int modsize)
+unsigned int WeightedValuesListHandle<T>::Hash(unsigned long modsize)
 {
   return ((unsigned int) reinterpret_cast<uintptr_t>(mapContents) >> 2) % modsize;
 }
diff --git a/CFLOBDD/weighted_values_list.h b/CFLOBDD/weighted_values_list.h
index 729e37f..a324e73 100644
--- a/CFLOBDD/weighted_values_list.h
+++ b/CFLOBDD/weighted_values_list.h
@@ -30,7 +30,7 @@ class WeightedValuesListHandle {
   WeightedValuesListHandle& operator= (const WeightedValuesListHandle &r); // Overloaded assignment
   bool operator!= (const WeightedValuesListHandle &r);      // Overloaded !=
   bool operator== (const WeightedValuesListHandle &r);      // Overloaded ==
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   unsigned int Size();
   void AddToEnd(T y);
   T& operator[](unsigned int i);                       // Overloaded []
@@ -61,7 +61,7 @@ class WeightedValuesListBody {//: public List<int> {
   WeightedValuesListBody(unsigned int capacity);
   void IncrRef();
   void DecrRef();
-  unsigned int Hash(unsigned int modsize);
+  unsigned int Hash(unsigned long modsize);
   void setHashCheck();
   void AddToEnd(T y);          // Override AddToEnd
   unsigned int refCount;         // reference-count value
diff --git a/CFLOBDD/zero_indices_map.cpp b/CFLOBDD/zero_indices_map.cpp
index 24a781d..f6a9617 100644
--- a/CFLOBDD/zero_indices_map.cpp
+++ b/CFLOBDD/zero_indices_map.cpp
@@ -27,6 +27,7 @@
 #include <iostream>
 #include <fstream>
 #include <cassert>
+#include <cstdint>
 #include "zero_indices_map.h"
 
 //***************************************************************
@@ -55,7 +56,7 @@ void ZeroIndicesMapBody::DecrRef()
 	}
 }
 
-unsigned int ZeroIndicesMapBody::Hash(unsigned int modsize)
+unsigned int ZeroIndicesMapBody::Hash(unsigned long modsize)
 {
 	/*if (modsize == HASHSETBASE)
 	return hashCheck;*/
@@ -192,7 +193,7 @@ std::ostream& operator<< (std::ostream & out, const ZeroIndicesMapHandle &r)
 	return(out);
 }
 
-unsigned int ZeroIndicesMapHandle::Hash(unsigned int modsize)
+unsigned int ZeroIndicesMapHandle::Hash(unsigned long modsize)
 {
 	if (!(mapContents->isCanonical)) {
 		std::cout << "Hash of a non-canonical LinearMapHandle occurred" << std::endl;
diff --git a/CFLOBDD/zero_indices_map.h b/CFLOBDD/zero_indices_map.h
index a338e4e..f699289 100644
--- a/CFLOBDD/zero_indices_map.h
+++ b/CFLOBDD/zero_indices_map.h
@@ -50,7 +50,7 @@ class ZeroIndicesMapHandle {
 	bool operator!= (const ZeroIndicesMapHandle &r) const;      // Overloaded !=
 	bool operator== (const ZeroIndicesMapHandle &r) const;      // Overloaded ==
 	int operator[](int i);                        // Overloaded []
-	unsigned int Hash(unsigned int modsize);
+	unsigned int Hash(unsigned long modsize);
 	void Add_BIndex(const int i);
 	bool Member(int i);
 	int Lookup(int x);
@@ -73,13 +73,13 @@ extern std::size_t hash_value(const ZeroIndicesMapHandle& val);
 class ZeroIndicesMapBody {
 
 	friend void ZeroIndicesMapHandle::Canonicalize();
-	friend unsigned int ZeroIndicesMapHandle::Hash(unsigned int modsize);
+	friend unsigned int ZeroIndicesMapHandle::Hash(unsigned long modsize);
 
 public:
 	ZeroIndicesMapBody();    // Constructor
 	void IncrRef();
 	void DecrRef();
-	unsigned int Hash(unsigned int modsize);
+	unsigned int Hash(unsigned long modsize);
 	void setHashCheck();
 	unsigned int refCount;         // reference-count value
 	std::vector<int> b_indices;
diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 0000000..38943c7
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,58 @@
+cmake_minimum_required(VERSION 3.12)
+project(cflobdd)
+
+# Set the C++ standard to 17, as specified in the compile command
+set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+
+# Add compiler flags: -g for debugging and -w to suppress warnings
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g -w")
+
+# Define the main source directory
+set(CFLOBDD_DIR ${CMAKE_CURRENT_SOURCE_DIR}/CFLOBDD)
+
+# Add include directories.
+# The user can specify the Boost path via CMAKE_PREFIX_PATH or by setting BOOST_ROOT.
+find_package(Boost REQUIRED CONFIG)
+include_directories(
+    ${CFLOBDD_DIR}
+    ${Boost_INCLUDE_DIRS}
+    ${CFLOBDD_DIR}/Solver/uwr/bit_vector
+    ${CFLOBDD_DIR}/Solver/uwr/assert
+    ${CFLOBDD_DIR}/Solver/uwr/matrix
+    ${CFLOBDD_DIR}/Solver/uwr/parsing
+)
+
+# Gather the source files.
+file(GLOB SOURCES
+    "${CFLOBDD_DIR}/*.cpp"
+    "${CFLOBDD_DIR}/Solver/uwr/bit_vector/*.cpp"
+    "${CFLOBDD_DIR}/Solver/uwr/parsing/*.cpp"
+    "${CFLOBDD_DIR}/cflobdd_c.cpp"
+)
+list(REMOVE_ITEM SOURCES "${CFLOBDD_DIR}/main.cpp")
+
+file(GLOB JAVA_SOURCES
+    "${CFLOBDD_DIR}/java_bindings/src/main/java/org/trishullab/cflobdd/*.java"
+    "${CFLOBDD_DIR}/java_bindings/src/main/java/org/trishullab/cflobdd/api/jdd/*.java"
+)
+
+# Create the shared library.
+add_library(cflobdd SHARED ${SOURCES})
+add_executable(cflobdd_test ${SOURCES} ${CFLOBDD_DIR}/main.cpp)
+
+add_custom_command(OUTPUT ${CFLOBDD_DIR}/java_bindings/target/cflobdd-1.0-SNAPSHOT.jar
+    COMMAND mvn package
+    DEPENDS ${JAVA_SOURCES}
+    WORKING_DIRECTORY ${CFLOBDD_DIR}/java_bindings
+)
+
+# Create a custom target to build the Java JAR by default
+add_custom_target(cflobdd_java ALL DEPENDS ${CFLOBDD_DIR}/java_bindings/target/cflobdd-1.0-SNAPSHOT.jar)
+
+# Link the math library.
+target_link_libraries(cflobdd m)
+target_compile_definitions(cflobdd PUBLIC PATH_COUNTING_ENABLED)
+
+target_link_libraries(cflobdd_test m)
+target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED)