From: bdemsky Date: Sun, 27 Aug 2017 08:14:12 +0000 (-0700) Subject: Convert structs to classes... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=c25ce5e80da20bb0eac14f371900bbf79bebb9b2 Convert structs to classes... --- diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 3dd9933..a7513d6 100644 --- 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 dee131d..f74965b 100644 --- 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 27cf8c7..1c5e58c 100644 --- 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 cef1e1f..aac331d 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -14,9 +14,7 @@ #include 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 221f562..47e22a1 100644 --- 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++) {