From f03c1e1162869bf8db6227005e3f94264d91d024 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Sat, 23 Feb 2019 00:35:24 -0800 Subject: [PATCH] Adding support for SMT solvers --- hexiom/csolverHexiom.py | 24 ++++++++++++++-- killerSudoku/argprocessor.py | 49 +++++++++++++++++++-------------- killerSudoku/csolversudoku.py | 13 +++++++-- nqueens/nqueens.cc | 29 +++++++++++++------ sudoku-csolver/Sudoku.py | 11 +++++++- sudoku-csolver/csolversudoku.py | 11 ++++++-- 6 files changed, 100 insertions(+), 37 deletions(-) diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py index 168e273b..6f5a2b9d 100755 --- a/hexiom/csolverHexiom.py +++ b/hexiom/csolverHexiom.py @@ -11,6 +11,17 @@ import os from itertools import combinations ############################################ +class Solver: + CSOLVER=1 + SERIALISE=2 + ALLOY=3 + Z3=4 + MATHSAT=5 + SMTRAT=6 +def getSolverType(solverID): + return solverID-2 + + #### # Helper functions ### @@ -772,7 +783,7 @@ import sys def main(): if len(sys.argv) <= 1: - print "usage: ./run.sh csolverHexiom.py [0-40] [--dump/--alloy]?" + print "usage: ./run.sh csolverHexiom.py [0-40] [--dump/--alloy/--z3/--mathsat/--smtrat]?" exit(1) level_no = int(sys.argv[1]) @@ -787,7 +798,16 @@ def main(): csolverlb = ps.loadCSolver(); csolver = csolverlb.createCCSolver() if len(sys.argv) > 2 and sys.argv[-1] == "--alloy": - csolverlb.setAlloyEncoder(csolver) + csolverlb.setInterpreter(csolver, getSolverType(Solver.ALLOY) ) + elif len(sys.argv) > 2 and sys.argv[-1] == "--z3": + csolverlb.setInterpreter(csolver, getSolverType(Solver.Z3)) + elif len(sys.argv) > 2 and sys.argv[-1] == "--mathsat": + csolverlb.setInterpreter(csolver, getSolverType(Solver.MATHSAT) ) + elif len(sys.argv) > 2 and sys.argv[-1] == "--smtrat": + csolverlb.setInterpreter(csolver, getSolverType(Solver.SMTRAT) ) + elif len(sys.argv) > 2: + print "Unknown command ..." + exit(-1) formulation = SAT_formulation_from_board_input(board_input, csolverlb, csolver) print '=== Done! Calling CSolver solver now ===' diff --git a/killerSudoku/argprocessor.py b/killerSudoku/argprocessor.py index 1c505ee9..08232b32 100644 --- a/killerSudoku/argprocessor.py +++ b/killerSudoku/argprocessor.py @@ -4,26 +4,35 @@ import sys class KSudokuArgParser: - def __init__(self): - self.parser = argparse.ArgumentParser(description='Killer Sudoku Puzzle!') - 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 __init__(self): + self.parser = argparse.ArgumentParser(description='Killer Sudoku Puzzle!') + 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.parser.add_argument('--z3', '-z', action='store_true',help='Solve problem via z3') + self.parser.add_argument('--mathsat', '-ms', action='store_true',help='Solve problem via MathSat') + self.parser.add_argument('--smtrat', '-sr', action='store_true',help='Solve problem via SMTRat') + self.args = self.parser.parse_args() - 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 getProblemName(self): + return self.args.problem + + def getCSolverOption(self): + if self.args.smtrat: + return 6 + if self.args.mathsat: + return 5 + if self.args.z3: + return 4 + 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 @@ -31,4 +40,4 @@ class KSudokuArgParser: # # # if __name__ == "__main__": -# main() \ No newline at end of file +# main() diff --git a/killerSudoku/csolversudoku.py b/killerSudoku/csolversudoku.py index 8a0d900d..3584b183 100644 --- a/killerSudoku/csolversudoku.py +++ b/killerSudoku/csolversudoku.py @@ -5,9 +5,15 @@ import sys from itertools import combinations, ifilter, chain class Solver: - CSOLVER=1 + CSOLVER=1 SERIALISE=2 ALLOY=3 + Z3=4 + MATHSAT=5 + SMTRAT=6 + +def getSolverType(solverID): + return solverID-2 def solveProblem(N, killerRules, solverOption): @@ -42,8 +48,9 @@ def generateEqualityConstraint(csolverlb, solver, e1, e2): def generateKillerSudokuConstraints(N, killerRules, solverOption): csolverlb = ps.loadCSolver() solver = csolverlb.createCCSolver() - if solverOption == Solver.ALLOY: - csolverlb.setAlloyEncoder(solver) + print solverOption + if solverOption >= Solver.ALLOY: + csolverlb.setInterpreter(solver, getSolverType(solverOption) ) 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)) diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc index a90c7fa4..2612b6fd 100644 --- a/nqueens/nqueens.cc +++ b/nqueens/nqueens.cc @@ -14,8 +14,10 @@ #define NANOSEC 1000000000.0 using namespace std; -enum SolverType {CSOLVER, DUMP, ALLOY}; - +enum SolverType {_CSOLVER, _DUMP, _ALLOY, _Z3, _MATHSAT, _SMTRAT}; +InterpreterType convertSolverToInterpreterType(SolverType type){ + return (InterpreterType)(type -1); +} void EqualOneToCNF(vector literals, vector< vector > & cnf){ int N = literals.size(); cnf.push_back(literals); @@ -460,14 +462,14 @@ void symmetryBreakingConstraint(CSolver *solver, int N, vector& elems) } -void csolverNQueens(int N, SolverType stype = CSOLVER){ +void csolverNQueens(int N, SolverType stype = _CSOLVER){ if(N <=1){ cout<<"Q" << endl; return; } CSolver *solver = new CSolver(); - if(stype = ALLOY){ - solver->setAlloyEncoder(); + if(stype >= _ALLOY){ + solver->setInterpreter( convertSolverToInterpreterType(stype) ); } uint64_t domain[N]; @@ -484,7 +486,7 @@ void csolverNQueens(int N, SolverType stype = CSOLVER){ diagonallyDifferentConstraintBothDir(solver, N, elems); symmetryBreakingConstraint(solver, N, elems); // solver->printConstraints(); - if(stype == DUMP){ + if(stype == _DUMP){ solver->serialize(); } if (solver->solve() != 1){ printf("Problem is Unsolvable ...\n"); @@ -507,7 +509,7 @@ void csolverNQueens(int N, SolverType stype = CSOLVER){ int main(int argc, char * argv[]){ if(argc < 2){ - printf("Two arguments are needed\n./nqueen [--csolver/--dump/--alloy]\n"); + printf("Two arguments are needed\n./nqueen [--csolver/--dump/--alloy/--z3/--mathsat/--smtrat]\n"); exit(-1); } int N = atoi(argv[1]); @@ -519,10 +521,19 @@ int main(int argc, char * argv[]){ csolverNQueens(N); }else if (strcmp( argv[2], "--dump") == 0){ printf("Running the CSolver encoding ...\n"); - csolverNQueens(N, DUMP); + csolverNQueens(N, _DUMP); }else if (strcmp( argv[2], "--alloy") == 0){ printf("Running the Alloy encoding ...\n"); - csolverNQueens(N, ALLOY); + csolverNQueens(N, _ALLOY); + }else if (strcmp( argv[2], "--z3") == 0){ + printf("Running the Z3 encoding ...\n"); + csolverNQueens(N, _Z3); + }else if (strcmp( argv[2], "--mathsat") == 0){ + printf("Running the mathsat encoding ...\n"); + csolverNQueens(N, _MATHSAT); + } else if (strcmp( argv[2], "--smtrat") == 0){ + printf("Running the SMTRat encoding ...\n"); + csolverNQueens(N, _SMTRAT); }else { printf("Unknown argument %s", argv[2]); } diff --git a/sudoku-csolver/Sudoku.py b/sudoku-csolver/Sudoku.py index e633e77d..838fdee1 100644 --- a/sudoku-csolver/Sudoku.py +++ b/sudoku-csolver/Sudoku.py @@ -37,6 +37,15 @@ def main(argv): elif "--alloy" in args: print "Solving the problem using alloy ..." read_problem_from_file(args[indx], 3) + elif "--z3" in args: + print "Solving the problem using alloy ..." + read_problem_from_file(args[indx], 4) + elif "--mathsat" in args: + print "Solving the problem using alloy ..." + read_problem_from_file(args[indx], 5) + elif "--smtrat" in args: + print "Solving the problem using alloy ..." + read_problem_from_file(args[indx], 6) else: read_problem_from_file(args[indx], 0) elif opt in ( "--gen"): @@ -57,7 +66,7 @@ def help(): print('Sudoku.py -h [or] --hard') print('Sudoku.py -v [or] --evil') print('Sudoku.py -b [or] --blank') - print('Sudoku.py --file file.problem [--csolver/--dump/--alloy]') + print('Sudoku.py --file file.problem [--csolver/--dump/--alloy/--z3/--mathsat/--smtrat]') print('Sudoku.py --gen 9 20 [--csolver/--dump]') print('All problems generated by websudoku.com') sys.exit() diff --git a/sudoku-csolver/csolversudoku.py b/sudoku-csolver/csolversudoku.py index e4733aad..fd792145 100644 --- a/sudoku-csolver/csolversudoku.py +++ b/sudoku-csolver/csolversudoku.py @@ -7,6 +7,13 @@ class Solver: CSOLVER=1 SERIALISE=2 ALLOY=3 + Z3=4 + MATHSAT=5 + SMTRAT=6 +def getSolverType(solverID): + return solverID-2 + + def generateProblem(N): return generateSudokuConstraints(N) @@ -61,8 +68,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) + if solverID >= Solver.ALLOY: + csolverlb.setInterpreter(solver, getSolverType(solverID)) 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)) -- 2.34.1