Several speed optimizations

git-svn-id: svn://sunsvr01.isp.uni-luebeck.de/swproj13/trunk@438 72836036-5685-4462-b002-a69064685172

9 files changed, 129 insertions, 83 deletions

diff --git a/src/jrummikub/ai/TurnLogic.java b/src/jrummikub/ai/TurnLogic.java
index dcb95fc..1ce752c 100644
--- a/src/jrummikub/ai/TurnLogic.java
+++ b/src/jrummikub/ai/TurnLogic.java
@@ -1,5 +1,15 @@
 package jrummikub.ai;
 
+import static jrummikub.ai.fdsolver.Constraints.constant;
+import static jrummikub.ai.fdsolver.Constraints.index;
+import static jrummikub.ai.fdsolver.Constraints.lessThan;
+import static jrummikub.ai.fdsolver.Constraints.lessThanEq;
+import static jrummikub.ai.fdsolver.Constraints.offset;
+import static jrummikub.ai.fdsolver.Constraints.same;
+import static jrummikub.ai.fdsolver.Constraints.sum;
+import static jrummikub.ai.fdsolver.Constraints.unless;
+import static jrummikub.ai.fdsolver.Constraints.when;
+
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.HashSet;
@@ -9,13 +19,9 @@ import java.util.Set;
 import jrummikub.ai.fdsolver.Constraint;
 import jrummikub.ai.fdsolver.Solver;
 import jrummikub.ai.fdsolver.Var;
-import jrummikub.ai.fdsolver.constraint.IfConstraint;
-import jrummikub.ai.fdsolver.constraint.IndexConstraint;
-import jrummikub.ai.fdsolver.constraint.LessThan;
 import jrummikub.model.GameSettings;
 import jrummikub.model.Stone;
 import jrummikub.model.StoneColor;
-import static jrummikub.ai.fdsolver.Constraints.*;
 
 /**
  * Provides Humanlike Advanced Logic (HAL) that models the options given to a
diff --git a/src/jrummikub/ai/fdsolver/Constraint.java b/src/jrummikub/ai/fdsolver/Constraint.java
index b081d4b..a046324 100644
--- a/src/jrummikub/ai/fdsolver/Constraint.java
+++ b/src/jrummikub/ai/fdsolver/Constraint.java
@@ -10,4 +10,8 @@ public abstract class Constraint {
 	public abstract Collection<Propagator> getPropagators(boolean negate);
 
 	public abstract Satisfiability getSatisfiability();
+	
+	public boolean isSatisfiable() {
+		return getSatisfiability() != Satisfiability.UNSAT;
+	}
 }
diff --git a/src/jrummikub/ai/fdsolver/Solver.java b/src/jrummikub/ai/fdsolver/Solver.java
index 2277ba4..0bdb344 100644
--- a/src/jrummikub/ai/fdsolver/Solver.java
+++ b/src/jrummikub/ai/fdsolver/Solver.java
@@ -7,6 +7,7 @@ import java.util.Collections;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Iterator;
+import java.util.List;
 import java.util.Map;
 import java.util.Set;
 import static jrummikub.ai.fdsolver.Satisfiability.*;
@@ -24,6 +25,8 @@ public class Solver {
 
 	Set<Constraint> constraints = new HashSet<Constraint>();
 
+	Set<Constraint> dirtyConstraints = new HashSet<Constraint>();
+
 	ArrayList<StackFrame> stack = new ArrayList<StackFrame>();
 
 	boolean contradiction = false;
@@ -83,27 +86,19 @@ public class Solver {
 		}
 	}
 
-	public void propagateOnce() {
-		Var<?> dirtyVar = Collections.min(dirtyVars);
-		dirtyVars.remove(dirtyVar);
-		outerLoop: for (Iterator<Constraint> i = dirtyVar.getConstraints()
-				.iterator(); i.hasNext();) {
-			Constraint constraint = i.next();
-			Satisfiability sat = constraint.getSatisfiability();
-			if (sat == UNSAT) {
-				contradiction = true;
-				break;
-			}
-			if (sat == TAUT) {
-				i.remove();
-				finishedConstraint(constraint, dirtyVar);
-				continue;
-			}
-			for (Propagator propagator : constraint.cachedPropagators) {
-				if (propagator.getWatchedVars().contains(dirtyVar)) {
-					propagator.propagate();
-					if (contradiction) {
-						break outerLoop;
+	public void propagateEach() {
+		List<Var<?>> oldDirtyVars = new ArrayList<Var<?>>(dirtyVars);
+		dirtyVars.clear();
+		Collections.sort(oldDirtyVars);
+		outerLoop: for(Var<?> dirtyVar : oldDirtyVars) {
+			for (Constraint constraint : dirtyVar.getConstraints()) {
+				dirtyConstraints.add(constraint);
+				for (Propagator propagator : constraint.cachedPropagators) {
+					if (propagator.getWatchedVars().contains(dirtyVar)) {
+						propagator.propagate();
+						if (contradiction) {
+							break outerLoop;
+						}
 					}
 				}
 			}
@@ -111,9 +106,31 @@ public class Solver {
 	}
 
 	public void propagateAll() {
+		int i = 0;
 		while (!(dirtyVars.isEmpty() || contradiction)) {
-			propagateOnce();
+			i++;
+			if (i == 50) {
+				cleanUpConstraints();
+				i = 0;
+			} else {
+				propagateEach();
+			}
+		}
+		cleanUpConstraints();
+	}
+	
+	private void cleanUpConstraints() {
+		for (Constraint constraint : dirtyConstraints) {
+			Satisfiability sat = constraint.getSatisfiability();
+			if (sat == UNSAT) {
+				contradiction = true;
+				break;
+			}
+			if (sat == TAUT) {
+				finishedConstraint(constraint, null);
+			}
 		}
+		dirtyConstraints.clear();
 	}
 
 	public void addVar(Var<?> var) {
diff --git a/src/jrummikub/ai/fdsolver/Var.java b/src/jrummikub/ai/fdsolver/Var.java
index 3124e8b..a454487 100644
--- a/src/jrummikub/ai/fdsolver/Var.java
+++ b/src/jrummikub/ai/fdsolver/Var.java
@@ -99,18 +99,12 @@ public class Var<T> implements Comparable<Var<T>> {
 		return constraints.size();
 	}
 	
-	private double fitness() {
-		return range.size();//neighborCount();
-	}
-	
 	@Override
 	public int compareTo(Var<T> other) {
-		return ((Double)fitness()).compareTo(other.fitness());
-		/*
 		int rangeCompare = ((Integer)range.size()).compareTo(other.range.size());
 		if (rangeCompare != 0)
 			return rangeCompare;
-		return -((Integer)neighborCount()).compareTo(other.neighborCount());*/
+		return -((Integer)neighborCount()).compareTo(other.neighborCount());
 	}
 
 }
diff --git a/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java b/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java
index ab0edde..019de92 100644
--- a/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java
+++ b/src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java
@@ -6,6 +6,7 @@ import java.util.Arrays;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.Comparator;
+import java.util.NoSuchElementException;
 
 import jrummikub.ai.fdsolver.Constraint;
 import jrummikub.ai.fdsolver.Propagator;
@@ -17,8 +18,9 @@ public class ComparatorConstraint<T> extends Constraint {
 	Comparator<T> comparator, reverseComparator;
 	ComparatorPropagator<T> trueX, trueY, falseX, falseY;
 	boolean allowEqual;
-	
-	ComparatorConstraint(final Comparator<T> comparator, boolean allowEqual, Var<T> x, Var<T> y) {
+
+	ComparatorConstraint(final Comparator<T> comparator, boolean allowEqual,
+			Var<T> x, Var<T> y) {
 		this.x = x;
 		this.y = y;
 		this.comparator = comparator;
@@ -31,37 +33,42 @@ public class ComparatorConstraint<T> extends Constraint {
 		};
 		trueX = new ComparatorPropagator<T>(comparator, allowEqual, x, y);
 		trueY = new ComparatorPropagator<T>(reverseComparator, allowEqual, y, x);
-		falseX = new ComparatorPropagator<T>(reverseComparator, !allowEqual, x, y);
+		falseX = new ComparatorPropagator<T>(reverseComparator, !allowEqual, x,
+				y);
 		falseY = new ComparatorPropagator<T>(comparator, !allowEqual, y, x);
 	}
-	
+
 	@Override
 	public Collection<Var<?>> getWatchedVars() {
-		return Arrays.<Var<?>>asList(x,y);
+		return Arrays.<Var<?>> asList(x, y);
 	}
 
 	@Override
 	public Collection<Propagator> getPropagators(boolean negate) {
 		if (negate) {
-			return Arrays.<Propagator>asList(falseX,falseY);
+			return Arrays.<Propagator> asList(falseX, falseY);
 		} else {
-			return Arrays.<Propagator>asList(trueX,trueY);
+			return Arrays.<Propagator> asList(trueX, trueY);
 		}
 	}
 
 	@Override
 	public Satisfiability getSatisfiability() {
-		T maxX = Collections.max(x.getRange(), comparator);
-		T minY = Collections.min(y.getRange(), comparator);
-		if (comparator.compare(maxX, minY) < (allowEqual ? 1 : 0)) {
-			return TAUT;
-		}
-		T minX = Collections.min(x.getRange(), comparator);
-		T maxY = Collections.max(y.getRange(), comparator);
-		if (comparator.compare(maxY, minX) < (allowEqual ? 0 : 1)) {
+		try {
+			T maxX = Collections.max(x.getRange(), comparator);
+			T minY = Collections.min(y.getRange(), comparator);
+			if (comparator.compare(maxX, minY) < (allowEqual ? 1 : 0)) {
+				return TAUT;
+			}
+			T minX = Collections.min(x.getRange(), comparator);
+			T maxY = Collections.max(y.getRange(), comparator);
+			if (comparator.compare(maxY, minX) < (allowEqual ? 0 : 1)) {
+				return UNSAT;
+			}
+			return SAT;
+		} catch (NoSuchElementException e) {
 			return UNSAT;
 		}
-		return SAT;
 	}
 
 }
diff --git a/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java b/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java
index 3046eb5..fc1b484 100644
--- a/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java
+++ b/src/jrummikub/ai/fdsolver/constraint/IfConstraint.java
@@ -63,7 +63,7 @@ public class IfConstraint extends Constraint {
 
 		@Override
 		public void propagate() {
-			if (child.getSatisfiability() == Satisfiability.UNSAT) {
+			if (!child.isSatisfiable()) {
 				condition.invalidate(!negateCond);
 			}
 		}
diff --git a/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java b/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java
index 9d80a37..6698282 100644
--- a/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java
+++ b/src/jrummikub/ai/fdsolver/constraint/IndexConstraint.java
@@ -8,6 +8,8 @@ import java.util.HashSet;
 import java.util.Iterator;
 import java.util.List;
 
+import org.w3c.dom.ranges.Range;
+
 import jrummikub.ai.fdsolver.Constraint;
 import jrummikub.ai.fdsolver.Propagator;
 import jrummikub.ai.fdsolver.Satisfiability;
@@ -47,16 +49,16 @@ public class IndexConstraint<T> extends Constraint {
 
 		@Override
 		public void propagate() {
-			HashSet<T> union = new HashSet<T>();
+			HashSet<T> invUnion = new HashSet<T>(target.getRange());
 			for (int i : index.getRange()) {
-				union.addAll(list.get(i).getRange());
-			}
-			for (Iterator<T> i = target.iterator(); i.hasNext();) {
-				T val = i.next();
-				if (!union.contains(val)) {
-					i.remove();
+				invUnion.removeAll(list.get(i).getRange());
+				if (invUnion.isEmpty()) {
+					return;
 				}
 			}
+			for (T val : invUnion) {
+				target.invalidate(val);
+			}
 		};
 	}
 
@@ -70,9 +72,8 @@ public class IndexConstraint<T> extends Constraint {
 		public void propagate() {
 			for (Iterator<Integer> i = index.iterator(); i.hasNext();) {
 				int id = i.next();
-				HashSet<T> range = new HashSet<T>(target.getRange());
-				range.retainAll(list.get(id).getRange());
-				if (range.isEmpty()) {
+				Var<T> item = list.get(id);
+				if (Collections.disjoint(item.getRange(), target.getRange())) {
 					i.remove();
 				}
 			}
@@ -107,28 +108,33 @@ public class IndexConstraint<T> extends Constraint {
 		}
 		return Arrays.<Propagator> asList(new UnionProp(), new IndexProp(), new VarProp());
 	}
-
+	
 	@Override
-	public Satisfiability getSatisfiability() {
-		HashSet<T> union = new HashSet<T>();
+	public boolean isSatisfiable() {
 		for (int i : index.getRange()) {
-			union.addAll(list.get(i).getRange());
-		}
-		boolean isSat = false;
-		for (T val : target.getRange()) {
-			if (union.contains(val)) {
-				isSat = true;
-				break;
+			if(!Collections.disjoint(list.get(i).getRange(), target.getRange())) {
+				return true;
 			}
 		}
-		if (!isSat) {
+		return false;
+	}
+
+	@Override
+	public Satisfiability getSatisfiability() {
+		boolean sat = isSatisfiable();
+		if (!sat) {
 			return Satisfiability.UNSAT;
-		} else {
-			if (union.size() == 1 && target.getRange().size() == 1) {
-				return Satisfiability.TAUT;
-			} else {
+		}
+		if (target.getRange().size() > 1)
+			return Satisfiability.SAT;
+		for (int i : index.getRange()) {
+			Var<T> var = list.get(i); 
+			if (var.getRange().size() > 1)
+				return Satisfiability.SAT;
+			if(var.getValue() != target.getValue()) {
 				return Satisfiability.SAT;
 			}
 		}
+		return Satisfiability.TAUT;
 	}
 }
diff --git a/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java b/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java
index a324d2a..eb72df8 100644
--- a/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java
+++ b/src/jrummikub/ai/fdsolver/constraint/OffsetConstraint.java
@@ -2,6 +2,7 @@ package jrummikub.ai.fdsolver.constraint;
 
 import java.util.Arrays;
 import java.util.Collection;
+import java.util.Collections;
 import java.util.HashSet;
 import java.util.Iterator;
 
@@ -60,12 +61,24 @@ public class OffsetConstraint extends Constraint {
 
 	@Override
 	public Satisfiability getSatisfiability() {
-		HashSet<Integer> shiftedRange = new HashSet<Integer>();
-		for (int val : x.getRange()) {
-			shiftedRange.add(val + offset);
+		boolean disjoint = true;
+		if (x.getRange().size() < y.getRange().size()) {
+			for (int xv : x.getRange()) {
+				if (y.getRange().contains(xv + offset)) {
+					disjoint = false;
+					break;
+				}
+			}
+		} else {
+			for (int yv : y.getRange()) {
+				if (x.getRange().contains(yv - offset)) {
+					disjoint = false;
+					break;
+				}
+			}
 		}
-		shiftedRange.retainAll(y.getRange());
-		if (shiftedRange.isEmpty()) {
+		
+		if (disjoint) {
 			return Satisfiability.UNSAT;
 		} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
 			return Satisfiability.TAUT;
diff --git a/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java b/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java
index 954b6fa..7fc0025 100644
--- a/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java
+++ b/src/jrummikub/ai/fdsolver/constraint/SameConstraint.java
@@ -2,6 +2,7 @@ package jrummikub.ai.fdsolver.constraint;
 
 import java.util.Arrays;
 import java.util.Collection;
+import java.util.Collections;
 import java.util.HashSet;
 import java.util.Iterator;
 
@@ -56,9 +57,7 @@ public class SameConstraint<T> extends Constraint {
 
 	@Override
 	public Satisfiability getSatisfiability() {
-		HashSet<T> range = new HashSet<T>(x.getRange());
-		range.retainAll(y.getRange());
-		if (range.isEmpty()) {
+		if (Collections.disjoint(x.getRange(), y.getRange())) {
 			return Satisfiability.UNSAT;
 		} else if (x.getRange().size() == 1 && y.getRange().size() == 1) {
 			return Satisfiability.TAUT;