7b8eae0d8ff16b6b7fc0521aa3af9956eb7dc90a
[satune.git] / src / Backend / sattranslator.cc
1 #include "sattranslator.h"
2 #include "element.h"
3 #include "csolver.h"
4 #include "satencoder.h"
5 #include "set.h"
6 #include "order.h"
7 #include "orderpair.h"
8
9 uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
10         uint index = 0;
11         for (int i = elemEnc->numVars - 1; i >= 0; i--) {
12                 index = index << 1;
13                 if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
14                         index |= 1;
15         }
16         if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
17                 model_print("WARNING: Element has undefined value!\n");
18         return elemEnc->encodingArray[index];
19 }
20
21 uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
22         uint64_t value = 0;
23         for (int i = elemEnc->numVars - 1; i >= 0; i--) {
24                 value = value << 1;
25                 if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
26                         value |= 1;
27         }
28         if (elemEnc->isBinaryValSigned &&
29                         This->getSATEncoder()->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
30                 //Do sign extension of negative number
31                 uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
32                 value += highbits;
33         }
34         value += elemEnc->offset;
35         return value;
36 }
37
38 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
39         uint index = 0;
40         for (uint i = 0; i < elemEnc->numVars; i++) {
41                 if (getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
42                         index = i;
43         }
44         ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
45         return elemEnc->encodingArray[index];
46 }
47
48 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
49         uint i;
50         for (i = 0; i < elemEnc->numVars; i++) {
51                 if (!getValueSolver(This->getSATEncoder()->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
52                         break;
53                 }
54         }
55
56         return elemEnc->encodingArray[i];
57 }
58
59 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
60         ElementEncoding *elemEnc = getElementEncoding(element);
61         if (elemEnc->numVars == 0)//case when the set has only one item
62                 return getElementSet(element)->getElement(0);
63         switch (elemEnc->type) {
64         case ONEHOT:
65                 return getElementValueOneHotSATTranslator(This, elemEnc);
66         case UNARY:
67                 return getElementValueUnarySATTranslator(This, elemEnc);
68         case BINARYINDEX:
69                 return getElementValueBinaryIndexSATTranslator(This, elemEnc);
70         case ONEHOTBINARY:
71                 ASSERT(0);
72                 break;
73         case BINARYVAL:
74                 ASSERT(0);
75                 break;
76         default:
77                 ASSERT(0);
78                 break;
79         }
80         return -1;
81 }
82
83 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
84         int index = getEdgeVar( ((BooleanVar *) boolean)->var );
85         return getValueSolver(This->getSATEncoder()->cnf->solver, index);
86 }
87
88 HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
89         ASSERT(order->orderPairTable != NULL);
90         OrderPair pair(first, second, E_NULL);
91         Edge var = getOrderConstraint(order->orderPairTable, &pair);
92         if (edgeIsNull(var))
93                 return UNORDERED;
94         return getValueCNF(This->getSATEncoder()->cnf, var) ? FIRST : SECOND;
95 }
96