Setting Alloy before adding constraints...

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 8668c1fec662f7c45f75a5f5d50eecfef4d0452e..168e273bdbefc92e672a4e6eaf164534baa66446 100755 (executable)
--- 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 3a17e98f7a98e3fabc4ac3d7bb5374c012edda11..8a0d900d1330578e370f86f3092fb7977c188b78 100644 (file)
--- 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 9550f161a51137c7941df7c8959794e4e1bfd929..a90c7fa422bd8f63b01444b6775961224b07a483 100644 (file)
--- 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 e93f7259b8298b9217d9b6a1682f82fa97e5e7da..e4733aad82c64f9d652aaedbf88ef31e899c8a52 100644 (file)
--- 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)