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 = pred->inputs.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 if(encoding->anyValue)
238 addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
241 void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
242 allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
243 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
244 //Add unary constraint
245 for (uint i = 1; i < encoding->numVars; i++) {
246 addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
250 void SATEncoder::generateElementEncoding(Element *element) {
251 ElementEncoding *encoding = element->getElementEncoding();
252 ASSERT(encoding->type != ELEM_UNASSIGNED);
253 if (encoding->variables != NULL)
255 switch (encoding->type) {
257 generateOneHotEncodingVars(encoding);
260 generateBinaryIndexEncodingVars(encoding);
263 generateUnaryEncodingVars(encoding);
266 generateBinaryValueEncodingVars(encoding);
273 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
274 if(encoding->numVars == 0)
277 for(uint i= encoding->encArraySize-1; i>=0; i--){
278 if(encoding->isinUseElement(i)){
279 if(i+1 < encoding->encArraySize){
286 addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
288 index = index == -1? encoding->encArraySize-1 : index-1;
289 for(int i= index; i>=0; i--) {
290 if (!encoding->isinUseElement(i)){
291 addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
296 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){
297 uint64_t minvalueminusoffset = encoding->low - encoding->offset;
298 uint64_t maxvalueminusoffset = encoding->high - encoding->offset;
299 model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
300 Edge lowerbound = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, maxvalueminusoffset);
301 Edge upperbound = constraintNegate(generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, minvalueminusoffset));
302 addConstraintCNF(cnf, lowerbound);
303 addConstraintCNF(cnf, upperbound);