From ec7fdc8cadb0c6d0883bc61e35c752ffd856e370 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 23 Jan 2019 13:27:44 -0800 Subject: [PATCH] Adding support for Alloy Compiler for NQueens and Hexiom --- hexiom/csolverHexiom.py | 50 +++++++++++++++++---------------- hexiom/run.sh | 1 + nqueens/nqueens.cc | 17 +++++++---- sudoku-csolver/csolversudoku.py | 2 +- 4 files changed, 39 insertions(+), 31 deletions(-) diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py index 8d07a96b..8668c1fe 100755 --- 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 aec86159..7e184417 100755 --- 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 5865c860..9550f161 100644 --- a/nqueens/nqueens.cc +++ b/nqueens/nqueens.cc @@ -11,11 +11,11 @@ #include "common.h" #include #include - #define NANOSEC 1000000000.0 - using namespace std; +enum SolverType {CSOLVER, DUMP, ALLOY}; + void EqualOneToCNF(vector literals, vector< vector > & cnf){ int N = literals.size(); cnf.push_back(literals); @@ -460,7 +460,7 @@ void symmetryBreakingConstraint(CSolver *solver, int N, vector& 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 [--csolver]\n"); + printf("Two arguments are needed\n./nqueen [--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 129fe52f..e93f7259 100644 --- 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) -- 2.34.1