Add NQueens test & fix CMake building script

CFLOBDD/tests_cfl.cpp

@@ -1949,6 +1949,115 @@ void CFLTests::ClearModules()
 #endif
 }
 
+void CFLTests::testNQueens(int n) {
+	std::cout << "Testing " << n << "-Queens" << std::endl;
+
+	auto start = high_resolution_clock::now();
+	std::vector<std::vector<CFLOBDD>> vars;
+	unsigned int numVars = n * n;
+	unsigned int level = std::ceil(std::log2(numVars));
+	for (unsigned int i = 0; i < n; i++) {
+		vars.push_back(std::vector<CFLOBDD>());
+		for (unsigned int j = 0; j < n; j++) {
+			vars[i].push_back(MkProjection(i * n + j, level));
+		}
+	}
+
+	std::vector<CFLOBDD> orBatch;
+	for (unsigned int i = 0; i < n; i++) {
+		CFLOBDD condition = MkFalse(level);
+		for (unsigned int j = 0; j < n; j++) {
+			condition = MkOr(condition, vars[i][j]);
+		}
+		orBatch.push_back(condition);
+	}
+
+	std::vector<std::vector<CFLOBDD>> impBatch;
+
+	for (unsigned int i = 0; i < n; i++) {
+		std::cout << "Processing implications for row " << i << " / " << n << std::endl;
+		std::vector<CFLOBDD> row;
+		for (unsigned int j = 0; j < n; j++) {
+			CFLOBDD a = MkTrue(level);
+			CFLOBDD b = MkTrue(level);
+			CFLOBDD c = MkTrue(level);
+			CFLOBDD d = MkTrue(level);
+
+			unsigned int k, l;
+
+			/* No one in the same row */
+			for (l = 0; l < n; l++) {
+				if (l != j) {
+					CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[i][l]));
+					a = MkAnd(a, mp);
+				}
+			}
+
+			/* No one in the same column */
+			for (k = 0; k < n; k++) {
+				if (k != i) {
+					CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][j]));
+					b = MkAnd(b, mp);
+				}
+			}
+
+			/* No one in the same up-right diagonal */
+			for (k = 0; k < n; k++) {
+				int ll = (int)k - (int)i + (int)j;
+				if (ll >= 0 && ll < n) {
+					if (k != i) {
+						CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][ll]));
+						c = MkAnd(c, mp);
+					}
+				}
+			}
+
+			/* No one in the same down-right diagonal */
+			for (k = 0; k < n; k++) {
+				int ll = (int)i + (int)j - (int)k;
+				if (ll >= 0 && ll < n) {
+					if (k != i) {
+						CFLOBDD mp = MkImplies(vars[i][j], MkNot(vars[k][ll]));
+						d = MkAnd(d, mp);
+					}
+				}
+			}
+
+			c = MkAnd(c, d);
+			b = MkAnd(b, c);
+			a = MkAnd(a, b);
+			row.push_back(a);
+		}
+		impBatch.push_back(row);
+	}
+
+	CFLOBDD queen = MkTrue(level);
+
+	for (unsigned int i = 0; i < n; i++) {
+		std::cout << "Combining OR conditions for row " << i << " / " << n << std::endl;
+		queen = MkAnd(queen, orBatch[i]);
+	}
+
+	for (unsigned int i = 0; i < n; i++) {
+		CFLOBDD tmp_queen = MkTrue(level);
+		for (unsigned int j = 0; j < n; j++) {
+			std::cout << "Combining implication conditions for position (" << i << ", " << j << ") " << " / " << n << std::endl;
+			tmp_queen = MkAnd(tmp_queen, impBatch[i][j]);
+		}
+		queen = MkAnd(queen, tmp_queen);
+	}
+
+	auto end = high_resolution_clock::now();
+	auto duration = duration_cast<milliseconds>(end - start);
+	std::cout << "Duration: " << duration.count() << " ms" << std::endl;
+	queen.CountPaths();
+	CFLOBDDInternalNode* queen_node = (CFLOBDDInternalNode*) queen.root->rootConnection.entryPointHandle.handleContents;
+
+	// number of solutions = 2 ^ log(num_solutions) / 2 ^ num_dummy_vars = 2^(log(num_solutions) - num_dummy_vars)
+	unsigned int numDummyVars = std::pow(2, std::ceil(std::log2(numVars))) - numVars;
+	std::cout << "Number of solutions for " << n << "-Queens: " << std::round(std::pow(2, queen_node->numPathsToExit[1] - numDummyVars)) << std::endl;
+}
+
 bool CFLTests::runTests(const char *arg, int size, int seed, int a){
 
 	CFLTests::InitModules();
@@ -2214,6 +2323,8 @@ bool CFLTests::runTests(const char *arg, int size, int seed, int a){
 		// Test VerifySubtractiveKaratsubaOneLevelModuliwise
 		std::cout << "Testing VerifySubtractiveKaratsubaOneLevelModuliwise" << std::endl;
 		VerifySubtractiveKaratsubaOneLevelModuliwise();
+	} else if (curTest == "nqueens") {
+		CFLTests::testNQueens(size);
 	}
 	else {
 		std::cout << "Unrecognized test name: " << curTest << std::endl;

CFLOBDD/tests_cfl.h

@@ -54,6 +54,7 @@ class CFLTests
         static void testXOR(int size);
         static void testMatMul(int size);
         static void testQFT(int size, int seed);
+        static void testNQueens(int size);
 
 #ifdef WCFLOBDD_SUPPORTED
         static void testWeightedOps(unsigned int size);

CMakeLists.txt

@@ -1,8 +1,8 @@
 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 the C++ standard to 20, as specified in the compile command
+set(CMAKE_CXX_STANDARD 20)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 
 # Add compiler flags: -g for debugging and -w to suppress warnings
@@ -28,10 +28,14 @@ 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")
 
+if(NOT WCFLOBDD_SUPPORTED)
+    file(GLOB WEIGHTED_SOURCES "${CFLOBDD_DIR}/weighted_*.cpp" "${CFLOBDD_DIR}/w*.cpp")
+    list(REMOVE_ITEM SOURCES ${WEIGHTED_SOURCES})
+endif()
+
 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"
@@ -52,7 +56,12 @@ add_custom_target(cflobdd_java ALL DEPENDS ${CFLOBDD_DIR}/java_bindings/target/c
 
 # Link the math library.
 target_link_libraries(cflobdd m)
-target_compile_definitions(cflobdd PUBLIC PATH_COUNTING_ENABLED)
+# target_compile_definitions(cflobdd PUBLIC PATH_COUNTING_ENABLED)
 
 target_link_libraries(cflobdd_test m)
-target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED)
+# target_compile_definitions(cflobdd_test PUBLIC PATH_COUNTING_ENABLED)
+
+if(WCFLOBDD_SUPPORTED)
+    target_compile_definitions(cflobdd PUBLIC WCFLOBDD_SUPPORTED)
+    target_compile_definitions(cflobdd_test PUBLIC WCFLOBDD_SUPPORTED)
+endif()