package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality

import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
import org.junit.After
import org.junit.Before
import org.junit.Test

import static org.junit.Assert.*

class Z3PolyhedronSolverTest {
	var Z3PolyhedronSolver solver
	var PolyhedronSaturationOperator operator

	@Before
	def void setUp() {
		solver = new Z3PolyhedronSolver(false)
	}

	@After
	def void tearDown() {
		destroyOperatorIfExists()
	}

	@Test
	def void singleDimensionTest() {
		val x = new Dimension("x", 0, 1)
		createSaturationOperator(new Polyhedron(#[x], #[], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(0, x.lowerBound)
		assertEquals(1, x.upperBound)
	}

	@Test
	def void singleDimensionNegativeValueTest() {
		val x = new Dimension("x", -2, -1)
		createSaturationOperator(new Polyhedron(#[x], #[], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(-2, x.lowerBound)
		assertEquals(-1, x.upperBound)
	}

	@Test
	def void singleDimensionConstraintTest() {
		val x = new Dimension("x", null, null)
		val constraint = new LinearConstraint(#{x -> 2}, 0, 2)
		createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(0, x.lowerBound)
		assertEquals(1, x.upperBound)
	}

	@Test
	def void singleDimensionConstraintUnitCoefficientTest() {
		val x = new Dimension("x", null, null)
		val constraint = new LinearConstraint(#{x -> 1}, 1, 3)
		createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(1, x.lowerBound)
		assertEquals(3, x.upperBound)
	}

	@Test
	def void singleDimensionConstraintIntegerTest() {
		val x = new Dimension("x", null, null)
		val constraint = new LinearConstraint(#{x -> 2}, 0, 3)
		createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(0, x.lowerBound)
		assertEquals(1, x.upperBound)
	}

	@Test
	def void singleDimensionUnboundedFromAboveTest() {
		val x = new Dimension("x", 0, null)
		createSaturationOperator(new Polyhedron(#[x], #[], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(0, x.lowerBound)
		assertEquals(null, x.upperBound)
	}

	@Test
	def void singleDimensionUnboundedFromBelowTest() {
		val x = new Dimension("x", null, 0)
		createSaturationOperator(new Polyhedron(#[x], #[], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(null, x.lowerBound)
		assertEquals(0, x.upperBound)
	}

	@Test
	def void singleDimensionUnsatisfiableTest() {
		val x = new Dimension("x", 0, 1)
		val constraint = new LinearConstraint(#{x -> 2}, -2, -1)
		createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.EMPTY, result)
	}

	@Test
	def void equalityConstraintTest() {
		val x = new Dimension("x", null, null)
		val y = new Dimension("y", 1, 2)
		val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6)
		createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(1, x.lowerBound)
		assertEquals(2, x.upperBound)
	}

	@Test
	def void saturateConstraintTest() {
		val x = new Dimension("x", 0, 2)
		val y = new Dimension("y", 1, 2)
		val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8)
		createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint]))

		val result = saturate()

		assertEquals(PolyhedronSaturationResult.SATURATED, result)
		assertEquals(1, constraint.lowerBound)
		assertEquals(6, constraint.upperBound)
	}

	@Test(expected=IllegalArgumentException)
	def void unknownVariableTest() {
		val x = new Dimension("x", 0, 1)
		val y = new Dimension("y", 0, 1)
		val constraint = new LinearConstraint(#{y -> 2}, 0, 2)
		createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x]))

		saturate()
	}

	@Test
	def void unsatisfiableMultipleInheritanceTest() {
		val x = new Dimension("x", 0, 1)
		val y = new Dimension("y", 0, 1)
		val z = new Dimension("z", 0, 1)
		createSaturationOperator(new Polyhedron(
			#[x, y, z],
			#[
				new LinearConstraint(#{x -> 1, y -> 1}, 1, 1),
				new LinearConstraint(#{x -> 1, z -> 1}, 1, 1),
				new LinearConstraint(#{y -> 1, z -> 1}, 1, 1)
			],
			#[x, y, z]
		))
		
		val result = saturate()
		
		assertEquals(PolyhedronSaturationResult.EMPTY, result)
	}

	private def createSaturationOperator(Polyhedron polyhedron) {
		destroyOperatorIfExists()
		operator = solver.createSaturationOperator(polyhedron)
	}

	private def destroyOperatorIfExists() {
		if (operator !== null) {
			operator.close
		}
	}

	private def saturate() {
		operator.saturate
	}
}