BooleanOrder (de)serialization works ...

diff --git a/src/AST/astops.h b/src/AST/astops.h
index b92c0e4d06ea0ac64adcc98f6b06764584328531..c3244fb7b2c1fee50cd5ea00fdc8bb22753b3539 100644 (file)
--- a/src/AST/astops.h
+++ b/src/AST/astops.h
@@ -7,7 +7,7 @@ typedef enum FunctionType FunctionType;
 enum PredicateType {TABLEPRED, OPERATORPRED};
 typedef enum PredicateType PredicateType;
 
-enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST, BOOLEANEDGE};
+enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST, BOOLEANEDGE, ORDERTYPE, SETTYPE};
 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 58bc05eaadaf550364bda3f7fe66a8218b3d8f88..1795f17f3de32f07e48fd5d0a27808707499dd91 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -104,7 +104,8 @@ void BooleanVar::serialize(Serializer* serializer){
                return;
        serializer->addObject(this);
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       serializer->mywrite(this, sizeof(BooleanVar*));
+       BooleanVar* This = this;
+       serializer->mywrite(&This, sizeof(BooleanVar*));
        serializer->mywrite(&vtype, sizeof(VarType));
 }
 
@@ -112,10 +113,19 @@ void BooleanOrder::serialize(Serializer* serializer){
        if(serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-//     order->serialize(serializer);
+       order->serialize(serializer);
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       serializer->mywrite(this, sizeof(BooleanOrder*));
+       BooleanOrder* This = this;
+       serializer->mywrite(&This, sizeof(BooleanOrder*));
        serializer->mywrite(&order, sizeof(Order*));
        serializer->mywrite(&first, sizeof(uint64_t));
        serializer->mywrite(&second, sizeof(uint64_t));
 }
+
+void BooleanPredicate::serialize(Serializer* serializer){
+       ASSERT(0);
+}
+
+void BooleanLogic::serialize(Serializer* serializer){
+       ASSERT(0);
+}
\ No newline at end of file

diff --git a/src/AST/order.cc b/src/AST/order.cc
index 609b4691e0db641ef15c24682595417b71478937..3920d3b88b7ac1cfc91e815407bb2c2f9d3a21ae 100644 (file)
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -45,3 +45,16 @@ Order::~Order() {
                delete graph;
        }
 }
+
+void Order::serialize(Serializer* serializer){
+       if(serializer->isSerialized(this))
+               return;
+       serializer->addObject(this);
+       set->serialize(serializer);
+       ASTNodeType asttype = ORDERTYPE;
+       serializer->mywrite(&asttype, sizeof(ASTNodeType));
+       Order* This = this;
+       serializer->mywrite(&This, sizeof(Order*));
+       serializer->mywrite(&type, sizeof(OrderType));
+       serializer->mywrite(&set, sizeof(Set *));
+}

diff --git a/src/AST/order.h b/src/AST/order.h
index b1f0559ed629010310bd344df5b40033a533bfbf..2301d47b41a6faac22d4f34a68aced8daf494a7f 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -7,15 +7,17 @@
 #include "orderencoding.h"
 #include "boolean.h"
 #include "orderpair.h"
+#include "serializable.h"
 
-class Order {
+class Order : public Serializable {
 public:
        Order(OrderType type, Set *set);
-       ~Order();
+       virtual ~Order();
        OrderType type;
        Set *set;
        OrderGraph *graph;
        Order *clone(CSolver *solver, CloneMap *map);
+       void serialize(Serializer *serializer );
        Vector<BooleanOrder *> constraints;
        OrderEncoding encoding;
        void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};

diff --git a/src/AST/set.cc b/src/AST/set.cc
index 4e7383aa7193be39450efa026c4eb97880e87c75..76d6713ad17ebc9f178ee8a506b5f098c44f6bc4 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -1,6 +1,7 @@
 #include "set.h"
 #include <stddef.h>
 #include "csolver.h"
+#include "serializer.h"
 
 Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
        members = new Vector<uint64_t>();
@@ -66,3 +67,24 @@ Set *Set::clone(CSolver *solver, CloneMap *map) {
        map->put(this, s);
        return s;
 }
+
+
+void Set::serialize(Serializer* serializer){
+       if(serializer->isSerialized(this))
+               return;
+       serializer->addObject(this);
+       ASTNodeType asttype = SETTYPE;
+       serializer->mywrite(&asttype, sizeof(ASTNodeType));
+       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));
+       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));
+       }
+}
\ No newline at end of file

diff --git a/src/AST/set.h b/src/AST/set.h
index 5a5cdab1748121606e4e5b1bd4ef0afa5e552c1b..6a41815cfe401eabdfbb0c2814dd1b398c125e9f 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -11,8 +11,9 @@
 #include "classlist.h"
 #include "structs.h"
 #include "mymemory.h"
+#include "serializable.h"
 
-class Set {
+class Set : public Serializable {
 public:
        Set(VarType t);
        Set(VarType t, uint64_t *elements, uint num);
@@ -25,6 +26,7 @@ public:
        uint64_t getMemberAt(uint index);
        uint64_t getElement(uint index);
        virtual Set *clone(CSolver *solver, CloneMap *map);
+       virtual void serialize(Serializer* serializer);
        CMEMALLOC;
 protected:
        VarType type;

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index bf97cbbafb296219b163740e6f59d51a1233c2eb..7616cd7e31a9186b6424eb06bb25704a61fe9c0c 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -26,10 +26,7 @@ Deserializer::~Deserializer() {
 }
 
 ssize_t Deserializer::myread(void* __buf, size_t __nbytes){
-       ssize_t t = read (filedesc, __buf, __nbytes);
-       write (1, __buf, __nbytes);
-       model_print("read\n");
-       return t;
+       return read (filedesc, __buf, __nbytes);
 }
 
 CSolver * Deserializer::deserialize(){
@@ -45,6 +42,12 @@ CSolver * Deserializer::deserialize(){
                        case ORDERCONST:
                                deserializeBooleanOrder();
                                break;
+                       case ORDERTYPE:
+                               deserializeOrder();
+                               break;
+                       case SETTYPE:
+                               deserializeSet();
+                               break;
                        default:
                                ASSERT(0);
                }
@@ -83,4 +86,40 @@ void Deserializer::deserializeBooleanOrder(){
        ASSERT(map.contains(optr));
        Order* order  = (Order*) map.get(optr);
        map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
-}
\ No newline at end of file
+}
+
+void Deserializer::deserializeOrder(){
+       Order* o_ptr;
+       myread(&o_ptr, sizeof(Order*));
+       OrderType type;
+       myread(&type, sizeof(OrderType));
+       Set * set_ptr;
+       myread(&set_ptr, sizeof(Set *));
+       ASSERT(map.contains(set_ptr));
+       Set* set  = (Set*) map.get(set_ptr);
+       map.put(o_ptr, solver->createOrder(type, set));
+}
+
+void Deserializer::deserializeSet(){
+       Set *s_ptr;
+       myread(&s_ptr, sizeof(Set*));
+       VarType type;
+       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));
+       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));
+               members.push(mem);
+       }
+       Set *set = isRange? solver->createRangeSet(type, low, high):
+               solver->createSet(type, members.expose(), size);
+       map.put(s_ptr, set);
+}

diff --git a/src/Serialize/deserializer.h b/src/Serialize/deserializer.h
index 7e26cf327ac3185ce7bcebe890312703072c2924..7c7d39a9b598353b1d57b135038082b7692c7b1a 100644 (file)
--- a/src/Serialize/deserializer.h
+++ b/src/Serialize/deserializer.h
@@ -27,6 +27,8 @@ private:
        void deserializeBooleanEdge();
        void deserializeBooleanVar();
        void deserializeBooleanOrder();
+       void deserializeOrder();
+       void deserializeSet();
        CSolver *solver;
        int filedesc;
        CloneMap map;

diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc
index bf894563cdb749ef3bb7108a74107a56d44acd3e..783cf88a8f91aaa46b2ea837a567c984e197e77d 100644 (file)
--- a/src/Serialize/serializer.cc
+++ b/src/Serialize/serializer.cc
@@ -26,18 +26,14 @@ Serializer::~Serializer() {
 }
 
 void Serializer::mywrite(const void *__buf, size_t __n){
-       write (1, __buf, __n);
-       model_print("\n");
        write (filedesc, __buf, __n);
 }
 
 
 void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be){
-       if(serializer->isSerialized(be.getRaw()))
-               return;
-       serializer->addObject(be.getRaw());
        be.getBoolean()->serialize(serializer);
        ASTNodeType type = BOOLEANEDGE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       serializer->mywrite(be.getRaw(), sizeof(Boolean*));
+       Boolean* boolean = be.getRaw();
+       serializer->mywrite(&boolean, sizeof(Boolean*));
 }
\ No newline at end of file

diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc
index e01fb8f8e315aeb7032f7a6345948b8a2fed2ce9..46bc2a302d5885e4428374c3f8f476aa0fe4ea88 100644 (file)
--- 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/ordertest.cc b/src/Test/ordertest.cc
index d9ad852594103b727690c870deb75a8aa101a212..9ffcab56c91acf7efab1f200e02b9a021451c881 100644 (file)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -15,6 +15,7 @@ int main(int numargs, char **argv) {
        BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
        solver->addConstraint(b1);
        solver->addConstraint(b2);
+       solver->serialize();
        if (solver->solve() == 1){
                printf("SAT\n");
                printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 

diff --git a/src/csolver.cc b/src/csolver.cc
index bbe2b0c2c28c744ba9c001ca5467217093098839..ce749b13c27b20d1645383f86e27f5101e3a6234 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -87,6 +87,7 @@ CSolver *CSolver::clone() {
 }
 
 void CSolver::serialize() {
+       model_print("serializing ...\n");
        {
                Serializer serializer("dump");
                SetIteratorBooleanEdge *it = getConstraints();