Merge

diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc
index 827f9e1c02fdbff2d9354b9d1059bbf4125c9162..bc58431acb3693a62748590cd33317403f4b083d 100644 (file)
--- a/src/AST/asthash.cc
+++ b/src/AST/asthash.cc
@@ -104,7 +104,7 @@ uint hashElement(Element *e) {
        }
        case ELEMFUNCRETURN: {
                ElementFunction *ef = (ElementFunction *) e;
-               return ((uint)(uintptr_t) ef->function) ^
+               return ((uint)(uintptr_t) ef->getFunction()) ^
                                         ((uint)(uintptr_t) ef->overflowstatus) ^
                                         hashArray(&ef->inputs);
        }
@@ -127,7 +127,7 @@ bool compareElement(Element *e1, Element *e2) {
        case ELEMFUNCRETURN: {
                ElementFunction *ef1 = (ElementFunction *) e1;
                ElementFunction *ef2 = (ElementFunction *) e2;
-               return (ef1->function == ef2->function) &&
+               return (ef1->getFunction() == ef2->getFunction()) &&
                                         (ef1->overflowstatus == ef2->overflowstatus) &&
                                         compareArray(&ef1->inputs, &ef2->inputs);
        }

diff --git a/src/AST/astops.h b/src/AST/astops.h
index f26326f3f2c07b3e9668d08af91daf2460e9661d..ebe9fc07b690ff1fb35f9a5b2df47ee865be1eff 100644 (file)
--- a/src/AST/astops.h
+++ b/src/AST/astops.h
@@ -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 --git a/src/AST/boolean.h b/src/AST/boolean.h
index df1f4e8c152f1f86f88feddfb0e6d3b1eb8167e9..6449a8e0f0eed13ff7559839123d25b937442f19 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -65,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 {

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 2617022b9abcdfdef75bbcf33fc20552932c1dd3..ed0a7416853453316d44d2bb565fa991d8326389 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -23,10 +23,10 @@ ElementSet::ElementSet(ASTNodeType _type, Set *s) :
 
 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) :

diff --git a/src/AST/element.h b/src/AST/element.h
index 19e35b68f5d07f6c50e78488481f6421032b147f..b829a47f07a14d32a6c7a4006cd4098c17d3a19d 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -46,7 +46,6 @@ public:
 class ElementFunction : public Element {
 public:
        ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
-       Function *function;
        Array<Element *> inputs;
        BooleanEdge overflowstatus;
        FunctionEncoding functionencoding;
@@ -54,7 +53,10 @@ public:
        virtual void serialize(Serializer* serializer);
        Set * getRange();
        void updateParents();
+       Function * getFunction() {return function;}
        CMEMALLOC;
+ private:
+       Function *function;
 };
 
 static inline ElementEncoding *getElementEncoding(Element *e) {

diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index 7f63faa042fcd6da4924f1316586ecd49fd81d5c..e3ae1db970280646bd4c30c17689c7374f415522 100644 (file)
--- a/src/AST/predicate.cc
+++ b/src/AST/predicate.cc
@@ -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) {

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 2f292b21c37741b3d9e3815bcffed27091278f41..beaebc9b09989122f45d64573a0e7868c499f0b2 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -23,9 +23,11 @@ public:
        bool evalPredicateOperator(uint64_t *inputs);
        Predicate *clone(CSolver *solver, CloneMap *map);
        virtual void serialize(Serializer* serializer);
-       CompOp op;
        Array<Set *> domains;
+       CompOp getOp() {return op;}
        CMEMALLOC;
+ private:
+       CompOp op;
 };
 
 class PredicateTable : public Predicate {

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index e337e56aa132e86e0f79aa1714ba5887ea858df3..8d34d473d6fcaec7a40930497c138b560004b1b1 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -1,6 +1,11 @@
 #include "encodinggraph.h"
 #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) {
@@ -8,30 +13,212 @@ EncodingGraph::EncodingGraph(CSolver * _solver) :
 
 }
 
-EncodingNode * EncodingGraph::getNode(Element * element) {
-       return NULL;
-}
-
 void EncodingGraph::buildGraph() {
        ElementIterator it(solver);
        while(it.hasNext()) {
                Element * e = it.next();
-               processElement(e);
+               switch(e->type) {
+               case ELEMSET:
+               case ELEMFUNCRETURN:
+                       processElement(e);
+                       break;
+               case ELEMCONST:
+                       break;
+               default:
+                       ASSERT(0);
+               }
+       }
+}
+
+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) {
-       switch(e->type) {
-       case ELEMSET: {
-               break;
+       uint size=e->parents.getSize();
+       for(uint i=0;i<size;i++) {
+               ASTNode * n = e->parents.get(i);
+               switch(n->type) {
+               case PREDICATEOP:
+                       processPredicate((BooleanPredicate *)n);
+                       break;
+               case ELEMFUNCRETURN:
+                       processFunction((ElementFunction *)n);
+                       break;
+               default:
+                       ASSERT(0);
+               }
        }
-       case ELEMFUNCRETURN: {
-               break;
+}
+
+void EncodingGraph::processFunction(ElementFunction *ef) {
+       Function *f=ef->getFunction();
+       if (f->type==OPERATORFUNC) {
+               FunctionOperator *fo=(FunctionOperator*)f;
+               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++;
        }
-       case ELEMCONST: {
-               break;
+}
+
+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);
+               }
        }
-       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;
+}
+
+void EncodingNode::addElement(Element *e) {
+       elements.add(e);
+}
+
+EncodingEdge::EncodingEdge(EncodingNode *_l, EncodingNode *_r) :
+       left(_l),
+       right(_r),
+       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),
+       encoding(EDGE_UNASSIGNED),
+       numArithOps(0),
+       numEquals(0),
+       numComparisons(0)
+{
+}
+
+uint hashEncodingEdge(EncodingEdge *edge) {
+       uintptr_t hash=(((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6);
+       return (uint) hash;
+}
+
+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();
 }

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index 452a0348e67ad2f0c4e44dba7ba4fec9a4bd727a..e44ccfd69c539b3eaaec6afdc7b1cce018a7a17e 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -3,33 +3,91 @@
 #include "classlist.h"
 #include "structs.h"
 
+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:
        EncodingGraph(CSolver * solver);
-       EncodingNode * getNode(Element * element);
        void buildGraph();
        
        CMEMALLOC;
  private:
        CSolver * solver;
-       HashTableEncoding encodingMap;
-       void processElement(Element *e);
+       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

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index ed761e3b62eabc8a28eb32cc85899bd20db1f1d5..7dcb5de6c10ebf7894e7946a14e6d431448430de 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -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;

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 4020ad625b49271aa1c255e10645ad312ef4aca2..1fe98ce398af1bf4e54b854b410448b72552914d 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -151,7 +151,7 @@ void SATEncoder::encodeElementSATEncoder(Element *element) {
 }
 
 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
-       switch (function->function->type) {
+       switch (function->getFunction()->type) {
        case TABLEFUNC:
                encodeTableElementFunctionSATEncoder(function);
                break;

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index bfd4ea6b6cb63f0921f7707458d5877aa4ac4afb..9fc3c4124f4f1187836fc93b9ebaf59c458ab055 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -88,7 +88,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 #ifdef TRACE_DEBUG
        model_print("Operator Function ...\n");
 #endif
-       FunctionOperator *function = (FunctionOperator *) func->function;
+       FunctionOperator *function = (FunctionOperator *) func->getFunction();
        uint numDomains = func->inputs.getSize();
 
        /* Call base encoders for children */
@@ -115,7 +115,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                Edge carray[numDomains + 1];
 
                uint64_t result = function->applyFunctionOperator(numDomains, vals);
-               bool isInRange = ((FunctionOperator *)func->function)->isInRangeFunction(result);
+               bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
                bool needClause = isInRange;
                if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
                        needClause = true;
@@ -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:

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index c8d53d168936ed2a9c883b7caaf4a92faa98163e..961d810f1766b7850b39926d6fd69d471111047d 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -177,10 +177,10 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 }
 
 void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
-       UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
+       UndefinedBehavior undefStatus = ((FunctionTable *) func->getFunction())->undefBehavior;
        ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
        Array<Element *> *elements = &func->inputs;
-       Table *table = ((FunctionTable *) (func->function))->table;
+       Table *table = ((FunctionTable *) (func->getFunction()))->table;
        uint size = table->getSize();
        Edge constraints[size];
        SetIteratorTableEntry *iterator = table->getEntries();
@@ -220,7 +220,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 #ifdef TRACE_DEBUG
        model_print("Enumeration Table functions ...\n");
 #endif
-       ASSERT(elemFunc->function->type == TABLEFUNC);
+       ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
        //First encode children
        Array<Element *> *elements = &elemFunc->inputs;
        for (uint i = 0; i < elements->getSize(); i++) {
@@ -228,7 +228,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                encodeElementSATEncoder(elem);
        }
 
-       FunctionTable *function = (FunctionTable *)elemFunc->function;
+       FunctionTable *function = (FunctionTable *)elemFunc->getFunction();
        switch (function->undefBehavior) {
        case SATC_IGNOREBEHAVIOR:
        case SATC_FLAGFORCEUNDEFINED:

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index e6f451ed3d6ba0f0b9997104ac2c5f3dad40b698..d5d6f5ef74f72678c98007a13e4823063394931e 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -26,13 +26,16 @@ 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;
 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 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 --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index d7585f4bc0372adfde75579a0c6781f227da455e..6797c66bf530b9024fba0fd3627f43643799ce04 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -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);

diff --git a/src/Serialize/serializer.h b/src/Serialize/serializer.h
index 12bff1306ecd9b47c7e77753bd23fbbab3a2e338..e6d2b50bce8707d23ae4a379c411ff936926a957 100644 (file)
--- a/src/Serialize/serializer.h
+++ b/src/Serialize/serializer.h
@@ -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);

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index bdcd1967cbf452625dc7af666e645ef650a51716..792d58b38bc62f7370b253b68e65007bb7cd2e64 100644 (file)
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -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);

diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index 52c7a704896d70ea2a4a985db05dfd4ad3ea6cf6..3e9586096e36a1d0121db35b760556c49b6597f2 100644 (file)
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -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);

diff --git a/src/Tuner/searchtuner.h b/src/Tuner/searchtuner.h
index 20edb7d8537e0a27fc10bb9ae979785ec9fa9a64..1464849e520f2b905a1627071af6760f3f7ea23c 100644 (file)
--- a/src/Tuner/searchtuner.h
+++ b/src/Tuner/searchtuner.h
@@ -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();}

diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index 1401b24bbb86ab502e979aeddbc081f5d5eb0f9d..eeba3a29de8ef4b46e4071dd47ef5e0b20f64bd5 100644 (file)
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -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;
+}

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 660c77db7ab0e64162b510036aaceb0f88c64235..012f420d7725bb2feb43c731d57a103b12bf8938 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -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