edit

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

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 7e6a67d239def78348bb3d4443b1a683735e4354..1fea1a58f41ebf23391bba824a6744bc84662ae8 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -25,16 +25,18 @@ Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint)
 Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
        PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
        uint numDomains = predicate->domains.getSize();
-
+       Polarity polarity = constraint->polarity;
        FunctionEncodingType encType = constraint->encoding.type;
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+       if (generateNegation)
+               polarity = negatePolarity(polarity);
 
        /* Call base encoders for children */
        for (uint i = 0; i < numDomains; i++) {
                Element *elem = constraint->inputs.get(i);
                encodeElementSATEncoder(elem);
        }
-       VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
+       VectorEdge *clauses = vector;
 
        uint indices[numDomains];       //setup indices
        bzero(indices, sizeof(uint) * numDomains);
@@ -46,17 +48,17 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
        }
 
        bool notfinished = true;
+        Edge carray[numDomains];
        while (notfinished) {
-               Edge carray[numDomains];
-
                if (predicate->evalPredicateOperator(vals) != generateNegation) {
                        //Include this in the set of terms
                        for (uint i = 0; i < numDomains; i++) {
                                Element *elem = constraint->inputs.get(i);
-                               carray[i] = getElementValueConstraint(elem, vals[i]);
+                               carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
                        }
                        Edge term = constraintAND(cnf, numDomains, carray);
                        pushVectorEdge(clauses, term);
+                       ASSERT(getSizeVectorEdge(clauses) > 0);
                }
 
                notfinished = false;
@@ -75,11 +77,10 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
                }
        }
        if (getSizeVectorEdge(clauses) == 0) {
-               deleteVectorEdge(clauses);
                return E_False;
        }
        Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       deleteVectorEdge(clauses);
+       clearVectorEdge(clauses);
        return generateNegation ? constraintNegate(cor) : cor;
 }
 
@@ -108,12 +109,9 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                vals[i] = set->getElement(indices[i]);
        }
 
-       Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
-
        bool notfinished = true;
+        Edge carray[numDomains + 1];
        while (notfinished) {
-               Edge carray[numDomains + 1];
-
                uint64_t result = function->applyFunctionOperator(numDomains, vals);
                bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
                bool needClause = isInRange;
@@ -125,10 +123,10 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                        //Include this in the set of terms
                        for (uint i = 0; i < numDomains; i++) {
                                Element *elem = func->inputs.get(i);
-                               carray[i] = getElementValueConstraint(elem, vals[i]);
+                               carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
                        }
                        if (isInRange) {
-                               carray[numDomains] = getElementValueConstraint(func, result);
+                               carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
                        }
 
                        Edge clause;
@@ -140,6 +138,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                                break;
                        }
                        case SATC_FLAGFORCESOVERFLOW: {
+                               Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
                                clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                break;
                        }
@@ -147,11 +146,13 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                                if (isInRange) {
                                        clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                                } else {
+                                       Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
                                        clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
                                }
                                break;
                        }
                        case SATC_FLAGIFFOVERFLOW: {
+                               Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
                                if (isInRange) {
                                        clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                } else {
@@ -189,8 +190,8 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                deleteVectorEdge(clauses);
                return;
        }
-       Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       addConstraintCNF(cnf, cor);
+       Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       addConstraintCNF(cnf, cand);
        deleteVectorEdge(clauses);
 }
 
@@ -200,11 +201,11 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
        encodeElementSATEncoder(elem0);
        Element *elem1 = constraint->inputs.get(1);
        encodeElementSATEncoder(elem1);
-       ElementEncoding *ee0 = getElementEncoding(elem0);
-       ElementEncoding *ee1 = getElementEncoding(elem1);
+       ElementEncoding *ee0 = elem0->getElementEncoding();
+       ElementEncoding *ee1 = elem1->getElementEncoding();
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
-       switch (predicate->op) {
+       switch (predicate->getOp()) {
        case SATC_EQUALS:
                return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
        case SATC_LT: