4 files changed, 68 insertions, 28 deletions

diff --git a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
index 3edc908..0a79823 100644
--- a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
@@ -1,36 +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, 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.
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index 58bee44..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))
+    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(BindAtom.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y)
+          // a simple builtin function with a "special" name.
+          (List(),List(BindAtom.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y)
     }
-    val classVisitor = new RDFoxClassExprConverter(term1,skolem)
+    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/RSAComb.scala b/src/main/scala/rsacomb/RSAComb.scala
index a6f237f..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}
@@ -55,6 +57,11 @@ object 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 {
@@ -68,12 +75,12 @@ object RSA {
     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.Constant(axiom.toString))
+      visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.ConstantRSA(axiom.toString), unsafe)
       rule  <- axiom.accept(visitor)
     } yield println(rule)
 
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
+  }
 }