Add full set of rules for filtering program

4 files changed, 363 insertions, 102 deletions

diff --git a/src/main/scala/rsacomb/FilteringProgram.scala b/src/main/scala/rsacomb/FilteringProgram.scala
new file mode 100644
index 0000000..91c98d8
--- /dev/null
+++ b/src/main/scala/rsacomb/FilteringProgram.scala
@@ -0,0 +1,295 @@
+package rsacomb
+
+import tech.oxfordsemantic.jrdfox.logic._
+import scala.collection.JavaConverters._
+
+class FilteringProgram(query: Query, constants: List[Term]) extends RDFTriple {
+
+  private val bounded: List[Term] = this.getBoundedVariables
+  private val answer: List[Term] = query.getAnswerVariables.asScala.toList
+
+  val facts: List[Atom] = constants.map(named)
+  val rules: List[Rule] = this.generateFilteringProgram()
+
+  private def named(t: Term): Atom =
+    Atom.rdf(t, IRI.RDF_TYPE, RSA.internal("NAMED"))
+
+  private def getBoundedVariables: List[Variable] = List()
+
+  private def generateFilteringProgram(): List[Rule] = {
+    // Query formula as a rule body
+    val body = queryToBody(query.getQueryFormula)
+    // Auxiliar predicates/helpers
+    def not(atom: Atom): BodyFormula = Negation.create(atom)
+    val predQM =
+      Atom.create(
+        TupleTableName.create(RSA.internal("QM").getIRI),
+        (answer ++ bounded): _*
+      )
+    def predID(t1: Term, t2: Term) =
+      Atom.create(
+        TupleTableName.create(RSA.internal("ID").getIRI),
+        (answer ++ bounded).appended(t1).appended(t2): _*
+      )
+    def predNI(t1: Term): Atom =
+      Atom.rdf(t1, IRI.RDF_TYPE, RSA.internal("NI"))
+    def predTQ(sx: String, t1: Term, t2: Term) =
+      Atom.create(
+        TupleTableName.create(RSA.internal(s"TQ_$sx").getIRI),
+        (answer ++ bounded).appended(t1).appended(t2): _*
+      )
+    def predAQ(sx: String, t1: Term, t2: Term) =
+      Atom.create(
+        TupleTableName.create(RSA.internal(s"AQ_$sx").getIRI),
+        (answer ++ bounded).appended(t1).appended(t2): _*
+      )
+    val predFK =
+      Atom.create(
+        TupleTableName.create(RSA.internal("FK").getIRI),
+        (answer ++ bounded): _*
+      )
+    val predSP =
+      Atom.create(
+        TupleTableName.create(RSA.internal("SP").getIRI),
+        (answer ++ bounded): _*
+      )
+    val predANS =
+      Atom.create(
+        TupleTableName.create(RSA.internal("ANS").getIRI),
+        answer: _*
+      )
+
+    /* Rule 1 */
+    val r1 = Rule.create(predQM, body: _*)
+
+    /* Rules 3x */
+    val r3a =
+      for ((v, i) <- bounded.zipWithIndex)
+        yield Rule.create(
+          predID(RSA.internal(i), RSA.internal(i)),
+          predQM,
+          not(predNI(v))
+        )
+    val r3b = Rule.create(
+      predID(Variable.create("V"), Variable.create("U")),
+      predID(Variable.create("U"), Variable.create("V"))
+    )
+    val r3c = Rule.create(
+      predID(Variable.create("U"), Variable.create("W")),
+      predID(Variable.create("U"), Variable.create("V")),
+      predID(Variable.create("V"), Variable.create("W"))
+    )
+
+    /* Rules 4x */
+    val r4a = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1 getArgument 2)
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2 getArgument 2)
+    } yield Rule.create(
+      predFK,
+      role1 suffix "_f",
+      role2 suffix "_f",
+      predID(
+        RSA.internal(bounded.indexOf(role1 getArgument 2)),
+        RSA.internal(bounded.indexOf(role2 getArgument 2))
+      ),
+      not(Atom.rdf(role1 getArgument 0, IRI.SAME_AS, role2 getArgument 0))
+    )
+    val r4b = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1 getArgument 2)
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2 getArgument 0)
+    } yield Rule.create(
+      predFK,
+      role1 suffix "_f",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded.indexOf(role1 getArgument 2)),
+        RSA.internal(bounded.indexOf(role2 getArgument 0))
+      ),
+      not(Atom.rdf(role1 getArgument 0, IRI.SAME_AS, role2 getArgument 2))
+    )
+    val r4c = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1 getArgument 0)
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2 getArgument 0)
+    } yield Rule.create(
+      predFK,
+      role1 suffix "_b",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded.indexOf(role1 getArgument 0)),
+        RSA.internal(bounded.indexOf(role2 getArgument 0))
+      ),
+      not(Atom.rdf(role1 getArgument 2, IRI.SAME_AS, role2 getArgument 2))
+    )
+
+    /* Rules 5x */
+    val r5a = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1 getArgument 0
+      role1arg2 = role1 getArgument 2
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2 getArgument 0
+      role2arg2 = role2 getArgument 2
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      predID(
+        RSA.internal(bounded indexOf role1arg0),
+        RSA.internal(bounded indexOf role2arg0)
+      ),
+      role1 suffix "_f",
+      role2 suffix "_f",
+      predID(
+        RSA.internal(bounded indexOf role1arg2),
+        RSA.internal(bounded indexOf role2arg2)
+      ),
+      Atom.rdf(role1arg0, IRI.SAME_AS, role2arg0),
+      not(predNI(role1arg0))
+    )
+    val r5b = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1 getArgument 0
+      role1arg2 = role1 getArgument 2
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2 getArgument 0
+      role2arg2 = role2 getArgument 2
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      predID(
+        RSA.internal(bounded indexOf role1arg0),
+        RSA.internal(bounded indexOf role2arg2)
+      ),
+      role1 suffix "_f",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded indexOf role1arg2),
+        RSA.internal(bounded indexOf role2arg0)
+      ),
+      Atom.rdf(role1arg0, IRI.SAME_AS, role2arg2),
+      not(predNI(role1arg0))
+    )
+    val r5c = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1 getArgument 0
+      role1arg2 = role1 getArgument 2
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2 getArgument 0
+      role2arg2 = role2 getArgument 2
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      predID(
+        RSA.internal(bounded indexOf role1arg2),
+        RSA.internal(bounded indexOf role2arg2)
+      ),
+      role1 suffix "_b",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded indexOf role1arg0),
+        RSA.internal(bounded indexOf role2arg0)
+      ),
+      Atom.rdf(role1arg2, IRI.SAME_AS, role2arg2),
+      not(predNI(role1arg2))
+    )
+
+    /* Rules 6 */
+    val r6 = for {
+      role <- body.filter(_.isRoleAssertion)
+      arg0 = role getArgument 0
+      arg2 = role getArgument 2
+      if bounded contains arg0
+      if bounded contains arg2
+      sx <- List("_f", "_b")
+    } yield Rule.create(
+      predAQ(sx, Variable.create("V"), Variable.create("W")),
+      role suffix sx,
+      predID(
+        RSA.internal(bounded indexOf arg0),
+        RSA.internal(Variable.create("V"))
+      ),
+      predID(
+        RSA.internal(bounded indexOf arg2),
+        RSA.internal(Variable.create("W"))
+      )
+    )
+
+    /* Rules 7x */
+    val r7a =
+      for (sx <- List("f", "b"))
+        yield Rule.create(
+          predTQ(sx, Variable.create("U"), Variable.create("V")),
+          predAQ(sx, Variable.create("U"), Variable.create("V"))
+        )
+    val r7b =
+      for (r <- List("f", "b"))
+        yield Rule.create(
+          predTQ(r, Variable.create("U"), Variable.create("W")),
+          predAQ(r, Variable.create("U"), Variable.create("V")),
+          predTQ(r, Variable.create("V"), Variable.create("W"))
+        )
+
+    /* Rules 8x */
+    val r8a =
+      for (v <- answer) yield Rule.create(predSP, predQM, not(named(v)))
+    val r8b =
+      Rule.create(predSP, predFK)
+    val r8c =
+      for (sx <- List("_f", "_b"))
+        yield Rule.create(
+          predSP,
+          predTQ(sx, Variable.create("V"), Variable.create("V"))
+        )
+
+    /* Rule 9 */
+    val r9 = Rule.create(predANS, predQM, not(predSP))
+
+    List.empty
+      .prepended(r9)
+      .prependedAll(r8c)
+      .prepended(r8b)
+      .prependedAll(r8a)
+      .prependedAll(r7b)
+      .prependedAll(r7a)
+      .prependedAll(r6)
+      .prependedAll(r5c)
+      .prependedAll(r5b)
+      .prependedAll(r5a)
+      .prependedAll(r4c)
+      .prependedAll(r4b)
+      .prependedAll(r4a)
+      .prepended(r3c)
+      .prepended(r3b)
+      .prependedAll(r3a)
+      .prepended(r1)
+  }
+
+  /* NOTE: we are restricting to queries that contain conjunctions of
+   * atoms for the time being. This might need to be reviewed in the
+   * future.
+   */
+  private def queryToBody(body: Formula): List[Atom] =
+    body match {
+      case a: Atom => List(a);
+      case a: Conjunction =>
+        a.getConjuncts.asScala.toList.flatMap(queryToBody);
+      case _ => List()
+    }
+
+} // class FilteringProgram
+
+object FilteringProgram {
+  def apply(query: Query, constants: List[Term]): FilteringProgram =
+    new FilteringProgram(query, constants)
+}
diff --git a/src/main/scala/rsacomb/RDFTriple.scala b/src/main/scala/rsacomb/RDFTriple.scala
new file mode 100644
index 0000000..11ad6d4
--- /dev/null
+++ b/src/main/scala/rsacomb/RDFTriple.scala
@@ -0,0 +1,60 @@
+package rsacomb
+
+import tech.oxfordsemantic.jrdfox.logic.{Atom, IRI, TupleTableName}
+
+trait RDFTriple {
+
+  implicit class RDFTriple(atom: Atom) {
+
+    /* 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: Boolean =
+      atom.getTupleTableName.getIRI.equals("internal:triple")
+
+    def isClassAssertion: Boolean =
+      atom.isRdfTriple && atom.getArgument(1).equals(IRI.RDF_TYPE)
+
+    def isRoleAssertion: Boolean =
+      atom.isRdfTriple && !atom.getArgument(1).equals(IRI.RDF_TYPE)
+
+    def suffix(sx: String): Atom =
+      if (this.isClassAssertion) {
+        val newclass = atom.getArgument(2) match {
+          case iri: IRI => IRI.create(iri.getIRI.appendedAll(sx))
+          case other    => other
+        }
+        Atom.rdf(
+          atom getArgument 0,
+          atom getArgument 1,
+          newclass
+        )
+      } else if (this.isRoleAssertion) {
+        val newrole = atom.getArgument(1) match {
+          case iri: IRI => IRI.create(iri.getIRI.appendedAll(sx))
+          case other    => other
+        }
+        Atom.rdf(
+          atom getArgument 0,
+          newrole,
+          atom getArgument 2
+        )
+      } else {
+        val newname =
+          TupleTableName.create(atom.getTupleTableName.getIRI.appendedAll(sx))
+        Atom.create(newname, atom.getArguments())
+      }
+  }
+
+}
diff --git a/src/main/scala/rsacomb/RSA.scala b/src/main/scala/rsacomb/RSA.scala
index edd3758..9125f9f 100644
--- a/src/main/scala/rsacomb/RSA.scala
+++ b/src/main/scala/rsacomb/RSA.scala
@@ -50,9 +50,10 @@ object RSA extends RSAOntology {
   val test_query =
     Query.create(QueryType.SELECT, false, testAnswerVars, testFormula)
 
-  def internal(name: String): IRI =
+  def internal(name: Any): IRI =
     IRI.create(
-      Prefixes.getPrefixIRIsByPrefixName.get("internal:").getIRI + name
+      Prefixes.getPrefixIRIsByPrefixName.get("internal:").getIRI
+        + name.toString
     )
 
   // TODO: move this somewhere else... maybe an OntoUtils class or something.
diff --git a/src/main/scala/rsacomb/RSAOntology.scala b/src/main/scala/rsacomb/RSAOntology.scala
index e49d4ac..efd6e7f 100644
--- a/src/main/scala/rsacomb/RSAOntology.scala
+++ b/src/main/scala/rsacomb/RSAOntology.scala
@@ -28,7 +28,9 @@ trait RSAOntology {
   /* Implements additional features to reason about RSA ontologies
    * on top of `OWLOntology` from the OWLAPI.
    */
-  implicit class RSAOntology(ontology: OWLOntology) extends RSAAxiom {
+  implicit class RSAOntology(ontology: OWLOntology)
+      extends RSAAxiom
+      with RDFTriple {
 
     /* Steps for RSA check
      * 1) convert ontology axioms into LP rules
@@ -224,28 +226,6 @@ trait RSAOntology {
           .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 isClassAssertion(atom: Atom): Boolean =
-        isRdfTriple(atom) && atom.getArgument(1).equals(IRI.RDF_TYPE)
-
-      def isRoleAssertion(atom: Atom): Boolean =
-        isRdfTriple(atom) && !atom.getArgument(1).equals(IRI.RDF_TYPE)
-
       def reify(
           formula: BodyFormula,
           head: Boolean
@@ -253,7 +233,7 @@ trait RSAOntology {
         def default[A <: BodyFormula](x: A) = Unaltered(x)
         formula match {
           case a: Atom => {
-            if (!isRdfTriple(a)) {
+            if (!a.isRdfTriple) {
               if (head) {
                 val b = getBindAtom(a)
                 ReifiedHead(b, reifyAtom(a, b.getBoundVariable))
@@ -293,83 +273,8 @@ trait RSAOntology {
         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 bounded: List[Term] = List()
-      val answer: List[Term] = query.getAnswerVariables.asScala.toList
-      def id(t1: Term, t2: Term) =
-        Atom.create(
-          TupleTableName.create("http://127.0.0.1/ID"),
-          (bounded ++ answer).appendedAll(List(t1, t2)).asJava
-        )
-      def tq(suffix: String, t1: Term, t2: Term) =
-        Atom.create(
-          TupleTableName.create(s"http://127.0.0.1/TQ$suffix"),
-          (bounded ++ answer).appendedAll(List(t1, t2)).asJava
-        )
-      def aq(suffix: String, t1: Term, t2: Term) =
-        Atom.create(
-          TupleTableName.create(s"http://127.0.0.1/AQ$suffix"),
-          (bounded ++ answer).appendedAll(List(t1, t2)).asJava
-        )
-      val qm =
-        Atom.create(TupleTableName.create("QM"), (bounded ++ answer).asJava)
-
-      /* Filtering program */
-      val rule1 = Rule.create(qm, body.asJava)
-      val rule3a =
-        for ((v, i) <- answer.zipWithIndex)
-          yield Rule.create(
-            id(
-              IRI.create(s"http://127.0.0.1/$i"),
-              IRI.create(s"http://127.0.0.1/$i")
-            ),
-            qm,
-            Negation.create(
-              Atom.rdf(v, IRI.RDF_TYPE, IRI.create("http://127.0.0.1/NI"))
-            )
-          )
-      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")),
-        id(Variable.create("U"), Variable.create("V")),
-        id(Variable.create("V"), Variable.create("W"))
-      )
-      val rule7a =
-        for (r <- Seq("f", "b"))
-          yield Rule.create(
-            tq(r, Variable.create("U"), Variable.create("V")),
-            aq(r, Variable.create("U"), Variable.create("V"))
-          )
-      val rule7b =
-        for (r <- Seq("f", "b"))
-          yield Rule.create(
-            tq(r, Variable.create("U"), Variable.create("W")),
-            aq(r, Variable.create("U"), Variable.create("V")),
-            tq(r, Variable.create("V"), Variable.create("W"))
-          )
-
-      var rules: List[Rule] =
-        List.empty
-          .prependedAll(rule7b)
-          .prependedAll(rule7a)
-          .prepended(rule3c)
-          .prepended(rule3b)
-          .prependedAll(rule3a)
-          .prepended(rule1)
-
       // DEBUG
+      val rules = FilteringProgram(query, List()).rules
       println("FILTERING PROGRAM:")
       rules.map(skolemizeRule(_)).foreach(println(_))