1 #include "sattranslator.h"
4 #include "satencoder.h"
7 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
9 for(int i=elemEnc->numVars-1;i>=0;i--) {
11 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
14 ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
15 return elemEnc->encodingArray[index];
18 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
19 //THIS WILL PROBABLY BE WRONG SINCE THE VALUES CAN BE OFFSET
21 for(int i=elemEnc->numVars-1;i>=0;i--) {
23 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
29 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
31 for(int i=elemEnc->numVars-1;i>=0;i--) {
32 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
35 ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
36 return elemEnc->encodingArray[index];
39 uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
41 for(i=0;i<elemEnc->numVars;i++) {
42 if (!This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) {
47 return elemEnc->encodingArray[i];
50 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
51 Set* set = getElementSet(element);
52 if(getSetSize( set ) ==1) //case when the set has only one item
53 return getSetElement(set, 0);
54 ElementEncoding* elemEnc = getElementEncoding(element);
55 switch(elemEnc->type){
57 getElementValueOneHotSATTranslator(This, elemEnc);
60 getElementValueUnarySATTranslator(This, elemEnc);
63 return getElementValueBinaryIndexSATTranslator(This, elemEnc);
77 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
78 int index = getEdgeVar( ((BooleanVar*) boolean)->var );
79 return This->satEncoder->cnf->solver->solution[index] == true;