package at.ac.tuwien.kr.alpha.core.grounder;

import static org.junit.jupiter.api.Assertions.assertEquals;
import static org.junit.jupiter.api.Assertions.assertNotNull;
import static org.junit.jupiter.api.Assertions.assertNull;

import org.junit.jupiter.api.Test;

import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
import at.ac.tuwien.kr.alpha.commons.substitutions.Unifier;
import at.ac.tuwien.kr.alpha.core.parser.ProgramPartParser;

/**
 * Copyright (c) 2021, the Alpha Team.
 */
public class UnificationTest {

	private ProgramPartParser partsParser = new ProgramPartParser();

	@Test
	public void simpleGroundUnification() {
		Atom pX = partsParser.parseLiteral("p(X)").getAtom();
		Atom pa = partsParser.parseLiteral("p(abc)").getAtom();
		Unifier unifier = Unification.unifyAtoms(pa, pX);
		assertNotNull(unifier);
		assertEquals(1, unifier.getMappedVariables().size());
		assertEquals("abc", unifier.eval(Terms.newVariable("X")).toString());
	}

	@Test
	public void unificationBothSides() {
		Atom left = partsParser.parseLiteral("p(X, 1)").getAtom();
		Atom right = partsParser.parseLiteral("p(d, Y)").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNotNull(unifier);
		assertEquals(2, unifier.getMappedVariables().size());
		assertEquals("d", unifier.eval(Terms.newVariable("X")).toString());
		assertEquals("1", unifier.eval(Terms.newVariable("Y")).toString());
	}

	@Test
	public void unificationNonGround() {
		Atom left = partsParser.parseLiteral("p(X, 13)").getAtom();
		Atom right = partsParser.parseLiteral("p(Z, Y)").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNotNull(unifier);
		assertEquals(3, unifier.getMappedVariables().size());
		assertEquals("13", unifier.eval(Terms.newVariable("Y")).toString());
		// Check that the unifier sets X=Z by either mapping X -> Z or Z -> X.
		if (unifier.eval(Terms.newVariable("X")) != null) {
			// X is mapped, it must map to Z now.
			assertEquals("Z", unifier.eval(Terms.newVariable("X")).toString());
		} else {
			// X is not mapped, so Z must map to X.
			assertEquals("X", unifier.eval(Terms.newVariable("Z")).toString());
		}
	}

	@Test
	public void unificationWithFunctionTerms() {
		Atom left = partsParser.parseLiteral("a(b, f(X, 13), g(Z), d)").getAtom();
		Atom right = partsParser.parseLiteral("a(b, A, g(e), d)").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNotNull(unifier);
		assertEquals(3, unifier.getMappedVariables().size());
		assertEquals(left.substitute(unifier).toString(), right.substitute(unifier).toString());
	}

	@Test
	public void unificationWithArithmeticTerms() {
		Atom left = partsParser.parseLiteral("a(X - (3 * Y))").getAtom();
		Atom right = partsParser.parseLiteral("a(15 - Z)").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNotNull(unifier);
		assertEquals(3, unifier.getMappedVariables().size());
		assertEquals(left.substitute(unifier).toString(), right.substitute(unifier).toString());
	}

	@Test
	public void nonunificationWithArithmeticTerms() {
		Atom left = partsParser.parseLiteral("a(X + 4)").getAtom();
		Atom right = partsParser.parseLiteral("a(Y - 4)").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNull(unifier);
	}

	@Test
	public void nonunificationWithArithmeticTermsNested() {
		Atom left = partsParser.parseLiteral("a(X + 7)").getAtom();
		Atom right = partsParser.parseLiteral("a(Y + (Z - 2))").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNull(unifier);
	}

	@Test
	public void nonunificationSimple() {
		Atom left = partsParser.parseLiteral("a(b,X)").getAtom();
		Atom right = partsParser.parseLiteral("a(c,Y)").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNull(unifier);
	}

	@Test
	public void nonunificationNested() {
		Atom left = partsParser.parseLiteral("a(f(X,a))").getAtom();
		Atom right = partsParser.parseLiteral("a(f(a,b))").getAtom();
		Unifier unifier = Unification.unifyAtoms(left, right);
		assertNull(unifier);
	}
}
