From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 26 Jul 2018 17:29:22 +0000 (-0700)
Subject: bug fix for nqueens
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=856a6698f7431f5fcc3d4b2c0bdc77e3fc1b008b;p=Benchmarks_CSolver.git

bug fix for nqueens
---

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index be0d6b25..657f005e 100644
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -305,7 +305,7 @@ void atmostOneConstraint(CSolver *solver, vector<BooleanEdge> &constraints){
 				BooleanEdge const1 = solver->applyLogicalOperation(SATC_NOT, constraints[i]);
 				BooleanEdge const2 = solver->applyLogicalOperation(SATC_NOT, constraints[j]);
 				BooleanEdge array[] = {const1, const2};
-				solver->applyLogicalOperation(SATC_OR, (BooleanEdge *)array, 2);
+				solver->addConstraint( solver->applyLogicalOperation(SATC_OR, (BooleanEdge *)array, 2));
 			}
 		}
 	
@@ -330,35 +330,35 @@ void differentInEachRow(CSolver* solver, int N, vector<Element*> &elems){
 void diagonallyDifferentConstraint(CSolver *solver, int N, vector<Element*> &elems){
 	Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 	for(int i=N-1; i>0; i--){
-		cout << "i:" << i << "\t";
+//		cout << "i:" << i << "\t";
 		vector<BooleanEdge> diagonals;
 		for(int j=i; j>=0; j--){
 			int index = i-j;
 			Element* e1 = elems[index];
-			cout << "e" << e1 <<"=" << j << ", ";
+//			cout << "e" << e1 <<"=" << j << ", ";
 			Element* e2 = solver->getElementConst(2, (uint64_t) j);
 			Element* in[] = {e1, e2};
 			BooleanEdge equals = solver->applyPredicate(eq, in, 2);
 			diagonals.push_back(equals);
 			
 		}
-		cout << endl;
+//		cout << endl;
 		atmostOneConstraint(solver, diagonals);
 	}
 	for(int i=1; i< N-1; i++){
-		cout << "i:" << i << "\t";
+//		cout << "i:" << i << "\t";
 		vector<BooleanEdge> diagonals;
 		for(int j=i; j<N; j++){
 			int index =N-1- (j-i);
 			Element* e1 = elems[index];
-			cout << "e" << e1 <<"=" << j << ", ";
+//			cout << "e" << e1 <<"=" << j << ", ";
 			Element* e2 = solver->getElementConst(2, (uint64_t) j);
 			Element* in[] = {e1, e2};
 			BooleanEdge equals = solver->applyPredicate(eq, in, 2);
 			diagonals.push_back(equals);
 			
 		}
-		cout << endl;
+//		cout << endl;
 		atmostOneConstraint(solver, diagonals);
 
 	}
@@ -368,7 +368,7 @@ void diagonallyDifferentConstraint(CSolver *solver, int N, vector<Element*> &ele
 void diagonallyDifferentConstraintBothDir(CSolver *solver, int N, vector<Element*> &elems){
 	diagonallyDifferentConstraint(solver, N, elems);
 	reverse(elems.begin(), elems.end());
-	cout << "Other Diagonal:" << endl;
+//	cout << "Other Diagonal:" << endl;
 	diagonallyDifferentConstraint(solver, N, elems);
 } 
 
@@ -391,6 +391,7 @@ void csolverNQueens(int N){
 	
 	differentInEachRow(solver, N, elems);
 	diagonallyDifferentConstraintBothDir(solver, N, elems);
+//	solver->printConstraints();
 //	solver->serialize();
 	if (solver->solve() != 1){
 		printf("Problem is Unsolvable ...\n");
@@ -399,7 +400,7 @@ void csolverNQueens(int N){
 		memset( table, 0, N*N*sizeof(int) );
 		for(int i=0; i<N; i++){
 			uint x = solver->getElementValue(elems[i]);
-			printf("X=%d, Y=%d\n", x, i);
+//			printf("X=%d, Y=%d\n", x, i);
 			ASSERT(N*x+i < N*N);
 			table[N*x+i] = 1;
 		}