From: Hamed Date: Sun, 10 Sep 2017 06:59:38 +0000 (-0700) Subject: completed serializer/deserializer X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=3c0ccc94fed7aeec6c3de6c27708e31807a56021 completed serializer/deserializer --- diff --git a/src/AST/astops.h b/src/AST/astops.h index c3244fb..f26326f 100644 --- a/src/AST/astops.h +++ b/src/AST/astops.h @@ -7,7 +7,8 @@ typedef enum FunctionType FunctionType; enum PredicateType {TABLEPRED, OPERATORPRED}; typedef enum PredicateType PredicateType; -enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST, BOOLEANEDGE, ORDERTYPE, SETTYPE}; +enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST, + BOOLEANEDGE, ORDERTYPE, SETTYPE, PREDTABLETYPE, PREDOPERTYPE, TABLETYPE, FUNCTABLETYPE, FUNCOPTYPE}; typedef enum ASTNodeType ASTNodeType; enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3}; diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 1795f17..565e0ef 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -123,9 +123,48 @@ void BooleanOrder::serialize(Serializer* serializer){ } void BooleanPredicate::serialize(Serializer* serializer){ - ASSERT(0); + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + predicate->serialize(serializer); + uint size = inputs.getSize(); + for(uint i=0; iserialize(serializer); + } + serializeBooleanEdge(serializer, undefStatus); + + serializer->mywrite(&type, sizeof(ASTNodeType)); + BooleanPredicate* This = this; + serializer->mywrite(&This, sizeof(BooleanPredicate*)); + serializer->mywrite(&predicate, sizeof(Predicate *)); + serializer->mywrite(&size, sizeof(uint)); + for(uint i=0; imywrite(&input, sizeof(Element *)); + } + Boolean* undefStat = undefStatus.getRaw(); + serializer->mywrite(&undefStat, sizeof(Boolean*)); } void BooleanLogic::serialize(Serializer* serializer){ - ASSERT(0); -} \ No newline at end of file + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + uint size = inputs.getSize(); + for(uint i=0; imywrite(&type, sizeof(ASTNodeType)); + BooleanLogic* This = this; + serializer->mywrite(&This, sizeof(BooleanLogic*)); + serializer->mywrite(&op, sizeof(LogicOp)); + serializer->mywrite(&size, sizeof(uint)); + for(uint i=0; imywrite(&input, sizeof(Boolean*)); + } +} + diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 1c45f04..df1f4e8 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -8,10 +8,9 @@ #include "astnode.h" #include "functionencoding.h" #include "constraint.h" -#include "serializable.h" #include "serializer.h" -class Boolean : public ASTNode, public Serializable { +class Boolean : public ASTNode { public: Boolean(ASTNodeType _type); virtual ~Boolean() {} diff --git a/src/AST/element.cc b/src/AST/element.cc index 05f6cef..2617022 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -63,3 +63,58 @@ void ElementFunction::updateParents() { Set * ElementFunction::getRange() { return function->getRange(); } + +void ElementSet::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + set->serialize(serializer); + + serializer->mywrite(&type, sizeof(ASTNodeType)); + ElementSet *This = this; + serializer->mywrite(&This, sizeof(ElementSet*)); + serializer->mywrite(&set, sizeof(Set*)); +} + +void ElementConst::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + set->serialize(serializer); + + serializer->mywrite(&type, sizeof(ASTNodeType)); + ElementSet *This = this; + serializer->mywrite(&This, sizeof(ElementSet*)); + VarType type = set->getType(); + serializer->mywrite(&type, sizeof(VarType)); + serializer->mywrite(&value, sizeof(uint64_t)); +} + +void ElementFunction::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + function->serialize(serializer); + uint size = inputs.getSize(); + for(uint i=0; iserialize(serializer); + } + serializeBooleanEdge(serializer, overflowstatus); + + serializer->mywrite(&type, sizeof(ASTNodeType)); + ElementFunction *This = this; + serializer->mywrite(&This, sizeof(ElementFunction *)); + serializer->mywrite(&function, sizeof(Function *)); + serializer->mywrite(&size, sizeof(uint)); + for(uint i=0; imywrite(&input, sizeof(Element*)); + } + Boolean* overflowstat = overflowstatus.getRaw(); + serializer->mywrite(&overflowstat, sizeof(Boolean*)); +} + diff --git a/src/AST/element.h b/src/AST/element.h index 076e831..19e35b6 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -15,6 +15,7 @@ public: Vector parents; ElementEncoding encoding; virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}; + virtual void serialize(Serializer* serializer) =0; virtual void updateParents() {} virtual Set * getRange() = 0; CMEMALLOC; @@ -25,9 +26,10 @@ public: ElementSet(ASTNodeType type, Set *s); ElementSet(Set *s); virtual Element *clone(CSolver *solver, CloneMap *map); + virtual void serialize(Serializer* serializer); CMEMALLOC; Set *getRange() {return set;} - private: + protected: Set *set; }; @@ -36,6 +38,7 @@ class ElementConst : public ElementSet { public: ElementConst(uint64_t value, Set *_set); uint64_t value; + virtual void serialize(Serializer* serializer); Element *clone(CSolver *solver, CloneMap *map); CMEMALLOC; }; @@ -48,6 +51,7 @@ public: BooleanEdge overflowstatus; FunctionEncoding functionencoding; Element *clone(CSolver *solver, CloneMap *map); + virtual void serialize(Serializer* serializer); Set * getRange(); void updateParents(); CMEMALLOC; diff --git a/src/AST/function.cc b/src/AST/function.cc index a882580..96b0797 100644 --- a/src/AST/function.cc +++ b/src/AST/function.cc @@ -2,6 +2,7 @@ #include "table.h" #include "set.h" #include "csolver.h" +#include "serializer.h" FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) : Function(OPERATORFUNC), @@ -64,3 +65,45 @@ Function *FunctionTable::clone(CSolver *solver, CloneMap *map) { Set * FunctionTable::getRange() { return table->getRange(); } + +void FunctionTable::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + table->serialize(serializer); + + ASTNodeType type = FUNCTABLETYPE; + serializer->mywrite(&type, sizeof(ASTNodeType)); + FunctionTable* This = this; + serializer->mywrite(&This, sizeof(FunctionTable*)); + serializer->mywrite(&table, sizeof(Table *)); + serializer->mywrite(&undefBehavior, sizeof(UndefinedBehavior)); + +} + +void FunctionOperator::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + uint size = domains.getSize(); + for(uint i=0; iserialize(serializer); + } + range->serialize(serializer); + + ASTNodeType nodeType = FUNCOPTYPE; + serializer->mywrite(&nodeType, sizeof(ASTNodeType)); + FunctionOperator* This = this; + serializer->mywrite(&This, sizeof(FunctionOperator*)); + serializer->mywrite(&op, sizeof(ArithOp)); + serializer->mywrite(&size, sizeof(uint)); + for(uint i=0; imywrite(&domain, sizeof(Set *)); + } + serializer->mywrite(&range, sizeof(Set *)); + serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior)); +} \ No newline at end of file diff --git a/src/AST/function.h b/src/AST/function.h index f34c02e..98ef536 100644 --- a/src/AST/function.h +++ b/src/AST/function.h @@ -12,6 +12,7 @@ public: FunctionType type; virtual ~Function() {} virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;} + virtual void serialize(Serializer* serialiezr) =0; virtual Set * getRange() = 0; CMEMALLOC; }; @@ -26,6 +27,7 @@ public: uint64_t applyFunctionOperator(uint numVals, uint64_t *values); bool isInRangeFunction(uint64_t val); Function *clone(CSolver *solver, CloneMap *map); + virtual void serialize(Serializer* serialiezr); Set * getRange() {return range;} CMEMALLOC; }; @@ -36,6 +38,7 @@ public: UndefinedBehavior undefBehavior; FunctionTable (Table *table, UndefinedBehavior behavior); Function *clone(CSolver *solver, CloneMap *map); + virtual void serialize(Serializer* serialiezr); Set * getRange(); CMEMALLOC; }; diff --git a/src/AST/order.h b/src/AST/order.h index 2301d47..b8ca724 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -7,9 +7,8 @@ #include "orderencoding.h" #include "boolean.h" #include "orderpair.h" -#include "serializable.h" -class Order : public Serializable { +class Order{ public: Order(OrderType type, Set *set); virtual ~Order(); diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc index d359811..7f63faa 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -50,3 +50,42 @@ Predicate *PredicateTable::clone(CSolver *solver, CloneMap *map) { map->put(this, p); return p; } + +void PredicateTable::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + table->serialize(serializer); + + ASTNodeType type = PREDTABLETYPE; + serializer->mywrite(&type, sizeof(ASTNodeType)); + PredicateTable* This = this; + serializer->mywrite(&This, sizeof(PredicateTable*)); + serializer->mywrite(&table, sizeof(Table *)); + serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior)); +} + +void PredicateOperator::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + uint size = domains.getSize(); + for(uint i=0; iserialize(serializer); + } + + ASTNodeType type = PREDOPERTYPE; + serializer->mywrite(&type, sizeof(ASTNodeType)); + PredicateOperator* This = this; + serializer->mywrite(&This, sizeof(PredicateOperator*)); + serializer->mywrite(&op, sizeof(CompOp)); + serializer->mywrite(&size, sizeof(uint)); + for(uint i=0; imywrite(&domain, sizeof(Set*)); + } +} + diff --git a/src/AST/predicate.h b/src/AST/predicate.h index 183a960..2f292b2 100644 --- a/src/AST/predicate.h +++ b/src/AST/predicate.h @@ -12,6 +12,7 @@ public: Predicate(PredicateType _type) : type(_type) {} virtual ~Predicate() {} virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;} + virtual void serialize(Serializer* serializer) = 0; PredicateType type; CMEMALLOC; }; @@ -21,6 +22,7 @@ public: PredicateOperator(CompOp op, Set **domain, uint numDomain); bool evalPredicateOperator(uint64_t *inputs); Predicate *clone(CSolver *solver, CloneMap *map); + virtual void serialize(Serializer* serializer); CompOp op; Array domains; CMEMALLOC; @@ -30,6 +32,7 @@ class PredicateTable : public Predicate { public: PredicateTable(Table *table, UndefinedBehavior undefBehavior); Predicate *clone(CSolver *solver, CloneMap *map); + virtual void serialize(Serializer* serializer); Table *table; UndefinedBehavior undefinedbehavior; CMEMALLOC; diff --git a/src/AST/set.h b/src/AST/set.h index 6a41815..6dbeac0 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -11,9 +11,8 @@ #include "classlist.h" #include "structs.h" #include "mymemory.h" -#include "serializable.h" -class Set : public Serializable { +class Set { public: Set(VarType t); Set(VarType t, uint64_t *elements, uint num); diff --git a/src/AST/table.cc b/src/AST/table.cc index e0f735f..4ce6270 100644 --- a/src/AST/table.cc +++ b/src/AST/table.cc @@ -5,6 +5,7 @@ #include "set.h" #include "mutableset.h" #include "csolver.h" +#include "serializer.h" Table::Table(Set **_domains, uint numDomain, Set *_range) : domains(_domains, numDomain), @@ -58,3 +59,40 @@ Table::~Table() { delete entries; } + + +void Table::serialize(Serializer* serializer){ + if(serializer->isSerialized(this)) + return; + serializer->addObject(this); + + uint size = domains.getSize(); + for(uint i=0; iserialize(serializer); + } + range->serialize(serializer); + + ASTNodeType type = TABLETYPE; + serializer->mywrite(&type, sizeof(ASTNodeType)); + Table* This = this; + serializer->mywrite(&This, sizeof(Table*)); + serializer->mywrite(&size, sizeof(uint)); + for(uint i=0; imywrite(&domain, sizeof(Set*)); + } + serializer->mywrite(&range, sizeof(Set*)); + size = entries->getSize(); + serializer->mywrite(&size, sizeof(uint)); + SetIteratorTableEntry* iterator = getEntries(); + while(iterator->hasNext()){ + TableEntry* entry = iterator->next(); + serializer->mywrite(&entry->output, sizeof(uint64_t)); + serializer->mywrite(&entry->inputSize, sizeof(uint)); + serializer->mywrite(entry->inputs, sizeof(uint64_t) * entry->inputSize); + ASSERT(0); + } +} + + diff --git a/src/AST/table.h b/src/AST/table.h index 6c7926e..db8d188 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -10,6 +10,7 @@ public: void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result); TableEntry *getTableEntry(uint64_t *inputs, uint inputSize); Table *clone(CSolver *solver, CloneMap *map); + void serialize(Serializer *serializer); ~Table(); Set * getRange() {return range;} diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc index 7616cd7..2b431de 100644 --- a/src/Serialize/deserializer.cc +++ b/src/Serialize/deserializer.cc @@ -10,6 +10,9 @@ #include "csolver.h" #include "unistd.h" #include "fcntl.h" +#include "predicate.h" +#include "table.h" +#include "element.h" Deserializer::Deserializer(const char* file): solver(new CSolver()) @@ -48,6 +51,36 @@ CSolver * Deserializer::deserialize(){ case SETTYPE: deserializeSet(); break; + case LOGICOP: + deserializeBooleanLogic(); + break; + case PREDICATEOP: + deserializeBooleanPredicate(); + break; + case PREDTABLETYPE: + deserializePredicateTable(); + break; + case PREDOPERTYPE: + deserializePredicateOperator(); + break; + case TABLETYPE: + deserializeTable(); + break; + case ELEMSET: + deserializeElementSet(); + break; + case ELEMCONST: + deserializeElementConst(); + break; + case ELEMFUNCRETURN: + deserializeElementFunction(); + break; + case FUNCOPTYPE: + deserializeFunctionOperator(); + break; + case FUNCTABLETYPE: + deserializeFunctionTable(); + break; default: ASSERT(0); } @@ -123,3 +156,202 @@ void Deserializer::deserializeSet(){ solver->createSet(type, members.expose(), size); map.put(s_ptr, set); } + +void Deserializer::deserializeBooleanLogic(){ + BooleanLogic *bl_ptr; + myread(&bl_ptr, sizeof(BooleanLogic *)); + LogicOp op; + myread(&op, sizeof(LogicOp)); + uint size; + myread(&size, sizeof(uint)); + Vector members; + for(uint i=0; iapplyLogicalOperation(op, members.expose(), size).getBoolean()); +} + +void Deserializer::deserializeBooleanPredicate(){ + BooleanPredicate *bp_ptr; + myread(&bp_ptr, sizeof(BooleanPredicate *)); + Predicate* predicate; + myread(&predicate, sizeof(Predicate*)); + ASSERT(map.contains(predicate)); + predicate = (Predicate*) map.get(predicate); + uint size; + myread(&size, sizeof(uint)); + Vector members; + for(uint i=0; iapplyPredicateTable(predicate, members.expose(), size, undefStatus).getBoolean()); +} + +void Deserializer::deserializePredicateTable(){ + PredicateTable *pt_ptr; + myread(&pt_ptr, sizeof(PredicateTable *)); + Table* table; + myread(&table, sizeof(Table*)); + ASSERT(map.contains(table)); + table = (Table*) map.get(table); + UndefinedBehavior undefinedbehavior; + myread(&undefinedbehavior, sizeof(UndefinedBehavior)); + + map.put(pt_ptr, solver->createPredicateTable(table, undefinedbehavior)); +} + +void Deserializer::deserializePredicateOperator(){ + PredicateOperator *po_ptr; + myread(&po_ptr, sizeof(PredicateOperator *)); + CompOp op; + myread(&op, sizeof(CompOp)); + uint size; + myread(&size, sizeof(uint)); + Vector domains; + for(uint i=0; icreatePredicateOperator(op, domains.expose(), size)); +} + +void Deserializer::deserializeTable(){ + Table *t_ptr; + myread(&t_ptr, sizeof(Table *)); + uint size; + myread(&size, sizeof(uint)); + Vector domains; + for(uint i=0; icreateTable(domains.expose(), size, range); + myread(&size, sizeof(uint)); + for(uint i=0; i inputs; + inputs.setSize(inputSize); + myread(inputs.expose(), sizeof(uint64_t)*inputSize); + ASSERT(0); + table->addNewTableEntry(inputs.expose(), inputSize, output); + } + + map.put(t_ptr, table); +} + + +void Deserializer::deserializeElementSet(){ + 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)); +} + +void Deserializer::deserializeElementConst(){ + 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)); +} + +void Deserializer::deserializeElementFunction(){ + ElementFunction *ef_ptr; + myread(&ef_ptr, sizeof(ElementFunction *)); + Function *function; + myread(&function, sizeof(Function*)); + ASSERT(map.contains(function)); + function = (Function*) map.get(function); + uint size; + myread(&size, sizeof(uint)); + Vector members; + for(uint i=0; iapplyFunction(function, members.expose(), size, undefStatus)); +} + + +void Deserializer::deserializeFunctionOperator(){ + FunctionOperator *fo_ptr; + myread(&fo_ptr, sizeof(FunctionOperator *)); + ArithOp op; + myread(&op, sizeof(ArithOp)); + uint size; + myread(&size, sizeof(uint)); + Vector domains; + for(uint i=0; icreateFunctionOperator(op, domains.expose(), size, range, overflowbehavior)); +} + +void Deserializer::deserializeFunctionTable(){ + FunctionTable *ft_ptr; + myread(&ft_ptr, sizeof(FunctionTable *)); + Table* table; + myread(&table, sizeof(Table*)); + ASSERT(map.contains(table)); + table = (Table*) map.get(table); + UndefinedBehavior undefinedbehavior; + myread(&undefinedbehavior, sizeof(UndefinedBehavior)); + + map.put(ft_ptr, solver->completeTable(table, undefinedbehavior)); +} \ No newline at end of file diff --git a/src/Serialize/deserializer.h b/src/Serialize/deserializer.h index 7c7d39a..057346d 100644 --- a/src/Serialize/deserializer.h +++ b/src/Serialize/deserializer.h @@ -29,6 +29,16 @@ private: void deserializeBooleanOrder(); void deserializeOrder(); void deserializeSet(); + void deserializeBooleanLogic(); + void deserializeBooleanPredicate(); + void deserializePredicateTable(); + void deserializePredicateOperator(); + void deserializeTable(); + void deserializeElementSet(); + void deserializeElementConst(); + void deserializeElementFunction(); + void deserializeFunctionOperator(); + void deserializeFunctionTable(); CSolver *solver; int filedesc; CloneMap map; diff --git a/src/Serialize/serializable.h b/src/Serialize/serializable.h deleted file mode 100644 index a5e769d..0000000 --- a/src/Serialize/serializable.h +++ /dev/null @@ -1,17 +0,0 @@ - -/* - * File: serializable.h - * Author: hamed - * - * Created on September 7, 2017, 3:39 PM - */ - -#ifndef SERIALIZABLE_H -#define SERIALIZABLE_H - -class Serializable{ - virtual void serialize(Serializer* ) = 0; -}; - -#endif /* SERIALIZABLE_H */ - diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc index 783cf88..524f9ee 100644 --- a/src/Serialize/serializer.cc +++ b/src/Serialize/serializer.cc @@ -30,7 +30,7 @@ void Serializer::mywrite(const void *__buf, size_t __n){ } -void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be){ +void serializeBooleanEdge(Serializer* serializer, BooleanEdge be){ be.getBoolean()->serialize(serializer); ASTNodeType type = BOOLEANEDGE; serializer->mywrite(&type, sizeof(ASTNodeType)); diff --git a/src/Serialize/serializer.h b/src/Serialize/serializer.h index eb114dc..12bff13 100644 --- a/src/Serialize/serializer.h +++ b/src/Serialize/serializer.h @@ -31,7 +31,7 @@ inline bool Serializer::isSerialized(void* obj){ -void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be); +void serializeBooleanEdge(Serializer* serializer, BooleanEdge be); #endif /* SERIALIZER_H */ diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc index 46bc2a3..e01fb8f 100644 --- a/src/Test/buildconstraintstest.cc +++ b/src/Test/buildconstraintstest.cc @@ -50,7 +50,7 @@ int main(int numargs, char **argv) { Element *inputs2 [] = {e4, e3}; BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2); solver->addConstraint(pred); -// solver->serialize(); + solver->serialize(); if (solver->solve() == 1) printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2)); else diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc index aeab4a5..e041cb0 100644 --- a/src/Test/elemequalsattest.cc +++ b/src/Test/elemequalsattest.cc @@ -24,6 +24,7 @@ int main(int numargs, char **argv) { Element *inputs[] = {e1, e2}; BooleanEdge b = solver->applyPredicate(equals, inputs, 2); solver->addConstraint(b); + solver->serialize(); if (solver->solve() == 1) printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2)); diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc index 6a7a067..123d6cd 100644 --- a/src/Test/elemequalunsattest.cc +++ b/src/Test/elemequalunsattest.cc @@ -19,7 +19,7 @@ int main(int numargs, char **argv) { Element *inputs[] = {e1, e2}; BooleanEdge b = solver->applyPredicate(equals, inputs, 2); solver->addConstraint(b); - + solver->serialize(); if (solver->solve() == 1) printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2)); else diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc index e3baeb9..72a0a83 100644 --- a/src/Test/funcencodingtest.cc +++ b/src/Test/funcencodingtest.cc @@ -72,6 +72,7 @@ int main(int numargs, char **argv) { Element *inputs2 [] = {e7, e6}; BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2); solver->addConstraint(pred); + solver->serialize(); if (solver->solve() == 1) printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n", diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc index 9b20015..7b30f80 100644 --- a/src/Test/logicopstest.cc +++ b/src/Test/logicopstest.cc @@ -24,6 +24,7 @@ int main(int numargs, char **argv) { solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2)); BooleanEdge barray5[] = {b1, b4}; solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2)); + solver->serialize(); if (solver->solve() == 1) printf("b1=%d b2=%d b3=%d b4=%d\n", solver->getBooleanValue(b1), solver->getBooleanValue(b2), diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc index d666833..11a315c 100644 --- a/src/Test/ltelemconsttest.cc +++ b/src/Test/ltelemconsttest.cc @@ -18,6 +18,7 @@ int main(int numargs, char **argv) { Element *inputs2[] = {e1, e2}; BooleanEdge b = solver->applyPredicate(lt, inputs2, 2); solver->addConstraint(b); + solver->serialize(); if (solver->solve() == 1) printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2)); else diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc index 80a57ff..fea3a9f 100644 --- a/src/Test/ordergraphtest.cc +++ b/src/Test/ordergraphtest.cc @@ -45,7 +45,7 @@ int main(int numargs, char **argv) { BooleanEdge array12[] = {o58, o81}; solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) ); - + solver->serialize(); /* if (solver->solve() == 1) printf("SAT\n"); else diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc index 11017c6..680d1c6 100644 --- a/src/Test/tablefuncencodetest.cc +++ b/src/Test/tablefuncencodetest.cc @@ -49,6 +49,7 @@ int main(int numargs, char **argv) { Element *inputs2 [] = {e4, e3}; BooleanEdge pred = solver->applyPredicate(lte, inputs2, 2); solver->addConstraint(pred); + solver->serialize(); if (solver->solve() == 1) printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " e4=%" PRIu64 " overFlow:%d\n", diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc index 47113fd..4007e25 100644 --- a/src/Test/tablepredicencodetest.cc +++ b/src/Test/tablepredicencodetest.cc @@ -57,6 +57,7 @@ int main(int numargs, char **argv) { Element *tmparray2[] = {e1, e2}; BooleanEdge pred2 = solver->applyPredicate(eq, tmparray2, 2); solver->addConstraint(pred2); + solver->serialize(); if (solver->solve() == 1) printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " undefFlag:%d\n",