From 864bdc4a01f6ed163fc162510fad94d9d0ca6aba Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 30 Nov 2012 17:49:09 +0100
Subject: [PATCH] Do not report error in case of invalid model

---
 .../scala/leon/solvers/z3/FairZ3Solver.scala  | 13 +++-
 .../scala/leon/synthesis/DerivationTree.scala | 64 -------------------
 .../scala/leon/test/PureScalaPrograms.scala   |  5 +-
 3 files changed, 14 insertions(+), 68 deletions(-)
 delete mode 100644 src/main/scala/leon/synthesis/DerivationTree.scala

diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index f784b63fc..f91fa5d2e 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -180,9 +180,9 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
           (true, asMap)
         }
         case RuntimeError(msg) => {
-          reporter.info("- Model leads to runtime error: " + msg)
-          reporter.error(modelAsString)
-          (true, asMap)
+          reporter.info("- Invalid model")
+          //reporter.error(modelAsString)
+          (false, asMap)
         }
         case OK(BooleanLiteral(false)) => {
           reporter.info("- Invalid model.")
@@ -381,6 +381,9 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
 
         reporter.info(" - Running Z3 search...")
 
+        //reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
+        //reporter.info("Assumptions:\n"+(blockingSetAsZ3 ++ assumptionsAsZ3).mkString("  AND  "))
+
         val res = solver.checkAssumptions((blockingSetAsZ3 ++ assumptionsAsZ3) :_*)
 
         reporter.info(" - Finished search with blocked literals")
@@ -426,6 +429,8 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
 
             val core = z3CoreToCore(solver.getUnsatCore)  
 
+            reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
+
             if (!forceStop) {
               if (Settings.luckyTest) {
                 // we need the model to perform the additional test
@@ -438,8 +443,10 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
 
               res2 match {
                 case Some(false) =>
+                  //reporter.info("UNSAT WITHOUT Blockers")
                   foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
                 case Some(true) =>
+                  //reporter.info("SAT WITHOUT Blockers")
                   if (Settings.luckyTest && !forceStop) {
                     // we might have been lucky :D
                     val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
diff --git a/src/main/scala/leon/synthesis/DerivationTree.scala b/src/main/scala/leon/synthesis/DerivationTree.scala
deleted file mode 100644
index 0bf44b00e..000000000
--- a/src/main/scala/leon/synthesis/DerivationTree.scala
+++ /dev/null
@@ -1,64 +0,0 @@
-package leon
-package synthesis
-
-/*
-class DerivationTree(root: RootTask)  {
-
-  private[this] var _nextID = 0
-
-  def nextID = {
-    _nextID += 1
-    _nextID
-  }
-
-  def escapeHTML(str: String) = str.replaceAll("<", "&lt;").replaceAll(">", "&gt;")
-
-  def toDot: String = {
-    val res = new StringBuffer()
-
-    res append "digraph D {\n"
-    res append " label=\"Derivation Tree\"\n"
-//    res append " rankdir=\"LR\"\n"
-
-    var taskNames = Map[Task, String]()
-    def taskName(t: Task) = {
-      taskNames.get(t) match {
-        case Some(name) =>
-          name
-        case None =>
-          val name = "task"+nextID
-          taskNames += t -> name
-          name
-      }
-    }
-
-    def printTask(t: Task) {
-
-      val node = taskName(t);
-
-      res append " "+node+" [ label = <<TABLE BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"><TR><TD BORDER=\"0\">"+t.rule+"</TD></TR><TR><TD BGCOLOR=\"indianred1\">"+escapeHTML(t.problem.toString)+"</TD></TR><TR><TD BGCOLOR=\"greenyellow\">"+escapeHTML(t.solution.map(_.toString).getOrElse("?"))+"</TD></TR></TABLE>> shape = \"none\" ];\n"
-
-      for (st <- t.solver.map(_.allSteps).flatten.flatMap(_.subSolvers.values)) {
-        res.append(" "+taskName(st)+" -> "+node+"\n")
-        printTask(st)
-      }
-
-    }
-
-
-    root.solverTask.foreach(printTask)
-
-    res append "}\n"
-
-    res.toString
-  }
-
-  def toDotFile(fname: String) {
-    import java.io.{BufferedWriter, FileWriter}
-    val out = new BufferedWriter(new FileWriter(fname))
-    out.write(toDot)
-    out.close()
-  }
-
-}
-*/
diff --git a/src/test/scala/leon/test/PureScalaPrograms.scala b/src/test/scala/leon/test/PureScalaPrograms.scala
index 92fbb68eb..f6241e682 100644
--- a/src/test/scala/leon/test/PureScalaPrograms.scala
+++ b/src/test/scala/leon/test/PureScalaPrograms.scala
@@ -21,11 +21,14 @@ class PureScalaPrograms extends FunSuite {
   private def mkTest(file : File)(block: Output=>Unit) = {
     val fullName = file.getPath()
     val start = fullName.indexOf("regression")
+    val displayName = file.getAbsolutePath()
+/*
     val displayName = if(start != -1) {
       fullName.substring(start, fullName.length)
     } else {
       fullName
     }
+    */
 
     test("PureScala program %3d: [%s]".format(nextInt(), displayName)) {
       assert(file.exists && file.isFile && file.canRead,
@@ -67,7 +70,7 @@ class PureScalaPrograms extends FunSuite {
   forEachFileIn("regression/verification/purescala/valid") { output =>
     val Output(report, reporter) = output
     assert(report.totalConditions === report.totalValid,
-           "All verification conditions should be valid.")
+           "All verification conditions ("+report.totalConditions+") should be valid.")
     assert(reporter.errorCount === 0)
     assert(reporter.warningCount === 0)
   }
-- 
GitLab