From 58b8d3c11a9deebb40e21c70d0b085d01cada745 Mon Sep 17 00:00:00 2001
From: Federico Igne <federico.igne@cs.ox.ac.uk>
Date: Wed, 15 Jul 2020 17:44:00 +0100
Subject: Add reworked code from previous repo

---
 src/main/scala/example/SkolemStrategy.scala | 46 +++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 src/main/scala/example/SkolemStrategy.scala

(limited to 'src/main/scala/example/SkolemStrategy.scala')

diff --git a/src/main/scala/example/SkolemStrategy.scala b/src/main/scala/example/SkolemStrategy.scala
new file mode 100644
index 0000000..9df167f
--- /dev/null
+++ b/src/main/scala/example/SkolemStrategy.scala
@@ -0,0 +1,46 @@
+package rsacomb
+
+sealed trait SkolemStrategy
+
+object SkolemStrategy {
+  // TODO: might want to use something else other than `hashCode` as a
+  // function to generate a fresh function/constant
+
+  /* No skolemization at all.
+   *
+   * From 
+   *    ∃R.A ⊑ B
+   * to
+   *    R(x,y), B(y) -> B(x)
+   */
+  case object None extends SkolemStrategy
+
+  /* Functional skolemization
+   *
+   * From 
+   *    A ⊑ ∃R.B
+   * to
+   *    A(y) -> R(x,f(x)), B(f(x))
+   * for f, fresh function associated with the input axiom
+   */
+  case class Standard(func : String) extends SkolemStrategy
+  object Standard {
+    def apply(axiom : String) = new Standard(genFunctionString(axiom))
+    def genFunctionString(str : String) = "f_" ++ str.hashCode.toString
+  }
+
+  /* Functional skolemization
+   *
+   * From 
+   *    A ⊑ ∃R.B
+   * to
+   *    A(y) -> R(x,c), B(c)
+   * for c, fresh constant associated with the input axiom
+   */
+  case class Constant(const : String) extends SkolemStrategy
+  object Constant {
+    def apply(axiom : String) = new Constant(genConstantString(axiom))
+    def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
+  }
+}
+
-- 
cgit v1.2.3