From 36b0cf70c30a406faa373079232f71e8749289f5 Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Fri, 25 Jan 2019 12:15:40 -0800
Subject: [PATCH] Alloy Support for Killer Sudoku

---
 killerSudoku/argprocessor.py  | 16 +++++++++++-----
 killerSudoku/csolversudoku.py | 15 +++++++++++----
 killerSudoku/killerSolver.py  |  4 ++--
 killerSudoku/run.sh           |  1 +
 4 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/killerSudoku/argprocessor.py b/killerSudoku/argprocessor.py
index c748e558..1c505ee9 100644
--- a/killerSudoku/argprocessor.py
+++ b/killerSudoku/argprocessor.py
@@ -9,16 +9,22 @@ class KSudokuArgParser:
         self.parser.add_argument('--problem', '-p', metavar='problem.killer', type=str, nargs=1,help='Files generated by KillerSudokuGenerator.py')
         self.parser.add_argument('--csolver', '-cs', action='store_true',help='Encode with the constraint solver (default: uses the original hand crafted encoding)')
         self.parser.add_argument('--dump', '-dp', action='store_true',help='Dumps the problem into a file')
+        self.parser.add_argument('--alloy', '-al', action='store_true',help='Solve problem via Alloy')
         self.args = self.parser.parse_args()
         
     def getProblemName(self):
         return self.args.problem
-    
-    def useCSolverEncoding(self):
-        return self.args.csolver
 
-    def shouldSerialize(self):
-        return self.args.dump
+    def getCSolverOption(self):
+        if self.args.alloy:
+            return 3
+        if self.args.dump:
+            return 2
+        if self.args.csolver:
+            return 1
+        else:
+            return 0
+
 # def main():
 #     print sys.argv
 #     argParser = KSudokuArgParser()
diff --git a/killerSudoku/csolversudoku.py b/killerSudoku/csolversudoku.py
index ed20da85..3a17e98f 100644
--- a/killerSudoku/csolversudoku.py
+++ b/killerSudoku/csolversudoku.py
@@ -4,9 +4,14 @@ import numpy as np
 import sys
 from itertools import combinations, ifilter, chain
 
-def solveProblem(N, killerRules, serialize = False):
+class Solver:
+	CSOLVER=1
+	SERIALISE=2
+	ALLOY=3
+
+def solveProblem(N, killerRules, solverOption):
 	
-	return generateKillerSudokuConstraints(N, killerRules, serialize)
+	return generateKillerSudokuConstraints(N, killerRules, solverOption)
 
 def getDomain(allPossible):
 	assert len(allPossible) > 0
@@ -34,7 +39,7 @@ def generateEqualityConstraint(csolverlb, solver, e1, e2):
         b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(2))
         return b
 
-def generateKillerSudokuConstraints(N, killerRules, serialize):
+def generateKillerSudokuConstraints(N, killerRules, solverOption):
 	csolverlb = ps.loadCSolver()
 	solver = csolverlb.createCCSolver()
 	s1 = [ i for i in range(1, N+1)]
@@ -227,8 +232,10 @@ def generateKillerSudokuConstraints(N, killerRules, serialize):
 			valid([problem[i + k % root, j + k // root] for k in range(N)])
 	
 	#Serializing the problem before solving it ....
-	if serialize:
+	if solverOption == Solver.SERIALISE:
 		csolverlb.serialize(solver)
+	if solverOption == Solver.ALLOY:
+		csolverlb.setAlloyEncoder(solver)
 	if csolverlb.solve(solver) != 1:
 		return None
 	result = [[0 for i in range(N)] for i in range(N)]
diff --git a/killerSudoku/killerSolver.py b/killerSudoku/killerSolver.py
index 803ef2f1..779e4d1d 100644
--- a/killerSudoku/killerSolver.py
+++ b/killerSudoku/killerSolver.py
@@ -323,8 +323,8 @@ def solveKillerSudoku(killerRules):
     global argparser
     result_matrix = None
     
-    if argparser.useCSolverEncoding() or argparser.shouldSerialize():
-        result_matrix = cs.solveProblem(N, killerRules, argparser.shouldSerialize())
+    if argparser.getCSolverOption() > 0:
+        result_matrix = cs.solveProblem(N, killerRules, argparser.getCSolverOption())
     else:
         result_matrix = solveOriginalEncoding(killerRules)
     
diff --git a/killerSudoku/run.sh b/killerSudoku/run.sh
index aec86159..7e184417 100755
--- a/killerSudoku/run.sh
+++ b/killerSudoku/run.sh
@@ -1,5 +1,6 @@
 #!/bin/bash
 
+export CLASSPATH=./csolver/original.jar:.:$CLASSPATH
 export PYTHONPATH=./csolver
 export LD_LIBRARY_PATH=./csolver
 # For Mac OSX
-- 
2.34.1