Fixing header bugs

diff --git a/src/AST/element.cc b/src/AST/element.cc
index ed0a7416853453316d44d2bb565fa991d8326389..922f0a107a8635e428c474a01553e8f7bdfdef20 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -5,6 +5,7 @@
 #include "function.h"
 #include "table.h"
 #include "csolver.h"
 #include "function.h"
 #include "table.h"
 #include "csolver.h"

+#include "boolean.h"

 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),

diff --git a/src/AST/element.h b/src/AST/element.h
index b829a47f07a14d32a6c7a4006cd4098c17d3a19d..6d253280618f74fefd6e99e0f2598ec7f37cf337 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -4,9 +4,9 @@
 #include "mymemory.h"
 #include "structs.h"
 #include "astnode.h"
 #include "mymemory.h"
 #include "structs.h"
 #include "astnode.h"

+#include "corestructs.h"

 #include "functionencoding.h"
 #include "elementencoding.h"
 #include "functionencoding.h"
 #include "elementencoding.h"

-#include "boolean.h"

 
 class Element : public ASTNode {
 public:
 
 class Element : public ASTNode {
 public:


@@ -14,6 +14,7 @@ public:
        virtual ~Element() {}
        Vector<ASTNode *> parents;
        ElementEncoding encoding;
        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() {}
        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;}
        Set * getRange();
        void updateParents();
        Function * getFunction() {return function;}

+       inline FunctionEncoding *getElementFunctionEncoding() {return &functionencoding;}

        CMEMALLOC;
  private:
        Function *function;
 };
 
        CMEMALLOC;
  private:
        Function *function;
 };
 

-static inline ElementEncoding *getElementEncoding(Element *e) {
-       return &e->encoding;
-}

 
 

-static inline FunctionEncoding *getElementFunctionEncoding(ElementFunction *func) {
-       return &func->functionencoding;
-}

 #endif
 #endif

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 8fe908a50a475938b60dad9b000e734e04fb6d49..60437f5ea4fd266f4f62437da3e9d255140b7943 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -6,6 +6,7 @@
 #include "set.h"
 #include "csolver.h"
 #include "tunable.h"
 #include "set.h"
 #include "csolver.h"
 #include "tunable.h"

+#include "boolean.h"

 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 2f61d72a41e31d86acd1ca814a7eb3df43ff38e5..95060423a6fe27902ae1cea4d02c4994e278b7b9 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -10,9 +10,6 @@
 
 typedef int Literal;
 
 
 typedef int Literal;
 

-struct Edge;
-typedef struct Edge Edge;
-

 struct Node;
 typedef struct Node Node;
 
 struct Node;
 typedef struct Node Node;
 

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 7dcb5de6c10ebf7894e7946a14e6d431448430de..27d5720abc32d1beca742ef20f65b0937acb601b 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -6,7 +6,7 @@
 #include "set.h"
 
 Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
 #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:
        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);
 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);
        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);
 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];
        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);
 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)
        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);
 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;
        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) {
 }
 
 void SATEncoder::generateElementEncoding(Element *element) {

-       ElementEncoding *encoding = getElementEncoding(element);
+       ElementEncoding *encoding = element->getElementEncoding();

        ASSERT(encoding->type != ELEM_UNASSIGNED);
        if (encoding->variables != NULL)
                return;
        ASSERT(encoding->type != ELEM_UNASSIGNED);
        if (encoding->variables != NULL)
                return;

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 1fe98ce398af1bf4e54b854b410448b72552914d..fdeee9ee8816faf0c812a7696bde8e69b6ba95eb 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -131,7 +131,7 @@ Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 
 void SATEncoder::encodeElementSATEncoder(Element *element) {
        /* Check to see if we have already encoded this element. */
 
 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. */
                return;
 
        /* Need to encode. */


@@ -164,7 +164,7 @@ void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
 }
 
 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
 }
 
 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {

-       switch (getElementFunctionEncoding(function)->type) {
+       switch (function->getElementFunctionEncoding()->type) {

        case ENUMERATEIMPLICATIONS:
                encodeEnumTableElemFunctionSATEncoder(function);
                break;
        case ENUMERATEIMPLICATIONS:
                encodeEnumTableElemFunctionSATEncoder(function);
                break;

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 9fc3c4124f4f1187836fc93b9ebaf59c458ab055..3f85fec3700ac5a7e7905f1f627f7f183b320931 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -200,8 +200,8 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
        encodeElementSATEncoder(elem0);
        Element *elem1 = constraint->inputs.get(1);
        encodeElementSATEncoder(elem1);
        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()) {
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
        switch (predicate->getOp()) {

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 2a85eaead2d96bd1ccd616b45c2f35301eb777b8..6d06f549d616b3b869d0022b5b6938ced17a12fa 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -7,6 +7,7 @@
 #include "array.h"
 #include "corestructs.h"
 
 #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);
 unsigned int table_entry_hash_function(TableEntry *This);
 bool table_entry_equals(TableEntry *key1, TableEntry *key2);
 unsigned int order_node_hash_function(OrderNode *This);

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 6797c66bf530b9024fba0fd3627f43643799ce04..37fff60943cf250ced384cc78a0fed3c76bcd1a4 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -1,8 +1,7 @@
 #ifndef ELEMENTENCODING_H
 #define ELEMENTENCODING_H
 #include "classlist.h"
 #ifndef ELEMENTENCODING_H
 #define ELEMENTENCODING_H
 #include "classlist.h"

-#include "naiveencoder.h"
-#include "constraint.h"
+#include "common.h"

 
 class ElementEncoding {
 public:
 
 class ElementEncoding {
 public:

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 2d77608772ba3d01351aa0a7b89e857b7c9d02ca..ace03131718e8e35b9a6d4f855eb656f5dc33183 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -63,7 +63,7 @@ void naiveEncodingPredicate(BooleanPredicate *This) {
 }
 
 void naiveEncodingElement(Element *This) {
 }
 
 void naiveEncodingElement(Element *This) {

-       ElementEncoding *encoding = getElementEncoding(This);
+       ElementEncoding *encoding = This->getElementEncoding();

        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
                encoding->setElementEncodingType(BINARYINDEX);
                encoding->encodingArrayInitialization();
        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);
                }
                        Element *element = function->inputs.get(i);
                        naiveEncodingElement(element);
                }

-               FunctionEncoding *encoding = getElementFunctionEncoding(function);
+               FunctionEncoding *encoding = function->getElementFunctionEncoding();

                if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
                if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)

-                       getElementFunctionEncoding(function)->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
+                       function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);

        }
 }
 
        }
 }
 

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index 792d58b38bc62f7370b253b68e65007bb7cd2e64..d49883e447642641fdd2f0f4073015763ebc7887 100644 (file)
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -57,7 +57,7 @@ uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemE
 }
 
 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
 }
 
 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) {
        if (elemEnc->numVars == 0)//case when the set has only one item
                return element->getRange()->getElement(0);
        switch (elemEnc->type) {

diff --git a/src/classlist.h b/src/classlist.h
index 5cddf5846a35d53b71e7c6f0810697f5645551fe..2c9a00048c8b0bc2d61a52c1dc1470e9653cd6f7 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -10,10 +10,9 @@
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
 
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
 

-#include "mymemory.h"

 #include <inttypes.h>
 #include "classes.h"
 #include <inttypes.h>
 #include "classes.h"

-#include "AST/astnode.h"
+#include "astnode.h"

 
 
 class BooleanOrder;
 
 
 class BooleanOrder;


@@ -67,10 +66,14 @@ class EncodingGraph;
 class EncodingNode;
 class EncodingEdge;
 
 class EncodingNode;
 class EncodingEdge;
 

+class ElementEncoding;
+class FunctionEncoding;
+

 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 typedef int TunableParam;
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 typedef int TunableParam;

-
+struct Edge;
+typedef struct Edge Edge;

 #endif
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index 575a12b6f347714e5711eccd08c6131ec381de81..d0d2c0612497800a6ee891a42f229163443b2797 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -21,6 +21,7 @@
 #include "preprocess.h"
 #include "serializer.h"
 #include "deserializer.h"
 #include "preprocess.h"
 #include "serializer.h"
 #include "deserializer.h"

+#include "naiveencoder.h"

 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),