Adding support for SMT solvers

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 168e273bdbefc92e672a4e6eaf164534baa66446..6f5a2b9d2c147d23d0790fd88cc5b4f32f6d3b5b 100755 (executable)
--- 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 1c505ee9f54ebea58021341680808b1ee914ed22..08232b3265d05191cf70907b9fa2f18dd8f43992 100644 (file)
--- 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 8a0d900d1330578e370f86f3092fb7977c188b78..3584b183d8924f5da3c835a48f90acecddb97fc9 100644 (file)
--- 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 a90c7fa422bd8f63b01444b6775961224b07a483..2612b6fd2f226a124c00663fbf9a4cc7abe5f093 100644 (file)
--- 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<int> literals, vector< vector<int> > & cnf){
        int N = literals.size();
        cnf.push_back(literals);
@@ -460,14 +462,14 @@ void symmetryBreakingConstraint(CSolver *solver, int N, vector<Element*>& 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 <size> [--csolver/--dump/--alloy]\n");
+               printf("Two arguments are needed\n./nqueen <size> [--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 e633e77d08657f5e71e662026129dca8b91e3a81..838fdee150ffc7e87043543f3fedd5962c3fa405 100644 (file)
--- 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 e4733aad82c64f9d652aaedbf88ef31e899c8a52..fd79214542cab5d3c3a4b4b49ff898da0aabde7f 100644 (file)
--- 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))