1 #include "satencoder.h"
8 Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
9 switch (getElementEncoding(elem)->type) {
11 return getElementValueOneHotConstraint(elem, value);
13 return getElementValueUnaryConstraint(elem, value);
15 return getElementValueBinaryIndexConstraint(elem, value);
20 return getElementValueBinaryValueConstraint(elem, value);
29 Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t value) {
30 ASTNodeType type = elem->type;
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(cnf, elemEnc->numVars, elemEnc->variables, i);
41 Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) {
42 ASTNodeType type = elem->type;
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];
53 Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) {
54 ASTNodeType type = elem->type;
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)
62 return constraintNegate(elemEnc->variables[0]);
63 else if ((i + 1) == elemEnc->encArraySize)
64 return elemEnc->variables[i - 1];
66 return constraintAND2(cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
72 Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, uint64_t value) {
73 ASTNodeType type = element->type;
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)
80 //Range wraps around 0
81 if (value < elemEnc->low && value > elemEnc->high)
85 uint64_t valueminusoffset = value - elemEnc->offset;
86 return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
89 void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
90 This->numVars = numVars;
91 This->variables = (Edge *)ourmalloc(sizeof(Edge) * numVars);
94 void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
95 ASSERT(encoding->type == BINARYVAL);
96 allocElementConstraintVariables(encoding, encoding->numBits);
97 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
100 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
101 ASSERT(encoding->type == BINARYINDEX);
102 allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
103 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
106 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
107 allocElementConstraintVariables(encoding, encoding->encArraySize);
108 getArrayNewVarsSATEncoder(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(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
114 addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
117 void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
118 allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
119 getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
120 //Add unary constraint
121 for (uint i = 1; i < encoding->numVars; i++) {
122 addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
126 void SATEncoder::generateElementEncoding(Element *element) {
127 ElementEncoding *encoding = getElementEncoding(element);
128 ASSERT(encoding->type != ELEM_UNASSIGNED);
129 if (encoding->variables != NULL)
131 switch (encoding->type) {
133 generateOneHotEncodingVars(encoding);
136 generateBinaryIndexEncodingVars(encoding);
139 generateUnaryEncodingVars(encoding);
144 generateBinaryValueEncodingVars(encoding);