/**
 * Copyright (c) 2017 Siemens AG
 * All rights reserved.
 * 
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 * 
 * 1) Redistributions of source code must retain the above copyright notice, this
 *    list of conditions and the following disclaimer.
 * 
 * 2) Redistributions in binary form must reproduce the above copyright notice,
 *    this list of conditions and the following disclaimer in the documentation
 *    and/or other materials provided with the distribution.
 * 
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package at.ac.tuwien.kr.alpha.core.solver;

import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertFalse;

import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import java.util.Optional;
import java.util.stream.Collectors;

import org.junit.jupiter.api.Disabled;

import at.ac.tuwien.kr.alpha.api.AnswerSet;
import at.ac.tuwien.kr.alpha.api.Solver;
import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program;
import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl;
import at.ac.tuwien.kr.alpha.core.test.util.TestUtils;

/**
 * Tests rule transformations described in the following research paper, and their effects on performance:
 * 
 * Anger, Christian; Gebser, Martin; Janhunen, Tomi; Schaub, Torsten (2006): What's a head without a body? In G. Brewka, S. Coradeschi, A. Perini, P. Traverso
 * (Eds.): Proceedings of the Seventeenth European Conference on Artificial Intelligence (ECAI'06): IOS Press, pp. 769–770.
 *
 */
public class HeadBodyTransformationTests {

	private static final int DEBUG_TIMEOUT_FACTOR = 5;
	

	@RegressionTest
	public void testProgramB_N1(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB(1), cfg));
	}

	@RegressionTest
	public void testProgramB_Transformed_N1(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB_TransformationB(1), cfg));
	}

	@RegressionTest
	public void testProgramA_N1(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA(1), cfg));
	}

	@RegressionTest
	public void testProgramA_Transformed_N1(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA_TransformationA(1), cfg));
	}

	@RegressionTest
	public void testProgramB_N2(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB(2), cfg));
	}

	@RegressionTest
	public void testProgramB_Transformed_N2(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB_TransformationB(2), cfg));
	}

	@RegressionTest
	public void testProgramA_N2(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA(2), cfg));
	}

	@RegressionTest
	public void testProgramA_Transformed_N2(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA_TransformationA(2), cfg));
	}

	@RegressionTest
	public void testProgramB_N4(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB(4), cfg));
	}

	@RegressionTest
	public void testProgramB_Transformed_N4(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB_TransformationB(4), cfg));
	}

	@RegressionTest
	public void testProgramA_N4(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA(4), cfg));
	}

	@RegressionTest
	public void testProgramA_Transformed_N4(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA_TransformationA(4), cfg));
	}

	@RegressionTest
	public void testProgramB_N8(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB(8), cfg));
	}

	@RegressionTest
	public void testProgramB_Transformed_N8(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB_TransformationB(8), cfg));
	}

	@RegressionTest
	public void testProgramA_N8(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA(8), cfg));
	}

	@RegressionTest
	public void testProgramA_Transformed_N8(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA_TransformationA(8), cfg));
	}

	@RegressionTest
	@Disabled("disabled to save resources during CI")
	public void testProgramB_N16(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB(16), cfg));
	}

	@RegressionTest
	@Disabled("disabled to save resources during CI")
	public void testProgramB_Transformed_N16(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramB_TransformationB(16), cfg));
	}

	@RegressionTest
	@Disabled("disabled to save resources during CI")
	public void testProgramA_N16(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA(16), cfg));
	}

	@RegressionTest
	@Disabled("disabled to save resources during CI")
	public void testProgramA_Transformed_N16(RegressionTestConfig cfg) {
		long timeout = 10000L;
		TestUtils.runWithTimeout(cfg, timeout, DEBUG_TIMEOUT_FACTOR, () -> test(constructProgramA_TransformationA(16), cfg));
	}

	private void test(ASPCore2Program program, RegressionTestConfig cfg) {
		Solver solver = TestUtils.buildSolverForRegressionTest(program, cfg);
		Optional<AnswerSet> answerSet = solver.stream().findFirst();
		assertFalse(answerSet.isPresent());
	}

	/**
	 * Constructs program Pi^n_B from the paper
	 * 
	 * @param n
	 */
	private ASPCore2Program constructProgramB(int n) {
		int numberOfRules = 3 * n + 1;
		List<String> strRules = new ArrayList<>(numberOfRules);
		strRules.add("x :- not x.");
		strRules.addAll(createXRules(n));
		strRules.addAll(createABRules(n));
		return checkNumberOfRulesAndParse(strRules, numberOfRules);
	}

	/**
	 * Constructs program Pi^n_B transformed with Tau_B from the paper
	 * 
	 * @param n
	 */
	private ASPCore2Program constructProgramB_TransformationB(int n) {
		int numberOfRules = 6 * n + 2;
		List<String> strRules = new ArrayList<>(numberOfRules);
		strRules.add("b_notX :- not x.");
		strRules.add("x :- b_notX.");
		strRules.addAll(createXRules_TransformationB(n));
		strRules.addAll(createABRules_TransformationB(n));
		return checkNumberOfRulesAndParse(strRules, numberOfRules);
	}

	/**
	 * Constructs program Pi^n_a from the paper
	 * 
	 * @param n
	 */
	private ASPCore2Program constructProgramA(int n) {
		int numberOfRules = 4 * n + 1;
		List<String> strRules = new ArrayList<>(numberOfRules);
		strRules.add(createXCRule(n));
		strRules.addAll(createCRules(n));
		strRules.addAll(createABRules(n));
		return checkNumberOfRulesAndParse(strRules, numberOfRules);
	}

	/**
	 * Constructs program Pi^n_a from the paper
	 * 
	 * @param n
	 */
	private ASPCore2Program constructProgramA_TransformationA(int n) {
		int numberOfRules = 7 * n + 2;
		List<String> strRules = new ArrayList<>(numberOfRules);
		strRules.addAll(createXCRules_TransformationA(n));
		strRules.addAll(createCRules_TransformationA(n));
		strRules.addAll(createABRules_TransformationA(n));
		return checkNumberOfRulesAndParse(strRules, numberOfRules);
	}

	private ASPCore2Program checkNumberOfRulesAndParse(List<String> strRules, int numberOfRules) {
		assertEquals(numberOfRules, strRules.size());
		String strProgram = strRules.stream().collect(Collectors.joining(System.lineSeparator()));
		ASPCore2Program parsedProgram = new ProgramParserImpl().parse(strProgram);
		assertEquals(numberOfRules, parsedProgram.getRules().size());
		return parsedProgram;
	}

	private Collection<String> createXRules(int n) {
		Collection<String> rules = new ArrayList<>(n);
		for (int i = 1; i <= n; i++) {
			rules.add(String.format("x :- not a%d, not b%d.", i, i));
		}
		return rules;
	}

	private Collection<String> createXRules_TransformationB(int n) {
		Collection<String> rules = new ArrayList<>(n);
		for (int i = 1; i <= n; i++) {
			String beta = String.format("b_nota%dnotb%d", i, i);
			rules.add(String.format("%s :- not a%d, not b%d.", beta, i, i));
			rules.add(String.format("x :- %s.", beta));
		}
		return rules;
	}

	private Collection<String> createABRules(int n) {
		Collection<String> rules = new ArrayList<>(2 * n);
		for (int i = 1; i <= n; i++) {
			rules.add(String.format("a%d :- not b%d.", i, i));
			rules.add(String.format("b%d :- not a%d.", i, i));
		}
		return rules;
	}

	private Collection<String> createABRules_TransformationB(int n) {
		Collection<String> rules = new ArrayList<>(4 * n);
		for (int i = 1; i <= n; i++) {
			rules.add(String.format("b_notb%d :- not b%d.", i, i));
			rules.add(String.format("a%d :- b_notb%d.", i, i));
			rules.add(String.format("b_nota%d :- not a%d.", i, i));
			rules.add(String.format("b%d :- b_nota%d.", i, i));
		}
		return rules;
	}

	private Collection<String> createABRules_TransformationA(int n) {
		Collection<String> rules = new ArrayList<>(4 * n);
		for (int i = 1; i <= n; i++) {
			rules.add(String.format("a_a%d :- not b%d.", i, i));
			rules.add(String.format("a%d :- a_a%d.", i, i));
			rules.add(String.format("a_b%d :- not a%d.", i, i));
			rules.add(String.format("b%d :- a_b%d.", i, i));
		}
		return rules;
	}

	private String createXCRule(int n) {
		StringBuilder stringBuilder = new StringBuilder("x :- ");
		for (int i = 1; i <= n; i++) {
			stringBuilder.append(String.format("c%d, ", i));
		}
		stringBuilder.append("not x.");
		return stringBuilder.toString();
	}

	private Collection<? extends String> createXCRules_TransformationA(int n) {
		Collection<String> rules = new ArrayList<>(2);
		rules.add("x :- a_x.");
		rules.add("a_" + createXCRule(n));
		return rules;
	}

	private Collection<? extends String> createCRules(int n) {
		Collection<String> rules = new ArrayList<>(2 * n);
		for (int i = 1; i <= n; i++) {
			rules.add(String.format("c%d :- not a%d.", i, i));
			rules.add(String.format("c%d :- not b%d.", i, i));
		}
		return rules;
	}

	private Collection<? extends String> createCRules_TransformationA(int n) {
		Collection<String> rules = new ArrayList<>(3 * n);
		for (int i = 1; i <= n; i++) {
			rules.add(String.format("a_c%d :- not a%d.", i, i));
			rules.add(String.format("a_c%d :- not b%d.", i, i));
			rules.add(String.format("c%d :- a_c%d.", i, i));
		}
		return rules;
	}

}
