Test NotUnify implementation

solve-classic/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestClassicNotUnify.kt

@@ -0,0 +1,96 @@
+package it.unibo.tuprolog.solve.systemtest
+
+import it.unibo.tuprolog.solve.*
+import it.unibo.tuprolog.solve.channel.InputChannel
+import it.unibo.tuprolog.solve.channel.OutputChannel
+import it.unibo.tuprolog.solve.exception.PrologWarning
+import it.unibo.tuprolog.solve.library.AliasedLibrary
+import it.unibo.tuprolog.solve.library.Libraries
+import it.unibo.tuprolog.solve.stdlib.DefaultBuiltins
+import it.unibo.tuprolog.theory.Theory
+import kotlin.test.Test
+
+class TestClassicNotUnify : TestNotUnify, SolverFactory {
+
+    private val prototype = TestNotUnify.prototype(this)
+
+    override val defaultBuiltins: AliasedLibrary
+        get() = DefaultBuiltins
+
+    override fun solverOf(
+            libraries: Libraries,
+            flags: FlagStore,
+            staticKb: Theory,
+            dynamicKb: Theory,
+            stdIn: InputChannel<String>,
+            stdOut: OutputChannel<String>,
+            stdErr: OutputChannel<String>,
+            warnings: OutputChannel<PrologWarning>
+    ) = Solver.classic(
+            libraries, flags, staticKb, dynamicKb, stdIn, stdOut, stdErr, warnings
+    )
+
+    override fun mutableSolverOf(
+            libraries: Libraries,
+            flags: FlagStore,
+            staticKb: Theory,
+            dynamicKb: Theory,
+            stdIn: InputChannel<String>,
+            stdOut: OutputChannel<String>,
+            stdErr: OutputChannel<String>,
+            warnings: OutputChannel<PrologWarning>
+    ) = MutableSolver.classic(
+            libraries, flags, staticKb, dynamicKb, stdIn, stdOut, stdErr, warnings
+    )
+
+    @Test
+    override fun testNumberNotUnify() {
+        prototype.testNumberNotUnify()
+    }
+
+    @Test
+    override fun testNumberXNotUnify() {
+        prototype.testNumberXNotUnify()
+    }
+
+    @Test
+    override fun testXYNotUnify() {
+        prototype.testXYNotUnify()
+    }
+
+    @Test
+    override fun testDoubleNotUnify() {
+        prototype.testDoubleNotUnify()
+    }
+
+    @Test
+    override fun testFDefNotUnify() {
+        prototype.testFDefNotUnify()
+    }
+
+    @Test
+    override fun testDiffNumberNotUnify() {
+        prototype.testDiffNumberNotUnify()
+    }
+
+    @Test
+    override fun testDecNumberNotUnify() {
+        prototype.testDecNumberNotUnify()
+    }
+
+    @Test
+    override fun testGNotUnifyFX() {
+        prototype.testGNotUnifyFX()
+    }
+
+    @Test
+    override fun testFNotUnify() {
+        prototype.testFNotUnify()
+    }
+
+    @Test
+    override fun testFMultipleTermNotUnify() {
+        prototype.testFMultipleTermNotUnify()
+    }
+
+}

test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnify.kt

@@ -0,0 +1,111 @@
+package it.unibo.tuprolog.solve
+
+interface TestNotUnify {
+    companion object{
+        fun prototype(solverFactory: SolverFactory): TestNotUnify =
+                TestNotUnifyImpl(solverFactory)
+    }
+
+    /** A short test max duration */
+    val shortDuration: TimeDuration
+        get() = 250L
+
+    /** A medium test max duration */
+    val mediumDuration: TimeDuration
+        get() = 2 * shortDuration
+
+    /** A long test max duration */
+    val longDuration: TimeDuration
+        get() = 4 * mediumDuration
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- `\\=`(1,1).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory.
+     */
+    fun testNumberNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- `\\=`(X,1).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testNumberXNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- `\\=`(X,Y).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testXYNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- ('\\='(X,Y),'\\='(X,abc)).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testDoubleNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- '\\='(f(X,def),f(def,Y)).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testFDefNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- '\\='(1,2).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory.
+     */
+    fun testDiffNumberNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- '\\='(1,1.0).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory.
+     */
+    fun testDecNumberNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- '\\='(g(X),f(f(X))).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory.
+     */
+    fun testGNotUnifyFX()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- '\\='(f(X,1),f(a(X))).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory.
+     */
+    fun testFNotUnify()
+
+    /**
+     * Tests the query
+     * ```prolog
+     * ?- '\\='(f(X,Y,X),f(a(X),a(Y),Y,2)).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory.
+     */
+    fun testFMultipleTermNotUnify()
+
+}

test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnifyImpl.kt

@@ -0,0 +1,147 @@
+package it.unibo.tuprolog.solve
+
+import it.unibo.tuprolog.dsl.theory.prolog
+import kotlin.collections.listOf as ktListOf
+
+internal class TestNotUnifyImpl(private val solverFactory: SolverFactory) : TestNotUnify {
+
+    override fun testNumberNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = 1 notEqualsTo 1
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.no()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testNumberXNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = "X" notEqualsTo 1
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.no()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testXYNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = "X" notEqualsTo  "Y"
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.no()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testDoubleNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = (("X" notEqualsTo  "Y") and ("X" notEqualsTo  "abc"))
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    ktListOf(query.no()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testFDefNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = "f"("X", "def") notEqualsTo  ("f"("def", "Y"))
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    ktListOf(query.no()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testDiffNumberNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = 1 notEqualsTo  2
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.yes()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testDecNumberNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = 1 notEqualsTo  1.0
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.yes()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testGNotUnifyFX() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = ("g"("X")) notEqualsTo  ("f"("a"("X")))
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.yes()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testFNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = ("f"("X", 1)) notEqualsTo ("f"("a"("X")))
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.yes()),
+                    solutions
+            )
+        }
+    }
+
+    override fun testFMultipleTermNotUnify() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = ("f"("X", "Y", "X")) notEqualsTo ("f"("a"("X"), "a"("Y"), "Y", 2))
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                    kotlin.collections.listOf(query.yes()),
+                    solutions
+            )
+        }
+    }
+}