1 #include "satencoder.h"
7 Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
8 switch(getElementEncoding(elem)->type){
10 return getElementValueOneHotConstraint(This, elem, value);
12 return getElementValueUnaryConstraint(This, elem, value);
14 return getElementValueBinaryIndexConstraint(This, elem, value);
19 return getElementValueBinaryValueConstraint(This, elem, value);
28 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) {
29 ASTNodeType type = GETELEMENTTYPE(elem);
30 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
31 ElementEncoding* elemEnc = getElementEncoding(elem);
32 for(uint i=0; i<elemEnc->encArraySize; i++){
33 if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
34 return (elemEnc->numVars == 0) ? E_True: generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
40 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value) {
41 ASTNodeType type = GETELEMENTTYPE(elem);
42 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
43 ElementEncoding* elemEnc = getElementEncoding(elem);
44 for(uint i=0; i<elemEnc->encArraySize; i++){
45 if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
46 return elemEnc->variables[i];
52 Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value) {
53 ASTNodeType type = GETELEMENTTYPE(elem);
54 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
55 ElementEncoding* elemEnc = getElementEncoding(elem);
56 for(uint i=0; i<elemEnc->encArraySize; i++){
57 if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
59 return constraintNegate(elemEnc->variables[0]);
60 else if ((i+1)==elemEnc->encArraySize)
61 return elemEnc->variables[i-1];
63 return constraintAND2(This->cnf, elemEnc->variables[i-1], constraintNegate(elemEnc->variables[i]));
69 Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value){
70 ASTNodeType type = GETELEMENTTYPE(element);
71 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
72 ElementEncoding* elemEnc = getElementEncoding(element);
73 for(uint i=0; i<elemEnc->encArraySize; i++){
74 if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
75 return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, value);
76 // This constraint can be generated right away without iterating over encodingArray
77 // but we need to make sure that element with that value is in use ...
83 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
84 This->numVars = numVars;
85 This->variables = ourmalloc(sizeof(Edge) * numVars);
88 void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding){
89 ASSERT(encoding->type==BINARYVAL);
90 allocElementConstraintVariables(encoding, getMaximumBitsBinaryValueEncodingVars(encoding));
91 getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
94 void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
95 ASSERT(encoding->type==BINARYINDEX);
96 allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize-1));
97 getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
100 void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
101 allocElementConstraintVariables(encoding, encoding->encArraySize);
102 getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
103 for(uint i=0;i<encoding->numVars;i++) {
104 for(uint j=i+1;j<encoding->numVars;j++) {
105 addConstraintCNF(This->cnf, constraintNegate(constraintAND2(This->cnf, encoding->variables[i], encoding->variables[j])));
108 addConstraintCNF(This->cnf, constraintOR(This->cnf, encoding->numVars, encoding->variables));
111 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
112 allocElementConstraintVariables(encoding, encoding->encArraySize-1);
113 getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
114 //Add unary constraint
115 for(uint i=1;i<encoding->numVars;i++) {
116 addConstraintCNF(This->cnf, constraintOR2(This->cnf, encoding->variables[i-1], constraintNegate(encoding->variables[i])));
120 void generateElementEncoding(SATEncoder* This, Element * element) {
121 ElementEncoding* encoding = getElementEncoding(element);
122 ASSERT(encoding->type!=ELEM_UNASSIGNED);
123 if(encoding->variables!=NULL)
125 switch(encoding->type) {
127 generateOneHotEncodingVars(This, encoding);
130 generateBinaryIndexEncodingVars(This, encoding);
133 generateUnaryEncodingVars(This, encoding);
138 generateBinaryValueEncodingVars(This, encoding);