More OO conversion
authorbdemsky <bdemsky@uci.edu>
Mon, 28 Aug 2017 00:55:25 +0000 (17:55 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 28 Aug 2017 00:55:25 +0000 (17:55 -0700)
src/Backend/satelemencoder.cc
src/Backend/satelemencoder.h [deleted file]
src/Backend/satencoder.cc
src/Backend/satencoder.h
src/Backend/satfuncopencoder.cc
src/Backend/satfuncopencoder.h [deleted file]
src/Backend/satfunctableencoder.cc
src/Backend/satfunctableencoder.h [deleted file]
src/Backend/satorderencoder.cc
src/Backend/satorderencoder.h [deleted file]

index 504f92c..2cb423d 100644 (file)
@@ -5,19 +5,19 @@
 #include "element.h"
 #include "set.h"
 
-Edge getElementValueConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
        switch (getElementEncoding(elem)->type) {
        case ONEHOT:
-               return getElementValueOneHotConstraint(This, elem, value);
+               return getElementValueOneHotConstraint(elem, value);
        case UNARY:
-               return getElementValueUnaryConstraint(This, elem, value);
+               return getElementValueUnaryConstraint(elem, value);
        case BINARYINDEX:
-               return getElementValueBinaryIndexConstraint(This, elem, value);
+               return getElementValueBinaryIndexConstraint(elem, value);
        case ONEHOTBINARY:
                ASSERT(0);
                break;
        case BINARYVAL:
-               return getElementValueBinaryValueConstraint(This, elem, value);
+               return getElementValueBinaryValueConstraint(elem, value);
                break;
        default:
                ASSERT(0);
@@ -26,19 +26,19 @@ Edge getElementValueConstraint(SATEncoder *This, Element *elem, uint64_t value)
        return E_BOGUS;
 }
 
-Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t value) {
        ASTNodeType type = GETELEMENTTYPE(elem);
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding *elemEnc = getElementEncoding(elem);
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
                if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
-                       return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, i);
+                       return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i);
                }
        }
        return E_False;
 }
 
-Edge getElementValueOneHotConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) {
        ASTNodeType type = GETELEMENTTYPE(elem);
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding *elemEnc = getElementEncoding(elem);
@@ -50,7 +50,7 @@ Edge getElementValueOneHotConstraint(SATEncoder *This, Element *elem, uint64_t v
        return E_False;
 }
 
-Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) {
        ASTNodeType type = GETELEMENTTYPE(elem);
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding *elemEnc = getElementEncoding(elem);
@@ -63,13 +63,13 @@ Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t va
                        else if ((i + 1) == elemEnc->encArraySize)
                                return elemEnc->variables[i - 1];
                        else
-                               return constraintAND2(This->getCNF(), elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
+                               return constraintAND2(cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
                }
        }
        return E_False;
 }
 
-Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, uint64_t value) {
+Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, uint64_t value) {
        ASTNodeType type = GETELEMENTTYPE(element);
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
        ElementEncoding *elemEnc = getElementEncoding(element);
@@ -83,7 +83,7 @@ Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, ui
        }
 
        uint64_t valueminusoffset = value - elemEnc->offset;
-       return generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, valueminusoffset);
+       return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
 }
 
 void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
@@ -91,57 +91,57 @@ void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
        This->variables = (Edge *)ourmalloc(sizeof(Edge) * numVars);
 }
 
-void generateBinaryValueEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYVAL);
        allocElementConstraintVariables(encoding, encoding->numBits);
-       getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+       getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
 }
 
-void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
-       getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+       getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
 }
 
-void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
        allocElementConstraintVariables(encoding, encoding->encArraySize);
-       getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+       getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
        for (uint i = 0; i < encoding->numVars; i++) {
                for (uint j = i + 1; j < encoding->numVars; j++) {
-                       addConstraintCNF(This->getCNF(), constraintNegate(constraintAND2(This->getCNF(), encoding->variables[i], encoding->variables[j])));
+                       addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
                }
        }
-       addConstraintCNF(This->getCNF(), constraintOR(This->getCNF(), encoding->numVars, encoding->variables));
+       addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
 }
 
-void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
        allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
-       getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+       getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
        //Add unary constraint
        for (uint i = 1; i < encoding->numVars; i++) {
-               addConstraintCNF(This->getCNF(), constraintOR2(This->getCNF(), encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
+               addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
        }
 }
 
-void generateElementEncoding(SATEncoder *This, Element *element) {
+void SATEncoder::generateElementEncoding(Element *element) {
        ElementEncoding *encoding = getElementEncoding(element);
        ASSERT(encoding->type != ELEM_UNASSIGNED);
        if (encoding->variables != NULL)
                return;
        switch (encoding->type) {
        case ONEHOT:
-               generateOneHotEncodingVars(This, encoding);
+               generateOneHotEncodingVars(encoding);
                return;
        case BINARYINDEX:
-               generateBinaryIndexEncodingVars(This, encoding);
+               generateBinaryIndexEncodingVars(encoding);
                return;
        case UNARY:
-               generateUnaryEncodingVars(This, encoding);
+               generateUnaryEncodingVars(encoding);
                return;
        case ONEHOTBINARY:
                return;
        case BINARYVAL:
-               generateBinaryValueEncodingVars(This, encoding);
+               generateBinaryValueEncodingVars(encoding);
                return;
        default:
                ASSERT(0);
diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h
deleted file mode 100644 (file)
index d75f2f8..0000000
+++ /dev/null
@@ -1,15 +0,0 @@
-#ifndef SATELEMENTENCODER_H
-#define SATELEMENTENCODER_H
-
-Edge getElementValueOneHotConstraint(SATEncoder *This, Element *elem, uint64_t value);
-Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t value);
-Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *element, uint64_t value);
-Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, uint64_t value);
-Edge getElementValueConstraint(SATEncoder *encoder, Element *This, uint64_t value);
-void allocElementConstraintVariables(ElementEncoding *This, uint numVars);
-void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateBinaryValueEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateElementEncoding(SATEncoder *This, Element *element);
-#endif
index 977147f..838170f 100644 (file)
@@ -11,7 +11,6 @@
 #include "order.h"
 #include "predicate.h"
 #include "set.h"
-#include "satfuncopencoder.h"
 
 //TODO: Should handle sharing of AST Nodes without recoding them a second time
 
@@ -44,74 +43,74 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
        switch (GETBOOLEANTYPE(constraint)) {
        case ORDERCONST:
-               return encodeOrderSATEncoder(this, (BooleanOrder *) constraint);
+               return encodeOrderSATEncoder((BooleanOrder *) constraint);
        case BOOLEANVAR:
-               return encodeVarSATEncoder(this, (BooleanVar *) constraint);
+               return encodeVarSATEncoder((BooleanVar *) constraint);
        case LOGICOP:
-               return encodeLogicSATEncoder(this, (BooleanLogic *) constraint);
+               return encodeLogicSATEncoder((BooleanLogic *) constraint);
        case PREDICATEOP:
-               return encodePredicateSATEncoder(this, (BooleanPredicate *) constraint);
+               return encodePredicateSATEncoder((BooleanPredicate *) constraint);
        default:
                model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
                exit(-1);
        }
 }
 
-void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
+void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
        for (uint i = 0; i < num; i++)
-               carray[i] = getNewVarSATEncoder(encoder);
+               carray[i] = getNewVarSATEncoder();
 }
 
-Edge getNewVarSATEncoder(SATEncoder *This) {
-       return constraintNewVar(This->getCNF());
+Edge SATEncoder::getNewVarSATEncoder() {
+       return constraintNewVar(cnf);
 }
 
-Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
+Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
        if (edgeIsNull(constraint->var)) {
-               constraint->var = getNewVarSATEncoder(This);
+               constraint->var = getNewVarSATEncoder();
        }
        return constraint->var;
 }
 
-Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
+Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
        Edge array[constraint->inputs.getSize()];
        for (uint i = 0; i < constraint->inputs.getSize(); i++)
-               array[i] = This->encodeConstraintSATEncoder(constraint->inputs.get(i));
+               array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
 
        switch (constraint->op) {
        case L_AND:
-               return constraintAND(This->getCNF(), constraint->inputs.getSize(), array);
+               return constraintAND(cnf, constraint->inputs.getSize(), array);
        case L_OR:
-               return constraintOR(This->getCNF(), constraint->inputs.getSize(), array);
+               return constraintOR(cnf, constraint->inputs.getSize(), array);
        case L_NOT:
                return constraintNegate(array[0]);
        case L_XOR:
-               return constraintXOR(This->getCNF(), array[0], array[1]);
+               return constraintXOR(cnf, array[0], array[1]);
        case L_IMPLIES:
-               return constraintIMPLIES(This->getCNF(), array[0], array[1]);
+               return constraintIMPLIES(cnf, array[0], array[1]);
        default:
                model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
                exit(-1);
        }
 }
 
-Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
        switch (GETPREDICATETYPE(constraint->predicate) ) {
        case TABLEPRED:
-               return encodeTablePredicateSATEncoder(This, constraint);
+               return encodeTablePredicateSATEncoder(constraint);
        case OPERATORPRED:
-               return encodeOperatorPredicateSATEncoder(This, constraint);
+               return encodeOperatorPredicateSATEncoder(constraint);
        default:
                ASSERT(0);
        }
        return E_BOGUS;
 }
 
-Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
        switch (constraint->encoding.type) {
        case ENUMERATEIMPLICATIONS:
        case ENUMERATEIMPLICATIONSNEGATE:
-               return encodeEnumTablePredicateSATEncoder(This, constraint);
+               return encodeEnumTablePredicateSATEncoder(constraint);
        case CIRCUIT:
                ASSERT(0);
                break;
@@ -121,14 +120,14 @@ Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constrai
        return E_BOGUS;
 }
 
-void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
-       switch ( GETELEMENTTYPE(This) ) {
+void SATEncoder::encodeElementSATEncoder(Element *element) {
+       switch ( GETELEMENTTYPE(element) ) {
        case ELEMFUNCRETURN:
-               generateElementEncoding(encoder, This);
-               encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
+               generateElementEncoding(element);
+               encodeElementFunctionSATEncoder((ElementFunction *) element);
                break;
        case ELEMSET:
-               generateElementEncoding(encoder, This);
+               generateElementEncoding(element);
                return;
        case ELEMCONST:
                return;
@@ -137,23 +136,23 @@ void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
        }
 }
 
-void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
-       switch (GETFUNCTIONTYPE(This->function)) {
+void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
+       switch (GETFUNCTIONTYPE(function->function)) {
        case TABLEFUNC:
-               encodeTableElementFunctionSATEncoder(encoder, This);
+               encodeTableElementFunctionSATEncoder(function);
                break;
        case OPERATORFUNC:
-               encodeOperatorElementFunctionSATEncoder(encoder, This);
+               encodeOperatorElementFunctionSATEncoder(function);
                break;
        default:
                ASSERT(0);
        }
 }
 
-void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
-       switch (getElementFunctionEncoding(This)->type) {
+void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
+       switch (getElementFunctionEncoding(function)->type) {
        case ENUMERATEIMPLICATIONS:
-               encodeEnumTableElemFunctionSATEncoder(encoder, This);
+               encodeEnumTableElemFunctionSATEncoder(function);
                break;
        case CIRCUIT:
                ASSERT(0);
index f88e993..d750c9e 100644 (file)
@@ -5,10 +5,6 @@
 #include "structs.h"
 #include "inc_solver.h"
 #include "constraint.h"
-#include "satelemencoder.h"
-#include "satorderencoder.h"
-#include "satfunctableencoder.h"
-
 
 class SATEncoder {
  public:
@@ -18,24 +14,51 @@ class SATEncoder {
        void encodeAllSATEncoder(CSolver *csolver);
        Edge encodeConstraintSATEncoder(Boolean *constraint);
        CNF * getCNF() { return cnf;}
-       CSolver * getSolver() { return solver; }
        long long getSolveTime() { return cnf->solveTime; }
        long long getEncodeTime() { return cnf->encodeTime; }
        
        MEMALLOC;
  private:
+       Edge getNewVarSATEncoder();
+       void getArrayNewVarsSATEncoder(uint num, Edge *carray);
+       Edge encodeVarSATEncoder(BooleanVar *constraint);
+       Edge encodeLogicSATEncoder(BooleanLogic *constraint);
+       Edge encodePredicateSATEncoder(BooleanPredicate *constraint);
+       Edge encodeTablePredicateSATEncoder(BooleanPredicate *constraint);
+       void encodeElementSATEncoder(Element *element);
+       void encodeElementFunctionSATEncoder(ElementFunction *function);
+       void encodeTableElementFunctionSATEncoder(ElementFunction *This);
+       Edge getElementValueOneHotConstraint(Element *elem, uint64_t value);
+       Edge getElementValueUnaryConstraint(Element *elem, uint64_t value);
+       Edge getElementValueBinaryIndexConstraint(Element *element, uint64_t value);
+       Edge getElementValueBinaryValueConstraint(Element *element, uint64_t value);
+       Edge getElementValueConstraint(Element *element, uint64_t value);
+       void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
+       void generateOneHotEncodingVars(ElementEncoding *encoding);
+       void generateUnaryEncodingVars(ElementEncoding *encoding);
+       void generateBinaryIndexEncodingVars(ElementEncoding *encoding);
+       void generateBinaryValueEncodingVars(ElementEncoding *encoding);
+       void generateElementEncoding(Element *element);
+       Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+       Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+       void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
+       Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
+       Edge encodeOrderSATEncoder(BooleanOrder *constraint);
+       Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
+       Edge getPairConstraint(Order *order, OrderPair *pair);
+       Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
+       Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
+       void createAllTotalOrderConstraintsSATEncoder(Order *order);
+       Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
+       Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK);
+       Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
+       Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
+       void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
+       void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
+       
        CNF *cnf;
        CSolver *solver;
 };
 
-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);
+Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
 #endif
index 597f66b..d416a15 100644 (file)
@@ -9,21 +9,20 @@
 #include "set.h"
 #include "element.h"
 #include "common.h"
-#include "satfuncopencoder.h"
 
-Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
        switch (constraint->encoding.type) {
        case ENUMERATEIMPLICATIONS:
-               return encodeEnumOperatorPredicateSATEncoder(This, constraint);
+               return encodeEnumOperatorPredicateSATEncoder(constraint);
        case CIRCUIT:
-               return encodeCircuitOperatorPredicateEncoder(This, constraint);
+               return encodeCircuitOperatorPredicateEncoder(constraint);
        default:
                ASSERT(0);
        }
        exit(-1);
 }
 
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
        PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
        uint numDomains = predicate->domains.getSize();
 
@@ -33,7 +32,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c
        /* Call base encoders for children */
        for (uint i = 0; i < numDomains; i++) {
                Element *elem = constraint->inputs.get(i);
-               encodeElementSATEncoder(This, elem);
+               encodeElementSATEncoder(elem);
        }
        VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
 
@@ -54,9 +53,9 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c
                        //Include this in the set of terms
                        for (uint i = 0; i < numDomains; i++) {
                                Element *elem = constraint->inputs.get(i);
-                               carray[i] = getElementValueConstraint(This, elem, vals[i]);
+                               carray[i] = getElementValueConstraint(elem, vals[i]);
                        }
-                       Edge term = constraintAND(This->getCNF(), numDomains, carray);
+                       Edge term = constraintAND(cnf, numDomains, carray);
                        pushVectorEdge(clauses, term);
                }
 
@@ -79,13 +78,13 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c
                deleteVectorEdge(clauses);
                return E_False;
        }
-       Edge cor = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        deleteVectorEdge(clauses);
        return generateNegation ? constraintNegate(cor) : cor;
 }
 
 
-void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *func) {
+void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
 #ifdef TRACE_DEBUG
        model_print("Operator Function ...\n");
 #endif
@@ -95,7 +94,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
        /* Call base encoders for children */
        for (uint i = 0; i < numDomains; i++) {
                Element *elem = func->inputs.get(i);
-               encodeElementSATEncoder(This, elem);
+               encodeElementSATEncoder(elem);
        }
 
        VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
@@ -126,10 +125,10 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
                        //Include this in the set of terms
                        for (uint i = 0; i < numDomains; i++) {
                                Element *elem = func->inputs.get(i);
-                               carray[i] = getElementValueConstraint(This, elem, vals[i]);
+                               carray[i] = getElementValueConstraint(elem, vals[i]);
                        }
                        if (isInRange) {
-                               carray[numDomains] = getElementValueConstraint(This, func, result);
+                               carray[numDomains] = getElementValueConstraint(func, result);
                        }
 
                        Edge clause;
@@ -137,26 +136,26 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
                        case IGNORE:
                        case NOOVERFLOW:
                        case WRAPAROUND: {
-                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
+                               clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                                break;
                        }
                        case FLAGFORCESOVERFLOW: {
-                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint)));
+                               clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                break;
                        }
                        case OVERFLOWSETSFLAG: {
                                if (isInRange) {
-                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
+                                       clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                                } else {
-                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint);
+                                       clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
                                }
                                break;
                        }
                        case FLAGIFFOVERFLOW: {
                                if (isInRange) {
-                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint)));
+                                       clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                } else {
-                                       clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint);
+                                       clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
                                }
                                break;
                        }
@@ -190,28 +189,28 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *
                deleteVectorEdge(clauses);
                return;
        }
-       Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       addConstraintCNF(This->getCNF(), cor);
+       Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       addConstraintCNF(cnf, cor);
        deleteVectorEdge(clauses);
 }
 
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint) {
        PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
        Element *elem0 = constraint->inputs.get(0);
-       encodeElementSATEncoder(This, elem0);
+       encodeElementSATEncoder(elem0);
        Element *elem1 = constraint->inputs.get(1);
-       encodeElementSATEncoder(This, elem1);
+       encodeElementSATEncoder(elem1);
        ElementEncoding *ee0 = getElementEncoding(elem0);
        ElementEncoding *ee1 = getElementEncoding(elem1);
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
        switch (predicate->op) {
        case EQUALS:
-               return generateEquivNVConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables);
+               return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
        case LT:
-               return generateLTConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables);
+               return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
        case GT:
-               return generateLTConstraint(This->getCNF(), numVars, ee1->variables, ee0->variables);
+               return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
        default:
                ASSERT(0);
        }
diff --git a/src/Backend/satfuncopencoder.h b/src/Backend/satfuncopencoder.h
deleted file mode 100644 (file)
index a9d0663..0000000
+++ /dev/null
@@ -1,9 +0,0 @@
-#ifndef SATFUNCOPENCODER_H
-#define SATFUNCOPENCODER_H
-
-Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-void encodeOperatorElementFunctionSATEncoder(SATEncoder *encoder,ElementFunction *This);
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint);
-
-#endif
index b2e04cc..fcb53aa 100644 (file)
@@ -10,7 +10,7 @@
 #include "element.h"
 #include "common.h"
 
-Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
        ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
        UndefinedBehavior undefStatus = ((PredicateTable *)constraint->predicate)->undefinedbehavior;
        ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
@@ -21,7 +21,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat
        uint size = table->entries->getSize();
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
        Edge constraints[size];
-       Edge undefConst = This->encodeConstraintSATEncoder(constraint->undefStatus);
+       Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
        printCNF(undefConst);
        model_print("**\n");
        HSIteratorTableEntry *iterator = table->entries->iterator();
@@ -35,21 +35,21 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat
                Edge carray[inputNum];
                for (uint j = 0; j < inputNum; j++) {
                        Element *el = inputs->get(j);
-                       carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+                       carray[j] = getElementValueConstraint(el, entry->inputs[j]);
                        printCNF(carray[j]);
                        model_print("\n");
                }
                Edge row;
                switch (undefStatus) {
                case IGNOREBEHAVIOR:
-                       row = constraintAND(This->getCNF(), inputNum, carray);
+                       row = constraintAND(cnf, inputNum, carray);
                        break;
                case FLAGFORCEUNDEFINED: {
-                       addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray),  constraintNegate(undefConst)));
+                       addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray),  constraintNegate(undefConst)));
                        if (generateNegation == (entry->output != 0)) {
                                continue;
                        }
-                       row = constraintAND(This->getCNF(), inputNum, carray);
+                       row = constraintAND(cnf, inputNum, carray);
                        break;
                }
                default:
@@ -62,12 +62,12 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat
        }
        delete iterator;
        ASSERT(i != 0);
-       Edge result = generateNegation ? constraintNegate(constraintOR(This->getCNF(), i, constraints))
-                                                               : constraintOR(This->getCNF(), i, constraints);
+       Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints))
+                                                               : constraintOR(cnf, i, constraints);
        printCNF(result);
        return result;
 }
-Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) {
 #ifdef TRACE_DEBUG
        model_print("Enumeration Table Predicate ...\n");
 #endif
@@ -77,13 +77,13 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
        uint inputNum = inputs->getSize();
        //Encode all the inputs first ...
        for (uint i = 0; i < inputNum; i++) {
-               encodeElementSATEncoder(This, inputs->get(i));
+               encodeElementSATEncoder(inputs->get(i));
        }
        PredicateTable *predicate = (PredicateTable *)constraint->predicate;
        switch (predicate->undefinedbehavior) {
        case IGNOREBEHAVIOR:
        case FLAGFORCEUNDEFINED:
-               return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
+               return encodeEnumEntriesTablePredicateSATEncoder(constraint);
        default:
                break;
        }
@@ -101,7 +101,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
                vals[i] = set->getElement(indices[i]);
        }
        bool hasOverflow = false;
-       Edge undefConstraint = This->encodeConstraintSATEncoder(constraint->undefStatus);
+       Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
        printCNF(undefConstraint);
        bool notfinished = true;
        while (notfinished) {
@@ -114,23 +114,23 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
                Edge clause;
                for (uint i = 0; i < numDomains; i++) {
                        Element *elem = constraint->inputs.get(i);
-                       carray[i] = getElementValueConstraint(This, elem, vals[i]);
+                       carray[i] = getElementValueConstraint(elem, vals[i]);
                }
 
                switch (predicate->undefinedbehavior) {
                case UNDEFINEDSETSFLAG:
                        if (isInRange) {
-                               clause = constraintAND(This->getCNF(), numDomains, carray);
+                               clause = constraintAND(cnf, numDomains, carray);
                        } else {
-                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint) );
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
                        }
                        break;
                case FLAGIFFUNDEFINED:
                        if (isInRange) {
-                               clause = constraintAND(This->getCNF(), numDomains, carray);
-                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint)));
+                               clause = constraintAND(cnf, numDomains, carray);
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
                        } else {
-                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint) );
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
                        }
                        break;
 
@@ -164,9 +164,9 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
        }
        Edge result = E_NULL;
        ASSERT(getSizeVectorEdge(clauses) != 0);
-       result = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        if (hasOverflow) {
-               result = constraintOR2(This->getCNF(), result, undefConstraint);
+               result = constraintOR2(cnf, result, undefConstraint);
        }
        if (generateNegation) {
                ASSERT(!hasOverflow);
@@ -176,7 +176,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons
        return result;
 }
 
-void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction *func) {
+void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
        UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
        ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
        Array<Element *> *elements = &func->inputs;
@@ -192,18 +192,18 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction
                Edge carray[inputNum];
                for (uint j = 0; j < inputNum; j++) {
                        Element *el = elements->get(j);
-                       carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+                       carray[j] = getElementValueConstraint(el, entry->inputs[j]);
                }
-               Edge output = getElementValueConstraint(This, (Element *)func, entry->output);
+               Edge output = getElementValueConstraint(func, entry->output);
                Edge row;
                switch (undefStatus ) {
                case IGNOREBEHAVIOR: {
-                       row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), output);
+                       row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output);
                        break;
                }
                case FLAGFORCEUNDEFINED: {
-                       Edge undefConst = This->encodeConstraintSATEncoder(func->overflowstatus);
-                       row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), constraintAND2(This->getCNF(), output, constraintNegate(undefConst)));
+                       Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
+                       row = constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst)));
                        break;
                }
                default:
@@ -213,10 +213,10 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction
                constraints[i++] = row;
        }
        delete iterator;
-       addConstraintCNF(This->getCNF(), constraintAND(This->getCNF(), size, constraints));
+       addConstraintCNF(cnf, constraintAND(cnf, size, constraints));
 }
 
-void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *elemFunc) {
+void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
 #ifdef TRACE_DEBUG
        model_print("Enumeration Table functions ...\n");
 #endif
@@ -225,14 +225,14 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
        Array<Element *> *elements = &elemFunc->inputs;
        for (uint i = 0; i < elements->getSize(); i++) {
                Element *elem = elements->get(i);
-               encodeElementSATEncoder(This, elem);
+               encodeElementSATEncoder(elem);
        }
 
        FunctionTable *function = (FunctionTable *)elemFunc->function;
        switch (function->undefBehavior) {
        case IGNOREBEHAVIOR:
        case FLAGFORCEUNDEFINED:
-               return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
+               return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
        default:
                break;
        }
@@ -250,7 +250,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
                vals[i] = set->getElement(indices[i]);
        }
 
-       Edge undefConstraint = This->encodeConstraintSATEncoder(elemFunc->overflowstatus);
+       Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
        bool notfinished = true;
        while (notfinished) {
                Edge carray[numDomains + 1];
@@ -259,10 +259,10 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
                ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
                for (uint i = 0; i < numDomains; i++) {
                        Element *elem = elemFunc->inputs.get(i);
-                       carray[i] = getElementValueConstraint(This, elem, vals[i]);
+                       carray[i] = getElementValueConstraint(elem, vals[i]);
                }
                if (isInRange) {
-                       carray[numDomains] = getElementValueConstraint(This, (Element *)elemFunc, tableEntry->output);
+                       carray[numDomains] = getElementValueConstraint(elemFunc, tableEntry->output);
                }
 
                Edge clause;
@@ -270,18 +270,18 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
                case UNDEFINEDSETSFLAG: {
                        if (isInRange) {
                                //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
-                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
+                               clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                        } else {
-                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint));
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
                        }
                        break;
                }
                case FLAGIFFUNDEFINED: {
                        if (isInRange) {
-                               clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
-                               addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint) ));
+                               clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint) ));
                        } else {
-                               addConstraintCNF(This->getCNF(),constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), undefConstraint));
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
                        }
                        break;
                }
@@ -316,7 +316,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el
                deleteVectorEdge(clauses);
                return;
        }
-       Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       addConstraintCNF(This->getCNF(), cor);
+       Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       addConstraintCNF(cnf, cor);
        deleteVectorEdge(clauses);
 }
diff --git a/src/Backend/satfunctableencoder.h b/src/Backend/satfunctableencoder.h
deleted file mode 100644 (file)
index ad11a1c..0000000
+++ /dev/null
@@ -1,9 +0,0 @@
-#ifndef SATFUNCTABLEENCODER_H
-#define SATFUNCTABLEENCODER_H
-
-Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-void encodeEnumTableElemFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
-void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *encoder, ElementFunction *This);
-
-#endif
index fc8beb2..20d163b 100644 (file)
 #include "predicate.h"
 #include "orderelement.h"
 
-Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
        switch ( constraint->order->type) {
        case PARTIAL:
-               return encodePartialOrderSATEncoder(This, constraint);
+               return encodePartialOrderSATEncoder(constraint);
        case TOTAL:
-               return encodeTotalOrderSATEncoder(This, constraint);
+               return encodeTotalOrderSATEncoder(constraint);
        default:
                ASSERT(0);
        }
@@ -50,7 +50,7 @@ Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _seco
        return E_NULL;
 }
 
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
        Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
        if (!edgeIsNull(gvalue))
                return gvalue;
@@ -66,7 +66,7 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
        }
        Edge constraint;
        if (!(table->contains(pair))) {
-               constraint = getNewVarSATEncoder(This);
+               constraint = getNewVarSATEncoder();
                OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
                table->put(paircopy, paircopy);
        } else
@@ -75,24 +75,24 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
        return negate ? constraintNegate(constraint) : constraint;
 }
 
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
+Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
        ASSERT(boolOrder->order->type == TOTAL);
        if (boolOrder->order->orderPairTable == NULL) {
                boolOrder->order->initializeOrderHashTable();
-               bool doOptOrderStructure = GETVARTUNABLE(This->getSolver()->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+               bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
-                       reachMustAnalysis(This->getSolver(), boolOrder->order->graph, true);
+                       reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
-               createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+               createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
        }
        OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
-       Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
+       Edge constraint = getPairConstraint(boolOrder->order, &pair);
        return constraint;
 }
 
 
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
+void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
 #ifdef TRACE_DEBUG
        model_print("in total order ...\n");
 #endif
@@ -104,14 +104,14 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
                for (uint j = i + 1; j < size; j++) {
                        uint64_t valueJ = mems->get(j);
                        OrderPair pairIJ(valueI, valueJ, E_NULL);
-                       Edge constIJ = getPairConstraint(This, order, &pairIJ);
+                       Edge constIJ = getPairConstraint(order, &pairIJ);
                        for (uint k = j + 1; k < size; k++) {
                                uint64_t valueK = mems->get(k);
                                OrderPair pairJK(valueJ, valueK, E_NULL);
                                OrderPair pairIK(valueI, valueK, E_NULL);
-                               Edge constIK = getPairConstraint(This, order, &pairIK);
-                               Edge constJK = getPairConstraint(This, order, &pairJK);
-                               addConstraintCNF(This->getCNF(), generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
+                               Edge constIK = getPairConstraint(order, &pairIK);
+                               Edge constJK = getPairConstraint(order, &pairJK);
+                               addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
                        }
                }
        }
@@ -135,15 +135,15 @@ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
        return negate ? constraintNegate(constraint) : constraint;
 }
 
-Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
+Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
        Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
-       Edge loop1 = constraintOR(This->getCNF(), 3, carray);
+       Edge loop1 = constraintOR(cnf, 3, carray);
        Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
-       Edge loop2 = constraintOR(This->getCNF(), 3, carray2 );
-       return constraintAND2(This->getCNF(), loop1, loop2);
+       Edge loop2 = constraintOR(cnf, 3, carray2 );
+       return constraintAND2(cnf, loop1, loop2);
 }
 
-Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
        ASSERT(constraint->order->type == PARTIAL);
        return E_BOGUS;
 }
diff --git a/src/Backend/satorderencoder.h b/src/Backend/satorderencoder.h
deleted file mode 100644 (file)
index ca6b4d4..0000000
+++ /dev/null
@@ -1,12 +0,0 @@
-#ifndef SATORDERENCODER_H
-#define SATORDERENCODER_H
-
-Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order);
-Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
-Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ, Edge constJK, Edge constIK);
-#endif