/* 
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.examples.sudoku;

import static kodkod.ast.Formula.and;
import static kodkod.ast.Relation.ternary;
import static kodkod.ast.Relation.unary;

import java.lang.management.ManagementFactory;
import java.lang.management.ThreadMXBean;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;

import kodkod.ast.Decls;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.Node;
import kodkod.ast.Relation;
import kodkod.ast.Variable;
import kodkod.engine.Proof;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.satlab.ReductionStrategy;
import kodkod.engine.satlab.SATFactory;
import kodkod.engine.ucore.AdaptiveRCEStrategy;
import kodkod.engine.ucore.NCEStrategy;
import kodkod.engine.ucore.SCEStrategy;
import kodkod.instance.Bounds;
import kodkod.instance.Tuple;
import kodkod.instance.TupleFactory;
import kodkod.instance.TupleSet;

/**
 * A simple encoding of Sudoku, that includes several alternative
 * encodings of the rules.
 * @specfield n: int // the order of this sudoku puzzle
 * @author Emina Torlak
 */
public final class Sudoku {
	private final Relation number = unary("number"), grid  = ternary("grid");
	private final Relation[] region;
	
	/**
	 * Constructs a new instance of (r^2)x(r^2) Sudoku.
	 * @requires r > 1
	 * @ensures this.n = r * r
	 */
	public Sudoku(final int r) { 
		if (r < 2) throw new IllegalArgumentException("r must be greater than 1:  r=" + r);
		region = new Relation[r];
		for(int i =0; i < r; i++) { 
			region[i] = Relation.unary("r"+(i+1));
		}
	}
	
	/**
	 * Returns the relation representing the grid.
	 * @return relation representing the grid.
	 */
	public final Relation grid() { return grid; }
	
	/**
	 * Returns the relation representing the set of numbers.
	 * @return relation representing the set of numbers
	 */
	public final Relation number() { return number; }
	
	/**
	 * Returns the ith region.
	 * @requires 0 <= i < sqrt(this.n)
	 * @return the ith region
	 */
	public final Relation region(int i) { return region[i]; }
	
	/**
	 * Returns grid[x][y].
	 * @return grid[x][y].
	 */
	private final Expression grid(Expression x, Expression y) { 
		return y.join(x.join(grid));
	}
	
	/**
	 * Returns the value of the complete predicate, given the specified rows and columns expressions.
	 * @requires rows.arity = cols.arity = 1
	 * @return complete(rows, cols)
	 */
	private final Formula complete(Expression rows, Expression cols) {
		return number.in(grid(rows,cols));
	}

	/**
	 * Returns the rules of the game that are a bit slower than the other two formulations.
	 * @return rules of the game
	 */
	public final Formula slowRules() { 
		final List<Formula> rules = new ArrayList<Formula>(3+region.length*region.length);

		final Variable x = Variable.unary("x"), y = Variable.unary("y");

		rules.add( grid(x,y).one().forAll(x.oneOf(number).and(y.oneOf(number))) );
		rules.add( complete(x, number).forAll(x.oneOf(number)) );
		rules.add( complete(number, y).forAll(y.oneOf(number)) );
	
		for(Relation rx : region) { 
			for(Relation ry: region) { 
				rules.add( complete(rx, ry) );
			}
		}
		return and(rules); 
	}
		
	/**
	 * Returns the rules of the game that yield better performance than {@linkplain #slowRules()}.
	 * @return rules of the game
	 */
	public final Formula rules() { 
		final List<Formula> rules = new ArrayList<Formula>(3+region.length*region.length);

		final Variable x = Variable.unary("x"), y = Variable.unary("y");
		final Decls decls = x.oneOf(number).and(y.oneOf(number));

		rules.add( grid(x,y).some().forAll(decls) );
		rules.add( grid(x,y).intersection(grid(x, number.difference(y))).no().forAll(decls) );	
		rules.add( grid(x,y).intersection(grid(number.difference(x), y)).no().forAll(decls) );
	
		for(Relation rx : region) { 
			for(Relation ry: region) { 
				rules.add( grid(x, y).intersection(grid(rx.difference(x),ry.difference(y))).no().forAll(x.oneOf(rx).and(y.oneOf(ry))) );
			}
		}
		
		return and(rules); 
	}
	
	/**
	 * Returns a slightly different version of the rules that yields
	 * better performance than {@linkplain #rules()}.
	 * @return rules of the game
	 */
	public final Formula fastRules() { 
		final List<Formula> rules = new ArrayList<Formula>(3+region.length*region.length);

		final Variable x = Variable.unary("x"), y = Variable.unary("y");
		final Decls decls = x.oneOf(number).and(y.oneOf(number));

		rules.add( grid(x,y).one().forAll(decls) );
		rules.add( grid(x,y).intersection(grid(x, number.difference(y))).no().forAll(decls) );	
		rules.add( grid(x,y).intersection(grid(number.difference(x), y)).no().forAll(decls) );
	
		for(Relation rx : region) { 
			for(Relation ry: region) { 
				rules.add( complete(rx, ry) );
			}
		}
		return and(rules); 
	}
	
	/**
	 * Returns the bounds for the default puzzle.
	 * @return bounds for the default puzzle.
	 */
	public static final TupleSet defaultPuzzle() { 
		return SudokuParser.parse("600200050018060020003000400000607800402050000000908000504090300020000014300005007");
	}
		
	/**
	 * Constructs new bounds using the given set of puzzle clues.
	 * @requires clues.universe = {i: Integer | 0 < i <= this.n}
	 * @requires clues.arity = 3
	 * @return new bounds using the given set of puzzle clues.
	 */
	public final Bounds bounds(TupleSet clues) { 
		final int r = region.length;
		final int n = r*r;
		if(clues.universe().size()!=n || clues.arity()!=3) throw new IllegalArgumentException();
		
		final Bounds bounds = new Bounds(clues.universe());
		final TupleFactory f = bounds.universe().factory();
		
		bounds.boundExactly(number, f.allOf(1));
		for(int i = 0; i < r; i++) { 
			bounds.boundExactly(region[i], f.range(f.tuple(i*r+1), f.tuple((i+1)*r)));
		}
		
		final TupleSet givens = clues.clone(), upper = f.allOf(3);
		for(Tuple t : clues) { 
			final int x = (Integer)t.atom(0), y = (Integer)t.atom(1), v = (Integer)t.atom(2);
			for(int i = 1; i<=n; i++ ) {
				if (v!=i) upper.remove(f.tuple(x, y, i));
			}
		}
		
		bounds.bound(grid, givens, upper);
		return bounds;
	}
		
	
	
	/**
	 * Solves the given puzzle using MiniSatProver and translation logging
	 * if core is true; otherwise solves it using MiniSat.  Solution is
	 * printed to standard output.
	 */
	private void solve(TupleSet clues, SudokuCoreExtractor extractor) { 
		final Solver solver = new Solver();
		
		solver.options().setSolver(SATFactory.MiniSatProver);
		solver.options().setLogTranslation(1);
		
				
		final Solution sol = solver.solve(rules(), bounds(clues));
		if (sol.instance()!=null) { 
			System.out.println(sol.stats());	
			System.out.println(SudokuParser.prettyPrint(sol.instance().tuples(grid)));
		} else {
			System.out.println(sol.stats());
			final Proof proof = sol.proof();
			final long[] coreData = extractor.extract(proof);
			System.out.println("Core (strategy="+extractor.name().toLowerCase()+", size="+coreData[0]+", ms="+coreData[1]+"):");
			for(Node n : proof.highLevelCore().values()) { 
				System.out.println(n);
			}
		}
	}
	
	private static void usage() { 
		System.out.println("Usage: java examples.sudoku.Sudoku [-core=<oce|rce|sce|nce>] [puzzle]");
		System.exit(1);
	}
		
	/**
	 * Enumerates core extractors for use with sudoku.
	 * @author Emina Torlak
	 */
	private static enum SudokuCoreExtractor {
		
		OCE {
			long[] extract(Proof proof) { 
				final ThreadMXBean bean = ManagementFactory.getThreadMXBean();
				bean.setThreadCpuTimeEnabled(true);
				final long start = bean.getCurrentThreadUserTime();
				final int initCore = proof.highLevelCore().size();
				final long end = bean.getCurrentThreadUserTime();
				return new long[]{ initCore, toMillis(end-start) };
			}
		},
		RCE,
		SCE,
		NCE;
		
		long[] extract(Proof proof) { 
			final ThreadMXBean bean = ManagementFactory.getThreadMXBean();
			bean.setThreadCpuTimeEnabled(true);
			final ReductionStrategy strategy;
			switch(this) { 
			case RCE : strategy = new AdaptiveRCEStrategy(proof.log()); break;
			case SCE : strategy = new SCEStrategy(proof.log()); break;
			case NCE : strategy = new NCEStrategy(proof.log()); break;
			default : throw new IllegalStateException("Unknown strategy: " + this);
			}
			final long start = bean.getCurrentThreadUserTime();
			proof.minimize(strategy);
			final int minCore = proof.highLevelCore().size();
			final long end = bean.getCurrentThreadUserTime();
			return new long[]{ minCore, toMillis(end-start) };
		}
		
		static long toMillis(long nanos) { return nanos / 1000000; }
	}
	
	/**
	 * Usage: java examples.sudoku.Sudoku [-core=<oce|rce|sce|nce>] [puzzle]
	 */
	public static void main(String[] args) {
		try {
			final TupleSet clues = args.length==0 ? defaultPuzzle() : SudokuParser.parse(args[args.length-1]);
			final SudokuCoreExtractor extractor;
			final Map<String,String> opts = SudokuParser.options(args);
			if (opts.containsKey("-core")) { 
				final String val = opts.get("-core");
				if (val==null) usage();
				extractor = SudokuCoreExtractor.valueOf(SudokuCoreExtractor.class, val.toUpperCase());	
			} else {
				extractor = SudokuCoreExtractor.RCE;
			}

			(new Sudoku((int)Math.sqrt(clues.universe().size()))).solve(clues, extractor);
		} catch (IllegalArgumentException iae) { 
			throw iae;
//			usage();
		}
	}
}