X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fconstraint.cc;h=7c3a094701d3c12ffa08d5a3fba5c83dd6b3f4d8;hp=df812dfe682918e3132ff3c2c1c6e71784cbbbd0;hb=0703630a40f4fcfd8c8dcad336472907f125c86c;hpb=7c10dbd982d74cf1e96c06b3078e329c62e6a3e8

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index df812df..7c3a094 100644
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -4,6 +4,7 @@
 #include "inc_solver.h"
 #include "cnfexpr.h"
 #include "common.h"
+#include "qsort.h"
 /*
    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
@@ -59,6 +60,8 @@ CNF *createCNF() {
 	initDefVectorEdge(&cnf->constraints);
 	initDefVectorEdge(&cnf->args);
 	cnf->solver = allocIncrementalSolver();
+	cnf->solveTime = 0;
+	cnf->encodeTime = 0;
 	return cnf;
 }
 
@@ -82,6 +85,8 @@ void resizeCNF(CNF *cnf, uint newCapacity) {
 	uint newMask = newCapacity - 1;
 	for (uint i = 0; i < oldCapacity; i++) {
 		Node *n = old_array[i];
+		if (n == NULL)
+			continue;
 		uint hashCode = n->hashCode;
 		uint newindex = hashCode & newMask;
 		for (;; newindex = (newindex + 1) & newMask) {
@@ -135,6 +140,7 @@ Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
 		}
 	}
 	*n_ptr = allocNode(type, numEdges, edges, hashvalue);
+	cnf->size++;
 	Edge e = {*n_ptr};
 	return e;
 }
@@ -182,7 +188,7 @@ int comparefunction(const Edge *e1, const Edge *e2) {
 
 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
 	ASSERT(numEdges != 0);
-	qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
+	bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
 	uint initindex = 0;
 	while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
 		initindex++;
@@ -316,9 +322,11 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 
 void addConstraintCNF(CNF *cnf, Edge constraint) {
 	pushVectorEdge(&cnf->constraints, constraint);
-	model_print("****ADDING NEW Constraint*****\n");
+#ifdef CONFIG_DEBUG
+	model_print("****SATC_ADDING NEW Constraint*****\n");
 	printCNF(constraint);
 	model_print("\n******************************\n");
+#endif
 }
 
 Edge constraintNewVar(CNF *cnf) {
@@ -328,10 +336,16 @@ Edge constraintNewVar(CNF *cnf) {
 }
 
 int solveCNF(CNF *cnf) {
+	long long startTime = getTimeNano();
 	countPass(cnf);
 	convertPass(cnf, false);
 	finishedClauses(cnf->solver);
-	return solve(cnf->solver);
+	long long startSolve = getTimeNano();
+	int result = solve(cnf->solver);
+	long long finishTime = getTimeNano();
+	cnf->encodeTime = startSolve - startTime;
+	cnf->solveTime = finishTime - startSolve;
+	return result;
 }
 
 bool getValueCNF(CNF *cnf, Edge var) {
@@ -826,8 +840,8 @@ CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
 				int eL = argExp->litSize;			// lits in argument
 				int aC = getClauseSizeCNF(accum);		// clauses in accum
 				int eC = getClauseSizeCNF(argExp);	// clauses in argument
-
-				if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
+				//POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
+				if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
 					disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
 				} else {
 					disjoinCNFExpr(accum, argExp, destroy);
@@ -885,26 +899,26 @@ Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 	return constraintAND(cnf, numvars, array);
 }
 
-Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
-	if(numvars == 0 )
+Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+	if (numvars == 0 )
 		return E_False;
-	Edge result =constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
+	Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
 	for (uint i = 1; i < numvars; i++) {
 		Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
-		Edge eq	= constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); 
-		result = constraintOR2(cnf, lt, eq); 
+		Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+		result = constraintOR2(cnf, lt, eq);
 	}
 	return result;
 }
 
-Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
-	if(numvars == 0 )
+Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+	if (numvars == 0 )
 		return E_True;
-	Edge result =constraintIMPLIES(cnf, var1[0], var2[0]);
+	Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
 	for (uint i = 1; i < numvars; i++) {
 		Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
-		Edge eq	= constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); 
-		result = constraintOR2(cnf, lt, eq); 
+		Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+		result = constraintOR2(cnf, lt, eq);
 	}
 	return result;
 }