projects
/
satune.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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 <stdarg.h>
#include "alloyinterpreter.h"
#include "smtinterpreter.h"
+#include "mathsatinterpreter.h"
+#include "smtratinterpreter.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
@@
-692,8
+694,14
@@
void CSolver::setInterpreter(InterpreterType type){
interpreter = new SMTInterpreter(this);
break;
}
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);
}
default:
ASSERT(0);
}