X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;h=592d1d51baf89e7c8f6b4a3d043ea4b07604be34;hb=0703630a40f4fcfd8c8dcad336472907f125c86c;hp=8ea79e439069e0ccb5baac8d0028c82fbdf9793b;hpb=16486cd2b25f9fc04819e811d519947704679bed;p=satune.git

diff --git a/src/csolver.cc b/src/csolver.cc
index 8ea79e4..592d1d5 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -118,6 +118,10 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
 	return set;
 }
 
+VarType CSolver::getSetVarType(Set *set){
+	return set->getType();
+}
+
 Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
 	Set *s = createRangeSet(type, lowrange, highrange);
 	return getElementVar(s);
@@ -149,6 +153,11 @@ Element *CSolver::getElementVar(Set *set) {
 	return element;
 }
 
+Set* CSolver::getElementRange (Element* element){
+	return element->getRange();
+}
+
+
 Element *CSolver::getElementConst(VarType type, uint64_t value) {
 	uint64_t array[] = {value};
 	Set *set = new Set(type, array, 1);
@@ -251,11 +260,11 @@ BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs,
 }
 
 bool CSolver::isTrue(BooleanEdge b) {
-	return b.isNegated()?b->isFalse():b->isTrue();
+        return b.isNegated()?b->isFalse():b->isTrue();
 }
 
 bool CSolver::isFalse(BooleanEdge b) {
-	return b.isNegated()?b->isTrue():b->isFalse();
+        return b.isNegated()?b->isTrue():b->isFalse();
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
@@ -303,9 +312,9 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 	case SATC_IFF: {
 		for (uint i = 0; i < 2; i++) {
 			if (array[i]->type == BOOLCONST) {
-				if (array[i]->isTrue()) {
+				if (isTrue(array[i])) { // It can be undefined
 					return array[1 - i];
-				} else {
+				} else if(isFalse(array[i])) {
 					newarray[0] = array[1 - i];
 					return applyLogicalOperation(SATC_NOT, newarray, 1);
 				}
@@ -333,10 +342,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 					return rewriteLogicalOperation(op, array, asize);
 			}
 			if (b->type == BOOLCONST) {
-				if (b->isTrue())
+				if (isTrue(b))
 					continue;
-				else
+				else{
 					return boolFalse;
+                                }
 			} else
 				newarray[newindex++] = b;
 		}
@@ -371,21 +381,27 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 		return BooleanEdge(boolean);
 	} else {
 		delete boolean;
-		return BooleanEdge(b);
+		return BooleanEdge(boolean);
 	}
 }
 
 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
+	ASSERT(first != second);
 	Boolean *constraint = new BooleanOrder(order, first, second);
 	allBooleans.push(constraint);
 	return BooleanEdge(constraint);
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
+	if(constraint.isNegated())
+		model_print("!");
+	constraint.getBoolean()->print();
 	if (isTrue(constraint))
 		return;
-	else if (isFalse(constraint))
+	else if (isFalse(constraint)) {
+		int t=0;
 		setUnSAT();
+	}
 	else {
 		if (constraint->type == LOGICOP) {
 			BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
@@ -405,8 +421,9 @@ void CSolver::addConstraint(BooleanEdge constraint) {
 		constraints.add(constraint);
 		Boolean *ptr=constraint.getBoolean();
 		
-		if (ptr->boolVal == BV_UNSAT)
+		if (ptr->boolVal == BV_UNSAT) {
 			setUnSAT();
+		}
 		
 		replaceBooleanWithTrueNoRemove(constraint);
 		constraint->parents.clear();
@@ -445,7 +462,9 @@ int CSolver::solve() {
 	
 	naiveEncodingDecision(this);
 	satEncoder->encodeAllSATEncoder(this);
+        model_print("Is problem UNSAT after encoding: %d\n", unsat);
 	int result = unsat ? IS_UNSAT : satEncoder->solve();
+        model_print("Result Computed in CSolver: %d\n", result);
 	long long finishTime = getTimeNano();
 	elapsedTime = finishTime - startTime;
 	if (deleteTuner) {