From 5c4571d369cfc6212e94db2d733419a70980a2b0 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 10 Nov 2016 18:05:33 +0100
Subject: [PATCH] Tip printing-parsing tests
---
src/it/scala/inox/tip/TipPrintingSuite.scala | 48 +++++++++++++++++++
...{TIPTestSuite.scala => TipTestSuite.scala} | 6 +--
2 files changed, 51 insertions(+), 3 deletions(-)
create mode 100644 src/it/scala/inox/tip/TipPrintingSuite.scala
rename src/it/scala/inox/tip/{TIPTestSuite.scala => TipTestSuite.scala} (78%)
diff --git a/src/it/scala/inox/tip/TipPrintingSuite.scala b/src/it/scala/inox/tip/TipPrintingSuite.scala
new file mode 100644
index 000000000..8eb71ef04
--- /dev/null
+++ b/src/it/scala/inox/tip/TipPrintingSuite.scala
@@ -0,0 +1,48 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package tip
+
+import org.scalatest._
+
+class TipPrintingSuite extends FunSuite with ResourceUtils {
+ import inox.trees._
+
+ val ctx = TestContext.empty
+
+ val files = resourceFiles("regression/tip/SAT", _.endsWith(".tip")).toList ++
+ resourceFiles("regression/tip/UNSAT", _.endsWith(".tip"))
+
+ private def checkScript(syms: Symbols, expr: Expr): Unit = {
+ for (fd <- syms.functions.values) {
+ assert(fd.fullBody.getType(syms) != Untyped)
+ }
+
+ assert(expr.getType(syms) != Untyped)
+ }
+
+ for (file <- files) {
+ test(s"Parsing file ${file.getName}") {
+ for ((syms, expr) <- new Parser(file).parseScript) {
+ checkScript(syms, expr)
+ }
+ }
+
+ test(s"Re-printing file ${file.getName}") {
+ for ((syms, expr) <- new Parser(file).parseScript) {
+ val program = InoxProgram(ctx, syms)
+
+ val file = java.io.File.createTempFile("test-output", ".tip")
+ val fw = new java.io.FileWriter(file, false)
+ val printer = new Printer(program, fw)
+ printer.printScript(expr)
+ printer.emit(smtlib.parser.Commands.CheckSat())
+ printer.free()
+
+ val Seq((newSyms, newExpr)) = new Parser(file).parseScript
+ file.delete()
+ checkScript(newSyms, newExpr)
+ }
+ }
+ }
+}
diff --git a/src/it/scala/inox/tip/TIPTestSuite.scala b/src/it/scala/inox/tip/TipTestSuite.scala
similarity index 78%
rename from src/it/scala/inox/tip/TIPTestSuite.scala
rename to src/it/scala/inox/tip/TipTestSuite.scala
index ae2aae5b8..21a603a82 100644
--- a/src/it/scala/inox/tip/TIPTestSuite.scala
+++ b/src/it/scala/inox/tip/TipTestSuite.scala
@@ -6,13 +6,13 @@ package tip
import solvers._
import org.scalatest._
-class TIPTestSuite extends FunSuite with ResourceUtils {
+class TipTestSuite extends FunSuite with ResourceUtils {
val ctx = TestContext.empty
for (file <- resourceFiles("regression/tip/SAT", _.endsWith(".tip"))) {
test(s"SAT - ${file.getName}") {
- for ((syms, expr) <- new tip.Parser(file).parseScript) {
+ for ((syms, expr) <- new Parser(file).parseScript) {
val program = InoxProgram(ctx, syms)
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr).isSAT)
}
@@ -21,7 +21,7 @@ class TIPTestSuite extends FunSuite with ResourceUtils {
for (file <- resourceFiles("regression/tip/UNSAT", _.endsWith(".tip"))) {
test(s"UNSAT - ${file.getName}") {
- for ((syms, expr) <- new tip.Parser(file).parseScript) {
+ for ((syms, expr) <- new Parser(file).parseScript) {
val program = InoxProgram(ctx, syms)
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr).isUNSAT)
}
--
GitLab