Merge branch 'encoding'
authorbdemsky <bdemsky@uci.edu>
Mon, 11 Sep 2017 23:27:36 +0000 (16:27 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 11 Sep 2017 23:27:36 +0000 (16:27 -0700)
39 files changed:
src/AST/astops.h
src/AST/boolean.cc
src/AST/boolean.h
src/AST/element.cc
src/AST/element.h
src/AST/function.cc
src/AST/function.h
src/AST/order.h
src/AST/predicate.cc
src/AST/predicate.h
src/AST/set.h
src/AST/table.cc
src/AST/table.h
src/ASTAnalyses/Encoding/encodinggraph.cc
src/ASTAnalyses/Encoding/encodinggraph.h
src/Backend/satelemencoder.cc
src/Backend/satfuncopencoder.cc
src/Collections/structs.h
src/Encoders/elementencoding.h
src/Serialize/deserializer.cc
src/Serialize/deserializer.h
src/Serialize/serializable.h [deleted file]
src/Serialize/serializer.cc
src/Serialize/serializer.h
src/Test/buildconstraintstest.cc
src/Test/elemequalsattest.cc
src/Test/elemequalunsattest.cc
src/Test/funcencodingtest.cc
src/Test/logicopstest.cc
src/Test/ltelemconsttest.cc
src/Test/ordergraphtest.cc
src/Test/tablefuncencodetest.cc
src/Test/tablepredicencodetest.cc
src/Translator/sattranslator.cc
src/Tuner/searchtuner.cc
src/Tuner/searchtuner.h
src/Tuner/tunable.cc
src/Tuner/tunable.h
src/csolver.cc

index c3244fb..ebe9fc0 100644 (file)
@@ -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};
@@ -16,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
index 1795f17..8a6f0d3 100644 (file)
@@ -114,6 +114,7 @@ void BooleanOrder::serialize(Serializer* serializer){
                return;
        serializer->addObject(this);
        order->serialize(serializer);
+       
        serializer->mywrite(&type, sizeof(ASTNodeType));
        BooleanOrder* This = this;
        serializer->mywrite(&This, sizeof(BooleanOrder*));
@@ -123,9 +124,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; i<size; i++){
+               Element* input = inputs.get(i);
+               input->serialize(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; i<size; i++){
+               Element *input = inputs.get(i);
+               serializer->mywrite(&input, sizeof(Element *));
+       }
+       Boolean* undefStat = undefStatus!= BooleanEdge(NULL)?undefStatus.getRaw() : NULL;
+       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; i<size; i++){
+               BooleanEdge input = inputs.get(i);
+               serializeBooleanEdge(serializer, input);
+       }
+       serializer->mywrite(&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; i<size; i++){
+               Boolean* input = inputs.get(i).getRaw();
+               serializer->mywrite(&input, sizeof(Boolean*));
+       }
+}
+
index 1c45f04..6449a8e 100644 (file)
@@ -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() {}
@@ -66,16 +65,17 @@ class BooleanPredicate : public Boolean {
 public:
        BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus);
        Boolean *clone(CSolver *solver, CloneMap *map);
+       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 {
index ca42290..ed0a741 100644 (file)
@@ -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; 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*));
+}
+
index db1cbfb..b829a47 100644 (file)
@@ -15,6 +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 @@ 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;
 };
@@ -47,6 +50,7 @@ public:
        BooleanEdge overflowstatus;
        FunctionEncoding functionencoding;
        Element *clone(CSolver *solver, CloneMap *map);
+       virtual void serialize(Serializer* serializer);
        Set * getRange();
        void updateParents();
        Function * getFunction() {return function;}
index a882580..96b0797 100644 (file)
@@ -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; i<size; i++){
+               Set* domain = domains.get(i);
+               domain->serialize(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; i<size; i++){
+               Set *domain = domains.get(i);
+               serializer->mywrite(&domain, sizeof(Set *));
+       }
+       serializer->mywrite(&range, sizeof(Set *));
+       serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior));
+}
\ No newline at end of file
index f34c02e..98ef536 100644 (file)
@@ -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;
 };
index 2301d47..b8ca724 100644 (file)
@@ -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();
index d359811..e3ae1db 100644 (file)
@@ -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 @@ 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; 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*));
+       }
+}
+
index 183a960..beaebc9 100644 (file)
@@ -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,15 +22,19 @@ public:
        PredicateOperator(CompOp op, Set **domain, uint numDomain);
        bool evalPredicateOperator(uint64_t *inputs);
        Predicate *clone(CSolver *solver, CloneMap *map);
-       CompOp op;
+       virtual void serialize(Serializer* serializer);
        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;
index 6a41815..6dbeac0 100644 (file)
@@ -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);
index e0f735f..838a53a 100644 (file)
@@ -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,41 @@ 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; i<size; i++){
+               Set* domain = domains.get(i);
+               domain->serialize(serializer);
+       }
+       if(range!= NULL)
+               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; i<size; i++){
+               Set* domain = domains.get(i);
+               serializer->mywrite(&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);
+       }
+       delete iterator;
+}
+
+
index 6c7926e..db8d188 100644 (file)
@@ -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;}
        
index 9c0a29e..8d34d47 100644 (file)
@@ -2,6 +2,10 @@
 #include "iterator.h"
 #include "element.h"
 #include "function.h"
+#include "predicate.h"
+#include "set.h"
+#include "csolver.h"
+#include "tunable.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {
@@ -26,6 +30,37 @@ void EncodingGraph::buildGraph() {
        }
 }
 
+void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
+       EncodingSubGraph *graph1=graphMap.get(first);
+       EncodingSubGraph *graph2=graphMap.get(second);
+       if (graph1 == NULL && graph2 == NULL) {
+               graph1 = new EncodingSubGraph();
+               graphMap.put(first, graph1);
+               graph1->addNode(first);
+       }
+       if (graph1 == NULL && graph2 != NULL) {
+               graph1 = graph2;
+               graph2 = NULL;
+               EncodingNode *tmp = second;
+               second = first;
+               first = tmp;
+       }
+       if (graph1 != NULL && graph2 != NULL) {
+               SetIteratorEncodingNode * nodeit=graph2->nodeIterator();
+               while(nodeit->hasNext()) {
+                       EncodingNode *node=nodeit->next();
+                       graph1->addNode(node);
+                       graphMap.put(node, graph1);
+               }
+               delete nodeit;
+               delete graph2;
+       } else {
+               ASSERT(graph1 != NULL && graph2 == NULL);
+               graph1->addNode(second);
+               graphMap.put(second, graph1);
+       }
+}
+
 void EncodingGraph::processElement(Element *e) {
        uint size=e->parents.getSize();
        for(uint i=0;i<size;i++) {
@@ -47,22 +82,92 @@ void EncodingGraph::processFunction(ElementFunction *ef) {
        Function *f=ef->getFunction();
        if (f->type==OPERATORFUNC) {
                FunctionOperator *fo=(FunctionOperator*)f;
-               ArithOp op=fo->op;
+               ASSERT(ef->inputs.getSize() == 2);
+               EncodingNode *left=createNode(ef->inputs.get(0));
+               EncodingNode *right=createNode(ef->inputs.get(1));
+               if (left == NULL && right == NULL)
+                       return;
+               EncodingNode *dst=createNode(ef);
+               EncodingEdge *edge=getEdge(left, right, dst);
+               edge->numArithOps++;
        }
 }
 
 void EncodingGraph::processPredicate(BooleanPredicate *b) {
+       Predicate *p=b->getPredicate();
+       if (p->type==OPERATORPRED) {
+               PredicateOperator *po=(PredicateOperator *)p;
+               ASSERT(b->inputs.getSize()==2);
+               EncodingNode *left=createNode(b->inputs.get(0));
+               EncodingNode *right=createNode(b->inputs.get(1));
+               if (left == NULL || right == NULL)
+                       return;
+               EncodingEdge *edge=getEdge(left, right, NULL);
+               CompOp op=po->getOp();
+               switch(op) {
+               case SATC_EQUALS:
+                       edge->numEquals++;
+                       break;
+               case SATC_LT:
+               case SATC_LTE:
+               case SATC_GT:
+               case SATC_GTE:
+                       edge->numComparisons++;
+                       break;
+               default:
+                       ASSERT(0);
+               }
+       }
+}
+
+static TunableDesc EdgeEncodingDesc(EDGE_UNASSIGNED, EDGE_MATCH, EDGE_UNASSIGNED);
+
+EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+       EncodingEdge e(left, right, dst);
+       EncodingEdge *result = edgeMap.get(&e);
+       if (result == NULL) {
+               result=new EncodingEdge(left, right, dst);
+               VarType v1=left->getType();
+               VarType v2=right->getType();
+               if (v1 > v2) {
+                       VarType tmp=v2;
+                       v2=v1;
+                       v1=tmp;
+               }
+               result->setEncoding((EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc));
+               edgeMap.put(result, result);
+       }
+       return result;
+}
+
+EncodingNode::EncodingNode(Set *_s) :
+       s(_s),
+       numElements(0) {
+}
+
+uint EncodingNode::getSize() {
+       return s->getSize();
+}
 
+VarType EncodingNode::getType() {
+       return s->getType();
 }
 
+static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+
 EncodingNode * EncodingGraph::createNode(Element *e) {
+       if (e->type == ELEMCONST)
+               return NULL;
        Set *s = e->getRange();
        EncodingNode *n = encodingMap.get(s);
        if (n == NULL) {
                n = new EncodingNode(s);
+               n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingDesc));
                encodingMap.put(s, n);
        }
        n->addElement(e);
+       if (discovered.add(e))
+               n->numElements++;
        return n;
 }
 
@@ -73,14 +178,22 @@ void EncodingNode::addElement(Element *e) {
 EncodingEdge::EncodingEdge(EncodingNode *_l, EncodingNode *_r) :
        left(_l),
        right(_r),
-       dst(NULL)
+       dst(NULL),
+       encoding(EDGE_UNASSIGNED),
+       numArithOps(0),
+       numEquals(0),
+       numComparisons(0)
 {
 }
 
 EncodingEdge::EncodingEdge(EncodingNode *_left, EncodingNode *_right, EncodingNode *_dst) :
        left(_left),
        right(_right),
-       dst(_dst)
+       dst(_dst),
+       encoding(EDGE_UNASSIGNED),
+       numArithOps(0),
+       numEquals(0),
+       numComparisons(0)
 {
 }
 
@@ -92,3 +205,20 @@ uint hashEncodingEdge(EncodingEdge *edge) {
 bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2) {
        return e1->left == e2->left && e1->right == e2->right && e1->dst == e2->dst;
 }
+
+EncodingSubGraph::EncodingSubGraph() {
+}
+
+void EncodingSubGraph::addNode(EncodingNode *n) {
+       nodes.add(n);
+       Set *s=n->s;
+       uint size=s->getSize();
+       for(uint i=0; i<size; i++) {
+               uint64_t val=s->getElement(i);
+               values.add(val);
+       }
+}
+
+SetIteratorEncodingNode * EncodingSubGraph::nodeIterator() {
+       return nodes.iterator();
+}
index adb467c..e44ccfd 100644 (file)
@@ -5,8 +5,13 @@
 
 uint hashEncodingEdge(EncodingEdge *edge);
 bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
+class EncodingSubGraph;
+
 
 typedef Hashtable<EncodingEdge *, EncodingEdge *, uintptr_t, PTRSHIFT, hashEncodingEdge, equalsEncodingEdge> HashtableEdge;
+typedef Hashset<EncodingNode *, uintptr_t, PTRSHIFT> HashsetEncodingNode;
+typedef SetIterator<EncodingNode *, uintptr_t, PTRSHIFT> SetIteratorEncodingNode;
+typedef Hashtable<EncodingNode *, EncodingSubGraph *, uintptr_t, PTRSHIFT> HashtableNodeToSubGraph;
 
 class EncodingGraph {
  public:
@@ -18,36 +23,71 @@ class EncodingGraph {
        CSolver * solver;
        HashtableEncoding encodingMap;
        HashtableEdge edgeMap;
+       HashsetElement discovered;
+       HashtableNodeToSubGraph graphMap;
+
+       
+       void mergeNodes(EncodingNode *first, EncodingNode *second);
        void processElement(Element *e);
        void processFunction(ElementFunction *f);
        void processPredicate(BooleanPredicate *b);
        EncodingNode * createNode(Element *e);
-
+       EncodingEdge * getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
 };
 
 class EncodingNode {
  public:
        EncodingNode(Set *_s);
        void addElement(Element *e);
+       uint getSize();
+       VarType getType();
+       void setEncoding(ElementEncodingType e) {encoding=e;}
+       
        CMEMALLOC;
  private:
        Set *s;
        HashsetElement elements;
+       uint numElements;
+       ElementEncodingType encoding;
+       friend class EncodingGraph;
+       friend class EncodingSubGraph;
 };
 
+class EncodingSubGraph {
+ public:
+       EncodingSubGraph();
+       void addNode(EncodingNode *n);
+       SetIteratorEncodingNode * nodeIterator();
+       
+       CMEMALLOC;
+ private:
+       HashsetEncodingNode nodes;
+       Hashset64Int values;
+};
+
+enum EdgeEncodingType { EDGE_UNASSIGNED, EDGE_BREAK, EDGE_MATCH};
+typedef enum EdgeEncodingType EdgeEncodingType;
+
 class EncodingEdge {
  public:
        EncodingEdge(EncodingNode *_l, EncodingNode *_r);
        EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d);
+       void setEncoding(EdgeEncodingType e) {encoding=e;}
        CMEMALLOC;
+       
  private:
        EncodingNode *left;
        EncodingNode *right;
        EncodingNode *dst;
+       EdgeEncodingType encoding;
+       uint numArithOps;
+       uint numEquals;
+       uint numComparisons;
        friend uint hashEncodingEdge(EncodingEdge *edge);
        friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
-
+       friend class EncodingGraph;
 };
 
 
+
 #endif
index ed761e3..7dcb5de 100644 (file)
@@ -13,9 +13,6 @@ Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
                return getElementValueUnaryConstraint(elem, value);
        case BINARYINDEX:
                return getElementValueBinaryIndexConstraint(elem, value);
-       case ONEHOTBINARY:
-               ASSERT(0);
-               break;
        case BINARYVAL:
                return getElementValueBinaryValueConstraint(elem, value);
                break;
@@ -138,8 +135,6 @@ void SATEncoder::generateElementEncoding(Element *element) {
        case UNARY:
                generateUnaryEncodingVars(encoding);
                return;
-       case ONEHOTBINARY:
-               return;
        case BINARYVAL:
                generateBinaryValueEncodingVars(encoding);
                return;
index 7e6a67d..9fc3c41 100644 (file)
@@ -204,7 +204,7 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
        ElementEncoding *ee1 = getElementEncoding(elem1);
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
-       switch (predicate->op) {
+       switch (predicate->getOp()) {
        case SATC_EQUALS:
                return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
        case SATC_LT:
index 6ee69ab..d5d6f5e 100644 (file)
@@ -26,6 +26,8 @@ typedef Hashset<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function
 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;
@@ -34,6 +36,7 @@ typedef Hashtable<void *, void *, uintptr_t, PTRSHIFT> CloneMap;
 
 typedef Hashtable<Set *, EncodingNode *, uintptr_t, PTRSHIFT> HashtableEncoding;
 
+
 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;
 typedef SetIterator<OrderNode *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
index d7585f4..6797c66 100644 (file)
@@ -4,12 +4,6 @@
 #include "naiveencoder.h"
 #include "constraint.h"
 
-enum ElementEncodingType {
-       ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
-};
-
-typedef enum ElementEncodingType ElementEncodingType;
-
 class ElementEncoding {
 public:
        ElementEncoding(Element *element);
index 7616cd7..7119119 100644 (file)
@@ -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())
@@ -23,6 +26,10 @@ Deserializer::Deserializer(const char* file):
 
 Deserializer::~Deserializer() {
        delete solver;
+       
+       if (-1 == close(filedesc)){
+               exit(-1);
+       }
 }
 
 ssize_t Deserializer::myread(void* __buf, size_t __nbytes){
@@ -48,6 +55,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);
                }
@@ -77,14 +114,14 @@ void Deserializer::deserializeBooleanVar(){
 void Deserializer::deserializeBooleanOrder(){
        BooleanOrder* bo_ptr;
        myread(&bo_ptr, sizeof(BooleanOrder*));
-       Order* optr;
-       myread(&optr, sizeof(Order*));
+       Order* order;
+       myread(&order, sizeof(Order*));
+       ASSERT(map.contains(order));
+       order  = (Order*) map.get(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());
 }
 
@@ -123,3 +160,214 @@ 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<BooleanEdge> members;
+       for(uint i=0; i<size; i++){
+               Boolean* member;
+               myread(&member, sizeof(Boolean *));
+               BooleanEdge tmp(member);
+               bool isNegated = tmp.isNegated();
+               ASSERT(map.contains(tmp.getBoolean()));
+               member = (Boolean*) map.get(tmp.getBoolean());
+               BooleanEdge res(member);
+               members.push( isNegated?res.negate():res );
+       }
+       map.put(bl_ptr, solver->applyLogicalOperation(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<Element*> members;
+       for(uint i=0; i<size; i++){
+               Element* input;
+               myread(&input, sizeof(Element *));
+               ASSERT(map.contains(input));
+               input = (Element*) map.get(input);
+               members.push(input);
+       }
+       
+       Boolean* stat_ptr;
+       myread(&stat_ptr, sizeof(Boolean *));
+       BooleanEdge undefStatus;
+       if(stat_ptr != NULL){
+               BooleanEdge tmp(stat_ptr);
+               bool isNegated = tmp.isNegated();
+               ASSERT(map.contains(tmp.getBoolean()));
+               stat_ptr = (Boolean*) map.get(tmp.getBoolean());
+               BooleanEdge res(stat_ptr);
+               undefStatus = isNegated?res.negate():res;
+       } else {
+               undefStatus = NULL;
+       }
+       map.put(bp_ptr, solver->applyPredicateTable(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<Set*> domains;
+       for(uint i=0; i<size; i++){
+               Set* domain;
+               myread(&domain, sizeof(Set*));
+               ASSERT(map.contains(domain));
+               domain = (Set*) map.get(domain);
+               domains.push(domain);
+       }
+
+       map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
+}
+
+void Deserializer::deserializeTable(){
+       Table *t_ptr;
+       myread(&t_ptr, sizeof(Table *));
+       uint size;
+       myread(&size, sizeof(uint));
+       Vector<Set*> domains;
+       for(uint i=0; i<size; i++){
+               Set* domain;
+               myread(&domain, sizeof(Set*));
+               ASSERT(map.contains(domain));
+               domain = (Set*) map.get(domain);
+               domains.push(domain);
+       }
+       Set* range;
+       myread(&range, sizeof(Set*));
+       if(range != NULL){
+               ASSERT(map.contains(range));
+               range = (Set*) map.get(range);
+       }
+       Table* table = solver->createTable(domains.expose(), size, range);
+       myread(&size, sizeof(uint));
+       for(uint i=0; i<size; i++){
+               uint64_t output;
+               myread(&output, sizeof(uint64_t));
+               uint inputSize;
+               myread(&inputSize, sizeof(uint));
+               Vector<uint64_t> inputs;
+               inputs.setSize(inputSize);
+               myread(inputs.expose(), sizeof(uint64_t)*inputSize);
+               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<Element*> members;
+       for(uint i=0; i<size; i++){
+               Element* input;
+               myread(&input, sizeof(Element *));
+               ASSERT(map.contains(input));
+               input = (Element*) map.get(input);
+               members.push(input);
+       }
+       
+       Boolean* overflowstatus;
+       myread(&overflowstatus, sizeof(Boolean *));
+       BooleanEdge tmp(overflowstatus);
+       bool isNegated = tmp.isNegated();
+       ASSERT(map.contains(tmp.getBoolean()));
+       overflowstatus = (Boolean*) map.get(tmp.getBoolean());
+       BooleanEdge res(overflowstatus);
+       BooleanEdge undefStatus = isNegated?res.negate():res;
+       
+       map.put(ef_ptr, solver->applyFunction(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<Set*> domains;
+       for(uint i=0; i<size; i++){
+               Set* domain;
+               myread(&domain, sizeof(Set*));
+               ASSERT(map.contains(domain));
+               domain = (Set*) map.get(domain);
+               domains.push(domain);
+       }
+       Set* range;
+       myread(&range, sizeof(Set*));
+       ASSERT(map.contains(range));
+       range = (Set*) map.get(range);
+       OverFlowBehavior overflowbehavior;
+       myread(&overflowbehavior, sizeof(OverFlowBehavior));
+       map.put(fo_ptr, solver->createFunctionOperator(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
index 7c7d39a..057346d 100644 (file)
@@ -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 (file)
index a5e769d..0000000
+++ /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 */
-
index 783cf88..b49b98b 100644 (file)
@@ -12,7 +12,7 @@
 #include "boolean.h"
 
 Serializer::Serializer(const char *file) {
-       filedesc = open(file, O_WRONLY | O_CREAT, 0666);
+       filedesc = open(file, O_WRONLY | O_CREAT | O_TRUNC, 0666);
  
        if (filedesc < 0) {
                exit(-1);
@@ -30,7 +30,9 @@ void Serializer::mywrite(const void *__buf, size_t __n){
 }
 
 
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be){
+void serializeBooleanEdge(Serializer* serializer, BooleanEdge be){
+       if(be == BooleanEdge(NULL))
+               return;
        be.getBoolean()->serialize(serializer);
        ASTNodeType type = BOOLEANEDGE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
index eb114dc..e6d2b50 100644 (file)
@@ -9,8 +9,10 @@
 #ifndef SERIALIZER_H
 #define SERIALIZER_H
 #include "mymemory.h"
+#include "classlist.h"
 #include "structs.h"
 
+
 class Serializer {
 public:
        Serializer(const char *file);
@@ -31,7 +33,7 @@ inline bool Serializer::isSerialized(void* obj){
 
 
 
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be);
+void serializeBooleanEdge(Serializer* serializer, BooleanEdge be);
 
 #endif /* SERIALIZER_H */
 
index 46bc2a3..e01fb8f 100644 (file)
@@ -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
index aeab4a5..e041cb0 100644 (file)
@@ -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));
index 6a7a067..123d6cd 100644 (file)
@@ -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
index e3baeb9..72a0a83 100644 (file)
@@ -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",
index 9b20015..7b30f80 100644 (file)
@@ -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),
index d666833..11a315c 100644 (file)
@@ -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
index 80a57ff..fea3a9f 100644 (file)
@@ -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
index 11017c6..680d1c6 100644 (file)
@@ -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",
index 47113fd..4007e25 100644 (file)
@@ -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",
index bdcd196..792d58b 100644 (file)
@@ -67,8 +67,6 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
                return getElementValueUnarySATTranslator(This, elemEnc);
        case BINARYINDEX:
                return getElementValueBinaryIndexSATTranslator(This, elemEnc);
-       case ONEHOTBINARY:
-               ASSERT(0);
                break;
        case BINARYVAL:
                ASSERT(0);
index 52c7a70..3e95860 100644 (file)
@@ -2,19 +2,29 @@
 
 TunableSetting::TunableSetting(VarType _type, TunableParam _param) :
        hasVar(true),
-       type(_type),
+       type1(_type),
+       type2(0),
+       param(_param) {
+}
+
+TunableSetting::TunableSetting(VarType _type1, VarType _type2, TunableParam _param) :
+       hasVar(true),
+       type1(_type1),
+       type2(_type2),
        param(_param) {
 }
 
 TunableSetting::TunableSetting(TunableParam _param) :
        hasVar(false),
-       type(0),
+       type1(0),
+       type2(0),
        param(_param) {
 }
 
 TunableSetting::TunableSetting(TunableSetting *ts) :
        hasVar(ts->hasVar),
-       type(ts->type),
+       type1(ts->type1),
+       type2(ts->type2),
        param(ts->param),
        lowValue(ts->lowValue),
        highValue(ts->highValue),
@@ -32,19 +42,21 @@ void TunableSetting::setDecision(int _low, int _high, int _default, int _selecti
 
 void TunableSetting::print() {
        if (hasVar) {
-               model_print("Type %" PRIu64 ", ", type);
+               model_print("Type1 %" PRIu64 ", ", type1);
+               model_print("Type2 %" PRIu64 ", ", type2);
        }
        model_print("Param %u = %u\n", param, selectedValue);
 }
 
 unsigned int tunableSettingHash(TunableSetting *setting) {
-       return setting->hasVar ^ setting->type ^ setting->param;
+       return setting->hasVar ^ setting->type1 ^ setting->type2 ^ setting->param;
 }
 
 bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
        return setting1->hasVar == setting2->hasVar &&
-                                setting1->type == setting2->type &&
-                                setting1->param == setting2->param;
+               setting1->type1 == setting2->type1 &&
+               setting1->type2 == setting2->type2 &&
+               setting1->param == setting2->param;
 }
 
 SearchTuner::SearchTuner() {
@@ -88,12 +100,17 @@ int SearchTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
 }
 
 int SearchTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
-       TunableSetting setting(vartype, param);
+       return getVarTunable(vartype, 0, param, descriptor);
+}
+
+int SearchTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+       TunableSetting setting(vartype1, vartype2, param);
        TunableSetting *result = usedSettings.get(&setting);
        if (result == NULL) {
                result = settings.get(&setting);
                if ( result == NULL) {
-                       result = new TunableSetting(vartype, param);
+                       result = new
+                               TunableSetting(vartype1, vartype2, param);
                        uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue));
                        result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
                        settings.add(result);
index 20edb7d..1464849 100644 (file)
@@ -7,6 +7,7 @@
 class TunableSetting {
 public:
        TunableSetting(VarType type, TunableParam param);
+       TunableSetting(VarType type1, VarType type2, TunableParam param);
        TunableSetting(TunableParam param);
        TunableSetting(TunableSetting *ts);
        void setDecision(int _low, int _high, int _default, int _selection);
@@ -14,7 +15,8 @@ public:
        CMEMALLOC;
 private:
        bool hasVar;
-       VarType type;
+       VarType type1;
+       VarType type2;
        TunableParam param;
        int lowValue;
        int highValue;
@@ -37,6 +39,7 @@ public:
        ~SearchTuner();
        int getTunable(TunableParam param, TunableDesc *descriptor);
        int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+       int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
        SearchTuner *copyUsed();
        void randomMutate();
        uint getSize() { return usedSettings.getSize();}
index 1401b24..eeba3a2 100644 (file)
@@ -6,6 +6,11 @@ DefaultTuner::DefaultTuner() {
 int DefaultTuner::getTunable(TunableParam param, TunableDesc *descriptor) {
        return descriptor->defaultValue;
 }
+
 int DefaultTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
        return descriptor->defaultValue;
 }
+
+int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {
+       return descriptor->defaultValue;
+}
index 660c77d..012f420 100644 (file)
@@ -7,6 +7,7 @@ class Tuner {
 public:
        virtual int getTunable(TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
        virtual int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
+       virtual int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
        virtual ~Tuner() {}
        CMEMALLOC;
 };
@@ -16,6 +17,7 @@ public:
        DefaultTuner();
        int getTunable(TunableParam param, TunableDesc *descriptor);
        int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
+       int getVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor);
        CMEMALLOC;
 };
 
@@ -37,6 +39,6 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING};
 typedef enum Tunables Tunables;
 #endif
index ce749b1..0eebb17 100644 (file)
@@ -228,7 +228,7 @@ BooleanEdge CSolver::getBooleanFalse() {
 }
 
 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
-       return applyPredicateTable(predicate, inputs, numInputs, NULL);
+       return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
 }
 
 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {