/**
 * Copyright (c) 2018-2019 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 at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSet;
import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSets;
import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSetsWithBase;
import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.ignoreTestForNaiveSolver;
import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.ignoreTestForSimplifiedSumAggregates;

/**
 * Tests if correct answer sets for programs containing aggregates are computed.
 */
public class AggregatesTest {

	private static final String LS = System.lineSeparator();
	
	@AggregateRegressionTest
	public void aggregateCountLeGroundPositive(RegressionTestConfig cfg) {
		String program = "a." + LS
				+ "b :- 1 <= #count { 1 : a }.";
		assertRegressionTestAnswerSet(cfg, program, "a,b");
	}

	@AggregateRegressionTest
	public void aggregateCountEqSingleElementPositive(RegressionTestConfig cfg) {
		String program = "thing(1..3)."
				+ "cnt_things(N) :- N = #count{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "thing(1), thing(2), thing(3), cnt_things(3)");
	}

	@AggregateRegressionTest
	public void aggregateCountEqEmptySetPositive(RegressionTestConfig cfg) {
		String program = "cnt_things(N) :- N = #count{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "cnt_things(0)");
	}

	@AggregateRegressionTest
	public void aggregateCountLeEmptySetPositive(RegressionTestConfig cfg) {
		String program = "zero_leq_cnt :- 0 <= #count{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "zero_leq_cnt");
	}

	@AggregateRegressionTest
	public void aggregateSumEqEmptySetPositive(RegressionTestConfig cfg) {
		String program = "sum_things(S) :- S = #sum{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "sum_things(0)");
	}
	
	@AggregateRegressionTest
	public void aggregateSumEqNegativeSum(RegressionTestConfig cfg) {
		ignoreTestForSimplifiedSumAggregates(cfg);
		String program = "thing(-1). thing(-2). thing(-3). sum_things(S) :- S = #sum{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "thing(-1), thing(-2), thing(-3), sum_things(-6)");
	}
	
	@AggregateRegressionTest
	public void aggregateSumEqMixedElementsSum(RegressionTestConfig cfg) {
		ignoreTestForSimplifiedSumAggregates(cfg);
		String program = "thing(-1). thing(6). thing(-3). sum_things(S) :- S = #sum{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "thing(-1), thing(6), thing(-3), sum_things(2)");		
	}

	@AggregateRegressionTest
	public void aggregateSumLeEmptySetPositive(RegressionTestConfig cfg) {
		String program = "zero_leq_sum :- 0 <= #sum{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "zero_leq_sum");
	}
	
	@AggregateRegressionTest
	public void aggregateSumLeNegativeSum(RegressionTestConfig cfg) {
		ignoreTestForSimplifiedSumAggregates(cfg);
		String program = "thing(-3). thing(4). "
				+ "minus_three_leq_sum :- -3 <= #sum{X : thing(X)}."
				+ "two_gt_sum :- 2 > #sum{X : thing(X)}.";
		assertRegressionTestAnswerSet(cfg, program, "thing(-3), thing(4), minus_three_leq_sum, two_gt_sum");
	}

	@AggregateRegressionTest
	public void aggregateSumLeNegativeElementsWithChoice(RegressionTestConfig cfg) {
		ignoreTestForSimplifiedSumAggregates(cfg);
		String program = "thing(3). thing(-5). thing(5). "
				+ "{summed_up_thing(X) : thing(X)}. "
				+ "seven_le :- 7 <= #sum{X : summed_up_thing(X)}.";
		assertRegressionTestAnswerSetsWithBase(cfg, program,
				"thing(-5), thing(3), thing(5)",
				"seven_le, summed_up_thing(3), summed_up_thing(5)",
				"summed_up_thing(5)",
				"summed_up_thing(3)",
				"summed_up_thing(-5)",
				"summed_up_thing(-5), summed_up_thing(3), summed_up_thing(5)",
				"summed_up_thing(-5), summed_up_thing(3)",
				"summed_up_thing(-5), summed_up_thing(5)",
				"");
	}
	
	@AggregateRegressionTest
	public void aggregateCountLeWithChoicePositive(RegressionTestConfig cfg) {
		String program = "potential_thing(1..4). "
				+ "{ thing(N) : potential_thing(N)}."
				+ "two_things_chosen :- thing(N1), thing(N2), N1 != N2."
				+ "three_things_chosen :- thing(N1), thing(N2), thing(N3), N1 != N2, N1 != N3, N2 != N3."
				+ ":- not two_things_chosen."
				+ ":- three_things_chosen."
				+ "two_leq_cnt :- 2 <= #count{ X : thing(X) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program,
				"potential_thing(1), potential_thing(2), potential_thing(3), potential_thing(4), two_things_chosen, two_leq_cnt",
				"thing(1), thing(2)",
				"thing(1), thing(3)",
				"thing(1), thing(4)",
				"thing(2), thing(3)",
				"thing(2), thing(4)",
				"thing(3), thing(4)");
	}

	@AggregateRegressionTest
	public void aggregateCountEqWithChoicePositive(RegressionTestConfig cfg) {
		String program = "potential_thing(1..4). "
				+ "{ thing(N) : potential_thing(N)}."
				+ "two_things_chosen :- thing(N1), thing(N2), N1 != N2."
				+ "three_things_chosen :- thing(N1), thing(N2), thing(N3), N1 != N2, N1 != N3, N2 != N3."
				+ ":- not two_things_chosen."
				+ ":- three_things_chosen."
				+ "cnt_things(CNT) :- CNT = #count{ X : thing(X) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program,
				"potential_thing(1), potential_thing(2), potential_thing(3), potential_thing(4), two_things_chosen, cnt_things(2)",
				"thing(1), thing(2)",
				"thing(1), thing(3)",
				"thing(1), thing(4)",
				"thing(2), thing(3)",
				"thing(2), thing(4)",
				"thing(3), thing(4)");
	}

	@AggregateRegressionTest
	public void aggregateSumEqWithChoicePositive(RegressionTestConfig cfg) {
		String program = "potential_thing(1..4). "
				+ "{ thing(N) : potential_thing(N)}."
				+ "two_things_chosen :- thing(N1), thing(N2), N1 != N2."
				+ "three_things_chosen :- thing(N1), thing(N2), thing(N3), N1 != N2, N1 != N3, N2 != N3."
				+ ":- not two_things_chosen."
				+ ":- three_things_chosen."
				+ "sum_things(SUM) :- SUM = #sum{ X : thing(X) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program,
				"potential_thing(1), potential_thing(2), potential_thing(3), potential_thing(4), two_things_chosen",
				"thing(1), thing(2), sum_things(3)",
				"thing(1), thing(3), sum_things(4)",
				"thing(1), thing(4), sum_things(5)",
				"thing(2), thing(3), sum_things(5)",
				"thing(2), thing(4), sum_things(6)",
				"thing(3), thing(4), sum_things(7)");
	}
	
	@AggregateRegressionTest
	public void aggregateSumEqOverMixedValuesWithChoicePositive(RegressionTestConfig cfg) {
		ignoreTestForSimplifiedSumAggregates(cfg);
		String program = "potential_thing(-2). potential_thing(-1). potential_thing(0). potential_thing(1). "
				+ "{ thing(N) : potential_thing(N)}."
				+ "two_things_chosen :- thing(N1), thing(N2), N1 != N2."
				+ "three_things_chosen :- thing(N1), thing(N2), thing(N3), N1 != N2, N1 != N3, N2 != N3."
				+ ":- not two_things_chosen."
				+ ":- three_things_chosen."
				+ "sum_things(SUM) :- SUM = #sum{ X : thing(X) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program,
				"potential_thing(-2), potential_thing(-1), potential_thing(0), potential_thing(1), two_things_chosen",
				"thing(-2), thing(-1), sum_things(-3)",
				"thing(-2), thing(0), sum_things(-2)",
				"thing(-2), thing(1), sum_things(-1)",
				"thing(-1), thing(0), sum_things(-1)",
				"thing(-1), thing(1), sum_things(0)",
				"thing(0), thing(1), sum_things(1)");
	}

	@AggregateRegressionTest
	public void aggregateSumBetweenNegative(RegressionTestConfig cfg) {
		String program = "potential_thing(1..4). "
				+ "{ thing(N) : potential_thing(N)}."
				+ "two_things_chosen :- thing(N1), thing(N2), N1 != N2."
				+ "three_things_chosen :- thing(N1), thing(N2), thing(N3), N1 != N2, N1 != N3, N2 != N3."
				+ ":- not two_things_chosen."
				+ ":- three_things_chosen."
				+ "sum_not_five :- not 4 < #sum{ X : thing(X) } < 6."
				+ ":- not sum_not_five."
				+ "sum_things(SUM) :- SUM = #sum{ X : thing(X) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program,
				"potential_thing(1), potential_thing(2), potential_thing(3), potential_thing(4), two_things_chosen, sum_not_five",
				"thing(1), thing(2), sum_things(3)",
				"thing(1), thing(3), sum_things(4)",
				"thing(2), thing(4), sum_things(6)",
				"thing(3), thing(4), sum_things(7)");
	}

	@AggregateRegressionTest
	public void aggregateMaxNegative(RegressionTestConfig cfg) {
		String program = "potential_thing(1..4). "
				+ "{ thing(N) : potential_thing(N) }."
				+ "one_chosen :- thing(_)."
				+ ":- not one_chosen."
				+ ":- thing(N1), thing(N2), N1 != N2."
				+ "max_chosen :- thing(X), not X < #max{M : potential_thing(M)}."
				+ ":- not max_chosen.";
		assertRegressionTestAnswerSet(cfg, program,
				"potential_thing(1), potential_thing(2), potential_thing(3), potential_thing(4), one_chosen, max_chosen, thing(4)");
	}

	@AggregateRegressionTest
	public void aggregateCountGroundNegative(RegressionTestConfig cfg) {
		String program = "{a}." + LS
				+ "b :- not c." + LS
				+ "c :- 1 <= #count { 1 : a }.";
		assertRegressionTestAnswerSets(cfg, program, "a,c", "b");
	}
	
	@AggregateRegressionTest
	public void aggregateCountNonGroundPositive(RegressionTestConfig cfg) {
		String program = "n(1..3)." + LS
				+ "{x(N)} :- n(N)." + LS
				+ "min(3)." + LS
				+ "ok :- min(M), M <= #count { N : n(N), x(N) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program, "n(1), n(2), n(3), min(3)",
				"", "x(1)", "x(2)", "x(3)", "x(1), x(2)", "x(1), x(3)",
				"x(2), x(3)", "x(1), x(2), x(3), ok");
	}
	
	@AggregateRegressionTest
	public void aggregateCountNonGroundLowerAndUpper(RegressionTestConfig cfg) {
		String program = "n(1..3)." + LS
				+ "{x(N)} :- n(N)." + LS
				+ "min(2)." + LS
				+ "max(2)." + LS
				+ "ok :- min(M), M <= #count { N : n(N), x(N) }, not exceedsMax." + LS
				+ "exceedsMax :- max(M), M1 = M + 1, M1 <= #count { N : n(N), x(N) }.";
		System.out.println(program);
		assertRegressionTestAnswerSetsWithBase(cfg, program, "n(1), n(2), n(3), min(2), max(2)",
				"", "x(1)", "x(2)", "x(3)", "x(1), x(2), ok", "x(1), x(3), ok",
				"x(2), x(3), ok", "x(1), x(2), x(3), exceedsMax");
	}
	
	@AggregateRegressionTest
	public void aggregateSumGroundLower(RegressionTestConfig cfg) {
		String program = "a." + LS
				+ "b :- 5 <= #sum { 2 : a; 3 }.";
		assertRegressionTestAnswerSet(cfg, program, "a,b");
	}
	
	@AggregateRegressionTest
	public void aggregateSumNonGroundLowerAndUpper(RegressionTestConfig cfg) {
		String program = "n(1..3)." + LS
				+ "{x(N)} :- n(N)." + LS
				+ "min(3)." + LS
				+ "max(4)." + LS
				+ "ok :- min(M), M <= #sum { N : n(N), x(N) }, not exceedsMax." + LS
				+ "exceedsMax :- max(M), M1 = M + 1, M1 <= #sum { N : n(N), x(N) }.";
		System.out.println(program);
		assertRegressionTestAnswerSetsWithBase(cfg, program, "n(1), n(2), n(3), min(3), max(4)",
				"", "x(1)", "x(2)", "x(3), ok", "x(1), x(2), ok", "x(1), x(3), ok",
				"x(2), x(3), exceedsMax", "x(1), x(2), x(3), exceedsMax");
	}
	
	@AggregateRegressionTest
	public void aggregateSumNonGroundLower(RegressionTestConfig cfg) {
		String program = "n(1..3)." + LS
				+ "{x(N)} :- n(N)." + LS
				+ "min(3)." + LS
				+ "ok :- min(M), M <= #sum { N : n(N), x(N) }.";
		System.out.println(program);
		assertRegressionTestAnswerSetsWithBase(cfg, program, "n(1), n(2), n(3), min(3)",
				"", "x(1)", "x(2)", "x(3), ok", "x(1), x(2), ok", "x(1), x(3), ok",
				"x(2), x(3), ok", "x(1), x(2), x(3), ok");
	}

	@AggregateRegressionTest
	public void aggregateSumComputed(RegressionTestConfig cfg) {
		ignoreTestForNaiveSolver(cfg); // Do not run this test case with the naive solver.
		String program = "n(1..3)." + LS
				+ "{x(N)} :- n(N)." + LS
				+ "potential_sum(0..6)." + LS
				+ "min(S) :- S <= #sum { N : n(N), x(N) }, potential_sum(S)." + LS
				+ "sum(S) :- min(S), not min(Sp1), Sp1 = S+1.";
		assertRegressionTestAnswerSetsWithBase(cfg, program, "n(1), n(2), n(3), potential_sum(0), potential_sum(1), "
				+ "potential_sum(2), potential_sum(3), potential_sum(4), potential_sum(5), potential_sum(6)",
				"min(0), sum(0)",
				"x(1), min(0), min(1), sum(1)",
				"x(2), min(0), min(1), min(2), sum(2)",
				"x(3), min(0), min(1), min(2), min(3), sum(3)",
				"x(1), x(2), min(0), min(1), min(2), min(3), sum(3)",
				"x(1), x(3), min(0), min(1), min(2), min(3), min(4), sum(4)",
				"x(2), x(3), min(0), min(1), min(2), min(3), min(4), min(5), sum(5)",
				"x(1), x(2), x(3), min(0), min(1), min(2), min(3), min(4), min(5), min(6), sum(6)");
	}
	
	@AggregateRegressionTest
	public void aggregateCountGlobalVariable(RegressionTestConfig cfg) {
		String program = "box(1..2)." + LS
				+ "in(1,1)." + LS
				+ "in(1,2)." + LS
				+ "in(2,2)." + LS
				+ "full(B) :- box(B), 2 <= #count { I : in(I,B) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program, "box(1), box(2), in(1,1), in(1,2), in(2,2)",
				"full(2)");
	}
	
	@AggregateRegressionTest
	public void aggregateSumGlobalVariable(RegressionTestConfig cfg) {
		String program = "box(1..2)." + LS
				+ "item_size(I,I) :- I=1..2." + LS
				+ "in(1,1)." + LS
				+ "in(1,2)." + LS
				+ "in(2,2)." + LS
				+ "full(B) :- box(B), 3 <= #sum { S : item_size(I,S), in(I,B) }.";
		assertRegressionTestAnswerSetsWithBase(cfg, program, "box(1), box(2), item_size(1,1), item_size(2,2), in(1,1), in(1,2), in(2,2)",
				"full(2)");
	}

	@AggregateRegressionTest
	public void aggregateRightHandTermCountGreater(RegressionTestConfig cfg) {
		String program = "p(1)." + 
			"p(2)." + 
			"q :- #count { N : p(N) } > 1.";
		assertRegressionTestAnswerSet(cfg, program, "p(1), p(2), q");
	}

	@AggregateRegressionTest
	public void aggregateRightHandTermCountEqAssigning(RegressionTestConfig cfg) {
		String program = "p(1)." + 
			"p(2)." + 
			"q :- #count { N : p(N) } = 2.";
		assertRegressionTestAnswerSet(cfg, program, "p(1), p(2), q");
	}

	@AggregateRegressionTest
	public void aggregateRightHandTermCountNeqAssigning(RegressionTestConfig cfg) {
		String program = "p(1)." + 
			"p(2)." + 
			"q :- #count { N : p(N) } != 1.";
		assertRegressionTestAnswerSet(cfg, program, "p(1), p(2), q");
	}

	@AggregateRegressionTest
	public void aggregateRightHandTermCountLt(RegressionTestConfig cfg) {
		String program = "p(1)." + 
			"p(2)." + 
			"q :- #count { N : p(N) } < 3.";
		assertRegressionTestAnswerSet(cfg, program, "p(1), p(2), q");
	}

}
