diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 4ebb7c93d233850e28f9db78e8e562b867a23e11..19cc7e932be34bd2fb7a4aa9baa900dba17e6801 100644
--- a/src/purescala/Analysis.scala
+++ b/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)
}
}
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index b57f61a7b06f5f9add948d50adc8f208c0c36080..21d59ebc110d565bdb529d2ad965d3794b470d65 100644
--- a/src/purescala/Extensions.scala
+++ b/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) {
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 63d03f20e623b2bbe0390108ab12862e4c12e802..3dfbd84f8605546c2ee5f9129d5748f75315c291 100644
--- a/src/purescala/Trees.scala
+++ b/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)
}
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 966d9cded788ed48e11e77d015c509596f8d3f10..c151521ba96ee18446034bb37952f52b20ef1407 100644
--- a/src/purescala/Z3Solver.scala
+++ b/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) => {