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.

11 files changed, 190 insertions, 236 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}"
+
+}
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
index 0d07923..42ca6bd 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
@@ -15,7 +15,7 @@ import tech.oxfordsemantic.jrdfox.logic.expression.Variable
 import scala.collection.JavaConverters._
 
 import uk.ac.ox.cs.rsacomb.RSAOntology
-import uk.ac.ox.cs.rsacomb.converter.SkolemStrategy
+import uk.ac.ox.cs.rsacomb.converter.{SkolemStrategy, NoSkolem}
 import uk.ac.ox.cs.rsacomb.suffix.Empty
 import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
 
@@ -94,10 +94,8 @@ class Ontology1_CanonicalModelSpec
   renderer.render(AsubClassOfD) should "be converted into a single Rule" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(AsubClassOfD, term, unsafe, skolem, suffix)
+      converter.convert(AsubClassOfD, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
     rules.loneElement shouldBe a[Rule]
   }
@@ -163,10 +161,8 @@ class Ontology1_CanonicalModelSpec
   ) should "produce 1 rule" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(AsomeValuesFromSiC, term, unsafe, skolem, suffix)
+      converter.convert(AsomeValuesFromSiC, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
     rules.loneElement shouldBe a[Rule]
   }
@@ -189,10 +185,8 @@ class Ontology1_CanonicalModelSpec
     // Rule 3 provides 48 rule (split in 2)
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(DsomeValuesFromRB, term, unsafe, skolem, suffix)
+      converter.convert(DsomeValuesFromRB, term, unsafe, NoSkolem, Empty)
     facts should have length 48
     rules should have length 98
   }
@@ -216,10 +210,8 @@ class Ontology1_CanonicalModelSpec
     // Then (1*2 + 32) + (0) + (32*2) = 98
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(BsomeValuesFromSD, term, unsafe, skolem, suffix)
+      converter.convert(BsomeValuesFromSD, term, unsafe, NoSkolem, Empty)
     facts should have length 32
     rules should have length 66
   }
@@ -229,10 +221,8 @@ class Ontology1_CanonicalModelSpec
   ) should "produce 2 rules" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(SsubPropertyOfT, term, unsafe, skolem, suffix)
+      converter.convert(SsubPropertyOfT, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
     rules should have length 2
   }
@@ -357,10 +347,8 @@ class Ontology2_CanonicalModelSpec
   ) should "produce 1 rule" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(AsomeValuesFromRB, term, unsafe, skolem, suffix)
+      converter.convert(AsomeValuesFromRB, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
     rules should have length 1
   }
@@ -372,10 +360,8 @@ class Ontology2_CanonicalModelSpec
   ) should "produce 1 rule" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(BsomeValuesFromSC, term, unsafe, skolem, suffix)
+      converter.convert(BsomeValuesFromSC, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
     rules should have length 1
   }
@@ -387,10 +373,8 @@ class Ontology2_CanonicalModelSpec
   ) should "produce 1 rule" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(CsomeValuesFromTD, term, unsafe, skolem, suffix)
+      converter.convert(CsomeValuesFromTD, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
     rules should have length 1
   }
@@ -402,10 +386,8 @@ class Ontology2_CanonicalModelSpec
   ) should "produce 1 rule" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
-    val skolem = SkolemStrategy.None
-    val suffix = Empty
     val (facts, rules) =
-      converter.convert(DsomeValuesFromPA, term, unsafe, skolem, suffix)
+      converter.convert(DsomeValuesFromPA, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
     rules should have length 1
   }
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLAxiomSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/OWLAxiomSpec.scala
index 8aee03d..d39dec7 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLAxiomSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/OWLAxiomSpec.scala
@@ -36,7 +36,13 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{
 import org.semanticweb.owlapi.model.{IRI => OWLIRI}
 import tech.oxfordsemantic.jrdfox.logic.expression.{IRI => RDFIRI}
 
-import uk.ac.ox.cs.rsacomb.converter.{RDFoxAxiomConverter, SkolemStrategy}
+import uk.ac.ox.cs.rsacomb.converter.{
+  RDFoxAxiomConverter,
+  SkolemStrategy,
+  NoSkolem,
+  Standard,
+  Constant
+}
 import uk.ac.ox.cs.rsacomb.util.RSA
 
 object OWLAxiomSpec {
@@ -172,7 +178,7 @@ object OWLAxiomSpec {
   def convertAxiom(
       axiom: OWLAxiom,
       term: Term,
-      skolem: SkolemStrategy = SkolemStrategy.None
+      skolem: SkolemStrategy = NoSkolem
   ): List[Rule] = {
     axiom.accept(RDFoxAxiomConverter(term, List()))
   }
@@ -210,13 +216,13 @@ class OWLAxiomSpec extends AnyFlatSpec with Matchers with LoneElement {
   // OWLSubClassOfAxiom #2 (w/ constant skolemization)
   (axiom_OWLSubClassOf2.toString + "\n(w/ constant skolemization)") should
     "be converted into a singleton List[Rule]" in {
-    val skolem = SkolemStrategy.Constant(axiom_OWLSubClassOf2.toString)
-    val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
-    result.loneElement shouldBe a[Rule]
-  }
+      val skolem = Constant(axiom_OWLSubClassOf2.toString)
+      val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
+      result.loneElement shouldBe a[Rule]
+    }
 
   it should "contain a single atom (Student[?x]) in the body of the rule" in {
-    val skolem = SkolemStrategy.Constant(axiom_OWLSubClassOf2.toString)
+    val skolem = Constant(axiom_OWLSubClassOf2.toString)
     val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
     val body =
       TupleTableAtom.rdf(term_x, RDFIRI.RDF_TYPE, iri_Student.getIRIString)
@@ -237,13 +243,13 @@ class OWLAxiomSpec extends AnyFlatSpec with Matchers with LoneElement {
   // OWLSubClassOfAxiom #2 (w/ skolemization)
   (axiom_OWLSubClassOf2.toString + "\n(w/ skolemization)") should
     "be converted into a singleton List[Rule]" in {
-    val skolem = SkolemStrategy.Standard(axiom_OWLSubClassOf2.toString)
-    val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
-    result.loneElement shouldBe a[Rule]
-  }
+      val skolem = Standard(axiom_OWLSubClassOf2.toString)
+      val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
+      result.loneElement shouldBe a[Rule]
+    }
 
   it should "contain an atom (Student[?x]) in the body of the rule" in {
-    val skolem = SkolemStrategy.Standard(axiom_OWLSubClassOf2.toString)
+    val skolem = Standard(axiom_OWLSubClassOf2.toString)
     val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
     val body =
       TupleTableAtom.rdf(term_x, RDFIRI.RDF_TYPE, iri_Student)
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLClassSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/OWLClassSpec.scala
index 459fe21..bc3ac2b 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLClassSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/OWLClassSpec.scala
@@ -36,7 +36,9 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{
 import uk.ac.ox.cs.rsacomb.converter.{
   RDFoxRuleShards,
   RDFoxClassExprConverter,
-  SkolemStrategy
+  SkolemStrategy,
+  Standard,
+  Constant
 }
 import uk.ac.ox.cs.rsacomb.util.RSA
 
@@ -179,16 +181,16 @@ class OWLClassSpec extends AnyFlatSpec with Matchers with LoneElement {
   // OWLObjectSomeValuesFrom
   (class_OWLObjectSomeValuesFrom.toString ++ " w/o skolemization") should
     "be converted into a RDFoxRuleShards" in {
-    val visitor = RDFoxClassExprConverter(term_x)
-    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
-    result shouldBe a[RDFoxRuleShards]
-  }
+      val visitor = RDFoxClassExprConverter(term_x)
+      val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+      result shouldBe a[RDFoxRuleShards]
+    }
 
   it should "have two TupleTableAtoms in its result list" in {
     val visitor = RDFoxClassExprConverter(term_x)
     val result = class_OWLObjectSomeValuesFrom.accept(visitor)
     exactly(2, result.res) should (be(an[TupleTableAtom])
-    //and have('numberOfArguments (3))
+      //and have('numberOfArguments (3))
     )
   }
 
@@ -200,23 +202,23 @@ class OWLClassSpec extends AnyFlatSpec with Matchers with LoneElement {
 
   (class_OWLObjectSomeValuesFrom.toString ++ " w/ skolemization") should
     "be converted into a RDFoxRuleShards" in {
-    val skolem = SkolemStrategy.Standard(class_OWLObjectSomeValuesFrom.toString)
-    val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
-    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
-    result shouldBe a[RDFoxRuleShards]
-  }
+      val skolem = Standard(class_OWLObjectSomeValuesFrom.toString)
+      val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
+      val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+      result shouldBe a[RDFoxRuleShards]
+    }
 
   it should "have exactly two TupleTableAtoms in its result list" in {
-    val skolem = SkolemStrategy.Standard(class_OWLObjectSomeValuesFrom.toString)
+    val skolem = Standard(class_OWLObjectSomeValuesFrom.toString)
     val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
     val result = class_OWLObjectSomeValuesFrom.accept(visitor)
     exactly(2, result.res) should (be(an[TupleTableAtom])
-    //and have('numberOfArguments (3))
+      //and have('numberOfArguments (3))
     )
   }
 
   it should "should have a single SKOLEM call in the extension list" in {
-    val skolem = SkolemStrategy.Standard(class_OWLObjectSomeValuesFrom.toString)
+    val skolem = Standard(class_OWLObjectSomeValuesFrom.toString)
     val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
     val result = class_OWLObjectSomeValuesFrom.accept(visitor)
     result.ext.loneElement shouldBe a[BindAtom]
@@ -228,23 +230,23 @@ class OWLClassSpec extends AnyFlatSpec with Matchers with LoneElement {
 
   (class_OWLObjectSomeValuesFrom.toString ++ " w/ constant skolemization") should
     "be converted into a RDFoxRuleShards" in {
-    val skolem = SkolemStrategy.Constant(class_OWLObjectSomeValuesFrom.toString)
-    val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
-    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
-    result shouldBe a[RDFoxRuleShards]
-  }
+      val skolem = Constant(class_OWLObjectSomeValuesFrom.toString)
+      val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
+      val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+      result shouldBe a[RDFoxRuleShards]
+    }
 
   it should "have exactly two TupleTableAtoms in its result list" in {
-    val skolem = SkolemStrategy.Constant(class_OWLObjectSomeValuesFrom.toString)
+    val skolem = Constant(class_OWLObjectSomeValuesFrom.toString)
     val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
     val result = class_OWLObjectSomeValuesFrom.accept(visitor)
     exactly(2, result.res) should (be(an[TupleTableAtom])
-    //and have('numberOfArguments (3))
+      //and have('numberOfArguments (3))
     )
   }
 
   it should "have an empty extension list" in {
-    val skolem = SkolemStrategy.Constant(class_OWLObjectSomeValuesFrom.toString)
+    val skolem = Constant(class_OWLObjectSomeValuesFrom.toString)
     val visitor = RDFoxClassExprConverter(term_x, List(), skolem)
     val result = class_OWLObjectSomeValuesFrom.accept(visitor)
     result.ext shouldBe empty
@@ -253,10 +255,10 @@ class OWLClassSpec extends AnyFlatSpec with Matchers with LoneElement {
   // OWLObjectMaxCardinalityImpl
   class_OWLObjectMaxCardinality.toString should
     "be converted into a RDFoxRuleShards" in {
-    val visitor = RDFoxClassExprConverter(term_x)
-    val result = class_OWLObjectMaxCardinality.accept(visitor)
-    result shouldBe a[RDFoxRuleShards]
-  }
+      val visitor = RDFoxClassExprConverter(term_x)
+      val result = class_OWLObjectMaxCardinality.accept(visitor)
+      result shouldBe a[RDFoxRuleShards]
+    }
 
   // it should "have a single <owl:sameAs> TupleTableAtom in the result list" in {
   //   val visitor = RDFoxClassExprConverter(term_x)
@@ -270,7 +272,7 @@ class OWLClassSpec extends AnyFlatSpec with Matchers with LoneElement {
     val visitor = RDFoxClassExprConverter(term_x)
     val result = class_OWLObjectMaxCardinality.accept(visitor)
     exactly(4, result.ext) should (be(an[TupleTableAtom])
-    //and have('numberOfArguments (3))
+      //and have('numberOfArguments (3))
     )
   }
 
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/RDFoxConverterSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/RDFoxConverterSpec.scala
index e2da6e4..5c9fa96 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/RDFoxConverterSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/RDFoxConverterSpec.scala
@@ -10,7 +10,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.TupleTableAtom
 import tech.oxfordsemantic.jrdfox.logic.expression.{Variable, IRI}
 import uk.ac.ox.cs.rsacomb.converter.RDFoxConverter
 import uk.ac.ox.cs.rsacomb.suffix.{Empty, Forward, Backward, Inverse}
-import uk.ac.ox.cs.rsacomb.converter.SkolemStrategy
+import uk.ac.ox.cs.rsacomb.converter.{SkolemStrategy, NoSkolem}
 
 object RDFoxConverterSpec {
 
@@ -44,7 +44,7 @@ class RDFoxConverterSpec
     val cls = factory.getOWLClass(iriString0)
     val atom = TupleTableAtom.rdf(term0, IRI.RDF_TYPE, IRI.create(iriString0))
     val (res, ext) =
-      convert(cls, term0, List(), SkolemStrategy.None, Empty)
+      convert(cls, term0, List(), NoSkolem, Empty)
     res.loneElement shouldEqual atom
     ext shouldBe empty
   }
@@ -55,13 +55,13 @@ class RDFoxConverterSpec
     val cls2 = factory.getOWLClass(iriString2)
     val conj = factory.getOWLObjectIntersectionOf(cls0, cls1, cls2)
     val (res0, ext0) =
-      convert(cls0, term0, List(), SkolemStrategy.None, Empty)
+      convert(cls0, term0, List(), NoSkolem, Empty)
     val (res1, ext1) =
-      convert(cls1, term0, List(), SkolemStrategy.None, Empty)
+      convert(cls1, term0, List(), NoSkolem, Empty)
     val (res2, ext2) =
-      convert(cls2, term0, List(), SkolemStrategy.None, Empty)
+      convert(cls2, term0, List(), NoSkolem, Empty)
     val (res, ext) =
-      convert(conj, term0, List(), SkolemStrategy.None, Empty)
+      convert(conj, term0, List(), NoSkolem, Empty)
     res should contain theSameElementsAs (res0 ::: res1 ::: res2)
     ext should contain theSameElementsAs (ext0 ::: ext1 ::: ext2)
   }
@@ -70,9 +70,9 @@ class RDFoxConverterSpec
     val cls0 = factory.getOWLClass(iriString0)
     val conj = factory.getOWLObjectIntersectionOf(cls0)
     val (res0, ext0) =
-      convert(cls0, term0, List(), SkolemStrategy.None, Empty)
+      convert(cls0, term0, List(), NoSkolem, Empty)
     val (res, ext) =
-      convert(conj, term0, List(), SkolemStrategy.None, Empty)
+      convert(conj, term0, List(), NoSkolem, Empty)
     res should contain theSameElementsAs res0
     ext should contain theSameElementsAs ext0
   }