#include "varorderingopt.h"
#include <time.h>
#include <stdarg.h>
-#include "alloyenc.h"
+#include "alloyinterpreter.h"
+#include "smtinterpreter.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
tuner(NULL),
elapsedTime(0),
satsolverTimeout(NOTIMEOUT),
- alloyEncoder(NULL)
+ interpreter(NULL)
{
satEncoder = new SATEncoder(this);
}
for (uint i = 0; i < size; i++) {
delete allFunctions.get(i);
}
+
+ if(interpreter != NULL){
+ delete interpreter;
+ }
delete boolTrue.getBoolean();
delete satEncoder;
return copy;
}
-CSolver *CSolver::deserialize(const char *file) {
+CSolver *CSolver::deserialize(const char *file, InterpreterType itype) {
model_print("deserializing %s ...\n", file);
- Deserializer deserializer(file);
+ 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()){
- alloyEncoder->encode();
- model_print("Problem encoded in Alloy\n");
- result = alloyEncoder->solve();
- model_print("Problem solved by Alloy\n");
+ if(useInterpreter()){
+ interpreter->encode();
+ model_print("Problem encoded in Interpreter\n");
+ result = interpreter->solve();
+ model_print("Problem solved by Interpreter\n");
} else{
{
return result;
}
-void CSolver::setAlloyEncoder(){
- alloyEncoder = new AlloyEnc(this);
+void CSolver::setInterpreter(InterpreterType type){
+ if(interpreter == NULL){
+ switch(type){
+ case SATUNE:
+ break;
+ case ALLOY:{
+ interpreter = new AlloyInterpreter(this);
+ break;
+ }case Z3:{
+ interpreter = new SMTInterpreter(this);
+ break;
+ }
+ case MATHSAT:
+ case SMTRAT:
+ default:
+ ASSERT(0);
+ }
+ }
}
void CSolver::printConstraints() {
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return useAlloyCompiler()? alloyEncoder->getValue(element):
+ return useInterpreter()? interpreter->getValue(element):
getElementValueSATTranslator(this, element);
default:
ASSERT(0);
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
- return useAlloyCompiler()? alloyEncoder->getBooleanValue(boolean):
+ return useInterpreter()? interpreter->getBooleanValue(boolean):
getBooleanVariableValueSATTranslator(this, boolean);
default:
ASSERT(0);