From f9960d603d34beb6746bc63587f9877c9374d172 Mon Sep 17 00:00:00 2001 From: Davide Greco Date: Fri, 28 Aug 2020 11:30:13 +0200 Subject: [PATCH] Test NotUnify implementation --- .../solve/systemtest/TestClassicNotUnify.kt | 96 ++++++++++++ .../it/unibo/tuprolog/solve/TestNotUnify.kt | 111 +++++++++++++ .../unibo/tuprolog/solve/TestNotUnifyImpl.kt | 147 ++++++++++++++++++ 3 files changed, 354 insertions(+) create mode 100644 solve-classic/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestClassicNotUnify.kt create mode 100644 test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnify.kt create mode 100644 test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnifyImpl.kt diff --git a/solve-classic/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestClassicNotUnify.kt b/solve-classic/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestClassicNotUnify.kt new file mode 100644 index 000000000..f928e33d3 --- /dev/null +++ b/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, + stdOut: OutputChannel, + stdErr: OutputChannel, + warnings: OutputChannel + ) = Solver.classic( + libraries, flags, staticKb, dynamicKb, stdIn, stdOut, stdErr, warnings + ) + + override fun mutableSolverOf( + libraries: Libraries, + flags: FlagStore, + staticKb: Theory, + dynamicKb: Theory, + stdIn: InputChannel, + stdOut: OutputChannel, + stdErr: OutputChannel, + warnings: OutputChannel + ) = 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() + } + +} \ No newline at end of file diff --git a/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnify.kt b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnify.kt new file mode 100644 index 000000000..b37c0f135 --- /dev/null +++ b/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() + +} \ No newline at end of file diff --git a/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnifyImpl.kt b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotUnifyImpl.kt new file mode 100644 index 000000000..3393ea1a5 --- /dev/null +++ b/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 + ) + } + } +} \ No newline at end of file