Restructured fdsolver api and made first test succeed

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

src/jrummikub/ai/fdsolver/Constraint.java

@@ -1,5 +1,11 @@
 package jrummikub.ai.fdsolver;
 
+import java.util.Collection;
+
 public interface Constraint {
-	
+	public Collection<Var<?>> getWatchedVars();
+
+	public Collection<Propagator> getPropagators(boolean negate);
+
+	public Satisfiability getSatisfiability();
 }

src/jrummikub/ai/fdsolver/Constraints.java

@@ -1,13 +0,0 @@
-package jrummikub.ai.fdsolver;
-
-public class Constraints {
-
-	public static <T extends Comparable<T>> void lessThan(Solver solver, Var<T> x, Var<T> y) {
-		// TODO Auto-generated method stub
-	}
-
-	public static <T extends Comparable<T>> void lessThan(Solver solver, Var<T> x, T y) {
-		// TODO Auto-generated method stub
-	}
-
-}

src/jrummikub/ai/fdsolver/LessThan.java

@@ -1,9 +0,0 @@
-package jrummikub.ai.fdsolver;
-
-public class LessThan<T> implements Constraint {
-
-	public LessThan(Var<T> x, Var<T> y) {
-		// TODO Auto-generated constructor stub
-	}
-
-}

src/jrummikub/ai/fdsolver/Propagator.java

@@ -0,0 +1,9 @@
+package jrummikub.ai.fdsolver;
+
+import java.util.Collection;
+
+public interface Propagator {
+	public abstract Collection<Var<?>> getWatchedVars();
+
+	public abstract void propagate();
+}

src/jrummikub/ai/fdsolver/Satisfiability.java

@@ -0,0 +1,5 @@
+package jrummikub.ai.fdsolver;
+
+public enum Satisfiability {
+	TAUT, SAT, UNSAT
+}

src/jrummikub/ai/fdsolver/Solver.java

@@ -1,25 +1,195 @@
 package jrummikub.ai.fdsolver;
 
-public class Solver {
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Map;
+import java.util.Set;
 
-	public void add(Constraint constraint) {
-		// TODO Auto-generated method stub
-		
+public class Solver {
+	Set<Var<?>> vars = new HashSet<Var<?>>();
+
+	Set<Var<?>> dirtyVars = new HashSet<Var<?>>();
+
+	Set<Var<?>> unsolvedVars = new HashSet<Var<?>>();
+
+	Set<Constraint> constraints = new HashSet<Constraint>();
+
+	ArrayList<StackFrame> stack = new ArrayList<StackFrame>();
+
+	boolean contradiction = false;
+
+	static private class StackFrame {
+		Map<Var<?>, HashSet<?>> invalidatedValues = new HashMap<Var<?>, HashSet<?>>();
+		Var<?> branchVar;
+		Object branchValue;
+
+		public <T> void invalidate(Var<T> var, T invalid) {
+			HashSet<T> values = (HashSet<T>) invalidatedValues.get(var);
+			if (values == null) {
+				invalidatedValues.put(var,
+						new HashSet<T>(Arrays.asList(invalid)));
+			} else {
+				values.add(invalid);
+			}
+		}
+
+		@Override
+		public String toString() {
+			return "StackItem [invalidatedValues=" + invalidatedValues + "]";
+		}
+	}
+
+	public Solver() {
+		stack.add(new StackFrame());
 	}
 
 	public boolean solve() {
-		// TODO Auto-generated method stub
-		return false;
+		do {
+			solveStep();
+		} while (!(contradiction || (dirtyVars.isEmpty() && unsolvedVars
+				.isEmpty())));
+		return !contradiction;
 	}
 
-	public void push() {
-		// TODO Auto-generated method stub
-		
+	public void solveStep() {
+		if (unsolvedVars.isEmpty() && dirtyVars.isEmpty()) {
+			contradiction = true;
+		} else {
+			propagateAll();
+		}
+		if (contradiction) {
+			if (stack.size() == 1) {
+				return;
+			}
+			backtrack();
+		} else if (unsolvedVars.isEmpty()) {
+			return;
+		} else {
+			branch();
+		}
 	}
 
-	public void pop() {
-		// TODO Auto-generated method stub
-		
+	public void propagateOnce() {
+		Iterator<Var<?>> it = dirtyVars.iterator();
+		Var<?> dirtyVar = it.next();
+		it.remove();
+		outerLoop: for (Constraint constraint : constraints) {
+			if (constraint.getWatchedVars().contains(dirtyVar)) {
+				for (Propagator propagator : constraint.getPropagators(false)) {
+					if (propagator.getWatchedVars().contains(dirtyVar)) {
+						propagator.propagate();
+						if (contradiction) {
+							break outerLoop;
+						}
+					}
+				}
+			}
+		}
+	}
+
+	public void propagateAll() {
+		while (!(dirtyVars.isEmpty() || contradiction)) {
+			propagateOnce();
+		}
+	}
+
+	public void addVar(Var<?> var) {
+		vars.add(var);
+		if (var.getRange().size() != 1) {
+			unsolvedVars.add(var);
+		}
+	}
+
+	public void addConstraint(Constraint constraint) {
+		constraints.add(constraint);
+
+		for (Var<?> var : constraint.getWatchedVars()) {
+			var.makeDirty();
+		}
+	}
+
+	// backtracking and logging
+
+	void branch() {
+		branchOn(unsolvedVars.iterator().next());
+	}
+
+	@SuppressWarnings("unchecked")
+	void branchOn(Var<?> var) {
+		Object value = var.getRange().iterator().next();
+		branchWith((Var<Object>) var, value);
+	}
+
+	<T> void branchWith(Var<T> var, T value) {
+		StackFrame stackFrame = new StackFrame();
+		stackFrame.branchVar = var;
+		stackFrame.branchValue = value;
+		stack.add(stackFrame);
+		var.choose(value);
+	}
+
+	private StackFrame getTopStackFrame() {
+		return stack.get(stack.size() - 1);
+	}
+
+	<T> void logInvalidation(Var<T> var, T invalid) {
+		getTopStackFrame().invalidate(var, invalid);
+		if (var.getRange().size() == 1) {
+			unsolvedVars.remove(var);
+		}
+	}
+
+	@SuppressWarnings("unchecked")
+	// This would need rank-2 types which java lacks
+	private void rollback(StackFrame item) {
+		for (Map.Entry<Var<?>, HashSet<?>> entry : item.invalidatedValues
+				.entrySet()) {
+			Var<Object> var = (Var<Object>) entry.getKey();
+			HashSet<Object> values = (HashSet<Object>) entry.getValue();
+			var.getRange().addAll(values);
+			if (var.getRange().size() != 1) {
+				unsolvedVars.add(var);
+			} else {
+				unsolvedVars.remove(var);
+			}
+		}
+	}
+
+	@SuppressWarnings("unchecked")
+	void backtrack() {
+		contradiction = false;
+		StackFrame topFrame = getTopStackFrame();
+		rollback(topFrame);
+		stack.remove(stack.size() - 1);
+		((Var<Object>) topFrame.branchVar).invalidate(topFrame.branchValue);
+	}
+
+	// factory methods for vars
+
+	public Var<Integer> makeRangeVar(int low, int high) {
+		ArrayList<Integer> range = new ArrayList<Integer>();
+		for (int i = low; i <= high; i++) {
+			range.add(i);
+		}
+		return makeVar(range);
+	}
+
+	public Var<Boolean> makeBoolVar() {
+		return makeVar(true, false);
+	}
+
+	public <T> Var<T> makeVar(Collection<T> range) {
+		Var<T> var = new Var<T>(this, range);
+		addVar(var);
+		return var;
+	}
+
+	public <T> Var<T> makeVar(T... range) {
+		return makeVar(Arrays.asList(range));
 	}
 
 }

src/jrummikub/ai/fdsolver/SolverMain.java

@@ -0,0 +1,42 @@
+package jrummikub.ai.fdsolver;
+
+
+public class SolverMain {
+
+	/*
+	 * eingabe: liste handsteinen + liste tischsteinen
+	 * 
+	 * foreach stein: stein id (durchlaufend nummeriert) Var<Boolean> onTable =
+	 * tisch ? {true}, {true, false} Var<Integer> value = {N} Var<StoneColor>
+	 * color = {C} Var<Integer> nachbarL,R = {-1, 0...steinanzahl} Var<Boolean>
+	 * groupOrRun
+	 * 
+	 * nachbarR != -1 => nachbarL[nachbarR[id]] == id nachbarL != -1 =>
+	 * nachbarR[nachbarL[id]] == id
+	 * 
+	 * nachbarR != -1 => gOR[nachbarR[id]] = gOR nachbarL != -1 =>
+	 * gOR[nachbarL[id]] = gOR
+	 * 
+	 * nachbar{R,L} != -1 => group <=> value[{R,L}] == value nachbar{R,L} != -1
+	 * && group => color[{R,L}] {<,>} color // hier auch <=> ?
+	 * 
+	 * nachbar{R,L} != -1 => run <=> color[{R,L}] == color nachbar{R,L} != -1 =>
+	 * run <=> value[{R,L}] == value {+,-} 1
+	 * 
+	 * Var<Integer> pos von {links, rechts} + constraints
+	 * 
+	 * links + rechts >= 3
+	 * 
+	 * foreach handstein: Var<Integer> badness = onTable ? ### (z. B. 1) : 0
+	 * 
+	 * totalBadness = sum(all badness)
+	 * 
+	 * foreach joker: Var<Integer> value = {-1, 1..13} Var<StoneColor> color =
+	 * {F, C0..C3} onTable == false <=> value == -1 same with color
+	 * 
+	 * joker sind sortiert
+	 */
+	public static void main(String[] args) {
+	}
+
+}

src/jrummikub/ai/fdsolver/Var.java

@@ -2,18 +2,15 @@ package jrummikub.ai.fdsolver;
 
 import java.util.Collection;
 import java.util.HashSet;
-import java.util.Set;
+import java.util.Iterator;
 
 public class Var<T> {
-	Set<T> range;
-	
-	public Var(Solver solver, Collection<T> range) {
-		this.range = new HashSet<T>(range);
-	}
+	private Solver solver;
+	private HashSet<T> range;
 
-	public static <T> Var<T> range(Solver solver, T low, T high) {
-		// TODO todo todo todo
-		return null;
+	public Var(Solver solver, Collection<T> range) {
+		this.solver = solver;
+		this.range = new HashSet<T>(range);
 	}
 
 	public T getValue() {
@@ -22,4 +19,60 @@ public class Var<T> {
 		return range.iterator().next();
 	}
 
+	public HashSet<T> getRange() {
+		return range;
+	}
+
+	public void choose(T value) {
+		for (Iterator<T> i = this.iterator(); i.hasNext();) {
+			if (i.next() != value) {
+				i.remove();
+			}
+		}
+	}
+
+	public void makeDirty() {
+		this.solver.dirtyVars.add(this);
+	}
+
+	public void invalidate(T value) {
+		range.remove(value);
+		solver.logInvalidation(this, value);
+		makeDirty();
+	}
+
+	public Iterator<T> iterator() {
+		final Iterator<T> iterator = range.iterator();
+		return new Iterator<T>() {
+			T lastValue;
+
+			@Override
+			public boolean hasNext() {
+				return iterator.hasNext();
+			}
+
+			@Override
+			public T next() {
+				lastValue = iterator.next();
+				return lastValue;
+			}
+
+			@Override
+			public void remove() {
+				// TODO logging
+				iterator.remove();
+				solver.logInvalidation(Var.this, lastValue);
+				makeDirty();
+				if (range.size() == 0) {
+					solver.contradiction = true;
+				}
+			}
+		};
+	}
+
+	@Override
+	public String toString() {
+		return "Var" + range;
+	}
+
 }

src/jrummikub/ai/fdsolver/constraint/ComparatorConstraint.java

@@ -0,0 +1,67 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import static jrummikub.ai.fdsolver.Satisfiability.*;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
+
+import jrummikub.ai.fdsolver.Constraint;
+import jrummikub.ai.fdsolver.Propagator;
+import jrummikub.ai.fdsolver.Satisfiability;
+import jrummikub.ai.fdsolver.Var;
+
+public class ComparatorConstraint<T> implements Constraint {
+	Var<T> x, y;
+	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) {
+		this.x = x;
+		this.y = y;
+		this.comparator = comparator;
+		this.allowEqual = allowEqual;
+		reverseComparator = new Comparator<T>() {
+			@Override
+			public int compare(T o1, T o2) {
+				return comparator.compare(o2, o1);
+			}
+		};
+		trueX = new ComparatorPropagator<T>(comparator, allowEqual, x, y);
+		trueY = new ComparatorPropagator<T>(reverseComparator, allowEqual, y, x);
+		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);
+	}
+
+	@Override
+	public Collection<Propagator> getPropagators(boolean negate) {
+		if (negate) {
+			return Arrays.<Propagator>asList(falseX,falseY);
+		} else {
+			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)) {
+			return UNSAT;
+		}
+		return SAT;
+	}
+
+}

src/jrummikub/ai/fdsolver/constraint/ComparatorPropagator.java

@@ -0,0 +1,42 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.List;
+
+import jrummikub.ai.fdsolver.Propagator;
+import jrummikub.ai.fdsolver.Var;
+
+public class ComparatorPropagator<T> implements Propagator {
+	private Var<T> x, y;
+	private Comparator<T> comparator;
+	private boolean allowEqual;
+	public ComparatorPropagator(Comparator<T> comparator, boolean allowEqual, Var<T> x, Var<T> y) {
+		this.comparator = comparator;
+		this.allowEqual = allowEqual;
+		this.x = x;
+		this.y = y;
+	}
+
+	@Override
+	public Collection<Var<?>> getWatchedVars() {
+		return Arrays.<Var<?>>asList(y);
+	}
+
+	@Override
+	public void propagate() {
+		T maxY = Collections.max(y.getRange(), comparator);
+		
+		for(Iterator<T> i = x.iterator(); i.hasNext();) {
+			T value = i.next();
+			int comparision = comparator.compare(value, maxY);
+			if (comparision > 0 || comparision == 0 && !allowEqual) {
+				i.remove();
+			}
+		}
+	}
+}

src/jrummikub/ai/fdsolver/constraint/Filter.java

@@ -0,0 +1,5 @@
+package jrummikub.ai.fdsolver.constraint;
+
+public interface Filter<T> {
+	public boolean accept(T value);
+}

src/jrummikub/ai/fdsolver/constraint/FilterConstraint.java

@@ -0,0 +1,65 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import static jrummikub.ai.fdsolver.Satisfiability.SAT;
+import static jrummikub.ai.fdsolver.Satisfiability.TAUT;
+import static jrummikub.ai.fdsolver.Satisfiability.UNSAT;
+
+import java.util.Arrays;
+import java.util.Collection;
+
+import jrummikub.ai.fdsolver.Constraint;
+import jrummikub.ai.fdsolver.Propagator;
+import jrummikub.ai.fdsolver.Satisfiability;
+import jrummikub.ai.fdsolver.Var;
+
+public class FilterConstraint<T> implements Constraint {
+	private Var<T> var;
+	private Propagator trueProp, falseProp;
+	private Filter<T> filter;
+
+	public FilterConstraint(final Filter<T> filter, Var<T> var) {
+		this.var = var;
+		this.filter = filter;
+		trueProp = new FilterPropagator<T>(filter, var);
+		falseProp = new FilterPropagator<T>(new Filter<T>() {
+			@Override
+			public boolean accept(T value) {
+				return !filter.accept(value);
+			}
+		}, var);
+	}
+
+	@Override
+	public Collection<Var<?>> getWatchedVars() {
+		return Arrays.<Var<?>> asList(var);
+	}
+
+	@Override
+	public Collection<Propagator> getPropagators(boolean negate) {
+		return Arrays.asList(negate ? falseProp : trueProp);
+	}
+
+	@Override
+	public Satisfiability getSatisfiability() {
+		boolean any = false;
+		boolean all = true;
+		
+		for (T value : var.getRange()) {
+			boolean accepted = filter.accept(value);
+			if (accepted) {
+				any = true;
+			} else {
+				all = false;
+			}
+		}
+		
+		if (all && any) {
+			return TAUT;
+		} else if (any) {
+			return SAT;
+		} else {
+			return UNSAT;
+		}
+	}
+
+}

src/jrummikub/ai/fdsolver/constraint/FilterPropagator.java

@@ -0,0 +1,31 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Iterator;
+
+import jrummikub.ai.fdsolver.Propagator;
+import jrummikub.ai.fdsolver.Var;
+
+public class FilterPropagator<T> implements Propagator {
+	private Filter<T> filter;
+	private Var<T> var;
+	
+	public FilterPropagator(Filter<T> filter, Var<T> var) {
+		this.filter = filter;
+		this.var = var;	
+	}
+	
+	@Override
+	public Collection<Var<?>> getWatchedVars() {
+		return Arrays.<Var<?>>asList(var);
+	}
+
+	@Override
+	public void propagate() {
+		for(Iterator<T> i = var.iterator(); i.hasNext();) {
+			if(!filter.accept(i.next()))
+				i.remove();
+		}
+	}
+}

src/jrummikub/ai/fdsolver/constraint/GreaterThan.java

@@ -0,0 +1,18 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import java.util.Comparator;
+
+import jrummikub.ai.fdsolver.Var;
+
+public class GreaterThan<T extends Comparable<T>> extends
+		ComparatorConstraint<T> {
+
+	public GreaterThan(boolean allowEqual, Var<T> x, Var<T> y) {
+		super(new Comparator<T>() {
+			@Override
+			public int compare(T o1, T o2) {
+				return o2.compareTo(o1);
+			}
+		}, allowEqual, x, y);
+	}
+}

src/jrummikub/ai/fdsolver/constraint/GreaterThanConst.java

@@ -0,0 +1,15 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import jrummikub.ai.fdsolver.Var;
+
+public class GreaterThanConst<T extends Comparable<T>> extends
+		FilterConstraint<T> {
+	public GreaterThanConst(final boolean allowEqual, Var<T> x, final T y) {
+		super(new Filter<T>() {
+			@Override
+			public boolean accept(T value) {
+				return y.compareTo(value) < (allowEqual ? 1 : 0);
+			}
+		}, x);
+	}
+}

src/jrummikub/ai/fdsolver/constraint/LessThan.java

@@ -0,0 +1,17 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import java.util.Comparator;
+
+import jrummikub.ai.fdsolver.Var;
+
+public class LessThan<T extends Comparable<T>> extends ComparatorConstraint<T> {
+
+	public LessThan(boolean allowEqual, Var<T> x, Var<T> y) {
+		super(new Comparator<T>() {
+			@Override
+			public int compare(T o1, T o2) {
+				return o1.compareTo(o2);
+			}
+		}, allowEqual, x, y);
+	}
+}

src/jrummikub/ai/fdsolver/constraint/LessThanConst.java

@@ -0,0 +1,18 @@
+package jrummikub.ai.fdsolver.constraint;
+
+import java.util.Collection;
+
+import jrummikub.ai.fdsolver.Propagator;
+import jrummikub.ai.fdsolver.Solver;
+import jrummikub.ai.fdsolver.Var;
+
+public class LessThanConst<T extends Comparable<T>> extends FilterConstraint<T> {
+	public LessThanConst(final boolean allowEqual, Var<T> x, final T y) {
+		super(new Filter<T>() {
+			@Override
+			public boolean accept(T value) {
+				return value.compareTo(y) < (allowEqual ? 1 : 0);
+			}
+		}, x);
+	}
+}

test/jrummikub/ai/fdsolver/SolverTest.java

@@ -1,8 +1,8 @@
 package jrummikub.ai.fdsolver;
 
 import static org.junit.Assert.assertEquals;
-
-import java.util.Arrays;
+import jrummikub.ai.fdsolver.constraint.LessThan;
+import jrummikub.ai.fdsolver.constraint.LessThanConst;
 
 import org.junit.Test;
 
@@ -11,18 +11,20 @@ public class SolverTest {
 	public void test() {
 		Solver solver = new Solver();
 
-		Var<Integer> x = new Var<Integer>(solver, Arrays.asList(1, 2, 3));
-		Var<Integer> y = Var.range(solver, 1,13);
+		Var<Integer> x = solver.makeVar(1, 2, 3);
+		Var<Integer> y = solver.makeRangeVar(1, 13);
 		
-		Constraints.lessThan(solver, y, x);
-				
-		while(solver.solve()) {
-			solver.push();
-			Constraints.lessThan(solver, x, x.getValue());
+		solver.addConstraint(new LessThan<Integer>(false, y, x));
+		
+		int lastx = 0, lasty = 0;
+		while (solver.solve()) {
+			lastx = x.getValue();
+			lasty = y.getValue();
+			System.out.println("x = " + lastx + ", y = " + lasty);
+			solver.addConstraint(new LessThanConst<Integer>(false, x, x.getValue()));
 		}
-		solver.pop();
-		
-		assertEquals(2, (int)x.getValue());
-		assertEquals(1, (int)y.getValue());
+
+		assertEquals(2, lastx);
+		assertEquals(1, lasty);
 	}
 }