From 852184b398d1e4c1e70b3d997bd18ba2b96490a5 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sun, 27 Aug 2017 17:55:25 -0700 Subject: [PATCH] More OO conversion --- src/Backend/satelemencoder.cc | 56 ++++++++++----------- src/Backend/satelemencoder.h | 15 ------ src/Backend/satencoder.cc | 67 ++++++++++++------------- src/Backend/satencoder.h | 53 ++++++++++++++------ src/Backend/satfuncopencoder.cc | 53 ++++++++++---------- src/Backend/satfuncopencoder.h | 9 ---- src/Backend/satfunctableencoder.cc | 80 +++++++++++++++--------------- src/Backend/satfunctableencoder.h | 9 ---- src/Backend/satorderencoder.cc | 40 +++++++-------- src/Backend/satorderencoder.h | 12 ----- 10 files changed, 185 insertions(+), 209 deletions(-) delete mode 100644 src/Backend/satelemencoder.h delete mode 100644 src/Backend/satfuncopencoder.h delete mode 100644 src/Backend/satfunctableencoder.h delete mode 100644 src/Backend/satorderencoder.h diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index 504f92c..2cb423d 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -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 index d75f2f8..0000000 --- a/src/Backend/satelemencoder.h +++ /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 diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 977147f..838170f 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -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); diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index f88e993..d750c9e 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -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 diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index 597f66b..d416a15 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -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 index a9d0663..0000000 --- a/src/Backend/satfuncopencoder.h +++ /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 diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index b2e04cc..fcb53aa 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -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 *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 *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 index ad11a1c..0000000 --- a/src/Backend/satfunctableencoder.h +++ /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 diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index fc8beb2..20d163b 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -13,12 +13,12 @@ #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 index ca6b4d4..0000000 --- a/src/Backend/satorderencoder.h +++ /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 -- 2.34.1