From: Hamed Date: Mon, 24 Jul 2017 18:55:47 +0000 (-0700) Subject: Testing one-hot encoding + fixing bugs ... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=90902ff4b8231690dd5875e96b966fb3acc4c534;p=satune.git Testing one-hot encoding + fixing bugs ... --- diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c index 20241b4..ab597a6 100644 --- a/src/Backend/satelemencoder.c +++ b/src/Backend/satelemencoder.c @@ -3,6 +3,7 @@ #include "common.h" #include "ops.h" #include "element.h" +#include "set.h" Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) { switch(getElementEncoding(elem)->type){ @@ -39,14 +40,14 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value) { ASTNodeType type = GETELEMENTTYPE(elem); - ASSERT(type == ELEMSET || type == ELEMFUNCRETURN); + ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST); ElementEncoding* elemEnc = getElementEncoding(elem); for(uint i=0; iencArraySize; i++){ if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) { - return elemEnc->variables[i]; + return (elemEnc->numVars == 0) ? E_True: elemEnc->variables[i]; } } - return E_BOGUS; + return E_False; } Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value) { @@ -100,8 +101,8 @@ void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables); } -void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) { - allocElementConstraintVariables(encoding, encoding->encArraySize); +void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) { + allocElementConstraintVariables(encoding, getSetSize( getElementSet(encoding->element))); getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables); for(uint i=0;inumVars;i++) { for(uint j=i+1;jnumVars;j++) { diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c index a872b62..a9c89fe 100644 --- a/src/Backend/sattranslator.c +++ b/src/Backend/sattranslator.c @@ -8,7 +8,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){ uint index=0; - for(int i=elemEnc->numVars-1;i>=0;i--) { + for(uint i=elemEnc->numVars-1;i>=0;i--) { index=index<<1; if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] ))) index |= 1; @@ -19,7 +19,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){ uint64_t value=0; - for(int i=elemEnc->numVars-1;i>=0;i--) { + for(uint i=elemEnc->numVars-1;i>=0;i--) { value=value<<1; if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) value |= 1; @@ -36,7 +36,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){ uint index=0; - for(int i=elemEnc->numVars-1;i>=0;i--) { + for(uint i=0; i< elemEnc->numVars; i++) { if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] ))) index = i; } @@ -61,11 +61,9 @@ uint64_t getElementValueSATTranslator(CSolver* This, Element* element){ return getSetElement(getElementSet(element), 0); switch(elemEnc->type){ case ONEHOT: - getElementValueOneHotSATTranslator(This, elemEnc); - break; + return getElementValueOneHotSATTranslator(This, elemEnc); case UNARY: - getElementValueUnarySATTranslator(This, elemEnc); - break; + return getElementValueUnarySATTranslator(This, elemEnc); case BINARYINDEX: return getElementValueBinaryIndexSATTranslator(This, elemEnc); case ONEHOTBINARY: diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c index ef0e29e..d5b88d7 100644 --- a/src/Encoders/naiveencoder.c +++ b/src/Encoders/naiveencoder.c @@ -61,8 +61,8 @@ void naiveEncodingPredicate(BooleanPredicate * This) { void naiveEncodingElement(Element * This) { ElementEncoding * encoding = getElementEncoding(This); if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) { - setElementEncodingType(encoding, BINARYINDEX); - baseBinaryIndexElementAssign(encoding); + setElementEncodingType(encoding, ONEHOT); + encodingArrayInitialization(encoding); } if(GETELEMENTTYPE(This) == ELEMFUNCRETURN) { @@ -77,7 +77,7 @@ void naiveEncodingElement(Element * This) { } } -void baseBinaryIndexElementAssign(ElementEncoding *This) { +void encodingArrayInitialization(ElementEncoding *This) { Element * element=This->element; Set * set= getElementSet(element); ASSERT(set->isRange==false); diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h index 3d92e12..20f2943 100644 --- a/src/Encoders/naiveencoder.h +++ b/src/Encoders/naiveencoder.h @@ -14,6 +14,6 @@ void naiveEncodingConstraint(Boolean * This); void naiveEncodingLogicOp(BooleanLogic * This); void naiveEncodingPredicate(BooleanPredicate * This); void naiveEncodingElement(Element * This); -void baseBinaryIndexElementAssign(ElementEncoding *This); +void encodingArrayInitialization(ElementEncoding *This); #endif diff --git a/src/Test/tablefuncencodetest.c b/src/Test/tablefuncencodetest.c index 9d5abed..13337ea 100644 --- a/src/Test/tablefuncencodetest.c +++ b/src/Test/tablefuncencodetest.c @@ -5,9 +5,13 @@ * e3= f(e1, e2) * 1 5 => 7 * 2 3 => 5 + * 1 7 => 1 + * 2 7 => 2 + * 2 5 => 3 + * 1 3 => 4 * e4 = {6, 10, 19} * e4 <= e3 - * Result: e1=1, e2=5, e4=6, overflow=0 + * Result: e1=1, e2=5, e3=7, e4=6, overflow=0 */ int main(int numargs, char ** argv) { CSolver * solver=allocCSolver(); @@ -26,8 +30,16 @@ int main(int numargs, char ** argv) { Table* t1 = createTable(solver, d1, 2, s2); uint64_t row1[] = {1, 5}; uint64_t row2[] = {2, 3}; + uint64_t row3[] = {1, 7}; + uint64_t row4[] = {2, 7}; + uint64_t row5[] = {2, 5}; + uint64_t row6[] = {1, 3}; addTableEntry(solver, t1, row1, 2, 7); addTableEntry(solver, t1, row2, 2, 5); + addTableEntry(solver, t1, row3, 2, 1); + addTableEntry(solver, t1, row4, 2, 2); + addTableEntry(solver, t1, row5, 2, 3); + addTableEntry(solver, t1, row6, 2, 4); Function * f1 = completeTable(solver, t1, FLAGIFFUNDEFINED); Element * e3 = applyFunction(solver, f1, (Element* []){e1,e2}, 2, overflow); @@ -38,8 +50,8 @@ int main(int numargs, char ** argv) { addConstraint(solver, pred); if (startEncoding(solver)==1) - printf("e1=%llu e2=%llu e4=%llu overFlow:%d\n", - getElementValue(solver,e1), getElementValue(solver, e2), + printf("e1=%llu e2=%llu e3=%llu e4=%llu overFlow:%d\n", + getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e3), getElementValue(solver, e4), getBooleanValue(solver, overflow)); else printf("UNSAT\n"); diff --git a/src/csolver.c b/src/csolver.c index 78c6083..d440aad 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -210,6 +210,7 @@ uint64_t getElementValue(CSolver* This, Element* element){ switch(GETELEMENTTYPE(element)){ case ELEMSET: case ELEMCONST: + case ELEMFUNCRETURN: return getElementValueSATTranslator(This, element); default: ASSERT(0);