From: bdemsky <bdemsky@uci.edu>
Date: Tue, 24 Jul 2018 18:33:50 +0000 (-0700)
Subject: more code
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=dea71d97549f037bd9b098b8abb121f02c6ba9df

more code
---

diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
index 5fa38e6..c9ccc44 100755
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -17,13 +17,18 @@ ElementOpt::~ElementOpt() {
 void ElementOpt::doTransform() {
 	if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
 		return;
-
-	BooleanIterator bit(solver);
-	while (bit.hasNext()) {
-		Boolean *b = bit.next();
-		if (b->type == PREDICATEOP)
-			processPredicate((BooleanPredicate *)b);
+	
+	SetIteratorBooleanEdge *iterator = solver->getConstraints();
+	while (iterator->hasNext()) {
+		BooleanEdge constraint = iterator->next();
+		if (constraint->type == PREDICATEOP)
+			workList.push((BooleanPredicate *)constraint.getBoolean());
+	}
+	while (workList.getSize() != 0) {
+		BooleanPredicate * pred = workList.last(); workList.pop();
+		processPredicate(pred);
 	}
+	delete iterator;
 }
 
 void ElementOpt::processPredicate(BooleanPredicate * pred) {
@@ -42,10 +47,51 @@ void ElementOpt::processPredicate(BooleanPredicate * pred) {
 	Element * right = pred->inputs.get(1);
 
 	if (left->type == ELEMCONST) {
+		Element * tmp = left;
+		left = right;
+		right = tmp;
+		op = flipOp(op);
+	} else if (right->type != ELEMCONST)
+		return;
 
-	} else if (right->type == ELEMCONST) {
-
-	} else {
+	if (left->type !=ELEMSET)
 		return;
+	
+	if (op == SATC_EQUALS) {
+		handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
+	} else {
+		handlePredicateInequality(pred, (ElementSet *) left, (ElementConst *) right);
+	}
+}
+
+void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
+	if (pred->isTrue()) {
+		replaceVarWithConst(pred, left, right);
+	} else if (pred->isFalse()) {
+		
+	} else ASSERT(0);
+}
+
+void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right) {
+
+}
+
+void ElementOpt::replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value) {
+	uint size = var->parents.getSize();
+	for(uint i=0; i < size; i++) {
+		ASTNode * parent = var->parents.get(i);
+		if (parent->type == PREDICATEOP && pred != parent) {
+			BooleanPredicate * newpred = (BooleanPredicate *) parent;
+			for(uint j=0; j < newpred->inputs.getSize(); j++) {
+				Element * e = newpred->inputs.get(j);
+				if (e == var) {
+					solver->boolMap.remove(newpred);
+					newpred->inputs.set(j, value);
+					solver->boolMap.put(newpred, newpred);
+					workList.push(newpred);
+					break;
+				}
+			}
+		}
 	}
 }
diff --git a/src/ASTTransform/elementopt.h b/src/ASTTransform/elementopt.h
index ad6e790..980bb87 100755
--- a/src/ASTTransform/elementopt.h
+++ b/src/ASTTransform/elementopt.h
@@ -12,6 +12,10 @@ public:
 	CMEMALLOC;
 private:
 	void processPredicate(BooleanPredicate *);
+	void handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
+	void handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
+	void replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value);
+	Vector<BooleanPredicate *> workList;
 };
 
 #endif
diff --git a/src/csolver.h b/src/csolver.h
index e02e340..044f79e 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -57,7 +57,7 @@ public:
 
 	Set *getElementRange (Element *element);
 
-        void mustHaveValue(Element *element);
+	void mustHaveValue(Element *element);
         
 	BooleanEdge getBooleanTrue();
 
@@ -159,7 +159,6 @@ public:
 	void replaceBooleanWithFalse(BooleanEdge bexpr);
 	void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
 	CSolver *clone();
-//        Set* addItemsToRange(Element* element, uint num, ...);
 	void serialize();
 	static CSolver *deserialize(const char *file);
 	void autoTune(uint budget);
@@ -220,5 +219,22 @@ private:
 	bool unsat;
 	Tuner *tuner;
 	long long elapsedTime;
+	friend class ElementOpt;
 };
+
+inline CompOp flipOp(CompOp op) {
+	switch (op) {
+	case SATC_EQUALS:
+		return SATC_EQUALS;
+	case SATC_LT:
+		return SATC_GT;
+	case SATC_GT:
+		return SATC_LT;
+	case SATC_LTE:
+		return SATC_GTE;
+	case SATC_GTE:
+		return SATC_LTE;
+	}
+	ASSERT(0);
+}
 #endif