From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 18 Jul 2017 00:19:15 +0000 (-0700)
Subject: Translating one-item sets by using number of vars
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1ffeb0dd90e64db8118e8953f9573f16d3de50dd;p=satune.git

Translating one-item sets by using number of vars
---

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 8d3d675..2693455 100644
--- 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 ff79d76..5ab5355 100644
--- 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 c16ba49..a72617f 100644
--- 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);