From: bdemsky <bdemsky@uci.edu>
Date: Sun, 9 Jul 2017 07:54:33 +0000 (-0700)
Subject: edits
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=33fe1087d5dd73b5d3417b9b20baec6a8d2cf0a7;p=satune.git

edits
---

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index b2d3ca9..937f7a6 100644
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -17,6 +17,15 @@ void initLitVector(LitVector *This) {
 	This->literals=ourmalloc(This->capacity * sizeof(Literal));
 }
 
+LitVector *cloneLitVector(LitVector *orig) {
+	LitVector *This=ourmalloc(sizeof(LitVector));
+	This->size=orig->size;
+	This->capacity=orig->capacity;
+	This->literals=ourmalloc(This->capacity * sizeof(Literal));
+	memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
+	return This;
+}
+
 void clearLitVector(LitVector *This) {
 	This->size=0;
 }
@@ -114,6 +123,81 @@ void conjoinCNFLit(CNFExpr *This, Literal l) {
 		This->litSize+=getSizeLitVector(&This->singletons);
 }
 
+void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
+	if (destroy) {
+		ourfree(This->singletons.literals);
+		ourfree(This->clauses.array);
+		This->litSize=expr->litSize;
+		This->singletons.literals=expr->singletons.literals;
+		This->singletons.capacity=expr->singletons.capacity;
+		This->clauses.size=expr->clauses.size;
+		This->clauses.array=expr->clauses.array;
+		This->clauses.capacity=expr->clauses.capacity;
+		ourfree(expr);
+	} else {
+		for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+			Literal l=getLiteralLitVector(&expr->singletons,i);
+			addLiteralLitVector(&This->singletons, l);
+		}
+		for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+			LitVector *lv=getVectorLitVector(&expr->clauses,i);
+			pushVectorLitVector(&This->clauses, cloneLitVector(lv));
+		}
+		This->litSize=expr->litSize;
+	}
+}
+
+void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
+	if (expr->litSize==0) {
+		if (!This->isTrue) {
+			clearCNF(This, false);
+		}
+		if (destroy) {
+			deleteCNFExpr(expr);
+		}
+		return;
+	}
+	if (This->litSize==0) {
+		if (This->isTrue) {
+			copyCNF(This, expr, destroy);
+		} else if (destroy) {
+			deleteCNFExpr(expr);
+		}
+		return;
+	}
+	uint litSize=This->litSize;
+	litSize-=getSizeLitVector(&expr->singletons);
+	for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+		Literal l=getLiteralLitVector(&expr->singletons,i);
+		addLiteralLitVector(&This->singletons, l);
+		if (getSizeLitVector(&This->singletons)==0) {
+			//Found conflict...
+			clearCNF(This, false);
+			if (destroy) {
+				deleteCNFExpr(expr);
+			}
+			return;
+		}
+	}
+	litSize+=getSizeLitVector(&expr->singletons);
+	if (destroy) {
+		for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+			LitVector *lv=getVectorLitVector(&expr->clauses,i);
+			litSize+=getSizeLitVector(lv);
+			pushVectorLitVector(&This->clauses, lv);
+		}
+		clearVectorLitVector(&expr->clauses);
+		deleteCNFExpr(expr);
+	} else {
+		for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+			LitVector *lv=getVectorLitVector(&expr->clauses,i);
+			litSize+=getSizeLitVector(lv);
+			pushVectorLitVector(&This->clauses, cloneLitVector(lv));
+		}
+	}
+	This->litSize=litSize;
+}
+
 void disjoinCNFLit(CNFExpr *This, Literal l) {
 	if (This->litSize==0) {
 		if (!This->isTrue) {
@@ -122,6 +206,7 @@ void disjoinCNFLit(CNFExpr *This, Literal l) {
 		}
 		return;
 	}
+
 	uint litSize=0;
 	uint newindex=0;
 	for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
@@ -155,6 +240,15 @@ void disjoinCNFLit(CNFExpr *This, Literal l) {
 	if (hasSameSingleton) {
 		addLiteralLitVector(&This->singletons, l);
 		litSize++;
+	} else if (litSize==0) {
+		This->isTrue=true;//we are true
 	}
 	This->litSize=litSize;
 }
+
+void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
+
+}
+
+
+
diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
index 18f5ff5..db9bbfe 100644
--- a/src/Backend/cnfexpr.h
+++ b/src/Backend/cnfexpr.h
@@ -28,6 +28,7 @@ LitVector * allocLitVector();
 void initLitVector(LitVector *This);
 void clearLitVector(LitVector *This);
 void freeLitVector(LitVector *This);
+LitVector *cloneLitVector(LitVector *orig);
 void deleteLitVector(LitVector *This);
 void addLiteralLitVector(LitVector *This, Literal l);
 Literal getLiteralLitVector(LitVector *This, uint index);
@@ -39,7 +40,7 @@ CNFExpr * allocCNFExprLiteral(Literal l);
 void deleteCNFExpr(CNFExpr *This);
 void clearCNFExpr(CNFExpr *This, bool isTrue);
 
-
+void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
 bool alwaysTrueCNF(CNFExpr * This);
 bool alwaysFalseCNF(CNFExpr * This);
 uint getLitSizeCNF(CNFExpr * This);