X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;h=c3208b91ec5fdd2747ffc763fa3e3b52dd60291a;hb=f9546315ab6ece42f48fa8b2e2e53abcd1f00b74;hp=0270758af28faa087efc0d2f2cc358e15a221d53;hpb=28703eaeadb4b35e607a1d4441b31729177feb19;p=satune.git

diff --git a/src/csolver.cc b/src/csolver.cc
index 0270758..c3208b9 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -11,10 +11,13 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "transformer.h"
+#include "decomposeordertransform.h"
 #include "autotuner.h"
 #include "astops.h"
 #include "structs.h"
+#include "orderresolver.h"
+#include "integerencoding.h"
+#include <stdlib.h>
 
 CSolver::CSolver() :
 	boolTrue(new BooleanConst(true)),
@@ -24,7 +27,6 @@ CSolver::CSolver() :
 	elapsedTime(0)
 {
 	satEncoder = new SATEncoder(this);
-	transformer = new Transformer(this);
 }
 
 /** This function tears down the solver and the entire AST */
@@ -68,7 +70,6 @@ CSolver::~CSolver() {
 	delete boolTrue;
 	delete boolFalse;
 	delete satEncoder;
-	delete transformer;
 }
 
 CSolver *CSolver::clone() {
@@ -210,7 +211,7 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu
 
 Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
 	BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
-	Boolean * b = boolMap.get(boolean);
+	Boolean *b = boolMap.get(boolean);
 	if (b == NULL) {
 		boolMap.put(boolean, boolean);
 		allBooleans.push(boolean);
@@ -229,22 +230,32 @@ bool CSolver::isFalse(Boolean *b) {
 	return b->isFalse();
 }
 
-Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2) {
-	Boolean * array[] = {arg1, arg2};
+Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) {
+	Boolean *array[] = {arg1, arg2};
 	return applyLogicalOperation(op, array, 2);
 }
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) {
-	Boolean * array[] = {arg};
+	Boolean *array[] = {arg};
 	return applyLogicalOperation(op, array, 1);
 }
 
+static int ptrcompares(const void *p1, const void *p2) {
+	uintptr_t b1 = *(uintptr_t const *) p1;
+  uintptr_t b2 = *(uintptr_t const *) p2;
+	if (b1 < b2)
+		return -1;
+	else if (b1 == b2)
+		return 0;
+	else
+		return 1;
+}
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
-	Boolean * newarray[asize];
-	switch(op) {
+	Boolean *newarray[asize];
+	switch (op) {
 	case SATC_NOT: {
-		if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) {
+		if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) {
 			return ((BooleanLogic *) array[0])->inputs.get(0);
 		} else if (array[0]->type == BOOLCONST) {
 			return array[0]->isTrue() ? boolFalse : boolTrue;
@@ -252,108 +263,64 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
 		break;
 	}
 	case SATC_IFF: {
-		for(uint i=0;i<2;i++) {
+		for (uint i = 0; i < 2; i++) {
 			if (array[i]->type == BOOLCONST) {
 				if (array[i]->isTrue()) {
-					return array[1-i];
+					return array[1 - i];
 				} else {
-					newarray[0]=array[1-i];
+					newarray[0] = array[1 - i];
 					return applyLogicalOperation(SATC_NOT, newarray, 1);
 				}
 			}
 		}
 		break;
 	}
-	case SATC_XOR: {
-		for(uint i=0;i<2;i++) {
-			if (array[i]->type == BOOLCONST) {
-				if (array[i]->isTrue()) {
-					newarray[0]=array[1-i];
-					return applyLogicalOperation(SATC_NOT, newarray, 1);
-				} else
-					return array[1-i];
-			}
-		}
-		break;
-	}
 	case SATC_OR: {
-		uint newindex=0;
-		for(uint i=0;i<asize;i++) {
-			Boolean *b=array[i];
-			if (b->type == BOOLCONST) {
-				if (b->isTrue())
-					return b;
-				else
-					continue;
-			} else
-				newarray[newindex++]=b;
-		}
-		if (newindex==1)
-			return newarray[0];
-		else if (newindex == 2) {
-			bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT;
-			bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT;
-
-			if (isNot0 != isNot1) {
-				if (isNot0) {
-					newarray[0] = ((BooleanLogic *) newarray[0])->inputs.get(0);
-				} else {
-					Boolean *tmp =  ((BooleanLogic *) array[1])->inputs.get(0);
-					array[1] = array[0];
-					array[0] = tmp;
-				}
-				return applyLogicalOperation(SATC_IMPLIES, newarray, 2);
-			}
-		} else {
-			array = newarray;
-			asize = newindex;
+		for (uint i =0; i <asize; i++) {
+			newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
 		}
-		break;
+		return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
 	}
 	case SATC_AND: {
-		uint newindex=0;
-		for(uint i=0;i<asize;i++) {
-			Boolean *b=array[i];
+		uint newindex = 0;
+		for (uint i = 0; i < asize; i++) {
+			Boolean *b = array[i];
 			if (b->type == BOOLCONST) {
 				if (b->isTrue())
 					continue;
 				else
-					return b;
+					return boolFalse;
 			} else
-				newarray[newindex++]=b;
+				newarray[newindex++] = b;
 		}
-		if(newindex==1) {
+		if (newindex == 0) {
+			return boolTrue;
+		} else if (newindex == 1) {
 			return newarray[0];
 		} else {
+			qsort(newarray, asize, sizeof(Boolean *), ptrcompares);
 			array = newarray;
 			asize = newindex;
 		}
 		break;
 	}
+	case SATC_XOR: {
+		//handle by translation
+		return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
+	}
 	case SATC_IMPLIES: {
-		if (array[0]->type == BOOLCONST) {
-			if (array[0]->isTrue()) {
-				return array[1];
-			} else {
-				return boolTrue;
-			}
-		} else if (array[1]->type == BOOLCONST) {
-			if (array[1]->isTrue()) {
-				return array[1];
-			} else {
-				return applyLogicalOperation(SATC_NOT, array, 1);
-			}
-		}
-		break;
+		//handle by translation
+		return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
 	}
 	}
-	
+
+	ASSERT(asize != 0);
 	Boolean *boolean = new BooleanLogic(this, op, array, asize);
 	Boolean *b = boolMap.get(boolean);
 	if (b == NULL) {
 		boolMap.put(boolean, boolean);
 		allBooleans.push(boolean);
-		return boolean;		
+		return boolean;
 	} else {
 		delete boolean;
 		return b;
@@ -371,13 +338,25 @@ void CSolver::addConstraint(Boolean *constraint) {
 		return;
 	else if (constraint == boolFalse)
 		setUnSAT();
-	else
+	else {
+		if (constraint->type == LOGICOP) {
+			BooleanLogic *b=(BooleanLogic *) constraint;
+			if (b->op==SATC_AND) {
+				for(uint i=0;i<b->inputs.getSize();i++) {
+					addConstraint(b->inputs.get(i));
+				}
+				return;
+			}
+		}
+
 		constraints.add(constraint);
+	}
 }
 
 Order *CSolver::createOrder(OrderType type, Set *set) {
 	Order *order = new Order(type, set);
 	allOrders.push(order);
+	activeOrders.add(order);
 	return order;
 }
 
@@ -387,10 +366,17 @@ int CSolver::solve() {
 		tuner = new DefaultTuner();
 		deleteTuner = true;
 	}
-		
+
 	long long startTime = getTimeNano();
 	computePolarities(this);
-	transformer->orderAnalysis();
+
+	DecomposeOrderTransform dot(this);
+	dot.doTransform();
+
+	//This leaks like crazy
+	//	IntegerEncodingTransform iet(this);
+	//iet.doTransform();
+
 	naiveEncodingDecision(this);
 	satEncoder->encodeAllSATEncoder(this);
 	int result = unsat ? IS_UNSAT : satEncoder->solve();
@@ -425,8 +411,8 @@ bool CSolver::getBooleanValue(Boolean *boolean) {
 	exit(-1);
 }
 
-HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
-	return getOrderConstraintValueSATTranslator(this, order, first, second);
+bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
+	return order->encoding.resolver->resolveOrder(first, second);
 }
 
 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
@@ -434,7 +420,7 @@ long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
 
 void CSolver::autoTune(uint budget) {
-	AutoTuner * autotuner=new AutoTuner(budget);
+	AutoTuner *autotuner = new AutoTuner(budget);
 	autotuner->addProblem(this);
 	autotuner->tune();
 	delete autotuner;