Adding a new test case for testing FLAGIFFUNDEFINED + bug fixes

[satune.git] / src / Backend / satfunctableencoder.c

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index a4f9a8248dd49334e609bed4185635f7ba760084..c15e822656d64ad7503a454451b1d3bf2a14c492 100644 (file)
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -40,7 +40,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredica
                                row=constraintAND(This->cnf, inputNum, carray);
                                break;
                        case FLAGFORCEUNDEFINED:{
-                               Edge undefConst = ((BooleanVar*)constraint->undefStatus)->var;
+                               Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus);
                                row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst));
                                break;
                        }
@@ -88,7 +88,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
                vals[i]=getSetElement(set, indices[i]);
        }
 
-       Edge undefConstraint = ((BooleanVar*) constraint->undefStatus)->var;
+       Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus);
        
        bool notfinished=true;
        while(notfinished) {
@@ -179,7 +179,7 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction*
                                break;
                        }
                        case FLAGFORCEUNDEFINED: {
-                               Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
+                               Edge undefConst = encodeConstraintSATEncoder(This, func->overflowstatus);
                                row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
                                break;
                        }
@@ -206,7 +206,6 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
        }
 
        FunctionTable* function =(FunctionTable*)elemFunc->function;
-       model_print("undefBehavior: %d\n", function->undefBehavior);
        switch(function->undefBehavior){
                case IGNOREBEHAVIOR:
                case FLAGFORCEUNDEFINED:
@@ -228,8 +227,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
                vals[i]=getSetElement(set, indices[i]);
        }
 
-       Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
-       
+       Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
        bool notfinished=true;
        while(notfinished) {
                Edge carray[numDomains+1];