1 #include "satencoder.h"
10 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
11 uint numParents = elem->parents.getSize();
15 if (elem->type == ELEMFUNCRETURN) {
18 for(uint i = 0; i < numParents; i++) {
19 ASTNode * node = elem->parents.get(i);
20 if (node->type == PREDICATEOP) {
21 BooleanPredicate * pred = (BooleanPredicate *) node;
22 Polarity polarity = pred->polarity;
23 FunctionEncodingType encType = pred->encoding.type;
24 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
25 if (pred->predicate->type == TABLEPRED) {
26 //Could be smarter, but just do default thing for now
28 UndefinedBehavior undefStatus = ((PredicateTable *)pred->predicate)->undefinedbehavior;
30 Polarity tpolarity=polarity;
32 tpolarity = negatePolarity(tpolarity);
33 if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
34 tpolarity = P_BOTHTRUEFALSE;
35 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
37 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
39 } else if (pred->predicate->type == OPERATORPRED) {
40 if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
41 Polarity tpolarity = polarity;
43 tpolarity = negatePolarity(tpolarity);
44 PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
45 uint numDomains = predicate->domains.getSize();
46 bool isConstant = true;
47 for (uint i = 0; i < numDomains; i++) {
48 Element *e = pred->inputs.get(i);
49 if (elem != e && e->type != ELEMCONST) {
53 if (predicate->getOp() == SATC_EQUALS) {
54 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
56 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
60 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
62 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
65 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
67 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
75 } else if (node->type == ELEMFUNCRETURN) {
76 //we are input to function, so memoize negative case
89 Edge SATEncoder::getElementValueConstraint(Element *elem, Polarity p, uint64_t value) {
90 switch (elem->getElementEncoding()->type) {
92 return getElementValueOneHotConstraint(elem, p, value);
94 return getElementValueUnaryConstraint(elem, p, value);
96 return getElementValueBinaryIndexConstraint(elem, p, value);
98 return getElementValueBinaryValueConstraint(elem, p, value);
107 bool impliesPolarity(Polarity curr, Polarity goal) {
108 return (((int) curr) & ((int)goal)) == ((int) goal);
111 Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, Polarity p, uint64_t value) {
112 ASTNodeType type = elem->type;
113 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
114 ElementEncoding *elemEnc = elem->getElementEncoding();
116 //Check if we need to generate proxy variables
117 if (elemEnc->encoding == EENC_UNKNOWN && elemEnc->numVars > 1) {
119 shouldMemoize(elem, value, memo);
121 elemEnc->encoding = EENC_BOTH;
122 elemEnc->polarityArray = (Polarity *) ourcalloc(1, sizeof(Polarity) * elemEnc->encArraySize);
123 elemEnc->edgeArray = (Edge *) ourcalloc(1, sizeof(Edge) * elemEnc->encArraySize);
125 elemEnc->encoding = EENC_NONE;
129 for (uint i = 0; i < elemEnc->encArraySize; i++) {
130 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
131 if (elemEnc->numVars == 0)
134 if (elemEnc->encoding != EENC_NONE && elemEnc->numVars > 1) {
135 if (impliesPolarity(elemEnc->polarityArray[i], p)) {
136 return elemEnc->edgeArray[i];
138 if (edgeIsNull(elemEnc->edgeArray[i])) {
139 elemEnc->edgeArray[i] = constraintNewVar(cnf);
141 if (elemEnc->polarityArray[i] == P_UNDEFINED && p == P_BOTHTRUEFALSE) {
142 generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_BOTHTRUEFALSE);
143 elemEnc->polarityArray[i] = p;
144 } else if (!impliesPolarity(elemEnc->polarityArray[i], P_TRUE) && impliesPolarity(p, P_TRUE)) {
145 generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);
146 elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_TRUE));
147 } else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE) && impliesPolarity(p, P_FALSE)) {
148 generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);
149 elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_FALSE));
151 return elemEnc->edgeArray[i];
154 return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i);
160 Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, Polarity p, uint64_t value) {
161 ASTNodeType type = elem->type;
162 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
163 ElementEncoding *elemEnc = elem->getElementEncoding();
164 for (uint i = 0; i < elemEnc->encArraySize; i++) {
165 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
166 return (elemEnc->numVars == 0) ? E_True : elemEnc->variables[i];
172 Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, Polarity p, uint64_t value) {
173 ASTNodeType type = elem->type;
174 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
175 ElementEncoding *elemEnc = elem->getElementEncoding();
176 for (uint i = 0; i < elemEnc->encArraySize; i++) {
177 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
178 if (elemEnc->numVars == 0)
181 return constraintNegate(elemEnc->variables[0]);
182 else if ((i + 1) == elemEnc->encArraySize)
183 return elemEnc->variables[i - 1];
185 return constraintAND2(cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
191 Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, Polarity p, uint64_t value) {
192 ASTNodeType type = element->type;
193 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
194 ElementEncoding *elemEnc = element->getElementEncoding();
195 if (elemEnc->low <= elemEnc->high) {
196 if (value < elemEnc->low || value > elemEnc->high)
199 //Range wraps around 0
200 if (value < elemEnc->low && value > elemEnc->high)
204 uint64_t valueminusoffset = value - elemEnc->offset;
205 return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
208 void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
209 This->numVars = numVars;
210 This->variables = (Edge *)ourmalloc(sizeof(Edge) * numVars);
213 void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
214 ASSERT(encoding->type == BINARYVAL);
215 allocElementConstraintVariables(encoding, encoding->numBits);
216 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
217 if(encoding->anyValue)
218 generateAnyValueBinaryValueEncoding(encoding);
221 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
222 ASSERT(encoding->type == BINARYINDEX);
223 allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
224 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
225 if(encoding->anyValue)
226 generateAnyValueBinaryIndexEncoding(encoding);
229 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
230 allocElementConstraintVariables(encoding, encoding->encArraySize);
231 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
232 for (uint i = 0; i < encoding->numVars; i++) {
233 for (uint j = i + 1; j < encoding->numVars; j++) {
234 addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
237 addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
238 if(encoding->anyValue)
239 generateAnyValueOneHotEncoding(encoding);
242 void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
243 allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
244 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
245 //Add unary constraint
246 for (uint i = 1; i < encoding->numVars; i++) {
247 addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
251 void SATEncoder::generateElementEncoding(Element *element) {
252 ElementEncoding *encoding = element->getElementEncoding();
253 ASSERT(encoding->type != ELEM_UNASSIGNED);
254 if (encoding->variables != NULL)
256 switch (encoding->type) {
258 generateOneHotEncodingVars(encoding);
261 generateBinaryIndexEncodingVars(encoding);
264 generateUnaryEncodingVars(encoding);
267 generateBinaryValueEncodingVars(encoding);
274 void SATEncoder::generateAnyValueOneHotEncoding(ElementEncoding *encoding){
275 if(encoding->numVars == 0)
277 Edge carray[encoding->numVars];
279 for (uint i = 0; i < encoding->encArraySize; i++) {
280 if (encoding->isinUseElement(i)){
281 carray[size++] = encoding->variables[i];
285 addConstraintCNF(cnf, constraintOR(cnf, size, carray));
289 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
290 if(encoding->numVars == 0)
292 Edge carray[encoding->numVars];
295 for(uint i= encoding->encArraySize-1; i>=0; i--){
296 if(encoding->isinUseElement(i)){
297 if(i+1 < encoding->encArraySize){
304 carray[size++] = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index);
306 index = index == -1? encoding->encArraySize-1 : index-1;
307 for(int i= index; i>=0; i--){
308 if (!encoding->isinUseElement(i)){
309 carray[size++] = constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i));
313 addConstraintCNF(cnf, constraintAND(cnf, size, carray));
317 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){
318 uint64_t minvalueminusoffset = encoding->low - encoding->offset;
319 uint64_t maxvalueminusoffset = encoding->high - encoding->offset;
320 model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
321 Edge lowerbound = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, maxvalueminusoffset);
322 Edge upperbound = constraintNegate(generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, minvalueminusoffset));
323 addConstraintCNF(cnf, constraintAND2(cnf, lowerbound, upperbound));