From: Hamed Gorjiara Date: Mon, 23 Oct 2017 09:35:11 +0000 (-0700) Subject: After resolving conflicts X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=cfbb106cf7c1281029b012c47580c9f14df1014b;p=satune.git After resolving conflicts --- cfbb106cf7c1281029b012c47580c9f14df1014b diff --cc src/AST/element.h index 1b79084,b74e582..1e7b1f2 --- a/src/AST/element.h +++ b/src/AST/element.h @@@ -26,14 -26,13 +26,14 @@@ public class ElementSet : public Element { public: ElementSet(ASTNodeType type, Set *s); + virtual ~ElementSet(){} ElementSet(Set *s); virtual Element *clone(CSolver *solver, CloneMap *map); - virtual void serialize(Serializer* serializer); - virtual void print(); + virtual void serialize(Serializer *serializer); + virtual void print(); CMEMALLOC; Set *getRange() {return set;} - protected: + protected: Set *set; }; @@@ -41,10 -40,9 +41,10 @@@ class ElementConst : public ElementSet { public: ElementConst(uint64_t value, Set *_set); + virtual ~ElementConst(){} uint64_t value; - virtual void serialize(Serializer* serializer); - virtual void print(); + virtual void serialize(Serializer *serializer); + virtual void print(); Element *clone(CSolver *solver, CloneMap *map); CMEMALLOC; }; diff --cc src/AST/set.cc index 5c07ac5,0a6e14f..52494e3 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@@ -127,36 -135,33 +135,36 @@@ void Set::serialize(Serializer *seriali serializer->addObject(this); ASTNodeType asttype = SETTYPE; serializer->mywrite(&asttype, sizeof(ASTNodeType)); - Set* This = this; - serializer->mywrite(&This, sizeof(Set*)); + Set *This = this; + serializer->mywrite(&This, sizeof(Set *)); serializer->mywrite(&type, sizeof(VarType)); serializer->mywrite(&isRange, sizeof(bool)); - serializer->mywrite(&low, sizeof(uint64_t)); - serializer->mywrite(&high, sizeof(uint64_t)); - bool isMutable = isMutableSet(); + bool isMutable = isMutableSet(); serializer->mywrite(&isMutable, sizeof(bool)); - uint size = members->getSize(); - serializer->mywrite(&size, sizeof(uint)); - for (uint i = 0; i < size; i++) { - uint64_t mem = members->get(i); - serializer->mywrite(&mem, sizeof(uint64_t)); - } + if(isRange){ + serializer->mywrite(&low, sizeof(uint64_t)); + serializer->mywrite(&high, sizeof(uint64_t)); + }else { + uint size = members->getSize(); + serializer->mywrite(&size, sizeof(uint)); + for(uint i=0; iget(i); + serializer->mywrite(&mem, sizeof(uint64_t)); + } + } } - void Set::print(){ + void Set::print() { model_print("{Set:"); - if(isRange){ - model_print("Range: low=%lu, high=%lu}\n\n", low, high); - } else { - uint size = members->getSize(); - model_print("Members: "); - for(uint i=0; iget(i); - model_print("%lu, ", mem); - } - model_println("}\n"); - } + if (isRange) { + model_print("Range: low=%lu, high=%lu}", low, high); + } else { + uint size = members->getSize(); + model_print("Members: "); + for (uint i = 0; i < size; i++) { + uint64_t mem = members->get(i); + model_print("%lu, ", mem); + } + model_print("}"); + } } diff --cc src/Serialize/deserializer.cc index bffb901,cd1e1a2..6f14484 --- a/src/Serialize/deserializer.cc +++ b/src/Serialize/deserializer.cc @@@ -145,40 -145,36 +145,39 @@@ void Deserializer::deserializeSet() myread(&type, sizeof(VarType)); bool isRange; myread(&isRange, sizeof(bool)); - uint64_t low; - myread(&low, sizeof(uint64_t)); - uint64_t high; - myread(&high, sizeof(uint64_t)); - bool isMutable; + bool isMutable; myread(&isMutable, sizeof(bool)); - Set *set; - if (isMutable) { - set = new MutableSet(type); - } - uint size; - myread(&size, sizeof(uint)); - Vector 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 = isRange ? solver->createRangeSet(type, low, high) : - 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; + if(isMutable){ + set = new MutableSet(type); + } + uint size; + myread(&size, sizeof(uint)); + Vector members; + for(uint i=0; iaddElementMSet(mem); + }else { + members.push(mem); + } + } + if(!isMutable){ + set = solver->createSet(type, members.expose(), size); + } + map.put(s_ptr, set); + } - } - void Deserializer::deserializeBooleanLogic(){ + void Deserializer::deserializeBooleanLogic() { BooleanLogic *bl_ptr; myread(&bl_ptr, sizeof(BooleanLogic *)); LogicOp op; @@@ -376,15 -372,15 +375,15 @@@ void Deserializer::deserializeFunctionO map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior)); } - void Deserializer::deserializeFunctionTable(){ + void Deserializer::deserializeFunctionTable() { FunctionTable *ft_ptr; myread(&ft_ptr, sizeof(FunctionTable *)); - Table* table; - myread(&table, sizeof(Table*)); + Table *table; + myread(&table, sizeof(Table *)); ASSERT(map.contains(table)); - table = (Table*) map.get(table); + table = (Table *) map.get(table); UndefinedBehavior undefinedbehavior; myread(&undefinedbehavior, sizeof(UndefinedBehavior)); - + map.put(ft_ptr, solver->completeTable(table, undefinedbehavior)); --} ++} diff --cc src/common.h index fac5a0b,52c0b5f..0efebf8 --- a/src/common.h +++ b/src/common.h @@@ -18,20 -18,22 +18,23 @@@ #include "config.h" #include "time.h" -/* - extern int model_out; - extern int model_err; - extern int switch_alloc; + - #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0) - #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0) - #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0) +#if 1 +extern int model_out; +extern int model_err; +extern int switch_alloc; - #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0) +#define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0) + +#define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0) +#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0) +#else + #define model_print printf +#endif +#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0) - #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0) - */ + -#define model_print printf + #define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1)))) #define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x)) diff --cc src/csolver.cc index d2e44b4,311ad0f..8132991 --- a/src/csolver.cc +++ b/src/csolver.cc @@@ -101,12 -98,12 +101,11 @@@ void CSolver::serialize() } delete it; } - model_print("deserializing ...\n"); - { - Deserializer deserializer("dump"); - deserializer.deserialize(); - } - +// model_print("deserializing ...\n"); +// { +// Deserializer deserializer("dump"); +// deserializer.deserialize(); +// } - } Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) { @@@ -417,27 -393,18 +398,21 @@@ BooleanEdge CSolver::orderConstraint(Or } void CSolver::addConstraint(BooleanEdge constraint) { +#ifdef TRACE_DEBUG + model_println("****New Constraint******"); +#endif if (isTrue(constraint)) return; - else if (isFalse(constraint)){ - int t=0; - #ifdef TRACE_DEBUG - model_println("Adding constraint which is false :|"); - #endif - setUnSAT(); - } + else if (isFalse(constraint)) { + int t = 0; + setUnSAT(); + } else { if (constraint->type == LOGICOP) { - BooleanLogic *b=(BooleanLogic *) constraint.getBoolean(); + BooleanLogic *b = (BooleanLogic *) constraint.getBoolean(); if (!constraint.isNegated()) { - if (b->op==SATC_AND) { - for(uint i=0;iinputs.getSize();i++) { - #ifdef TRACE_DEBUG - model_println("In loop"); - #endif + if (b->op == SATC_AND) { + for (uint i = 0; i < b->inputs.getSize(); i++) { addConstraint(b->inputs.get(i)); } return;