Fixed review issues

klogic-core/src/main/kotlin/org/klogic/core/Constraint.kt

@@ -80,18 +80,8 @@ data class InequalityConstraint internal constructor(
     override fun toString(): String = simplifiedConstraints.joinToString(separator = ", ", prefix = "[", postfix = "]")
 
     companion object {
-        fun <T : Term<T>> of(variable: UnboundedValue<T>, term: Term<T>): InequalityConstraint =
-            InequalityConstraint(listOf(SingleInequalityConstraint(variable, term)))
-
-        // This method does not check that variable type equals to type of corresponding term,
-        // as it has to be in SingleInequalityConstraint, so it should be used very carefully
-        private fun unsafeOf(vararg pairs: Pair<UnboundedValue<out Term<*>>, Term<*>>): InequalityConstraint {
-            val singleInequalityConstraints = pairs.map {
-                SingleInequalityConstraint(it.first, it.second.cast())
-            }
-
-            return InequalityConstraint(singleInequalityConstraints)
-        }
+        fun <T : Term<T>> of(unboundedValue: UnboundedValue<T>, term: Term<T>): InequalityConstraint =
+            InequalityConstraint(listOf(SingleInequalityConstraint(unboundedValue, term)))
     }
 
 

klogic-core/src/main/kotlin/org/klogic/core/Context.kt

@@ -25,11 +25,6 @@ open class RelationalContext : AutoCloseable {
      */
     private var lastCreatedVariableIndex: Int = 0
 
-    /**
-     * The index of the last [Wildcard] created in this context.
-     */
-    private var lastCreatedWildcardIndex: Int = 0
-
     fun addUnificationListener(unificationListener: UnificationListener) {
         unificationListeners += unificationListener
     }
@@ -70,7 +65,8 @@ open class RelationalContext : AutoCloseable {
      *
      * NOTE: this method is not thread-safe and requires explicit outer synchronization in multithreading applications.
      */
-    fun <T : Term<T>> freshTypedWildcard(): Wildcard<T> = Wildcard(lastCreatedWildcardIndex++)
+    @Suppress("UNCHECKED_CAST")
+    fun <T : Term<T>> freshTypedWildcard(): Term<T> = Wildcard as T
 
     /**
      * Returns a result of invoking [run] overloading with goals for the fresh variable created using the passed [state].

klogic-core/src/main/kotlin/org/klogic/core/Substitution.kt

@@ -28,7 +28,7 @@ value class Substitution(private val innerSubstitution: PersistentMap<UnboundedV
     fun <T : Term<T>> ineq(left: Term<T>, right: Term<T>): ConstraintVerificationResult<InequalityConstraint> {
         return toUnificationState().unify(left, right)?.let { unificationState ->
             // Filter out wildcards as they add no information
-            val delta = unificationState.substitutionDifference.filter { !(it.key is Wildcard || it.value is Wildcard) }
+            val delta = unificationState.substitutionDifference.filterNot { it.key is Wildcard || it.value is Wildcard }
             // If the substitution from unification does not differ from the current substitution,
             // it means that this constraint is violated.
             if (delta.isEmpty()) {

klogic-core/src/main/kotlin/org/klogic/core/Term.kt

@@ -172,13 +172,12 @@ value class Var<T : Term<T>> internal constructor(val index: Int) : UnboundedVal
  * Represents all logic values of the specific type (in consideration of [InequalityConstraint]s).
  * For more information [take a look at the paper](https://danyaberezun.github.io/publications/assets/mk-2022-wild.pdf).
  */
-@JvmInline
-value class Wildcard<T : Term<T>> internal constructor(val index: Int) : UnboundedValue<T> {
+object Wildcard : UnboundedValue<Nothing> {
     override fun <R : Term<R>> occurs(variable: Var<R>): Boolean = false
 
-    override fun walk(substitution: Substitution): Wildcard<T> = this
+    override fun walk(substitution: Substitution): Wildcard = this
 
-    override fun unifyImpl(walkedOther: Term<T>, unificationState: UnificationState): UnificationState? {
+    override fun unifyImpl(walkedOther: Term<Nothing>, unificationState: UnificationState): UnificationState? {
         if (walkedOther is Wildcard) {
             return unificationState
         }
@@ -187,11 +186,11 @@ value class Wildcard<T : Term<T>> internal constructor(val index: Int) : Unbound
     }
 
     @Suppress("UNCHECKED_CAST")
-    override fun <R : Term<R>> cast(): Wildcard<R> = this as Wildcard<R>
+    override fun <R : Term<R>> cast(): Term<R> = this as Term<R>
 
-    override fun asReified(): T = error("Wildcard $this cannot be reified")
+    override fun asReified(): Nothing = error("Wildcard $this cannot be reified")
 
-    override fun toString(): String = "*.$index"
+    override fun toString(): String = "__"
 }
 
 /**
@@ -225,10 +224,7 @@ interface CustomTerm<T : CustomTerm<T>> : Term<T> {
 
     override fun unifyImpl(walkedOther: Term<T>, unificationState: UnificationState): UnificationState? {
         if (walkedOther is Wildcard) {
-            val newAssociation = walkedOther to this
-            unificationState.substitutionDifference[newAssociation.first] = newAssociation.second
-
-            return unificationState.copy(substitution = unificationState.substitution + newAssociation)
+            return unificationState
         }
 
         if (walkedOther !is CustomTerm) {

klogic-core/src/test/kotlin/org/klogic/core/wildcards/WildcardsTest.kt

@@ -2,22 +2,22 @@ package org.klogic.core.wildcards
 
 import org.junit.jupiter.api.Assertions.assertEquals
 import org.junit.jupiter.api.Assertions.assertTrue
-import org.junit.jupiter.api.DisplayName
 import org.junit.jupiter.api.Test
-import org.klogic.core.*
-import org.klogic.core.InequalityConstraint.SingleInequalityConstraint
-import org.klogic.core.Var.Companion.createTypedVar
-import org.klogic.utils.singleReifiedTerm
+import org.klogic.core.Goal
+import org.klogic.core.InequalityConstraint
+import org.klogic.core.Term
+import org.klogic.core.Var
+import org.klogic.core.and
+import org.klogic.utils.terms.LogicList.Companion.logicListOf
 import org.klogic.utils.terms.LogicPair
 import org.klogic.utils.terms.Symbol
 import org.klogic.utils.terms.Symbol.Companion.toSymbol
-import org.klogic.utils.withEmptyContext
 import org.klogic.utils.terms.logicTo
+import org.klogic.utils.withEmptyContext
 
 class WildcardsTest {
     @Test
-    @DisplayName("x !== *")
-    fun testAlwaysFail() {
+    fun `x !== __ -- failure`() {
         withEmptyContext {
             val goal = { x: Term<Symbol> -> x `!==` freshTypedWildcard() }
 
@@ -27,76 +27,88 @@ class WildcardsTest {
     }
 
     @Test
-    @DisplayName("x === *")
-    fun testAlwaysSuccess() {
+    fun `x !== (__, 1) && x === (1, y)`() {
         withEmptyContext {
-            val goal = { x: Term<Symbol> -> x `===` freshTypedWildcard() }
+            val one = "1".toSymbol()
 
-            val run = run(10, goal)
-            assertTrue(run.single().term is Var)
+            fun goal(x: Term<LogicPair<Symbol, Symbol>>, y: Term<Symbol>): Goal =
+                (x `!==` (freshTypedWildcard<Symbol>() logicTo one)) and (x `===` (one logicTo y))
+
+            val y = freshTypedVar<Symbol>()
+            val x = freshTypedVar<LogicPair<Symbol, Symbol>>()
+
+            val run = run(10, x, goal(x, y))
+            val answer = run.single()
+
+            val answerTerm = answer.term.asReified()
+            assertEquals(one, answerTerm.first)
+
+            // x == (1, y), y != 1
+            val inequalityConstraint = answer.constraints.single() as InequalityConstraint
+            val answerConstraint = inequalityConstraint.simplifiedConstraints.single()
+            assertEquals(answerTerm.second, answerConstraint.unboundedValue)
+            assertEquals(one, answerConstraint.term)
         }
     }
 
     @Test
-    @DisplayName("x === * && y === *")
-    fun testFewWildcards() {
+    fun `(1, __) != (__, 1) --- failure`() {
         withEmptyContext {
-            val a = (-1).createTypedVar<Symbol>()
-            val b = (-2).createTypedVar<Symbol>()
-            val goal = { x: Term<Symbol>, y: Term<Symbol> -> (x `===` freshTypedWildcard()) and (y `===` freshTypedWildcard()) }
+            val one = "1".toSymbol()
 
-            val run = unreifiedRun(10, goal(a, b))
-            val answers = listOf(a, b).map { run.reify(it) }
+            val goal = { _: Term<*> -> (one logicTo freshTypedWildcard<Symbol>()) `!==` (freshTypedWildcard<Symbol>() logicTo one) }
 
-            assertEquals(a, answers[0].single().term)
-            assertEquals(b, answers[1].single().term)
+            val run = run(10, goal)
+            assertTrue(run.isEmpty())
         }
     }
 
     @Test
-    @DisplayName("x !== (1, *) && x === (1, *)")
-    fun testWildcardInTermWithDisequality() {
+    fun `(x, 2, __) != (1, __, 2) --- x != 1`() {
         withEmptyContext {
             val one = "1".toSymbol()
-            val goal = { x: Term<LogicPair<Symbol, Symbol>> ->
-                (x `!==` (freshTypedWildcard<Symbol>() logicTo one)) and (x `===` (one logicTo freshTypedWildcard()))
+            val two = "2".toSymbol()
+
+            val goal = { x: Term<Symbol> ->
+                logicListOf(x, two, freshTypedWildcard()) `!==` logicListOf(one, freshTypedWildcard(), two)
             }
 
             val run = run(10, goal)
             val answer = run.single()
 
-            assertEquals(one, answer.term.asReified().first)
+            val variable = answer.term
+            assertTrue(variable is Var)
 
-            val wildcardInPair = answer.term.asReified().second as Wildcard<Symbol>
-            val answerConstraint = answer.constraints.single() as InequalityConstraint
+            val inequalityConstraint = answer.constraints.single() as InequalityConstraint
+            val answerConstraint = inequalityConstraint.simplifiedConstraints.single()
 
-            val expectedConstraint = SingleInequalityConstraint(wildcardInPair, one)
-            assertTrue(answerConstraint.simplifiedConstraints.any { it == expectedConstraint })
+            assertEquals(variable, answerConstraint.unboundedValue)
+            assertEquals(one, answerConstraint.term)
         }
     }
 
     @Test
-    @DisplayName("(*, 1) === (1, *)")
-    fun testWildcardsInTerms() {
+    fun `(x, y) != (1, __) --- x != 1`() {
         withEmptyContext {
-            val goal = { _: Term<*> -> (freshTypedWildcard<Symbol>() logicTo "1".toSymbol()) `===` ("1".toSymbol() logicTo freshTypedWildcard()) }
+            val one = "1".toSymbol()
 
-            val run = run(10, goal)
+            val x = freshTypedVar<Symbol>()
+            val y = freshTypedVar<Symbol>()
+            val goal = { symbol: Term<Symbol> ->
+                logicListOf(symbol, y) `!==` logicListOf(one, freshTypedWildcard())
+            }
+
+            val run = run(10, x, goal(x))
             val answer = run.single()
 
-            assertTrue(answer.term is Var)
-            assertTrue(answer.constraints.isEmpty())
-        }
-    }
+            val variable = answer.term
+            assertTrue(variable is Var)
 
-    @Test
-    @DisplayName("x === * && x === 5")
-    fun testRedundantWildcard() {
-        withEmptyContext {
-            val goal = { x: Term<Symbol> -> x `===` freshTypedWildcard() and (x `===` "5".toSymbol()) }
+            val inequalityConstraint = answer.constraints.single() as InequalityConstraint
+            val answerConstraint = inequalityConstraint.simplifiedConstraints.single()
 
-            val run = run(10, goal)
-            assertEquals("5".toSymbol(), run.singleReifiedTerm)
+            assertEquals(variable, answerConstraint.unboundedValue)
+            assertEquals(one, answerConstraint.term)
         }
     }
 }