From 73cec6661a74153f16cc34f3c143d0cc78e64a42 Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 29 Apr 2021 18:44:25 +0200
Subject: [PATCH] Remove failing function and test suite

---
 src/main/scala/z3/scala/Z3Context.scala | 18 ------------
 src/test/scala/z3/scala/Abs.scala       | 38 -------------------------
 2 files changed, 56 deletions(-)
 delete mode 100644 src/test/scala/z3/scala/Abs.scala

diff --git a/src/main/scala/z3/scala/Z3Context.scala b/src/main/scala/z3/scala/Z3Context.scala
index edd2ec5..b2e952c 100644
--- a/src/main/scala/z3/scala/Z3Context.scala
+++ b/src/main/scala/z3/scala/Z3Context.scala
@@ -1024,24 +1024,6 @@ sealed class Z3Context(val config: Map[String, String]) {
     res
   }
 
-  // XXX: this is a HUGE hack to get around the fact that the Z3 api doesn't
-  //      provide a handle to the absolute value function.
-  def getAbsFuncDecl(): Z3FuncDecl = {
-    val ast = parseSMTLIB2String("""
-      (declare-fun x () Int)
-      (declare-fun y () Int)
-      (assert (= y (abs x)))
-    """)
-
-    getASTKind(ast) match {
-      case Z3AppAST(_, Seq(_, absAst)) => getASTKind(absAst) match {
-        case Z3AppAST(decl, _) => decl
-        case c => error("Unexpected ast kind " + c)
-      }
-      case c => error("Unexpected ast kind " + c)
-    }
-  }
-
   // Parser interface
   private def parseSMTLIB2(file: Boolean, str: String) : Z3AST = {
     if(file) {
diff --git a/src/test/scala/z3/scala/Abs.scala b/src/test/scala/z3/scala/Abs.scala
deleted file mode 100644
index c33d418..0000000
--- a/src/test/scala/z3/scala/Abs.scala
+++ /dev/null
@@ -1,38 +0,0 @@
-package z3.scala
-
-import org.scalatest.{FunSuite, Matchers}
-
-class Abs extends FunSuite with Matchers {
-
-  test("array-map absolute value") {
-    val z3 = new Z3Context("MODEL" -> true)
-
-    val is = z3.mkIntSort
-    val intArraySort = z3.mkArraySort(is, is)
-    val array1 = z3.mkFreshConst("arr", intArraySort)
-    val array2 = z3.mkFreshConst("arr", intArraySort)
-
-    val abs = z3.getAbsFuncDecl()
-
-    val solver = z3.mkSolver
-
-    solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(0, is)), z3.mkInt(1, is)))
-    solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(1, is)), z3.mkInt(0, is)))
-    solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(2, is)), z3.mkInt(-1, is)))
-
-    solver.assertCnstr(z3.mkEq(array2, z3.mkArrayMap(abs, array1)))
-    
-    val (result, model) = solver.checkAndGetModel
-
-    result should equal(Some(true))
-
-    val array2Ev = model.eval(array2)
-    array2Ev should be (Symbol("defined"))
-    val array2Val = model.getArrayValue(array2Ev.get)
-    array2Val should be (Symbol("defined"))
-    val (valueMap, default) = array2Val.get
-    valueMap(z3.mkInt(0, is)) should equal (z3.mkInt(1, is))
-    valueMap(z3.mkInt(1, is)) should equal (z3.mkInt(0, is))
-    valueMap(z3.mkInt(2, is)) should equal (z3.mkInt(1, is))
-  }
-}