Handle sets of 1

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 4f22ba02d59c1bd72403e31df1fad213a9728ab1..5a47435dcda90adf0205bd02b62eac8f8a77c13b 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -31,10 +31,10 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint
        ElementEncoding* elemEnc = getElementEncoding(elem);
        for(uint i=0; i<elemEnc->encArraySize; i++){
                if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
-                       return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
+                       return (elemEnc->numVars == 0) ? E_True: generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
                }
        }
-       return E_BOGUS;
+       return E_False;
 }
 
 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value) {

diff --git a/src/common.h b/src/common.h
index 5d8c389710200942c30681065f12a367696d430a..a06dab21eb16ffc9a5a5ba8aad3304dcda457cb2 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -32,7 +32,7 @@ extern int switch_alloc;
 
 #define model_print printf
 
-#define NEXTPOW2(x) (1<<(sizeof(uint)*8-__builtin_clz(x-1)))
+#define NEXTPOW2(x) ((x==1) ? 1 : (1<<(sizeof(uint)*8-__builtin_clz(x-1))))
 #define NUMBITS(x) ((x==0) ? 0 : 8*sizeof(x)-__builtin_clz(x))
 
 #ifdef CONFIG_DEBUG