/*
 * LpSolverTest.java
 * JUnit based test
 *
 * 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:
 * v0.1 (2007-02-14): initial version
 * v0.1.5 (2007-02-14):
 * - 1 test added
 * v1.0.0 (2007-05-06):
 * - documentation added
 *
 * PENDING write more tests
 */

package lp.trans;

import java.util.HashSet;
import java.util.Set;
import junit.framework.*;
import lp.parse.LpParser;
import lp.unit.LogicProgram;
import lp.unit.StableModel;

/**
 * Contains tests of the {@link LpSolver} class.
 *
 * @author Martin Slota
 * @version 1.0.0
 * @see LpSolver
 */
public class LpSolverTest extends TestCase {
	/**
	 * The parser used in the tests.
	 */
	private final LpParser parser = new LpParser();
	
	/**
	 * The grounder used in the tests.
	 */
	private final LpGrounder grounder = new LpGrounder();
	
	/**
	 * The instance of {@link LpSolver} that is being tested.
	 */
	private final LpSolver solver = new LpSolver();
	
	/**
	 * Object for collecting the computed models.
	 */
	private final CollectingModelConsumer consumer =
			new CollectingModelConsumer();
	
	/**
	 * A default test case constructor.
	 *
	 * @param testName the name of the test case
	 */
	public LpSolverTest(String testName) {
		super(testName);
	}
	
	/**
	 * Tests {@link LpGrounder} on an empty input program.
	 *
	 * This test can only pass if both the lparse binary and the smodels binary
	 * can be executed by issuing simple {@code "lparse"} and
	 * {@code "smodels"} commands, respectively.
	 */
	public void testEmptyInput() {
		String programSource = "";
		Set<String> expModelSources = new HashSet<String>();
		expModelSources.add("");
		doTest(programSource, expModelSources);
	}
	
	/**
	 * Tests {@link LpGrounder} on a program containing only the rule
	 * "a :- not a.".
	 *
	 * This test can only pass if both the lparse binary and the smodels binary
	 * can be executed by issuing simple {@code "lparse"} and
	 * {@code "smodels"} commands, respectively.
	 */
	public void testKillerRule() {
		String programSource = "a :- not a.";
		Set<String> expModelSources = new HashSet<String>();
		doTest(programSource, expModelSources);
	}
	
	/**
	 * Tests {@link LpGrounder} on a typical program.
	 *
	 * This test can only pass if both the lparse binary and the smodels binary
	 * can be executed by issuing simple {@code "lparse"} and
	 * {@code "smodels"} commands, respectively.
	 */
	public void testOrdinaryInput() {
		String programSource = "date(1). date(2). date(3). date(4).\n" +
				"sunny(X) <- date(X), not rainy(X).\n" +
				"rainy(X) <- not sunny(X), date(X).";
		Set<String> expModelSources = new HashSet<String>();
		for (int i = 0; i < 16; i++) {
			StringBuilder sb = new StringBuilder();
			sb.append("date(1) date(2) date(3) date(4) ");
			sb.append((i % 2 == 0) ? "sunny(1) " : "rainy(1) ");
			sb.append((i % 4 < 2) ? "sunny(2) " : "rainy(2) ");
			sb.append((i % 8 < 4) ? "sunny(3) " : "rainy(3) ");
			sb.append((i < 8) ? "sunny(4) " : "rainy(4) ");
			expModelSources.add(sb.toString());
		}
		
		doTest(programSource, expModelSources);
	}
	
	/**
	 * Performs a single call of
	 *
	 *<pre>
	 *solver.solve(program);
	 *</pre>
	 *
	 * where {@code program} is the logic program obtained by parsing
	 * {@code programSource}. Then it tests if the expected set of models is
	 * computed.
	 *
	 * @param programSource the string with the input program
	 * @param expModelSources string representations of the expected models
	 */
	private void doTest(String programSource, Set<String> expModelSources) {
		parser.setInput(programSource);
		LogicProgram program = grounder.ground(parser.parseAllRules());
		parser.close();
		
		Set<StableModel> expModels = new HashSet<StableModel>();
		for (String expModelSource : expModelSources) {
			parser.setInput(expModelSource);
			StableModel expModel = new StableModel();
			while (parser.hasMoreTokens()) {
				expModel.add(parser.parseAtom());
			}
			expModels.add(expModel);
		}
		
		consumer.clear();
		solver.solve(program, consumer);
		
		assertEquals("The stable models are not as expected!",
				expModels, consumer);
	}
}