uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
ElementEncoding *elemEnc = getElementEncoding(element);
if (elemEnc->numVars == 0)//case when the set has only one item
- return getElementSet(element)->getElement(0);
+ return element->getRange()->getElement(0);
switch (elemEnc->type) {
case ONEHOT:
return getElementValueOneHotSATTranslator(This, elemEnc);
return getElementValueUnarySATTranslator(This, elemEnc);
case BINARYINDEX:
return getElementValueBinaryIndexSATTranslator(This, elemEnc);
- case ONEHOTBINARY:
- ASSERT(0);
break;
case BINARYVAL:
ASSERT(0);
}
bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
- int index = getEdgeVar( ((BooleanVar *) boolean)->var );
- return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
+ if (boolean->boolVal == BV_MUSTBETRUE)
+ return true;
+ else if (boolean->boolVal == BV_MUSTBEFALSE)
+ return false;
+ else {
+ int index = getEdgeVar( ((BooleanVar *) boolean)->var );
+ return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
+ }
}
-HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
- ASSERT(order->orderPairTable != NULL);
- OrderPair pair(first, second, E_NULL);
- Edge var = getOrderConstraint(order->orderPairTable, &pair);
- if (edgeIsNull(var))
- return SATC_UNORDERED;
- return getValueCNF(This->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;
-}