Adding support for SMT solvers

[Benchmarks_CSolver.git] / nqueens / nqueens.cc

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]);
        }