Convert structs to classes...

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 3dd9933802964758d092a09e34af4cca4cb00433..a7513d6120eb9180c8b33f127742b4f625e21597 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -15,42 +15,39 @@
 
 //TODO: Should handle sharing of AST Nodes without recoding them a second time
 
-SATEncoder *allocSATEncoder(CSolver *solver) {
-       SATEncoder *This = (SATEncoder *)ourmalloc(sizeof (SATEncoder));
-       This->solver = solver;
-       This->varcount = 1;
-       This->cnf = createCNF();
-       return This;
+SATEncoder::SATEncoder(CSolver * _solver) :
+       varcount(1),
+       cnf(createCNF()),
+       solver(_solver) {
 }
 
-void deleteSATEncoder(SATEncoder *This) {
-       deleteCNF(This->cnf);
-       ourfree(This);
+SATEncoder::~SATEncoder() {
+       deleteCNF(cnf);
 }
 
-void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
+void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        HSIteratorBoolean *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                Boolean *constraint = iterator->next();
                model_print("Encoding All ...\n\n");
-               Edge c = encodeConstraintSATEncoder(This, constraint);
+               Edge c = encodeConstraintSATEncoder(constraint);
                model_print("Returned Constraint in EncodingAll:\n");
                ASSERT( !equalsEdge(c, E_BOGUS));
-               addConstraintCNF(This->cnf, c);
+               addConstraintCNF(cnf, c);
        }
        delete iterator;
 }
 
-Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
        switch (GETBOOLEANTYPE(constraint)) {
        case ORDERCONST:
-               return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
+               return encodeOrderSATEncoder(this, (BooleanOrder *) constraint);
        case BOOLEANVAR:
-               return encodeVarSATEncoder(This, (BooleanVar *) constraint);
+               return encodeVarSATEncoder(this, (BooleanVar *) constraint);
        case LOGICOP:
-               return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
+               return encodeLogicSATEncoder(this, (BooleanLogic *) constraint);
        case PREDICATEOP:
-               return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
+               return encodePredicateSATEncoder(this, (BooleanPredicate *) constraint);
        default:
                model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
                exit(-1);
@@ -76,7 +73,7 @@ Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
        Edge array[constraint->inputs.getSize()];
        for (uint i = 0; i < constraint->inputs.getSize(); i++)
-               array[i] = encodeConstraintSATEncoder(This, constraint->inputs.get(i));
+               array[i] = This->encodeConstraintSATEncoder(constraint->inputs.get(i));
 
        switch (constraint->op) {
        case L_AND:

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index dee131dc5b4dd584962e0e20d000d76fcad8f3c9..f74965b4af8ac92333ca5041d3487e7cacbd7ae7 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -5,32 +5,33 @@
 #include "structs.h"
 #include "inc_solver.h"
 #include "constraint.h"
-
-struct SATEncoder {
-       uint varcount;
-       CNF *cnf;
-       CSolver *solver;
-};
-
 #include "satelemencoder.h"
 #include "satorderencoder.h"
 #include "satfunctableencoder.h"
 
-SATEncoder *allocSATEncoder(CSolver *solver);
-void deleteSATEncoder(SATEncoder *This);
-void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
-Edge getNewVarSATEncoder(SATEncoder *This);
-void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray);
-Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
-Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint);
-Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint);
-Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
 
+class SATEncoder {
+ public:
+       uint varcount;
+       CNF *cnf;
+       CSolver *solver;
+
+       SATEncoder(CSolver *solver);
+       ~SATEncoder();
+       void encodeAllSATEncoder(CSolver *csolver);
+       Edge encodeConstraintSATEncoder(Boolean *constraint);
+       MEMALLOC;
+};
 
 
-void encodeElementSATEncoder(SATEncoder *encoder, Element *This);
-void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
-void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
+       Edge getNewVarSATEncoder(SATEncoder *This);
+       void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray);
 
+       Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint);
+       Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint);
+       Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
+       Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
+       void encodeElementSATEncoder(SATEncoder *encoder, Element *This);
+       void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
+       void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
 #endif

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 27cf8c7664073b749d0fff7d31f440d76266179e..1c5e58cb425baa1adce1b993c358309e7563689f 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -21,7 +21,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat
        uint size = table->entries->getSize();
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
        Edge constraints[size];
-       Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus);
+       Edge undefConst = This->encodeConstraintSATEncoder(constraint->undefStatus);
        printCNF(undefConst);
        model_print("**\n");
        HSIteratorTableEntry *iterator = table->entries->iterator();
@@ -101,7 +101,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
                vals[i] = set->getElement(indices[i]);
        }
        bool hasOverflow = false;
-       Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus);
+       Edge undefConstraint = This->encodeConstraintSATEncoder(constraint->undefStatus);
        printCNF(undefConstraint);
        bool notfinished = true;
        while (notfinished) {
@@ -202,7 +202,7 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction
                        break;
                }
                case FLAGFORCEUNDEFINED: {
-                       Edge undefConst = encodeConstraintSATEncoder(This, func->overflowstatus);
+                       Edge undefConst = This->encodeConstraintSATEncoder(func->overflowstatus);
                        row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
                        break;
                }
@@ -250,7 +250,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
                vals[i] = set->getElement(indices[i]);
        }
 
-       Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
+       Edge undefConstraint = This->encodeConstraintSATEncoder(elemFunc->overflowstatus);
        bool notfinished = true;
        while (notfinished) {
                Edge carray[numDomains + 1];

diff --git a/src/classlist.h b/src/classlist.h
index cef1e1fe6bcc8fd4f46b50f73c71a0a9f945754a..aac331d1154c75139e9cb4d2b00cb30399685b5d 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -14,9 +14,7 @@
 #include <inttypes.h>
 
 class CSolver;
-struct SATEncoder;
-typedef struct SATEncoder SATEncoder;
-
+class SATEncoder;
 class Boolean;
 class BooleanOrder;
 class BooleanVar;
@@ -59,9 +57,6 @@ typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 
-struct OrderEncoder;
-typedef struct OrderEncoder OrderEncoder;
-
 class Tuner;
 class TunableDesc;
 

diff --git a/src/csolver.cc b/src/csolver.cc
index 221f5628a275702badd9531e56146511f52f3c39..47e22a14c159f2a283ea9e06fcbd3fe0fded3ce0 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -15,7 +15,7 @@
 
 CSolver::CSolver() : unsat(false) {
        tuner = new Tuner();
-       satEncoder = allocSATEncoder(this);
+       satEncoder = new SATEncoder(this);
 }
 
 /** This function tears down the solver and the entire AST */
@@ -56,7 +56,7 @@ CSolver::~CSolver() {
                delete allFunctions.get(i);
        }
 
-       deleteSATEncoder(satEncoder);
+       delete satEncoder;
        delete tuner;
 }
 
@@ -201,7 +201,7 @@ int CSolver::startEncoding() {
        computePolarities(this);
        orderAnalysis(this);
        naiveEncodingDecision(this);
-       encodeAllSATEncoder(this, satEncoder);
+       satEncoder->encodeAllSATEncoder(this);
        int result = solveCNF(satEncoder->cnf);
        model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
        for (int i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) {