Translating one-item sets by using number of vars

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 8d3d675940d3bca6ebc86653216a5859dd059a72..2693455a0ba0f85da0c731709482c5b2de67d152 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -79,8 +79,6 @@ static inline void setExpanded(Node *n, int isNegated) {
 }
 
 static inline Edge constraintNegate(Edge e) {
-       if(edgeIsNull(e))
-               return e;
        Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
        return enew;
 }

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index ff79d76a8536be3223dd4086f4de2b9174d309c0..5ab535568cb772c0d4f132477545140cde55d381 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -80,7 +80,7 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
        ASSERT(pair->first!= pair->second);
        Edge constraint = getOrderPair(table, pair)->constraint;
-       if(pair->first > pair->second)
+       if(pair->first > pair->second || edgeIsNull(constraint))
                return constraint;
        else
                return constraintNegate(constraint);

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index c16ba491ee2d22318a1eea12546b2f802e13b53d..a72617fda658f8682c1f359c730a06db438f0831 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -3,6 +3,8 @@
 #include "csolver.h"
 #include "satencoder.h"
 #include "set.h"
+#include "order.h"
+#include "orderpair.h"
 
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint index=0;
@@ -48,10 +50,9 @@ uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemE
 }
 
 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
-       Set* set = getElementSet(element);
-       if(getSetSize( set ) ==1)       //case when the set has only one item
-               return getSetElement(set, 0);
        ElementEncoding* elemEnc = getElementEncoding(element);
+       if(elemEnc->numVars == 0)       //case when the set has only one item
+               return getSetElement(getElementSet(element), 0);
        switch(elemEnc->type){
                case ONEHOT:
                        getElementValueOneHotSATTranslator(This, elemEnc);