edits

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/element.cc b/src/AST/element.cc
index 05f6cefdc9a0ab621d092f6747687a7f2691c167..ca42290953e7495126f37aaea3f8161236b2b193 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 076e83186209ea9f9e3dee0da2ed603c58cba6be..db1cbfb6b00f7f203851af0500451394bfced602 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -43,14 +43,16 @@ public:
 class ElementFunction : public Element {
 public:
        ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
-       Function *function;
        Array<Element *> inputs;
        BooleanEdge overflowstatus;
        FunctionEncoding functionencoding;
        Element *clone(CSolver *solver, CloneMap *map);
        Set * getRange();
        void updateParents();
+       Function * getFunction() {return function;}
        CMEMALLOC;
+ private:
+       Function *function;
 };
 
 static inline ElementEncoding *getElementEncoding(Element *e) {

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index e337e56aa132e86e0f79aa1714ba5887ea858df3..9c0a29e7b70a882a159114d081b96a70984b0f90 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -1,6 +1,7 @@
 #include "encodinggraph.h"
 #include "iterator.h"
 #include "element.h"
+#include "function.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {
@@ -8,30 +9,86 @@ 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::processElement(Element *e) {
-       switch(e->type) {
-       case ELEMSET: {
-               break;
-       }
-       case ELEMFUNCRETURN: {
-               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 ELEMCONST: {
-               break;
+}
+
+void EncodingGraph::processFunction(ElementFunction *ef) {
+       Function *f=ef->getFunction();
+       if (f->type==OPERATORFUNC) {
+               FunctionOperator *fo=(FunctionOperator*)f;
+               ArithOp op=fo->op;
        }
-       default:
-               ASSERT(0);
+}
+
+void EncodingGraph::processPredicate(BooleanPredicate *b) {
+
+}
+
+EncodingNode * EncodingGraph::createNode(Element *e) {
+       Set *s = e->getRange();
+       EncodingNode *n = encodingMap.get(s);
+       if (n == NULL) {
+               n = new EncodingNode(s);
+               encodingMap.put(s, n);
        }
+       n->addElement(e);
+       return n;
+}
+
+void EncodingNode::addElement(Element *e) {
+       elements.add(e);
+}
+
+EncodingEdge::EncodingEdge(EncodingNode *_l, EncodingNode *_r) :
+       left(_l),
+       right(_r),
+       dst(NULL)
+{
+}
+
+EncodingEdge::EncodingEdge(EncodingNode *_left, EncodingNode *_right, EncodingNode *_dst) :
+       left(_left),
+       right(_right),
+       dst(_dst)
+{
+}
+
+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;
 }

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index 452a0348e67ad2f0c4e44dba7ba4fec9a4bd727a..adb467cc6b279faaf7e7e3c62fb49fa5a1e53b7b 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -3,33 +3,51 @@
 #include "classlist.h"
 #include "structs.h"
 
+uint hashEncodingEdge(EncodingEdge *edge);
+bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
+
+typedef Hashtable<EncodingEdge *, EncodingEdge *, uintptr_t, PTRSHIFT, hashEncodingEdge, equalsEncodingEdge> HashtableEdge;
+
 class EncodingGraph {
  public:
        EncodingGraph(CSolver * solver);
-       EncodingNode * getNode(Element * element);
        void buildGraph();
        
        CMEMALLOC;
  private:
        CSolver * solver;
-       HashTableEncoding encodingMap;
+       HashtableEncoding encodingMap;
+       HashtableEdge edgeMap;
        void processElement(Element *e);
+       void processFunction(ElementFunction *f);
+       void processPredicate(BooleanPredicate *b);
+       EncodingNode * createNode(Element *e);
 
 };
 
 class EncodingNode {
  public:
-       
+       EncodingNode(Set *_s);
+       void addElement(Element *e);
        CMEMALLOC;
  private:
-       
+       Set *s;
+       HashsetElement elements;
 };
 
 class EncodingEdge {
  public:
-
+       EncodingEdge(EncodingNode *_l, EncodingNode *_r);
+       EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d);
        CMEMALLOC;
  private:
+       EncodingNode *left;
+       EncodingNode *right;
+       EncodingNode *dst;
+       friend uint hashEncodingEdge(EncodingEdge *edge);
+       friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
+
 };
 
+
 #endif

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..7e6a67d239def78348bb3d4443b1a683735e4354 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;

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..6ee69ab5614978e995dbe2afadcf8b60595095bb 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -32,7 +32,7 @@ typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, PTRSHIFT, order_pair_hash
 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;