Add generation of rules for safe T5 axioms

1 files changed, 139 insertions, 4 deletions

diff --git a/src/main/scala/rsacomb/CanonicalModel.scala b/src/main/scala/rsacomb/CanonicalModel.scala
index 162bea1..c957940 100644
--- a/src/main/scala/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/rsacomb/CanonicalModel.scala
@@ -1,20 +1,32 @@
 package rsacomb
 
 import org.semanticweb.owlapi.model.{
+  OWLOntology,
+  OWLClass,
   OWLSubObjectPropertyOfAxiom,
   OWLSubClassOfAxiom,
   OWLObjectProperty,
-  OWLObjectPropertyExpression
+  OWLObjectPropertyExpression,
+  OWLObjectSomeValuesFrom
 }
-import tech.oxfordsemantic.jrdfox.logic.{IRI, Atom, Rule, Term, Variable}
+import tech.oxfordsemantic.jrdfox.logic.{
+  IRI,
+  BodyFormula,
+  Atom,
+  Rule,
+  Term,
+  Variable
+}
+import scala.collection.JavaConverters._
 
 object ProgramGenerator {
 
   def apply(
+      ontology: OWLOntology,
       term: Term,
       unsafe: List[OWLObjectPropertyExpression] = List()
   ): RDFoxAxiomConverter =
-    new ProgramGenerator(term, unsafe)
+    new ProgramGenerator(ontology, term, unsafe)
 
   def generateRoleRules(
       roles: List[OWLObjectPropertyExpression]
@@ -57,11 +69,131 @@ object ProgramGenerator {
 }
 
 class ProgramGenerator(
+    ontology: OWLOntology,
     term: Term,
     unsafe: List[OWLObjectPropertyExpression]
 ) extends RDFoxAxiomConverter(term, unsafe, SkolemStrategy.None, RSASuffix.None)
+    with RSAOntology
     with RSAAxiom {
 
+  import RDFoxUtil._
+
+  def rules1(axiom: OWLSubClassOfAxiom): (List[Rule], List[Atom]) = {
+    val unfold = ontology.cycle(axiom).toList
+    // Fresh Variables
+    val v0 = IRI.create("v0_" ++ axiom.hashCode.toString)
+    val varX = Variable.create("x")
+    // Predicates
+    val atomA: Atom = {
+      val cls = axiom.getSubClass.asInstanceOf[OWLClass].getIRI
+      Atom.rdf(varX, IRI.RDF_TYPE, cls)
+    }
+    def notIn(t: Term): Atom = {
+      Atom.rdf(
+        t,
+        RSA.internal("notIn"),
+        RSA.internal(unfold.hashCode.toString)
+      )
+    }
+    val roleRf: Atom = {
+      val visitor =
+        new RDFoxPropertyExprConverter(varX, v0, RSASuffix.Forward)
+      axiom.getSuperClass
+        .asInstanceOf[OWLObjectSomeValuesFrom]
+        .getProperty
+        .accept(visitor)
+        .head
+    }
+    val atomB: Atom = {
+      val cls = axiom.getSuperClass
+        .asInstanceOf[OWLObjectSomeValuesFrom]
+        .getFiller
+        .asInstanceOf[OWLClass]
+        .getIRI
+      Atom.rdf(v0, IRI.RDF_TYPE, cls)
+    }
+    (
+      List(
+        Rule.create(roleRf, atomA, notIn(varX)),
+        Rule.create(atomB, atomA, notIn(varX))
+      ),
+      unfold map notIn
+    )
+  }
+
+  def rules2(axiom: OWLSubClassOfAxiom): List[Rule] = {
+    val roleR =
+      axiom.getSuperClass
+        .asInstanceOf[OWLObjectSomeValuesFrom]
+        .getProperty
+    if (ontology.confl(roleR) contains roleR) {
+      // Fresh Variables
+      val v0 = IRI.create("v0_" ++ axiom.hashCode.toString)
+      val v1 = IRI.create("v1_" ++ axiom.hashCode.toString)
+      val v2 = IRI.create("v2_" ++ axiom.hashCode.toString)
+      // Predicates
+      def atomA(t: Term): Atom = {
+        val cls = axiom.getSubClass.asInstanceOf[OWLClass].getIRI
+        Atom.rdf(t, IRI.RDF_TYPE, cls)
+      }
+      def roleRf(t1: Term, t2: Term): Atom = {
+        val visitor = new RDFoxPropertyExprConverter(t1, t2, RSASuffix.Forward)
+        roleR.accept(visitor).head
+      }
+      def atomB(t: Term): Atom = {
+        val cls = axiom.getSuperClass
+          .asInstanceOf[OWLObjectSomeValuesFrom]
+          .getFiller
+          .asInstanceOf[OWLClass]
+          .getIRI
+        Atom.rdf(t, IRI.RDF_TYPE, cls)
+      }
+      //Rules
+      List(
+        Rule.create(roleRf(v0, v1), atomA(v0)),
+        Rule.create(atomB(v1), atomA(v0)),
+        Rule.create(roleRf(v1, v2), atomA(v1)),
+        Rule.create(atomB(v2), atomA(v1))
+      )
+    } else {
+      List()
+    }
+  }
+
+  def rules3(axiom: OWLSubClassOfAxiom): List[Rule] = {
+    val cycle = ontology.cycle(axiom).toList
+    val roleR =
+      axiom.getSuperClass
+        .asInstanceOf[OWLObjectSomeValuesFrom]
+        .getProperty
+    // Fresh Variables
+    val v1 = IRI.create("v1_" ++ axiom.hashCode.toString)
+    // Predicates
+    def atomA(t: Term): Atom = {
+      val cls = axiom.getSubClass.asInstanceOf[OWLClass].getIRI
+      Atom.rdf(t, IRI.RDF_TYPE, cls)
+    }
+    def roleRf(t: Term): Atom = {
+      val visitor =
+        new RDFoxPropertyExprConverter(t, v1, RSASuffix.Forward)
+      roleR.accept(visitor).head
+    }
+    val atomB: Atom = {
+      val cls = axiom.getSuperClass
+        .asInstanceOf[OWLObjectSomeValuesFrom]
+        .getFiller
+        .asInstanceOf[OWLClass]
+        .getIRI
+      Atom.rdf(v1, IRI.RDF_TYPE, cls)
+    }
+    cycle.flatMap { x =>
+      List(
+        Rule.create(roleRf(x), atomA(x)),
+        Rule.create(atomB, atomA(x))
+      )
+    }
+  }
+
   override def visit(axiom: OWLSubClassOfAxiom): List[Rule] = {
     if (axiom.isT5) {
       // TODO: get role in T5 axiom
@@ -77,7 +209,10 @@ class ProgramGenerator(
           )
         axiom.accept(visitor)
       } else {
-        List()
+        val (r1, f1) = rules1(axiom)
+        val r2 = rules2(axiom)
+        val r3 = rules3(axiom)
+        r1 ++ r2 ++ r3
       }
     } else {
       // Fallback to standard OWL to LP translation