ASTNodeType type = GETELEMENTTYPE(element);
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
ElementEncoding* elemEnc = getElementEncoding(element);
- for(uint i=0; i<elemEnc->encArraySize; i++){
- if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
- return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, value);
- // This constraint can be generated right away without iterating over encodingArray
- // but we need to make sure that element with that value is in use ...
- }
+ if (elemEnc->low <= elemEnc->high) {
+ if (value < elemEnc->low || value > elemEnc->high)
+ return E_False;
+ } else {
+ //Range wraps around 0
+ if (value < elemEnc->low && value > elemEnc->high)
+ return E_False;
}
- return E_BOGUS;
+
+ uint64_t valueminusoffset=value-elemEnc->offset;
+ return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
}
void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding){
ASSERT(encoding->type==BINARYVAL);
- allocElementConstraintVariables(encoding, getMaximumBitsBinaryValueEncodingVars(encoding));
+ allocElementConstraintVariables(encoding, encoding->numBits);
getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
}
}
uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
- //THIS WILL PROBABLY BE WRONG SINCE THE VALUES CAN BE OFFSET
uint64_t value=0;
for(int i=elemEnc->numVars-1;i>=0;i--) {
value=value<<1;
if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
value |= 1;
}
+ if (elemEnc->isBinaryValSigned &&
+ This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars-1])]) {
+ //Do sign extension of negative number
+ uint64_t highbits=0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+ value+=highbits;
+ }
+ value+=elemEnc->offset;
return value;
}
This->type = type;
}
-uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding) {
- uint64_t max = 0;
- for(uint i=0; i< encoding->encArraySize; i++){
- if(encoding->encodingArray[i]>max)
- max = encoding->encodingArray[i];
- }
- return NUMBITS(max-1);
-}
ElementEncodingType type;
Element * element;
Edge * variables;/* List Variables Used To Encode Element */
- uint64_t * encodingArray; /* List the Variables in the appropriate order */
- uint64_t * inUseArray;/* Bitmap to track variables in use */
- uint encArraySize;
+ union {
+ struct {
+ uint64_t * encodingArray; /* List the Variables in the appropriate order */
+ uint64_t * inUseArray;/* Bitmap to track variables in use */
+ uint encArraySize;
+ };
+ struct {
+ uint64_t offset;/* Value = offset + encoded number (interpretted according to isBinaryValSigned) */
+ uint64_t low;/* Lowest value to encode */
+ uint64_t high;/* High value to encode. If low > high, we assume wrap around to include 0. */
+ uint numBits;
+ bool isBinaryValSigned;
+ };
+ };
uint numVars; /* Number of variables */
};
This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
}
-uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding);
-
#endif