/**
 * Copyright (c) 2017-2018, 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.api.impl;

import at.ac.tuwien.kr.alpha.api.Alpha;
import at.ac.tuwien.kr.alpha.api.AnswerSet;
import at.ac.tuwien.kr.alpha.api.config.Heuristic;
import at.ac.tuwien.kr.alpha.api.config.InputConfig;
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.NormalProgram;
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.api.programs.rules.Rule;
import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head;
import at.ac.tuwien.kr.alpha.api.programs.terms.ConstantTerm;
import at.ac.tuwien.kr.alpha.api.programs.tests.TestResult;
import at.ac.tuwien.kr.alpha.commons.AnswerSetBuilder;
import at.ac.tuwien.kr.alpha.commons.Predicates;
import at.ac.tuwien.kr.alpha.commons.programs.Programs;
import at.ac.tuwien.kr.alpha.commons.programs.Programs.ASPCore2ProgramBuilder;
import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
import at.ac.tuwien.kr.alpha.commons.programs.literals.Literals;
import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules;
import at.ac.tuwien.kr.alpha.commons.programs.rules.heads.Heads;
import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
import at.ac.tuwien.kr.alpha.core.common.fixedinterpretations.MethodPredicateInterpretation;
import at.ac.tuwien.kr.alpha.core.externals.AspStandardLibrary;
import at.ac.tuwien.kr.alpha.core.externals.Externals;
import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl;
import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram;
import org.junit.jupiter.api.Disabled;
import org.junit.jupiter.api.Test;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.nio.file.StandardOpenOption;
import java.util.*;
import java.util.stream.Collectors;

import static java.util.Arrays.asList;
import static java.util.Collections.*;
import static org.junit.jupiter.api.Assertions.*;

public class AlphaImplTest {

	private static final Logger LOGGER = LoggerFactory.getLogger(AspStandardLibrary.class);

	//@formatter:off
	private static final String STRINGSTUFF_ASP =
			"string(\"bla\")."
			+ "string(\"blubb\")."
			+ "string(\"foo\")."
			+ "string(\"bar\")."
			+ "{ strcat(S1, S2) } :- string(S1), string(S2)."
			+ "resultstring(SCAT) :- strcat(S1, S2), &stdlib_string_concat[S1, S2](SCAT)."
			+ ":- resultstring(S), &stdlib_string_length[S](LEN), LEN != 6."
			+ "containsFoo(S) :- resultstring(S), &stdlib_string_matches_regex[S, \".*foo.*\"]."
			+ ":- resultstring(S), not containsFoo(S)."
			+ "has_resultstring :- resultstring(_)."
			+ ":- not has_resultstring.";
	
	// same as stringstuff asp, but without the "containsFoo" intermediate predicate
	private static final String NEGATED_EXTERNAL_ASP =
			"string(\"bla\")."
			+ "string(\"blubb\")."
			+ "string(\"foo\")."
			+ "string(\"bar\")."
			+ "{ strcat(S1, S2) } :- string(S1), string(S2)."
			+ "resultstring(SCAT) :- strcat(S1, S2), &stdlib_string_concat[S1, S2](SCAT)."
			+ ":- resultstring(S), &stdlib_string_length[S](LEN), LEN != 6."
			+ ":- resultstring(S), not &stdlib_string_matches_regex[S, \".*foo.*\"]."
			+ "has_resultstring :- resultstring(_)."
			+ ":- not has_resultstring.";
	//@formatter:on

	private static final String UNIT_TEST_EXPECT_UNSAT =
			"p(1). p(2). "
			+ ":- p(X), p(Y), X + Y = 3."
			+ "#test expected_unsat(expect: unsat) {"
			+ "given {}"
			+ "}";

	private static final String UNIT_TEST_BASIC_TEST =
			"a :- b. #test ensure_a(expect: 1) { given { b. } assertForAll { :- not a. } }";
	private static final String UNIT_TEST_MORE_ASSERTIONS =
			"a :- b. #test ensure_a(expect: 1) { given { b. } assertForAll { :- not a. } assertForSome { :- not a.} }";

	private static final String UNIT_TEST_MORE_TCS =
			"a :- b. #test ensure_a(expect: 1) { given { b. } assertForAll { :- not a. }} " +
					"#test ensure_not_c (expect: 1) { given { b.} assertForAll { :- c. }}";

	private static final String UNIT_TEST_FAILING_ASSERTION =
			"a :- b. #test ensure_c(expect: 1) { given { b. } assertForAll { :- not c. } }";

	private static final String UNIT_TEST_FAILING_COUNT =
			"a :- b. #test ensure_a(expect: 2) { given { b. } assertForAll { :- not a. } }";

	private static int invocations;

	@at.ac.tuwien.kr.alpha.api.externals.Predicate
	public static boolean isOne(int term) {
		invocations++;
		return term == 1;
	}

	@at.ac.tuwien.kr.alpha.api.externals.Predicate
	public static boolean isFoo(Integer a) {
		return a == 0xF00;
	}

	@SuppressWarnings("unused")
	@at.ac.tuwien.kr.alpha.api.externals.Predicate
	public static boolean thinger(Thingy thingy) {
		return true;
	}

	@Test
	public void withExternal() throws Exception {
		Alpha alpha = new AlphaImpl();
		InputConfig inputCfg = InputConfig.forString("a :- &isOne[1].");
		inputCfg.addPredicateMethod("isOne", Externals.processPredicateMethod(this.getClass().getMethod("isOne", int.class)));
		ASPCore2Program program = alpha.readProgram(inputCfg);
		Set<AnswerSet> actual = alpha.solve(program).collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").build()));
		assertEquals(expected, actual);
	}

	@Test
	public void addsFacts() {
		Alpha system = new AlphaImpl();
		Thingy a = new Thingy();
		Thingy b = new Thingy();
		List<Thingy> things = asList(a, b);
		ASPCore2Program program = Programs.builder().addFacts(Externals.asFacts(Thingy.class, things)).build();
		Set<AnswerSet> actual = system.solve(program).collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("thingy").instance(a).instance(b).build()));
		assertEquals(expected, actual);
	}

	@Test
	public void withExternalTypeConflict() {
		assertThrows(IllegalArgumentException.class, () -> {
			Alpha system = new AlphaImpl();
			InputConfig inputCfg = InputConfig.forString("a :- &isFoo[\"adsfnfdsf\"].");
			inputCfg.addPredicateMethod("isFoo", Externals.processPredicateMethod(this.getClass().getMethod("isFoo", Integer.class)));
			Set<AnswerSet> actual = system.solve(system.readProgram(inputCfg)).collect(Collectors.toSet());
			Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").build()));
			assertEquals(expected, actual);
		});
	}

	@Test
	public void smallGraph() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig inputCfg = InputConfig.forString("node(1). node(2). node(3). a :- &connected[1,2].");
		inputCfg.addPredicateMethod("connected", Externals.processPredicate((Integer a, Integer b) -> (a == 1 && b == 2) || (b == 2 || b == 3)));
		ASPCore2Program program = system.readProgram(inputCfg);

		Set<AnswerSet> actual = system.solve(program).collect(Collectors.toSet());
		Set<AnswerSet> expected = AnswerSetsParser.parse("{ a, node(1), node(2), node(3) }");
		assertEquals(expected, actual);
	}

	@Test
	public void filterOutput() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig inputCfg = InputConfig.forString("node(1). node(2). outgoing13(X) :- node(X), &getLargeGraphEdges(13,X).");
		inputCfg.addPredicateMethod("getLargeGraphEdges",
				Externals.processPredicate(() -> new HashSet<>(asList(asList(Terms.newConstant(1), Terms.newConstant(2)),
						asList(Terms.newConstant(2), Terms.newConstant(1)), asList(Terms.newConstant(13), Terms.newConstant(1))))));
		ASPCore2Program program = system.readProgram(inputCfg);
		Set<AnswerSet> actual = system.solve(program).collect(Collectors.toSet());
		Set<AnswerSet> expected = AnswerSetsParser.parse("{ node(1), node(2), outgoing13(1) }");
		assertEquals(expected, actual);
	}

	@Test
	public void supplier() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("node(1). a :- &bestNode(X), node(X).");
		cfg.addPredicateMethod("bestNode", Externals.processPredicate(() -> singleton(singletonList(Terms.newConstant(1)))));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> expected = AnswerSetsParser.parse("{ node(1), a }");
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		assertEquals(expected, actual);
	}

	@at.ac.tuwien.kr.alpha.api.externals.Predicate
	public static Set<List<ConstantTerm<?>>> bestNode() {
		return singleton(singletonList(Terms.newConstant(1)));
	}

	@Test
	public void noInput() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("node(1). a :- &bestNode(X), node(X).");
		cfg.addPredicateMethod("bestNode", Externals.processPredicateMethod(this.getClass().getMethod("bestNode")));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> expected = AnswerSetsParser.parse("{ node(1), a }");
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		assertEquals(expected, actual);
	}

	@Test
	public void smallGraphWithWrongType() {
		assertThrows(IllegalArgumentException.class, () -> {
			Alpha system = new AlphaImpl();
			InputConfig cfg = InputConfig.forString("a :- &connected[\"hello\",2].");
			cfg.addPredicateMethod("connected", Externals.processPredicate((Integer a, Integer b) -> (a == 1 && b == 2) || (b == 2 || b == 3)));
			ASPCore2Program prog = system.readProgram(cfg);

			system.solve(prog).collect(Collectors.toSet());
		});
	}

	public static Set<List<ConstantTerm<Integer>>> neighbors(int node) {
		if (node == 1) {
			return new HashSet<>(asList(singletonList(Terms.newConstant(2)), singletonList(Terms.newConstant(3))));
		}
		return emptySet();
	}

	public static Set<List<ConstantTerm<Integer>>> coolNode(int node) {
		if (node == 1) {
			return singleton(emptyList());
		}
		return emptySet();
	}

	@Test
	@Disabled("Test program is not safe (external lacking output variables). This should throw some exception.")
	public void smallGraphNoNeighbors() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("noNeighbors(2) :- not &neighbors[2].");
		cfg.addPredicateMethod("neighbors", Externals.processPredicateMethod(this.getClass().getMethod("neighbors", int.class)));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> expected = AnswerSetsParser.parse("{ noNeighbors(2) }");
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		assertEquals(expected, actual);
	}

	@Test
	public void smallGraphCoolNode() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("node(1..2). in(X) :- node(X), &coolNode[X].");
		cfg.addPredicateMethod("coolNode", Externals.processPredicateMethod(this.getClass().getMethod("coolNode", int.class)));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		Set<AnswerSet> expected = AnswerSetsParser.parse("{ in(1), node(1), node(2) }");
		assertEquals(expected, actual);
	}

	@Test
	public void smallGraphSingleNeighbor() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("node(1..3). in(1,X) :- &neighbors[1](X), node(X).");
		cfg.addPredicateMethod("neighbors", Externals.processPredicateMethod(this.getClass().getMethod("neighbors", int.class)));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> expected = AnswerSetsParser.parse("{ in(1,2), in(1,3), node(1), node(2), node(3) }");
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		assertEquals(expected, actual);
	}

	@Test
	@Disabled("Test program is not safe (external lacking output variables). This should throw some exception.")
	public void smallGraphSingleNeighborNoTerm() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("success :- &neighbors[1], not &neighbors[2].");
		cfg.addPredicateMethod("neighbors", Externals.processPredicateMethod(this.getClass().getMethod("neighbors", int.class)));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> expected = AnswerSetsParser.parse("{ success }");
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		assertEquals(expected, actual);
	}

	private static class Thingy implements Comparable<Thingy> {
		@Override
		public String toString() {
			return "thingy";
		}

		@Override
		public int compareTo(Thingy o) {
			return 0;
		}
	}

	private static class SubThingy extends Thingy {
	}

	@Test
	public void withExternalSubtype() throws Exception {
		SubThingy thingy = new SubThingy();

		Rule<Head> rule = Rules.newRule(
				Heads.newNormalHead(Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Terms.newConstant("x"))),
				singletonList(Literals.fromAtom(Atoms.newExternalAtom(Predicates.getPredicate("thinger", 1),
						new MethodPredicateInterpretation(this.getClass().getMethod("thinger", Thingy.class)), singletonList(Terms.newConstant(thingy)),
						emptyList()), true)));

		Alpha system = new AlphaImpl();

		ASPCore2Program prog = Programs.newASPCore2Program(singletonList(rule), emptyList(), Programs.newInlineDirectives());

		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("p").instance("x").build()));
		assertEquals(expected, actual);
	}

	@Test
	public void withExternalViaAnnotation() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("a :- &isOne[1].");
		cfg.addPredicateMethods(Externals.scan(this.getClass()));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").build()));
		assertEquals(expected, actual);
	}

	/**
	 * Externals may only be scanned once per implementation.
	 * If at the time of a scan, the name of an external is already registered,
	 * an exception is thrown.
	 */
	@Test
	public void errorDuplicateExternal() {
		assertThrows(IllegalArgumentException.class, () -> {
			InputConfig cfg = InputConfig.forString("someString.");
			cfg.addPredicateMethods(Externals.scan(this.getClass()));
			cfg.addPredicateMethods(Externals.scan(this.getClass()));
		});
	}

	@Test
	public void withNativeExternal() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("a :- &isTwo[2].");
		cfg.addPredicateMethod("isTwo", Externals.processPredicate((Integer t) -> t == 2));
		ASPCore2Program prog = system.readProgram(cfg);

		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").build()));
		assertEquals(expected, actual);
	}

	@Test
	@Disabled("External atom has state, which is not allowed. Caching of calls makes the number of invocations wrong.")
	public void withExternalInvocationCounted1() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("a :- &isOne[1], &isOne[1].");
		cfg.addPredicateMethod("isOne", Externals.processPredicateMethod(this.getClass().getMethod("isOne", int.class)));
		ASPCore2Program prog = system.readProgram(cfg);

		int before = invocations;
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		int after = invocations;

		assertEquals(2, after - before);

		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").build()));
		assertEquals(expected, actual);
	}

	@Test
	@Disabled("External atom has state, which is not allowed. Caching of calls makes the number of invocations wrong.")
	public void withExternalInvocationCounted2() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("a. b :- &isOne[1], &isOne[2].");
		cfg.addPredicateMethod("isOne", Externals.processPredicateMethod(this.getClass().getMethod("isOne", int.class)));
		ASPCore2Program prog = system.readProgram(cfg);

		int before = invocations;
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		int after = invocations;

		assertEquals(2, after - before);

		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").build()));
		assertEquals(expected, actual);
	}

	@Test
	@Disabled("External atom has state, which is not allowed. Caching of calls makes the number of invocations wrong.")
	public void withExternalInvocationCounted3() throws Exception {
		Alpha system = new AlphaImpl();
		InputConfig cfg = InputConfig.forString("a :- &isOne[1], not &isOne[2].");
		cfg.addPredicateMethod("isOne", Externals.processPredicateMethod(this.getClass().getMethod("isOne", int.class)));
		ASPCore2Program prog = system.readProgram(cfg);

		int before = invocations;
		Set<AnswerSet> actual = system.solve(prog).collect(Collectors.toSet());
		int after = invocations;

		assertEquals(1, after - before);

		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").build()));
		assertEquals(expected, actual);
	}

	@Test
	@SuppressWarnings("unchecked")
	public void programWithExternalStringStuff() throws IOException {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgram(InputConfig.forString(STRINGSTUFF_ASP));
		Set<AnswerSet> answerSets = alpha.solve(prog).collect(Collectors.toSet());
		// Verify every result string has length 6 and contains "foo"
		for (AnswerSet as : answerSets) {
			for (Atom atom : as.getPredicateInstances(Predicates.getPredicate("resultstring", 1))) {
				String resultstring = ((ConstantTerm<String>) atom.getTerms().get(0)).getObject();
				assertEquals(6, resultstring.length());
				assertTrue(resultstring.contains("foo"));
			}
		}
	}

	@Test
	@SuppressWarnings("unchecked")
	public void withNegatedExternal() throws IOException {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgram(InputConfig.forString(NEGATED_EXTERNAL_ASP));
		Set<AnswerSet> answerSets = alpha.solve(prog).collect(Collectors.toSet());
		assertEquals(31, answerSets.size());
		// Verify every result string has length 6 and contains "foo"
		for (AnswerSet as : answerSets) {
			for (Atom atom : as.getPredicateInstances(Predicates.getPredicate("resultstring", 1))) {
				String resultstring = ((ConstantTerm<String>) atom.getTerms().get(0)).getObject();
				LOGGER.debug("ResultString is {}", resultstring);
				assertEquals(6, resultstring.length());
				assertTrue(resultstring.contains("foo"));
			}
		}
	}

	@Test
	public void reifyInput() {
		String aspInput = "p(X) :- q(X), not r(X).";
		Alpha system = new AlphaImpl();
		ASPCore2Program input = system.readProgramString(aspInput);
		Set<BasicAtom> reified = system.reify(input);

		Set<BasicAtom> reifiedPredicates = reified.stream()
				.filter((a) -> a.getPredicate().equals(Predicates.getPredicate("predicate", 3)))
				.collect(Collectors.toSet());
		Set<BasicAtom> reifiedRuleHeads = reified.stream()
				.filter((a) -> a.getPredicate().equals(Predicates.getPredicate("rule_head", 2)))
				.collect(Collectors.toSet());
		Set<BasicAtom> reifiedBodyLiterals = reified.stream()
				.filter((a) -> a.getPredicate().equals(Predicates.getPredicate("rule_bodyLiteral", 2)))
				.collect(Collectors.toSet());
		assertEquals(3, reifiedPredicates.size());
		assertEquals(1, reifiedRuleHeads.size());
		assertEquals(2, reifiedBodyLiterals.size());
	}

	@Test
	public void basicUsage() throws Exception {
		Alpha system = new AlphaImpl();
		Set<AnswerSet> actual = system.solve(system.readProgram(InputConfig.forString("p(a)."))).collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("p").symbolicInstance("a").build()));
		assertEquals(expected, actual);
	}

	@Test
	public void basicUsageWithString() throws Exception {
		Alpha system = new AlphaImpl();
		Set<AnswerSet> actual = system.solve(system.readProgram(InputConfig.forString("p(\"a\")."))).collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("p").instance("a").build()));
		assertEquals(expected, actual);
	}

	/**
	 * Verifies that filters are handled correctly (regression test case introduced when fixing issue #189).
	 */
	@Test
	public void filterTest() {
		String progstr = "a. b. c. d :- c. e(a, b) :- d.";
		Alpha system = new AlphaImpl();
		ASPCore2Program prog = system.readProgramString(progstr);
		Set<AnswerSet> actual = system.solve(prog, (p) -> p.equals(Predicates.getPredicate("a", 0)) || p.equals(Predicates.getPredicate("e", 2)))
				.collect(Collectors.toSet());
		Set<AnswerSet> expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("a").predicate("e").symbolicInstance("a", "b").build()));
		assertEquals(expected, actual);
	}

	/**
	 * Verifies that no stratified evaluation is performed up-front when disabled in config.
	 */
	@Test
	public void disableStratifiedEvalTest() {
		// Note: This might be cleaner if the test used the debugSolve method from the interface
		String progstr = "p(a). q(X) :- p(X).";
		SystemConfig cfg = new SystemConfig();
		cfg.setEvaluateStratifiedPart(false);
		AlphaImpl system = new AlphaImpl(cfg);
		ASPCore2Program input = system.readProgramString(progstr);
		NormalProgram normal = system.normalizeProgram(input);
		CompiledProgram preprocessed = system.performProgramPreprocessing(normal);
		assertFalse(preprocessed.getFacts().contains(Atoms.newBasicAtom(Predicates.getPredicate("q", 1), Terms.newSymbolicConstant("a"))),
				"Preprocessed program contains fact derived from stratifiable rule, but should not!");
	}

	/**
	 * Verifies that stratified evaluation is performed up-front if not otherwise configured.
	 */
	@Test
	public void enableStratifiedEvalTest() {
		// Note: This might be cleaner if the test used the debugSolve method from the interface
		String progstr = "p(a). q(X) :- p(X).";
		SystemConfig cfg = new SystemConfig();
		AlphaImpl system = new AlphaImpl(cfg);
		ASPCore2Program input = system.readProgramString(progstr);
		NormalProgram normal = system.normalizeProgram(input);
		CompiledProgram preprocessed = system.performProgramPreprocessing(normal);
		assertTrue(preprocessed.getFacts().contains(Atoms.newBasicAtom(Predicates.getPredicate("q", 1), Terms.newSymbolicConstant("a"))),
				"Preprocessed program does not contain fact derived from stratifiable rule, but should!");
	}

	@Test
	public void passingUnitTestExpectUnsat() {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgramString(UNIT_TEST_EXPECT_UNSAT);
		TestResult testResult = alpha.test(prog);
		assertTrue(testResult.isSuccess());
	}

	@Test
	public void passingUnitTestBasicTest() {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgramString(UNIT_TEST_BASIC_TEST);
		TestResult testResult = alpha.test(prog);
		assertTrue(testResult.isSuccess());
		assertEquals(1, testResult.getTestCaseResults().size());
		TestResult.TestCaseResult tcResult = testResult.getTestCaseResults().get(0);
		assertTrue(tcResult.isSuccess());
		assertEquals(1, tcResult.getAssertionsPassed());
		assertEquals(0, tcResult.getAssertionsFailed());
		assertFalse(tcResult.answerSetCountVerificationResult().isPresent());
		assertTrue(tcResult.getAssertionErrors().isEmpty());
	}

	@Test
	public void passingUnitTestMultipleAssertions() {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgramString(UNIT_TEST_MORE_ASSERTIONS);
		TestResult testResult = alpha.test(prog);
		assertTrue(testResult.isSuccess());
		assertEquals(1, testResult.getTestCaseResults().size());
		TestResult.TestCaseResult tcResult = testResult.getTestCaseResults().get(0);
		assertTrue(tcResult.isSuccess());
		assertEquals(2, tcResult.getAssertionsPassed());
		assertEquals(0, tcResult.getAssertionsFailed());
		assertFalse(tcResult.answerSetCountVerificationResult().isPresent());
		assertTrue(tcResult.getAssertionErrors().isEmpty());
	}

	@Test
	public void passingUnitTestMultipleTestCases() {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgramString(UNIT_TEST_MORE_TCS);
		TestResult testResult = alpha.test(prog);
		assertTrue(testResult.isSuccess());
		assertEquals(2, testResult.getTestCaseResults().size());
	}

	@Test
	public void failingAssertionUnitTest() {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgramString(UNIT_TEST_FAILING_ASSERTION);
		TestResult testResult = alpha.test(prog);
		assertFalse(testResult.isSuccess());
		assertEquals(1, testResult.getTestCaseResults().size());
		TestResult.TestCaseResult tcResult = testResult.getTestCaseResults().get(0);
		assertFalse(tcResult.isSuccess());
		assertEquals(0, tcResult.getAssertionsPassed());
		assertEquals(1, tcResult.getAssertionsFailed());
		assertFalse(tcResult.answerSetCountVerificationResult().isPresent());
		assertEquals(1, tcResult.getAssertionErrors().size());
	}

	@Test
	public void failingAnswerSetCountUnitTest() {
		Alpha alpha = new AlphaImpl();
		ASPCore2Program prog = alpha.readProgramString(UNIT_TEST_FAILING_COUNT);
		TestResult testResult = alpha.test(prog);
		assertFalse(testResult.isSuccess());
		assertEquals(1, testResult.getTestCaseResults().size());
		TestResult.TestCaseResult tcResult = testResult.getTestCaseResults().get(0);
		assertFalse(tcResult.isSuccess());
		assertEquals(1, tcResult.getAssertionsPassed());
		assertEquals(0, tcResult.getAssertionsFailed());
		assertTrue(tcResult.answerSetCountVerificationResult().isPresent());
	}

	/**
	 * Runs a test that formerly caused some sort of exception.
	 */
	@Test
	public void problematicRun_3col_1119654162577372() throws IOException {
		/*
		 * NOTE: This was constructed from the following commandline invocation: -DebugEnableInternalChecks -q -g naive -s
		 * default -e 1119654162577372 -n 200 -i
		 * 3col-20-38.txt
		 */
		problematicRun("3col-20-38.txt", 1119654162577372L, 200);
	}

	/**
	 * Runs a test that formerly caused some sort of exception.
	 */
	@Test
	public void problematicRun_3col_1119718541727902() throws IOException {
		/*
		 * NOTE: This was constructed from the following commandline invocation:
		 * -DebugEnableInternalChecks -q -g naive -s default -e 1119718541727902 -n 200 -i
		 * 3col-20-38.txt
		 */
		problematicRun("3col-20-38.txt", 1119718541727902L, 200);
	}

	/**
	 * Runs a test that formerly caused some sort of exception.
	 */
	@Test
	public void problematicRun_vehicle_97598271567626() throws IOException {
		/*
		 * NOTE: This was constructed from the following commandline invocation:
		 * -DebugEnableInternalChecks -q -g naive -s default -e 97598271567626 -n 2 -i vehicle_normal_small.asp
		 */
		problematicRun("vehicle_normal_small.asp", 1119718541727902L, 2);
	}

	/**
	 * Runs a test that formerly caused some sort of exception.
	 */
	@Test
	public void problematicRun_3col_1119718541727902_sorted_400() throws IOException {
		/*
		 * NOTE: This was constructed from the following commandline invocation:
		 * -DebugEnableInternalChecks -q -g naive -s default -sort -n 400 -i 3col-20-38.txt
		 */
		SystemConfig cfg = new SystemConfig();
		cfg.setGrounderName("naive");
		cfg.setSolverName("default");
		cfg.setNogoodStoreName("alpharoaming");
		cfg.setDebugInternalChecks(true);
		cfg.setSeed(1119718541727902L);
		final Alpha system = new AlphaImpl(cfg);

		final Path path = Paths.get("src", "test", "resources", "PreviouslyProblematic").resolve("3col-20-38.txt");
		InputConfig inputCfg = new InputConfig();
		List<String> files = new ArrayList<>();
		files.add(path.toString());
		inputCfg.setFiles(files);
		ASPCore2Program prog = system.readProgram(inputCfg);

		assertFalse(system.solve(prog).sorted().limit(400).collect(Collectors.toList()).isEmpty());
	}

	private void problematicRun(String program, long seed, int limit) throws IOException {
		final Path base = Paths.get("src", "test", "resources", "PreviouslyProblematic");
		SystemConfig cfg = new SystemConfig();
		cfg.setGrounderName("naive");
		cfg.setSolverName("default");
		cfg.setNogoodStoreName("alpharoaming");
		cfg.setDebugInternalChecks(true);
		cfg.setSeed(seed);
		final Alpha system = new AlphaImpl(cfg);
		InputConfig inputCfg = new InputConfig();
		List<String> files = new ArrayList<>();
		files.add(base.resolve(program).toString());
		inputCfg.setFiles(files);
		ASPCore2Program prog = system.readProgram(inputCfg);
		assertFalse(system.solve(prog).limit(limit).collect(Collectors.toList()).isEmpty());
	}

	// Detailed reproduction test-case for github issue #239.
	@Test
	public void testLearnedUnaryNoGoodCausingOutOfOrderLiteralsConflict() throws IOException {
		final ProgramParser parser = new ProgramParserImpl();
		ASPCore2ProgramBuilder bld = Programs.builder();
		bld.accumulate(parser.parse(Files.newInputStream(Paths.get("src", "test", "resources", "HanoiTower_Alpha.asp"), StandardOpenOption.READ)));
		bld.accumulate(
				parser.parse(Files.newInputStream(Paths.get("src", "test", "resources", "HanoiTower_instances", "simple.asp"), StandardOpenOption.READ)));
		ASPCore2Program parsedProgram = bld.build();

		SystemConfig config = new SystemConfig();
		config.setSolverName("default");
		config.setNogoodStoreName("alpharoaming");
		config.setSeed(0);
		config.setBranchingHeuristic(Heuristic.valueOf("VSIDS"));
		config.setDebugInternalChecks(true);
		config.setDisableJustificationSearch(false);
		config.setEvaluateStratifiedPart(false);
		config.setReplayChoices(Arrays.asList(21, 26, 36, 56, 91, 96, 285, 166, 101, 290, 106, 451, 445, 439, 448,
				433, 427, 442, 421, 415, 436, 409, 430, 397, 391, 424, 385, 379,
				418, 373, 412, 406, 394, 388, 382, 245, 232, 208));
		Alpha alpha = new AlphaImpl(config);
		Optional<AnswerSet> answerSet = alpha.solve(parsedProgram).findFirst();
		assertTrue(answerSet.isPresent());
	}

}
