From 43234b253a74e71977ce29d0c7e2947e64fc6966 Mon Sep 17 00:00:00 2001
From: Federico Igne <federico.igne@cs.ox.ac.uk>
Date: Tue, 10 Nov 2020 17:16:02 +0000
Subject: Fix SKOLEM call creation during function skolemization

The first argument of a SKOLEM call needs to be a literal string. Note
that this is not enforced in any way by RDFox, that will fail silently.
---
 src/main/scala/rsacomb/RDFoxClassExprConverter.scala |  8 ++++----
 src/main/scala/rsacomb/SkolemStrategy.scala          | 20 ++++++++++++++++----
 2 files changed, 20 insertions(+), 8 deletions(-)

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

diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index de0f623..7f44ab1 100644
--- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
@@ -20,6 +20,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
 }
 import tech.oxfordsemantic.jrdfox.logic.expression.{
   Term,
+  Literal,
   Variable,
   FunctionCall,
   IRI
@@ -118,14 +119,13 @@ class RDFoxClassExprConverter(
         else
           (List(), List(), c)
       }
-      case SkolemStrategy.Standard(f) =>
-        // particular class for the "SKOLEM" operator and it is instead
-        // a simple builtin function with a "special" name.
+      case SkolemStrategy.Standard(f) => {
         (
           List(),
-          List(BindAtom.create(FunctionCall.create("SKOLEM", term), y)),
+          List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)),
           y
         )
+      }
     }
     val classVisitor =
       new RDFoxClassExprConverter(term1, unsafe, skolem, suffix)
diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala
index b05cd17..a2ad0a1 100644
--- a/src/main/scala/rsacomb/SkolemStrategy.scala
+++ b/src/main/scala/rsacomb/SkolemStrategy.scala
@@ -1,6 +1,7 @@
 package rsacomb
 
-import tech.oxfordsemantic.jrdfox.logic.expression.IRI
+import tech.oxfordsemantic.jrdfox.logic.Datatype
+import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, IRI}
 
 sealed trait SkolemStrategy
 
@@ -22,13 +23,24 @@ object SkolemStrategy {
    * From
    *    A ⊑ ∃R.B
    * to
-   *    A(y) -> R(x,f(x)), B(f(x))
+   *    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: IRI) extends SkolemStrategy
+  case class Standard(func: Literal) extends SkolemStrategy
   object Standard {
     def apply(axiom: String) =
-      new Standard(IRI.create(genFunctionString(axiom)))
+      new Standard(
+        Literal.create(genFunctionString(axiom), Datatype.XSD_STRING)
+      )
     def genFunctionString(str: String) = "f_" ++ str.hashCode.toString
   }
 
-- 
cgit v1.2.3