No commit message

No commit message

src/purescala/Analysis.scala

@@ -68,19 +68,23 @@ class Analysis(val program: Program) {
         if(vc != BooleanLiteral(true)) {
           reporter.info("Verification condition (post) for " + funDef.id + ":")
           reporter.info(vc)
-
-          if(Settings.runDefaultExtensions) {
-          }
+          // reporter.info("Negated:")
+          // reporter.info(negate(vc))
+          // reporter.info("Negated, expanded:")
+          // reporter.info(expandLets(negate(vc)))
 
           // try all solvers until one returns a meaningful answer
           solverExtensions.find(se => {
-            reporter.info("Trying with solver: " + se.description)
+            reporter.info("Trying with solver: " + se.shortDescription)
             se.solve(vc) match {
-              case None => reporter.warning("UNKNOWN"); false
+              case None => false
               case Some(true) => reporter.info("VALID"); true
               case Some(false) => reporter.error("INVALID"); true
             }
-          })
+          }) match {
+            case None => reporter.warning("No solver could prove or disprove the verification condition.")
+            case _ => 
+          } 
         }
       } else {
         if(funDef.postcondition.isDefined) {
@@ -107,6 +111,16 @@ class Analysis(val program: Program) {
   }
 
   def rewritePatternMatching(expr: Expr) : Expr = {
-    expr
+    def isPMExpr(e: Expr) : Boolean = e match {
+      case MatchExpr(_, _) => true
+      case _ => false
+    }
+
+    def rewritePM(e: Expr) : Expr = e match {
+      case m @ MatchExpr(_, _) => m
+      case _ => e
+    }
+
+    replace(isPMExpr, rewritePM, expr)
   }
 }

src/purescala/Extensions.scala

@@ -5,8 +5,8 @@ import purescala.Definitions._
 
 object Extensions {
   sealed abstract class Extension(reporter: Reporter) {
-    val description: String
-    val shortDescription: String = description
+    def description: String
+    def shortDescription: String = description
   }
 
   abstract class Solver(reporter: Reporter) extends Extension(reporter) {

src/purescala/Trees.scala

@@ -125,15 +125,33 @@ object Trees {
   case class CaseClassSelector(caseClass: Expr, selector: Identifier) extends Expr
 
   /* Arithmetic */
-  case class Plus(lhs: Expr, rhs: Expr) extends Expr
-  case class Minus(lhs: Expr, rhs: Expr) extends Expr 
-  case class UMinus(expr: Expr) extends Expr 
-  case class Times(lhs: Expr, rhs: Expr) extends Expr 
-  case class Division(lhs: Expr, rhs: Expr) extends Expr 
-  case class LessThan(lhs: Expr, rhs: Expr) extends Expr 
-  case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr 
-  case class LessEquals(lhs: Expr, rhs: Expr) extends Expr 
-  case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr 
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+    val fixedType = Int32Type
+  }
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr with FixedType { 
+    val fixedType = Int32Type
+  }
+  case class UMinus(expr: Expr) extends Expr with FixedType { 
+    val fixedType = Int32Type
+  }
+  case class Times(lhs: Expr, rhs: Expr) extends Expr with FixedType { 
+    val fixedType = Int32Type
+  }
+  case class Division(lhs: Expr, rhs: Expr) extends Expr with FixedType { 
+    val fixedType = Int32Type
+  }
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr with FixedType { 
+    val fixedType = BooleanType
+  }
+  case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr with FixedType { 
+    val fixedType = BooleanType
+  }
+  case class LessEquals(lhs: Expr, rhs: Expr) extends Expr with FixedType { 
+    val fixedType = BooleanType
+  }
+  case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+    val fixedType = BooleanType
+  }
 
   /* Option expressions */
   case class OptionSome(value: Expr) extends Expr 
@@ -225,13 +243,35 @@ object Trees {
       case _ => None
     }
   }
+
+  def negate(expr: Expr) : Expr = expr match {
+    case Let(i,b,e) => Let(i,b,negate(e))
+    case Not(e) => e
+    case Iff(e1,e2) => Iff(negate(e1),e2)
+    case Implies(e1,e2) => And(e1, negate(e2))
+    case Or(exs) => And(exs.map(negate(_)))
+    case And(exs) => Or(exs.map(negate(_)))
+    case LessThan(e1,e2) => GreaterEquals(e1,e2)
+    case LessEquals(e1,e2) => GreaterThan(e1,e2)
+    case GreaterThan(e1,e2) => LessEquals(e1,e2)
+    case GreaterEquals(e1,e2) => LessThan(e1,e2)
+    case i @ IfExpr(c,e1,e2) => IfExpr(c, negate(e1), negate(e2)).setType(i.getType)
+    case _ => Not(expr)
+  }
  
   // Warning ! This may loop forever if the substitutions are not
   // well-formed!
   def replace(substs: Map[Expr,Expr], expr: Expr) : Expr = {
+    replace(substs.isDefinedAt(_), substs(_), expr)
+  }
+
+  // the replacement map should be understood as follows:
+  //   - on each subexpression, checkFun checks whether it should be replaced
+  //   - repFun is applied is checkFun succeeded
+  def replace(checkFun: Expr=>Boolean, repFun: Expr=>Expr, expr: Expr) : Expr = {
     def rec(ex: Expr) : Expr = ex match {
-      case _ if (substs.get(ex).isDefined) => {
-        val newExpr = substs(ex)
+      case _ if (checkFun(ex)) => {
+        val newExpr = repFun(ex)
         if(newExpr.getType == NoType) {
           Settings.reporter.warning("REPLACING IN EXPRESSION WITH AN UNTYPED TREE ! " + ex + " --to--> " + newExpr)
         }

src/purescala/Z3Solver.scala

@@ -15,10 +15,10 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
     z3cfg.setParamValue("MODEL", "true")
     val z3 = new Z3Context(z3cfg)
 
-    val result = toZ3Formula(z3, vc) match {
+    val result = toZ3Formula(z3, negate(vc)) match {
       case None => None // means it could not be translated
       case Some(z3f) => {
-        z3.assertCnstr(z3.mkNot(z3f))
+        z3.assertCnstr(z3f)
         //z3.print
         z3.checkAndGetModel() match {
           case (Some(true),m) => {