6 files changed, 261 insertions, 48 deletions

diff --git a/src/main/scala/rsacomb/Main.scala b/src/main/scala/rsacomb/Main.scala
index 9cd6680..d2bc2a8 100644
--- a/src/main/scala/rsacomb/Main.scala
+++ b/src/main/scala/rsacomb/Main.scala
@@ -48,18 +48,20 @@ object RSAComb {
      */
 
     val ontology = RSA.loadOntology(ontoPath)
-    ontology.isRSA
+    if (ontology.isRSA) {
 
-    /* Build canonical model */
-    //val tboxCanon = rsa.canonicalModel()
+      /* Build canonical model */
+      //val tboxCanon = rsa.canonicalModel()
 
-    /* Load query */
-    //val query = ...
+      /* Load query */
+      val query = RSA.test_query
 
-    /* Compute the filtering program from the given query */
-    //val tboxFilter = rsa.filteringProgram(query)
+      /* Compute the filtering program from the given query */
+      val filter = ontology.getFilteringProgram(query)
 
-    /* ... */
+      /* ... */
+
+    }
 
     /* DEBUG ONLY */
     println("Ok!")
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index b9d3ea2..467b3f1 100644
--- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
@@ -61,7 +61,8 @@ class RDFoxClassExprConverter(
 
   // OWLClass
   override def visit(expr: OWLClass): RDFoxRuleShards = {
-    val atom = List(Atom.rdf(term, IRI.RDF_TYPE, expr.getIRI()))
+    val iri: IRI = if (expr.isTopEntity()) IRI.THING else expr.getIRI()
+    val atom = List(Atom.rdf(term, IRI.RDF_TYPE, iri))
     RDFoxRuleShards(atom, List())
   }
 
@@ -97,6 +98,7 @@ class RDFoxClassExprConverter(
     // 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")
+    // Here we are assuming a role name
     val prop = expr.getProperty()
     // Computes the result of rule skolemization. Depending on the used
     // technique it might involve the introduction of additional atoms,
diff --git a/src/main/scala/rsacomb/RDFoxUtil.scala b/src/main/scala/rsacomb/RDFoxUtil.scala
index 4cefd83..9699fb4 100644
--- a/src/main/scala/rsacomb/RDFoxUtil.scala
+++ b/src/main/scala/rsacomb/RDFoxUtil.scala
@@ -15,6 +15,10 @@ object RDFoxUtil {
     IRI.create(iri.getIRIString())
   }
 
+  implicit def owlapi2rdfox(iri: String): IRI = {
+    IRI.create(iri)
+  }
+
   def openConnection(
       dataStore: String
   ): (ServerConnection, DataStoreConnection) = {
@@ -37,7 +41,7 @@ object RDFoxUtil {
     (server, data)
   }
 
-  def query(
+  def submitQuery(
       data: DataStoreConnection,
       prefixes: Prefixes,
       query: String
diff --git a/src/main/scala/rsacomb/RSA.scala b/src/main/scala/rsacomb/RSA.scala
index 79617c7..c0d4e51 100644
--- a/src/main/scala/rsacomb/RSA.scala
+++ b/src/main/scala/rsacomb/RSA.scala
@@ -8,6 +8,18 @@ import tech.oxfordsemantic.jrdfox.Prefixes
 import tech.oxfordsemantic.jrdfox.logic.IRI
 import org.semanticweb.owlapi.apibinding.OWLManager
 import org.semanticweb.owlapi.model.OWLOntology
+import rsacomb.RSAOntology
+
+// Debug only
+import tech.oxfordsemantic.jrdfox.logic.{
+  Formula,
+  Atom,
+  Variable,
+  Query,
+  QueryType,
+  Conjunction
+}
+import scala.collection.JavaConverters._
 
 object RSA extends RSAOntology {
 
@@ -18,6 +30,18 @@ object RSA extends RSAOntology {
   Prefixes.declarePrefix("rdfs:", "http://www.w3.org/2000/01/rdf-schema#")
   Prefixes.declarePrefix("owl:", "http://www.w3.org/2002/07/owl#")
 
+  val varX = Variable.create("X")
+  val varY = Variable.create("Y")
+  val varZ = Variable.create("Z")
+  val testAnswerVars = List[Variable](varX, varY, varZ).asJava;
+  val testFormula: Formula =
+    Conjunction.create(
+      Atom.rdf(varX, IRI.TOP_OBJECT_PROPERTY, varY),
+      Atom.rdf(varY, IRI.TOP_OBJECT_PROPERTY, varZ)
+    )
+  val test_query =
+    Query.create(QueryType.SELECT, false, testAnswerVars, testFormula)
+
   def internal(name: String): IRI =
     IRI.create(
       Prefixes.getPrefixIRIsByPrefixName.get("internal:").getIRI + name
diff --git a/src/main/scala/rsacomb/RSAAxiom.scala b/src/main/scala/rsacomb/RSAAxiom.scala
index 9e9a016..50dc37e 100644
--- a/src/main/scala/rsacomb/RSAAxiom.scala
+++ b/src/main/scala/rsacomb/RSAAxiom.scala
@@ -1,10 +1,23 @@
 package rsacomb
 
 /* Java imports */
-import org.semanticweb.owlapi.model.{OWLAxiom,OWLSubClassOfAxiom, OWLEquivalentClassesAxiom}
-import org.semanticweb.owlapi.model.{OWLObjectPropertyExpression,OWLClass,OWLClassExpression,OWLObjectSomeValuesFrom,OWLObjectMaxCardinality}
+import org.semanticweb.owlapi.model.{
+  OWLAxiom,
+  OWLSubClassOfAxiom,
+  OWLEquivalentClassesAxiom
+}
+import org.semanticweb.owlapi.model.{
+  OWLObjectPropertyExpression,
+  OWLClass,
+  OWLClassExpression,
+  OWLObjectSomeValuesFrom,
+  OWLObjectMaxCardinality
+}
 import org.semanticweb.owlapi.model.ClassExpressionType
-import org.semanticweb.owlapi.model.{OWLAxiomVisitorEx,OWLClassExpressionVisitorEx}
+import org.semanticweb.owlapi.model.{
+  OWLAxiomVisitorEx,
+  OWLClassExpressionVisitorEx
+}
 
 /* Wrapper trait for the implicit class `RSAAxiom`.
  */
@@ -16,10 +29,10 @@ trait RSAAxiom {
    */
   private sealed trait RSAAxiomType
   private object RSAAxiomType {
-    case object T3    extends RSAAxiomType // ∃R.A ⊑ B
+    case object T3 extends RSAAxiomType // ∃R.A ⊑ B
     case object T3top extends RSAAxiomType // ∃R.⊤ ⊑ B
-    case object T4    extends RSAAxiomType // A ⊑ ≤1R.B
-    case object T5    extends RSAAxiomType // A ⊑ ∃R.B
+    case object T4 extends RSAAxiomType // A ⊑ ≤1R.B
+    case object T5 extends RSAAxiomType // A ⊑ ∃R.B
   }
 
   /* Implements additional features on top of `OWLAxiom` from
@@ -32,20 +45,22 @@ trait RSAAxiom {
      * In order to reason about role unsafety in Horn-ALCHOIQ
      * ontologies we need to detect and filter axioms by their
      * "type".
-     * 
+     *
      * This is a simple implementation following the Visitor
      * pattern imposed by the OWLAPI.
      */
     private class RSAAxiomTypeDetector(t: RSAAxiomType)
-      extends OWLAxiomVisitorEx[Boolean]
-    {
-      override
-      def visit(axiom: OWLSubClassOfAxiom): Boolean = {
+        extends OWLAxiomVisitorEx[Boolean] {
+      override def visit(axiom: OWLSubClassOfAxiom): Boolean = {
         val sub = axiom.getSubClass().getClassExpressionType()
         val sup = axiom.getSuperClass().getClassExpressionType()
         t match {
           case RSAAxiomType.T3top => // ∃R.⊤ ⊑ B
-            axiom.isT5 && axiom.getSubClass().asInstanceOf[OWLObjectSomeValuesFrom].getFiller.isOWLThing
+            axiom.isT3 && axiom
+              .getSubClass()
+              .asInstanceOf[OWLObjectSomeValuesFrom]
+              .getFiller
+              .isOWLThing
           case RSAAxiomType.T3 => // ∃R.A ⊑ B
             sub == ClassExpressionType.OBJECT_SOME_VALUES_FROM && sup == ClassExpressionType.OWL_CLASS
           case RSAAxiomType.T4 => // A ⊑ ≤1R.B
@@ -55,13 +70,12 @@ trait RSAAxiom {
         }
       }
 
-      override
-      def visit(axiom: OWLEquivalentClassesAxiom): Boolean = {
+      override def visit(axiom: OWLEquivalentClassesAxiom): Boolean = {
         // TODO
         false
       }
 
-      def doDefault(axiom : OWLAxiom): Boolean = false
+      def doDefault(axiom: OWLAxiom): Boolean = false
     }
 
     private def isOfType(t: RSAAxiomType): Boolean = {
@@ -74,13 +88,13 @@ trait RSAAxiom {
     def isT3: Boolean = isOfType(RSAAxiomType.T3)
     def isT4: Boolean = isOfType(RSAAxiomType.T4)
     def isT5: Boolean = isOfType(RSAAxiomType.T5)
-    
+
     /* Extracting ObjectPropertyExpressions from axioms
      *
      * This extracts all ObjectPropertyExpressions from a given
      * axiom. While the implementation is generic we use it on axioms
      * of specific types (see above).
-     * 
+     *
      * NOTE: it is not possible to use the `objectPropertyInSignature`
      * method of `OWLAxiom` because it returns all "role names" involved
      * in the signature of an axiom. In particular we won't get the inverse
@@ -88,55 +102,61 @@ trait RSAAxiom {
      * itself instead).
      */
     private class RSAAxiomRoleExtractor()
-      extends OWLAxiomVisitorEx[List[OWLObjectPropertyExpression]]
-    {
+        extends OWLAxiomVisitorEx[List[OWLObjectPropertyExpression]] {
 
       private class RSAExprRoleExtractor()
-        extends OWLClassExpressionVisitorEx[List[OWLObjectPropertyExpression]]
-      {
-        override
-        def visit(expr: OWLObjectSomeValuesFrom): List[OWLObjectPropertyExpression] =
+          extends OWLClassExpressionVisitorEx[
+            List[OWLObjectPropertyExpression]
+          ] {
+        override def visit(
+            expr: OWLObjectSomeValuesFrom
+        ): List[OWLObjectPropertyExpression] =
           List(expr.getProperty)
 
-        override
-        def visit(expr: OWLObjectMaxCardinality): List[OWLObjectPropertyExpression] =
+        override def visit(
+            expr: OWLObjectMaxCardinality
+        ): List[OWLObjectPropertyExpression] =
           List(expr.getProperty)
 
         /* NOTE: this instance of `visit` for `OWLClass` shouldn't be necessary. However
          * if missing, the code throws a `NullPointerException`. It seems like, for some
-         * reason, `OWLClass` is not really a subinterface of `OWLClassExpression`, as 
+         * reason, `OWLClass` is not really a subinterface of `OWLClassExpression`, as
          * stated in the JavaDocs.
          */
-        override
-        def visit(expr: OWLClass): List[OWLObjectPropertyExpression] =
+        override def visit(expr: OWLClass): List[OWLObjectPropertyExpression] =
           List()
 
-        def doDefault(expr: OWLClassExpression): List[OWLObjectPropertyExpression] =
+        def doDefault(
+            expr: OWLClassExpression
+        ): List[OWLObjectPropertyExpression] =
           List()
       }
 
-      override
-      def visit(axiom: OWLSubClassOfAxiom): List[OWLObjectPropertyExpression] = {
+      override def visit(
+          axiom: OWLSubClassOfAxiom
+      ): List[OWLObjectPropertyExpression] = {
         val visitor = new RSAExprRoleExtractor()
         val sub = axiom.getSubClass.accept(visitor)
         val sup = axiom.getSuperClass.accept(visitor)
         sub ++ sup
       }
 
-      override
-      def visit(axiom: OWLEquivalentClassesAxiom): List[OWLObjectPropertyExpression] = {
+      override def visit(
+          axiom: OWLEquivalentClassesAxiom
+      ): List[OWLObjectPropertyExpression] = {
         // TODO
         List()
       }
 
-      def doDefault(axiom : OWLAxiom): List[OWLObjectPropertyExpression] = List()
+      def doDefault(axiom: OWLAxiom): List[OWLObjectPropertyExpression] = List()
     }
 
     /* Exposed methods */
-    def objectPropertyExpressionsInSignature: List[OWLObjectPropertyExpression] = {
+    def objectPropertyExpressionsInSignature
+        : List[OWLObjectPropertyExpression] = {
       val visitor = new RSAAxiomRoleExtractor()
       axiom.accept(visitor)
     }
   }
 
-} // trait RSAAxiom
\ No newline at end of file
+} // trait RSAAxiom
diff --git a/src/main/scala/rsacomb/RSAOntology.scala b/src/main/scala/rsacomb/RSAOntology.scala
index 3d9210e..9d52612 100644
--- a/src/main/scala/rsacomb/RSAOntology.scala
+++ b/src/main/scala/rsacomb/RSAOntology.scala
@@ -19,6 +19,7 @@ import scalax.collection.GraphEdge.UnDiEdge
 
 /* Debug only */
 import org.semanticweb.owlapi.dlsyntax.renderer.DLSyntaxObjectRenderer
+import tech.oxfordsemantic.jrdfox.logic._
 
 /* Wrapper trait for the implicit class `RSAOntology`.
  */
@@ -163,8 +164,9 @@ trait RSAOntology {
       } yield role1
 
       /* TODO: We should be able to avoid this last conversion to List.
-       * Maybe we should just move everything to Sets instead of Lists, since
-       * they have a more straightforward conversion from Java collections.
+       * Maybe we should just move everything to Sets instead of Lists,
+       * since they have a more straightforward conversion from Java
+       * collections.
        */
       (unsafe1 ++ unsafe2).toList
     }
@@ -184,6 +186,165 @@ trait RSAOntology {
       Graph(edges: _*)
     }
 
+    def getFilteringProgram(query: Query): List[Rule] = {
+
+      // Import implicit conversion to RDFox IRI
+      import RDFoxUtil._
+
+      sealed trait Reified;
+      case class ReifiedHead(bind: BindAtom, atoms: List[Atom]) extends Reified
+      case class ReifiedBody(atoms: List[Atom]) extends Reified
+      case class Unaltered(formula: BodyFormula) extends Reified
+
+      def getBindAtom(atom: Atom): BindAtom = {
+        // TODO: We need to implement another way to introduce fresh
+        // variables.
+        val varA = Variable.create("A")
+        val args = atom
+          .getArguments()
+          .asScala
+          .toSeq
+        //.prepended(atom.getTupleTableName.getIRI)
+        BindAtom.create(
+          BuiltinFunctionCall
+            .create("SKOLEM", args: _*),
+          varA
+        )
+      }
+
+      def reifyAtom(atom: Atom, variable: Variable): List[Atom] = {
+        def iri(i: Int) = atom.getTupleTableName().getIRI() ++ s"_$i"
+        atom
+          .getArguments()
+          .asScala
+          .zipWithIndex
+          .map { case (t, i) => Atom.rdf(variable, iri(i), t) }
+          .toList
+      }
+
+      // Is this the best way to determine if an atom is an RDF triple?
+      // Note that we can't use `getNumberOfArguments()` because is not
+      // "consistent":
+      // - for an atom created with `rdf(<term1>, <term2>, <term3>)`,
+      // `getNumberOfArguments` returns 3
+      // - for an atom created with `Atom.create(<tupletablename>, <term1>,
+      // <term2>, <term3>)`, `getNumberOfArguments()` returns 3
+      //
+      // This is probably because `Atom.rdf(...) is implemented as:
+      // ```scala
+      //  def rdf(term1: Term, term2: Term, term3: Term): Atom =
+      //    Atom.create(TupleTableName.create("internal:triple"), term1, term2, term3)
+      // ```
+      def isRdfTriple(atom: Atom): Boolean =
+        atom.getTupleTableName.getIRI.equals("internal:triple")
+
+      def reify(
+          formula: BodyFormula,
+          head: Boolean
+      ): Reified = {
+        def default[A <: BodyFormula](x: A) = Unaltered(x)
+        formula match {
+          case a: Atom => {
+            if (!isRdfTriple(a)) {
+              if (head) {
+                val b = getBindAtom(a)
+                ReifiedHead(b, reifyAtom(a, b.getBoundVariable))
+              } else {
+                val varA = Variable.create("A")
+                ReifiedBody(reifyAtom(a, varA))
+              }
+            } else {
+              default(a)
+            }
+          }
+          case a => default(a)
+        }
+      }
+
+      def skolemizeRule(rule: Rule): Rule = {
+        // Rule body
+        val body =
+          rule.getBody.asScala.map(reify(_, false)).flatMap {
+            case ReifiedHead(_, _) => List(); /* handle impossible case */
+            case ReifiedBody(x)    => x;
+            case Unaltered(x)      => List(x)
+          }
+        // Rule head
+        val reified = rule.getHead.asScala.map(reify(_, true))
+        val skols = reified.flatMap {
+          case ReifiedHead(x, _) => Some(x);
+          case ReifiedBody(_)    => None; /* handle impossible case */
+          case Unaltered(_)      => None
+        }
+        val head = reified.flatMap {
+          case ReifiedHead(_, x) => x;
+          case ReifiedBody(_)    => List(); /* handle impossible case */
+          case Unaltered(x) =>
+            List(x.asInstanceOf[Atom]) /* Can we do better that a cast? */
+        }
+        Rule.create(head.asJava, (skols ++ body).asJava)
+      }
+
+      def formulaToRuleBody(body: Formula): List[BodyFormula] = {
+        body match {
+          case a: BodyFormula => List(a);
+          case a: Conjunction =>
+            a.getConjuncts().asScala.toList.flatMap(formulaToRuleBody(_));
+          case _ => List() /* We don't handle this for now */
+        }
+      }
+
+      val body = formulaToRuleBody(query.getQueryFormula)
+      val vars: List[Term] = query.getAnswerVariables.asScala.toList
+      def id(t1: Term, t2: Term) =
+        Atom.create(
+          TupleTableName.create("http://127.0.0.1/ID"),
+          vars.appendedAll(List(t1, t2)).asJava
+        )
+      val qm = Atom.create(TupleTableName.create("QM"), vars.asJava)
+
+      /* Filtering program */
+      val rule1 = Rule.create(qm, body.asJava)
+      val rule3a =
+        for ((v, i) <- vars.zipWithIndex)
+          yield Rule.create(
+            id(
+              IRI.create(s"http://127.0.0.1/$i"),
+              IRI.create(s"http://127.0.0.1/$i")
+            ),
+            List(
+              qm,
+              Negation.create(
+                Atom.rdf(v, IRI.RDF_TYPE, IRI.create("http://127.0.0.1/NI"))
+              )
+            ).asJava
+          )
+      val rule3b = Rule.create(
+        id(Variable.create("V"), Variable.create("U")),
+        id(Variable.create("U"), Variable.create("V"))
+      )
+      val rule3c = Rule.create(
+        id(Variable.create("U"), Variable.create("W")),
+        List[BodyFormula](
+          id(Variable.create("U"), Variable.create("V")),
+          id(Variable.create("V"), Variable.create("W"))
+        ).asJava
+      )
+
+      var rules: List[Rule] =
+        List.empty
+          .prepended(rule3c)
+          .prepended(rule3b)
+          .prependedAll(rule3a)
+          .prepended(rule1)
+
+      // DEBUG
+      println("FILTERING PROGRAM:")
+      rules.map(skolemizeRule(_)).foreach(println(_))
+
+      List()
+    }
+
   } // implicit class RSAOntology
 
 } // trait RSAOntology