5 files changed, 117 insertions, 39 deletions

diff --git a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
index 675ca7d..0a79823 100644
--- a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
@@ -1,35 +1,39 @@
 package rsacomb
 
-import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom}
+import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom, OWLObjectPropertyExpression}
 import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
 
 import tech.oxfordsemantic.jrdfox.logic.{Rule, BodyFormula}
-import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Literal}
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal}
+import tech.oxfordsemantic.jrdfox.logic.{TupleTableName}
 
 import scala.collection.JavaConverters._
 
 import rsacomb.SkolemStrategy
 import rsacomb.RDFoxRuleShards
+import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom
+import org.semanticweb.owlapi.model.OWLObjectProperty
 
 object RDFoxAxiomConverter {
 
-  def apply(term : Term, skolem : SkolemStrategy) : RDFoxAxiomConverter =
-        new RDFoxAxiomConverter(term, skolem)
-
-  def apply(term : Term) : RDFoxAxiomConverter =
-        new RDFoxAxiomConverter(term, SkolemStrategy.None)
+  def apply(
+    term : Term = Variable.create("x"),
+    skolem : SkolemStrategy = SkolemStrategy.None,
+    unsafe : List[OWLObjectPropertyExpression] = List()
+  ) : RDFoxAxiomConverter =
+          new RDFoxAxiomConverter(term, skolem, unsafe)
 
 } // object RDFoxAxiomConverter
 
-class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy)
+class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OWLObjectPropertyExpression])
   extends OWLAxiomVisitorEx[List[Rule]]
 {
 
   override
   def visit(axiom : OWLSubClassOfAxiom) : List[Rule] = {
     // Skolemization is needed only for the head of an axiom
-    val subVisitor = new RDFoxClassExprConverter(term,SkolemStrategy.None)
-    val superVisitor = new RDFoxClassExprConverter(term, skolem)
+    val subVisitor = new RDFoxClassExprConverter(term,SkolemStrategy.None, unsafe)
+    val superVisitor = new RDFoxClassExprConverter(term, skolem, unsafe)
     // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext):
     // - the `res` List is a list of atoms resulting from the conversion
     //   of the axiom.
@@ -46,11 +50,23 @@ class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy)
 
   override
   def visit(axiom : OWLEquivalentClassesAxiom) : List[Rule] = {
-        for {
-          axiom1 <- axiom.asPairwiseAxioms.asScala.toList
-          axiom2 <- axiom1.asOWLSubClassOfAxioms.asScala.toList
-          rule   <- axiom2.accept(this)
-        } yield rule
+    for {
+      axiom1 <- axiom.asPairwiseAxioms.asScala.toList
+      axiom2 <- axiom1.asOWLSubClassOfAxioms.asScala.toList
+      rule   <- axiom2.accept(this)
+    } yield rule
+  }
+
+  override
+  def visit(axiom : OWLSubObjectPropertyOfAxiom) : List[Rule] = {
+    // TODO: variables needs to be handled at visitor level. Hardcoding
+    // the name of the varibles might lead to errors for complex cases.
+    val term1 = Variable.create("y")
+    val subVisitor = new RDFoxPropertyExprConverter(term,term1,SkolemStrategy.None)
+    val superVisitor = new RDFoxPropertyExprConverter(term,term1,skolem)
+    val body: List[BodyFormula] = axiom.getSubProperty.accept(subVisitor)
+    val head: List[Atom] = axiom.getSuperProperty.accept(superVisitor)
+    List(Rule.create(head.asJava,body.asJava))
   }
 
   def doDefault(axiom : OWLAxiom) : List[Rule] = List()
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index bf026c3..227c25b 100644
--- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
@@ -10,14 +10,17 @@ import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal, Datatype
 
 import rsacomb.SkolemStrategy
 import rsacomb.RDFoxRuleShards
+import org.semanticweb.owlapi.model.OWLObjectPropertyExpression
+import org.semanticweb.owlapi.model.OWLObjectProperty
 
 object RDFoxClassExprConverter {
 
-  def apply(term : Term, skolem : SkolemStrategy) : RDFoxClassExprConverter =
-        new RDFoxClassExprConverter(term, skolem)
-
-  def apply(term : Term) : RDFoxClassExprConverter =
-        new RDFoxClassExprConverter(term, SkolemStrategy.None)
+  def apply(
+    term : Term = Variable.create("x"),
+    skolem : SkolemStrategy = SkolemStrategy.None,
+    unsafe : List[OWLObjectPropertyExpression] = List()
+  ) : RDFoxClassExprConverter =
+          new RDFoxClassExprConverter(term, skolem, unsafe)
 
   def merge(rules : List[RDFoxRuleShards]) : RDFoxRuleShards = {
     rules.foldLeft(RDFoxRuleShards(List(),List())) {
@@ -31,7 +34,7 @@ object RDFoxClassExprConverter {
 
 } // object RDFoxClassExprConverter
 
-class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy)
+class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OWLObjectPropertyExpression])
   extends OWLClassExpressionVisitorEx[RDFoxRuleShards]
 {
 
@@ -46,7 +49,7 @@ class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy)
   // OWLObjectIntersectionOf
   override
   def visit(expr : OWLObjectIntersectionOf) : RDFoxRuleShards = {
-    val visitor = new RDFoxClassExprConverter(term,skolem)
+    val visitor = new RDFoxClassExprConverter(term, skolem, unsafe)
     // TODO: maybe using `flatMap` instead of `merge` + `map` works as well
         RDFoxClassExprConverter.merge (
       expr.asConjunctSet.asScala.toList
@@ -75,22 +78,33 @@ class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy)
     // TODO: variables needs to be handled at visitor level. Hardcoding
     // the name of the varibles might lead to errors for complex cases.
     val y = Variable.create("y")
-        val (fun,term1) = skolem match {
-      case SkolemStrategy.None => (List(),y)
-      case SkolemStrategy.Constant(c) => (List(), Literal.create(c, Datatype.IRI_REFERENCE))
-      case SkolemStrategy.Standard(f) => 
-        // At the time of writing the RDFox library does not have a
-        // particular class for the "SKOLEM" operator and it is instead
-        // a simple builtin function with a special name.
-        (List(BindAtom.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y)
-        }
-    val classVisitor = new RDFoxClassExprConverter(term1,skolem)
+    val prop = expr.getProperty()
+    // Computes the result of rule skolemization. Depending on the used 
+    // technique it might involve the introduction of additional atoms,
+    // and/or fresh constants and variables.
+    val (head, body, term1) = skolem match {
+        case SkolemStrategy.None => (List(), List(), y)
+        case SkolemStrategy.Constant(c) => (List(), List(), Literal.create(c, Datatype.IRI_REFERENCE))
+        case SkolemStrategy.ConstantRSA(c) => {
+          val lit = Literal.create(c, Datatype.IRI_REFERENCE)
+          if (unsafe.contains(prop))
+            (List(Atom.create(TupleTableName.create("internal:PE"),term,lit), Atom.create(TupleTableName.create("internal:U"),lit)), List(), lit)
+          else 
+            (List(), List(), lit)
+        }
+        case SkolemStrategy.Standard(f) => 
+          // At the time of writing the RDFox library does not have a
+          // particular class for the "SKOLEM" operator and it is instead
+          // a simple builtin function with a "special" name.
+          (List(),List(BindAtom.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y)
+    }
+    val classVisitor = new RDFoxClassExprConverter(term1, skolem, unsafe)
     val classResult = expr.getFiller.accept(classVisitor)
     val propertyVisitor = new RDFoxPropertyExprConverter(term, term1, skolem)
     val propertyResult = expr.getProperty.accept(propertyVisitor)
     RDFoxRuleShards(
-      classResult.res ++ propertyResult,
-      fun ++ classResult.ext
+      classResult.res ++ propertyResult ++ head,
+      classResult.ext ++ body
     )
   }
 
@@ -100,7 +114,7 @@ class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy)
     // TODO: again, no hardcoded variables
     val vars = List(Variable.create("y"),Variable.create("z"))
     val classResult = RDFoxClassExprConverter.merge(
-      vars.map(new RDFoxClassExprConverter(_,skolem))
+      vars.map(new RDFoxClassExprConverter(_,skolem, unsafe))
           .map(expr.getFiller.accept(_))
     )
     val propertyResult = 
diff --git a/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala b/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
index 8d472bf..78ac98c 100644
--- a/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
@@ -7,6 +7,7 @@ import tech.oxfordsemantic.jrdfox.logic.{TupleTableName}
 import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal}
 
 import rsacomb.SkolemStrategy
+import org.semanticweb.owlapi.model.OWLObjectInverseOf
 
 class RDFoxPropertyExprConverter(term1 : Term, term2 : Term, skolem : SkolemStrategy)
   extends OWLPropertyExpressionVisitorEx[List[Atom]]
@@ -18,6 +19,12 @@ class RDFoxPropertyExprConverter(term1 : Term, term2 : Term, skolem : SkolemStra
     List(Atom.create(TupleTableName.create(name), term1, term2))
   }
 
+  override
+  def visit(expr : OWLObjectInverseOf) : List[Atom] = {
+    val name = expr.getInverse.getNamedProperty.getIRI.getIRIString;
+    List(Atom.create(TupleTableName.create(name ++ "_inv"), term1, term2))
+  }
+
   def doDefault(expr : OWLPropertyExpression) : List[Atom] = List()
 
 } // class RDFoxPropertyExprConverter
diff --git a/src/main/scala/rsacomb/RSAComb.scala b/src/main/scala/rsacomb/RSAComb.scala
index 16d7a04..62414e9 100644
--- a/src/main/scala/rsacomb/RSAComb.scala
+++ b/src/main/scala/rsacomb/RSAComb.scala
@@ -10,7 +10,9 @@ import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalent
 import org.semanticweb.owlapi.model.OWLClassExpression
 import org.semanticweb.owlapi.model.OWLOntology
 import org.semanticweb.owlapi.model.OWLOntologyManager
+import org.semanticweb.owlapi.model.IRI
 import org.semanticweb.owlapi.model.parameters.Imports
+import uk.ac.manchester.cs.owl.owlapi.OWLObjectPropertyImpl
 
 import tech.oxfordsemantic.jrdfox.Prefixes
 import tech.oxfordsemantic.jrdfox.client.{ConnectionFactory, ServerConnection, DataStoreConnection}
@@ -22,6 +24,7 @@ import tech.oxfordsemantic.jrdfox.logic.{LogicFormat}
 import scala.collection.JavaConverters._
 
 import rsacomb.SkolemStrategy
+import org.semanticweb.owlapi.dlsyntax.renderer.DLSyntaxObjectRenderer
 
 class RSA(ontology : OWLOntology) {
 
@@ -52,12 +55,34 @@ object RSA {
      *    step of approximation of an Horn-ALCHOIQ to RSA
      */
 
+    val renderer = new DLSyntaxObjectRenderer()
+
+    // Here we need to compute the unsafe roles. This is hardcoded for now.
+    val unsafe = List(
+      new OWLObjectPropertyImpl(IRI.create("http://example.com/rsa_example.owl#S")).getInverseProperty()
+    )
+
+    /* Print TBox axioms */
+    println("TBox/RBox:")
+    for {
+      axiom <- onto.tboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala
+    } yield println(renderer.render(axiom))
+    for {
+      axiom <- onto.rboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala
+    } yield println(renderer.render(axiom))
+
     /* Ontology axiom convertion into LP rules */
-        for {
+    println("Logic rules:")
+    for {
       axiom <- onto.tboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala
-      visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.Constant(axiom.toString))
+      visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.ConstantRSA(axiom.toString), unsafe)
+      rule  <- axiom.accept(visitor)
+    } yield println(rule)
+    for {
+      axiom <- onto.rboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala
+      visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.ConstantRSA(axiom.toString), unsafe)
       rule  <- axiom.accept(visitor)
-        } yield println(rule)
+    } yield println(rule)
 
     /* Return true for now... */
     true
diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala
index 9df167f..bcf6828 100644
--- a/src/main/scala/rsacomb/SkolemStrategy.scala
+++ b/src/main/scala/rsacomb/SkolemStrategy.scala
@@ -29,7 +29,7 @@ object SkolemStrategy {
     def genFunctionString(str : String) = "f_" ++ str.hashCode.toString
   }
 
-  /* Functional skolemization
+  /* Constant skolemization
    *
    * From 
    *    A ⊑ ∃R.B
@@ -42,5 +42,21 @@ object SkolemStrategy {
     def apply(axiom : String) = new Constant(genConstantString(axiom))
     def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
   }
+
+  /* (RSA) Constant skolemization
+   * This is a special skolemization option to introduce additional atoms for RSA
+   * checking algorithm.
+   *
+   * From 
+   *    A ⊑ ∃R.B
+   * to
+   *    A(y) -> R(x,c), PE(x,c), B(c)
+   * for c, fresh constant associated with the input axiom and PE an internal predicate.
+   */
+  case class ConstantRSA(const : String) extends SkolemStrategy
+  object ConstantRSA {
+    def apply(axiom : String) = new ConstantRSA(genConstantString(axiom))
+    def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
+  }
 }