1 files changed, 17 insertions, 1 deletions

diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala
index 9df167f..bcf6828 100644
--- a/src/main/scala/rsacomb/SkolemStrategy.scala
+++ b/src/main/scala/rsacomb/SkolemStrategy.scala
@@ -29,7 +29,7 @@ object SkolemStrategy {
     def genFunctionString(str : String) = "f_" ++ str.hashCode.toString
   }
 
-  /* Functional skolemization
+  /* Constant skolemization
    *
    * From 
    *    A ⊑ ∃R.B
@@ -42,5 +42,21 @@ object SkolemStrategy {
     def apply(axiom : String) = new Constant(genConstantString(axiom))
     def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
   }
+
+  /* (RSA) Constant skolemization
+   * This is a special skolemization option to introduce additional atoms for RSA
+   * checking algorithm.
+   *
+   * From 
+   *    A ⊑ ∃R.B
+   * to
+   *    A(y) -> R(x,c), PE(x,c), B(c)
+   * for c, fresh constant associated with the input axiom and PE an internal predicate.
+   */
+  case class ConstantRSA(const : String) extends SkolemStrategy
+  object ConstantRSA {
+    def apply(axiom : String) = new ConstantRSA(genConstantString(axiom))
+    def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
+  }
 }