#include "varorderingopt.h"
#include <time.h>
#include <stdarg.h>
-#include "alloyenc.h"
+#include "alloyinterpreter.h"
+#include "smtinterpreter.h"
+#include "mathsatinterpreter.h"
+#include "smtratinterpreter.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
return copy;
}
-CSolver *CSolver::deserialize(const char *file, bool alloy) {
+CSolver *CSolver::deserialize(const char *file, InterpreterType itype) {
model_print("deserializing %s ...\n", file);
- Deserializer deserializer(file, alloy);
+ Deserializer deserializer(file, itype);
return deserializer.deserialize();
}
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
- if(!useAlloyCompiler()){
+ if(!useInterpreter()){
BooleanEdge newarray[asize];
switch (op) {
case SATC_NOT: {
}
}
Boolean *constraint = new BooleanOrder(order, first, second);
- if (!useAlloyCompiler() ){
+ if (!useInterpreter() ){
Boolean *b = boolMap.get(constraint);
if (b == NULL) {
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if(!useAlloyCompiler()){
+ if(!useInterpreter()){
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
deleteTuner = true;
}
int result = IS_INDETER;
- if(useAlloyCompiler()){
+ if(useInterpreter()){
interpreter->encode();
- model_print("Problem encoded in Alloy\n");
+ model_print("Problem encoded in Interpreter\n");
result = interpreter->solve();
- model_print("Problem solved by Alloy\n");
+ model_print("Problem solved by Interpreter\n");
} else{
{
return result;
}
-void CSolver::setAlloyEncoder(){
+void CSolver::setInterpreter(InterpreterType type){
if(interpreter == NULL){
- interpreter = new AlloyEnc(this);
+ switch(type){
+ case SATUNE:
+ break;
+ case ALLOY:{
+ interpreter = new AlloyInterpreter(this);
+ break;
+ }case Z3:{
+ interpreter = new SMTInterpreter(this);
+ break;
+ }
+ case MATHSAT:{
+ interpreter = new MathSATInterpreter(this);
+ break;
+ }
+ case SMTRAT:{
+ interpreter = new SMTRatInterpreter(this);
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
}
}
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return useAlloyCompiler()? interpreter->getValue(element):
+ return useInterpreter()? interpreter->getValue(element):
getElementValueSATTranslator(this, element);
default:
ASSERT(0);
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
- return useAlloyCompiler()? interpreter->getBooleanValue(boolean):
+ return useInterpreter()? interpreter->getBooleanValue(boolean):
getBooleanVariableValueSATTranslator(this, boolean);
default:
ASSERT(0);