From: bdemsky <bdemsky@uci.edu>
Date: Tue, 11 Jul 2017 00:04:23 +0000 (-0700)
Subject: Optimize function for constraint
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=f0dafb2dc6c0047365faaf9ef45af09479d0dc73

Optimize function for constraint
---

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 307114e..935aff9 100644
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -11,6 +11,7 @@
 #define SATSOLVER "sat_solver"
 #include <fcntl.h>
 #include "common.h"
+#include <string.h>
 
 IncrementalSolver * allocIncrementalSolver() {
 	IncrementalSolver *This=(IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
@@ -44,16 +45,25 @@ void addClauseLiteral(IncrementalSolver * This, int literal) {
 }
 
 void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals) {
-	for(uint i=0;i<numliterals; i++) {
-		This->buffer[This->offset++]=literals[i];
-		if (This->offset==IS_BUFFERSIZE) {
+	uint index=0;
+	while(true) {
+		uint bufferspace=IS_BUFFERSIZE-This->offset;
+		uint numtowrite=numliterals-index;
+		if (bufferspace > numtowrite) {
+			memcpy(&This->buffer[This->offset], &literals[index], numtowrite*sizeof(int));
+			This->offset+=numtowrite;
+			This->buffer[This->offset++]=0; //have one extra spot always
+			if (This->offset==IS_BUFFERSIZE) {//Check if full
+				flushBufferSolver(This);
+			}
+			return;
+		} else {
+			memcpy(&This->buffer[This->offset], &literals[index], bufferspace*sizeof(int));
+			This->offset+=bufferspace;
+			index+=bufferspace;
 			flushBufferSolver(This);
 		}
 	}
-	This->buffer[This->offset++]=0;
-	if (This->offset==IS_BUFFERSIZE) {
-		flushBufferSolver(This);
-	}
 }
 
 void finishedClauses(IncrementalSolver * This) {