From 657224fadd5b93738a03928112af69cf9efb03c2 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 16 Nov 2012 20:39:43 +0100
Subject: [PATCH] Simplification operations in TreeOps are now immune to solver
 crashes.

---
 src/main/scala/leon/purescala/TreeOps.scala   | 35 ++++++++++++-------
 .../z3/UninterpretedZ3SolverTests.scala       | 11 ++++++
 2 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 91999a014..37939efa0 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1210,37 +1210,46 @@ object TreeOps {
 
   def simplifyTautologies(solver : Solver)(expr : Expr) : Expr = {
     def pre(e : Expr) = e match {
-      case IfExpr(cond, then, elze) => solver.solve(cond) match {
-        case Some(true)  => then
-        case Some(false) => solver.solve(Not(cond)) match {
-          case Some(true) => elze
-          case _ => e
+
+      case IfExpr(cond, then, elze) => 
+        try {
+          solver.solve(cond) match {
+            case Some(true)  => then
+            case Some(false) => solver.solve(Not(cond)) match {
+              case Some(true) => elze
+              case _ => e
+            }
+            case None => e
+          }
+        } catch {
+          // let's give up when the solver crashes
+          case _ : Exception => e 
         }
-        case None => e
-      }
+
       case _ => e
     }
 
     simplePreTransform(pre)(expr)
   }
 
-  // NOTE : this is currently untested, use at your own risk !
-  // (or better yet, write tests for it)
-  // TODO : test and remove this header.
-  // PS
+  // This function could be made ridiculously faster by using push/pop...
   def simplifyPaths(solver : Solver)(expr : Expr) : Expr = {
-    def impliedBy(e : Expr, path : Seq[Expr]) : Boolean = {
+    def impliedBy(e : Expr, path : Seq[Expr]) : Boolean = try {
       solver.solve(Implies(And(path), e)) match {
         case Some(true) => true
         case _ => false
       }
+    } catch {
+      case _ : Exception => false
     }
 
-    def contradictedBy(e : Expr, path : Seq[Expr]) : Boolean = {
+    def contradictedBy(e : Expr, path : Seq[Expr]) : Boolean = try {
       solver.solve(Implies(And(path), Not(e))) match {
         case Some(true) => true
         case _ => false
       }
+    } catch {
+      case _ : Exception => false
     }
 
     def rec(e : Expr, path : Seq[Expr]): Expr = e match {
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index 6b015b9af..1ae79ce1d 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -45,6 +45,10 @@ class UninterpretedZ3SolverTests extends FunSuite {
   private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Int32Type, VarDecl(fx, Int32Type) :: Nil)
   fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
 
+  // g is a function that is not in the program (on purpose)
+  private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Int32Type, VarDecl(fx, Int32Type) :: Nil)
+  gDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
+
   private val minimalProgram = Program(
     FreshIdentifier("Minimal"), 
     ObjectDef(FreshIdentifier("Minimal"), Seq(
@@ -55,6 +59,7 @@ class UninterpretedZ3SolverTests extends FunSuite {
   private val x : Expr = Variable(FreshIdentifier("x").setType(Int32Type))
   private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
   private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
+  private def g(e : Expr) : Expr = FunctionInvocation(gDef, e :: Nil)
 
   private val solver = new UninterpretedZ3Solver(silentReporter)
   solver.setProgram(minimalProgram)
@@ -82,4 +87,10 @@ class UninterpretedZ3SolverTests extends FunSuite {
   // This is true, but that solver shouldn't know it.
   private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1)))
   assertUnknown(solver, unknown1)
+
+  test("Expected crash on undefined functions.") {
+    intercept[Exception] {
+      solver.solve(Equals(g(x), g(x)))
+    }
+  }
 }
-- 
GitLab