Adding SMT Interpreters

[satune.git] / src / Serialize / deserializer.cc

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index 56acc523676c382af2a15edb3a1abebd76f243eb..eac11e9709296311733611220024de8898f34a4a 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -17,7 +17,7 @@
 
 #define READBUFFERSIZE 16384
 
-Deserializer::Deserializer(const char *file) :
+Deserializer::Deserializer(const char *file, InterpreterType itype) :
        buffer((char *) ourmalloc(READBUFFERSIZE)),
        bufferindex(0),
        bufferbytes(0),
@@ -29,6 +29,9 @@ Deserializer::Deserializer(const char *file) :
        if (filedesc < 0) {
                exit(-1);
        }
+       if(itype != SATUNE){
+               solver->setInterpreter(itype);
+       }
 }
 
 Deserializer::~Deserializer() {
@@ -76,6 +79,9 @@ CSolver *Deserializer::deserialize() {
                case BOOLEANVAR:
                        deserializeBooleanVar();
                        break;
+               case BOOLCONST:
+                       deserializeBooleanConst();
+                       break;
                case ORDERCONST:
                        deserializeBooleanOrder();
                        break;
@@ -145,6 +151,15 @@ void Deserializer::deserializeBooleanVar() {
        map.put(b, solver->getBooleanVar(vtype).getBoolean());
 }
 
+void Deserializer::deserializeBooleanConst() {
+       BooleanVar *b;
+       myread(&b, sizeof(BooleanVar *));
+       bool istrue;
+       myread(&istrue, sizeof(bool));
+       map.put(b, istrue ? solver->getBooleanTrue().getBoolean() :
+                                       solver->getBooleanFalse().getBoolean());
+}
+
 void Deserializer::deserializeBooleanOrder() {
        BooleanOrder *bo_ptr;
        myread(&bo_ptr, sizeof(BooleanOrder *));
@@ -283,40 +298,21 @@ void Deserializer::deserializePredicateOperator() {
        myread(&po_ptr, sizeof(PredicateOperator *));
        CompOp op;
        myread(&op, sizeof(CompOp));
-       uint size;
-       myread(&size, sizeof(uint));
-       Vector<Set *> domains;
-       for (uint i = 0; i < size; i++) {
-               Set *domain;
-               myread(&domain, sizeof(Set *));
-               ASSERT(map.contains(domain));
-               domain = (Set *) map.get(domain);
-               domains.push(domain);
-       }
 
-       map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
+       map.put(po_ptr, solver->createPredicateOperator(op));
 }
 
 void Deserializer::deserializeTable() {
        Table *t_ptr;
        myread(&t_ptr, sizeof(Table *));
-       uint size;
-       myread(&size, sizeof(uint));
-       Vector<Set *> domains;
-       for (uint i = 0; i < size; i++) {
-               Set *domain;
-               myread(&domain, sizeof(Set *));
-               ASSERT(map.contains(domain));
-               domain = (Set *) map.get(domain);
-               domains.push(domain);
-       }
        Set *range;
        myread(&range, sizeof(Set *));
        if (range != NULL) {
                ASSERT(map.contains(range));
                range = (Set *) map.get(range);
        }
-       Table *table = solver->createTable(domains.expose(), size, range);
+       Table *table = solver->createTable(range);
+       uint size;
        myread(&size, sizeof(uint));
        for (uint i = 0; i < size; i++) {
                uint64_t output;
@@ -334,26 +330,36 @@ void Deserializer::deserializeTable() {
 
 
 void Deserializer::deserializeElementSet() {
+       bool anyValue = false;
+       myread(&anyValue, sizeof(bool));
        ElementSet *es_ptr;
        myread(&es_ptr, sizeof(ElementSet *));
        Set *set;
        myread(&set, sizeof(Set *));
        ASSERT(map.contains(set));
        set  = (Set *) map.get(set);
-       map.put(es_ptr, solver->getElementVar(set));
+       Element *newEl = solver->getElementVar(set);
+       newEl->anyValue = anyValue;
+       map.put(es_ptr, newEl);
 }
 
 void Deserializer::deserializeElementConst() {
+       bool anyValue = false;
+       myread(&anyValue, sizeof(bool));
        ElementSet *es_ptr;
        myread(&es_ptr, sizeof(ElementSet *));
        VarType type;
        myread(&type, sizeof(VarType));
        uint64_t value;
        myread(&value, sizeof(uint64_t));
-       map.put(es_ptr, solver->getElementConst(type, value));
+       Element *newEl = solver->getElementConst(type, value);
+       newEl->anyValue = anyValue;
+       map.put(es_ptr, newEl);
 }
 
 void Deserializer::deserializeElementFunction() {
+       bool anyValue = false;
+       myread(&anyValue, sizeof(bool));
        ElementFunction *ef_ptr;
        myread(&ef_ptr, sizeof(ElementFunction *));
        Function *function;
@@ -379,7 +385,9 @@ void Deserializer::deserializeElementFunction() {
        overflowstatus = (Boolean *) map.get(tmp.getBoolean());
        BooleanEdge res(overflowstatus);
        BooleanEdge undefStatus = isNegated ? res.negate() : res;
-       map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
+       Element *newEl = solver->applyFunction(function, members.expose(), size, undefStatus);
+       newEl->anyValue = anyValue;
+       map.put(ef_ptr, newEl);
 }
 
 
@@ -388,23 +396,13 @@ void Deserializer::deserializeFunctionOperator() {
        myread(&fo_ptr, sizeof(FunctionOperator *));
        ArithOp op;
        myread(&op, sizeof(ArithOp));
-       uint size;
-       myread(&size, sizeof(uint));
-       Vector<Set *> domains;
-       for (uint i = 0; i < size; i++) {
-               Set *domain;
-               myread(&domain, sizeof(Set *));
-               ASSERT(map.contains(domain));
-               domain = (Set *) map.get(domain);
-               domains.push(domain);
-       }
        Set *range;
        myread(&range, sizeof(Set *));
        ASSERT(map.contains(range));
        range = (Set *) map.get(range);
        OverFlowBehavior overflowbehavior;
        myread(&overflowbehavior, sizeof(OverFlowBehavior));
-       map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior));
+       map.put(fo_ptr, solver->createFunctionOperator(op, range, overflowbehavior));
 }
 
 void Deserializer::deserializeFunctionTable() {