From c59f14d146d2c6bd2eb6378965370ae86e1241c9 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain.ruetschi@gmail.com>
Date: Wed, 4 Sep 2019 15:26:21 +0200
Subject: [PATCH] Add test for Int<->BigInt conversions

Also implement model extraction for BigInt,
as well as more robust model extraction for Int.
---
 src/main/scala/z3/scala/Z3Model.scala        | 42 ++++++++----
 src/test/scala/z3/scala/IntConversions.scala | 69 ++++++++++++++++++++
 src/test/scala/z3/scala/IntExtraction.scala  | 26 ++++++++
 3 files changed, 123 insertions(+), 14 deletions(-)
 create mode 100644 src/test/scala/z3/scala/IntConversions.scala
 create mode 100644 src/test/scala/z3/scala/IntExtraction.scala

diff --git a/src/main/scala/z3/scala/Z3Model.scala b/src/main/scala/z3/scala/Z3Model.scala
index f50e675..413fbbd 100644
--- a/src/main/scala/z3/scala/Z3Model.scala
+++ b/src/main/scala/z3/scala/Z3Model.scala
@@ -1,30 +1,44 @@
 package z3.scala
 
+import scala.util.Try
 import com.microsoft.z3.Native
 
 object Z3Model {
-  implicit def ast2int(model: Z3Model, ast: Z3AST): Option[Int] = {
-    val res = model.eval(ast)
-    if (res.isEmpty)
+  private def parseInt(str: String): Option[Int] = {
+    if (str.startsWith("#b"))
+      Try(BigInt(str.drop(2), 2).toInt).toOption
+    else if (str.startsWith("#x"))
+      Try(BigInt(str.drop(2), 16).toInt).toOption
+    else if (str.startsWith("#"))
       None
     else
-      model.context.getNumeralInt(res.get).value
+      Try(Integer.parseInt(str, 10)).toOption
+  }
+
+  implicit def ast2bigint(model: Z3Model, ast: Z3AST): Option[BigInt] = {
+    model.eval(ast) flatMap { res =>
+      model.context.getNumeralInt(res).value.map(BigInt(_)).orElse {
+        Some(BigInt(res.toString, 10))
+      }
+    }
+  }
+
+  implicit def ast2int(model: Z3Model, ast: Z3AST): Option[Int] = {
+    model.eval(ast) flatMap { res =>
+      model.context.getNumeralInt(res).value.orElse(parseInt(res.toString))
+    }
   }
 
   implicit def ast2bool(model: Z3Model, ast: Z3AST): Option[Boolean] = {
-    val res = model.eval(ast)
-    if (res.isEmpty)
-      None
-    else
-      model.context.getBoolValue(res.get)
+    model.eval(ast) flatMap { res =>
+      model.context.getBoolValue(res)
+    }
   }
 
   implicit def ast2char(model: Z3Model, ast: Z3AST): Option[Char] = {
-    val res = model.eval(ast)
-    if (res.isEmpty)
-      None
-    else
-      model.context.getNumeralInt(res.get).value.map(_.toChar)
+    model.eval(ast) flatMap { res =>
+      model.context.getNumeralInt(res).value.map(_.toChar)
+    }
   }
 }
 
diff --git a/src/test/scala/z3/scala/IntConversions.scala b/src/test/scala/z3/scala/IntConversions.scala
new file mode 100644
index 0000000..6ab8c56
--- /dev/null
+++ b/src/test/scala/z3/scala/IntConversions.scala
@@ -0,0 +1,69 @@
+package z3.scala
+
+import org.scalatest.{FunSuite, Matchers}
+
+class IntConversions extends FunSuite with Matchers {
+
+  testIntToBigInt(0)
+  testIntToBigInt(42)
+  testIntToBigInt(-42)
+  testIntToBigInt(Int.MinValue)
+  testIntToBigInt(Int.MaxValue)
+
+  testBigIntToInt(0)
+  testBigIntToInt(42)
+  testBigIntToInt(-42)
+  testBigIntToInt(Int.MinValue)
+  testBigIntToInt(Int.MaxValue)
+
+  private def testIntToBigInt(value: Int): Unit = test(s"Int -> BigInt: $value") {
+    val z3 = new Z3Context("MODEL" -> true)
+
+    val Int  = z3.mkIntSort
+    val BV32 = z3.mkBVSort(32)
+
+    val in  = z3.mkConst(z3.mkStringSymbol("in"), BV32)
+    val out = z3.mkConst(z3.mkStringSymbol("out"), Int)
+
+    val solver = z3.mkSolver
+
+    solver.assertCnstr(z3.mkEq(in,  z3.mkInt(value, BV32)))
+    solver.assertCnstr(z3.mkEq(out, z3.mkBV2Int(in, true)))
+
+    solver.assertCnstr(z3.mkNot(
+      z3.mkEq(out, z3.mkInt(value, Int))
+    ))
+
+    val (sol, model) = solver.checkAndGetModel
+
+    (sol, model) should equal((Some(false), null))
+
+    z3.delete
+  }
+
+  private def testBigIntToInt(value: Int): Unit = test(s"BigInt -> Int: $value") {
+    val z3 = new Z3Context("MODEL" -> true)
+
+    val Int  = z3.mkIntSort
+    val BV32 = z3.mkBVSort(32)
+
+    val in  = z3.mkConst(z3.mkStringSymbol("in"), Int)
+    val out = z3.mkConst(z3.mkStringSymbol("out"), BV32)
+
+    val solver = z3.mkSolver
+
+    solver.assertCnstr(z3.mkEq(in,  z3.mkInt(value, Int)))
+    solver.assertCnstr(z3.mkEq(out, z3.mkInt2BV(32, in)))
+
+    solver.assertCnstr(z3.mkNot(
+      z3.mkEq(out, z3.mkInt(value, BV32))
+    ))
+
+    val (sol, model) = solver.checkAndGetModel
+
+    (sol, model) should equal((Some(false), null))
+
+    z3.delete
+  }
+}
+
diff --git a/src/test/scala/z3/scala/IntExtraction.scala b/src/test/scala/z3/scala/IntExtraction.scala
new file mode 100644
index 0000000..cfdccfd
--- /dev/null
+++ b/src/test/scala/z3/scala/IntExtraction.scala
@@ -0,0 +1,26 @@
+package z3.scala
+
+import org.scalatest.{FunSuite, Matchers}
+
+class IntExtraction extends FunSuite with Matchers {
+
+  test(s"BigInt extraction") {
+    val z3 = new Z3Context("MODEL" -> true)
+
+    val i = z3.mkIntSort
+    val x = z3.mkConst(z3.mkStringSymbol("x"), i)
+    val m = z3.mkInt(Int.MaxValue, i)
+
+    val solver = z3.mkSolver
+
+    solver.assertCnstr(z3.mkEq(x, z3.mkAdd(m, m)))
+
+    val (sol, model) = solver.checkAndGetModel
+
+    sol should equal(Some(true))
+    model.evalAs[BigInt](x) should equal(Some(BigInt(Int.MaxValue) * 2))
+
+    z3.delete
+  }
+}
+