From 3a166085e656be5f957423e6e371b6647b313997 Mon Sep 17 00:00:00 2001
From: Federico Igne <federico.igne@cs.ox.ac.uk>
Date: Wed, 19 Aug 2020 11:11:53 +0100
Subject: Use `rdf(..)` instead of `create(..)` to create `Atom`s

---
 src/main/scala/rsacomb/SkolemStrategy.scala | 32 ++++++++++++++++-------------
 1 file changed, 18 insertions(+), 14 deletions(-)

(limited to 'src/main/scala/rsacomb/SkolemStrategy.scala')

diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala
index bcf6828..9d45b4c 100644
--- a/src/main/scala/rsacomb/SkolemStrategy.scala
+++ b/src/main/scala/rsacomb/SkolemStrategy.scala
@@ -1,5 +1,7 @@
 package rsacomb
 
+import tech.oxfordsemantic.jrdfox.logic.IRI
+
 sealed trait SkolemStrategy
 
 object SkolemStrategy {
@@ -8,7 +10,7 @@ object SkolemStrategy {
 
   /* No skolemization at all.
    *
-   * From 
+   * From
    *    ∃R.A ⊑ B
    * to
    *    R(x,y), B(y) -> B(x)
@@ -17,46 +19,48 @@ object SkolemStrategy {
 
   /* Functional skolemization
    *
-   * From 
+   * From
    *    A ⊑ ∃R.B
    * to
    *    A(y) -> R(x,f(x)), B(f(x))
    * for f, fresh function associated with the input axiom
    */
-  case class Standard(func : String) extends SkolemStrategy
+  case class Standard(func: IRI) extends SkolemStrategy
   object Standard {
-    def apply(axiom : String) = new Standard(genFunctionString(axiom))
-    def genFunctionString(str : String) = "f_" ++ str.hashCode.toString
+    def apply(axiom: String) =
+      new Standard(IRI.create(genFunctionString(axiom)))
+    def genFunctionString(str: String) = "f_" ++ str.hashCode.toString
   }
 
   /* Constant skolemization
    *
-   * From 
+   * 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 : String) extends SkolemStrategy
+  case class Constant(const: IRI) extends SkolemStrategy
   object Constant {
-    def apply(axiom : String) = new Constant(genConstantString(axiom))
-    def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
+    def apply(axiom: String) =
+      new Constant(IRI.create(genConstantString(axiom)))
+    def genConstantString(str: String) = "c_" ++ str.hashCode.toString
   }
 
   /* (RSA) Constant skolemization
    * This is a special skolemization option to introduce additional atoms for RSA
    * checking algorithm.
    *
-   * From 
+   * 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
+  case class ConstantRSA(const: IRI) extends SkolemStrategy
   object ConstantRSA {
-    def apply(axiom : String) = new ConstantRSA(genConstantString(axiom))
-    def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
+    def apply(axiom: String) =
+      new ConstantRSA(IRI.create(genConstantString(axiom)))
+    def genConstantString(str: String) = "c_" ++ str.hashCode.toString
   }
 }
-
-- 
cgit v1.2.3