content: package at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates;
  
  import static org.junit.jupiter.api.Assertions.assertEquals;
  import static org.junit.jupiter.api.Assertions.assertTrue;
  
  import java.util.List;
  
  import org.junit.jupiter.api.Test;
  
  import at.ac.tuwien.kr.alpha.api.programs.rules.Rule;
  import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head;
  import at.ac.tuwien.kr.alpha.core.test.util.RuleParser;
  
  public class AggregateLiteralSplittingTest {
  
  	//@formatter:off
  	public static final String LITERAL_SPLITTING_POS1_ASP = 
  			"count_between :- "
  				+ "X < #count{ N : thing2(N) } < Y, "
  				+ "X = #count{ K : thing1(K) },"
  				+ "Y = #count{ L : thing3(L) }.";
  	public static final String LITERAL_SPLITTING_POS2_ASP = 
  			"count_between :- "
  				+ "X < #count{ N : thing2(N) } < Y, "
  				+ "dom(X),"
  				+ "dom1(Y),"
  				+ "Y < #count{ L : thing3(L) } = Z.";
  	public static final String LITERAL_SPLITTING_NEG1_ASP =
  			"count_not_between :- "
  			+ "dom(X), dom(Y),"
  			+ "not X < #count{N : thing(N)} < Y.";
  	public static final String LITERAL_SPLITTING_NEG2_ASP =
  			"count_not_between :- "
  			+ "dom(X), dom(Y), dom(U), dom(V),"
  			+ "not X < #count{N : thing(N)} < Y,"
  			+ "not U < #count{K : thing(K)} < V.";
  	public static final String LITERAL_SPLITTING_NEG_POS_ASP =
  			"count_between_and_not_between(U, V, X, Y) :- "
  			+ "dom(X), dom(Y), dom(U), dom(V),"
  			+ "U < #count{K : thing(K)} < V,"
  			+ "not X < #count{N : thing(N)} < Y.";
  	//@formatter:on
  
  	@Test
  	public void singlePositiveLiteral() {
  		Rule<Head> inputRule = RuleParser.parse(LITERAL_SPLITTING_POS1_ASP);
  		Rule<Head> expectedRewrittenRule = RuleParser
  				.parse("count_between :- X < #count{N : thing2(N)}, Y > #count{N : thing2(N)}, X = #count{ K : thing1(K) }, Y = #count{ L : thing3(L) }.");
  		List<Rule<Head>> rewritten = AggregateLiteralSplitting.split(inputRule);
  		assertEquals(1, rewritten.size());
  		assertEquals(expectedRewrittenRule, rewritten.get(0));
  	}
  
  	@Test
  	public void multiplePositiveLiterals() {
  		Rule<Head> inputRule = RuleParser.parse(LITERAL_SPLITTING_POS2_ASP);
  		Rule<Head> expectedRewrittenRule = RuleParser
  				.parse("count_between :- X < #count{N : thing2(N)}, Y > #count{N : thing2(N)}, Y < #count{L : thing3(L)}, Z = #count{L : thing3(L)}, dom(X), dom1(Y).");
  		List<Rule<Head>> rewritten = AggregateLiteralSplitting.split(inputRule);
  		assertEquals(1, rewritten.size());
  		assertEquals(expectedRewrittenRule, rewritten.get(0));
  	}
  
  	@Test
  	public void singleNegativeLiteral() {
  		Rule<Head> inputRule = RuleParser.parse(LITERAL_SPLITTING_NEG1_ASP);
  		Rule<Head> expectedRewrittenRule1 = RuleParser
  				.parse("count_not_between :- dom(X), dom(Y), not X < #count{N : thing(N)}.");
  		Rule<Head> expectedRewrittenRule2 = RuleParser
  				.parse("count_not_between :- dom(X), dom(Y), not Y > #count{N : thing(N)}.");
  		List<Rule<Head>> rewritten = AggregateLiteralSplitting.split(inputRule);
  		assertEquals(2, rewritten.size());
  		assertTrue(rewritten.contains(expectedRewrittenRule1));
  		assertTrue(rewritten.contains(expectedRewrittenRule2));
  	}
  
  	@Test
  	public void multipleNegativeLiterals() {
  		Rule<Head> inputRule = RuleParser.parse(LITERAL_SPLITTING_NEG2_ASP);
  		Rule<Head> expectedRewrittenRule1 = RuleParser
  				.parse("count_not_between :- dom(X), dom(Y), dom(U), dom(V), not X < #count{N : thing(N)}, not U < #count{K : thing(K)}.");
  		Rule<Head> expectedRewrittenRule2 = RuleParser
  				.parse("count_not_between :- dom(X), dom(Y), dom(U), dom(V), not X < #count{N : thing(N)}, not V > #count{K : thing(K)}.");
  		Rule<Head> expectedRewrittenRule3 = RuleParser
  				.parse("count_not_between :- dom(X), dom(Y), dom(U), dom(V), not Y > #count{N : thing(N)}, not U < #count{K : thing(K)}.");
  		Rule<Head> expectedRewrittenRule4 = RuleParser
  				.parse("count_not_between :- dom(X), dom(Y), dom(U), dom(V), not Y > #count{N : thing(N)}, not V > #count{K : thing(K)}.");
  		List<Rule<Head>> rewritten = AggregateLiteralSplitting.split(inputRule);
  		assertEquals(4, rewritten.size());
  		assertTrue(rewritten.contains(expectedRewrittenRule1));
  		assertTrue(rewritten.contains(expectedRewrittenRule2));
  		assertTrue(rewritten.contains(expectedRewrittenRule3));
  		assertTrue(rewritten.contains(expectedRewrittenRule4));
  	}
  
  	@Test
  	public void negativeAndPositiveLiteral() {
  		Rule<Head> inputRule = RuleParser.parse(LITERAL_SPLITTING_NEG_POS_ASP);
  		Rule<Head> expectedRewrittenRule1 = RuleParser
  				.parse("count_between_and_not_between(U, V, X, Y) :- dom(X), dom(Y), dom(U), dom(V), not X < #count{N : thing(N)}, U < #count{K : thing(K)}, V > #count{K : thing(K)}.");
  		Rule<Head> expectedRewrittenRule2 = RuleParser
  				.parse("count_between_and_not_between(U, V, X, Y) :- dom(X), dom(Y), dom(U), dom(V), not Y > #count{N : thing(N)}, U < #count{K : thing(K)}, V > #count{K : thing(K)}.");
  		List<Rule<Head>> rewritten = AggregateLiteralSplitting.split(inputRule);
  		assertEquals(2, rewritten.size());
  		assertTrue(rewritten.contains(expectedRewrittenRule1));
  		assertTrue(rewritten.contains(expectedRewrittenRule2));
  	}
  
  }
  