1 #include "satencoder.h"
8 Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
9 switch (elem->getElementEncoding()->type) {
11 return getElementValueOneHotConstraint(elem, value);
13 return getElementValueUnaryConstraint(elem, value);
15 return getElementValueBinaryIndexConstraint(elem, value);
17 return getElementValueBinaryValueConstraint(elem, value);
26 Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t value) {
27 ASTNodeType type = elem->type;
28 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
29 ElementEncoding *elemEnc = elem->getElementEncoding();
30 for (uint i = 0; i < elemEnc->encArraySize; i++) {
31 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
32 return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i);
38 Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) {
39 ASTNodeType type = elem->type;
40 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
41 ElementEncoding *elemEnc = elem->getElementEncoding();
42 for (uint i = 0; i < elemEnc->encArraySize; i++) {
43 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
44 return (elemEnc->numVars == 0) ? E_True : elemEnc->variables[i];
50 Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) {
51 ASTNodeType type = elem->type;
52 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
53 ElementEncoding *elemEnc = elem->getElementEncoding();
54 for (uint i = 0; i < elemEnc->encArraySize; i++) {
55 if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
56 if (elemEnc->numVars == 0)
59 return constraintNegate(elemEnc->variables[0]);
60 else if ((i + 1) == elemEnc->encArraySize)
61 return elemEnc->variables[i - 1];
63 return constraintAND2(cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
69 Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, uint64_t value) {
70 ASTNodeType type = element->type;
71 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
72 ElementEncoding *elemEnc = element->getElementEncoding();
73 if (elemEnc->low <= elemEnc->high) {
74 if (value < elemEnc->low || value > elemEnc->high)
77 //Range wraps around 0
78 if (value < elemEnc->low && value > elemEnc->high)
82 uint64_t valueminusoffset = value - elemEnc->offset;
83 return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
86 void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
87 This->numVars = numVars;
88 This->variables = (Edge *)ourmalloc(sizeof(Edge) * numVars);
91 void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
92 ASSERT(encoding->type == BINARYVAL);
93 allocElementConstraintVariables(encoding, encoding->numBits);
94 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
97 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
98 ASSERT(encoding->type == BINARYINDEX);
99 allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
100 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
103 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
104 allocElementConstraintVariables(encoding, encoding->encArraySize);
105 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
106 for (uint i = 0; i < encoding->numVars; i++) {
107 for (uint j = i + 1; j < encoding->numVars; j++) {
108 addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
111 addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
114 void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
115 allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
116 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
117 //Add unary constraint
118 for (uint i = 1; i < encoding->numVars; i++) {
119 addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
123 void SATEncoder::generateElementEncoding(Element *element) {
124 ElementEncoding *encoding = element->getElementEncoding();
125 ASSERT(encoding->type != ELEM_UNASSIGNED);
126 if (encoding->variables != NULL)
128 switch (encoding->type) {
130 generateOneHotEncodingVars(encoding);
133 generateBinaryIndexEncodingVars(encoding);
136 generateUnaryEncodingVars(encoding);
139 generateBinaryValueEncodingVars(encoding);