From: bdemsky <bdemsky@uci.edu>
Date: Tue, 2 Oct 2018 18:00:18 +0000 (-0700)
Subject: Performance improvement
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=dc9528ed1aa556265c68d9f456d00524d74c9e0b;hp=4ecb751464ff6982cf4110da97078ff911da1d90;ds=sidebyside

Performance improvement
---

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0ccf31c..78e797f 100644
--- 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 ff91dc3..c2b9025 100644
--- 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);