Adding support for Alloy Compiler for NQueens and Hexiom

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 8d07a96bd2cbab699d7b8a3233724547b43876f7..8668c1fec662f7c45f75a5f5d50eecfef4d0452e 100755 (executable)
--- a/hexiom/csolverHexiom.py
+++ b/hexiom/csolverHexiom.py
@@ -771,33 +771,35 @@ import sys
 
 def main():
 
-    if len(sys.argv) <= 1:
-        print "usage: ./hexiom_solve.py [0-40] [--dump]?"
-        exit(1)
+       if len(sys.argv) <= 1:
+               print "usage: ./run.sh csolverHexiom.py [0-40] [--dump/--alloy]?"
+               exit(1)
 
-    level_no = int(sys.argv[1])
+       level_no = int(sys.argv[1])
 
-    input_filename   = LEVEL_INPUT_FILENAME_PATTERN(level_no)
+       input_filename   = LEVEL_INPUT_FILENAME_PATTERN(level_no)
     
-    with open(input_filename, 'r') as fil:
-        board_input = read_input(fil)
-
-    print '== Level to solve== '
-    board_input.print_to_stdout()
-    csolverlb = ps.loadCSolver();
-    csolver = csolverlb.createCCSolver()
-    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)
+       with open(input_filename, 'r') as fil:
+               board_input = read_input(fil)
+
+       print '== Level to solve== '
+       board_input.print_to_stdout()
+       csolverlb = ps.loadCSolver();
+       csolver = csolverlb.createCCSolver()
+       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! ***'
-        sys.exit(1)
-    else:
-        print '** Solution found! ***'
-        print_board_from_assignments(csolverlb, csolver, formulation)
+       if csolverlb.solve(csolver) != 1:
+               print '*** Got UNSAT result! ***'
+               sys.exit(1)
+       else:
+               print '** Solution found! ***'
+               print_board_from_assignments(csolverlb, csolver, formulation)
 
 if __name__ == '__main__':
-    main()
+       main()

diff --git a/hexiom/run.sh b/hexiom/run.sh
index aec861598dbe5e4a41b133615cf0f0e59b58454d..7e18441782f1154f86eae12ca2a2b4e69855bfe8 100755 (executable)
--- a/hexiom/run.sh
+++ b/hexiom/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

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index 5865c860cfa77e968767ba818fc81645d2494da7..9550f161a51137c7941df7c8959794e4e1bfd929 100644 (file)
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -11,11 +11,11 @@
 #include "common.h"
 #include <algorithm>
 #include <ctime>
-
 #define NANOSEC 1000000000.0
-
 using namespace std;
 
+enum SolverType {CSOLVER, DUMP, ALLOY};
+
 void EqualOneToCNF(vector<int> literals, vector< vector<int> > & cnf){
        int N = literals.size();
        cnf.push_back(literals);
@@ -460,7 +460,7 @@ void symmetryBreakingConstraint(CSolver *solver, int N, vector<Element*>& elems)
 
 }
 
-void csolverNQueens(int N, bool serialize=false){
+void csolverNQueens(int N, SolverType stype = CSOLVER){
        if(N <=1){
                cout<<"Q" << endl;
                return;
@@ -480,8 +480,10 @@ void csolverNQueens(int N, bool serialize=false){
        diagonallyDifferentConstraintBothDir(solver, N, elems);
        symmetryBreakingConstraint(solver, N, elems);
 //     solver->printConstraints();
-       if(serialize){
+       if(stype == DUMP){
                solver->serialize();
+       } else if(stype = ALLOY){
+               solver->setAlloyEncoder();
        }
        if (solver->solve() != 1){
                printf("Problem is Unsolvable ...\n");
@@ -504,7 +506,7 @@ void csolverNQueens(int N, bool serialize=false){
 
 int main(int argc, char * argv[]){
        if(argc < 2){
-               printf("Two arguments are needed\n./nqueen <size> [--csolver]\n");
+               printf("Two arguments are needed\n./nqueen <size> [--csolver/--dump/--alloy]\n");
                exit(-1);
        }
        int N = atoi(argv[1]);
@@ -516,7 +518,10 @@ int main(int argc, char * argv[]){
                csolverNQueens(N);
        }else if (strcmp( argv[2], "--dump") == 0){
                printf("Running the CSolver encoding ...\n");
-               csolverNQueens(N, true);
+               csolverNQueens(N, DUMP);
+       }else if (strcmp( argv[2], "--alloy") == 0){
+               printf("Running the Alloy encoding ...\n");
+               csolverNQueens(N, ALLOY);
        }else {
                printf("Unknown argument %s", argv[2]);
        }

diff --git a/sudoku-csolver/csolversudoku.py b/sudoku-csolver/csolversudoku.py
index 129fe52f5ef49632b8734deef515e57134f2e2d4..e93f7259b8298b9217d9b6a1682f82fa97e5e7da 100644 (file)
--- a/sudoku-csolver/csolversudoku.py
+++ b/sudoku-csolver/csolversudoku.py
@@ -130,7 +130,7 @@ def generateSudokuConstraints(N, sudoku = None, solverID  = -1):
        if solverID == Solver.SERIALISE:
                csolverlb.serialize(solver)
        if solverID == Solver.ALLOY:
-               csolverlb.setAlloyEncode(solver)
+               csolverlb.setAlloyEncoder(solver)
        if csolverlb.solve(solver) != 1:
                print "Problem is unsolvable!"
                 sys.exit(1)