Bug Fixes

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 07cfe88bd93e5672c94a729f86e88d2111edd00a..9237eccb2cfded8de3f999f7e4277f523f49e675 100644 (file)
--- 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: {
                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);
                        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:
                        break;
                }
                default:


@@ -274,7 +282,11 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                switch (function->undefBehavior) {
                case SATC_UNDEFINEDSETSFLAG: {
                        if (isInRange) {
                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));
                        } 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) {
                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));
                        }
                        } else {
                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
                        }