/*******************************************************************************
 * Copyright (c) 2007, 2009 IBM Corporation and others. All rights reserved. This
 * program and the accompanying materials are made available under the terms of
 * the Eclipse Public License v1.0 which accompanies this distribution, and is
 * available at http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors: IBM Corporation - initial API and implementation
 * Daniel Le Berre - Fix in the encoding and the optimization function
 * Alban Browaeys - Optimized string concatenation in bug 251357
 * Jed Anderson - switch from opb files to API calls to DependencyHelper in bug 200380
 ******************************************************************************/
package org.eclipse.equinox.p2.cudf.solver;

import java.io.PrintWriter;
import java.util.*;
import org.eclipse.core.runtime.*;
import org.eclipse.core.runtime.jobs.Job;
import org.eclipse.equinox.p2.cudf.Log;
import org.eclipse.equinox.p2.cudf.Main;
import org.eclipse.equinox.p2.cudf.metadata.*;
import org.eclipse.equinox.p2.cudf.query.*;
import org.eclipse.osgi.util.NLS;
import org.sat4j.minisat.restarts.LubyRestarts;
import org.sat4j.pb.*;
import org.sat4j.pb.core.PBSolverResolution;
import org.sat4j.pb.tools.LexicoHelper;
import org.sat4j.pb.tools.WeightedObject;
import org.sat4j.specs.*;

/**
 * This class is the interface between SAT4J and the planner. It produces a
 * boolean satisfiability problem, invokes the solver, and converts the solver result
 * back into information understandable by the planner.
 */
public class Projector {
	private static final boolean DEBUG = false; //SET THIS TO FALSE FOR THE COMPETITION
	private static final boolean TIMING = false; //SET THIS TO FALSE FOR THE COMPETITION
	private static final boolean DEBUG_ENCODING = false; //SET THIS TO FALSE FOR THE COMPETITION
	private static final boolean PURGE = true;

	private QueryableArray picker;

	private Map noopVariables; //key IU, value AbstractVariable
	private List abstractVariables;

	private TwoTierMap slice; //The IUs that have been considered to be part of the problem

	LexicoHelper dependencyHelper;
	private Collection solution;
	private Collection assumptions;

	private MultiStatus result;

	private InstallableUnit entryPoint;

	private SolverConfiguration configuration;
	private OptimizationFunction optFunction;

	private List optionalityVariables;
	private List optionalityPairs;

	static class AbstractVariable {
		private String str;

		AbstractVariable() {
			// no value for str
		}

		AbstractVariable(String str) {
			this.str = str;
		}

		public String toString() {
			return "AbstractVariable: " + (str == null ? "" + hashCode() : str); //$NON-NLS-1$
		}
	}

	public Projector(QueryableArray q) {
		picker = q;
		noopVariables = new HashMap();
		slice = new TwoTierMap(q.getSize(), TwoTierMap.POLICY_BOTH_MAPS_PRESERVE_ORDERING);
		abstractVariables = new ArrayList();
		result = new MultiStatus(Main.PLUGIN_ID, IStatus.OK, Messages.Planner_Problems_resolving_plan, null);
		assumptions = new ArrayList();
		optionalityVariables = new ArrayList();
		optionalityPairs = new ArrayList();
	}

	private void purgeIU(InstallableUnit iu) {
		if (PURGE) {
			iu.setCapabilities(InstallableUnit.NO_PROVIDES);
			iu.setRequiredCapabilities(InstallableUnit.NO_REQUIRES);
		}
	}

	public void encode(InstallableUnit entryPointIU, SolverConfiguration conf) {
		this.configuration = conf;
		this.entryPoint = entryPointIU;
		solution = null;
		try {
			long start = 0;
			if (TIMING) {
				start = System.currentTimeMillis();
				Tracing.debug("Starting projection ... "); //$NON-NLS-1$
			}
			IPBSolver solver;
			if (DEBUG_ENCODING) {
				solver = new UserFriendlyPBStringSolver(); //.newOPBStringSolver();
			} else if (conf.encoding) {
				solver = SolverFactory.newOPBStringSolver();
			} else {
				PBSolverResolution mysolver = SolverFactory.newCompetPBResLongWLMixedConstraintsObjectiveExpSimp();
				mysolver.setSimplifier(mysolver.SIMPLE_SIMPLIFICATION);
				mysolver.setRestartStrategy(new LubyRestarts(512));
				// mysolver.setLearnedConstraintsDeletionStrategy(mysolver.memory_based);
				// mysolver.setSearchListener(new DecisionTracing("/tmp/rand992.dat"));
				solver = mysolver; // SolverFactory.newResolutionGlucoseSimpleSimp();// SolverFactory.newEclipseP2();
			}
			if ("default".equals(configuration.timeout)) {
				solver.setTimeout(300); // 5 minutes
			} else {
				int number = Integer.valueOf(configuration.timeout.substring(0, configuration.timeout.length() - 1)).intValue();
				if (configuration.timeout.endsWith("s")) {
					solver.setTimeout(number);
				} else {
					solver.setTimeoutOnConflicts(number);
				}
			}
			solver.setVerbose(configuration.verbose);
			solver.setLogPrefix("# ");
			Log.printlnNoPrefix(solver.toString("# "));
			dependencyHelper = new LexicoHelper(solver, conf.explain);
			if (DEBUG_ENCODING) {
				((UserFriendlyPBStringSolver) solver).setMapping(dependencyHelper.getMappingToDomain());
			}
			Iterator iusToEncode = picker.iterator();
			List iusToOrder = new ArrayList(picker.getSize());
			while (iusToEncode.hasNext()) {
				iusToOrder.add(iusToEncode.next());
			}
			Collections.sort(iusToOrder);
			iusToEncode = iusToOrder.iterator();
			while (iusToEncode.hasNext()) {
				InstallableUnit iuToEncode = (InstallableUnit) iusToEncode.next();
				if (iuToEncode != entryPointIU) {
					processIU(iuToEncode, false);
				}
			}
			createConstraintsForSingleton();

			createMustHave(entryPointIU);

			optFunction = getOptimizationFactory(configuration.objective);
			setObjectiveFunction(optFunction.createOptimizationFunction(entryPointIU));
			if (TIMING) {
				Tracing.debug("Objective function contains " + solver.getObjectiveFunction().getVars().size() + " literals");
				long stop = System.currentTimeMillis();
				Tracing.debug("Projection completed: " + (stop - start) + "ms."); //$NON-NLS-1$
			}
			if (DEBUG_ENCODING) {
				Log.println(solver.toString());
			}
		} catch (IllegalStateException e) {
			result.add(new Status(IStatus.ERROR, Main.PLUGIN_ID, e.getMessage(), e));
			if (configuration.verbose) {
				Log.println("*** PBM *** " + e.getMessage());
			}
		} catch (ContradictionException e) {
			result.add(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unsatisfiable_problem));
			if (configuration.verbose) {
				Log.println("Unsat OPB problem ");
			}
		}
	}

	private OptimizationFunction getOptimizationFactory(String optFunctionName) {
		OptimizationFunction function = null;
		function = new UserDefinedOptimizationFunction2012(optFunctionName);
		Log.println("Optimization function: " + function.getName());
		function.slice = slice;
		function.noopVariables = noopVariables;
		function.picker = picker;
		function.dependencyHelper = dependencyHelper;
		function.optionalityVariables = optionalityVariables;
		function.optionalityPairs = optionalityPairs;
		return function;
	}

	private void setObjectiveFunction(List weightedObjects) {
		if (weightedObjects == null)
			return;
		if (DEBUG) {
			StringBuffer b = new StringBuffer();
			for (Iterator i = weightedObjects.iterator(); i.hasNext();) {
				WeightedObject object = (WeightedObject) i.next();
				if (b.length() > 0)
					b.append(", "); //$NON-NLS-1$
				b.append(object.getWeight());
				b.append(' ');
				b.append(object.thing);
			}
			Tracing.debug("objective function: " + b); //$NON-NLS-1$
		}
		dependencyHelper.setObjectiveFunction((WeightedObject[]) weightedObjects.toArray(new WeightedObject[weightedObjects.size()]));
	}

	private void createMustHave(InstallableUnit iu) throws ContradictionException {
		processIU(iu, true);
		if (DEBUG) {
			Tracing.debug(iu + "=1"); //$NON-NLS-1$
		}
		dependencyHelper.setTrue(iu, new Explanation.IUToInstall(iu));
		// assumptions.add(iu);
	}

	private void createNegation(InstallableUnit iu, IRequiredCapability req) throws ContradictionException {
		if (DEBUG) {
			Tracing.debug(iu + "=0"); //$NON-NLS-1$
		}
		dependencyHelper.setFalse(iu, new Explanation.MissingIU(iu, req));
	}

	private void expandNegatedRequirement(IRequiredCapability req, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
		IRequiredCapability negatedReq = ((NotRequirement) req).getRequirement();
		List matches = getApplicableMatches(negatedReq);
		matches.remove(iu);
		if (matches.isEmpty()) {
			return;
		}
		Explanation explanation;
		if (isRootIu) {
			InstallableUnit reqIu = (InstallableUnit) matches.iterator().next();
			explanation = new Explanation.IUToInstall(reqIu);
		} else {
			explanation = new Explanation.HardRequirement(iu, req);
		}
		createNegationImplication(iu, matches, explanation);
	}

	private void expandRequirement(IRequiredCapability req, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
		if (req.isNegation()) {
			expandNegatedRequirement(req, iu, isRootIu);
			return;
		}
		List matches = getApplicableMatches(req);
		if (!req.isOptional()) {
			if (matches.isEmpty()) {
				missingRequirement(iu, req);
			} else {
				if (req.getArity() == 1) {
					createAtMostOne((InstallableUnit[]) matches.toArray(new InstallableUnit[matches.size()]));
					return;
				}
				InstallableUnit reqIu = (InstallableUnit) matches.iterator().next();
				Explanation explanation = new Explanation.IUToInstall(reqIu);
				createImplication(iu, matches, explanation);
			}
		} else {
			AbstractVariable abs = getAbstractVariable(iu.toString() + "->" + req.toString());
			matches.add(abs);
			createImplication(iu, matches, Explanation.OPTIONAL_REQUIREMENT);
			optionalityVariables.add(abs);
			optionalityPairs.add(new Pair(iu, abs));
		}
	}

	private void expandRequirements(IRequiredCapability[] reqs, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
		if (reqs.length == 0) {
			return;
		}
		for (int i = 0; i < reqs.length; i++) {
			expandRequirement(reqs[i], iu, isRootIu);
		}
	}

	public void processIU(InstallableUnit iu, boolean isRootIU) throws ContradictionException {
		slice.put(iu.getId(), iu.getVersion(), iu);
		expandRequirements(getRequiredCapabilities(iu), iu, isRootIU);
	}

	private IRequiredCapability[] getRequiredCapabilities(InstallableUnit iu) {
		return iu.getRequiredCapabilities();
	}

	private void missingRequirement(InstallableUnit iu, IRequiredCapability req) throws ContradictionException {
		result.add(new Status(IStatus.WARNING, Main.PLUGIN_ID, NLS.bind(Messages.Planner_Unsatisfied_dependency, iu, req)));
		createNegation(iu, req);
	}

	/**
	 * @param req
	 * @return a list of mandatory requirements if any, an empty list if req.isOptional().
	 */
	private List getApplicableMatches(IRequiredCapability req) {
		List target = new ArrayList();
		Collector matches = picker.query(new CapabilityQuery(req), new Collector(), null);
		for (Iterator iterator = matches.iterator(); iterator.hasNext();) {
			InstallableUnit match = (InstallableUnit) iterator.next();
			target.add(match);
		}
		return target;
	}

	//This will create as many implication as there is element in the right argument
	private void createNegationImplication(Object left, List right, Explanation name) throws ContradictionException {
		if (DEBUG) {
			Tracing.debug(name + ": " + left + "->" + right); //$NON-NLS-1$ //$NON-NLS-2$
		}
		for (Iterator iterator = right.iterator(); iterator.hasNext();) {
			dependencyHelper.implication(new Object[] {left}).impliesNot(iterator.next()).named(name);
		}

	}

	private void createImplication(Object left, List right, Explanation name) throws ContradictionException {
		if (DEBUG) {
			Tracing.debug(name + ": " + left + "->" + right); //$NON-NLS-1$ //$NON-NLS-2$
		}
		dependencyHelper.implication(new Object[] {left}).implies(right.toArray()).named(name);
	}

	//Create constraints to deal with singleton
	//When there is a mix of singleton and non singleton, several constraints are generated
	private void createConstraintsForSingleton() throws ContradictionException {
		Set s = slice.entrySet();
		for (Iterator iterator = s.iterator(); iterator.hasNext();) {
			Map.Entry entry = (Map.Entry) iterator.next();
			HashMap conflictingEntries = (HashMap) entry.getValue();
			if (conflictingEntries.size() < 2)
				continue;

			Collection conflictingVersions = conflictingEntries.values();
			List singletons = new ArrayList();
			List nonSingletons = new ArrayList();
			for (Iterator conflictIterator = conflictingVersions.iterator(); conflictIterator.hasNext();) {
				InstallableUnit iu = (InstallableUnit) conflictIterator.next();
				if (iu.isSingleton()) {
					singletons.add(iu);
				} else {
					nonSingletons.add(iu);
				}
			}
			if (singletons.isEmpty())
				continue;

			InstallableUnit[] singletonArray;
			if (nonSingletons.isEmpty()) {
				singletonArray = (InstallableUnit[]) singletons.toArray(new InstallableUnit[singletons.size()]);
				createAtMostOne(singletonArray);
			} else {
				singletonArray = (InstallableUnit[]) singletons.toArray(new InstallableUnit[singletons.size() + 1]);
				for (Iterator iterator2 = nonSingletons.iterator(); iterator2.hasNext();) {
					singletonArray[singletonArray.length - 1] = (InstallableUnit) iterator2.next();
					createAtMostOne(singletonArray);
				}
			}
		}
	}

	private void createAtMostOne(InstallableUnit[] ius) throws ContradictionException {
		if (DEBUG) {
			StringBuffer b = new StringBuffer();
			for (int i = 0; i < ius.length; i++) {
				b.append(ius[i].toString());
			}
			Tracing.debug("At most 1 of " + b); //$NON-NLS-1$
		}
		dependencyHelper.atMost(1, ius).named(new Explanation.Singleton(ius));
	}

	private AbstractVariable getAbstractVariable(String name) {
		AbstractVariable abstractVariable = new AbstractVariable(name);
		abstractVariables.add(abstractVariable);
		return abstractVariable;
	}

	private void purge() {
		if (PURGE) {
			Iterator iusToEncode = picker.iterator();
			while (iusToEncode.hasNext()) {
				purgeIU((InstallableUnit) iusToEncode.next());
			}

			picker = null;
			noopVariables = null;
			abstractVariables = null;
			slice = null;
			//		assumptions = null;
		}
	}

	private boolean isSatisfiable;

	public IStatus invokeSolver() {
		purge();
		isSatisfiable = false;
		if (result.getSeverity() == IStatus.ERROR)
			return result;
		// CNF filename is given on the command line
		long start = System.currentTimeMillis();
		if (TIMING)
			Tracing.debug("Invoking solver ..."); //$NON-NLS-1$
		try {
			Log.println("p cnf " + dependencyHelper.getSolver().nVars() + " " + dependencyHelper.getSolver().nConstraints());
			if (dependencyHelper.hasASolution(assumptions)) {
				isSatisfiable = true;
				if (DEBUG) {
					Tracing.debug("Satisfiable !"); //$NON-NLS-1$
				}
				if (TIMING)
					Tracing.debug("Solver first solution found: " + (System.currentTimeMillis() - start) + "ms."); //$NON-NLS-1$
				backToIU();
				long stop = System.currentTimeMillis();
				if (TIMING)
					Tracing.debug("Solver best solution decoded: " + (stop - start) + "ms."); //$NON-NLS-1$
				if (configuration.verbose)
					dependencyHelper.getSolver().printStat(new PrintWriter(System.out, true), "# ");
			} else {
				long stop = System.currentTimeMillis();
				if (DEBUG) {
					Tracing.debug("Unsatisfiable !"); //$NON-NLS-1$
					Tracing.debug("Solver solution NOT found: " + (stop - start)); //$NON-NLS-1$
				}
				result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unsatisfiable_problem));
			}
		} catch (TimeoutException e) {
			result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Timeout));
			if (configuration.verbose) {
				Log.println("Timeout reached");
			}
		} catch (Exception e) {
			result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unexpected_problem, e));
			if (configuration.verbose) {
				Log.println("*** PBM *** " + e.getMessage());
			}
		}
		return result;
	}

	private void backToIU() {
		solution = null;
		if (!isSatisfiable)
			return;
		solution = new ArrayList();
		IVec sat4jSolution = dependencyHelper.getSolution();
		if (sat4jSolution.isEmpty())
			return;
		if (configuration.verbose && optFunction != null)
			optFunction.printSolutionValue();
		for (Iterator i = sat4jSolution.iterator(); i.hasNext();) {
			Object var = i.next();
			if (var instanceof InstallableUnit) {
				InstallableUnit iu = (InstallableUnit) var;
				if (iu == entryPoint)
					continue;
				solution.add(iu);
			}
		}
	}

	private void printSolution(Collection state) {
		ArrayList l = new ArrayList(state);
		Collections.sort(l);
		Tracing.debug("Solution:"); //$NON-NLS-1$
		Tracing.debug("Numbers of IUs selected: " + l.size()); //$NON-NLS-1$
		for (Iterator iterator = l.iterator(); iterator.hasNext();) {
			Tracing.debug(iterator.next().toString());
		}
	}

	public Collection extractSolution() {
		if (DEBUG)
			printSolution(solution);
		return solution;
	}

	public Set getExplanation() {
		ExplanationJob job = new ExplanationJob(dependencyHelper);
		job.schedule();
		IProgressMonitor pm = new NullProgressMonitor();
		pm.beginTask(Messages.Planner_NoSolution, 1000);
		try {
			synchronized (job) {
				while (job.getExplanationResult() == null && job.getState() != Job.NONE) {
					if (pm.isCanceled()) {
						job.cancel();
						throw new OperationCanceledException();
					}
					pm.worked(1);
					try {
						job.wait(100);
					} catch (InterruptedException e) {
						if (DEBUG)
							Tracing.debug("Interrupted while computing explanations"); //$NON-NLS-1$
					}
				}
			}
		} finally {
			pm.done();
		}
		return job.getExplanationResult();
	}

	public void stopSolver() {
		if (dependencyHelper != null)
			dependencyHelper.stopSolver();
	}

	public Collection getBestSolutionFoundSoFar() {
		if (solution == null) {
			backToIU();
		}
		if (solution == null)
			return null;
		return extractSolution();
	}
}