Performance improvements to incremental invariant generation

.gitignore

@@ -1 +1,5 @@
 bin
+*.xml
+*.yc_base
+*.yc_induct
+*.yc_inv

src/jkind/processes/InvariantProcess.java

@@ -46,8 +46,7 @@ public void main() {
 			debug("No invariants proposed");
 			return;
 		}
-
-		assertInductiveTransition(0);
+
 		for (int k = 1; k <= kMax; k++) {
 			debug("K = " + k);
 
@@ -77,40 +76,39 @@ private void defineCandidates(List<Candidate> candidates) {
 		}
 	}
 
-	private void assertInductiveTransition(int k) {
-		solver.send(new Cons("assert", new Cons(Keywords.T, getInductiveIndex(k))));
-	}
-
-	private Sexp getInductiveIndex(int offset) {
-		return new Cons("+", Keywords.N, Sexp.fromInt(offset));
-	}
-
-	private boolean refineBaseStep(int k, Graph graph) {
+	private void refineBaseStep(int k, Graph graph) {
+		solver.push();
 		SolverResult result;
-		boolean refined = false;
+
+		for (int i = 0; i < k; i++) {
+			assertBaseTransition(i);
+		}
 
 		do {
-			result = solver.query(getBaseQuery(k, graph));
+			result = solver.query(graph.toInvariant(Sexp.fromInt(k - 1)));
 
-			if (result.getResult() == Result.SAT) {
-				refined = true;
+			if (result.getResult() == Result.SAT) {
 				graph.refine(result.getModel(), BigInteger.valueOf(k - 1));
 				debug("Base step refinement, graph size = " + graph.size());
 			}
 		} while (!graph.isTrivial() && result.getResult() == Result.SAT);
-
-		return refined;
+		
+		solver.pop();
 	}
 
-	private Sexp getBaseQuery(int k, Graph graph) {
-		Sexp inv = graph.toInvariant(Sexp.fromInt(k - 1));
-		return new Cons("=>", new Cons("=", Keywords.N, Sexp.fromInt(k - 1)), inv);
+	private void assertBaseTransition(int i) {
+		solver.send(new Cons("assert", new Cons(Keywords.T, Sexp.fromInt(i))));
 	}
 
 	private Graph refineInductiveStep(int k, Graph original) {
+		solver.push();
 		Graph graph = new Graph(original);
 		SolverResult result;
 
+		for (int i = 0; i <= k; i++) {
+			assertInductiveTransition(i);
+		}
+
 		do {
 			result = solver.query(getInductiveQuery(k, graph));
 
@@ -122,9 +120,18 @@ private Graph refineInductiveStep(int k, Graph original) {
 			}
 		} while (!graph.isTrivial() && result.getResult() != Result.UNSAT);
 
+		solver.pop();
 		return graph;
 	}
 
+	private void assertInductiveTransition(int k) {
+		solver.send(new Cons("assert", new Cons(Keywords.T, getInductiveIndex(k))));
+	}
+
+	private Sexp getInductiveIndex(int offset) {
+		return new Cons("+", Keywords.N, Sexp.fromInt(offset));
+	}
+
 	private BigInteger getN(Model model) {
 		NumericValue value = (NumericValue) model.getValue(Keywords.N);
 		return new BigInteger(value.toString());