Fixing header bugs
authorHamed <hamed.gorjiara@gmail.com>
Tue, 19 Sep 2017 23:36:05 +0000 (16:36 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Tue, 19 Sep 2017 23:36:05 +0000 (16:36 -0700)
13 files changed:
src/AST/element.cc
src/AST/element.h
src/ASTAnalyses/Encoding/encodinggraph.cc
src/Backend/constraint.h
src/Backend/satelemencoder.cc
src/Backend/satencoder.cc
src/Backend/satfuncopencoder.cc
src/Collections/structs.h
src/Encoders/elementencoding.h
src/Encoders/naiveencoder.cc
src/Translator/sattranslator.cc
src/classlist.h
src/csolver.cc

index ed0a741..922f0a1 100644 (file)
@@ -5,6 +5,7 @@
 #include "function.h"
 #include "table.h"
 #include "csolver.h"
+#include "boolean.h"
 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
index b829a47..6d25328 100644 (file)
@@ -4,9 +4,9 @@
 #include "mymemory.h"
 #include "structs.h"
 #include "astnode.h"
+#include "corestructs.h"
 #include "functionencoding.h"
 #include "elementencoding.h"
-#include "boolean.h"
 
 class Element : public ASTNode {
 public:
@@ -14,6 +14,7 @@ public:
        virtual ~Element() {}
        Vector<ASTNode *> parents;
        ElementEncoding encoding;
+       inline ElementEncoding *getElementEncoding(){ return &encoding; }
        virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
        virtual void serialize(Serializer* serializer) =0;
        virtual void updateParents() {}
@@ -54,16 +55,11 @@ public:
        Set * getRange();
        void updateParents();
        Function * getFunction() {return function;}
+       inline FunctionEncoding *getElementFunctionEncoding() {return &functionencoding;}
        CMEMALLOC;
  private:
        Function *function;
 };
 
-static inline ElementEncoding *getElementEncoding(Element *e) {
-       return &e->encoding;
-}
 
-static inline FunctionEncoding *getElementFunctionEncoding(ElementFunction *func) {
-       return &func->functionencoding;
-}
 #endif
index 8fe908a..60437f5 100644 (file)
@@ -6,6 +6,7 @@
 #include "set.h"
 #include "csolver.h"
 #include "tunable.h"
+#include "boolean.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {
index 2f61d72..9506042 100644 (file)
@@ -10,9 +10,6 @@
 
 typedef int Literal;
 
-struct Edge;
-typedef struct Edge Edge;
-
 struct Node;
 typedef struct Node Node;
 
index 7dcb5de..27d5720 100644 (file)
@@ -6,7 +6,7 @@
 #include "set.h"
 
 Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
-       switch (getElementEncoding(elem)->type) {
+       switch (elem->getElementEncoding()->type) {
        case ONEHOT:
                return getElementValueOneHotConstraint(elem, value);
        case UNARY:
@@ -26,7 +26,7 @@ Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
 Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t value) {
        ASTNodeType type = elem->type;
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
-       ElementEncoding *elemEnc = getElementEncoding(elem);
+       ElementEncoding *elemEnc = elem->getElementEncoding();
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
                if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
                        return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i);
@@ -38,7 +38,7 @@ Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t va
 Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) {
        ASTNodeType type = elem->type;
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
-       ElementEncoding *elemEnc = getElementEncoding(elem);
+       ElementEncoding *elemEnc = elem->getElementEncoding();
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
                if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
                        return (elemEnc->numVars == 0) ? E_True : elemEnc->variables[i];
@@ -50,7 +50,7 @@ Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value)
 Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) {
        ASTNodeType type = elem->type;
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
-       ElementEncoding *elemEnc = getElementEncoding(elem);
+       ElementEncoding *elemEnc = elem->getElementEncoding();
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
                if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
                        if (elemEnc->numVars == 0)
@@ -69,7 +69,7 @@ Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) {
 Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, uint64_t value) {
        ASTNodeType type = element->type;
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
-       ElementEncoding *elemEnc = getElementEncoding(element);
+       ElementEncoding *elemEnc = element->getElementEncoding();
        if (elemEnc->low <= elemEnc->high) {
                if (value < elemEnc->low || value > elemEnc->high)
                        return E_False;
@@ -121,7 +121,7 @@ void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
 }
 
 void SATEncoder::generateElementEncoding(Element *element) {
-       ElementEncoding *encoding = getElementEncoding(element);
+       ElementEncoding *encoding = element->getElementEncoding();
        ASSERT(encoding->type != ELEM_UNASSIGNED);
        if (encoding->variables != NULL)
                return;
index 1fe98ce..fdeee9e 100644 (file)
@@ -131,7 +131,7 @@ Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 
 void SATEncoder::encodeElementSATEncoder(Element *element) {
        /* Check to see if we have already encoded this element. */
-       if (getElementEncoding(element)->variables != NULL)
+       if (element->getElementEncoding()->variables != NULL)
                return;
 
        /* Need to encode. */
@@ -164,7 +164,7 @@ void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
 }
 
 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
-       switch (getElementFunctionEncoding(function)->type) {
+       switch (function->getElementFunctionEncoding()->type) {
        case ENUMERATEIMPLICATIONS:
                encodeEnumTableElemFunctionSATEncoder(function);
                break;
index 9fc3c41..3f85fec 100644 (file)
@@ -200,8 +200,8 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
        encodeElementSATEncoder(elem0);
        Element *elem1 = constraint->inputs.get(1);
        encodeElementSATEncoder(elem1);
-       ElementEncoding *ee0 = getElementEncoding(elem0);
-       ElementEncoding *ee1 = getElementEncoding(elem1);
+       ElementEncoding *ee0 = elem0->getElementEncoding();
+       ElementEncoding *ee1 = elem1->getElementEncoding();
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
        switch (predicate->getOp()) {
index 2a85eae..6d06f54 100644 (file)
@@ -7,6 +7,7 @@
 #include "array.h"
 #include "corestructs.h"
 
+
 unsigned int table_entry_hash_function(TableEntry *This);
 bool table_entry_equals(TableEntry *key1, TableEntry *key2);
 unsigned int order_node_hash_function(OrderNode *This);
index 6797c66..37fff60 100644 (file)
@@ -1,8 +1,7 @@
 #ifndef ELEMENTENCODING_H
 #define ELEMENTENCODING_H
 #include "classlist.h"
-#include "naiveencoder.h"
-#include "constraint.h"
+#include "common.h"
 
 class ElementEncoding {
 public:
index 2d77608..ace0313 100644 (file)
@@ -63,7 +63,7 @@ void naiveEncodingPredicate(BooleanPredicate *This) {
 }
 
 void naiveEncodingElement(Element *This) {
-       ElementEncoding *encoding = getElementEncoding(This);
+       ElementEncoding *encoding = This->getElementEncoding();
        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
                encoding->setElementEncodingType(BINARYINDEX);
                encoding->encodingArrayInitialization();
@@ -75,9 +75,9 @@ void naiveEncodingElement(Element *This) {
                        Element *element = function->inputs.get(i);
                        naiveEncodingElement(element);
                }
-               FunctionEncoding *encoding = getElementFunctionEncoding(function);
+               FunctionEncoding *encoding = function->getElementFunctionEncoding();
                if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
-                       getElementFunctionEncoding(function)->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
+                       function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
        }
 }
 
index 792d58b..d49883e 100644 (file)
@@ -57,7 +57,7 @@ uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemE
 }
 
 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
-       ElementEncoding *elemEnc = getElementEncoding(element);
+       ElementEncoding *elemEnc = element->getElementEncoding();
        if (elemEnc->numVars == 0)//case when the set has only one item
                return element->getRange()->getElement(0);
        switch (elemEnc->type) {
index 5cddf58..2c9a000 100644 (file)
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
 
-#include "mymemory.h"
 #include <inttypes.h>
 #include "classes.h"
-#include "AST/astnode.h"
+#include "astnode.h"
 
 
 class BooleanOrder;
@@ -67,10 +66,14 @@ class EncodingGraph;
 class EncodingNode;
 class EncodingEdge;
 
+class ElementEncoding;
+class FunctionEncoding;
+
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 typedef int TunableParam;
-
+struct Edge;
+typedef struct Edge Edge;
 #endif
index 575a12b..d0d2c06 100644 (file)
@@ -21,6 +21,7 @@
 #include "preprocess.h"
 #include "serializer.h"
 #include "deserializer.h"
+#include "naiveencoder.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),