Rework skolemization strategies

In particular `ConstantRSA` has been removed, since it was *not* a
skolemization strategy. The case for extra atoms generation previously
handled by `ConstantRSA` is not dealt with inside the RSA check.

7 files changed, 125 insertions, 161 deletions

diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
index bcc336a..c605e51 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -24,12 +24,7 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{
   IRI
 }
 
-import uk.ac.ox.cs.rsacomb.converter.{
-  SkolemStrategy,
-  RDFoxConverter
-  // RDFoxAxiomConverter,
-  // RDFoxPropertyExprConverter
-}
+import uk.ac.ox.cs.rsacomb.converter._
 import uk.ac.ox.cs.rsacomb.suffix._
 import uk.ac.ox.cs.rsacomb.util.RSA
 
@@ -114,10 +109,8 @@ class CanonicalModel(val ontology: RSAOntology) {
     val (facts, rules) = {
       val term = RSAOntology.genFreshVariable()
       val unsafe = ontology.unsafeRoles
-      val skolem = SkolemStrategy.None
-      val suffix = Empty
       ontology.axioms
-        .map(CanonicalModelConverter.convert(_, term, unsafe, skolem, suffix))
+        .map(CanonicalModelConverter.convert(_, term, unsafe, NoSkolem, Empty))
         .unzip
     }
     (
@@ -245,10 +238,9 @@ class CanonicalModel(val ontology: RSAOntology) {
 
         case a: OWLSubClassOfAxiom if a.isT5 => {
           val role = axiom.objectPropertyExpressionsInSignature(0)
-          if (unsafe contains role) {
-            val skolem = SkolemStrategy.Standard(a.toString)
-            super.convert(a, term, unsafe, skolem, Forward)
-          } else {
+          if (unsafe contains role)
+            super.convert(a, term, unsafe, new Standard(a), Forward)
+          else {
             val (f1, r1) = rules1(a)
             (f1, r1 ::: rules2(a) ::: rules3(a))
           }
@@ -256,9 +248,9 @@ class CanonicalModel(val ontology: RSAOntology) {
 
         case a: OWLSubObjectPropertyOfAxiom => {
           val (factsF, rulesF) =
-            super.convert(a, term, unsafe, SkolemStrategy.None, Forward)
+            super.convert(a, term, unsafe, NoSkolem, Forward)
           val (factsB, rulesB) =
-            super.convert(a, term, unsafe, SkolemStrategy.None, Backward)
+            super.convert(a, term, unsafe, NoSkolem, Backward)
           (factsF ::: factsB, rulesF ::: rulesB)
         }
 
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
index a965ef9..8fae4c8 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -50,7 +50,7 @@ import org.semanticweb.owlapi.dlsyntax.renderer.DLSyntaxObjectRenderer
 import tech.oxfordsemantic.jrdfox.logic._
 import org.semanticweb.owlapi.model.OWLObjectInverseOf
 
-import uk.ac.ox.cs.rsacomb.converter.{RDFoxConverter, SkolemStrategy}
+import uk.ac.ox.cs.rsacomb.converter._
 import uk.ac.ox.cs.rsacomb.suffix._
 import uk.ac.ox.cs.rsacomb.sparql._
 import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
@@ -163,16 +163,16 @@ class RSAOntology(val ontology: OWLOntology) {
       ): Shards =
         (expr, skolem) match {
 
-          case (e: OWLObjectSomeValuesFrom, SkolemStrategy.Constant(c))
+          case (e: OWLObjectSomeValuesFrom, c: Constant)
               if unsafe contains e.getProperty => {
             val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
-            (RSA.PE(term, c) :: RSA.U(c) :: res, ext)
+            (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
           }
 
-          case (e: OWLDataSomeValuesFrom, SkolemStrategy.Constant(c))
+          case (e: OWLDataSomeValuesFrom, c: Constant)
               if unsafe contains e.getProperty => {
             val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
-            (RSA.PE(term, c) :: RSA.U(c) :: res, ext)
+            (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
           }
 
           case _ => super.convert(expr, term, unsafe, skolem, suffix)
@@ -183,10 +183,7 @@ class RSAOntology(val ontology: OWLOntology) {
     /* Ontology convertion into LP rules */
     val term = RSAOntology.genFreshVariable()
     val datalog = axioms
-      .map(a => {
-        val skolem = SkolemStrategy.Constant(a.toString)
-        RSAConverter.convert(a, term, unsafe, skolem, Empty)
-      })
+      .map(a => RSAConverter.convert(a, term, unsafe, new Constant(a), Empty))
       .unzip
     val facts = datalog._1.flatten
     val rules = datalog._2.flatten
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala
index 93d8f8c..1fbf28a 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala
@@ -44,7 +44,7 @@ object RDFoxAxiomConverter {
   def apply(
       term: Term,
       unsafe: List[OWLObjectPropertyExpression],
-      skolem: SkolemStrategy = SkolemStrategy.None,
+      skolem: SkolemStrategy = NoSkolem,
       suffix: RSASuffix = Empty
   ): RDFoxAxiomConverter =
     new RDFoxAxiomConverter(term, unsafe, skolem, suffix)
@@ -63,7 +63,7 @@ class RDFoxAxiomConverter(
   override def visit(axiom: OWLSubClassOfAxiom): List[Rule] = {
     // Skolemization is needed only for the head of an axiom
     val subVisitor =
-      new RDFoxClassExprConverter(term, unsafe, SkolemStrategy.None, suffix)
+      new RDFoxClassExprConverter(term, unsafe, NoSkolem, suffix)
     val superVisitor = new RDFoxClassExprConverter(term, unsafe, skolem, suffix)
     // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext):
     // - the `res` List is a list of atoms resulting from the conversion
@@ -121,7 +121,7 @@ class RDFoxAxiomConverter(
       val term = RDFoxIRI.create(ind.asOWLNamedIndividual().getIRI.getIRIString)
       val cls = axiom.getClassExpression
       val visitor =
-        new RDFoxClassExprConverter(term, unsafe, SkolemStrategy.None, suffix)
+        new RDFoxClassExprConverter(term, unsafe, NoSkolem, suffix)
       val shard = cls.accept(visitor)
       List(Rule.create(shard.res.asJava, shard.ext.asJava))
     } else {
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala
index 4ededf9..9551c61 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala
@@ -39,7 +39,7 @@ object RDFoxClassExprConverter {
   def apply(
       term: Term,
       unsafe: List[OWLObjectPropertyExpression] = List(),
-      skolem: SkolemStrategy = SkolemStrategy.None,
+      skolem: SkolemStrategy = NoSkolem,
       suffix: RSASuffix = Empty
   ): RDFoxClassExprConverter =
     new RDFoxClassExprConverter(term, unsafe, skolem, suffix)
@@ -58,8 +58,8 @@ object RDFoxClassExprConverter {
 class RDFoxClassExprConverter(
     term: Term,
     unsafe: List[OWLObjectPropertyExpression],
-    skolem: SkolemStrategy,
-    suffix: RSASuffix
+    skolem: SkolemStrategy = NoSkolem,
+    suffix: RSASuffix = Empty
 ) extends OWLClassExpressionVisitorEx[RDFoxRuleShards] {
 
   import uk.ac.ox.cs.rsacomb.implicits.RDFox._
@@ -106,18 +106,14 @@ class RDFoxClassExprConverter(
     // 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(), c)
-      case SkolemStrategy.ConstantRSA(c) => {
-        if (unsafe.contains(prop))
-          (List(RSA.PE(term, c), RSA.U(c)), List(), c)
-        else
-          (List(), List(), c)
-      }
-      case SkolemStrategy.Standard(f) => {
+      case NoSkolem    => (List(), List(), y)
+      case c: Constant => (List(), List(), c.iri)
+      case s: Standard => {
         (
           List(),
-          List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)),
+          List(
+            BindAtom.create(FunctionCall.create("SKOLEM", s.literal, term), y)
+          ),
           y
         )
       }
@@ -152,18 +148,14 @@ class RDFoxClassExprConverter(
     // 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(), c)
-      case SkolemStrategy.ConstantRSA(c) => {
-        if (unsafe.contains(prop))
-          (List(RSA.PE(term, c), RSA.U(c)), List(), c)
-        else
-          (List(), List(), c)
-      }
-      case SkolemStrategy.Standard(f) => {
+      case NoSkolem    => (List(), List(), y)
+      case c: Constant => (List(), List(), c.iri)
+      case s: Standard => {
         (
           List(),
-          List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)),
+          List(
+            BindAtom.create(FunctionCall.create("SKOLEM", s.literal, term), y)
+          ),
           y
         )
       }
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
index 7fd4dbe..1c8374c 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
@@ -38,7 +38,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
 }
 import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, FunctionCall}
 import uk.ac.ox.cs.rsacomb.RSAOntology
-import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Inverse}
+import uk.ac.ox.cs.rsacomb.suffix.{Empty, Inverse, RSASuffix}
 import uk.ac.ox.cs.rsacomb.util.RSA
 
 /** Horn-ALCHOIQ to RDFox axiom converter.
@@ -144,7 +144,7 @@ trait RDFoxConverter {
 
       case a: OWLSubClassOfAxiom => {
         val (sub, _) =
-          convert(a.getSubClass, term, unsafe, SkolemStrategy.None, suffix)
+          convert(a.getSubClass, term, unsafe, NoSkolem, suffix)
         val (sup, ext) =
           convert(a.getSuperClass, term, unsafe, skolem, suffix)
         val rule = Rule.create(sup, ext ::: sub)
@@ -202,7 +202,7 @@ trait RDFoxConverter {
           case i: OWLNamedIndividual => {
             val cls = a.getClassExpression
             val (res, _) =
-              convert(cls, i.getIRI, unsafe, SkolemStrategy.None, suffix)
+              convert(cls, i.getIRI, unsafe, NoSkolem, suffix)
             ResultF(res)
           }
           case _ => Result()
@@ -309,32 +309,18 @@ trait RDFoxConverter {
       case e: OWLObjectSomeValuesFrom => {
         val cls = e.getFiller()
         val role = e.getProperty()
-        // TODO: simplify this:
-        // 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(), RSAOntology.genFreshVariable)
-          case SkolemStrategy.Constant(c) => (List(), List(), c)
-          case SkolemStrategy.ConstantRSA(c) => {
-            if (unsafe.contains(role))
-              (List(RSA.PE(term, c), RSA.U(c)), List(), c)
-            else
-              (List(), List(), c)
-          }
-          case SkolemStrategy.Standard(f) => {
-            val x = RSAOntology.genFreshVariable
-            (
-              List(),
-              List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), x)),
-              x
-            )
+        val varX = RSAOntology.genFreshVariable
+        val (bind, term1) = skolem match {
+          case NoSkolem    => (None, varX)
+          case c: Constant => (None, c.iri)
+          case s: Standard => {
+            val func = FunctionCall.create("SKOLEM", s.literal, term)
+            (Some(BindAtom.create(func, varX)), varX)
           }
         }
         val (res, ext) = convert(cls, term1, unsafe, skolem, suffix)
         val prop = convert(role, term, term1, suffix)
-        (prop :: head ::: res, body ::: ext)
+        (prop :: res, ext ++ bind)
       }
 
       /** Existential class expression (for data properties).
@@ -354,27 +340,17 @@ trait RDFoxConverter {
         // 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(), RSAOntology.genFreshVariable)
-          case SkolemStrategy.Constant(c) => (List(), List(), c)
-          case SkolemStrategy.ConstantRSA(c) => {
-            if (unsafe.contains(role))
-              (List(RSA.PE(term, c), RSA.U(c)), List(), c)
-            else
-              (List(), List(), c)
-          }
-          case SkolemStrategy.Standard(f) => {
-            val y = RSAOntology.genFreshVariable()
-            (
-              List(),
-              List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)),
-              y
-            )
+        val varX = RSAOntology.genFreshVariable
+        val (bind, term1) = skolem match {
+          case NoSkolem    => (None, varX)
+          case c: Constant => (None, c.iri)
+          case s: Standard => {
+            val func = FunctionCall.create("SKOLEM", s.literal, term)
+            (Some(BindAtom.create(func, varX)), varX)
           }
         }
         val prop = convert(role, term, term1, suffix)
-        (prop :: head, body)
+        (List(prop), bind.toList)
       }
 
       /** Maximum cardinality restriction class
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
index 0d72226..587db91 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
@@ -1,78 +1,76 @@
 package uk.ac.ox.cs.rsacomb.converter
 
+import org.semanticweb.owlapi.model.OWLAxiom
 import tech.oxfordsemantic.jrdfox.logic.Datatype
 import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, IRI}
 
 sealed trait SkolemStrategy
 
-object SkolemStrategy {
-  // TODO: might want to use something else other than `hashCode` as a
-  // function to generate a fresh function/constant
+/** No skolemization.
+  *
+  * @example role `R` from
+  * {{{
+  *   ∃R.A ⊑ B
+  * }}}
+  * to
+  * {{{
+  *   R(x,y), B(y) -> B(x)
+  * }}}
+  */
+case object NoSkolem extends SkolemStrategy
 
-  /* No skolemization at all.
-   *
-   * From
-   *    ∃R.A ⊑ B
-   * to
-   *    R(x,y), B(y) -> B(x)
-   */
-  case object None extends SkolemStrategy
-
-  /* Functional skolemization
-   *
-   * From
-   *    A ⊑ ∃R.B
-   * to
-   *    A(x) -> R(x,f(x)), B(f(x))
-   * for f, fresh function associated with the input axiom
-   *
-   * In RDFox this can represented combining the BIND operator with the
-   * SKOLEM operator as such:
-   *    A(x), BIND(y, SKOLEM("f", x)) -> R(x,y), B(y)
-   * The first argument of a SKOLEM call is a literal string (ideally
-   * identifing the simulated function name).
-   *
-   * NOTE: this requirement for the SKOLEM operator is not enforced by
-   * RDFox, that will fail silently if omitted.
-   */
-  case class Standard(func: Literal) extends SkolemStrategy
-  object Standard {
-    def apply(axiom: String) =
-      new Standard(
-        Literal.create(genFunctionString(axiom), Datatype.XSD_STRING)
-      )
-    def genFunctionString(str: String) = "f_" ++ str.hashCode.toString
-  }
-
-  /* Constant skolemization
-   *
-   * From
-   *    A ⊑ ∃R.B
-   * to
-   *    A(y) -> R(x,c), B(c)
-   * for c, fresh constant associated with the input axiom
-   */
-  case class Constant(const: IRI) extends SkolemStrategy
-  object Constant {
-    def apply(axiom: String) =
-      new Constant(IRI.create(genConstantString(axiom)))
-    def genConstantString(str: String) = "c_" ++ str.hashCode.toString
-  }
+/** Functional skolemization
+  *
+  * The factory object should be used to create new instances of the
+  * class.
+  *
+  * @example role `R` from
+  * {{{
+  *   A ⊑ ∃R.B
+  * }}}
+  * to
+  * {{{
+  *   A(x) -> R(x,f(x)), B(f(x))
+  * }}}
+  * for `f`, fresh function uniquely associated with the input axiom.
+  *
+  * RDFox does not support function symbols. We can still implement
+  * function symbols combining the `BIND` operator with the `SKOLEM`
+  * operator as such:
+  * {{{
+  *   A(x), BIND(y, SKOLEM("f", x)) -> R(x,y), B(y)
+  * }}}
+  * The first argument of a `SKOLEM` call '''must''' be a literal string
+  * (ideally identifing the simulated function name).
+  *
+  * @note this requirement is not enforced by RDFox, that will fail
+  * silently if a string argument is omitted.
+  */
+class Standard(var axiom: OWLAxiom)(implicit toString: (OWLAxiom) => String)
+    extends SkolemStrategy {
+  def dup(a: OWLAxiom) = new Standard(a)(toString)
+  lazy val literal =
+    Literal.create(s"f_${toString(axiom)}", Datatype.XSD_STRING)
+}
 
-  /* (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: IRI) extends SkolemStrategy
-  object ConstantRSA {
-    def apply(axiom: String) =
-      new ConstantRSA(IRI.create(genConstantString(axiom)))
-    def genConstantString(str: String) = "c_" ++ str.hashCode.toString
-  }
+/** Constant skolemization
+  *
+  * The factory object should be used to create new instances of the
+  * class.
+  *
+  * @example role `R` from
+  * {{{
+  *   A ⊑ ∃R.B
+  * }}}
+  * to
+  * {{{
+  *   A(y) -> R(x,c), B(c)
+  * }}}
+  * for `c`, fresh constant '''uniquely''' associated with the input
+  * axiom
+  */
+class Constant(var axiom: OWLAxiom)(implicit toString: (OWLAxiom) => String)
+    extends SkolemStrategy {
+  def dup(a: OWLAxiom) = new Constant(a)(toString)
+  lazy val iri = IRI.create(s"c_${toString(axiom)}")
 }
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/package.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/package.scala
new file mode 100644
index 0000000..0484153
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/package.scala
@@ -0,0 +1,9 @@
+package uk.ac.ox.cs.rsacomb
+package object converter {
+
+  import org.semanticweb.owlapi.model.OWLAxiom
+
+  implicit def axiomToHashedString(axiom: OWLAxiom): String =
+    s"${axiom.toString.hashCode}"
+
+}