edits
[satune.git] / src / Backend / satelemencoder.cc
1 #include "satencoder.h"
2 #include "structs.h"
3 #include "common.h"
4 #include "ops.h"
5 #include "element.h"
6 #include "set.h"
7
8 Edge getElementValueConstraint(SATEncoder *This, Element *elem, uint64_t value) {
9         switch (getElementEncoding(elem)->type) {
10         case ONEHOT:
11                 return getElementValueOneHotConstraint(This, elem, value);
12         case UNARY:
13                 return getElementValueUnaryConstraint(This, elem, value);
14         case BINARYINDEX:
15                 return getElementValueBinaryIndexConstraint(This, elem, value);
16         case ONEHOTBINARY:
17                 ASSERT(0);
18                 break;
19         case BINARYVAL:
20                 return getElementValueBinaryValueConstraint(This, elem, value);
21                 break;
22         default:
23                 ASSERT(0);
24                 break;
25         }
26         return E_BOGUS;
27 }
28
29 Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *elem, uint64_t value) {
30         ASTNodeType type = GETELEMENTTYPE(elem);
31         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
32         ElementEncoding *elemEnc = getElementEncoding(elem);
33         for (uint i = 0; i < elemEnc->encArraySize; i++) {
34                 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
35                         return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, i);
36                 }
37         }
38         return E_False;
39 }
40
41 Edge getElementValueOneHotConstraint(SATEncoder *This, Element *elem, uint64_t value) {
42         ASTNodeType type = GETELEMENTTYPE(elem);
43         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
44         ElementEncoding *elemEnc = getElementEncoding(elem);
45         for (uint i = 0; i < elemEnc->encArraySize; i++) {
46                 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
47                         return (elemEnc->numVars == 0) ? E_True : elemEnc->variables[i];
48                 }
49         }
50         return E_False;
51 }
52
53 Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t value) {
54         ASTNodeType type = GETELEMENTTYPE(elem);
55         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
56         ElementEncoding *elemEnc = getElementEncoding(elem);
57         for (uint i = 0; i < elemEnc->encArraySize; i++) {
58                 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
59                         if (elemEnc->numVars == 0)
60                                 return E_True;
61                         if (i == 0)
62                                 return constraintNegate(elemEnc->variables[0]);
63                         else if ((i + 1) == elemEnc->encArraySize)
64                                 return elemEnc->variables[i - 1];
65                         else
66                                 return constraintAND2(This->getCNF(), elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
67                 }
68         }
69         return E_False;
70 }
71
72 Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, uint64_t value) {
73         ASTNodeType type = GETELEMENTTYPE(element);
74         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
75         ElementEncoding *elemEnc = getElementEncoding(element);
76         if (elemEnc->low <= elemEnc->high) {
77                 if (value < elemEnc->low || value > elemEnc->high)
78                         return E_False;
79         } else {
80                 //Range wraps around 0
81                 if (value < elemEnc->low && value > elemEnc->high)
82                         return E_False;
83         }
84
85         uint64_t valueminusoffset = value - elemEnc->offset;
86         return generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, valueminusoffset);
87 }
88
89 void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
90         This->numVars = numVars;
91         This->variables = (Edge *)ourmalloc(sizeof(Edge) * numVars);
92 }
93
94 void generateBinaryValueEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
95         ASSERT(encoding->type == BINARYVAL);
96         allocElementConstraintVariables(encoding, encoding->numBits);
97         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
98 }
99
100 void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
101         ASSERT(encoding->type == BINARYINDEX);
102         allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
103         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
104 }
105
106 void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
107         allocElementConstraintVariables(encoding, encoding->encArraySize);
108         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
109         for (uint i = 0; i < encoding->numVars; i++) {
110                 for (uint j = i + 1; j < encoding->numVars; j++) {
111                         addConstraintCNF(This->getCNF(), constraintNegate(constraintAND2(This->getCNF(), encoding->variables[i], encoding->variables[j])));
112                 }
113         }
114         addConstraintCNF(This->getCNF(), constraintOR(This->getCNF(), encoding->numVars, encoding->variables));
115 }
116
117 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
118         allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
119         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
120         //Add unary constraint
121         for (uint i = 1; i < encoding->numVars; i++) {
122                 addConstraintCNF(This->getCNF(), constraintOR2(This->getCNF(), encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
123         }
124 }
125
126 void generateElementEncoding(SATEncoder *This, Element *element) {
127         ElementEncoding *encoding = getElementEncoding(element);
128         ASSERT(encoding->type != ELEM_UNASSIGNED);
129         if (encoding->variables != NULL)
130                 return;
131         switch (encoding->type) {
132         case ONEHOT:
133                 generateOneHotEncodingVars(This, encoding);
134                 return;
135         case BINARYINDEX:
136                 generateBinaryIndexEncodingVars(This, encoding);
137                 return;
138         case UNARY:
139                 generateUnaryEncodingVars(This, encoding);
140                 return;
141         case ONEHOTBINARY:
142                 return;
143         case BINARYVAL:
144                 generateBinaryValueEncodingVars(This, encoding);
145                 return;
146         default:
147                 ASSERT(0);
148         }
149 }
150