From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Fri, 9 Feb 2018 02:22:05 +0000 (-0800)
Subject: Bug Fixes
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=bb457e194713776587cab5987fc418160b406e76

Bug Fixes
---

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 07cfe88..9237ecc 100644
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -208,12 +208,20 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func)
 		Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
 		switch (undefStatus ) {
 		case SATC_IGNOREBEHAVIOR: {
-			addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
+                        if(inputNum == 0){
+                                addConstraintCNF(cnf, output);
+                        }else{
+                                addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
+                        }
 			break;
 		}
 		case SATC_FLAGFORCEUNDEFINED: {
 			Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
-			addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
+                        if(inputNum ==0){
+                                addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
+                        }else{
+                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
+                        }
 			break;
 		}
 		default:
@@ -274,7 +282,11 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 		switch (function->undefBehavior) {
 		case SATC_UNDEFINEDSETSFLAG: {
 			if (isInRange) {
-				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
+                                if(numDomains == 0){
+                                        addConstraintCNF(cnf,carray[numDomains]);
+                                }else{
+                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
+                                }
 			} else {
 				Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
@@ -284,10 +296,15 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 		case SATC_FLAGIFFUNDEFINED: {
 			Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 			if (isInRange) {
-				Edge freshvar = constraintNewVar(cnf);
-				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
-				addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
-				addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
+                                if(numDomains == 0){
+                                        addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
+                                }else{
+                                        Edge freshvar = constraintNewVar(cnf);
+                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
+                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
+                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
+                                }
+				
 			} else {
 				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
 			}