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->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
16 model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, isinUseElement(elemEnc, index));
17 ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
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->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
28 if (elemEnc->isBinaryValSigned &&
29 This->satEncoder->cnf->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) {
40 for (uint i = 0; i < elemEnc->numVars; i++) {
41 if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
44 ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
45 return elemEnc->encodingArray[index];
48 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
50 for (i = 0; i < elemEnc->numVars; i++) {
51 if (!getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
56 return elemEnc->encodingArray[i];
59 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
60 ElementEncoding *elemEnc = getElementEncoding(element);
61 if (elemEnc->numVars == 0)//case when the set has only one item
62 return getSetElement(getElementSet(element), 0);
63 switch (elemEnc->type) {
65 return getElementValueOneHotSATTranslator(This, elemEnc);
67 return getElementValueUnarySATTranslator(This, elemEnc);
69 return getElementValueBinaryIndexSATTranslator(This, elemEnc);
83 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
84 int index = getEdgeVar( ((BooleanVar *) boolean)->var );
85 return getValueSolver(This->satEncoder->cnf->solver, index);
88 HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
89 ASSERT(order->orderPairTable != NULL);
90 OrderPair pair = {first, second, E_NULL};
91 Edge var = getOrderConstraint(order->orderPairTable, &pair);
94 return getValueCNF(This->satEncoder->cnf, var) ? FIRST : SECOND;