13 files changed, 40 insertions, 24 deletions

diff --git a/README.md b/README.md
index 1ce9b07..dbf0ead 100644
--- a/README.md
+++ b/README.md
@@ -71,8 +71,11 @@ The following is a summary of fixes (🔧), changes (🔄) and improvements (⚡
   ```
   where `rsa:named` is an internal predicate keeping track of all constants in the original ontology.
 
-+ ⚡ Both in the canonical model and the filtering program computations,
-  rules without a body are loaded into RDFox as facts.
++ ⚡ In Def. 3, regarding the generation of the logic program used for the RSA checkk, only T5 axioms involving an unsafe role will introduce the internal predicates `PE` and `U`.
+
++ ⚡ Both in the canonical model and the filtering program computations, rules without a body are loaded into RDFox as facts.
+
++ ⚡ The `cycle` function introduced in Def.4 establishing the direction of the *unraveling* of loops is defined over triples `(A,R,B)`. We are currently limiting the triple only to those appearing in a T5 axiom `A ⊑ ∃R.B`. Note that this greatly limits the size of cycle for a given triple, and as a consequence limits the number of rules used to compute the canonical model.
 
 ## References
 
diff --git a/build.sbt b/build.sbt
index 040f7c3..860b064 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,6 +1,6 @@
 import Dependencies._
 
-ThisBuild / scalaVersion          := "2.13.3"
+ThisBuild / scalaVersion          := "2.13.4"
 ThisBuild / version               := "0.1.0"
 ThisBuild / organization          := "uk.ac.ox.cs.rsacomb"
 ThisBuild / organizationName      := "Department of Computer Science - University of Oxford"
diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 1cafe11..39e8e2e 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -2,8 +2,8 @@ import sbt._
 
 object Dependencies {
   // Versions
-  lazy val scalatestVersion = "3.2.2"
-  lazy val owlapiVersion = "5.1.16"
+  lazy val scalatestVersion = "3.2.3"
+  lazy val owlapiVersion = "5.1.17"
   lazy val scalagraphVersion = "1.13.2"
 
   // Libraries
diff --git a/project/build.properties b/project/build.properties
index 0837f7a..7de0a93 100644
--- a/project/build.properties
+++ b/project/build.properties
@@ -1 +1 @@
-sbt.version=1.3.13
+sbt.version=1.4.4
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 c605e51..5001c8a 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -247,11 +247,10 @@ class CanonicalModel(val ontology: RSAOntology) {
         }
 
         case a: OWLSubObjectPropertyOfAxiom => {
-          val (factsF, rulesF) =
-            super.convert(a, term, unsafe, NoSkolem, Forward)
-          val (factsB, rulesB) =
-            super.convert(a, term, unsafe, NoSkolem, Backward)
-          (factsF ::: factsB, rulesF ::: rulesB)
+          val (facts, rules) = List(Empty, Forward, Backward)
+            .map(super.convert(a, term, unsafe, NoSkolem, _))
+            .unzip
+          (facts.flatten, rules.flatten)
         }
 
         case a => super.convert(a, term, unsafe, skolem, suffix)
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 79f2ef3..dc64c79 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -11,6 +11,7 @@ import org.semanticweb.owlapi.model.{OWLOntology, OWLAxiom, OWLLogicalAxiom}
 import org.semanticweb.owlapi.model.{
   OWLClass,
   OWLClassExpression,
+  OWLDataPropertyAssertionAxiom,
   OWLObjectProperty,
   OWLSubObjectPropertyOfAxiom,
   OWLObjectPropertyExpression,
@@ -35,7 +36,8 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{
   Term,
   Variable,
   IRI,
-  Resource
+  Resource,
+  Literal
 }
 import tech.oxfordsemantic.jrdfox.logic.sparql.statement.SelectQuery
 
@@ -122,6 +124,12 @@ class RSAOntology(val ontology: OWLOntology) {
       .map(implicits.RDFox.owlapiToRdfoxIri)
       .toList
 
+  val literals: List[Literal] =
+    abox
+      .collect { case a: OWLDataPropertyAssertionAxiom => a }
+      .map(_.getObject)
+      .map(implicits.RDFox.owlapiToRdfoxLiteral)
+
   val concepts: List[OWLClass] =
     ontology.getClassesInSignature().asScala.toList
 
@@ -298,7 +306,7 @@ class RSAOntology(val ontology: OWLOntology) {
 
   def filteringProgram(query: ConjunctiveQuery): FilteringProgram =
     Logger.timed(
-      new FilteringProgram(query, individuals),
+      new FilteringProgram(query, individuals ++ literals),
       "Generating filtering program",
       Logger.DEBUG
     )
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 6c83caf..6193296 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
@@ -225,7 +225,7 @@ trait RDFoxConverter {
         * @see [[org.semanticweb.owlapi.model.OWLDataPropertyAssertionAxiom OWLDataPropertyAssertionAxiom]]
         */
       case a: OWLDataPropertyAssertionAxiom =>
-        if (!a.getSubject.isNamed || !a.getObject.isNamed)
+        if (!a.getSubject.isNamed)
           Result()
         else {
           val subj = a.getSubject.asOWLNamedIndividual.getIRI
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/sparql/ConjunctiveQueryAnswers.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/sparql/ConjunctiveQueryAnswers.scala
index 50cbb86..667defc 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/sparql/ConjunctiveQueryAnswers.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/sparql/ConjunctiveQueryAnswers.scala
@@ -1,6 +1,11 @@
 package uk.ac.ox.cs.rsacomb.sparql
 
-import tech.oxfordsemantic.jrdfox.logic.expression.{IRI, Resource, Variable}
+import tech.oxfordsemantic.jrdfox.logic.expression.{
+  IRI,
+  Literal,
+  Resource,
+  Variable
+}
 
 /** A collections of answers to a query.
   *
@@ -30,8 +35,9 @@ class ConjunctiveQueryAnswers(
         val header = variables map (_.getName) mkString "\t"
         val body = answers
           .map(_.map {
-            case x: IRI => x.getIRI
-            case x      => x.toString
+            case x: IRI     => x.getIRI
+            case x: Literal => x.getLexicalForm
+            case x          => x.toString
           }.mkString("\t"))
           .mkString("\n")
         s"$header\n$body"
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 a7d7f27..0d18e66 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/CanonicalModelSpec.scala
@@ -1,4 +1,4 @@
-package rsacomb
+package uk.ac.ox.cs.rsacomb
 
 import java.io.File
 import org.scalatest.LoneElement
@@ -218,13 +218,13 @@ class Ontology1_CanonicalModelSpec
 
   renderer.render(
     SsubPropertyOfT
-  ) should "produce 2 rules" in {
+  ) should "produce 3 rules" in {
     val term = Variable.create("X")
     val unsafe = ontology.unsafeRoles
     val (facts, rules) =
       converter.convert(SsubPropertyOfT, term, unsafe, NoSkolem, Empty)
     facts shouldBe empty
-    rules should have length 2
+    rules should have length 3
   }
 
 }
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/FilteringProgramSpecs.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/FilteringProgramSpecs.scala
index 93e312c..e627bf7 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/FilteringProgramSpecs.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/FilteringProgramSpecs.scala
@@ -1,4 +1,4 @@
-package rsacomb
+package uk.ac.ox.cs.rsacomb
 
 import org.scalatest.flatspec.AnyFlatSpec
 import org.scalatest.matchers.should.Matchers
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLAxiomSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/OWLAxiomSpec.scala
index e1ece62..eb49c7d 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLAxiomSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/OWLAxiomSpec.scala
@@ -1,4 +1,4 @@
-package rsacomb
+package uk.ac.ox.cs.rsacomb.converter
 
 import java.util.{ArrayList => JList}
 import org.scalatest.LoneElement
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLClassSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/OWLClassSpec.scala
index def864b..09ab6eb 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/OWLClassSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/OWLClassSpec.scala
@@ -1,4 +1,4 @@
-package rsacomb
+package uk.ox.ac.cs.rsacomb.converter
 
 import java.util.{ArrayList => JList}
 
diff --git a/src/test/scala/uk/ac/ox/cs/rsacomb/RDFoxConverterSpec.scala b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverterSpec.scala
index 5c9fa96..a401abf 100644
--- a/src/test/scala/uk/ac/ox/cs/rsacomb/RDFoxConverterSpec.scala
+++ b/src/test/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverterSpec.scala
@@ -1,4 +1,4 @@
-package rsacomb
+package uk.ac.ox.cs.rsacomb.converter
 
 import org.scalatest.LoneElement
 import org.scalatest.flatspec.AnyFlatSpec