Merging with branch master
authorHamed <hamed.gorjiara@gmail.com>
Fri, 8 Sep 2017 21:15:09 +0000 (14:15 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Fri, 8 Sep 2017 21:15:09 +0000 (14:15 -0700)
1  2 
src/Makefile
src/Serialize/deserializer.cc
src/Test/buildconstraintstest.cc
src/csolver.cc

diff --combined src/Makefile
index ee81df13ae02a4f701f554cc7fb3b4f68cb12e88,e099994e89c59b1445a63c705e84609cc6615a5a..acf435a7d3d65b684f76102c7c87c62e34a1ae58
@@@ -4,16 -4,16 +4,16 @@@ PHONY += directorie
  MKDIR_P = mkdir -p
  OBJ_DIR = bin
  
- CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc)
 -CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
++CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc)
  
- C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c)
 -C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c)
++C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c)
  
- HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h)
 -HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
++HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h)
  
  OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
  
  CFLAGS := -Wall -g -O0
- CFLAGS += -IAST -IASTTransform -IASTAnalyses -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
 -CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner
++CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
  LDFLAGS := -ldl -lrt -rdynamic
  SHARED := -shared
  
@@@ -33,13 -33,15 +33,16 @@@ ${OBJ_DIR}
        ${MKDIR_P} ${OBJ_DIR}
        ${MKDIR_P} ${OBJ_DIR}/AST
        ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses
+       ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses/Order
+       ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses/Encoding
+       ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses/Polarity
        ${MKDIR_P} ${OBJ_DIR}/ASTTransform
        ${MKDIR_P} ${OBJ_DIR}/Translator
        ${MKDIR_P} ${OBJ_DIR}/Tuner
        ${MKDIR_P} ${OBJ_DIR}/Collections
        ${MKDIR_P} ${OBJ_DIR}/Backend
        ${MKDIR_P} ${OBJ_DIR}/Encoders
 +      ${MKDIR_P} ${OBJ_DIR}/Serialize
  
  debug: CFLAGS += -DCONFIG_DEBUG
  debug: all
@@@ -76,10 -78,10 +79,10 @@@ tags
        ctags -R
  
  tabbing:
-       uncrustify -c C.cfg --no-backup *.cc */*.cc
-       uncrustify -c C.cfg --no-backup *.h */*.h
+       uncrustify -c C.cfg --no-backup *.cc */*.cc */*/*.cc
+       uncrustify -c C.cfg --no-backup *.h */*.h */*/*.h
  
  wc:
-       wc */*.cc */*.h *.cc *.h
+       wc */*.cc */*.h *.cc *.h */*/*.cc */*/*.h
  
  .PHONY: $(PHONY)
index 163bd199e643e86a90a9b7eaf8b0b7248cebcbef,0000000000000000000000000000000000000000..bf97cbbafb296219b163740e6f59d51a1233c2eb
mode 100644,000000..100644
--- /dev/null
@@@ -1,83 -1,0 +1,86 @@@
 +
 +/* 
 + * File:   deserializer.cc
 + * Author: hamed
 + * 
 + * Created on September 7, 2017, 6:08 PM
 + */
 +
 +#include "deserializer.h"
 +#include "csolver.h"
 +#include "unistd.h"
 +#include "fcntl.h"
 +
 +Deserializer::Deserializer(const char* file):
 +      solver(new CSolver())
 +{
 +      filedesc = open(file, O_RDONLY);
 + 
 +      if (filedesc < 0) {
 +              exit(-1);
 +      }
 +}
 +
 +Deserializer::~Deserializer() {
 +      delete solver;
 +}
 +
 +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;
 +}
 +
 +CSolver * Deserializer::deserialize(){
 +      ASTNodeType nodeType;
 +      while(myread(&nodeType, sizeof(ASTNodeType) ) >0){
 +              switch(nodeType){
 +                      case BOOLEANEDGE:
 +                              deserializeBooleanEdge();
 +                              break;
 +                      case BOOLEANVAR:
 +                              deserializeBooleanVar();
 +                              break;
++                      case ORDERCONST:
++                              deserializeBooleanOrder();
++                              break;
 +                      default:
 +                              ASSERT(0);
 +              }
 +      }
 +      return solver;
 +}
 +
 +void Deserializer::deserializeBooleanEdge(){
 +      Boolean *b;
 +      myread(&b, sizeof(Boolean*));
 +      BooleanEdge tmp(b);
 +      bool isNegated = tmp.isNegated();
 +      ASSERT(map.contains(tmp.getBoolean()));
 +      b = (Boolean*) map.get(tmp.getBoolean());
 +      BooleanEdge res(b);
 +      solver->addConstraint(isNegated?res.negate():res);
 +}
 +
 +void Deserializer::deserializeBooleanVar(){
 +      BooleanVar *b;
 +      myread(&b, sizeof(BooleanVar*));
 +      VarType vtype;
 +      myread(&vtype, sizeof(VarType));
 +      map.put(b, solver->getBooleanVar(vtype).getBoolean());
 +}
 +
 +void Deserializer::deserializeBooleanOrder(){
 +      BooleanOrder* bo_ptr;
 +      myread(&bo_ptr, sizeof(BooleanOrder*));
 +      Order* optr;
 +      myread(&optr, sizeof(Order*));
 +      uint64_t first;
 +      myread(&first, sizeof(uint64_t));
 +      uint64_t second;
 +      myread(&second, sizeof(uint64_t));
 +      ASSERT(map.contains(optr));
 +      Order* order  = (Order*) map.get(optr);
 +      map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
 +}
index e01fb8f8e315aeb7032f7a6345948b8a2fed2ce9,af17a4bb33d81b30abc79d43d726138f206d21c7..e01fb8f8e315aeb7032f7a6345948b8a2fed2ce9
mode 100755,100644..100644
@@@ -50,7 -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();
        if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
diff --combined src/csolver.cc
index bcd8f3fe33043298383aa85e0d7a0cd989573a8e,3c6767f585078bba9c0037afa6b259acb02282c2..bbe2b0c2c28c744ba9c001ca5467217093098839
@@@ -19,8 -19,6 +19,8 @@@
  #include "integerencoding.h"
  #include "qsort.h"
  #include "preprocess.h"
 +#include "serializer.h"
 +#include "deserializer.h"
  
  CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@@ -86,24 -84,6 +86,24 @@@ CSolver *CSolver::clone() 
        return copy;
  }
  
 +void CSolver::serialize() {
 +      {
 +              Serializer serializer("dump");
 +              SetIteratorBooleanEdge *it = getConstraints();
 +              while (it->hasNext()) {
 +                      BooleanEdge b = it->next();
 +                      serializeBooleanEdge(&serializer, b);
 +              }
 +              delete it;
 +      }
 +      model_print("deserializing ...\n");
 +      {
 +              Deserializer deserializer("dump");
 +              deserializer.deserialize();
 +      }
 +      
 +}
 +
  Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
        Set *set = new Set(type, elements, numelements);
        allSets.push(set);
@@@ -146,7 -126,7 +146,7 @@@ Element *CSolver::getElementVar(Set *se
  Element *CSolver::getElementConst(VarType type, uint64_t value) {
        uint64_t array[] = {value};
        Set *set = new Set(type, array, 1);
-       Element *element = new ElementConst(value, type, set);
+       Element *element = new ElementConst(value, set);
        Element *e = elemMap.get(element);
        if (e == NULL) {
                allSets.push(set);