Introduce naive fresh variable generator

5 files changed, 45 insertions, 35 deletions

diff --git a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
index 0a79823..d90c966 100644
--- a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
@@ -1,6 +1,11 @@
 package rsacomb
 
-import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom, OWLObjectPropertyExpression}
+import org.semanticweb.owlapi.model.{
+  OWLAxiom,
+  OWLSubClassOfAxiom,
+  OWLEquivalentClassesAxiom,
+  OWLObjectPropertyExpression
+}
 import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
 
 import tech.oxfordsemantic.jrdfox.logic.{Rule, BodyFormula}
@@ -17,22 +22,24 @@ import org.semanticweb.owlapi.model.OWLObjectProperty
 object RDFoxAxiomConverter {
 
   def apply(
-    term : Term = Variable.create("x"),
-    skolem : SkolemStrategy = SkolemStrategy.None,
-    unsafe : List[OWLObjectPropertyExpression] = List()
-  ) : RDFoxAxiomConverter =
-          new RDFoxAxiomConverter(term, skolem, unsafe)
+      term: Term,
+      skolem: SkolemStrategy = SkolemStrategy.None,
+      unsafe: List[OWLObjectPropertyExpression] = List()
+  ): RDFoxAxiomConverter =
+    new RDFoxAxiomConverter(term, skolem, unsafe)
 
 } // object RDFoxAxiomConverter
 
-class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OWLObjectPropertyExpression])
-  extends OWLAxiomVisitorEx[List[Rule]]
-{
+class RDFoxAxiomConverter(
+    term: Term,
+    skolem: SkolemStrategy,
+    unsafe: List[OWLObjectPropertyExpression]
+) extends OWLAxiomVisitorEx[List[Rule]] {
 
-  override
-  def visit(axiom : OWLSubClassOfAxiom) : List[Rule] = {
+  override def visit(axiom: OWLSubClassOfAxiom): List[Rule] = {
     // Skolemization is needed only for the head of an axiom
-    val subVisitor = new RDFoxClassExprConverter(term,SkolemStrategy.None, unsafe)
+    val subVisitor =
+      new RDFoxClassExprConverter(term, SkolemStrategy.None, unsafe)
     val superVisitor = new RDFoxClassExprConverter(term, skolem, unsafe)
     // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext):
     // - the `res` List is a list of atoms resulting from the conversion
@@ -45,30 +52,27 @@ class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OW
     val sup = axiom.getSuperClass.accept(superVisitor)
     val head = sup.res.asJava
     val body = (sub.res ++ sup.ext).asJava
-    List(Rule.create(head,body))
+    List(Rule.create(head, body))
   }
 
-  override
-  def visit(axiom : OWLEquivalentClassesAxiom) : List[Rule] = {
+  override def visit(axiom: OWLEquivalentClassesAxiom): List[Rule] = {
     for {
       axiom1 <- axiom.asPairwiseAxioms.asScala.toList
       axiom2 <- axiom1.asOWLSubClassOfAxioms.asScala.toList
-      rule   <- axiom2.accept(this)
+      rule <- axiom2.accept(this)
     } yield rule
   }
 
-  override
-  def visit(axiom : OWLSubObjectPropertyOfAxiom) : List[Rule] = {
-    // TODO: variables needs to be handled at visitor level. Hardcoding
-    // the name of the varibles might lead to errors for complex cases.
-    val term1 = Variable.create("y")
-    val subVisitor = new RDFoxPropertyExprConverter(term,term1,SkolemStrategy.None)
-    val superVisitor = new RDFoxPropertyExprConverter(term,term1,skolem)
+  override def visit(axiom: OWLSubObjectPropertyOfAxiom): List[Rule] = {
+    val term1 = RSA.getFreshVariable()
+    val subVisitor =
+      new RDFoxPropertyExprConverter(term, term1, SkolemStrategy.None)
+    val superVisitor = new RDFoxPropertyExprConverter(term, term1, skolem)
     val body: List[BodyFormula] = axiom.getSubProperty.accept(subVisitor)
     val head: List[Atom] = axiom.getSuperProperty.accept(superVisitor)
-    List(Rule.create(head.asJava,body.asJava))
+    List(Rule.create(head.asJava, body.asJava))
   }
 
-  def doDefault(axiom : OWLAxiom) : List[Rule] = List()
+  def doDefault(axiom: OWLAxiom): List[Rule] = List()
 
 } // class RDFoxAxiomConverter
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index 467b3f1..a319d86 100644
--- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
@@ -34,7 +34,7 @@ import org.semanticweb.owlapi.model.OWLObjectProperty
 object RDFoxClassExprConverter {
 
   def apply(
-      term: Term = Variable.create("x"),
+      term: Term,
       skolem: SkolemStrategy = SkolemStrategy.None,
       unsafe: List[OWLObjectPropertyExpression] = List()
   ): RDFoxClassExprConverter =
@@ -95,9 +95,7 @@ class RDFoxClassExprConverter(
 
   // OWLObjectSomeValuesFrom
   override def visit(expr: OWLObjectSomeValuesFrom): RDFoxRuleShards = {
-    // 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")
+    val y = RSA.getFreshVariable()
     // Here we are assuming a role name
     val prop = expr.getProperty()
     // Computes the result of rule skolemization. Depending on the used
@@ -141,7 +139,7 @@ class RDFoxClassExprConverter(
   // OWLObjectMaxCardinality
   override def visit(expr: OWLObjectMaxCardinality): RDFoxRuleShards = {
     // TODO: again, no hardcoded variables
-    val vars = List(Variable.create("y"), Variable.create("z"))
+    val vars = List(RSA.getFreshVariable(), RSA.getFreshVariable())
     val classResult = RDFoxClassExprConverter.merge(
       vars
         .map(new RDFoxClassExprConverter(_, skolem, unsafe))
diff --git a/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala b/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
index 340fa90..6eecdbf 100644
--- a/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
@@ -3,7 +3,7 @@ package rsacomb
 import org.semanticweb.owlapi.model.{OWLPropertyExpression, OWLObjectProperty}
 import org.semanticweb.owlapi.model.OWLPropertyExpressionVisitorEx
 
-import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, IRI, Variable, Literal}
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, IRI, Literal}
 
 import rsacomb.SkolemStrategy
 import org.semanticweb.owlapi.model.OWLObjectInverseOf
diff --git a/src/main/scala/rsacomb/RSA.scala b/src/main/scala/rsacomb/RSA.scala
index c0d4e51..edd3758 100644
--- a/src/main/scala/rsacomb/RSA.scala
+++ b/src/main/scala/rsacomb/RSA.scala
@@ -30,6 +30,14 @@ 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#")
 
+  // Counter used to implement a simple fresh variable generator
+  private var counter = -1;
+
+  def getFreshVariable(): Variable = {
+    counter += 1
+    Variable.create(f"I$counter%03d")
+  }
+
   val varX = Variable.create("X")
   val varY = Variable.create("Y")
   val varZ = Variable.create("Z")
diff --git a/src/main/scala/rsacomb/RSAOntology.scala b/src/main/scala/rsacomb/RSAOntology.scala
index 5846672..06351d5 100644
--- a/src/main/scala/rsacomb/RSAOntology.scala
+++ b/src/main/scala/rsacomb/RSAOntology.scala
@@ -61,7 +61,7 @@ trait RSAOntology {
       val datalog = for {
         axiom <- axioms
         visitor = new RDFoxAxiomConverter(
-          Variable.create("x"),
+          RSA.getFreshVariable(),
           SkolemStrategy.ConstantRSA(axiom.toString),
           unsafe
         )
@@ -199,7 +199,7 @@ trait RSAOntology {
       def getBindAtom(atom: Atom): BindAtom = {
         // TODO: We need to implement another way to introduce fresh
         // variables.
-        val varA = Variable.create("A")
+        val newvar = RSA.getFreshVariable()
         val name =
           Literal.create(atom.getTupleTableName.getIRI, Datatype.XSD_STRING)
         val args = atom
@@ -210,7 +210,7 @@ trait RSAOntology {
         BindAtom.create(
           BuiltinFunctionCall
             .create("SKOLEM", args: _*),
-          varA
+          newvar
         )
       }
 
@@ -252,7 +252,7 @@ trait RSAOntology {
                 val b = getBindAtom(a)
                 ReifiedHead(b, reifyAtom(a, b.getBoundVariable))
               } else {
-                val varA = Variable.create("A")
+                val varA = RSA.getFreshVariable()
                 ReifiedBody(reifyAtom(a, varA))
               }
             } else {