X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Finc_solver.c;h=b9cc549fdbf30dc3fa408b008d8f24ec63db8ade;hb=f83b458891ec481c524ee439b296f92fbb3b407d;hp=5e1ed548ab31e487d958bc1fb293c840ffc0533b;hpb=561b93dec85db0c90426345c0dc669fe3de2d4f7;p=satune.git

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 5e1ed54..b9cc549 100644
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -42,6 +42,15 @@ 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) {
+			flushBufferSolver(This);
+		}
+	}
+}
+
 void finishedClauses(IncrementalSolver * This) {
 	addClauseLiteral(This, 0);
 }