1 #include "sattranslator.h"
4 #include "satencoder.h"
9 uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
11 for (int i = elemEnc->numVars - 1; i >= 0; i--) {
13 if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
16 if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
17 model_print("WARNING: Element has undefined value!\n");
18 return elemEnc->encodingArray[index];
21 uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
23 for (int i = elemEnc->numVars - 1; i >= 0; i--) {
25 if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) )
28 if (elemEnc->isBinaryValSigned &&
29 This->getSATEncoder()->getCNF()->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
30 //Do sign extension of negative number
31 uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
34 value += elemEnc->offset;
38 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
41 for (uint i = 0; i < elemEnc->numVars; i++) {
42 if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))) {
48 model_print("WARNING: Element has undefined value!\n");
49 ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
50 return elemEnc->encodingArray[index];
53 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
55 for (i = 0; i < elemEnc->numVars; i++) {
56 if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
61 return elemEnc->encodingArray[i];
64 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
65 ElementEncoding *elemEnc = element->getElementEncoding();
66 if (elemEnc->numVars == 0)//case when the set has only one item
67 return element->getRange()->getElement(0);
68 switch (elemEnc->type) {
70 return getElementValueOneHotSATTranslator(This, elemEnc);
72 return getElementValueUnarySATTranslator(This, elemEnc);
74 return getElementValueBinaryIndexSATTranslator(This, elemEnc);
86 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
87 if (boolean->boolVal == BV_MUSTBETRUE)
89 else if (boolean->boolVal == BV_MUSTBEFALSE)
92 int index = getEdgeVar( ((BooleanVar *) boolean)->var );
93 return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);