Add LTE function for completeness and fix bug in LT

[satune.git] / src / Backend / sattranslator.c

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a9c89fe6c781410b3c7f22702613768a05ecc8c5..ca0fdaeccda4aeb69dcc1c5bfaa2f43b92832304 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -6,48 +6,49 @@
 #include "order.h"
 #include "orderpair.h"
 
-uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-       uint index=0;
-       for(uint i=elemEnc->numVars-1;i>=0;i--) {
-               index=index<<1;
+uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+       uint index = 0;
+       for (int i = elemEnc->numVars - 1; i >= 0; i--) {
+               index = index << 1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
        }
-       ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
+       model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, isinUseElement(elemEnc, index));
+       ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
        return elemEnc->encodingArray[index];
 }
 
-uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-       uint64_t value=0;
-       for(uint i=elemEnc->numVars-1;i>=0;i--) {
-               value=value<<1;
+uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+       uint64_t value = 0;
+       for (int i = elemEnc->numVars - 1; i >= 0; i--) {
+               value = value << 1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;
        }
        if (elemEnc->isBinaryValSigned &&
-                       This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars-1])]) {
+                       This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
                //Do sign extension of negative number
-               uint64_t highbits=0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
-               value+=highbits;
+               uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+               value += highbits;
        }
-       value+=elemEnc->offset;
+       value += elemEnc->offset;
        return value;
 }
 
-uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-       uint index=0;
-       for(uint i=0; i< elemEnc->numVars; i++) {
+uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+       uint index = 0;
+       for (uint i = 0; i < elemEnc->numVars; i++) {
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index = i;
        }
-       ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
+       ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
        return elemEnc->encodingArray[index];
 }
 
-uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
+uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
        uint i;
-       for(i=0;i<elemEnc->numVars;i++) {
-               if (! getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+       for (i = 0; i < elemEnc->numVars; i++) {
+               if (!getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
                        break;
                }
        }
@@ -55,41 +56,41 @@ uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemE
        return elemEnc->encodingArray[i];
 }
 
-uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
-       ElementEncoding* elemEnc = getElementEncoding(element);
-       if(elemEnc->numVars == 0)       //case when the set has only one item
+uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
+       ElementEncoding *elemEnc = getElementEncoding(element);
+       if (elemEnc->numVars == 0)//case when the set has only one item
                return getSetElement(getElementSet(element), 0);
-       switch(elemEnc->type){
-               case ONEHOT:
-                       return getElementValueOneHotSATTranslator(This, elemEnc);
-               case UNARY:
-                       return getElementValueUnarySATTranslator(This, elemEnc);
-               case BINARYINDEX:
-                       return getElementValueBinaryIndexSATTranslator(This, elemEnc);
-               case ONEHOTBINARY:
-                       ASSERT(0);
-                       break;
-               case BINARYVAL:
-                       ASSERT(0);
-                       break;
-               default:
-                       ASSERT(0);
-                       break;
+       switch (elemEnc->type) {
+       case ONEHOT:
+               return getElementValueOneHotSATTranslator(This, elemEnc);
+       case UNARY:
+               return getElementValueUnarySATTranslator(This, elemEnc);
+       case BINARYINDEX:
+               return getElementValueBinaryIndexSATTranslator(This, elemEnc);
+       case ONEHOTBINARY:
+               ASSERT(0);
+               break;
+       case BINARYVAL:
+               ASSERT(0);
+               break;
+       default:
+               ASSERT(0);
+               break;
        }
        return -1;
 }
 
-bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
-       int index = getEdgeVar( ((BooleanVar*) boolean)->var );
+bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
+       int index = getEdgeVar( ((BooleanVar *) boolean)->var );
        return getValueSolver(This->satEncoder->cnf->solver, index);
 }
 
-HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
-       ASSERT(order->orderPairTable!= NULL);
-       OrderPair pair={first, second, E_NULL};
-       Edge var = getOrderConstraint(order->orderPairTable, &pair); 
-       if(edgeIsNull(var))
+HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
+       ASSERT(order->orderPairTable != NULL);
+       OrderPair pair = {first, second, E_NULL};
+       Edge var = getOrderConstraint(order->orderPairTable, &pair);
+       if (edgeIsNull(var))
                return UNORDERED;
-       return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND;
+       return getValueCNF(This->satEncoder->cnf, var) ? FIRST : SECOND;
 }