1 #include "satencoder.h"
11 void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
12 uint numParents = elem->parents.getSize();
16 if (elem->type == ELEMFUNCRETURN) {
19 for (uint i = 0; i < numParents; i++) {
20 ASTNode *node = elem->parents.get(i);
21 if (node->type == PREDICATEOP) {
22 BooleanPredicate *pred = (BooleanPredicate *) node;
23 Polarity polarity = pred->polarity;
24 FunctionEncodingType encType = pred->encoding.type;
25 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
26 if (pred->predicate->type == TABLEPRED) {
27 //Could be smarter, but just do default thing for now
29 UndefinedBehavior undefStatus = ((PredicateTable *)pred->predicate)->undefinedbehavior;
31 Polarity tpolarity = polarity;
33 tpolarity = negatePolarity(tpolarity);
34 if (undefStatus == SATC_FLAGFORCEUNDEFINED)
35 tpolarity = P_BOTHTRUEFALSE;
36 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
38 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
40 } else if (pred->predicate->type == OPERATORPRED) {
41 if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
42 Polarity tpolarity = polarity;
44 tpolarity = negatePolarity(tpolarity);
45 PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
46 uint numDomains = pred->inputs.getSize();
47 bool isConstant = true;
48 for (uint i = 0; i < numDomains; i++) {
49 Element *e = pred->inputs.get(i);
50 if (elem != e && e->type != ELEMCONST) {
54 if (predicate->getOp() == SATC_EQUALS) {
55 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
57 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
61 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
63 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
66 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
68 if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
76 } else if (node->type == ELEMFUNCRETURN) {
77 //we are input to function, so memoize negative case
90 Edge SATEncoder::getElementValueConstraint(Element *elem, Polarity p, uint64_t value) {
91 switch (elem->getElementEncoding()->type) {
93 return getElementValueOneHotConstraint(elem, p, value);
95 return getElementValueUnaryConstraint(elem, p, value);
97 return getElementValueBinaryIndexConstraint(elem, p, value);
99 return getElementValueBinaryValueConstraint(elem, p, value);
108 bool impliesPolarity(Polarity curr, Polarity goal) {
109 return (((int) curr) & ((int)goal)) == ((int) goal);
112 Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, Polarity p, uint64_t value) {
113 ASTNodeType type = elem->type;
114 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
115 ElementEncoding *elemEnc = elem->getElementEncoding();
117 //Check if we need to generate proxy variables
118 if (elemEnc->encoding == EENC_UNKNOWN && elemEnc->numVars > 1) {
120 shouldMemoize(elem, value, memo);
122 elemEnc->encoding = EENC_BOTH;
123 elemEnc->polarityArray = (Polarity *) ourcalloc(1, sizeof(Polarity) * elemEnc->encArraySize);
124 elemEnc->edgeArray = (Edge *) ourcalloc(1, sizeof(Edge) * elemEnc->encArraySize);
126 elemEnc->encoding = EENC_NONE;
130 for (uint i = 0; i < elemEnc->encArraySize; i++) {
131 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
132 if (elemEnc->numVars == 0)
135 if (elemEnc->encoding != EENC_NONE && elemEnc->numVars > 1) {
136 if (impliesPolarity(elemEnc->polarityArray[i], p)) {
137 return elemEnc->edgeArray[i];
139 if (edgeIsNull(elemEnc->edgeArray[i])) {
140 elemEnc->edgeArray[i] = constraintNewVar(cnf);
142 if (elemEnc->polarityArray[i] == P_UNDEFINED && p == P_BOTHTRUEFALSE) {
143 generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_BOTHTRUEFALSE);
144 elemEnc->polarityArray[i] = p;
145 } else if (!impliesPolarity(elemEnc->polarityArray[i], P_TRUE) && impliesPolarity(p, P_TRUE)) {
146 generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);
147 elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_TRUE));
148 } else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE) && impliesPolarity(p, P_FALSE)) {
149 generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);
150 elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_FALSE));
152 return elemEnc->edgeArray[i];
155 return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i);
161 Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, Polarity p, uint64_t value) {
162 ASTNodeType type = elem->type;
163 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
164 ElementEncoding *elemEnc = elem->getElementEncoding();
165 for (uint i = 0; i < elemEnc->encArraySize; i++) {
166 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
167 return (elemEnc->numVars == 0) ? E_True : elemEnc->variables[i];
173 Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, Polarity p, uint64_t value) {
174 ASTNodeType type = elem->type;
175 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
176 ElementEncoding *elemEnc = elem->getElementEncoding();
177 for (uint i = 0; i < elemEnc->encArraySize; i++) {
178 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
179 if (elemEnc->numVars == 0)
182 return constraintNegate(elemEnc->variables[0]);
183 else if ((i + 1) == elemEnc->encArraySize)
184 return elemEnc->variables[i - 1];
186 return constraintAND2(cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
192 Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, Polarity p, uint64_t value) {
193 ASTNodeType type = element->type;
194 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
195 ElementEncoding *elemEnc = element->getElementEncoding();
196 if (elemEnc->low <= elemEnc->high) {
197 if (value < elemEnc->low || value > elemEnc->high)
200 //Range wraps around 0
201 if (value < elemEnc->low && value > elemEnc->high)
205 uint64_t valueminusoffset = value - elemEnc->offset;
206 return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
209 void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
210 This->numVars = numVars;
211 This->variables = (Edge *)ourmalloc(sizeof(Edge) * numVars);
214 void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
215 ASSERT(encoding->type == BINARYVAL);
216 allocElementConstraintVariables(encoding, encoding->numBits);
217 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
218 if (encoding->element->anyValue)
219 generateAnyValueBinaryValueEncoding(encoding);
222 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
223 ASSERT(encoding->type == BINARYINDEX);
224 allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
225 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
226 if (encoding->element->anyValue) {
227 uint setSize = encoding->element->getRange()->getSize();
228 uint encArraySize = encoding->encArraySize;
229 if (setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) / 10) {
230 generateAnyValueBinaryIndexEncodingPositive(encoding);
232 generateAnyValueBinaryIndexEncoding(encoding);
237 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
238 allocElementConstraintVariables(encoding, encoding->encArraySize);
239 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
240 for (uint i = 0; i < encoding->numVars; i++) {
241 for (uint j = i + 1; j < encoding->numVars; j++) {
242 addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
245 if (encoding->element->anyValue)
246 addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
249 void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
250 allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
251 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
252 //Add unary constraint
253 for (uint i = 1; i < encoding->numVars; i++) {
254 addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
258 void SATEncoder::generateElementEncoding(Element *element) {
259 ElementEncoding *encoding = element->getElementEncoding();
260 ASSERT(encoding->type != ELEM_UNASSIGNED);
261 if (encoding->variables != NULL)
263 switch (encoding->type) {
265 generateOneHotEncodingVars(encoding);
268 generateBinaryIndexEncodingVars(encoding);
271 generateUnaryEncodingVars(encoding);
274 generateBinaryValueEncodingVars(encoding);
281 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
282 if (encoding->numVars == 0)
285 for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
286 if (encoding->isinUseElement(i)) {
287 if (i + 1 < encoding->encArraySize) {
294 addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
296 index = index == -1 ? encoding->encArraySize - 1 : index - 1;
297 for (int i = index; i >= 0; i--) {
298 if (!encoding->isinUseElement(i)) {
299 addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
304 void SATEncoder::generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding) {
305 if (encoding->numVars == 0)
307 Edge carray[encoding->encArraySize];
309 for (uint i = 0; i < encoding->encArraySize; i++) {
310 if (encoding->isinUseElement(i)) {
311 carray[size] = generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i);
315 addConstraintCNF(cnf, constraintOR(cnf, size, carray));
318 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
319 uint64_t minvalueminusoffset = encoding->low - encoding->offset;
320 uint64_t maxvalueminusoffset = encoding->high - encoding->offset;
321 model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
322 Edge lowerbound = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, maxvalueminusoffset);
323 Edge upperbound = constraintNegate(generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, minvalueminusoffset));
324 addConstraintCNF(cnf, lowerbound);
325 addConstraintCNF(cnf, upperbound);