Alloy compiler for Sudoku
[Benchmarks_CSolver.git] / sudoku-csolver / csolversudoku.py
index ac1fef6359463ce7adc1cf1d78edc313df140231..129fe52f5ef49632b8734deef515e57134f2e2d4 100644 (file)
@@ -3,11 +3,16 @@ from ctypes import *
 import numpy as np
 import sys
 
+class Solver:
+       CSOLVER=1
+       SERIALISE=2
+       ALLOY=3
+
 def generateProblem(N):
        return generateSudokuConstraints(N)     
 
-def solveProblem(N, problem, serialize):
-       return generateSudokuConstraints(N, problem, serialize)
+def solveProblem(N, problem, solverID):
+       return generateSudokuConstraints(N, problem, solverID)
 
 def replaceWithElemConstOptimization(elemConsts, problem, sudoku):
        for i,row in enumerate(sudoku):
@@ -53,7 +58,7 @@ def extractItemInSetOptimization(csolverlb, solver, sudoku, N):
        
        return np.array([[csolverlb.getElementVar(solver,sets[i][j]) for j in range(N)] for i in range(N)])
 
-def generateSudokuConstraints(N, sudoku = None, serialize=False):
+def generateSudokuConstraints(N, sudoku = None, solverID  = -1):
        csolverlb = ps.loadCSolver()
        solver = csolverlb.createCCSolver()
        s1 = [ i for i in range(1, N+1)]
@@ -122,8 +127,10 @@ def generateSudokuConstraints(N, sudoku = None, serialize=False):
 
 #      csolverlb.printConstraints(solver);     
        #Serializing the problem before solving it ....
-       if serialize:
+       if solverID == Solver.SERIALISE:
                csolverlb.serialize(solver)
+       if solverID == Solver.ALLOY:
+               csolverlb.setAlloyEncode(solver)
        if csolverlb.solve(solver) != 1:
                print "Problem is unsolvable!"
                 sys.exit(1)