From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 7 Feb 2019 00:17:28 +0000 (-0800)
Subject: Setting Alloy before adding constraints...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e81afdba2a70f6b191011583fb4cdc04e4df41b4;p=Benchmarks_CSolver.git

Setting Alloy before adding constraints...
---

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 8668c1fe..168e273b 100755
--- a/hexiom/csolverHexiom.py
+++ b/hexiom/csolverHexiom.py
@@ -786,13 +786,14 @@ def main():
 	board_input.print_to_stdout()
 	csolverlb = ps.loadCSolver();
 	csolver = csolverlb.createCCSolver()
+	if len(sys.argv) > 2 and sys.argv[-1] == "--alloy":
+		csolverlb.setAlloyEncoder(csolver)
 	formulation = SAT_formulation_from_board_input(board_input, csolverlb, csolver)
 
 	print '=== Done! Calling CSolver solver now ==='
 	if len(sys.argv) > 2 and sys.argv[-1] == "--dump":
 		csolverlb.serialize(csolver)
-	if len(sys.argv) > 2 and sys.argv[-1] == "--alloy":
-		csolverlb.setAlloyEncoder(csolver)
+	
 #     csolverlb.printConstraints(csolver)
 	if csolverlb.solve(csolver) != 1:
 		print '*** Got UNSAT result! ***'
diff --git a/killerSudoku/csolversudoku.py b/killerSudoku/csolversudoku.py
index 3a17e98f..8a0d900d 100644
--- a/killerSudoku/csolversudoku.py
+++ b/killerSudoku/csolversudoku.py
@@ -42,6 +42,8 @@ def generateEqualityConstraint(csolverlb, solver, e1, e2):
 def generateKillerSudokuConstraints(N, killerRules, solverOption):
 	csolverlb = ps.loadCSolver()
 	solver = csolverlb.createCCSolver()
+	if solverOption == Solver.ALLOY:
+		csolverlb.setAlloyEncoder(solver)
 	s1 = [ i for i in range(1, N+1)]
 	set1 = (c_long* len(s1))(*s1)
 	s1 = csolverlb.createSet(solver, c_uint(1), set1, c_uint(N))
@@ -232,10 +234,11 @@ def generateKillerSudokuConstraints(N, killerRules, solverOption):
 			valid([problem[i + k % root, j + k // root] for k in range(N)])
 	
 	#Serializing the problem before solving it ....
+	print "Done with encoding ...."
 	if solverOption == Solver.SERIALISE:
 		csolverlb.serialize(solver)
-	if solverOption == Solver.ALLOY:
-		csolverlb.setAlloyEncoder(solver)
+
+	print "start solving the problem ..."
 	if csolverlb.solve(solver) != 1:
 		return None
 	result = [[0 for i in range(N)] for i in range(N)]
diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index 9550f161..a90c7fa4 100644
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -466,6 +466,10 @@ void csolverNQueens(int N, SolverType stype = CSOLVER){
 		return;
 	}
 	CSolver *solver = new CSolver();
+	if(stype = ALLOY){
+		solver->setAlloyEncoder();
+	}
+
 	uint64_t domain[N];
 	for(int i=0; i<N; i++){
 		domain[i] = i;
@@ -482,10 +486,7 @@ void csolverNQueens(int N, SolverType stype = CSOLVER){
 //	solver->printConstraints();
 	if(stype == DUMP){
 		solver->serialize();
-	} else if(stype = ALLOY){
-		solver->setAlloyEncoder();
-	}
-	if (solver->solve() != 1){
+	} if (solver->solve() != 1){
 		printf("Problem is Unsolvable ...\n");
 	}else {
 		int table[N*N];
diff --git a/sudoku-csolver/csolversudoku.py b/sudoku-csolver/csolversudoku.py
index e93f7259..e4733aad 100644
--- a/sudoku-csolver/csolversudoku.py
+++ b/sudoku-csolver/csolversudoku.py
@@ -61,6 +61,8 @@ def extractItemInSetOptimization(csolverlb, solver, sudoku, N):
 def generateSudokuConstraints(N, sudoku = None, solverID  = -1):
 	csolverlb = ps.loadCSolver()
 	solver = csolverlb.createCCSolver()
+	if solverID == Solver.ALLOY:
+		csolverlb.setAlloyEncoder(solver)
 	s1 = [ i for i in range(1, N+1)]
 	set1 = (c_long* len(s1))(*s1)
 	s1 = csolverlb.createSet(solver, c_uint(1), set1, c_uint(N))
@@ -129,8 +131,7 @@ def generateSudokuConstraints(N, sudoku = None, solverID  = -1):
 	#Serializing the problem before solving it ....
 	if solverID == Solver.SERIALISE:
 		csolverlb.serialize(solver)
-	if solverID == Solver.ALLOY:
-		csolverlb.setAlloyEncoder(solver)
+
 	if csolverlb.solve(solver) != 1:
 		print "Problem is unsolvable!"
                 sys.exit(1)