Merging with Tuner branch

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 2670e4745a24c0371aaa4db082be7890bec86666..1eba56d4bd46afdfa886a9e7b5efbfaa361360a2 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -31,6 +31,8 @@
 #include <stdarg.h>
 #include "alloyinterpreter.h"
 #include "smtinterpreter.h"
+#include "mathsatinterpreter.h"
+#include "smtratinterpreter.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -692,8 +694,14 @@ void CSolver::setInterpreter(InterpreterType type){
                                interpreter = new SMTInterpreter(this);
                                break;
                        }
-                       case MATHSAT:
-                       case SMTRAT:
+                       case MATHSAT:{
+                               interpreter = new MathSATInterpreter(this);
+                               break;
+                       }
+                       case SMTRAT:{
+                               interpreter = new SMTRatInterpreter(this);
+                               break;
+                       }
                        default:
                                ASSERT(0);
                }