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 a768a4fa61d011cb047d8d0c4650ac548b5463ba..ca0fdaeccda4aeb69dcc1c5bfaa2f43b92832304 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -2,40 +2,95 @@
 #include "element.h"
 #include "csolver.h"
 #include "satencoder.h"
+#include "set.h"
+#include "order.h"
+#include "orderpair.h"
 
-uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-       uint index=0;
-       for(int i=elemEnc->numVars-1;i>=0;i--) {
-               index=index<<1;
-               if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
+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 getElementValueSATTranslator(CSolver* This, Element* element){
-       switch(getElementEncoding(element)->type){
-               case ONEHOT:
-                       ASSERT(0);
-                       break;
-               case UNARY:
-                       ASSERT(0);
-                       break;
-               case BINARYINDEX:
-                       return getElementValueBinaryIndexSATTranslator(This, getElementEncoding(element));
-               case ONEHOTBINARY:
-                       ASSERT(0);
-                       break;
-               case BINARYVAL:
-                       ASSERT(0);
-                       break;
-               default:
-                       ASSERT(0);
+
+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])]) {
+               //Do sign extension of negative number
+               uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+               value += highbits;
+       }
+       value += elemEnc->offset;
+       return value;
+}
+
+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));
+       return elemEnc->encodingArray[index];
+}
+
+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] )) ) {
                        break;
+               }
+       }
+
+       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
+               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;
        }
+       return -1;
+}
+
+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))
+               return UNORDERED;
+       return getValueCNF(This->satEncoder->cnf, var) ? FIRST : SECOND;
 }
 
-bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
-       int index = getEdgeVar( ((BooleanVar*) boolean)->var );
-       return This->satEncoder->cnf->solver->solution[index] == true;
-}
\ No newline at end of file