X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.cc;h=618b8c17c22114177393754313dda6a3c1d8aa5c;hp=91e323d4d4842996076de9054f4a0c39c788fe0b;hb=cbd921ee35b6a29934fd7cecccde7f160228af17;hpb=a0daa81a61273f51fdaad8a6d5aaf078387851bc diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 91e323d..618b8c1 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -11,107 +11,140 @@ #include "order.h" #include "predicate.h" #include "set.h" -#include "satfuncopencoder.h" +#include "tunable.h" -//TODO: Should handle sharing of AST Nodes without recoding them a second time +SATEncoder::SATEncoder(CSolver *_solver) : + cnf(createCNF()), + solver(_solver), + vector(allocDefVectorEdge()) { +} + +SATEncoder::~SATEncoder() { + deleteCNF(cnf); + deleteVectorEdge(vector); +} -SATEncoder *allocSATEncoder(CSolver *solver) { - SATEncoder *This = (SATEncoder *)ourmalloc(sizeof (SATEncoder)); - This->solver = solver; - This->varcount = 1; - This->cnf = createCNF(); - return This; +void SATEncoder::resetSATEncoder() { + resetCNF(cnf); + booledgeMap.reset(); } -void deleteSATEncoder(SATEncoder *This) { - deleteCNF(This->cnf); - ourfree(This); +int SATEncoder::solve(long timeout) { + cnf->solver->timeout = timeout; + return solveCNF(cnf); } -void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) { - HSIteratorBoolean *iterator=csolver->getConstraints(); - while(iterator->hasNext()) { - Boolean *constraint = iterator->next(); - model_print("Encoding All ...\n\n"); - Edge c = encodeConstraintSATEncoder(This, constraint); - model_print("Returned Constraint in EncodingAll:\n"); - ASSERT( ! equalsEdge(c, E_BOGUS)); - addConstraintCNF(This->cnf, c); +void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { + if(csolver->isUnSAT()){ + return; + } + SetIteratorBooleanEdge *iterator = csolver->getConstraints(); + while (iterator->hasNext()) { + BooleanEdge constraint = iterator->next(); + Edge c = encodeConstraintSATEncoder(constraint); + addConstraintCNF(cnf, c); } delete iterator; } -Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { - switch (GETBOOLEANTYPE(constraint)) { +Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) { + Edge result; + Boolean *constraint = c.getBoolean(); + + if (booledgeMap.contains(constraint)) { + Edge e = {(Node *) booledgeMap.get(constraint)}; + return c.isNegated() ? constraintNegate(e) : e; + } + + switch (constraint->type) { case ORDERCONST: - return encodeOrderSATEncoder(This, (BooleanOrder *) constraint); + result = encodeOrderSATEncoder((BooleanOrder *) constraint); + break; case BOOLEANVAR: - return encodeVarSATEncoder(This, (BooleanVar *) constraint); + result = encodeVarSATEncoder((BooleanVar *) constraint); + break; case LOGICOP: - return encodeLogicSATEncoder(This, (BooleanLogic *) constraint); + result = encodeLogicSATEncoder((BooleanLogic *) constraint); + break; case PREDICATEOP: - return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint); + result = encodePredicateSATEncoder((BooleanPredicate *) constraint); + break; + case BOOLCONST: + result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False; + break; default: - model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint)); + model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type); exit(-1); } + Polarity p = constraint->polarity; + uint pSize = constraint->parents.getSize(); + + if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) { + Edge e = getNewVarSATEncoder(); + generateProxy(cnf, result, e, p); + booledgeMap.put(constraint, e.node_ptr); + result = e; + } + + return c.isNegated() ? constraintNegate(result) : result; } -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->cnf); +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] = encodeConstraintSATEncoder(This, constraint->inputs.get(i)); + array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i)); switch (constraint->op) { - case L_AND: - return constraintAND(This->cnf, constraint->inputs.getSize(), array); - case L_OR: - return constraintOR(This->cnf, constraint->inputs.getSize(), array); - case L_NOT: + case SATC_AND: + return constraintAND(cnf, constraint->inputs.getSize(), array); + case SATC_NOT: return constraintNegate(array[0]); - case L_XOR: - return constraintXOR(This->cnf, array[0], array[1]); - case L_IMPLIES: - return constraintIMPLIES(This->cnf, array[0], array[1]); + case SATC_IFF: + ASSERT(constraint->inputs.getSize() == 2); + return constraintIFF(cnf, array[0], array[1]); + case SATC_OR: + case SATC_XOR: + case SATC_IMPLIES: + //Don't handle, translate these away... default: model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op); exit(-1); } } -Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) { - switch (GETPREDICATETYPE(constraint->predicate) ) { +Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) { + switch (constraint->predicate->type) { 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 +154,19 @@ Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constrai return E_BOGUS; } -void encodeElementSATEncoder(SATEncoder *encoder, Element *This) { - switch ( GETELEMENTTYPE(This) ) { +void SATEncoder::encodeElementSATEncoder(Element *element) { + /* Check to see if we have already encoded this element. */ + if (element->getElementEncoding()->variables != NULL) + return; + + /* Need to encode. */ + switch ( element->type) { 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 +175,23 @@ void encodeElementSATEncoder(SATEncoder *encoder, Element *This) { } } -void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) { - switch (GETFUNCTIONTYPE(This->function)) { +void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) { + switch (function->getFunction()->type) { 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 (function->getElementFunctionEncoding()->type) { case ENUMERATEIMPLICATIONS: - encodeEnumTableElemFunctionSATEncoder(encoder, This); + encodeEnumTableElemFunctionSATEncoder(function); break; case CIRCUIT: ASSERT(0);