From 8f6d5f183512c9623cdebdcc95428a4579833a04 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Fri, 9 Jul 2021 13:32:31 +1000
Subject: [PATCH] Update lexicographic_minimize definition

---
 chapters/5_incremental.tex | 42 +++++++++++++++-----------------------
 1 file changed, 17 insertions(+), 25 deletions(-)

diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex
index d111d76..892da84 100644
--- a/chapters/5_incremental.tex
+++ b/chapters/5_incremental.tex
@@ -205,31 +205,23 @@ It required that, once a solution is found, each subsequent solution must either
 We can model this strategy restarts as such:
 
 \begin{mzn}
-	predicate lex_minimize(array[int] of var int: o) =
-		let {
-			var index_set(o): stage
-			array[index_set(o)] of var int: best;
-		} in if status() = START then
-			stage = min(index_set(o))
-		else
-			if status() = UNSAT then
-				if lastval(stage) < l then
-					stage = lastval(stage) + 1
-				else
-					complete()  % we are finished
-				endif
-			else
-				stage = lastval(stage)
-				/\ best[stage] = sol(_objective)
-			endif
-			/\ for(i in min(index_set(o))..stage-1) (
-				o[i] = lastval(best[i])
-			)
-			/\ if status() = SAT then
-					o[stage] < sol(_objective)
-			endif
-			/\ _objective = o[stage]
-		endif;
+predicate lex_minimize(array[int] of var int: o) =
+	let {
+		var min(index_set(o))..max(index_set(o))+1: stage;
+	} in if status() = START then
+		stage = min(index_set(o))
+	elseif status() = UNSAT then
+		stage = lastval(stage) + 1
+	else /* status() = SAT */
+		stage = lastval(stage)
+		/\ o[stage] < sol(o[stage])
+	endif
+	/\ forall(i in min(index_set(o))..stage-1) (
+		o[i] = sol(o[i])
+	)
+	/\ if stage > max(index_set(o)) then
+		complete()
+	endif;
 \end{mzn}
 
 The lexicographic objective changes the objective at each stage in the evaluation.