/**
 * Copyright (c) 2019, the Alpha Team.
 * All rights reserved.
 *
 * Additional changes made by Siemens.
 *
 * 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.programs.transformation;

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

import java.io.IOException;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.function.Function;

import org.junit.jupiter.api.Test;

import at.ac.tuwien.kr.alpha.api.AnswerSet;
import at.ac.tuwien.kr.alpha.api.Solver;
import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation;
import at.ac.tuwien.kr.alpha.api.config.SystemConfig;
import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program;
import at.ac.tuwien.kr.alpha.api.programs.Predicate;
import at.ac.tuwien.kr.alpha.api.programs.ProgramParser;
import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom;
import at.ac.tuwien.kr.alpha.commons.Predicates;
import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
import at.ac.tuwien.kr.alpha.commons.substitutions.Instance;
import at.ac.tuwien.kr.alpha.core.common.AtomStore;
import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl;
import at.ac.tuwien.kr.alpha.core.externals.Externals;
import at.ac.tuwien.kr.alpha.core.grounder.Grounder;
import at.ac.tuwien.kr.alpha.core.grounder.GrounderFactory;
import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl;
import at.ac.tuwien.kr.alpha.core.programs.AnalyzedProgram;
import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram;
import at.ac.tuwien.kr.alpha.core.programs.InternalProgram;
import at.ac.tuwien.kr.alpha.core.solver.SolverFactory;
import at.ac.tuwien.kr.alpha.core.test.util.TestUtils;

public class StratifiedEvaluationTest {

	private final ProgramParser parser = new ProgramParserImpl();
	private final NormalizeProgramTransformation normalizer = new NormalizeProgramTransformation(SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG);
	private final StratifiedEvaluation evaluator = new StratifiedEvaluation();
	private final Function<String, CompiledProgram> parseAndEvaluate = (str) -> {
		return evaluator.apply(AnalyzedProgram.analyzeNormalProgram(normalizer.apply(parser.parse(str))));
	};

	private final Function<CompiledProgram, Set<AnswerSet>> solveCompiledProg = (prog) -> {
		AtomStore atomStore = new AtomStoreImpl();
		Grounder grounder = GrounderFactory.getInstance("naive", prog, atomStore, false);
		Solver solver = SolverFactory.getInstance(new SystemConfig(), atomStore, grounder);
		return solver.collectSet();
	};

	@Test
	public void testDuplicateFacts() {
		String aspStr = "p(a). p(b). q(b). q(X) :- p(X).";
		CompiledProgram evaluated = parseAndEvaluate.apply(aspStr);
		Instance qOfB = new Instance(TestUtils.basicAtomWithSymbolicTerms("q", "b").getTerms());
		Set<Instance> facts = evaluated.getFactsByPredicate().get(Predicates.getPredicate("q", 1));
		int numQOfB = 0;
		for (Instance at : facts) {
			if (at.equals(qOfB)) {
				numQOfB++;
			}
		}
		assertEquals(1, numQOfB);
	}

	@Test
	public void testEqualityWithConstantTerms() {
		String aspStr = "equal :- 1 = 1.";
		CompiledProgram evaluated = parseAndEvaluate.apply(aspStr);
		Atom equal = TestUtils.basicAtomWithSymbolicTerms("equal");
		assertTrue(evaluated.getFacts().contains(equal));
	}

	@Test
	public void testEqualityWithVarTerms() {
		String aspStr = "a(1). a(2). a(3). b(X) :- a(X), X = 1. c(X) :- a(X), X = 2. d(X) :- X = 3, a(X).";
		CompiledProgram evaluated = parseAndEvaluate.apply(aspStr);
		Set<AnswerSet> answerSets = solveCompiledProg.apply(evaluated);
		TestUtils.assertAnswerSetsEqual("a(1), a(2), a(3), b(1), c(2), d(3)", answerSets);
	}

	@Test
	public void testNonGroundableRule() {
		String asp = "p(a). q(a, b). s(X, Y) :- p(X), q(X, Y), r(Y).";
		CompiledProgram evaluated = parseAndEvaluate.apply(asp);
		Set<AnswerSet> answerSets = solveCompiledProg.apply(evaluated);
		TestUtils.assertAnswerSetsEqual("p(a), q(a,b)", answerSets);
	}

	@Test
	public void testCountAggregate() {
		String asp = "a. b :- 1 <= #count { 1 : a }.";
		CompiledProgram evaluated = parseAndEvaluate.apply(asp);
		Set<AnswerSet> answerSets = solveCompiledProg.apply(evaluated);
		TestUtils.assertAnswerSetsEqual("a, b", answerSets);
	}

	@Test
	public void testIntervalFact() {
		String asp = "a(1..3).";
		CompiledProgram evaluated = parseAndEvaluate.apply(asp);
		Set<AnswerSet> answerSets = solveCompiledProg.apply(evaluated);
		TestUtils.assertAnswerSetsEqual("a(1), a(2), a(3)", answerSets);
	}

	@Test
	public void testAggregateSpecial() {
		String asp = "thing(1..3).\n" + "% choose exactly one - since Alpha doesn't support bounds,\n" + "% this needs two constraints\n"
				+ "{ chosenThing(X) : thing(X) }.\n" + "chosenSomething :- chosenThing(X).\n" + ":- not chosenSomething.\n"
				+ ":- chosenThing(X), chosenThing(Y), X != Y.\n" + "allThings :- 3 <= #count{ X : thing(X)}. \n"
				+ "chosenMaxThing :- allThings, chosenThing(3).\n" + ":- not chosenMaxThing.";
		CompiledProgram evaluated = parseAndEvaluate.apply(asp);
		assertTrue(evaluated.getFacts().contains(TestUtils.basicAtomWithSymbolicTerms("allThings")));
		Set<AnswerSet> answerSets = solveCompiledProg.apply(evaluated);
		TestUtils.assertAnswerSetsEqual("allThings, thing(1), thing(2), thing(3), chosenMaxThing, chosenSomething, chosenThing(3)", answerSets);
	}

	@Test
	public void testNegatedFixedInterpretationLiteral() {
		String asp = "stuff(1). stuff(2). smallStuff(X) :- stuff(X), not X > 1.";
		CompiledProgram evaluated = parseAndEvaluate.apply(asp);
		Set<AnswerSet> answerSets = solveCompiledProg.apply(evaluated);
		TestUtils.assertAnswerSetsEqual("stuff(1), stuff(2), smallStuff(1)", answerSets);
	}

	@SuppressWarnings("unused")
	@at.ac.tuwien.kr.alpha.api.externals.Predicate
	public static boolean sayTrue(Object o) {
		return true;
	}

	@Test
	public void testNegatedExternalLiteral() throws Exception {
		String asp = "claimedTruth(bla). truth(X) :- claimedTruth(X), &sayTrue[X]. lie(X) :- claimedTruth(X), not &sayTrue[X].";
		Map<String, PredicateInterpretation> externals = new HashMap<>();
		externals.put("sayTrue", Externals.processPredicateMethod(this.getClass().getMethod("sayTrue", Object.class)));
		ProgramParser parserWithExternals = new ProgramParserImpl();
		AnalyzedProgram analyzed = AnalyzedProgram.analyzeNormalProgram(normalizer.apply(parserWithExternals.parse(asp, externals)));
		CompiledProgram evaluated = new StratifiedEvaluation().apply(analyzed);
		Set<AnswerSet> answerSets = solveCompiledProg.apply(evaluated);
		TestUtils.assertAnswerSetsEqual("claimedTruth(bla), truth(bla)", answerSets);
	}

	/**
	 * Tests an encoding associated with the partner units problem (PUP) that computes a topological order to be used by
	 * domain-specific heuristics. The entire program can be solved by stratified evaluation.
	 */
	@Test
	public void testPartnerUnitsProblemTopologicalOrder() throws IOException {
		ASPCore2Program prg = parser.parse(StratifiedEvaluationTest.class.getResourceAsStream("/partial-eval/pup_topological_order.asp"));
		CompiledProgram evaluated = new StratifiedEvaluation().apply(AnalyzedProgram.analyzeNormalProgram(normalizer.apply(prg)));
		assertTrue(evaluated.getRules().isEmpty(), "Not all rules eliminated by stratified evaluation");
		assertEquals(57, evaluated.getFacts().size());
	}

	/**
	 * Verifies correct handling of negated basic literals in StratifiedEvaluation.
	 * For details, see comments in test program
	 * 
	 * @throws IOException
	 */
	@Test
	public void testNegatedLiteralInRecursiveRule() throws IOException {
		//@formatter:off
		String expectedAnswerSet = "basefact1(1), basefact2(1), max_value(10), min_value(1), "
				+ "basefact1(9), basefact2(9), base(1), base(9), "
				+ "inc_value(1), inc_value(2), inc_value(2), inc_value(3), "
				+ "inc_value(4), inc_value(5), inc_value(6), inc_value(7), "
				+ "inc_value(8)";
		//@formatter:on
		ASPCore2Program prog = new ProgramParserImpl().parse(
				StratifiedEvaluationTest.class.getResourceAsStream("/partial-eval/recursive_w_negated_condition.asp"),
				new HashMap<>());

		// Run stratified evaluation and solve
		CompiledProgram inputStratEval = new StratifiedEvaluation().apply(AnalyzedProgram.analyzeNormalProgram(normalizer.apply(prog)));
		Set<AnswerSet> asStrat = solveCompiledProg.apply(inputStratEval);
		TestUtils.assertAnswerSetsEqual(expectedAnswerSet, asStrat);

		// Solve without stratified evaluation
		CompiledProgram inputNoStratEval = InternalProgram.fromNormalProgram(normalizer.apply(prog));
		Set<AnswerSet> as = solveCompiledProg.apply(inputNoStratEval);
		TestUtils.assertAnswerSetsEqual(expectedAnswerSet, as);
	}

	@Test
	public void testRecursiveRanking() {
		//@formatter:off
		String asp = "thing(a).\n" + 
				"thing(b).\n" + 
				"thing(c).\n" + 
				"thing_before(a, b).\n" + 
				"thing_before(b, c).\n" + 
				"has_prev_thing(X) :- thing(X), thing_succ(_, X).\n" + 
				"first_thing(X) :- thing(X), not has_prev_thing(X).\n" + 
				"thing_not_succ(X, Y) :-\n" + 
				"	thing(X),\n" + 
				"	thing(Y),\n" + 
				"	thing(INTM),\n" + 
				"	thing_before(X, Y),\n" + 
				"	thing_before(X, INTM),\n" + 
				"	thing_before(INTM, X).\n" + 
				"thing_succ(X, Y) :-\n" + 
				"	thing(X),\n" + 
				"	thing(Y),\n" + 
				"	thing_before(X, Y),\n" + 
				"	not thing_not_succ(X, Y).\n" + 
				"thing_rank(X, 1) :- first_thing(X).\n" + 
				"thing_rank(X, R) :-\n" + 
				"	thing(X),\n" + 
				"	thing_succ(Y, X),\n" + 
				"	thing_rank(Y, K),\n" + 
				"	R = K + 1.";
		//@formatter:on
		CompiledProgram evaluated = parseAndEvaluate.apply(asp);
		Predicate rank = Predicates.getPredicate("thing_rank", 2);
		BasicAtom rank1 = Atoms.newBasicAtom(rank, Terms.newSymbolicConstant("a"), Terms.newConstant(1));
		BasicAtom rank2 = Atoms.newBasicAtom(rank, Terms.newSymbolicConstant("b"), Terms.newConstant(2));
		BasicAtom rank3 = Atoms.newBasicAtom(rank, Terms.newSymbolicConstant("c"), Terms.newConstant(3));
		List<Atom> evaluatedFacts = evaluated.getFacts();
		assertTrue(evaluatedFacts.contains(rank1));
		assertTrue(evaluatedFacts.contains(rank2));
		assertTrue(evaluatedFacts.contains(rank3));
	}

}
