X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatfuncopencoder.c;h=b8a814d54d46f43f3c33191cbc6818c70c274c54;hb=5f7ad155a72a38dda20e1ffd4e8bf8c7c1132251;hp=1df9c61de5477ad77c992495845b010e3ffda63c;hpb=ebd02cfd7a813355f24c2e9c89b493ca4985c4f8;p=satune.git diff --git a/src/Backend/satfuncopencoder.c b/src/Backend/satfuncopencoder.c index 1df9c61..b8a814d 100644 --- a/src/Backend/satfuncopencoder.c +++ b/src/Backend/satfuncopencoder.c @@ -11,121 +11,121 @@ #include "common.h" #include "satfuncopencoder.h" -Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { - switch(constraint->encoding.type){ - case ENUMERATEIMPLICATIONS: - return encodeEnumOperatorPredicateSATEncoder(This, constraint); - case CIRCUIT: - return encodeCircuitOperatorPredicateEncoder(This, constraint); - default: - ASSERT(0); +Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) { + switch (constraint->encoding.type) { + case ENUMERATEIMPLICATIONS: + return encodeEnumOperatorPredicateSATEncoder(This, constraint); + case CIRCUIT: + return encodeCircuitOperatorPredicateEncoder(This, constraint); + default: + ASSERT(0); } exit(-1); } -Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { - PredicateOperator* predicate = (PredicateOperator*)constraint->predicate; - uint numDomains=getSizeArraySet(&predicate->domains); +Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) { + PredicateOperator *predicate = (PredicateOperator *)constraint->predicate; + uint numDomains = getSizeArraySet(&predicate->domains); FunctionEncodingType encType = constraint->encoding.type; bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; /* Call base encoders for children */ - for(uint i=0;iinputs, i); encodeElementSATEncoder(This, elem); } - VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses - - uint indices[numDomains]; //setup indices - bzero(indices, sizeof(uint)*numDomains); - - uint64_t vals[numDomains]; //setup value array - for(uint i=0;idomains, i); - vals[i]=getSetElement(set, indices[i]); + VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses + + uint indices[numDomains]; //setup indices + bzero(indices, sizeof(uint) * numDomains); + + uint64_t vals[numDomains];//setup value array + for (uint i = 0; i < numDomains; i++) { + Set *set = getArraySet(&predicate->domains, i); + vals[i] = getSetElement(set, indices[i]); } - - bool notfinished=true; - while(notfinished) { + + bool notfinished = true; + while (notfinished) { Edge carray[numDomains]; if (evalPredicateOperator(predicate, vals) ^ generateNegation) { //Include this in the set of terms - for(uint i=0;iinputs, i); + for (uint i = 0; i < numDomains; i++) { + Element *elem = getArrayElement(&constraint->inputs, i); carray[i] = getElementValueConstraint(This, elem, vals[i]); } - Edge term=constraintAND(This->cnf, numDomains, carray); + Edge term = constraintAND(This->cnf, numDomains, carray); pushVectorEdge(clauses, term); } - - notfinished=false; - for(uint i=0;idomains, i); + + notfinished = false; + for (uint i = 0; i < numDomains; i++) { + uint index = ++indices[i]; + Set *set = getArraySet(&predicate->domains, i); if (index < getSetSize(set)) { - vals[i]=getSetElement(set, index); - notfinished=true; + vals[i] = getSetElement(set, index); + notfinished = true; break; } else { - indices[i]=0; - vals[i]=getSetElement(set, 0); + indices[i] = 0; + vals[i] = getSetElement(set, 0); } } } - if(getSizeVectorEdge(clauses) == 0) { + if (getSizeVectorEdge(clauses) == 0) { deleteVectorEdge(clauses); return E_False; } - Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + Edge cor = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); deleteVectorEdge(clauses); return generateNegation ? constraintNegate(cor) : cor; } -void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) { +void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *func) { #ifdef TRACE_DEBUG model_print("Operator Function ...\n"); #endif - FunctionOperator * function = (FunctionOperator *) func->function; - uint numDomains=getSizeArrayElement(&func->inputs); + FunctionOperator *function = (FunctionOperator *) func->function; + uint numDomains = getSizeArrayElement(&func->inputs); /* Call base encoders for children */ - for(uint i=0;iinputs, i); encodeElementSATEncoder(This, elem); } - VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses - - uint indices[numDomains]; //setup indices - bzero(indices, sizeof(uint)*numDomains); - - uint64_t vals[numDomains]; //setup value array - for(uint i=0;iinputs, i)); - vals[i]=getSetElement(set, indices[i]); + VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses + + uint indices[numDomains]; //setup indices + bzero(indices, sizeof(uint) * numDomains); + + uint64_t vals[numDomains];//setup value array + for (uint i = 0; i < numDomains; i++) { + Set *set = getElementSet(getArrayElement(&func->inputs, i)); + vals[i] = getSetElement(set, indices[i]); } - Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var; - - bool notfinished=true; - while(notfinished) { - Edge carray[numDomains+1]; + Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var; + + bool notfinished = true; + while (notfinished) { + Edge carray[numDomains + 1]; - uint64_t result=applyFunctionOperator(function, numDomains, vals); - bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result); + uint64_t result = applyFunctionOperator(function, numDomains, vals); + bool isInRange = isInRangeFunction((FunctionOperator *)func->function, result); bool needClause = isInRange; if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) { - needClause=true; + needClause = true; } - + if (needClause) { //Include this in the set of terms - for(uint i=0;iinputs, i); + for (uint i = 0; i < numDomains; i++) { + Element *elem = getArrayElement(&func->inputs, i); carray[i] = getElementValueConstraint(This, elem, vals[i]); } if (isInRange) { @@ -133,30 +133,30 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* } Edge clause; - switch(function->overflowbehavior) { + switch (function->overflowbehavior) { case IGNORE: case NOOVERFLOW: case WRAPAROUND: { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); + clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, 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->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint))); break; } case OVERFLOWSETSFLAG: { if (isInRange) { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); + clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); } else { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint); + clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, 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->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint))); } else { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint); + clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint); } break; } @@ -170,35 +170,35 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* #endif pushVectorEdge(clauses, clause); } - - notfinished=false; - for(uint i=0;iinputs, i)); + + notfinished = false; + for (uint i = 0; i < numDomains; i++) { + uint index = ++indices[i]; + Set *set = getElementSet(getArrayElement(&func->inputs, i)); if (index < getSetSize(set)) { - vals[i]=getSetElement(set, index); - notfinished=true; + vals[i] = getSetElement(set, index); + notfinished = true; break; } else { - indices[i]=0; - vals[i]=getSetElement(set, 0); + indices[i] = 0; + vals[i] = getSetElement(set, 0); } } } - if(getSizeVectorEdge(clauses) == 0){ + if (getSizeVectorEdge(clauses) == 0) { deleteVectorEdge(clauses); return; } - Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); addConstraintCNF(This->cnf, cor); deleteVectorEdge(clauses); } -Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) { - PredicateOperator * predicate = (PredicateOperator*) constraint->predicate; - - switch(predicate->op) { +Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) { + PredicateOperator *predicate = (PredicateOperator *) constraint->predicate; + + switch (predicate->op) { case EQUALS: { return encodeCircuitEquals(This, constraint); } @@ -208,21 +208,21 @@ Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * exit(-1); } -Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) { - PredicateOperator * predicate = (PredicateOperator*) constraint->predicate; +Edge encodeCircuitEquals(SATEncoder *This, BooleanPredicate *constraint) { + PredicateOperator *predicate = (PredicateOperator *) constraint->predicate; ASSERT(getSizeArraySet(&predicate->domains) == 2); Element *elem0 = getArrayElement( &constraint->inputs, 0); encodeElementSATEncoder(This, elem0); Element *elem1 = getArrayElement( &constraint->inputs, 1); encodeElementSATEncoder(This, elem1); - ElementEncoding *ee0=getElementEncoding(elem0); - ElementEncoding *ee1=getElementEncoding(elem1); - ASSERT(ee0->numVars==ee1->numVars); - uint numVars=ee0->numVars; + ElementEncoding *ee0 = getElementEncoding(elem0); + ElementEncoding *ee1 = getElementEncoding(elem1); + ASSERT(ee0->numVars == ee1->numVars); + uint numVars = ee0->numVars; ASSERT(numVars != 0); Edge carray[numVars]; - for (uint i=0; icnf, ee0->variables[i], ee1->variables[i]); + for (uint i = 0; i < numVars; i++) { + carray[i] = constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]); } return constraintAND(This->cnf, numVars, carray); }