Implement loose ends for OWL RL. Add tests.

modules/core/src/main/scala/org/geneontology/whelk/Model.scala

@@ -74,6 +74,10 @@ object BuiltIn {
 
   final val Bottom = AtomicConcept(s"$owl#Nothing")
 
+  final val SameAs = Role(s"$owl#sameAs")
+
+  final val DifferentFrom = Role(s"$owl#differentFrom")
+
 }
 
 final case class Conjunction(left: Concept, right: Concept) extends Concept {
@@ -112,6 +116,30 @@ final case class ExistentialRestriction(role: Role, concept: Concept) extends Co
 
 }
 
+final case class UniversalRestriction(role: Role, concept: Concept) extends Concept {
+
+  def conceptSignature: Set[Concept] = concept.conceptSignature + this
+
+  def signature: Set[Entity] = concept.signature + role
+
+  def isAnonymous: Boolean = true
+
+  override val hashCode: Int = scala.util.hashing.MurmurHash3.productHash(this)
+
+}
+
+final case class MaxCardinalityRestriction(role: Role, concept: Concept, cardinality: Int) extends Concept {
+
+  def conceptSignature: Set[Concept] = concept.conceptSignature + this
+
+  def signature: Set[Entity] = concept.signature + role
+
+  def isAnonymous: Boolean = true
+
+  override val hashCode: Int = scala.util.hashing.MurmurHash3.productHash(this)
+
+}
+
 final case class SelfRestriction(role: Role) extends Concept {
 
   def conceptSignature: Set[Concept] = Set(this)
@@ -260,6 +288,22 @@ final case class RoleAtom(predicate: Role, subject: IndividualArgument, target:
 
 }
 
+final case class SameIndividualsAtom(left: IndividualArgument, right: IndividualArgument) extends RuleAtom {
+
+  def signature: Set[Entity] = left.signature ++ right.signature
+
+  def variables: Set[Variable] = Set(left, right).collect { case v: Variable => v }
+
+}
+
+final case class DifferentIndividualsAtom(left: IndividualArgument, right: IndividualArgument) extends RuleAtom {
+
+  def signature: Set[Entity] = left.signature ++ right.signature
+
+  def variables: Set[Variable] = Set(left, right).collect { case v: Variable => v }
+
+}
+
 final case class Rule(body: List[RuleAtom], head: List[RuleAtom]) extends Axiom {
 
   def signature: Set[Entity] = body.flatMap(_.signature).toSet ++ head.flatMap(_.signature).toSet

modules/core/src/main/scala/org/geneontology/whelk/Reasoner.scala

@@ -26,6 +26,9 @@ final case class ReasonerState(
                                 negExistsMapByConcept: Map[Concept, Set[ExistentialRestriction]] = Map.empty,
                                 propagations: Map[Concept, Map[Role, List[ExistentialRestriction]]] = Map.empty,
                                 assertedNegativeSelfRestrictionsByRole: Map[Role, SelfRestriction] = Map.empty,
+                                universalRestrictionTypesByRole: Map[Nominal, Map[Role, List[Concept]]] = Map.empty,
+                                maxOneCardinalityRestrictionTypesByRole: Map[Nominal, Map[Role, List[Concept]]] = Map.empty,
+                                maxOneCardinalityRestrictionTypesByFiller: Map[Concept, Map[Role, List[Nominal]]] = Map.empty,
                                 ruleEngine: RuleEngine = RuleEngine.empty,
                                 wm: WorkingMemory = RuleEngine.empty.emptyMemory,
                                 disableBottom: Boolean = false,
@@ -123,7 +126,7 @@ object Reasoner {
     val hier: Map[Role, Set[Role]] = saturateRoles(allRoleInclusions) |+| allRoles.map(r => r -> Set(r)).toMap
     val hierList = hier.map { case (k, v) => k -> v.toList }
     val hierComps = indexRoleCompositions(hier, axioms.collect { case rc: RoleComposition => rc })
-    val rules = axioms.collect { case r: Rule => r } //TODO create rules from certain Whelk axioms
+    val rules = axioms.collect { case r: Rule => r }
     val anonymousRulePredicates = rules.flatMap(_.body.collect {
       case ConceptAtom(concept, _) if concept.isAnonymous => ConceptInclusion(concept, Top)
     })
@@ -134,18 +137,25 @@ object Reasoner {
   }
 
   def assert(axioms: Set[ConceptInclusion], reasoner: ReasonerState): ReasonerState = {
+    val ruleConcepts = reasoner.ruleEngine.rules.flatMap(_.signature).collect {
+      case ac: AtomicConcept => ac
+      case i: Individual     => Nominal(i)
+    }
     val distinctConcepts = axioms.flatMap {
       case ConceptInclusion(subclass, superclass) => Set(subclass, superclass)
     }.flatMap(_.conceptSignature)
-    val atomicConcepts = distinctConcepts.collect { case a: AtomicConcept => a }
+    val conceptsToQueue = distinctConcepts.collect {
+      case a: AtomicConcept => a
+      case n: Nominal       => n
+    }
     val additionalAxioms = distinctConcepts.flatMap {
       case d @ Disjunction(_) => `R⊔`(d)
       case c @ Complement(_)  => `R¬`(c, reasoner.disableBottom)
       case _                  => Set.empty[ConceptInclusion]
     }
     val negativeSelfRestrictions = axioms.flatMap(_.subclass.conceptSignature).collect { case sr: SelfRestriction => sr.role -> sr }.toMap
     val updatedAssertions = additionalAxioms.toList ::: axioms.toList
-    val todo = mutable.Stack.from[QueueExpression](atomicConcepts.toList ::: updatedAssertions)
+    val todo = mutable.Stack.from[QueueExpression](ruleConcepts.toList ::: conceptsToQueue.toList ::: updatedAssertions)
     computeClosure(reasoner.copy(
       assertions = reasoner.assertions ::: updatedAssertions,
       assertedNegativeSelfRestrictionsByRole = negativeSelfRestrictions),
@@ -199,10 +209,12 @@ object Reasoner {
         val closureSubsBySuperclass = reasoner.closureSubsBySuperclass.updated(superclass, subs + subclass)
         val supers = reasoner.closureSubsBySubclass.getOrElse(subclass, Set.empty)
         val closureSubsBySubclass = reasoner.closureSubsBySubclass.updated(subclass, supers + superclass)
-        val updatedReasoner = `R⊔right`(ci, `R+⟲`(ci, `R-⟲`(ci, `R⊑right`(ci, `R+∃b-right`(ci, `R-∃`(ci, `R+⨅left`(ci, `R+⨅right`(ci, `R-⨅`(ci, `R⊥left`(ci, reasoner.copy(closureSubsBySuperclass = closureSubsBySuperclass, closureSubsBySubclass = closureSubsBySubclass), todo), todo), todo), todo), todo), todo), todo), todo), todo))
+        val updatedReasoner = `R≤1-c`(ci, `R≤1-a`(ci, `R∀-left`(ci, `R∃ind-left`(ci, `R⊔right`(ci, `R+⟲`(ci, `R-⟲`(ci, `R⊑right`(ci, `R+∃b-right`(ci, `R-∃`(ci, `R+⨅left`(ci, `R+⨅right`(ci, `R-⨅`(ci, `R⊥left`(ci, reasoner.copy(closureSubsBySuperclass = closureSubsBySuperclass, closureSubsBySubclass = closureSubsBySubclass), todo), todo), todo), todo), todo), todo), todo), todo), todo)), todo), todo), todo), todo)
         val newState = ci match {
-          case ConceptInclusion(Nominal(ind), concept) => reasoner.ruleEngine.processConceptAssertion(ConceptAssertion(concept, ind), updatedReasoner, todo)
-          case _                                       => updatedReasoner
+          case ConceptInclusion(Nominal(left), Nominal(right)) =>
+            reasoner.ruleEngine.processRoleAssertion(RoleAssertion(BuiltIn.SameAs, left, right), updatedReasoner, todo)
+          case ConceptInclusion(Nominal(ind), concept)         => reasoner.ruleEngine.processConceptAssertion(ConceptAssertion(concept, ind), updatedReasoner, todo)
+          case _                                               => updatedReasoner
         }
         newState.queueDelegates.keysIterator.foldLeft(newState) { (state, delegateKey) =>
           state.queueDelegates(delegateKey).processConceptInclusion(ci, state)
@@ -218,10 +230,11 @@ object Reasoner {
         val closureSubsBySuperclass = reasoner.closureSubsBySuperclass.updated(superclass, subs + subclass)
         val supers = reasoner.closureSubsBySubclass.getOrElse(subclass, Set.empty)
         val closureSubsBySubclass = reasoner.closureSubsBySubclass.updated(subclass, supers + superclass)
-        val updatedReasoner = `R⊔right`(ci, `R-⟲`(ci, `R⊑right`(ci, `R+∃b-right`(ci, `R+⨅left`(ci, `R+⨅right`(ci, `R⊥left`(ci, reasoner.copy(closureSubsBySuperclass = closureSubsBySuperclass, closureSubsBySubclass = closureSubsBySubclass), todo), todo), todo), todo), todo), todo))
+        val updatedReasoner = `R≤1-c`(ci, `R≤1-a`(ci, `R∀-left`(ci, `R∃ind-left`(ci, `R⊔right`(ci, `R-⟲`(ci, `R⊑right`(ci, `R+∃b-right`(ci, `R+⨅left`(ci, `R+⨅right`(ci, `R⊥left`(ci, reasoner.copy(closureSubsBySuperclass = closureSubsBySuperclass, closureSubsBySubclass = closureSubsBySubclass), todo), todo), todo), todo), todo), todo)), todo), todo), todo), todo)
         val newState = ci match {
-          case ConceptInclusion(Nominal(ind), concept) => updatedReasoner.ruleEngine.processConceptAssertion(ConceptAssertion(concept, ind), updatedReasoner, todo)
-          case _                                       => updatedReasoner
+          case ConceptInclusion(Nominal(left), Nominal(right)) => reasoner.ruleEngine.processRoleAssertion(RoleAssertion(BuiltIn.SameAs, left, right), updatedReasoner, todo)
+          case ConceptInclusion(Nominal(ind), concept)         => updatedReasoner.ruleEngine.processConceptAssertion(ConceptAssertion(concept, ind), updatedReasoner, todo)
+          case _                                               => updatedReasoner
         }
         newState.queueDelegates.keysIterator.foldLeft(newState) { (state, delegateKey) =>
           state.queueDelegates(delegateKey).processSubPlus(ci, state)
@@ -242,7 +255,7 @@ object Reasoner {
       val updatedSubjects = subject :: subjects
       val updatedRolesToSubjects = rolesToSubjects.updated(role, updatedSubjects)
       val linksByTarget = reasoner.linksByTarget.updated(target, updatedRolesToSubjects)
-      val updatedReasoner = `R+⟲𝒪`(link, `R⤳`(link, `R∘left`(link, `R∘right`(link, `R+∃right`(link, `R⊥right`(link, reasoner.copy(linksBySubject = linksBySubject, linksByTarget = linksByTarget), todo), todo), todo), todo), todo), todo)
+      val updatedReasoner = `R≤1-b`(link, `R∀-right`(link, `R∃ind-right`(link, `R+⟲𝒪`(link, `R⤳`(link, `R∘left`(link, `R∘right`(link, `R+∃right`(link, `R⊥right`(link, reasoner.copy(linksBySubject = linksBySubject, linksByTarget = linksByTarget), todo), todo), todo), todo), todo), todo), todo), todo), todo)
       val newState = link match {
         case Link(Nominal(subjectInd), aRole, Nominal(targetInd)) => updatedReasoner.ruleEngine.processRoleAssertion(RoleAssertion(aRole, subjectInd, targetInd), updatedReasoner, todo)
         case _                                                    => updatedReasoner
@@ -383,7 +396,7 @@ object Reasoner {
       // better for GO
       for {
         (right, conjunction) <- conjunctionsMatchingLeft
-        if (d2s(right))
+        if d2s(right)
       } todo.push(`Sub+`(ConceptInclusion(c, conjunction)))
     }
     reasoner
@@ -403,7 +416,7 @@ object Reasoner {
     } else {
       for {
         (left, conjunction) <- conjunctionsMatchingRight
-        if (d1s(left))
+        if d1s(left)
       } todo.push(`Sub+`(ConceptInclusion(c, conjunction)))
     }
     reasoner
@@ -474,6 +487,154 @@ object Reasoner {
     reasoner
   }
 
+  // Implementation of OWL RL eq-rep-o
+  private[this] def `R∃ind-left`(ci: ConceptInclusion, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState = {
+    ci match {
+      case ConceptInclusion(subclass: Nominal, superclass: Nominal) =>
+        for {
+          (r, subjects) <- reasoner.linksByTarget.getOrElse(superclass, Map.empty)
+          s <- subjects
+        } todo.push(Link(s, r, subclass))
+      case _                                                        => ()
+    }
+    reasoner
+  }
+
+  // Implementation of OWL RL eq-rep-o
+  private[this] def `R∃ind-right`(link: Link, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState = {
+    link match {
+      case Link(s: Nominal, r, o: Nominal) =>
+        for {
+          same <- reasoner.closureSubsBySuperclass.getOrElse(o, Set.empty).collect {
+            case n: Nominal => n
+          }
+        } todo.push(Link(s, r, same))
+      case _                               => ()
+    }
+    reasoner
+  }
+
+  // Implementation of OWL RL cls-avf
+  private[this] def `R∀-left`(ci: ConceptInclusion, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState = {
+    val updatedRestrictionTypesByRole = ci match {
+      case ConceptInclusion(n: Nominal, UniversalRestriction(role, filler)) =>
+        for {
+          target @ Nominal(_) <- reasoner.linksBySubject.getOrElse(n, Map.empty).getOrElse(role, Set.empty)
+        } todo.push(ConceptInclusion(target, filler))
+        reasoner.universalRestrictionTypesByRole.updatedWith(n) {
+          case Some(rolesToFillers) => Some(rolesToFillers.updatedWith(role) {
+            case Some(fillers) => Some(filler :: fillers)
+            case None          => Some(List(filler))
+          })
+          case None                 => Some(Map(role -> List(filler)))
+        }
+      case _                                                                => reasoner.universalRestrictionTypesByRole
+    }
+    reasoner.copy(universalRestrictionTypesByRole = updatedRestrictionTypesByRole)
+  }
+
+  // Implementation of OWL RL cls-avf
+  private[this] def `R∀-right`(link: Link, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState = {
+    link match {
+      case Link(s: Nominal, role, o: Nominal) =>
+        for {
+          filler <- reasoner.universalRestrictionTypesByRole.getOrElse(s, Map.empty).getOrElse(role, Nil)
+        } todo.push(ConceptInclusion(o, filler))
+      case _                                  => ()
+    }
+    reasoner
+  }
+
+  // Max 1 restrictions rules may need some optimization to reduce repeated joins
+  // x ⊑ ≤1R.C  ∧  x R y  ∧  x R z  ∧  y ⊑ C  ∧  z ⊑ C
+  // assuming all role subsumptions get materialized for individuals
+  // this rule: x ⊑ ≤1R.C
+  private[this] def `R≤1-a`(ci: ConceptInclusion, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState =
+    ci match {
+      case ConceptInclusion(subject: Nominal, MaxCardinalityRestriction(role, filler, cardinality))
+        if cardinality == 1 =>
+        val fillerSubclasses = reasoner.closureSubsBySuperclass.getOrElse(filler, Set.empty)
+        val targets = reasoner.linksBySubject.getOrElse(subject, Map.empty).getOrElse(role, Set.empty)
+          .collect {
+            case n: Nominal => n
+          }
+          .filter(fillerSubclasses)
+        if (targets.size > 1) {
+          for {
+            pair <- targets.toList.combinations(2)
+          } todo.push(ConceptInclusion(pair(0), pair(1)), ConceptInclusion(pair(1), pair(0)))
+        }
+        val updatedRestrictionTypesByRole = reasoner.maxOneCardinalityRestrictionTypesByRole.updatedWith(subject) {
+          case Some(rolesToFillers) => Some(rolesToFillers.updatedWith(role) {
+            case Some(fillers) => Some(filler :: fillers)
+            case None          => Some(List(filler))
+          })
+          case None                 => Some(Map(role -> List(filler)))
+        }
+        val updatedRestrictionTypesByFiller = reasoner.maxOneCardinalityRestrictionTypesByFiller.updatedWith(filler) {
+          case Some(rolesToInstances) => Some(rolesToInstances.updatedWith(role) {
+            case Some(instances) => Some(subject :: instances)
+            case None            => Some(List(subject))
+          })
+          case None                   => Some(Map(role -> List(subject)))
+        }
+        reasoner.copy(maxOneCardinalityRestrictionTypesByRole = updatedRestrictionTypesByRole,
+          maxOneCardinalityRestrictionTypesByFiller = updatedRestrictionTypesByFiller)
+
+      case _ => reasoner
+    }
+
+  // x ⊑ ≤1R.C  ∧  x R y  ∧  x R z  ∧  y ⊑ C  ∧  z ⊑ C
+  // this rule: x R y or x R z
+  private[this] def `R≤1-b`(link: Link, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState = {
+    link match {
+      case Link(s: Nominal, role, o: Nominal) =>
+        val fillers = reasoner.maxOneCardinalityRestrictionTypesByRole.getOrElse(s, Map.empty).getOrElse(role, Nil)
+        if (fillers.nonEmpty) {
+          val targets = reasoner.linksBySubject.getOrElse(s, Map.empty).getOrElse(role, Set.empty)
+            .collect {
+              case n: Nominal => n
+            }
+          for {
+            filler <- fillers
+            fillerSubclasses = reasoner.closureSubsBySuperclass.getOrElse(filler, Set.empty)
+            target <- targets.iterator.filter(fillerSubclasses)
+            if target != o
+          } {
+            todo.push(ConceptInclusion(o, target))
+            todo.push(ConceptInclusion(target, o))
+          }
+        }
+      case _                                  => ()
+    }
+    reasoner
+  }
+
+  // x ⊑ ≤1R.C  ∧  x R y  ∧  x R z  ∧  y ⊑ C  ∧  z ⊑ C
+  // this rule: y ⊑ C or z ⊑ C
+  private[this] def `R≤1-c`(ci: ConceptInclusion, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState = {
+    ci match {
+      case ConceptInclusion(target: Nominal, filler) =>
+        val restrictionInstancesByRole = reasoner.maxOneCardinalityRestrictionTypesByFiller.getOrElse(filler, Map.empty)
+        if (restrictionInstancesByRole.nonEmpty) {
+          for {
+            (role, subjects) <- restrictionInstancesByRole
+            subject <- subjects
+            otherTarget <- reasoner.linksBySubject.getOrElse(subject, Map.empty).getOrElse(role, Set.empty).iterator
+              .collect {
+                case n: Nominal => n
+              }
+            if otherTarget != target
+          } {
+            todo.push(ConceptInclusion(otherTarget, target))
+            todo.push(ConceptInclusion(target, otherTarget))
+          }
+        }
+      case _                                         => ()
+    }
+    reasoner
+  }
+
   private[this] def `R-⟲`(ci: ConceptInclusion, reasoner: ReasonerState, todo: mutable.Stack[QueueExpression]): ReasonerState = ci match {
     case ConceptInclusion(sub, SelfRestriction(role)) =>
       todo.push(Link(sub, role, sub))