Performance improvement

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0ccf31cfcdcb012ee00a533e81e1ed788dfea2c3..78e797ff4f73d28f854cc1084166fff47a890c39 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -44,6 +44,7 @@ private:
        void generateElementEncoding(Element *element);
        Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
        Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+       Edge encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint);
        void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
        Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
        Edge encodeOrderSATEncoder(BooleanOrder *constraint);

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index ff91dc31b20ef41e75c7030601acc55ef8439381..c2b9025f06008d56ec6014c181653a580fc6af8b 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -22,6 +22,63 @@ Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint)
        exit(-1);
 }
 
+Edge SATEncoder::encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint) {
+       Polarity polarity = constraint->polarity;
+
+       /* Call base encoders for children */
+       for (uint i = 0; i < 2; i++) {
+               Element *elem = constraint->inputs.get(i);
+               encodeElementSATEncoder(elem);
+       }
+       VectorEdge *clauses = vector;
+
+       Set *set0 = constraint->inputs.get(0)->getRange();
+       uint size0 = set0->getSize();
+
+       Set *set1 = constraint->inputs.get(1)->getRange();
+       uint size1 = set1->getSize();
+
+       uint64_t val0 = set0->getElement(0);
+       uint64_t val1 = set1->getElement(0);
+       if (size0 != 0 && size1 != 0)
+               for (uint i = 0, j = 0; true; ) {
+                       if (val0 == val1) {
+                               Edge carray[2];
+                               carray[0] = getElementValueConstraint(constraint->inputs.get(0), polarity, val0);
+                               carray[1] = getElementValueConstraint(constraint->inputs.get(1), polarity, val0);
+                               Edge term = constraintAND(cnf, 2, carray);
+                               pushVectorEdge(clauses, term);
+                               i++; j++;
+                               if (i < size0)
+                                       val0 = set0->getElement(i);
+                               else
+                                       break;
+                               if (j < size1)
+                                       val1 = set1->getElement(j);
+                               else
+                                       break;
+                       } else if (val0 < val1) {
+                               i++;
+                               if (i < size0)
+                                       val0 = set0->getElement(i);
+                               else
+                                       break;
+                       } else {
+                               j++;
+                               if (j < size1)
+                                       val1 = set1->getElement(j);
+                               else
+                                       break;
+                       }
+               }
+       if (getSizeVectorEdge(clauses) == 0) {
+               return E_False;
+       }
+       Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       clearVectorEdge(clauses);
+       return cor;
+}
+
 Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
        PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
        uint numDomains = constraint->inputs.getSize();
@@ -31,6 +88,9 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
        if (generateNegation)
                polarity = negatePolarity(polarity);
 
+       if (!generateNegation && predicate->getOp() == SATC_EQUALS)
+               return encodeEnumEqualsPredicateSATEncoder(constraint);
+
        /* Call base encoders for children */
        for (uint i = 0; i < numDomains; i++) {
                Element *elem = constraint->inputs.get(i);