#define READBUFFERSIZE 16384
-Deserializer::Deserializer(const char *file) :
+Deserializer::Deserializer(const char *file, InterpreterType itype) :
buffer((char *) ourmalloc(READBUFFERSIZE)),
bufferindex(0),
bufferbytes(0),
if (filedesc < 0) {
exit(-1);
}
+ if(itype != SATUNE){
+ solver->setInterpreter(itype);
+ }
}
Deserializer::~Deserializer() {
out += bytestocopy;
bytestoread -= bytestocopy;
} else {
- size_t bytesread = read (filedesc, buffer, buffercap);
+ ssize_t bytesread = read (filedesc, buffer, buffercap);
bufferindex = 0;
bufferbytes = bytesread;
if (bytesread == 0) {
case BOOLEANVAR:
deserializeBooleanVar();
break;
+ case BOOLCONST:
+ deserializeBooleanConst();
+ break;
case ORDERCONST:
deserializeBooleanOrder();
break;
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 *));
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;
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;
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);
}
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() {