From 8762ed97c242788e724b509b705a308868eb4974 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sun, 27 Aug 2017 17:27:52 -0700 Subject: [PATCH] edits --- src/ASTTransform/integerencoding.cc | 20 ++++++------- src/ASTTransform/integerencoding.h | 5 ++-- src/Backend/constraint.cc | 8 +++++- src/Backend/constraint.h | 2 ++ src/Backend/satelemencoder.cc | 12 ++++---- src/Backend/satencoder.cc | 15 ++++++---- src/Backend/satencoder.h | 32 ++++++++++++--------- src/Backend/satfuncopencoder.cc | 26 ++++++++--------- src/Backend/satfunctableencoder.cc | 44 ++++++++++++++--------------- src/Backend/satorderencoder.cc | 12 ++++---- src/Backend/sattranslator.cc | 14 ++++----- src/Tuner/tunable.cc | 6 ++-- src/Tuner/tunable.h | 12 +++++++- src/classlist.h | 1 + src/common.h | 7 +++++ src/csolver.cc | 26 +++++++++++------ src/csolver.h | 10 ++++++- 17 files changed, 151 insertions(+), 101 deletions(-) diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index 0a415b9..3d7ab5c 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -9,29 +9,29 @@ #include "set.h" -void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) { +void orderIntegerEncodingSATEncoder(CSolver *solver, BooleanOrder *boolOrder) { Order *order = boolOrder->order; if (order->elementTable == NULL) { order->initializeOrderElementsHashTable(); } //getting two elements and using LT predicate ... - ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->first); - ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->second); + ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(solver, order, boolOrder->first); + ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(solver, order, boolOrder->second); Set *sarray[] = {elem1->set, elem2->set}; - Predicate *predicate = This->solver->createPredicateOperator(LT, sarray, 2); + Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2); Element *parray[] = {elem1, elem2}; - Boolean *boolean = This->solver->applyPredicate(predicate, parray, 2); - This->solver->addConstraint(boolean); - This->solver->replaceBooleanWithBoolean(boolOrder, boolean); + Boolean *boolean = solver->applyPredicate(predicate, parray, 2); + solver->addConstraint(boolean); + solver->replaceBooleanWithBoolean(boolOrder, boolean); } -Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) { +Element *getOrderIntegerElement(CSolver * solver, Order *order, uint64_t item) { HashSetOrderElement *eset = order->elementTable; OrderElement oelement(item, NULL); if ( !eset->contains(&oelement)) { - Set *set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize()); - Element *elem = This->solver->getElementVar(set); + Set *set = solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize()); + Element *elem = solver->getElementVar(set); eset->add(new OrderElement(item, elem)); return elem; } else diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h index 15fbdd7..2288dab 100644 --- a/src/ASTTransform/integerencoding.h +++ b/src/ASTTransform/integerencoding.h @@ -16,9 +16,8 @@ #include "classlist.h" #include "structs.h" -Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item); -void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder); - +Element *getOrderIntegerElement(CSolver *solver, Order *order, uint64_t item); +void orderIntegerEncodingSATEncoder(CSolver *solver, BooleanOrder *boolOrder); #endif/* INTEGERENCODING_H */ diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index 1c36cd1..201d7db 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -328,10 +328,16 @@ Edge constraintNewVar(CNF *cnf) { } int solveCNF(CNF *cnf) { + long long startTime=getTimeNano(); countPass(cnf); convertPass(cnf, false); finishedClauses(cnf->solver); - return solve(cnf->solver); + long long startSolve=getTimeNano(); + int result = solve(cnf->solver); + long long finishTime=getTimeNano(); + cnf->encodeTime=startSolve-startTime; + cnf->solveTime=finishTime-startSolve; + return result; } bool getValueCNF(CNF *cnf, Edge var) { diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h index 02fe3da..2f61d72 100644 --- a/src/Backend/constraint.h +++ b/src/Backend/constraint.h @@ -63,6 +63,8 @@ struct CNF { IncrementalSolver *solver; VectorEdge constraints; VectorEdge args; + long long solveTime; + long long encodeTime; }; typedef struct CNF CNF; diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index 8513d92..504f92c 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -32,7 +32,7 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *elem, uint6 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->cnf, elemEnc->numVars, elemEnc->variables, i); + return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, i); } } return E_False; @@ -63,7 +63,7 @@ Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t va else if ((i + 1) == elemEnc->encArraySize) return elemEnc->variables[i - 1]; else - return constraintAND2(This->cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i])); + return constraintAND2(This->getCNF(), elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i])); } } return E_False; @@ -83,7 +83,7 @@ Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, ui } uint64_t valueminusoffset = value - elemEnc->offset; - return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset); + return generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, valueminusoffset); } void allocElementConstraintVariables(ElementEncoding *This, uint numVars) { @@ -108,10 +108,10 @@ void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) { getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables); for (uint i = 0; i < encoding->numVars; i++) { for (uint j = i + 1; j < encoding->numVars; j++) { - addConstraintCNF(This->cnf, constraintNegate(constraintAND2(This->cnf, encoding->variables[i], encoding->variables[j]))); + addConstraintCNF(This->getCNF(), constraintNegate(constraintAND2(This->getCNF(), encoding->variables[i], encoding->variables[j]))); } } - addConstraintCNF(This->cnf, constraintOR(This->cnf, encoding->numVars, encoding->variables)); + addConstraintCNF(This->getCNF(), constraintOR(This->getCNF(), encoding->numVars, encoding->variables)); } void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) { @@ -119,7 +119,7 @@ void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) { getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables); //Add unary constraint for (uint i = 1; i < encoding->numVars; i++) { - addConstraintCNF(This->cnf, constraintOR2(This->cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i]))); + addConstraintCNF(This->getCNF(), constraintOR2(This->getCNF(), encoding->variables[i - 1], constraintNegate(encoding->variables[i]))); } } diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index a7513d6..977147f 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -16,7 +16,6 @@ //TODO: Should handle sharing of AST Nodes without recoding them a second time SATEncoder::SATEncoder(CSolver * _solver) : - varcount(1), cnf(createCNF()), solver(_solver) { } @@ -25,6 +24,10 @@ SATEncoder::~SATEncoder() { deleteCNF(cnf); } +int SATEncoder::solve() { + return solveCNF(cnf); +} + void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { HSIteratorBoolean *iterator = csolver->getConstraints(); while (iterator->hasNext()) { @@ -60,7 +63,7 @@ void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) { } Edge getNewVarSATEncoder(SATEncoder *This) { - return constraintNewVar(This->cnf); + return constraintNewVar(This->getCNF()); } Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) { @@ -77,15 +80,15 @@ Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) { switch (constraint->op) { case L_AND: - return constraintAND(This->cnf, constraint->inputs.getSize(), array); + return constraintAND(This->getCNF(), constraint->inputs.getSize(), array); case L_OR: - return constraintOR(This->cnf, constraint->inputs.getSize(), array); + return constraintOR(This->getCNF(), constraint->inputs.getSize(), array); case L_NOT: return constraintNegate(array[0]); case L_XOR: - return constraintXOR(This->cnf, array[0], array[1]); + return constraintXOR(This->getCNF(), array[0], array[1]); case L_IMPLIES: - return constraintIMPLIES(This->cnf, array[0], array[1]); + return constraintIMPLIES(This->getCNF(), array[0], array[1]); default: model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op); exit(-1); diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index f74965b..f88e993 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -12,26 +12,30 @@ class SATEncoder { public: - uint varcount; - CNF *cnf; - CSolver *solver; - + int solve(); SATEncoder(CSolver *solver); ~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: + CNF *cnf; + CSolver *solver; }; +Edge getNewVarSATEncoder(SATEncoder *This); +void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray); - 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 encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint); +Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint); +Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint); +Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint); +void encodeElementSATEncoder(SATEncoder *encoder, Element *This); +void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This); +void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This); #endif diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index 695493b..597f66b 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -56,7 +56,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c Element *elem = constraint->inputs.get(i); carray[i] = getElementValueConstraint(This, elem, vals[i]); } - Edge term = constraintAND(This->cnf, numDomains, carray); + Edge term = constraintAND(This->getCNF(), numDomains, carray); pushVectorEdge(clauses, term); } @@ -79,7 +79,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c deleteVectorEdge(clauses); return E_False; } - Edge cor = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + Edge cor = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); deleteVectorEdge(clauses); return generateNegation ? constraintNegate(cor) : cor; } @@ -137,26 +137,26 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * case IGNORE: case NOOVERFLOW: case WRAPAROUND: { - clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]); break; } case FLAGFORCESOVERFLOW: { - clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint))); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint))); break; } case OVERFLOWSETSFLAG: { if (isInRange) { - clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]); } else { - clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint); } break; } case FLAGIFFOVERFLOW: { if (isInRange) { - clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint))); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint))); } else { - clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint); } break; } @@ -190,8 +190,8 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * deleteVectorEdge(clauses); return; } - Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); - addConstraintCNF(This->cnf, cor); + Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + addConstraintCNF(This->getCNF(), cor); deleteVectorEdge(clauses); } @@ -207,11 +207,11 @@ Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *c uint numVars = ee0->numVars; switch (predicate->op) { case EQUALS: - return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables); + return generateEquivNVConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables); case LT: - return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables); + return generateLTConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables); case GT: - return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables); + return generateLTConstraint(This->getCNF(), numVars, ee1->variables, ee0->variables); default: ASSERT(0); } diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index 1c5e58c..b2e04cc 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -42,14 +42,14 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat Edge row; switch (undefStatus) { case IGNOREBEHAVIOR: - row = constraintAND(This->cnf, inputNum, carray); + row = constraintAND(This->getCNF(), inputNum, carray); break; case FLAGFORCEUNDEFINED: { - addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintNegate(undefConst))); + addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), constraintNegate(undefConst))); if (generateNegation == (entry->output != 0)) { continue; } - row = constraintAND(This->cnf, inputNum, carray); + row = constraintAND(This->getCNF(), inputNum, carray); break; } default: @@ -62,8 +62,8 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat } delete iterator; ASSERT(i != 0); - Edge result = generateNegation ? constraintNegate(constraintOR(This->cnf, i, constraints)) - : constraintOR(This->cnf, i, constraints); + Edge result = generateNegation ? constraintNegate(constraintOR(This->getCNF(), i, constraints)) + : constraintOR(This->getCNF(), i, constraints); printCNF(result); return result; } @@ -120,17 +120,17 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons switch (predicate->undefinedbehavior) { case UNDEFINEDSETSFLAG: if (isInRange) { - clause = constraintAND(This->cnf, numDomains, carray); + clause = constraintAND(This->getCNF(), numDomains, carray); } else { - addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) ); + addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint) ); } break; case FLAGIFFUNDEFINED: if (isInRange) { - clause = constraintAND(This->cnf, numDomains, carray); - addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint))); + clause = constraintAND(This->getCNF(), numDomains, carray); + addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint))); } else { - addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) ); + addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), 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->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + result = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); if (hasOverflow) { - result = constraintOR2(This->cnf, result, undefConstraint); + result = constraintOR2(This->getCNF(), result, undefConstraint); } if (generateNegation) { ASSERT(!hasOverflow); @@ -198,12 +198,12 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction Edge row; switch (undefStatus ) { case IGNOREBEHAVIOR: { - row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output); + row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), output); break; } case FLAGFORCEUNDEFINED: { Edge undefConst = This->encodeConstraintSATEncoder(func->overflowstatus); - row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst))); + row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), constraintAND2(This->getCNF(), output, constraintNegate(undefConst))); break; } default: @@ -213,7 +213,7 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction constraints[i++] = row; } delete iterator; - addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints)); + addConstraintCNF(This->getCNF(), constraintAND(This->getCNF(), size, constraints)); } void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *elemFunc) { @@ -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->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]); } else { - addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint)); + addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint)); } break; } case FLAGIFFUNDEFINED: { if (isInRange) { - clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); - addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint) )); + clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]); + addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint) )); } else { - addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint)); + addConstraintCNF(This->getCNF(),constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), undefConstraint)); } break; } @@ -316,7 +316,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el deleteVectorEdge(clauses); return; } - Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); - addConstraintCNF(This->cnf, cor); + Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + addConstraintCNF(This->getCNF(), cor); deleteVectorEdge(clauses); } diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 5744736..fc8beb2 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -79,10 +79,10 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) { ASSERT(boolOrder->order->type == TOTAL); if (boolOrder->order->orderPairTable == NULL) { boolOrder->order->initializeOrderHashTable(); - bool doOptOrderStructure = GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); + bool doOptOrderStructure = GETVARTUNABLE(This->getSolver()->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); if (doOptOrderStructure) { boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); - reachMustAnalysis(This->solver, boolOrder->order->graph, true); + reachMustAnalysis(This->getSolver(), boolOrder->order->graph, true); } createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order); } @@ -111,7 +111,7 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) { OrderPair pairIK(valueI, valueK, E_NULL); Edge constIK = getPairConstraint(This, order, &pairIK); Edge constJK = getPairConstraint(This, order, &pairJK); - addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); + addConstraintCNF(This->getCNF(), generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); } } } @@ -137,10 +137,10 @@ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) { Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) { Edge carray[] = {constIJ, constJK, constraintNegate(constIK)}; - Edge loop1 = constraintOR(This->cnf, 3, carray); + Edge loop1 = constraintOR(This->getCNF(), 3, carray); Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK}; - Edge loop2 = constraintOR(This->cnf, 3, carray2 ); - return constraintAND2(This->cnf, loop1, loop2); + Edge loop2 = constraintOR(This->getCNF(), 3, carray2 ); + return constraintAND2(This->getCNF(), loop1, loop2); } Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) { diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc index 7b8eae0..1cd0815 100644 --- a/src/Backend/sattranslator.cc +++ b/src/Backend/sattranslator.cc @@ -10,7 +10,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding uint index = 0; for (int i = elemEnc->numVars - 1; i >= 0; i--) { index = index << 1; - if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] ))) + if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))) index |= 1; } if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index)) @@ -22,11 +22,11 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding uint64_t value = 0; for (int i = elemEnc->numVars - 1; i >= 0; i--) { value = value << 1; - if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) + if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) value |= 1; } if (elemEnc->isBinaryValSigned && - This->getSATEncoder()->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) { + This->getSATEncoder()->getCNF()->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) { //Do sign extension of negative number uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1); value += highbits; @@ -38,7 +38,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) { uint index = 0; for (uint i = 0; i < elemEnc->numVars; i++) { - if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] ))) + if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))) index = i; } ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index)); @@ -48,7 +48,7 @@ uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elem uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) { uint i; for (i = 0; i < elemEnc->numVars; i++) { - if (!getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) { + if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) { break; } } @@ -82,7 +82,7 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) { bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) { int index = getEdgeVar( ((BooleanVar *) boolean)->var ); - return getValueSolver(This->getSATEncoder()->cnf->solver, index); + return getValueSolver(This->getSATEncoder()->getCNF()->solver, index); } HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) { @@ -91,6 +91,6 @@ HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, Edge var = getOrderConstraint(order->orderPairTable, &pair); if (edgeIsNull(var)) return UNORDERED; - return getValueCNF(This->getSATEncoder()->cnf, var) ? FIRST : SECOND; + return getValueCNF(This->getSATEncoder()->getCNF(), var) ? FIRST : SECOND; } diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc index 5c13a12..1401b24 100644 --- a/src/Tuner/tunable.cc +++ b/src/Tuner/tunable.cc @@ -1,11 +1,11 @@ #include "tunable.h" -Tuner::Tuner() { +DefaultTuner::DefaultTuner() { } -int Tuner::getTunable(TunableParam param, TunableDesc *descriptor) { +int DefaultTuner::getTunable(TunableParam param, TunableDesc *descriptor) { return descriptor->defaultValue; } -int Tuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) { +int DefaultTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) { return descriptor->defaultValue; } diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h index 6077891..8d696af 100644 --- a/src/Tuner/tunable.h +++ b/src/Tuner/tunable.h @@ -5,12 +5,22 @@ class Tuner { public: - Tuner(); + virtual int getTunable(TunableParam param, TunableDesc *descriptor); + virtual int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor); + virtual ~Tuner(); + MEMALLOC; +}; + +class DefaultTuner : public Tuner { +public: + DefaultTuner(); int getTunable(TunableParam param, TunableDesc *descriptor); int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor); MEMALLOC; }; + + class TunableDesc { public: TunableDesc(int _lowValue, int _highValue, int _defaultValue) : lowValue(_lowValue), highValue(_highValue), defaultValue(_defaultValue) {} diff --git a/src/classlist.h b/src/classlist.h index aac331d..dd97e08 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -50,6 +50,7 @@ class OrderGraph; class OrderNode; class OrderEdge; +class AutoTuner; struct IncrementalSolver; typedef struct IncrementalSolver IncrementalSolver; diff --git a/src/common.h b/src/common.h index 0ebb7ec..3fffb34 100644 --- a/src/common.h +++ b/src/common.h @@ -16,6 +16,7 @@ #include #include "config.h" +#include "time.h" /* extern int model_out; @@ -65,4 +66,10 @@ void assert_hook(void); #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__) void print_trace(void); + +static inline long long getTimeNano() { + struct timespec time; + clock_gettime(CLOCK_REALTIME, & time); + return time.tv_sec * 1000000000 + time.tv_nsec; +} #endif/* __COMMON_H__ */ diff --git a/src/csolver.cc b/src/csolver.cc index 47e22a1..c83f4b9 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -12,9 +12,13 @@ #include "tunable.h" #include "polarityassignment.h" #include "orderdecompose.h" +#include "autotuner.h" -CSolver::CSolver() : unsat(false) { - tuner = new Tuner(); +CSolver::CSolver() : + unsat(false), + tuner(new DefaultTuner()), + elapsedTime(0) +{ satEncoder = new SATEncoder(this); } @@ -198,16 +202,14 @@ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) } int CSolver::startEncoding() { + long long startTime = getTimeNano(); computePolarities(this); orderAnalysis(this); naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); - int result = solveCNF(satEncoder->cnf); - model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize); - for (int i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) { - model_print("%d, ", satEncoder->cnf->solver->solution[i]); - } - model_print("\n"); + int result = satEncoder->solve(); + long long finishTime = getTimeNano(); + elapsedTime = finishTime - startTime; return result; } @@ -237,3 +239,11 @@ HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, ui return getOrderConstraintValueSATTranslator(this, order, first, second); } +long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); } + +long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); } + +void CSolver::autoTune() { + AutoTuner * autotuner=new AutoTuner(); + autotuner->tune(this); +} diff --git a/src/csolver.h b/src/csolver.h index 1f77993..7939ee5 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -108,7 +108,7 @@ public: Vector *getOrders() { return &allOrders;} Tuner *getTuner() { return tuner; } - + HSIteratorBoolean *getConstraints() { return constraints.iterator(); } SATEncoder *getSATEncoder() {return satEncoder;} @@ -117,7 +117,13 @@ public: void replaceBooleanWithFalse(Boolean *bexpr); void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb); CSolver *clone(); + void autoTune(); + void setTuner(Tuner * _tuner) { tuner = _tuner; } + long long getElapsedTime() { return elapsedTime; } + long long getEncodeTime(); + long long getSolveTime(); + MEMALLOC; private: @@ -154,5 +160,7 @@ private: SATEncoder *satEncoder; bool unsat; Tuner *tuner; + + long long elapsedTime; }; #endif -- 2.34.1