X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=71205f68aab557baf933689510435ee4f312d328;hp=d316724791f2648aa332e989d6a3507d99b8c0aa;hb=44ac39afe074506f18b8d2c29430cc7d88ace944;hpb=747484c9f7ce17d58e4084730c0683f392b19dee

diff --git a/src/csolver.cc b/src/csolver.cc
index d316724..71205f6 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -66,7 +66,6 @@ CSolver::~CSolver() {
 	for (uint i = 0; i < size; i++) {
 		delete allOrders.get(i);
 	}
-
 	size = allFunctions.getSize();
 	for (uint i = 0; i < size; i++) {
 		delete allFunctions.get(i);
@@ -175,6 +174,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
 	}
 }
 
+
 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
 	Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
 	Element *e = elemMap.get(element);
@@ -311,13 +311,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 	}
 	case SATC_IFF: {
 		for (uint i = 0; i < 2; i++) {
-			if (array[i]->type == BOOLCONST) {
-				if (isTrue(array[i])) {	// It can be undefined
-					return array[1 - i];
-				} else if (isFalse(array[i])) {
-					newarray[0] = array[1 - i];
-					return applyLogicalOperation(SATC_NOT, newarray, 1);
-				}
+			if (isTrue(array[i])) {	// It can be undefined
+				return array[1 - i];
+			} else if (isFalse(array[i])) {
+				newarray[0] = array[1 - i];
+				return applyLogicalOperation(SATC_NOT, newarray, 1);
 			} else if (array[i]->type == LOGICOP) {
 				BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
 				if (b->replaced) {
@@ -341,12 +339,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 				if (((BooleanLogic *)b.getBoolean())->replaced)
 					return rewriteLogicalOperation(op, array, asize);
 			}
-			if (b->type == BOOLCONST) {
-				if (isTrue(b))
-					continue;
-				else {
-					return boolFalse;
-				}
+			if (isTrue(b))
+				continue;
+			else if (isFalse(b)) {
+				return boolFalse;
 			} else
 				newarray[newindex++] = b;
 		}
@@ -389,7 +385,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 	//	ASSERT(first != second);
 	if (first == second)
 		return getBooleanFalse();
-	
+
 	bool negate = false;
 	if (order->type == SATC_TOTAL) {
 		if (first > second) {
@@ -510,7 +506,6 @@ void CSolver::printConstraints() {
 		model_print("\n");
 	}
 	delete it;
-
 }
 
 void CSolver::printConstraint(BooleanEdge b) {