BUG FIX when there is no usedSettings

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

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 07cfe88bd93e5672c94a729f86e88d2111edd00a..da8955092c11eaa7bff79a51af63224ccc0d58c2 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -9,6 +9,8 @@
 #include "set.h"
 #include "element.h"
 #include "common.h"
+#include "tunable.h"
+#include "csolver.h"
 
 Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
        ASSERT(constraint->predicate->type == TABLEPRED);
@@ -23,7 +25,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
        if (generateNegation)
                polarity = negatePolarity(polarity);
-       if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+       if (undefStatus == SATC_FLAGFORCEUNDEFINED)
                polarity = P_BOTHTRUEFALSE;
 
        Edge constraints[size];
@@ -47,14 +49,18 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
                        row = constraintAND(cnf, inputNum, carray);
                        break;
                case SATC_FLAGFORCEUNDEFINED: {
-                       Edge proxy = constraintNewVar(cnf);
-                       generateProxy(cnf, constraintAND(cnf, inputNum, carray), proxy, P_BOTHTRUEFALSE);
-                       Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
-                       addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy,  constraintNegate(undefConst)));
-                       if (generateNegation == (entry->output != 0)) {
-                               continue;
+                       row = constraintAND(cnf, inputNum, carray);
+                       uint pSize = constraint->parents.getSize();
+                       if (!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)) {
+                               Edge proxy = constraintNewVar(cnf);
+                               generateProxy(cnf, row, proxy, P_BOTHTRUEFALSE);
+                               Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy,  constraintNegate(undefConst)));
+                               if (generateNegation == (entry->output != 0)) {
+                                       continue;
+                               }
+                               row = proxy;
                        }
-                       row = proxy;
                        break;
                }
                default:
@@ -92,12 +98,12 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
                break;
        }
        bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
-       uint numDomains = predicate->table->numDomains();
+       uint numDomains = constraint->inputs.getSize();
 
        if (generateNegation)
                polarity = negatePolarity(polarity);
-       
-        ASSERT(numDomains != 0);
+
+       ASSERT(numDomains != 0);
        VectorEdge *clauses = allocDefVectorEdge();
 
        uint indices[numDomains];       //setup indices
@@ -105,7 +111,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = predicate->table->getDomain(i);
+               Set *set = constraint->inputs.get(i)->getRange();
                vals[i] = set->getElement(indices[i]);
        }
        bool hasOverflow = false;
@@ -159,7 +165,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = predicate->table->getDomain(i);
+                       Set *set = constraint->inputs.get(i)->getRange();
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);
@@ -208,12 +214,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:
@@ -229,7 +243,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
        model_print("Enumeration Table functions ...\n");
 #endif
        ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
-       
+
        //First encode children
        Array<Element *> *elements = &elemFunc->inputs;
        for (uint i = 0; i < elements->getSize(); i++) {
@@ -246,14 +260,14 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                break;
        }
 
-       uint numDomains = function->table->numDomains();
+       uint numDomains = elemFunc->inputs.getSize();
 
        uint indices[numDomains];       //setup indices
        bzero(indices, sizeof(uint) * numDomains);
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = function->table->getDomain(i);
+               Set *set = elemFunc->inputs.get(i)->getRange();
                vals[i] = set->getElement(indices[i]);
        }
 
@@ -274,7 +288,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 +302,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));
                        }
@@ -307,7 +330,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = function->table->getDomain(i);
+                       Set *set = elemFunc->inputs.get(i)->getRange();
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);