Merge

diff --combined src/AST/astops.h
index 8ddbdd11dff336c4df174bea0422ab0c479e431f,f26326f3f2c07b3e9668d08af91daf2460e9661d..ebe9fc07b690ff1fb35f9a5b2df47ee865be1eff
--- 1/src/AST/astops.h
--- 2/src/AST/astops.h
+++ b/src/AST/astops.h
@@@ -7,7 -7,8 +7,8 @@@ typedef enum FunctionType FunctionType
  enum PredicateType {TABLEPRED, OPERATORPRED};
  typedef enum PredicateType PredicateType;
  
- enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
+ 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};
@@@ -16,11 -17,4 +17,11 @@@ typedef enum Polarity Polarity
  enum BooleanValue {BV_UNDEFINED=0, BV_MUSTBETRUE=1, BV_MUSTBEFALSE=2, BV_UNSAT=3};
  typedef enum BooleanValue BooleanValue;
  
 +enum ElementEncodingType {
 +      ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, BINARYVAL
 +};
 +
 +typedef enum ElementEncodingType ElementEncodingType;
 +
 +
  #endif

diff --combined src/AST/boolean.h
index 9d7e9ab16df375e9fc5a2cc4d2708abf75bba99e,df1f4e8c152f1f86f88feddfb0e6d3b1eb8167e9..6449a8e0f0eed13ff7559839123d25b937442f19
--- 1/src/AST/boolean.h
--- 2/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@@ -8,14 -8,14 +8,14 @@@
  #include "astnode.h"
  #include "functionencoding.h"
  #include "constraint.h"
- 
- 
+ #include "serializer.h"
  
  class Boolean : public ASTNode {
  public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
        virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
+       virtual void serialize(Serializer* ) = 0;
        virtual bool isTrue() {return boolVal == BV_MUSTBETRUE;}
        virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;}
        Polarity polarity;
@@@ -32,6 -32,8 +32,8 @@@ public
        Boolean *clone(CSolver *solver, CloneMap *map);
        bool isTrue() {return istrue;}
        bool isFalse() {return !istrue;}
+       void serialize(Serializer *serializer ){};
+       
        bool istrue;
        CMEMALLOC;
  };
@@@ -40,7 -42,8 +42,8 @@@ class BooleanVar : public Boolean 
  public:
        BooleanVar(VarType t);
        Boolean *clone(CSolver *solver, CloneMap *map);
- 
+       void serialize(Serializer *serializer );
+       
        VarType vtype;
        Edge var;
        CMEMALLOC;
@@@ -50,7 -53,8 +53,8 @@@ class BooleanOrder : public Boolean 
  public:
        BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
        Boolean *clone(CSolver *solver, CloneMap *map);
- 
+       void serialize(Serializer *serializer );
+       
        Order *order;
        uint64_t first;
        uint64_t second;
@@@ -61,22 -65,24 +65,25 @@@ class BooleanPredicate : public Boolea
  public:
        BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus);
        Boolean *clone(CSolver *solver, CloneMap *map);
-       CMEMALLOC;
 +      Predicate *getPredicate() {return predicate;}
 +      FunctionEncoding *getFunctionEncoding() {return &encoding;}
 +      void updateParents();
+       void serialize(Serializer *serializer );
 +      
++      CMEMALLOC;
+ 
        Predicate *predicate;
        FunctionEncoding encoding;
        Array<Element *> inputs;
        BooleanEdge undefStatus;
 -      FunctionEncoding *getFunctionEncoding() {return &encoding;}
 -      void updateParents();
 -
 -      CMEMALLOC;
  };
  
  class BooleanLogic : public Boolean {
  public:
        BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize);
        Boolean *clone(CSolver *solver, CloneMap *map);
- 
+       void serialize(Serializer *serializer );
+       
        LogicOp op;
        bool replaced;
        Array<BooleanEdge> inputs;

diff --combined src/AST/element.cc
index ca42290953e7495126f37aaea3f8161236b2b193,2617022b9abcdfdef75bbcf33fc20552932c1dd3..ed0a7416853453316d44d2bb565fa991d8326389
--- 1/src/AST/element.cc
--- 2/src/AST/element.cc
+++ b/src/AST/element.cc
@@@ -23,10 -23,10 +23,10 @@@ ElementSet::ElementSet(ASTNodeType _typ
  
  ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, BooleanEdge _overflowstatus) :
        Element(ELEMFUNCRETURN),
 -      function(_function),
        inputs(array, numArrays),
        overflowstatus(_overflowstatus),
 -      functionencoding(this) {
 +      functionencoding(this),
 +      function(_function) {
  }
  
  ElementConst::ElementConst(uint64_t _value, Set *_set) :
@@@ -63,3 -63,58 +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; i<size; i++){
+               Element *input = inputs.get(i);
+               input->serialize(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; i<size; i++){
+               Element* input = inputs.get(i);
+               serializer->mywrite(&input, sizeof(Element*));
+       }
+       Boolean* overflowstat = overflowstatus.getRaw();
+       serializer->mywrite(&overflowstat, sizeof(Boolean*));
+ }
+ 

diff --combined src/AST/element.h
index db1cbfb6b00f7f203851af0500451394bfced602,19e35b68f5d07f6c50e78488481f6421032b147f..b829a47f07a14d32a6c7a4006cd4098c17d3a19d
--- 1/src/AST/element.h
--- 2/src/AST/element.h
+++ b/src/AST/element.h
@@@ -15,6 -15,7 +15,7 @@@ public
        Vector<ASTNode *> 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 +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 +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;
  };
@@@ -43,16 -46,15 +46,17 @@@
  class ElementFunction : public Element {
  public:
        ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
 -      Function *function;
        Array<Element *> inputs;
        BooleanEdge overflowstatus;
        FunctionEncoding functionencoding;
        Element *clone(CSolver *solver, CloneMap *map);
+       virtual void serialize(Serializer* serializer);
        Set * getRange();
        void updateParents();
 +      Function * getFunction() {return function;}
        CMEMALLOC;
 + private:
 +      Function *function;
  };
  
  static inline ElementEncoding *getElementEncoding(Element *e) {

diff --combined src/AST/predicate.cc
index f37d4cdc72d1dde709325c76b57cec300d4d4356,7f63faa042fcd6da4924f1316586ecd49fd81d5c..e3ae1db970280646bd4c30c17689c7374f415522
--- 1/src/AST/predicate.cc
--- 2/src/AST/predicate.cc
+++ b/src/AST/predicate.cc
@@@ -4,7 -4,7 +4,7 @@@
  #include "table.h"
  #include "csolver.h"
  
 -PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), op(_op), domains(domain, numDomain) {
 +PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), domains(domain, numDomain), op(_op) {
  }
  
  PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
@@@ -50,3 -50,42 +50,42 @@@ Predicate *PredicateTable::clone(CSolve
        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; i<size; i++){
+               Set* domain = domains.get(i);
+               domain->serialize(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; i<size; i++){
+               Set* domain = domains.get(i);
+               serializer->mywrite(&domain, sizeof(Set*));
+       }
+ }
+ 

diff --combined src/AST/predicate.h
index 80515fa9e06a75968ae1e53507bcd7c1577f2db4,2f292b21c37741b3d9e3815bcffed27091278f41..beaebc9b09989122f45d64573a0e7868c499f0b2
--- 1/src/AST/predicate.h
--- 2/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@@ -12,6 -12,7 +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,17 -22,17 +22,19 @@@ public
        PredicateOperator(CompOp op, Set **domain, uint numDomain);
        bool evalPredicateOperator(uint64_t *inputs);
        Predicate *clone(CSolver *solver, CloneMap *map);
-       CompOp getOp() {return op;}
+       virtual void serialize(Serializer* serializer);
 -      CompOp op;
        Array<Set *> domains;
++      CompOp getOp() {return op;}
        CMEMALLOC;
 + private:
 +      CompOp op;
  };
  
  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 --combined src/Collections/structs.h
index 1e957ae997a7a01783dbd9b81d5e06a710f77c04,e6f451ed3d6ba0f0b9997104ac2c5f3dad40b698..d5d6f5ef74f72678c98007a13e4823063394931e
--- 1/src/Collections/structs.h
--- 2/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@@ -26,17 -26,13 +26,16 @@@ typedef Hashset<OrderElement *, uintptr
  typedef Hashset<Boolean *, uintptr_t, PTRSHIFT> HashsetBoolean;
  typedef Hashset<Element *, uintptr_t, PTRSHIFT> HashsetElement;
  typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
 +typedef Hashset<uint64_t, uint64_t, 0> Hashset64Int;
 +
+ 
  typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, PTRSHIFT> HashtableNodeToNodeSet;
  typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, PTRSHIFT, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
  typedef Hashtable<void *, void *, uintptr_t, PTRSHIFT> CloneMap;
  
  
 -typedef Hashtable<Set *, EncodingNode *, uintptr_t, PTRSHIFT> HashTableEncoding;
 +typedef Hashtable<Set *, EncodingNode *, uintptr_t, PTRSHIFT> HashtableEncoding;
- typedef Hashset<EncodingNode *, uintptr_t, PTRSHIFT> HashsetEncodingNode;
- typedef SetIterator<EncodingNode *, uintptr_t, PTRSHIFT> SetIteratorEncodingNode;
 +
  
  typedef SetIterator<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
  typedef SetIterator<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;

diff --combined src/Serialize/serializer.h
index 0000000000000000000000000000000000000000,12bff1306ecd9b47c7e77753bd23fbbab3a2e338..e6d2b50bce8707d23ae4a379c411ff936926a957
mode 000000,100644..100644
--- /dev/null
--- 2/src/Serialize/serializer.h
+++ b/src/Serialize/serializer.h
@@@ -1,0 -1,37 +1,39 @@@
+ 
+ /* 
+  * File:   serializer.h
+  * Author: hamed
+  *
+  * Created on September 7, 2017, 3:38 PM
+  */
+ 
+ #ifndef SERIALIZER_H
+ #define SERIALIZER_H
+ #include "mymemory.h"
++#include "classlist.h"
+ #include "structs.h"
+ 
++
+ class Serializer {
+ public:
+       Serializer(const char *file);
+       void mywrite(const void *__buf, size_t __n);
+       inline bool isSerialized(void *obj);
+       inline void addObject(void *obj) { map.put(obj, obj);}
+       virtual ~Serializer();
+       CMEMALLOC;
+ private:
+       int filedesc;
+       CloneMap map;
+ };
+ 
+ inline bool Serializer::isSerialized(void* obj){
+       return map.contains(obj);
+ }
+ 
+ 
+ 
+ 
+ void serializeBooleanEdge(Serializer* serializer, BooleanEdge be);
+ 
+ #endif /* SERIALIZER_H */
+