/*
 * Solver.java
 *
 * Copyright (C) 2006 - 2007 Martin Slota
 *
 * This program is free software; you can redistribute it and/or modify it under
 * the terms of the GNU General Public License as published by the Free Software
 * Foundation; either version 2 of the License, or (at your option) any later
 * version.
 *
 * This program is distributed in the hope that it will be useful, but WITHOUT
 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
 * details.
 *
 * You should have received a copy of the GNU General Public License along with
 * this program; if not, write to the Free Software Foundation, Inc., 51
 * Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
 */

/*
 * History:
 * v1.0.0 (2007-05-06):
 * - contains common methods of LpSolver, DlpSolver and EvolpSolver
 *
 * PENDING create a junit test (tests of setLparsePath, setSmodelsPath and
 * setModelLimit; test of IllegalArgumentException in constructor...)
 */

package lp.trans;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.OutputStreamWriter;
import java.io.Writer;
import lp.struct.LpRule;
import lp.struct.util.LpPrettyPrinter;
import lp.struct.util.LpPrinter;
import lp.unit.LogicProgram;
import lp.util.ExceptionAdapter;
import lp.wrap.LparseWrapper;
import lp.wrap.SmodelsWrapper;
import lp.wrap.WrapperUtils;

/**
 * An abstract class that contains common functionality of classes used to
 * compute stable models of grounded logic programs ({@link LpSolver},
 * {@link DlpSolver} and {@link EvolpSolver}). The inheriting classes differ in
 * the way they interprete the resulting models (they may throw some computed
 * atoms away or transform them to different atoms).
 *
 * @author Martin Slota
 * @version 1.0.0
 * @see LpSolver
 * @see DlpSolver
 * @see EvolpSolver
 */
public abstract class Solver<M> {
	/**
	 * An {@link LparseWrapper} instance used to execute lparse before executing
	 * smodels.
	 */
	private final LparseWrapper lw;
	
	/**
	 * An {@link SmodelsWrapper} instance used to compute the stable models.
	 */
	private final SmodelsWrapper sw;
	
	/**
	 * The printer used to write a logic program to the {@link LparseWrapper}.
	 */
	private final LpPrinter<Writer> printer;
	
	/**
	 * Number of models that were computed.
	 */
	private int modelCount;
	
	/**
	 * Creates a new instance of that uses the given objects to invoke lparse
	 * and smodels when computing the stable models.
	 *
	 * @param lparseWrapper the object used to execute lparse
	 * @param smodelsWrapper the object used to execute smodels
	 */
	public Solver(LparseWrapper lparseWrapper,
			SmodelsWrapper smodelsWrapper) {
		if (lparseWrapper == null)
			throw new IllegalArgumentException(
					"The lparse wrapper object must not be null!");
		if (smodelsWrapper == null)
			throw new IllegalArgumentException(
					"The smodels wrapper object must not be null!");
		lw = lparseWrapper;
		sw = smodelsWrapper;
		printer = new LpPrettyPrinter<Writer>(null, ":-", false);
	}
	
	/**
	 * Sets the path to lparse binary that is used to invoke lparse.
	 *
	 * @param lparsePath path to the lparse binary
	 * @throws IllegalArgumentException if {@code lparsePath} is {@code null} or
	 * an empty string
	 */
	public void setLparsePath(String lparsePath) {
		lw.setLparsePath(lparsePath);
	}
	
	/**
	 * Sets the path to smodels binary that is used to invoke smodels.
	 *
	 * @param smodelsPath path to the smodels binary
	 * @throws IllegalArgumentException if {@code smodelsPath} is {@code null}
	 * or an empty string
	 */
	public void setSmodelsPath(String smodelsPath) {
		sw.setSmodelsPath(smodelsPath);
	}
	
	/**
	 * Sets the maximum number of stable models that should be computed by
	 * smodels. If set to zero, all models will be computed.
	 *
	 * @param modelLimit the maximum number of stable models that should be
	 * computed by smodels.
	 * @throws IllegalArgumentException if {@code modelLimit} is negative
	 */
	public void setModelLimit(int modelLimit) {
		sw.setModelLimit(modelLimit);
	}
	
	/**
	 * Computes the stable models of the grounded logic program {@code program}
	 * and passes them to {@code consumer}.
	 *
	 * @param program logic program whose stable models should be computed
	 * @param consumer object that processes the resulting models
	 *
	 * @throws IllegalArgumentException if {@code program} has not been grounded
	 * yet
	 *
	 * @throws IOException (wrapped in an {@link lp.util.ExceptionAdapter}) if
	 * an I/O error occurs while manipulating the standard input and output
	 * streams of an lparse process
	 *
	 * @throws WrapperException if an error occurs while calling lparse or
	 * smodels, see {@link LparseWrapper#waitFor()} and
	 * {@link SmodelsWrapper#waitFor()}.
	 *
	 * @throws LpParserException if an error occurs while the resulting models
	 * are being converted to their object representation (probably indicates a
	 * bug in this class)
	 */
	public void solve(LogicProgram program, Consumer<M> consumer) {
		if (!program.isGround())
			throw new IllegalArgumentException("The program must be grounded" +
					"before its models are computed!");
		
		lw.exec();
		
		printer.setOut(new OutputStreamWriter(lw.getStdin()));
		for (LpRule r : program) {
			printer.append(r);
			printer.append('\n');
		}
		printer.close();
		
		InputStream lparseOutput = lw.getStdout();
		
		sw.exec();
		WrapperUtils.getInstance().transfer(lparseOutput, sw.getStdin());
		sw.closeStdin();
		BufferedReader smodelsOutput = new BufferedReader(
				new InputStreamReader(sw.getStdout()));
		
		modelCount = 0;
		try {
			String modelString = getNextModelString(smodelsOutput);
			while (modelString != null) {
				modelCount++;
				consumer.consume(parseModel(modelString));
				modelString = getNextModelString(smodelsOutput);
			}
			smodelsOutput.close();
		} catch (IOException e) {
			throw new ExceptionAdapter(e);
		}
		
		lw.waitFor();
		sw.waitFor();
	}
	
	/**
	 * Returns the number of models that were computed.
	 *
	 * @return as specified above
	 */
	public int getModelCount() {
		return modelCount;
	}
	
	/**
	 * Returns the string containing space-separated atoms in the next model
	 * computed by smodels.
	 *
	 * @param smodelsOutput reader of the output of smodels
	 * @return as specified above
	 */
	protected static String getNextModelString(BufferedReader smodelsOutput)
	throws IOException {
		String INTRO = "Stable Model: ";
		String line = "";
		while (line != null && !line.startsWith(INTRO))
			line = smodelsOutput.readLine();
		if (line != null) {
			line = line.substring(INTRO.length());
			return line;
		}
		return null;
	}
	
	/**
	 * Parses {@code modelString} and returns the model that it represents.
	 *
	 * @param modelString a string representation of a model returned by smodels
	 * @return the object representation of the model
	 * @throws LpParserException if an error occurs while the resulting models
	 * are being converted to their object representation (probably indicates a
	 * bug in this class)
	 */
	protected abstract M parseModel(String modelString);
}