#include "element.h"
#include "mutableset.h"
-Deserializer::Deserializer(const char *file) :
+#define READBUFFERSIZE 16384
+
+Deserializer::Deserializer(const char *file, bool alloy) :
+ buffer((char *) ourmalloc(READBUFFERSIZE)),
+ bufferindex(0),
+ bufferbytes(0),
+ buffercap(READBUFFERSIZE),
solver(new CSolver())
{
filedesc = open(file, O_RDONLY);
if (filedesc < 0) {
exit(-1);
}
+ if(alloy){
+ solver->setAlloyEncoder();
+ }
}
Deserializer::~Deserializer() {
- delete solver;
-
if (-1 == close(filedesc)) {
exit(-1);
}
+ ourfree(buffer);
}
-ssize_t Deserializer::myread(void *__buf, size_t __nbytes) {
- return read (filedesc, __buf, __nbytes);
+ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
+ char *out = (char * ) __buf;
+ size_t totalbytesread = 0;
+ while (bytestoread) {
+ if (bufferbytes != 0) {
+ uint bytestocopy = (bufferbytes > bytestoread) ? bytestoread : bufferbytes;
+ memcpy(out, &buffer[bufferindex], bytestocopy);
+ //update local buffer
+ bufferbytes -= bytestocopy;
+ bufferindex += bytestocopy;
+ totalbytesread += bytestocopy;
+ //update request pointers
+ out += bytestocopy;
+ bytestoread -= bytestocopy;
+ } else {
+ ssize_t bytesread = read (filedesc, buffer, buffercap);
+ bufferindex = 0;
+ bufferbytes = bytesread;
+ if (bytesread == 0) {
+ break;
+ } else if (bytesread < 0) {
+ exit(-1);
+ }
+ }
+ }
+ return totalbytesread;
}
CSolver *Deserializer::deserialize() {
case BOOLEANVAR:
deserializeBooleanVar();
break;
+ case BOOLCONST:
+ deserializeBooleanConst();
+ break;
case ORDERCONST:
deserializeBooleanOrder();
break;
}
void Deserializer::deserializeBooleanEdge() {
- Boolean *b;
- myread(&b, sizeof(Boolean *));
- BooleanEdge tmp(b);
+ Boolean *b_ptr;
+ myread(&b_ptr, sizeof(Boolean *));
+ BooleanEdge tmp(b_ptr);
bool isNegated = tmp.isNegated();
ASSERT(map.contains(tmp.getBoolean()));
- b = (Boolean *) map.get(tmp.getBoolean());
- BooleanEdge res(b);
- solver->addConstraint(isNegated ? res.negate() : res);
+ b_ptr = (Boolean *) map.get(tmp.getBoolean());
+ BooleanEdge res(b_ptr);
+ bool isTopLevel;
+ myread(&isTopLevel, sizeof(bool));
+ if (isTopLevel) {
+ solver->addConstraint(isNegated ? res.negate() : res);
+ }
}
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 *));
myread(&type, sizeof(VarType));
bool isRange;
myread(&isRange, sizeof(bool));
- bool isMutable;
+ bool isMutable;
myread(&isMutable, sizeof(bool));
- if(isRange){
- uint64_t low;
- myread(&low, sizeof(uint64_t));
- uint64_t high;
- myread(&high, sizeof(uint64_t));
- map.put(s_ptr, new Set(type, low, high));
- } else{
- Set *set;
- if(isMutable){
- set = new MutableSet(type);
- }
- uint size;
- myread(&size, sizeof(uint));
- Vector<uint64_t> members;
- for(uint i=0; i<size; i++){
- uint64_t mem;
- myread(&mem, sizeof(uint64_t));
- if(isMutable) {
- ((MutableSet*) set)->addElementMSet(mem);
- }else {
- members.push(mem);
- }
- }
- if(!isMutable){
- set = solver->createSet(type, members.expose(), size);
- }
- map.put(s_ptr, set);
- }
+ if (isRange) {
+ uint64_t low;
+ myread(&low, sizeof(uint64_t));
+ uint64_t high;
+ myread(&high, sizeof(uint64_t));
+ map.put(s_ptr, new Set(type, low, high));
+ } else {
+ Set *set = NULL;
+ if (isMutable) {
+ set = new MutableSet(type);
+ }
+ uint size;
+ myread(&size, sizeof(uint));
+ Vector<uint64_t> members;
+ for (uint i = 0; i < size; i++) {
+ uint64_t mem;
+ myread(&mem, sizeof(uint64_t));
+ if (isMutable) {
+ ((MutableSet *) set)->addElementMSet(mem);
+ } else {
+ members.push(mem);
+ }
+ }
+ if (!isMutable) {
+ set = solver->createSet(type, members.expose(), size);
+ }
+ map.put(s_ptr, set);
+ }
}
void Deserializer::deserializeBooleanLogic() {
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() {
projects / satune.git / blobdiff